src/constraint.c

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