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 constraint constraint_makeNew (void);
  21
  22
  23 constraint makeConstraintParse (sRef x, lltok relOp, exprNode cconstant)
  24
  25 {
  26   char *t;
  27   int c;
  28   constraint ret;
  29   ret = constraint_makeNew();
  30   llassert (x);
  31   if (!x)
  32     return ret;
  33
  34
  35   ret->lexpr = constraintExpr_makeTermsRef (x);
  36   #warning fix abstraction
  37
  38   if (relOp.tok == GE_OP)
  39       ret->ar = GTE;
  40   else if (relOp.tok == LE_OP)
  41     ret->ar = LTE;
  42   else if (relOp.tok == EQ_OP)
  43     ret->ar = EQ;
  44   else
  45   llfatalbug("Unsupported relational operator");
  46
  47
  48   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  49   c = atoi( t );
  50   ret->expr = constraintExpr_makeIntLiteral (c);
  51
  52   ret->post = TRUE;
  53   //  ret->orig = ret;
  54   DPRINTF(("GENERATED CONSTRAINT:"));
  55   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  56   return ret;
  57 }
  58
  59 constraint makeConstraintParse2 (constraintExpr l, lltok relOp, exprNode cconstant)
  60
  61 {
  62   char *t;
  63   int c;
  64   constraint ret;
  65   ret = constraint_makeNew();
  66   llassert (l);
  67   if (!l)
  68     return ret;
  69
  70
  71   ret->lexpr = constraintExpr_copy (l);
  72   #warning fix abstraction
  73
  74   if (relOp.tok == GE_OP)
  75       ret->ar = GTE;
  76   else if (relOp.tok == LE_OP)
  77     ret->ar = LTE;
  78   else if (relOp.tok == EQ_OP)
  79     ret->ar = EQ;
  80   else
  81   llfatalbug("Unsupported relational operator");
  82
  83
  84   t =  cstring_toCharsSafe (exprNode_unparse(cconstant));
  85   c = atoi( t );
  86   ret->expr = constraintExpr_makeIntLiteral (c);
  87
  88   ret->post = TRUE;
  89   //  ret->orig = ret;
  90   DPRINTF(("GENERATED CONSTRAINT:"));
  91   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
  92   return ret;
  93 }
  94
  95
  96 constraint makeConstraintParse3 (constraintExpr l, lltok relOp, constraintExpr r)
  97 {
  98   constraint ret;
  99   ret = constraint_makeNew();
 100   llassert (l);
 101   if (!l)
 102     return ret;
 103
 104
 105   ret->lexpr = constraintExpr_copy (l);
 106   #warning fix abstraction
 107
 108   if (relOp.tok == GE_OP)
 109       ret->ar = GTE;
 110   else if (relOp.tok == LE_OP)
 111     ret->ar = LTE;
 112   else if (relOp.tok == EQ_OP)
 113     ret->ar = EQ;
 114   else
 115   llfatalbug("Unsupported relational operator");
 116
 117   ret->expr = constraintExpr_copy (r);
 118
 119   ret->post = TRUE;
 120   //  ret->orig = ret;
 121   DPRINTF(("GENERATED CONSTRAINT:"));
 122   DPRINTF( (message ("%s", constraint_print(ret) ) ) );
 123   return ret;
 124 }
 125
 126 constraint constraint_copy (constraint c)
 127 {
 128   constraint ret;
 129   ret = constraint_makeNew();
 130   ret->lexpr = constraintExpr_copy (c->lexpr);
 131   ret->ar = c->ar;
 132   ret->expr =  constraintExpr_copy (c->expr);
 133   ret->post = c->post;
 134   /*@i33 fix this*/
 135   if (c->orig != NULL)
 136     ret->orig = constraint_copy (c->orig);
 137   else
 138     ret->orig = NULL;
 139   return ret;
 140 }
 141
 142 /*like copy expect it doesn't allocate memory for the constraint*/
 143
 144 void constraint_overWrite (constraint c1, constraint c2)
 145 {
 146   c1->lexpr = constraintExpr_copy (c2->lexpr);
 147   c1->ar = c2->ar;
 148   c1->expr =  constraintExpr_copy (c2->expr);
 149   c1->post = c2->post;
 150   /*@i33 fix this*/
 151   if (c2->orig != NULL)
 152     c1->orig = constraint_copy (c2->orig);
 153   else
 154     c1->orig = NULL;
 155
 156 }
 157
 158 bool constraint_resolve (/*@unused@*/ constraint c)
 159 {
 160   return FALSE;
 161 }
 162
 163
 164
 165 constraint constraint_makeNew (void)
 166 {
 167   constraint ret;
 168   ret = dmalloc(sizeof (*ret) );
 169   ret->lexpr = NULL;
 170   ret->expr = NULL;
 171   ret->ar = LT;
 172   ret->post = FALSE;
 173   ret->orig = NULL;
 174   /*@i23*/return ret;
 175 }
 176
 177 fileloc constraint_getFileloc (constraint c)
 178 {
 179   return (constraintExpr_getFileloc (c->lexpr) );
 180
 181
 182 }
 183
 184 constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 185 {
 186   constraint ret = constraint_makeNew();
 187   //  constraintTerm term;
 188   po = exprNode_fakeCopy(po);
 189   ind = exprNode_fakeCopy(ind);
 190   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 191   ret->ar    = GTE;
 192   ret->expr  = constraintExpr_makeValueExpr (ind);
 193   return ret;
 194 }
 195
 196 constraint constraint_makeWriteSafeInt (exprNode po, int ind)
 197 {
 198   constraint ret = constraint_makeNew();
 199
 200
 201   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 202   ret->ar = GTE;
 203   ret->expr =  constraintExpr_makeValueInt (ind);
 204   /*@i1*/return ret;
 205 }
 206
 207 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 208 {
 209   constraint ret = constraint_makeNew();
 210
 211
 212   ret->lexpr =constraintExpr_makeMaxSetExpr(po);
 213   ret->ar = GTE;
 214   ret->expr =  constraintExpr_makeValueExpr (ind);
 215   /*@i1*/return ret;
 216 }
 217
 218 constraint constraint_makeReadSafeInt ( exprNode po, int ind)
 219 {
 220   constraint ret = constraint_makeNew();
 221
 222   po = exprNode_fakeCopy(po);
 223
 224   ret->lexpr = constraintExpr_makeMaxReadExpr(po);
 225   ret->ar    = GTE;
 226   ret->expr  = constraintExpr_makeValueInt (ind);
 227   return ret;
 228 }
 229
 230 constraint constraint_makeEnsureMaxReadAtLeast (exprNode e1, exprNode t2, fileloc sequencePoint)
 231 {
 232   constraint ret = constraint_makeNew();
 233
 234
 235   e1 = exprNode_fakeCopy (e1);
 236   t2 = exprNode_fakeCopy (t2);
 237
 238   ret = constraint_makeReadSafeExprNode(e1, t2);
 239
 240   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 241
 242   ret->post = TRUE;
 243
 244   //  fileloc_incColumn (ret->lexpr->term->loc);
 245   return ret;
 246 }
 247
 248
 249 /* make constraint ensures e1 == e2 */
 250
 251 constraint constraint_makeEnsureEqual (exprNode e1, exprNode e2, fileloc sequencePoint)
 252 {
 253   constraint ret = constraint_makeNew();
 254   exprNode e;
 255
 256   e = exprNode_fakeCopy(e1);
 257   ret->lexpr = constraintExpr_makeValueExpr (e);
 258   ret->ar = EQ;
 259   ret->post = TRUE;
 260   e = exprNode_fakeCopy(e2);
 261   ret->expr =  constraintExpr_makeValueExpr (e);
 262
 263   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 264 //   fileloc_incColumn (  ret->lexpr->term->loc);
 265 //   fileloc_incColumn (  ret->lexpr->term->loc);
 266   return ret;
 267 }
 268
 269
 270 exprNode exprNode_copyConstraints (exprNode dst, exprNode src)
 271 {
 272   dst->ensuresConstraints = constraintList_copy (src->ensuresConstraints );
 273   dst->requiresConstraints = constraintList_copy (src->requiresConstraints );
 274   dst->trueEnsuresConstraints = constraintList_copy (src->trueEnsuresConstraints );
 275   dst->falseEnsuresConstraints = constraintList_copy (src->falseEnsuresConstraints );
 276   return dst;
 277 }
 278
 279 constraint constraint_makeMaxSetSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 280 {
 281   constraint ret = constraint_makeNew();
 282   //constraintTerm term;
 283
 284   e = exprNode_fakeCopy(e);
 285   ret->lexpr = constraintExpr_makeValueExpr (e);
 286   ret->ar = EQ;
 287   ret->post = TRUE;
 288   ret->expr =  constraintExpr_makeValueExpr (e);
 289   ret->expr =  constraintExpr_makeIncConstraintExpr (ret->expr);
 290
 291   ret->lexpr = constraintExpr_setFileloc (ret->lexpr, sequencePoint);
 292 //   fileloc_incColumn (  ret->lexpr->term->loc);
 293 //   fileloc_incColumn (  ret->lexpr->term->loc);
 294   return ret;
 295 }
 296
 297
 298
 299 // constraint constraint_makeMaxReadSideEffectPostIncrement (exprNode e, fileloc sequencePoint)
 300 // {
 301 //   constraint ret = constraint_makeNew();
 302 //   //constraintTerm term;
 303
 304 //   e = exprNode_fakeCopy(e);
 305 //   ret->lexpr = constraintExpr_makeMaxReadExpr(e);
 306 //   ret->ar = EQ;
 307 //   ret->post = TRUE;
 308 //   ret->expr = constraintExpr_makeIncConstraintExpr (e);
 309 //   ret->lexpr = constraintExpr_setFileLoc (ret->lexpr, sequencePoint);
 310 //   return ret;
 311 // }
 312
 313
 314 cstring arithType_print (arithType ar)
 315 {
 316   cstring st = cstring_undefined;
 317   switch (ar)
 318     {
 319     case LT:
 320       st = cstring_makeLiteral (" < ");
 321       break;
 322     case        LTE:
 323       st = cstring_makeLiteral (" <= ");
 324       break;
 325     case        GT:
 326       st = cstring_makeLiteral (" > ");
 327       break;
 328     case        GTE:
 329       st = cstring_makeLiteral (" >= ");
 330       break;
 331     case        EQ:
 332       st = cstring_makeLiteral (" == ");
 333       break;
 334     case        NONNEGATIVE:
 335       st = cstring_makeLiteral (" NONNEGATIVE ");
 336       break;
 337     case        POSITIVE:
 338       st = cstring_makeLiteral (" POSITIVE ");
 339       break;
 340     default:
 341       llassert(FALSE);
 342       break;
 343     }
 344   return st;
 345 }
 346
 347
 348 cstring  constraint_printDetailed (constraint c)
 349 {
 350   cstring st = cstring_undefined;
 351
 352   if (!c->post)
 353     {
 354     if (c->orig)
 355       st = message ("Unresolved constraint:\nLclint is unable to resolve %s needed to satisy %s", constraint_print (c), constraint_print(c->orig) );
 356     else
 357       st = message ("Unresolved constraint:\nLclint is unable to resolve %s", constraint_print (c));
 358
 359     }
 360   else
 361     {
 362       if (c->orig)
 363         st = message ("Block Post condition:\nThis function block has the post condition %s\n based on %s", constraint_print (c), constraint_print(c->orig) );
 364       else
 365         st = message ("Block Post condition:\nThis function block has the post condition %s", constraint_print (c));
 366     }
 367   return st;
 368 }
 369
 370 cstring  constraint_print (constraint c)
 371 {
 372   cstring st = cstring_undefined;
 373   cstring type = cstring_undefined;
 374   llassert (c);
 375   if (c->post)
 376     {
 377       type = cstring_makeLiteral ("Ensures: ");
 378     }
 379   else
 380     {
 381       type = cstring_makeLiteral ("Requires: ");
 382     }
 383   st = message ("%s: %s %s %s",
 384                 type,
 385                 constraintExpr_print (c->lexpr),
 386                 arithType_print(c->ar),
 387                 constraintExpr_print(c->expr)
 388                 );
 389   return st;
 390 }
 391
 392 constraint constraint_doSRefFixBaseParam (constraint precondition,
 393                                                    exprNodeList arglist)
 394 {
 395   precondition->lexpr = constraintExpr_doSRefFixBaseParam (precondition->lexpr,
 396                                                            arglist);
 397   precondition->expr = constraintExpr_doSRefFixBaseParam (precondition->expr,
 398                                                            arglist);
 399
 400   return precondition;
 401 }
 402
 403
 404 // bool constraint_hasTerm (constraint c, constraintTerm term)
 405 // {
 406 //   DPRINTF((message ("Constraint %s", constraint_print (c) ) ) );
 407
 408 //   if (constraintExpr_includesTerm (c->lexpr, term) )
 409 //     return TRUE;
 410
 411 //   if (constraintExpr_includesTerm (c->expr, term) )
 412 //     return TRUE;
 413
 414 //   return FALSE;
 415 // }
 416
 417 constraint constraint_preserveOrig (constraint c)
 418 {
 419   c->orig = constraint_copy (c);
 420   return c;
 421 }
 422 /*@=fcnuse*/
 423 /*@=assignexpose*/
 424 /*@=czechfcns@*/