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   /*@i33 fix this*/
 137   if (c->orig != NULL)
 138     ret->orig = constraint_copy (c->orig);
 139   else
 140     ret->orig = NULL;
 141   return ret;
 142 }
 143
 144 /*like copy expect it doesn't allocate memory for the constraint*/
 145
 146 void constraint_overWrite (constraint c1, constraint c2)
 147 {
 148   c1->lexpr = constraintExpr_copy (c2->lexpr);
 149   c1->ar = c2->ar;
 150   c1->expr =  constraintExpr_copy (c2->expr);
 151   c1->post = c2->post;
 152   /*@i33 fix this*/
 153   if (c2->orig != NULL)
 154     c1->orig = constraint_copy (c2->orig);
 155   else
 156     c1->orig = NULL;
 157
 158 }
 159
 160 bool constraint_resolve (/*@unused@*/ constraint c)
 161 {
 162   return FALSE;
 163 }
 164
 165
 166
 167 constraint constraint_makeNew (void)
 168 {
 169   constraint ret;
 170   ret = dmalloc(sizeof (*ret) );
 171   ret->lexpr = NULL;
 172   ret->expr = NULL;
 173   ret->ar = LT;
 174   ret->post = FALSE;
 175   ret->orig = NULL;
 176   /*@i23*/return ret;
 177 }
 178
 179 fileloc constraint_getFileloc (constraint c)
 180 {
 181   return (constraintExpr_getFileloc (c->lexpr) );
 182
 183
 184 }
 185
 186 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 187 {
 188   constraint ret = constraint_makeNew();
 189   //  constraintTerm term;
 190   po = exprNode_fakeCopy(po);
 191   ind = exprNode_fakeCopy(ind);
 192   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 193   ret->ar    = GTE;
 194   ret->expr  = constraintExpr_makeValueExpr (ind);
 195   return ret;
 196 }
 197
 198 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
 199 {
 200   constraint ret = constraint_makeNew();
 201
 202
 203   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 204   ret->ar = GTE;
 205   ret->expr =  constraintExpr_makeValueInt (ind);
 206   /*@i1*/return ret;
 207 }
 208
 209
 210 constraint constraint_makeSRefWriteSafeInt (sRef s, int ind)
 211 {
 212   constraint ret = constraint_makeNew();
 213
 214
 215   ret->lexpr = constraintExpr_makeSRefMaxset (s);
 216   ret->ar = GTE;
 217   ret->expr =  constraintExpr_makeValueInt (ind);
 218   ret->post = TRUE;
 219   /*@i1*/return ret;
 220 }
 221
 222
 223 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 224 {
 225   constraint ret = constraint_makeNew();
 226
 227
 228   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 229   ret->ar = GTE;
 230   ret->expr =  constraintExpr_makeValueExpr (ind);
 231   /*@i1*/return ret;
 232 }
 233
 234
 235 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 236 {
 237   constraint ret = constraint_makeNew();
 238
 239   po = exprNode_fakeCopy(po);
 240
 241   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 242   ret->ar    = GTE;
 243   ret->expr  = constraintExpr_makeValueInt (ind);
 244   return ret;
 245 }
 246
 247 constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 248 {
 249   constraint ret = constraint_makeNew();
 250
 251
 252   e1 = exprNode_fakeCopy (e1);
 253   t2 = exprNode_fakeCopy (t2);
 254
 255   ret = constraint_makeReadSafeExprNode(e1, t2);
 256
 257   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 258
 259   ret->post = TRUE;
 260
 261   //  fileloc_incColumn (ret->lexpr->term->loc);
 262   return ret;
 263 }
 264
 265
 266 static constraint constraint_makeEnsuresOp (exprNode e1, exprNode e2, fileloc sequencePoint,  arithType  ar)
 267 {
 268   constraint ret = constraint_makeNew();
 269   exprNode e;
 270
 271   e = exprNode_fakeCopy(e1);
 272   if (! (e1 && e2) )
 273     {
 274       TPRINTF((message("Warning null exprNode, Exprnodes are %s and %s",
 275                        exprNode_unparse(e1), exprNode_unparse(e2) )
 276                ));
 277     }
 278
 279   ret->lexpr = constraintExpr_makeValueExpr (e);
 280   ret->ar = ar;
 281   ret->post = TRUE;
 282   e = exprNode_fakeCopy(e2);
 283   ret->expr =  constraintExpr_makeValueExpr (e);
 284
 285   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 286   return ret;
 287 }
 288
 289
 290 /* make constraint ensures e1 == e2 */
 291
 292 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 293 {
 294   return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, EQ) );
 295 }
 296
 297 /*make constraint ensures e1 < e2 */
 298 constraint constraint_makeEnsureLessThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 299 {
 300  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LT) );
 301 }
 302
 303 constraint constraint_makeEnsureLessThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 304 {
 305  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, LTE) );
 306 }
 307
 308 constraint constraint_makeEnsureGreaterThan (exprNode e1, exprNode e2, fileloc sequencePoint)
 309 {
 310  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GT) );
 311 }
 312
 313 constraint constraint_makeEnsureGreaterThanEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 314 {
 315  return ( constraint_makeEnsuresOp (e1, e2, sequencePoint, GTE) );
 316 }
 317
 318
 319 exprNode exprNode_copyConstraints (exprNode dst, exprNode src)
 320 {
 321   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 322   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 323   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 324   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 325   return dst;
 326 }
 327
 328 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 329 {
 330   constraint ret = constraint_makeNew();
 331   //constraintTerm term;
 332
 333   e = exprNode_fakeCopy(e);
 334   ret->lexpr = constraintExpr_makeValueExpr (e);
 335   ret->ar = EQ;
 336   ret->post = TRUE;
 337   ret->expr =  constraintExpr_makeValueExpr (e);
 338   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 339
 340   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 341 //   fileloc_incColumn (  ret->lexpr->term->loc);
 342 //   fileloc_incColumn (  ret->lexpr->term->loc);
 343   return ret;
 344 }
 345
 346
 347
 348 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 349 // {
 350 //   constraint ret = constraint_makeNew();
 351 //   //constraintTerm term;
 352
 353 //   e = exprNode_fakeCopy(e);
 354 //   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 355 //   ret->ar = EQ;
 356 //   ret->post = TRUE;
 357 //   ret->expr = constraintExpr_makeIncConstraintExpr (e);
 358 //   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
 359 //   return ret;
 360 // }
 361
 362
 363 cstring arithType_print (arithType ar)
 364 {
 365   cstring st = cstring_undefined;
 366   switch (ar)
 367     {
 368     case LT:
 369       st = cstring_makeLiteral (" < ");
 370       break;
 371     case        LTE:
 372       st = cstring_makeLiteral (" <= ");
 373       break;
 374     case        GT:
 375       st = cstring_makeLiteral (" > ");
 376       break;
 377     case        GTE:
 378       st = cstring_makeLiteral (" >= ");
 379       break;
 380     case        EQ:
 381       st = cstring_makeLiteral (" == ");
 382       break;
 383     case        NONNEGATIVE:
 384       st = cstring_makeLiteral (" NONNEGATIVE ");
 385       break;
 386     case        POSITIVE:
 387       st = cstring_makeLiteral (" POSITIVE ");
 388       break;
 389     default:
 390       llassert(FALSE);
 391       break;
 392     }
 393   return st;
 394 }
 395
 396 void constraint_printError (constraint c, fileloc loc)
 397 {
 398   cstring string;
 399
 400   string = constraint_printDetailed (c);
 401
 402   if (c->post)
 403     {
 404        voptgenerror (FLG_FUNCTIONPOST, string, loc);
 405     }
 406   else
 407     {
 408       voptgenerror (FLG_FUNCTIONCONSTRAINT, string, loc);
 409     }
 410
 411 }
 412
 413 cstring  constraint_printDetailed (constraint c)
 414 {
 415   cstring st = cstring_undefined;
 416
 417
 418   if (!c->post)
 419     {
 420     if (c->orig)
 421       st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) );
 422     else
 423       st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
 424
 425     }
 426   else
 427     {
 428       if (c->orig)
 429         st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
 430       else
 431         st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
 432     }
 433   return st;
 434 }
 435
 436 cstring  constraint_print (constraint c) /*@*/
 437 {
 438   cstring st = cstring_undefined;
 439   cstring type = cstring_undefined;
 440   llassert (c);
 441   if (c->post)
 442     {
 443       type = cstring_makeLiteral ("Ensures: ");
 444     }
 445   else
 446     {
 447       type = cstring_makeLiteral ("Requires: ");
 448     }
 449   st = message ("%s: %s %s %s",
 450                 type,
 451                 constraintExpr_print (c->lexpr),
 452                 arithType_print(c->ar),
 453                 constraintExpr_print(c->expr)
 454                 );
 455   return st;
 456 }
 457
 458 constraint constraint_doSRefFixBaseParam (constraint precondition,
 459                                                    exprNodeList arglist)
 460 {
 461   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 462                                                            arglist);
 463   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 464                                                            arglist);
 465
 466   return precondition;
 467 }
 468
 469
 470 // bool constraint_hasTerm (constraint c, constraintTerm term)
 471 // {
 472 //   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 473
 474 //   if (constraintExpr_includesTerm (c->lexpr, term) )
 475 //     return TRUE;
 476
 477 //   if (constraintExpr_includesTerm (c->expr, term) )
 478 //     return TRUE;
 479
 480 //   return FALSE;
 481 // }
 482
 483 constraint constraint_preserveOrig (constraint c)
 484 {
 485   c->orig = constraint_copy (c);
 486   return c;
 487 }
 488 /*@=fcnuse*/
 489 /*@=assignexpose*/
 490 /*@=czechfcns@*/