src/constraint.c

   1 /*
   2 ** constraintList.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 "aliasChecks.h"
  15 # include "exprNodeSList.h"
  16 //# include "exprData.i"
  17
  18 /*@i33*/
  19 /*@-fcnuse*/
  20 /*@-assignexpose*/
  21
  22 /*@notnull@*/ constraint constraint_makeNew (void);
  23
  24
  25 constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
  26
  27 {
  28   char *t;
  29   int c;
  30   constraint ret;
  31   ret = constraint_makeNew();
  32   llassert (sRef_isValid(x) );
  33   if (!sRef_isValid(x))
  34     return ret;
  35
  36
  37   ret->lexpr = constraintExpr_makeTermsRef (x);
  38   #warning fix abstraction
  39
  40   if (relOp.tok == GE_OP)
  41       ret->ar = GTE;
  42   else if (relOp.tok == LE_OP)
  43     ret->ar = LTE;
  44   else if (relOp.tok == EQ_OP)
  45     ret->ar = EQ;
  46   else
  47     llfatalbug(message ("Unsupported relational operator") );
  48
  49
  50   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  51   c = atoi( t );
  52   ret->expr = constraintExpr_makeIntLiteral (c);
  53
  54   ret->post = TRUE;
  55   //  ret->orig = ret;
  56   DPRINTF(("GENERATED CONSTRAINT:"));
  57   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  58   return ret;
  59 }
  60
  61 constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
  62
  63 {
  64   char *t;
  65   int c;
  66   constraint ret;
  67   ret = constraint_makeNew();
  68   llassert (l!=NULL);
  69   if (!l)
  70     return ret;
  71
  72
  73   ret->lexpr = constraintExpr_copy (l);
  74   #warning fix abstraction
  75
  76   if (relOp.tok == GE_OP)
  77       ret->ar = GTE;
  78   else if (relOp.tok == LE_OP)
  79     ret->ar = LTE;
  80   else if (relOp.tok == EQ_OP)
  81     ret->ar = EQ;
  82   else
  83   llfatalbug(message("Unsupported relational operator") );
  84
  85
  86   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  87   c = atoi( t );
  88   ret->expr = constraintExpr_makeIntLiteral (c);
  89
  90   ret->post = TRUE;
  91   //  ret->orig = ret;
  92   DPRINTF(("GENERATED CONSTRAINT:"));
  93   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  94   return ret;
  95 }
  96
  97
  98 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
  99 {
 100   constraint ret;
 101   ret = constraint_makeNew();
 102   llassert (l !=NULL);
 103   if (!l)
 104     return ret;
 105
 106
 107   ret->lexpr = constraintExpr_copy (l);
 108   #warning fix abstraction
 109
 110   if (relOp.tok == GE_OP)
 111       ret->ar = GTE;
 112   else if (relOp.tok == LE_OP)
 113     ret->ar = LTE;
 114   else if (relOp.tok == EQ_OP)
 115     ret->ar = EQ;
 116   else
 117   llfatalbug( message("Unsupported relational operator") );
 118
 119   ret->expr = constraintExpr_copy (r);
 120
 121   ret->post = TRUE;
 122   //  ret->orig = ret;
 123   DPRINTF(("GENERATED CONSTRAINT:"));
 124   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
 125   return ret;
 126 }
 127
 128 constraint constraint_copy (constraint c)
 129 {
 130   constraint ret;
 131   ret = constraint_makeNew();
 132   ret->lexpr = constraintExpr_copy (c->lexpr);
 133   ret->ar = c->ar;
 134   ret->expr =  constraintExpr_copy (c->expr);
 135   ret->post = c->post;
 136   ret->generatingExpr = exprNode_fakeCopy(c->generatingExpr);
 137
 138   /*@i33 fix this*/
 139   if (c->orig != NULL)
 140     ret->orig = constraint_copy (c->orig);
 141   else
 142     ret->orig = NULL;
 143   return ret;
 144 }
 145
 146 /*like copy expect it doesn't allocate memory for the constraint*/
 147
 148 void constraint_overWrite (constraint c1, constraint c2)
 149 {
 150   c1->lexpr = constraintExpr_copy (c2->lexpr);
 151   c1->ar = c2->ar;
 152   c1->expr =  constraintExpr_copy (c2->expr);
 153   c1->post = c2->post;
 154   /*@i33 fix this*/
 155   if (c2->orig != NULL)
 156     c1->orig = constraint_copy (c2->orig);
 157   else
 158     c1->orig = NULL;
 159   c1->generatingExpr = exprNode_fakeCopy (c2->generatingExpr );
 160 }
 161
 162 bool constraint_resolve (/*@unused@*/ constraint c)
 163 {
 164   return FALSE;
 165 }
 166
 167
 168
 169 /*@notnull@*/ constraint constraint_makeNew (void)
 170 {
 171   constraint ret;
 172   ret = dmalloc(sizeof (*ret) );
 173   ret->lexpr = NULL;
 174   ret->expr = NULL;
 175   ret->ar = LT;
 176   ret->post = FALSE;
 177   ret->orig = NULL;
 178   ret->generatingExpr = NULL;
 179   return ret;
 180 }
 181
 182 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 183 {
 184
 185   if (c->generatingExpr == NULL)
 186     {
 187       c->generatingExpr = exprNode_fakeCopy(e);
 188       DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 189     }
 190   else
 191     {
 192       DPRINTF ((message ("Not setting generatingExpr for %s to %s", constraint_print(c), exprNode_unparse(e) )  ));
 193     }
 194   return c;
 195 }
 196
 197 fileloc constraint_getFileloc (constraint c)
 198 {
 199   if (c->generatingExpr)
 200     return (exprNode_getfileloc (c->generatingExpr) );
 201
 202   return (constraintExpr_getFileloc (c->lexpr) );
 203
 204
 205 }
 206
 207 static bool checkForMaxSet (constraint c)
 208 {
 209   if (constraintExpr_hasMaxSet(c->lexpr) || constraintExpr_hasMaxSet(c->expr) )
 210     return TRUE;
 211
 212   return FALSE;
 213 }
 214
 215 bool constraint_hasMaxSet(constraint c)
 216 {
 217   if (c->orig != NULL)
 218     {
 219       if (checkForMaxSet(c->orig) )
 220         return TRUE;
 221     }
 222
 223   return (checkForMaxSet(c) );
 224 }
 225
 226 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 227 {
 228   constraint ret = constraint_makeNew();
 229   //  constraintTerm term;
 230   po = exprNode_fakeCopy(po);
 231   ind = exprNode_fakeCopy(ind);
 232   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 233   ret->ar    = GTE;
 234   ret->expr  = constraintExpr_makeValueExpr (ind);
 235   return ret;
 236 }
 237
 238 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
 239 {
 240   constraint ret = constraint_makeNew();
 241
 242
 243   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 244   ret->ar = GTE;
 245   ret->expr =  constraintExpr_makeValueInt (ind);
 246   /*@i1*/return ret;
 247 }
 248
 249 constraint constraint_makeSRefSetBufferSize (sRef s, int size)
 250 {
 251  constraint ret = constraint_makeNew();
 252  ret->lexpr = constraintExpr_makeSRefMaxset (s);
 253  ret->ar = EQ;
 254  ret->expr =  constraintExpr_makeValueInt (size);
 255  ret->post = TRUE;
 256  /*@i1*/return ret;
 257 }
 258
 259 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 260 {
 261   constraint ret = constraint_makeNew();
 262
 263
 264   ret->lexpr = constraintExpr_makeSRefMaxset (s);
 265   ret->ar = GTE;
 266   ret->expr =  constraintExpr_makeValueInt (ind);
 267   ret->post = TRUE;
 268   /*@i1*/return ret;
 269 }
 270
 271 /* drl added 01/12/2000
 272
 273   makes the constraint: Ensures index <= MaxRead(buffer) */
 274
 275 constraint constraint_makeEnsureLteMaxRead(exprNode index, exprNode buffer)
 276 {
 277   constraint ret = constraint_makeNew();
 278
 279   ret->lexpr = constraintExpr_makeValueExpr (index);
 280   ret->ar = LTE;
 281   ret->expr = constraintExpr_makeMaxReadExpr(buffer);
 282   ret->post = TRUE;
 283   return ret;
 284 }
 285
 286 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 287 {
 288   constraint ret = constraint_makeNew();
 289
 290
 291   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 292   ret->ar = GTE;
 293   ret->expr =  constraintExpr_makeValueExpr (ind);
 294   /*@i1*/return ret;
 295 }
 296
 297
 298 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 299 {
 300   constraint ret = constraint_makeNew();
 301
 302   po = exprNode_fakeCopy(po);
 303
 304   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 305   ret->ar    = GTE;
 306   ret->expr  = constraintExpr_makeValueInt (ind);
 307   return ret;
 308 }
 309
 310 constraint constraint_makeSRefReadSafeInt (sRef s, int ind)
 311 {
 312   constraint ret = constraint_makeNew();
 313
 314
 315   ret->lexpr = constraintExpr_makeSRefMaxRead (s);
 316   ret->ar = GTE;
 317   ret->expr =  constraintExpr_makeValueInt (ind);
 318   ret->post = TRUE;
 319   /*@i1*/return ret;
 320 }
 321
 322 constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 323 {
 324   constraint ret = constraint_makeNew();
 325
 326
 327   e1 = exprNode_fakeCopy (e1);
 328   t2 = exprNode_fakeCopy (t2);
 329
 330   ret = constraint_makeReadSafeExprNode(e1, t2);
 331
 332   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 333
 334   ret->post = TRUE;
 335
 336   //  fileloc_incColumn (ret->lexpr->term->loc);
 337   return ret;
 338 }
 339
 340 static constraint constraint_makeEnsuresOpConstraintExpr (constraintExpr c1, constraintExpr c2, fileloc sequencePoint,  arithType  ar)
 341 {
 342
 343   constraint ret;
 344
 345   llassert(c1 && c2);
 346   //  llassert(sequencePoint);
 347
 348   ret = constraint_makeNew();
 349
 350   ret->lexpr = c1;
 351   ret->ar = ar;
 352   ret->post = TRUE;
 353   ret->expr =  c2;
 354   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 355   return ret;
 356 }
 357
 358 static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
 359 {
 360   constraintExpr c1, c2;
 361   constraint ret;
 362   exprNode e;
 363
 364   if (! (e1 && e2) )
 365     {
 366       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 367                        exprNode_unparse(e1), exprNode_unparse(e2) )
 368                ));
 369     }
 370
 371   //  llassert (sequencePoint);
 372
 373   e  =  exprNode_fakeCopy(e1);
 374   c1 =  constraintExpr_makeValueExpr (e);
 375
 376   e  =  exprNode_fakeCopy(e2);
 377   c2 =  constraintExpr_makeValueExpr (e);
 378
 379   ret = constraint_makeEnsuresOpConstraintExpr (c1, c2, sequencePoint, ar);
 380
 381   return ret;
 382 }
 383
 384
 385 /* make constraint ensures e1 == e2 */
 386
 387 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 388 {
 389   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
 390 }
 391
 392 /*make constraint ensures e1 < e2 */
 393 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 394 {
 395   constraintExpr t1, t2;
 396
 397   t1 = constraintExpr_makeValueExpr (e1);
 398   t2 = constraintExpr_makeValueExpr (e2);
 399
 400   /*change this to e1 <= (e2 -1) */
 401
 402   t2 = constraintExpr_makeDecConstraintExpr (t2);
 403
 404  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, LTE) );
 405 }
 406
 407 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 408 {
 409  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
 410 }
 411
 412 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 413 {
 414   constraintExpr t1, t2;
 415
 416   t1 = constraintExpr_makeValueExpr (e1);
 417   t2 = constraintExpr_makeValueExpr (e2);
 418
 419
 420   /* change this to e1 >= (e2 + 1) */
 421   t2 = constraintExpr_makeIncConstraintExpr (t2);
 422
 423
 424  return ( constraint_makeEnsuresOpConstraintExpr (t1, t2, sequencePoint, GTE) );
 425 }
 426
 427 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 428 {
 429  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
 430 }
 431
 432
 433 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 434 {
 435   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 436   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 437   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 438   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 439   return dst;
 440 }
 441
 442 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 443 {
 444   constraint ret = constraint_makeNew();
 445   //constraintTerm term;
 446
 447   e = exprNode_fakeCopy(e);
 448   ret->lexpr = constraintExpr_makeValueExpr (e);
 449   ret->ar = EQ;
 450   ret->post = TRUE;
 451   ret->expr =  constraintExpr_makeValueExpr (e);
 452   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 453
 454   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 455 //   fileloc_incColumn (  ret->lexpr->term->loc);
 456 //   fileloc_incColumn (  ret->lexpr->term->loc);
 457   return ret;
 458 }
 459 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 460 {
 461   constraint ret = constraint_makeNew();
 462   //constraintTerm term;
 463
 464   e = exprNode_fakeCopy(e);
 465   ret->lexpr = constraintExpr_makeValueExpr (e);
 466   ret->ar = EQ;
 467   ret->post = TRUE;
 468   ret->expr =  constraintExpr_makeValueExpr (e);
 469   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 470
 471   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 472 //   fileloc_incColumn (  ret->lexpr->term->loc);
 473 //   fileloc_incColumn (  ret->lexpr->term->loc);
 474   return ret;
 475 }
 476
 477
 478
 479 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 480 // {
 481 //   constraint ret = constraint_makeNew();
 482 //   //constraintTerm term;
 483
 484 //   e = exprNode_fakeCopy(e);
 485 //   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 486 //   ret->ar = EQ;
 487 //   ret->post = TRUE;
 488 //   ret->expr = constraintExpr_makeIncConstraintExpr (e);
 489 //   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
 490 //   return ret;
 491 // }
 492
 493
 494 cstring arithType_print (arithType ar) /*@*/
 495 {
 496   cstring st = cstring_undefined;
 497   switch (ar)
 498     {
 499     case LT:
 500       st = cstring_makeLiteral (" < ");
 501       break;
 502     case        LTE:
 503       st = cstring_makeLiteral (" <= ");
 504       break;
 505     case        GT:
 506       st = cstring_makeLiteral (" > ");
 507       break;
 508     case        GTE:
 509       st = cstring_makeLiteral (" >= ");
 510       break;
 511     case        EQ:
 512       st = cstring_makeLiteral (" == ");
 513       break;
 514     case        NONNEGATIVE:
 515       st = cstring_makeLiteral (" NONNEGATIVE ");
 516       break;
 517     case        POSITIVE:
 518       st = cstring_makeLiteral (" POSITIVE ");
 519       break;
 520     default:
 521       llassert(FALSE);
 522       break;
 523     }
 524   return st;
 525 }
 526
 527 void constraint_printError (constraint c, fileloc loc)
 528 {
 529   cstring string;
 530   fileloc errorLoc;
 531
 532   string = constraint_printDetailed (c);
 533
 534   errorLoc = loc;
 535
 536   if (constraint_getFileloc(c) )
 537     /*@-branchstate@*/
 538       errorLoc = constraint_getFileloc(c);
 539   /*@=branchstate@*/
 540
 541   if (c->post)
 542     {
 543        voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 544     }
 545   else
 546     {
 547       voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
 548     }
 549
 550 }
 551
 552 cstring  constraint_printDetailed (constraint c)
 553 {
 554   cstring st = cstring_undefined;
 555
 556
 557   if (!c->post)
 558     {
 559     if (c->orig != NULL)
 560       st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
 561     else
 562       st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
 563
 564     }
 565   else
 566     {
 567       if (c->orig != NULL)
 568         st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
 569       else
 570         st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
 571     }
 572
 573   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 574     {
 575       cstring temp;
 576       // llassert (c->generatingExpr);
 577       temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 578                       exprNode_unparse(c->generatingExpr) );
 579       st = cstring_concat (st, temp);
 580
 581       if (constraint_hasMaxSet(c) )
 582         {
 583           cstring temp2;
 584           temp2 = message ("\nHas MaxSet\n");
 585           st = cstring_concat (st, temp2);
 586         }
 587     }
 588   return st;
 589 }
 590
 591 cstring  constraint_print (constraint c) /*@*/
 592 {
 593   cstring st = cstring_undefined;
 594   cstring type = cstring_undefined;
 595   llassert (c !=NULL);
 596   if (c->post)
 597     {
 598       type = cstring_makeLiteral ("Ensures: ");
 599     }
 600   else
 601     {
 602       type = cstring_makeLiteral ("Requires: ");
 603     }
 604   st = message ("%s: %s %s %s",
 605                 type,
 606                 constraintExpr_print (c->lexpr),
 607                 arithType_print(c->ar),
 608                 constraintExpr_print(c->expr)
 609                 );
 610   return st;
 611 }
 612
 613 /*@only@*/ constraint constraint_doSRefFixBaseParam (/*@returned@*/ /*@only@*/ constraint precondition,
 614                                                    exprNodeList arglist)
 615 {
 616   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 617                                                            arglist);
 618   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 619                                                            arglist);
 620
 621   return precondition;
 622 }
 623
 624
 625 constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
 626 {
 627   postcondition = constraint_copy (postcondition);
 628   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
 629   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
 630
 631   return postcondition;
 632 }
 633
 634 constraint constraint_doSRefFixConstraintParam (constraint precondition,
 635                                                    exprNodeList arglist)
 636 {
 637
 638   precondition = constraint_copy (precondition);
 639   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
 640   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 641
 642   return precondition;
 643 }
 644
 645 // bool constraint_hasTerm (constraint c, constraintTerm term)
 646 // {
 647 //   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 648
 649 //   if (constraintExpr_includesTerm (c->lexpr, term) )
 650 //     return TRUE;
 651
 652 //   if (constraintExpr_includesTerm (c->expr, term) )
 653 //     return TRUE;
 654
 655 //   return FALSE;
 656 // }
 657
 658 /*@only@*/ constraint constraint_preserveOrig (/*@returned@*/ /*@only@*/ constraint c) /*@modifies c @*/
 659 {
 660   c->orig = constraint_copy (c);
 661   return c;
 662 }
 663 /*@=fcnuse*/
 664 /*@=assignexpose*/
 665 /*@=czechfcns@*/