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