src/constraint.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2002 University of Virginia,
   4 **         Massachusetts Institute of Technology
   5 **
   6 ** This program is free software; you can redistribute it and/or modify it
   7 ** under the terms of the GNU General Public License as published by the
   8 ** Free Software Foundation; either version 2 of the License, or (at your
   9 ** option) any later version.
  10 **
  11 ** This program is distributed in the hope that it will be useful, but
  12 ** WITHOUT ANY WARRANTY; without even the implied warranty of
  13 ** MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  14 ** General Public License for more details.
  15 **
  16 ** The GNU General Public License is available from http://www.gnu.org/ or
  17 ** the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  18 ** MA 02111-1307, USA.
  19 **
  20 ** For information on splint: info@splint.org
  21 ** To report a bug: splint-bug@splint.org
  22 ** For more information: http://www.splint.org
  23 */
  24
  25 /*
  26 ** constraint.c
  27 */
  28
  29 /* #define DEBUGPRINT 1 */
  30
  31 # include <ctype.h> /* for isdigit */
  32 # include "splintMacros.nf"
  33 # include "basic.h"
  34 # include "cgrammar.h"
  35 # include "cgrammar_tokens.h"
  36
  37 # include "exprChecks.h"
  38 # include "exprNodeSList.h"
  39
  40 /*@i33*/
  41
  42 /*@access exprNode@*/ /* !!! NO! Don't do this recklessly! */
  43 /*@-nullderef@*/ /* !!! DRL needs to fix this code! */
  44 /*@-nullstate@*/ /* !!! DRL needs to fix this code! */
  45 /*@-temptrans@*/ /* !!! DRL needs to fix this code! */
  46
  47 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint p_c);
  48
  49
  50 static /*@notnull@*/ /*@special@*/ constraint constraint_makeNew (void)
  51      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
  52      /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/;
  53
  54 static void
  55 advanceField (char **s)
  56 {
  57   reader_checkChar (s, '@');
  58 }
  59
  60 # if 0
  61 static constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
  62 {
  63   char *t;
  64   int c;
  65   constraint ret;
  66   ret = constraint_makeNew ();
  67   llassert (constraintExpr_isDefined (l));
  68
  69   ret->lexpr = constraintExpr_copy (l);
  70
  71
  72   if (relOp.tok == GE_OP)
  73       ret->ar = GTE;
  74   else if (relOp.tok == LE_OP)
  75     ret->ar = LTE;
  76   else if (relOp.tok == EQ_OP)
  77     ret->ar = EQ;
  78   else
  79   llfatalbug (message ("Unsupported relational operator"));
  80
  81
  82   t =  cstring_toCharsSafe (exprNode_unparse (cconstant));
  83   c = atoi ( t);
  84   ret->expr = constraintExpr_makeIntLiteral (c);
  85
  86   ret->post = TRUE;
  87   DPRINTF (("GENERATED CONSTRAINT:"));
  88   DPRINTF ((message ("%s", constraint_print (ret))));
  89   return ret;
  90 }
  91 # endif
  92
  93 bool constraint_same (constraint c1, constraint c2)
  94 {
  95   llassert (c1 != NULL);
  96   llassert (c2 != NULL);
  97
  98   if (c1->ar != c2->ar)
  99     {
 100       return FALSE;
 101     }
 102
 103   if (!constraintExpr_similar (c1->lexpr, c2->lexpr))
 104     {
 105       return FALSE;
 106     }
 107
 108   if (!constraintExpr_similar (c1->expr, c2->expr))
 109     {
 110       return FALSE;
 111     }
 112
 113   return TRUE;
 114 }
 115
 116 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
 117 {
 118   constraint ret;
 119   ret = constraint_makeNew ();
 120   llassert (constraintExpr_isDefined (l));
 121
 122   ret->lexpr = constraintExpr_copy (l);
 123
 124   if (lltok_getTok (relOp) == GE_OP)
 125     {
 126       ret->ar = GTE;
 127     }
 128   else if (lltok_getTok (relOp) == LE_OP)
 129     {
 130       ret->ar = LTE;
 131     }
 132   else if (lltok_getTok (relOp) == EQ_OP)
 133     {
 134       ret->ar = EQ;
 135     }
 136   else
 137     llfatalbug ( message ("Unsupported relational operator"));
 138
 139   ret->expr = constraintExpr_copy (r);
 140
 141   ret->post = TRUE;
 142
 143   ret->orig = constraint_copy (ret);
 144
 145   ret = constraint_simplify (ret);
 146   /* ret->orig = ret; */
 147
 148   DPRINTF (("GENERATED CONSTRAINT:"));
 149   DPRINTF ((message ("%s", constraint_print (ret))));
 150   return ret;
 151 }
 152
 153 constraint constraint_copy (/*@temp@*/ /*@observer@*/ constraint c)
 154 {
 155   constraint ret;
 156
 157   llassert (constraint_isDefined (c));
 158
 159   ret = constraint_makeNew ();
 160   ret->lexpr = constraintExpr_copy (c->lexpr);
 161   ret->ar = c->ar;
 162   ret->expr =  constraintExpr_copy (c->expr);
 163   ret->post = c->post;
 164   /*@-assignexpose@*/
 165   ret->generatingExpr = c->generatingExpr;
 166   /*@=assignexpose@*/
 167
 168   /*@i33 fix this*/
 169   if (c->orig != NULL)
 170     ret->orig = constraint_copy (c->orig);
 171   else
 172     ret->orig = NULL;
 173
 174   if (c->or != NULL)
 175     ret->or = constraint_copy (c->or);
 176   else
 177     ret->or = NULL;
 178
 179   ret->fcnPre = c->fcnPre;
 180
 181   return ret;
 182 }
 183
 184 /*like copy expect it doesn't allocate memory for the constraint*/
 185
 186 void constraint_overWrite (constraint c1, constraint c2)
 187 {
 188   llassert (constraint_isDefined (c1));
 189
 190   llassert (c1 != c2);
 191
 192   DPRINTF ((message ("OverWriteing constraint %q with %q", constraint_print (c1),
 193                    constraint_print (c2))));
 194
 195   constraintExpr_free (c1->lexpr);
 196   constraintExpr_free (c1->expr);
 197
 198   c1->lexpr = constraintExpr_copy (c2->lexpr);
 199   c1->ar = c2->ar;
 200   c1->expr =  constraintExpr_copy (c2->expr);
 201   c1->post = c2->post;
 202
 203   if (c1->orig != NULL)
 204     constraint_free (c1->orig);
 205
 206   if (c2->orig != NULL)
 207     c1->orig = constraint_copy (c2->orig);
 208   else
 209     c1->orig = NULL;
 210
 211   /*@i33 make sure that the or is freed correctly*/
 212   if (c1->or != NULL)
 213     constraint_free (c1->or);
 214
 215   if (c2->or != NULL)
 216     c1->or = constraint_copy (c2->or);
 217   else
 218     c1->or = NULL;
 219
 220   c1->fcnPre = c2->fcnPre;
 221
 222   /*@-assignexpose@*/
 223   c1->generatingExpr = c2->generatingExpr;
 224   /*@=assignexpose@*/
 225 }
 226
 227
 228
 229 static /*@notnull@*/  /*@special@*/ constraint constraint_makeNew (void)
 230      /*@post:isnull result->or, result->orig,  result->generatingExpr, result->fcnPre @*/
 231      /*@defines result->or, result->generatingExpr, result->orig, result->fcnPre @*/
 232 {
 233   constraint ret;
 234   ret = dmalloc (sizeof (*ret));
 235   ret->lexpr = NULL;
 236   ret->expr = NULL;
 237   ret->ar = LT;
 238   ret->post = FALSE;
 239   ret->orig = NULL;
 240   ret->or = NULL;
 241   ret->generatingExpr = NULL;
 242   ret->fcnPre = NULL;
 243   return ret;
 244 }
 245
 246 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, /*@exposed@*/ exprNode e)
 247 {
 248
 249   if (c->generatingExpr == NULL)
 250     {
 251       c->generatingExpr = e;
 252       DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
 253     }
 254   else
 255     {
 256       DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
 257     }
 258   return c;
 259 }
 260
 261 constraint constraint_origAddGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 262 {
 263
 264   if (c->orig != constraint_undefined)
 265     {
 266       c->orig = constraint_addGeneratingExpr (c->orig, e);
 267     }
 268   else
 269     {
 270       DPRINTF ((message ("constraint_origAddGeneratingExpr: Not setting generatingExpr for %s to %s", constraint_print (c), exprNode_unparse (e)) ));
 271     }
 272   return c;
 273 }
 274
 275 constraint constraint_setFcnPre (/*@returned@*/ constraint c)
 276 {
 277
 278   if (c->orig != constraint_undefined)
 279     {
 280       c->orig->fcnPre = TRUE;
 281     }
 282   else
 283     {
 284       c->fcnPre = TRUE;
 285       DPRINTF (( message ("Warning Setting fcnPre directly")));
 286     }
 287   return c;
 288 }
 289
 290
 291
 292
 293 fileloc constraint_getFileloc (constraint c)
 294 {
 295   if (exprNode_isDefined (c->generatingExpr))
 296     return (fileloc_copy (exprNode_getfileloc (c->generatingExpr)));
 297
 298   return (constraintExpr_getFileloc (c->lexpr));
 299
 300
 301 }
 302
 303 static bool checkForMaxSet (constraint c)
 304 {
 305   if (constraintExpr_hasMaxSet (c->lexpr) || constraintExpr_hasMaxSet (c->expr))
 306     return TRUE;
 307
 308   return FALSE;
 309 }
 310
 311 bool constraint_hasMaxSet (constraint c)
 312 {
 313   if (checkForMaxSet (c))
 314     return TRUE;
 315
 316   if (c->orig != NULL)
 317     {
 318       if (checkForMaxSet (c->orig))
 319         return TRUE;
 320     }
 321
 322   return FALSE;
 323 }
 324
 325 constraint constraint_makeReadSafeExprNode (exprNode po, exprNode ind)
 326 {
 327   constraint ret = constraint_makeNew ();
 328
 329   po = po;
 330   ind = ind;
 331   ret->lexpr = constraintExpr_makeMaxReadExpr (po);
 332   ret->ar    = GTE;
 333   ret->expr  = constraintExpr_makeValueExpr (ind);
 334   ret->post = FALSE;
 335   return ret;
 336 }
 337
 338 constraint constraint_makeWriteSafeInt (   exprNode po, int ind)
 339 {
 340   constraint ret = constraint_makeNew ();
 341
 342
 343   ret->lexpr =constraintExpr_makeMaxSetExpr (po);
 344   ret->ar = GTE;
 345   ret->expr =  constraintExpr_makeIntLiteral (ind);
 346   /*@i1*/return ret;
 347 }
 348
 349 constraint constraint_makeSRefSetBufferSize (sRef s, long int size)
 350 {
 351  constraint ret = constraint_makeNew ();
 352  ret->lexpr = constraintExpr_makeSRefMaxset (s);
 353  ret->ar = EQ;
 354  ret->expr =  constraintExpr_makeIntLiteral ((int)size);
 355  ret->post = TRUE;
 356  /*@i1*/return ret;
 357 }
 358
 359 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 360 {
 361   constraint ret = constraint_makeNew ();
 362
 363
 364   ret->lexpr = constraintExpr_makeSRefMaxset ( s);
 365   ret->ar = GTE;
 366   ret->expr =  constraintExpr_makeIntLiteral (ind);
 367   ret->post = TRUE;
 368   /*@i1*/return ret;
 369 }
 370
 371 /* drl added 01/12/2000
 372
 373   makes the constraint: Ensures index <= MaxRead (buffer) */
 374
 375 constraint constraint_makeEnsureLteMaxRead (exprNode index, exprNode buffer)
 376 {
 377   constraint ret = constraint_makeNew ();
 378
 379   ret->lexpr = constraintExpr_makeValueExpr (index);
 380   ret->ar = LTE;
 381   ret->expr = constraintExpr_makeMaxReadExpr (buffer);
 382   ret->post = TRUE;
 383   return ret;
 384 }
 385
 386 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 387 {
 388   constraint ret = constraint_makeNew ();
 389
 390
 391   ret->lexpr =constraintExpr_makeMaxSetExpr (po);
 392   ret->ar = GTE;
 393   ret->expr =  constraintExpr_makeValueExpr (ind);
 394   /*@i1*/return ret;
 395 }
 396
 397
 398 constraint constraint_makeReadSafeInt ( exprNode t1, int index)
 399 {
 400   constraint ret = constraint_makeNew ();
 401
 402   ret->lexpr = constraintExpr_makeMaxReadExpr (t1);
 403   ret->ar    = GTE;
 404   ret->expr  = constraintExpr_makeIntLiteral (index);
 405   ret->post = FALSE;
 406   return ret;
 407 }
 408
 409 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 410 {
 411   constraint ret = constraint_makeNew ();
 412
 413
 414   ret->lexpr = constraintExpr_makeSRefMaxRead (s);
 415   ret->ar = GTE;
 416   ret->expr =  constraintExpr_makeIntLiteral (ind);
 417   ret->post = TRUE;
 418   /*@i1*/return ret;
 419 }
 420
 421 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
 422 {
 423   constraint ret;
 424
 425   ret = constraint_makeReadSafeExprNode (t1, t2);
 426   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 427   ret->post = TRUE;
 428
 429   return ret;
 430 }
 431
 432 static constraint constraint_makeEnsuresOpConstraintExpr (/*@only@*/ constraintExpr c1, /*@only@*/ constraintExpr c2, fileloc sequencePoint,  arithType  ar)
 433 {
 434
 435   constraint ret;
 436
 437   llassert (constraintExpr_isDefined (c1) && constraintExpr_isDefined (c2));
 438
 439   ret = constraint_makeNew ();
 440
 441   ret->lexpr = c1;
 442   ret->ar = ar;
 443   ret->post = TRUE;
 444   ret->expr =  c2;
 445   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 446   return ret;
 447 }
 448
 449 static constraint constraint_makeEnsuresOp (/*@dependent@*/ exprNode e1, /*@dependent@*/ exprNode e2, fileloc sequencePoint,  arithType  ar)
 450 {
 451   constraintExpr c1, c2;
 452   constraint ret;
 453   exprNode e;
 454
 455   if (! (exprNode_isDefined (e1) && exprNode_isDefined (e2)))
 456     {
 457       llcontbug ((message ("null exprNode, Exprnodes are %s and %s",
 458                        exprNode_unparse (e1), exprNode_unparse (e2))
 459                 ));
 460     }
 461
 462   e  =  e1;
 463   c1 =  constraintExpr_makeValueExpr (e);
 464
 465   e  =  e2;
 466   c2 =  constraintExpr_makeValueExpr (e);
 467
 468   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
 469
 470   return ret;
 471 }
 472
 473
 474 /* make constraint ensures e1 == e2 */
 475
 476 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 477 {
 478   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ));
 479 }
 480
 481 /*make constraint ensures e1 < e2 */
 482 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 483 {
 484   constraintExpr t1, t2;
 485   constraint t3;
 486
 487   t1 = constraintExpr_makeValueExpr (e1);
 488   t2 = constraintExpr_makeValueExpr (e2);
 489
 490   /*change this to e1 <= (e2 -1) */
 491
 492   t2 = constraintExpr_makeDecConstraintExpr (t2);
 493
 494   t3 =  constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE);
 495
 496   t3 = constraint_simplify(t3);
 497   return (t3);
 498 }
 499
 500 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 501 {
 502  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE));
 503 }
 504
 505 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 506 {
 507   constraintExpr t1, t2;
 508   constraint t3;
 509
 510   t1 = constraintExpr_makeValueExpr (e1);
 511   t2 = constraintExpr_makeValueExpr (e2);
 512
 513
 514   /* change this to e1 >= (e2 + 1) */
 515   t2 = constraintExpr_makeIncConstraintExpr (t2);
 516
 517   t3 =  constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE);
 518
 519   t3 = constraint_simplify(t3);
 520
 521   return t3;
 522 }
 523
 524 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 525 {
 526  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE));
 527 }
 528
 529
 530 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 531 {
 532   constraintList_free (dst->ensuresConstraints);
 533   constraintList_free (dst->requiresConstraints);
 534   constraintList_free (dst->trueEnsuresConstraints);
 535   constraintList_free (dst->falseEnsuresConstraints);
 536
 537   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints);
 538   dst->requiresConstraints = constraintList_copy (src->requiresConstraints);
 539   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints);
 540   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints);
 541   return dst;
 542 }
 543
 544 /* Makes the constraint e = e + f */
 545 constraint constraint_makeAddAssign (exprNode e, exprNode f, fileloc sequencePoint)
 546 {
 547   constraintExpr x1, x2, y;
 548   constraint ret;
 549
 550   ret = constraint_makeNew ();
 551
 552   x1 =  constraintExpr_makeValueExpr (e);
 553   x2 =  constraintExpr_copy (x1);
 554   y  =  constraintExpr_makeValueExpr (f);
 555
 556   ret->lexpr = x1;
 557   ret->ar = EQ;
 558   ret->post = TRUE;
 559   ret->expr = constraintExpr_makeAddExpr (x2, y);
 560
 561   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 562
 563   return ret;
 564 }
 565
 566
 567 /* Makes the constraint e = e - f */
 568 constraint constraint_makeSubtractAssign (exprNode e, exprNode f, fileloc sequencePoint)
 569 {
 570   constraintExpr x1, x2, y;
 571   constraint ret;
 572
 573   ret = constraint_makeNew ();
 574
 575   x1 =  constraintExpr_makeValueExpr (e);
 576   x2 =  constraintExpr_copy (x1);
 577   y  =  constraintExpr_makeValueExpr (f);
 578
 579   ret->lexpr = x1;
 580   ret->ar = EQ;
 581   ret->post = TRUE;
 582   ret->expr = constraintExpr_makeSubtractExpr (x2, y);
 583
 584   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 585
 586   return ret;
 587 }
 588
 589 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 590 {
 591   constraint ret = constraint_makeNew ();
 592
 593   ret->lexpr = constraintExpr_makeValueExpr (e);
 594   ret->ar = EQ;
 595   ret->post = TRUE;
 596   ret->expr =  constraintExpr_makeValueExpr (e);
 597   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 598   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 599   return ret;
 600 }
 601 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 602 {
 603   constraint ret = constraint_makeNew ();
 604
 605   ret->lexpr = constraintExpr_makeValueExpr (e);
 606   ret->ar = EQ;
 607   ret->post = TRUE;
 608   ret->expr =  constraintExpr_makeValueExpr (e);
 609   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 610
 611   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 612   return ret;
 613 }
 614
 615
 616 void constraint_free (/*@only@*/ constraint c)
 617 {
 618   llassert (constraint_isDefined (c));
 619
 620
 621   if (constraint_isDefined (c->orig))
 622     constraint_free (c->orig);
 623   if ( constraint_isDefined (c->or))
 624     constraint_free (c->or);
 625
 626
 627   constraintExpr_free (c->lexpr);
 628   constraintExpr_free (c->expr);
 629
 630   c->orig = NULL;
 631   c->or = NULL;
 632   c->lexpr = NULL;
 633   c->expr  = NULL;
 634
 635   free (c);
 636
 637 }
 638
 639 cstring arithType_print (arithType ar) /*@*/
 640 {
 641   cstring st = cstring_undefined;
 642   switch (ar)
 643     {
 644     case LT:
 645       st = cstring_makeLiteral ("<");
 646       break;
 647     case        LTE:
 648       st = cstring_makeLiteral ("<=");
 649       break;
 650     case        GT:
 651       st = cstring_makeLiteral (">");
 652       break;
 653     case        GTE:
 654       st = cstring_makeLiteral (">=");
 655       break;
 656     case        EQ:
 657       st = cstring_makeLiteral ("==");
 658       break;
 659     case        NONNEGATIVE:
 660       st = cstring_makeLiteral ("NONNEGATIVE");
 661       break;
 662     case        POSITIVE:
 663       st = cstring_makeLiteral ("POSITIVE");
 664       break;
 665     default:
 666       llassert (FALSE);
 667       break;
 668     }
 669   return st;
 670 }
 671
 672 void constraint_printErrorPostCondition (constraint c, fileloc loc)
 673 {
 674   cstring string;
 675   fileloc errorLoc, temp;
 676
 677   string = constraint_printDetailedPostCondition (c);
 678
 679   errorLoc = loc;
 680
 681   loc = NULL;
 682
 683   temp = constraint_getFileloc (c);
 684
 685
 686   if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
 687     {
 688       string = cstring_replaceChar(string, '\n', ' ');
 689     }
 690
 691   if (fileloc_isDefined (temp))
 692     {
 693       errorLoc = temp;
 694       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 695       fileloc_free (temp);
 696     }
 697   else
 698     {
 699       voptgenerror (  FLG_CHECKPOST, string, errorLoc);
 700     }
 701 }
 702
 703  /*drl added 8-11-001*/
 704 cstring constraint_printLocation (/*@observer@*/ /*@temp@*/ constraint c) /*@*/
 705 {
 706   cstring string, ret;
 707   fileloc errorLoc;
 708
 709   string = constraint_print (c);
 710
 711   errorLoc = constraint_getFileloc (c);
 712
 713   ret = message ("constraint: %q @ %q", string, fileloc_unparse (errorLoc));
 714
 715   fileloc_free (errorLoc);
 716   return ret;
 717
 718 }
 719
 720
 721
 722 void constraint_printError (constraint c, fileloc loc)
 723 {
 724   cstring string;
 725   fileloc errorLoc, temp;
 726
 727   bool isLikely;
 728
 729   /*drl 11/26/2001 avoid printing tautological constraints */
 730   if (constraint_isAlwaysTrue (c))
 731     {
 732       return;
 733     }
 734
 735
 736   string = constraint_printDetailed (c);
 737
 738   errorLoc = loc;
 739
 740   temp = constraint_getFileloc (c);
 741
 742   if (fileloc_isDefined (temp))
 743     {
 744       errorLoc = temp;
 745     }
 746   else
 747     {
 748       llassert (FALSE);
 749       DPRINTF (("constraint %s had undefined fileloc %s", constraint_print (c), fileloc_unparse (temp)));
 750       fileloc_free (temp);
 751       errorLoc = fileloc_copy (errorLoc);
 752     }
 753
 754
 755   if (context_getFlag (FLG_BOUNDSCOMPACTERRORMESSAGES ) )
 756     {
 757       string = cstring_replaceChar(string, '\n', ' ');
 758     }
 759
 760   /*drl added 12/19/2002 print
 761     a different error fro "likely" bounds-errors*/
 762
 763   isLikely = constraint_isConstantOnly(c);
 764
 765   if (isLikely)
 766     {
 767       if (c->post)
 768         {
 769           voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 770         }
 771       else
 772         {
 773           if (constraint_hasMaxSet (c))
 774             {
 775               voptgenerror (FLG_LIKELYBOUNDSWRITE, string, errorLoc);
 776             }
 777           else
 778             {
 779               voptgenerror (FLG_LIKELYBOUNDSREAD, string, errorLoc);
 780             }
 781         }
 782     }
 783   else if (c->post)
 784     {
 785       voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 786     }
 787   else
 788     {
 789       if (constraint_hasMaxSet (c))
 790         {
 791           voptgenerror (FLG_BOUNDSWRITE, string, errorLoc);
 792         }
 793       else
 794         {
 795           voptgenerror (FLG_BOUNDSREAD, string, errorLoc);
 796         }
 797     }
 798
 799   fileloc_free(errorLoc);
 800 }
 801
 802 static cstring constraint_printDeep (constraint c)
 803 {
 804   cstring genExpr;
 805   cstring st = cstring_undefined;
 806
 807   st = constraint_print(c);
 808
 809   if (c->orig != constraint_undefined)
 810     {
 811       st = cstring_appendChar (st, '\n');
 812       genExpr =  exprNode_unparse (c->orig->generatingExpr);
 813
 814       if (!c->post)
 815         {
 816           if (c->orig->fcnPre)
 817             {
 818               st = cstring_concatFree (st, message (" derived from %s precondition: %q",
 819                                                     genExpr, constraint_printDeep (c->orig)));
 820             }
 821           else
 822             {
 823               st = cstring_concatFree (st, message (" needed to satisfy precondition:\n%q",
 824                                                    constraint_printDeep (c->orig)));
 825             }
 826         }
 827       else
 828         {
 829           st = cstring_concatFree (st, message ("derived from: %q",
 830                                                constraint_printDeep (c->orig)));
 831         }
 832     }
 833
 834   return st;
 835 }
 836
 837
 838 static /*@only@*/ cstring  constraint_printDetailedPostCondition (/*@observer@*/ /*@temp@*/ constraint c)
 839 {
 840   cstring st = cstring_undefined;
 841   cstring genExpr;
 842
 843   st = message ("Unsatisfied ensures constraint condition:\nSplint is unable to verify the constraint %q", constraint_printDeep (c));
 844
 845   genExpr = exprNode_unparse (c->generatingExpr);
 846
 847   if (context_getFlag (FLG_CONSTRAINTLOCATION))
 848     {
 849       cstring temp;
 850
 851       temp = message ("\nOriginal Generating expression %q: %s\n",
 852                       fileloc_unparse ( exprNode_getfileloc (c->generatingExpr)),
 853                       genExpr);
 854       st = cstring_concatFree (st, temp);
 855
 856       if (constraint_hasMaxSet (c))
 857         {
 858           temp = message ("Has MaxSet\n");
 859           st = cstring_concatFree (st, temp);
 860         }
 861     }
 862   return st;
 863 }
 864
 865 cstring  constraint_printDetailed (constraint c)
 866 {
 867   cstring st = cstring_undefined;
 868   cstring temp = cstring_undefined;
 869   cstring genExpr;
 870   bool isLikely;
 871
 872   if (!c->post)
 873     {
 874       st = message ("Unable to resolve constraint:\n%q", constraint_printDeep (c));
 875     }
 876   else
 877     {
 878       st = message ("Block Post condition:\nThis function block has the post condition %q", constraint_printDeep (c));
 879     }
 880
 881   isLikely = constraint_isConstantOnly(c);
 882
 883   if (isLikely)
 884     {
 885       if (constraint_hasMaxSet (c))
 886         {
 887           temp = cstring_makeLiteral ("Likely out-of-bounds store:\n");
 888         }
 889       else
 890         {
 891           temp = cstring_makeLiteral ("Likely out-of-bounds read:\n");
 892         }
 893     }
 894   else
 895     {
 896
 897       if (constraint_hasMaxSet (c))
 898         {
 899           temp = cstring_makeLiteral ("Possible out-of-bounds store:\n");
 900         }
 901       else
 902         {
 903           temp = cstring_makeLiteral ("Possible out-of-bounds read:\n");
 904         }
 905     }
 906
 907   genExpr = exprNode_unparse (c->generatingExpr);
 908
 909   if (context_getFlag (FLG_CONSTRAINTLOCATION))
 910     {
 911       cstring temp2;
 912       temp2 = message ("%s\n", genExpr);
 913       temp = cstring_concatFree (temp, temp2);
 914     }
 915
 916   st  = cstring_concatFree (temp,st);
 917
 918   return st;
 919 }
 920
 921 /*@only@*/ cstring  constraint_print (constraint c) /*@*/
 922 {
 923   cstring st = cstring_undefined;
 924   cstring type = cstring_undefined;
 925   llassert (c !=NULL);
 926   if (c->post)
 927     {
 928       if (context_getFlag (FLG_PARENCONSTRAINT))
 929         {
 930           type = cstring_makeLiteral ("ensures: ");
 931         }
 932       else
 933         {
 934            type = cstring_makeLiteral ("ensures");
 935         }
 936     }
 937   else
 938     {
 939       if (context_getFlag (FLG_PARENCONSTRAINT))
 940         {
 941           type = cstring_makeLiteral ("requires: ");
 942         }
 943       else
 944         {
 945           type = cstring_makeLiteral ("requires");
 946         }
 947
 948     }
 949       if (context_getFlag (FLG_PARENCONSTRAINT))
 950         {
 951           st = message ("%q: %q %q %q",
 952                         type,
 953                         constraintExpr_print (c->lexpr),
 954                         arithType_print (c->ar),
 955                         constraintExpr_print (c->expr)
 956                         );
 957         }
 958       else
 959         {
 960           st = message ("%q %q %q %q",
 961                         type,
 962                         constraintExpr_print (c->lexpr),
 963                         arithType_print (c->ar),
 964                         constraintExpr_print (c->expr)
 965                 );
 966         }
 967   return st;
 968 }
 969
 970 cstring  constraint_printOr (constraint c) /*@*/
 971 {
 972   cstring ret;
 973   constraint temp;
 974
 975   ret = cstring_undefined;
 976   temp = c;
 977
 978   ret = cstring_concatFree (ret, constraint_print (temp));
 979
 980   temp = temp->or;
 981
 982   while ( constraint_isDefined (temp))
 983     {
 984       ret = cstring_concatFree (ret, cstring_makeLiteral (" OR "));
 985       ret = cstring_concatFree (ret, constraint_print (temp));
 986       temp = temp->or;
 987     }
 988
 989   return ret;
 990
 991 }
 992
 993 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
 994                                                    exprNodeList arglist)
 995 {
 996   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 997                                                            arglist);
 998   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 999                                                            arglist);
1000
1001   return precondition;
1002 }
1003
1004
1005 constraint constraint_doFixResult (constraint postcondition, /*@dependent@*/ exprNode fcnCall)
1006 {
1007   postcondition = constraint_copy (postcondition);
1008   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
1009   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
1010
1011   return postcondition;
1012 }
1013 /*Commenting out temporally
1014
1015 / *@only@* /constraint  constraint_doSRefFixInvarConstraint(constraint invar, sRef s, ctype ct )
1016 {
1017
1018   invar = constraint_copy (invar);
1019   invar->lexpr = constraintExpr_doSRefFixInvarConstraint (invar->lexpr, s, ct);
1020   invar->expr = constraintExpr_doSRefFixInvarConstraint (invar->expr, s, ct);
1021
1022   return invar;
1023 }
1024 */
1025
1026 /*@only@*/ constraint constraint_doSRefFixConstraintParam (constraint precondition,
1027                                                    exprNodeList arglist)
1028 {
1029
1030   precondition = constraint_copy (precondition);
1031   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
1032   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
1033
1034   precondition->fcnPre = FALSE;
1035   return constraint_simplify(precondition);
1036 }
1037
1038 constraint constraint_preserveOrig (/*@returned@*/ constraint c) /*@modifies c @*/
1039 {
1040
1041   DPRINTF ((message ("Doing constraint_preserverOrig for %q ", constraint_printDetailed (c))));
1042
1043   if (c->orig == constraint_undefined)
1044     c->orig = constraint_copy (c);
1045
1046   else if (c->orig->fcnPre)
1047     {
1048       constraint temp;
1049
1050       temp = c->orig;
1051
1052       /* avoid infinite loop */
1053       c->orig = NULL;
1054       c->orig = constraint_copy (c);
1055       if (c->orig->orig == NULL)
1056         {
1057           c->orig->orig = temp;
1058           temp = NULL;
1059         }
1060       else
1061         {
1062           llcontbug ((message ("Expected c->orig->orig to be null")));
1063           constraint_free (c->orig->orig);
1064           c->orig->orig = temp;
1065           temp = NULL;
1066         }
1067     }
1068   else
1069     {
1070       DPRINTF ((message ("Not changing constraint")));
1071     }
1072
1073   DPRINTF ((message ("After Doing constraint_preserverOrig for %q ", constraint_printDetailed (c))));
1074
1075   return c;
1076 }
1077 /*@=fcnuse*/
1078 /*@=assignexpose*/
1079 /*@=czechfcns@*/
1080
1081
1082 constraint constraint_togglePost (/*@returned@*/ constraint c)
1083 {
1084   c->post = !c->post;
1085   return c;
1086 }
1087
1088 constraint constraint_togglePostOrig (/*@returned@*/ constraint c)
1089 {
1090   if (c->orig != NULL)
1091     c->orig = constraint_togglePost (c->orig);
1092   return c;
1093 }
1094
1095 bool constraint_hasOrig ( /*@observer@*/ /*@temp@*/ constraint c)
1096 {
1097   if (c->orig == NULL)
1098     return FALSE;
1099   else
1100     return TRUE;
1101 }
1102
1103
1104 constraint constraint_undump (FILE *f)
1105 {
1106   constraint c;
1107   bool           fcnPre;
1108   bool post;
1109   arithType       ar;
1110
1111   constraintExpr lexpr;
1112   constraintExpr  expr;
1113
1114
1115   char * s;
1116
1117   char *os;
1118
1119   os = mstring_create (MAX_DUMP_LINE_LENGTH);
1120
1121   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1122
1123   /*@i33*/ /*this should probably be wrappered...*/
1124
1125   fcnPre = (bool) reader_getInt (&s);
1126   advanceField (&s);
1127   post = (bool) reader_getInt (&s);
1128   advanceField (&s);
1129   ar = (arithType) reader_getInt (&s);
1130
1131   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1132
1133   reader_checkChar (&s, 'l');
1134
1135   lexpr = constraintExpr_undump (f);
1136
1137   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
1138
1139   reader_checkChar (&s, 'r');
1140   expr = constraintExpr_undump (f);
1141
1142   c = constraint_makeNew ();
1143
1144   c->fcnPre = fcnPre;
1145   c->post = post;
1146   c->ar = ar;
1147
1148   c->lexpr = lexpr;
1149   c->expr =  expr;
1150
1151   free (os);
1152   c = constraint_preserveOrig (c);
1153   return c;
1154 }
1155
1156
1157 void constraint_dump (/*@observer@*/ constraint c,  FILE *f)
1158 {
1159   bool           fcnPre;
1160   bool post;
1161   arithType       ar;
1162
1163   constraintExpr lexpr;
1164   constraintExpr  expr;
1165
1166
1167   fcnPre = c->fcnPre;
1168   post   = c->post;
1169   ar     = c->ar;
1170   lexpr = c->lexpr;
1171   expr = c->expr;
1172
1173   fprintf (f, "%d@%d@%d\n", (int) fcnPre, (int) post, (int) ar);
1174   fprintf (f,"l\n");
1175   constraintExpr_dump (lexpr, f);
1176   fprintf (f,"r\n");
1177   constraintExpr_dump (expr, f);
1178 }
1179
1180
1181 int constraint_compare (/*@observer@*/ /*@temp@*/ const constraint * c1, /*@observer@*/ /*@temp@*/ const constraint * c2) /*@*/
1182 {
1183   fileloc loc1, loc2;
1184
1185   int ret;
1186
1187   llassert (constraint_isDefined (*c1));
1188   llassert (constraint_isDefined (*c2));
1189
1190   if (constraint_isUndefined (*c1))
1191     {
1192         if (constraint_isUndefined (*c2))
1193           return 0;
1194         else
1195           return 1;
1196     }
1197
1198   if (constraint_isUndefined (*c2))
1199     {
1200       return -1;
1201     }
1202
1203   loc1 = constraint_getFileloc (*c1);
1204   loc2 = constraint_getFileloc (*c2);
1205
1206   ret = fileloc_compare (loc1, loc2);
1207
1208   fileloc_free (loc1);
1209   fileloc_free (loc2);
1210
1211   return ret;
1212 }
1213
1214
1215 bool constraint_isPost  (/*@observer@*/ /*@temp@*/ constraint c)
1216 {
1217   llassert (constraint_isDefined (c));
1218
1219   if (constraint_isUndefined (c))
1220     return FALSE;
1221
1222   return (c->post);
1223 }
1224
1225
1226 static int constraint_getDepth (/*@observer@*/ /*@temp@*/ constraint c)
1227 {
1228   int l , r;
1229
1230   l = constraintExpr_getDepth (c->lexpr);
1231   r = constraintExpr_getDepth (c->expr);
1232
1233   if (l > r)
1234     {
1235       DPRINTF (( message ("constraint depth returning %d for %s", l, constraint_print (c))));
1236       return l;
1237     }
1238   else
1239     {
1240       DPRINTF (( message ("constraint depth returning %d for %s", r, constraint_print (c))));
1241       return r;
1242     }
1243 }
1244
1245
1246 bool constraint_tooDeep (/*@observer@*/ /*@temp@*/ constraint c)
1247 {
1248   int temp;
1249
1250   temp = constraint_getDepth (c);
1251
1252   if (temp >= 20)
1253     {
1254       return TRUE;
1255     }
1256
1257   return FALSE;
1258
1259 }
1260
1261 /*drl added 12/19/2002*/
1262 /*whether constraints consist only of
1263   terms which are constants*/
1264 bool constraint_isConstantOnly (constraint c)
1265 {
1266   bool l, r;
1267
1268   l = constraintExpr_isConstantOnly(c->lexpr);
1269   r = constraintExpr_isConstantOnly(c->expr);
1270
1271   if (l && r)
1272     {
1273       return TRUE;
1274     }
1275
1276   else
1277     {
1278       return FALSE;
1279     }
1280
1281 }