src/constraint.c

   1 /*
   2 ** constraintList.c
   3 */
   4
   5 # include <ctype.h> /* for isdigit */
   6 # include "lclintMacros.nf"
   7 # include "basic.h"
   8 # include "cgrammar.h"
   9 # include "cgrammar_tokens.h"
  10
  11 # include "exprChecks.h"
  12 # include "aliasChecks.h"
  13 # include "exprNodeSList.h"
  14 # include "exprData.i"
  15
  16 /*@i33*/
  17 /*@-fcnuse*/
  18 /*@-assignexpose*/
  19
  20 /*@notnull@*/
  21 /*@special@*/ constraint constraint_makeNew (void)
  22      /*@post:isnull result->term, result->expr, result->constrType@*/
  23      /*@defines result->ar, result->post@*/;
  24
  25 constraint constraint_copy (constraint c)
  26 {
  27   constraint ret;
  28   ret = constraint_makeNew();
  29   ret->lexpr = constraintExpr_copy (c->lexpr);
  30   ret->ar = c->ar;
  31   ret->expr =  constraintExpr_copy (c->expr);
  32   ret->post = c->post;
  33   /*@i33 fix this*/
  34   if (c->orig != NULL)
  35     ret->orig = constraint_copy (c->orig);
  36   else
  37     ret->orig = NULL;
  38   return ret;
  39 }
  40
  41 bool constraint_resolve (/*@unused@*/ constraint c)
  42 {
  43   return FALSE;
  44 }
  45
  46 /*@notnull@*/
  47 /*@special@*/ constraint constraint_makeNew (void)
  48      /*@post:isnull result->term, result->expr, result->constrType@*/
  49      /*@defines result->ar, result->post@*/
  50 {
  51   constraint ret;
  52   ret = dmalloc(sizeof (*ret) );
  53   ret->lexpr = NULL;
  54   ret->expr = NULL;
  55   ret->ar = LT;
  56   ret->post = FALSE;
  57   ret->orig = NULL;
  58   /*@i23*/return ret;
  59 }
  60 /*@-czechfcns@*/
  61 constraintExpr constraintExpr_alloc ()
  62 {
  63   constraintExpr ret;
  64   ret = dmalloc (sizeof (*ret) );
  65   ret->term = NULL;
  66   ret->expr = NULL;
  67   ret->op = PLUS;
  68   return ret;
  69 }
  70
  71 constraintExpr constraintExpr_copy (constraintExpr expr)
  72 {
  73   constraintExpr ret;
  74   ret = constraintExpr_alloc();
  75   ret->term = constraintTerm_copy(expr->term);
  76   ret->op   = expr->op;
  77   if (expr->expr != NULL)
  78     {
  79       ret->expr = constraintExpr_copy (expr->expr);
  80     }
  81   else
  82     {
  83       ret->expr = NULL;
  84     }
  85   return ret;
  86 }
  87
  88 constraintExpr constraintExpr_makeMaxSetExpr (exprNode expr)
  89 {
  90   constraintExpr ret;
  91   ret = constraintExpr_alloc();
  92   ret->term = constraintTerm_makeMaxSetexpr(expr);
  93   return ret;
  94 }
  95
  96 constraintExpr  constraintExpr_makeMaxReadExpr (exprNode expr)
  97 {
  98   constraintExpr ret;
  99   ret = constraintExpr_alloc();
 100   ret->term = constraintTerm_makeMaxReadexpr(expr);
 101   return ret;
 102 }
 103
 104 constraintExpr  constraintExpr_makeMinSetExpr (exprNode expr)
 105 {
 106   constraintExpr ret;
 107   ret = constraintExpr_alloc();
 108   ret->term = constraintTerm_makeMinSetexpr(expr);
 109   return ret;
 110 }
 111
 112 constraintExpr  constraintExpr_makeMinReadExpr (exprNode expr)
 113 {
 114   constraintExpr ret;
 115   ret = constraintExpr_alloc();
 116   ret->term = constraintTerm_makeMinReadexpr(expr);
 117   return ret;
 118 }
 119
 120 constraintExpr constraintExpr_makeValueExpr (exprNode expr)
 121 {
 122   constraintExpr ret;
 123   ret = constraintExpr_alloc();
 124   ret->term = constraintTerm_makeValueexpr(expr);
 125   return ret;
 126 }
 127
 128
 129 constraintExpr makeConstraintExprIntlit (int i)
 130 {
 131   constraintExpr ret;
 132   ret = dmalloc (sizeof (*ret) );
 133   ret->term = constraintTerm_makeIntLitValue(i);
 134   ret->expr = NULL;
 135   ret->op = PLUS;
 136   /*@i1*/ return ret;
 137 }
 138
 139
 140 constraintExpr constraintExpr_makeValueInt (int i)
 141 {
 142   return makeConstraintExprIntlit(i);
 143 }
 144
 145 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 146 {
 147   constraint ret = constraint_makeNew();
 148   constraintTerm term;
 149
 150   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 151   ret->ar = GTE;
 152   ret->expr =  constraintExpr_makeValueExpr (ind);
 153   /*@i1*/return ret;
 154 }
 155
 156 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 157 {
 158   constraint ret = constraint_makeNew();
 159   //  constraintTerm term;
 160   po = exprNode_fakeCopy(po);
 161   ind = exprNode_fakeCopy(ind);
 162   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 163   ret->ar    = GTE;
 164   ret->expr  = constraintExpr_makeValueExpr (ind);
 165   return ret;
 166 }
 167
 168 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
 169 {
 170   constraint ret = constraint_makeNew();
 171   constraintTerm term;
 172
 173   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 174   ret->ar = GTE;
 175   ret->expr =  constraintExpr_makeValueInt (ind);
 176   /*@i1*/return ret;
 177 }
 178
 179 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 180 {
 181   constraint ret = constraint_makeNew();
 182
 183   po = exprNode_fakeCopy(po);
 184
 185   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 186   ret->ar    = GTE;
 187   ret->expr  = constraintExpr_makeValueInt (ind);
 188   return ret;
 189 }
 190
 191 constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 192 {
 193   constraint ret = constraint_makeNew();
 194   constraintTerm term;
 195
 196   e1 = exprNode_fakeCopy (e1);
 197   t2 = exprNode_fakeCopy (t2);
 198
 199   ret = constraint_makeReadSafeExprNode(e1, t2);
 200   if (ret->lexpr->term->loc != NULL)
 201     fileloc_free(ret->lexpr->term->loc);
 202
 203   ret->lexpr->term->loc = fileloc_copy (sequencePoint);
 204   ret->post = TRUE;
 205
 206   fileloc_incColumn (ret->lexpr->term->loc);
 207   return ret;
 208 }
 209
 210
 211 constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint)
 212 {
 213   constraint ret = constraint_makeNew();
 214   constraintTerm term;
 215   po = exprNode_fakeCopy(po);
 216   ind = exprNode_fakeCopy(ind);
 217
 218   ret->lexpr = constraintExpr_makeMinReadExpr(po);
 219   ret->ar = LTE;
 220   ret->expr = constraintExpr_makeValueExpr (ind);
 221   ret->post = TRUE;
 222
 223   if (ret->lexpr->term->loc != NULL)
 224     fileloc_free(ret->lexpr->term->loc);
 225
 226   ret->lexpr->term->loc = fileloc_copy (sequencePoint);
 227   /*make this refer to element after preconditions */
 228   fileloc_incColumn (ret->lexpr->term->loc);
 229   /*@i1*/ return ret;
 230 }
 231
 232 constraintExpr makeMaxSetPostOpInc (exprNode e)
 233 {
 234   constraintExpr ret;
 235   ret = constraintExpr_makeValueExpr (e);
 236   ret->op = PLUS;
 237   ret->expr =  makeConstraintExprIntlit (1);
 238   return ret;
 239 }
 240
 241 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 242 {
 243   constraint ret = constraint_makeNew();
 244   //constraintTerm term;
 245   exprNode t2;
 246   e = exprNode_fakeCopy(e);
 247   ret->lexpr = constraintExpr_makeValueExpr (e);
 248   ret->ar = EQ;
 249   ret->post = TRUE;
 250   ret->expr = makeMaxSetPostOpInc(e);
 251
 252   fileloc_incColumn (  ret->lexpr->term->loc);
 253   fileloc_incColumn (  ret->lexpr->term->loc);
 254   return ret;
 255 }
 256
 257 constraintExpr makeMaxReadPostOpInc (exprNode e)
 258 {
 259   constraintExpr ret;
 260   ret = constraintExpr_makeValueExpr (e);
 261   ret->term  = constraintTerm_makeMaxReadexpr (e);
 262   ret->op = MINUS;
 263   ret->expr =  makeConstraintExprIntlit (1);
 264   return ret;
 265 }
 266
 267 constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 268 {
 269   constraint ret = constraint_makeNew();
 270   //constraintTerm term;
 271   exprNode t2;
 272   e = exprNode_fakeCopy(e);
 273   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 274   ret->ar = EQ;
 275   ret->post = TRUE;
 276   ret->expr = makeMaxReadPostOpInc(e);
 277
 278   fileloc_incColumn (  ret->lexpr->term->loc);
 279   fileloc_incColumn (  ret->lexpr->term->loc);
 280   return ret;
 281 }
 282
 283
 284 cstring arithType_print (arithType ar)
 285 {
 286   cstring st = cstring_undefined;
 287   switch (ar)
 288     {
 289     case LT:
 290       st = cstring_makeLiteral (" < ");
 291       break;
 292     case        LTE:
 293       st = cstring_makeLiteral (" <= ");
 294       break;
 295     case        GT:
 296       st = cstring_makeLiteral (" > ");
 297       break;
 298     case        GTE:
 299       st = cstring_makeLiteral (" >= ");
 300       break;
 301     case        EQ:
 302       st = cstring_makeLiteral (" == ");
 303       break;
 304     case        NONNEGATIVE:
 305       st = cstring_makeLiteral (" NONNEGATIVE ");
 306       break;
 307     case        POSITIVE:
 308       st = cstring_makeLiteral (" POSITIVE ");
 309       break;
 310     default:
 311       llassert(FALSE);
 312       break;
 313     }
 314   return st;
 315 }
 316
 317 cstring constraintExpr_print (constraintExpr ex)
 318 {
 319   cstring st;
 320   cstring opStr;
 321   llassert (ex != NULL);
 322
 323   st = message ("%s",
 324                 constraintTerm_print (ex->term));
 325
 326     if (ex->expr != NULL)
 327     {
 328       if (ex->op == PLUS)
 329         {
 330          opStr = cstring_makeLiteral (" + ");
 331         }
 332       else
 333         {
 334           opStr = cstring_makeLiteral (" - ");
 335         }
 336     st = message ("%s %s %s", st, opStr, constraintExpr_print (ex->expr) );
 337     }
 338   return st;
 339 }
 340
 341
 342 cstring  constraint_printDetailed (constraint c)
 343 {
 344   cstring st = cstring_undefined;
 345
 346   if (!c->post)
 347     {
 348
 349     st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) );
 350     }
 351   else
 352     {
 353     st = message ("Function Post condition:\nBased on the constraint %s this function appears to have the post condition %s", constraint_print (c), constraint_print(c->orig) );
 354     }
 355   return st;
 356 }
 357
 358 cstring  constraint_print (constraint c)
 359 {
 360   cstring st = cstring_undefined;
 361   cstring type = cstring_undefined;
 362   llassert (c);
 363   if (c->post)
 364     {
 365       type = cstring_makeLiteral ("Ensures: ");
 366     }
 367   else
 368     {
 369       type = cstring_makeLiteral ("Requires: ");
 370     }
 371   st = message ("%s: %s %s %s",
 372                 type,
 373                 constraintExpr_print (c->lexpr),
 374                 arithType_print(c->ar),
 375                 constraintExpr_print(c->expr)
 376                 );
 377   return st;
 378 }
 379
 380 bool constraint_hasTerm (constraint c, constraintTerm term)
 381 {
 382   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 383
 384   if (constraintExpr_includesTerm (c->lexpr, term) )
 385     return TRUE;
 386
 387   if (constraintExpr_includesTerm (c->expr, term) )
 388     return TRUE;
 389
 390   return FALSE;
 391 }
 392
 393 bool constraintExpr_includesTerm (constraintExpr expr, constraintTerm term)
 394 {
 395   if (constraintTerm_hasTerm (expr->term, term) )
 396     return TRUE;
 397
 398   if ( (expr->expr) != NULL)
 399     {
 400       return ( constraintExpr_includesTerm (expr->expr, term) );
 401     }
 402   return FALSE;
 403
 404 }
 405
 406 constraint constraint_preserveOrig (constraint c)
 407 {
 408   c->orig = constraint_copy (c);
 409   return c;
 410 }
 411 /*@=fcnuse*/
 412 /*@=assignexpose*/
 413 /*@=czechfcns@*/