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 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("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);
  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("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);
 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("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 = 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 = c2->generatingExpr;
 160 }
 161
 162 bool constraint_resolve (/*@unused@*/ constraint c)
 163 {
 164   return FALSE;
 165 }
 166
 167
 168
 169 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   /*@i23*/return ret;
 180 }
 181
 182 constraint constraint_addGeneratingExpr (/*@returned@*/ constraint c, exprNode e)
 183 {
 184
 185   if (c->generatingExpr == NULL)
 186     {
 187       c->generatingExpr = 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)
 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_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 311 {
 312   constraint ret = constraint_makeNew();
 313
 314
 315   e1 = exprNode_fakeCopy (e1);
 316   t2 = exprNode_fakeCopy (t2);
 317
 318   ret = constraint_makeReadSafeExprNode(e1, t2);
 319
 320   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 321
 322   ret->post = TRUE;
 323
 324   //  fileloc_incColumn (ret->lexpr->term->loc);
 325   return ret;
 326 }
 327
 328
 329 static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
 330 {
 331   constraint ret = constraint_makeNew();
 332   exprNode e;
 333
 334   e = exprNode_fakeCopy(e1);
 335   if (! (e1 && e2) )
 336     {
 337       llcontbug((message("null exprNode, Exprnodes are %s and %s",
 338                        exprNode_unparse(e1), exprNode_unparse(e2) )
 339                ));
 340     }
 341
 342   ret->lexpr = constraintExpr_makeValueExpr (e);
 343   ret->ar = ar;
 344   ret->post = TRUE;
 345   e = exprNode_fakeCopy(e2);
 346   ret->expr =  constraintExpr_makeValueExpr (e);
 347
 348   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 349   return ret;
 350 }
 351
 352
 353 /* make constraint ensures e1 == e2 */
 354
 355 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 356 {
 357   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
 358 }
 359
 360 /*make constraint ensures e1 < e2 */
 361 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 362 {
 363  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
 364 }
 365
 366 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 367 {
 368  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
 369 }
 370
 371 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 372 {
 373  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
 374 }
 375
 376 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 377 {
 378  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
 379 }
 380
 381
 382 exprNode exprNode_copyConstraints (/*@returned@*/ exprNode dst, exprNode src)
 383 {
 384   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 385   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 386   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 387   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 388   return dst;
 389 }
 390
 391 constraint constraint_makeMaxSetSideEffectPostDecrement (exprNode e, fileloc sequencePoint)
 392 {
 393   constraint ret = constraint_makeNew();
 394   //constraintTerm term;
 395
 396   e = exprNode_fakeCopy(e);
 397   ret->lexpr = constraintExpr_makeValueExpr (e);
 398   ret->ar = EQ;
 399   ret->post = TRUE;
 400   ret->expr =  constraintExpr_makeValueExpr (e);
 401   ret->expr =  constraintExpr_makeDecConstraintExpr (ret->expr);
 402
 403   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 404 //   fileloc_incColumn (  ret->lexpr->term->loc);
 405 //   fileloc_incColumn (  ret->lexpr->term->loc);
 406   return ret;
 407 }
 408 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 409 {
 410   constraint ret = constraint_makeNew();
 411   //constraintTerm term;
 412
 413   e = exprNode_fakeCopy(e);
 414   ret->lexpr = constraintExpr_makeValueExpr (e);
 415   ret->ar = EQ;
 416   ret->post = TRUE;
 417   ret->expr =  constraintExpr_makeValueExpr (e);
 418   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 419
 420   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 421 //   fileloc_incColumn (  ret->lexpr->term->loc);
 422 //   fileloc_incColumn (  ret->lexpr->term->loc);
 423   return ret;
 424 }
 425
 426
 427
 428 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 429 // {
 430 //   constraint ret = constraint_makeNew();
 431 //   //constraintTerm term;
 432
 433 //   e = exprNode_fakeCopy(e);
 434 //   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 435 //   ret->ar = EQ;
 436 //   ret->post = TRUE;
 437 //   ret->expr = constraintExpr_makeIncConstraintExpr (e);
 438 //   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
 439 //   return ret;
 440 // }
 441
 442
 443 cstring arithType_print (arithType ar)
 444 {
 445   cstring st = cstring_undefined;
 446   switch (ar)
 447     {
 448     case LT:
 449       st = cstring_makeLiteral (" < ");
 450       break;
 451     case        LTE:
 452       st = cstring_makeLiteral (" <= ");
 453       break;
 454     case        GT:
 455       st = cstring_makeLiteral (" > ");
 456       break;
 457     case        GTE:
 458       st = cstring_makeLiteral (" >= ");
 459       break;
 460     case        EQ:
 461       st = cstring_makeLiteral (" == ");
 462       break;
 463     case        NONNEGATIVE:
 464       st = cstring_makeLiteral (" NONNEGATIVE ");
 465       break;
 466     case        POSITIVE:
 467       st = cstring_makeLiteral (" POSITIVE ");
 468       break;
 469     default:
 470       llassert(FALSE);
 471       break;
 472     }
 473   return st;
 474 }
 475
 476 void constraint_printError (constraint c, fileloc loc)
 477 {
 478   cstring string;
 479   fileloc errorLoc;
 480
 481   string = constraint_printDetailed (c);
 482
 483   errorLoc = loc;
 484
 485   if (constraint_getFileloc(c) )
 486     errorLoc = constraint_getFileloc(c);
 487
 488
 489   if (c->post)
 490     {
 491        voptgenerror (FLG_FUNCTIONPOST, string, errorLoc);
 492     }
 493   else
 494     {
 495       voptgenerror (FLG_FUNCTIONCONSTRAINT, string, errorLoc);
 496     }
 497
 498 }
 499
 500 cstring  constraint_printDetailed (constraint c)
 501 {
 502   cstring st = cstring_undefined;
 503
 504
 505   if (!c->post)
 506     {
 507     if (c->orig)
 508       st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisfy %s", constraint_print (c), constraint_print(c->orig) );
 509     else
 510       st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
 511
 512     }
 513   else
 514     {
 515       if (c->orig)
 516         st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
 517       else
 518         st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
 519     }
 520
 521   if (context_getFlag (FLG_CONSTRAINTLOCATION) )
 522     {
 523       cstring temp;
 524       // llassert (c->generatingExpr);
 525       temp = message ("\nOriginal Generating expression %s: %s\n", fileloc_unparse( exprNode_getfileloc (c->generatingExpr) ),
 526                       exprNode_unparse(c->generatingExpr) );
 527       st = cstring_concat (st, temp);
 528
 529       if (constraint_hasMaxSet(c) )
 530         {
 531           cstring temp2;
 532           temp2 = message ("\nHas MaxSet\n");
 533           st = cstring_concat (st, temp2);
 534         }
 535     }
 536   return st;
 537 }
 538
 539 cstring  constraint_print (constraint c) /*@*/
 540 {
 541   cstring st = cstring_undefined;
 542   cstring type = cstring_undefined;
 543   llassert (c);
 544   if (c->post)
 545     {
 546       type = cstring_makeLiteral ("Ensures: ");
 547     }
 548   else
 549     {
 550       type = cstring_makeLiteral ("Requires: ");
 551     }
 552   st = message ("%s: %s %s %s",
 553                 type,
 554                 constraintExpr_print (c->lexpr),
 555                 arithType_print(c->ar),
 556                 constraintExpr_print(c->expr)
 557                 );
 558   return st;
 559 }
 560
 561 constraint constraint_doSRefFixBaseParam (constraint precondition,
 562                                                    exprNodeList arglist)
 563 {
 564   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 565                                                            arglist);
 566   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 567                                                            arglist);
 568
 569   return precondition;
 570 }
 571
 572
 573 constraint constraint_doFixResult (constraint postcondition, exprNode fcnCall)
 574 {
 575   postcondition = constraint_copy (postcondition);
 576   postcondition->lexpr = constraintExpr_doFixResult (postcondition->lexpr, fcnCall);
 577   postcondition->expr = constraintExpr_doFixResult (postcondition->expr, fcnCall);
 578
 579   return postcondition;
 580 }
 581
 582 constraint constraint_doSRefFixConstraintParam (constraint precondition,
 583                                                    exprNodeList arglist)
 584 {
 585
 586   precondition = constraint_copy (precondition);
 587   precondition->lexpr = constraintExpr_doSRefFixConstraintParam (precondition->lexpr, arglist);
 588   precondition->expr = constraintExpr_doSRefFixConstraintParam (precondition->expr, arglist);
 589
 590   return precondition;
 591 }
 592
 593 // bool constraint_hasTerm (constraint c, constraintTerm term)
 594 // {
 595 //   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 596
 597 //   if (constraintExpr_includesTerm (c->lexpr, term) )
 598 //     return TRUE;
 599
 600 //   if (constraintExpr_includesTerm (c->expr, term) )
 601 //     return TRUE;
 602
 603 //   return FALSE;
 604 // }
 605
 606 constraint constraint_preserveOrig (constraint c)
 607 {
 608   c->orig = constraint_copy (c);
 609   return c;
 610 }
 611 /*@=fcnuse*/
 612 /*@=assignexpose*/
 613 /*@=czechfcns@*/