src/constraint.c

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