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_copy (constraint c)
  21 {
  22   constraint ret;
  23   ret = constraint_makeNew();
  24   ret->c1 = c->c1;
  25   ret->t1 = c->t1;
  26   ret->ar = c->ar;
  27   ret->e1 = c->e1;
  28   ret->post = c->post;
  29   return ret;
  30 }
  31
  32 bool constraint_resolve (/*@unused@*/ constraint c)
  33 {
  34   return FALSE;
  35 }
  36
  37 /*@notnull@*/
  38 /*@special@*/ constraint constraint_makeNew (void)
  39      /*@post:isnull result->t1, result->e1, result->c1@*/
  40      /*@defines result->ar, result->post@*/
  41 {
  42   constraint ret;
  43   ret = dmalloc(sizeof (*ret) );
  44   ret->t1 = NULL;
  45   ret->e1 = NULL;
  46   ret->c1 = NULL;
  47   ret->ar = LT;
  48   ret->post = FALSE;
  49   /*@i23*/return ret;
  50 }
  51 /*@-czechfcns@*/
  52
  53 /*@out@*/ constraintTerm new_constraintTermExpr (void)
  54 {
  55   constraintTerm ret;
  56   ret = dmalloc (sizeof (* ret ) );
  57
  58   return ret;
  59 }
  60
  61 constraintTerm exprNode_makeConstraintTerm (/*@only@*/ exprNode e)
  62 {
  63   constraintTerm ret = new_constraintTermExpr();
  64   ret->loc =  exprNode_getfileloc(e);
  65   ret->value.expr = e;
  66   ret->kind = EXPRNODE;
  67   return ret;
  68 }
  69
  70
  71 constraintTerm intLit_makeConstraintTerm (int i)
  72 {
  73   constraintTerm ret = new_constraintTermExpr();
  74   ret->value.intlit = i;
  75   ret->kind = INTLITERAL;
  76   ret->loc =  fileloc_undefined;
  77   return ret;
  78 }
  79
  80
  81 /*@special@*/ constraintExpr makeConstraintExpr (/*@only@*/ /*@notnull@*/ constraintTerm term)
  82  /*@post:isnull result->e1@*/
  83      /*@post:notnull result->t1@*/
  84      /*@defines result->e1, result->t1, result->c1@, result->op*/
  85 {
  86   constraintExpr ret;
  87   ret = dmalloc (sizeof (*ret) );
  88   ret->t1 = term;
  89   ret->e1 = NULL;
  90   ret->c1 = UNDEFINED;
  91   ret->op = PLUS;
  92   return ret;
  93 }
  94
  95
  96  constraintExpr makeConstraintExprIntlit (int i)
  97 {
  98   constraintExpr ret;
  99   ret = dmalloc (sizeof (*ret) );
 100   ret->t1 = intLit_makeConstraintTerm (i);
 101   ret->e1 = NULL;
 102   ret->c1 = VALUE;
 103   ret->op = PLUS;
 104   /*@i1*/ return ret;
 105 }
 106
 107
 108 /*@i33*/
 109 /*@null@*/ constraint constraint_makeReadSafeExprNode ( exprNode po, exprNode ind)
 110 {
 111   constraint ret = constraint_makeNew();
 112   constraintTerm term;
 113   po = exprNode_fakeCopy(po);
 114   ind = exprNode_fakeCopy(ind);
 115   printf ("Requires maxr(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
 116           cstring_toCharsSafe ( exprNode_unparse (ind)  ) );
 117   ret->t1 = exprNode_makeConstraintTerm(po);
 118   ret->c1 = MAXREAD;
 119   ret->ar = GTE;
 120
 121   term = exprNode_makeConstraintTerm (ind);
 122
 123   ret->e1 =  makeConstraintExpr (term);
 124   ret->e1->c1 = VALUE;
 125   /*@i1*/return ret;
 126 }
 127
 128 constraint constraint_makeWriteSafeExprNode (exprNode po, exprNode ind)
 129 {
 130   constraint ret = constraint_makeNew();
 131   constraintTerm term;
 132   printf ("Requires maxw(%s) >= %s\n", cstring_toCharsSafe (exprNode_unparse (po ) ),
 133          cstring_toCharsSafe( exprNode_unparse (ind)  ) );
 134   ret->t1 = exprNode_makeConstraintTerm(po);
 135   ret->c1 = MAXSET;
 136   ret->ar = GTE;
 137
 138   term = exprNode_makeConstraintTerm(ind);
 139
 140   ret->e1 =  makeConstraintExpr (term);
 141   ret->e1->c1 = VALUE;
 142   /*@i1*/return ret;
 143 }
 144
 145
 146 constraint constraint_makeReadSafeInt (exprNode t1, int index)
 147 {
 148   constraint ret = constraint_makeNew();
 149   constraintTerm term;
 150   printf ("Ensures maxr((valueof(%s)) >= %d\n", cstring_toCharsSafe (exprNode_unparse (t1 ) ),
 151           index   );
 152   t1 = exprNode_fakeCopy(t1);
 153   ret->t1 = exprNode_makeConstraintTerm(t1);
 154   ret->c1 = MAXREAD;
 155   ret->ar = GTE;
 156   ret->post = TRUE;
 157   term = intLit_makeConstraintTerm(index);
 158
 159   ret->e1 =  makeConstraintExpr (term);
 160   ret->e1->c1 = VALUE;
 161   /*make this refer to element after preconditions */
 162   fileloc_incColumn (ret->t1->loc);
 163   /*@i1*/ return ret;
 164 }
 165
 166
 167 constraint constraint_makeEnsureMaxReadAtLeast (exprNode t1, exprNode t2, fileloc sequencePoint)
 168 {
 169   constraint ret = constraint_makeNew();
 170   constraintTerm term;
 171
 172   t1 = exprNode_fakeCopy (t1);
 173   t2 = exprNode_fakeCopy (t2);
 174
 175   ret->t1 = exprNode_makeConstraintTerm(t1);
 176
 177   if (ret->t1->loc != NULL)
 178     fileloc_free(ret->t1->loc);
 179
 180   ret->t1->loc = fileloc_copy (sequencePoint);
 181   ret->c1 = MAXREAD;
 182   ret->ar = GTE;
 183   ret->post = TRUE;
 184   term = exprNode_makeConstraintTerm (t2);
 185
 186   ret->e1 =  makeConstraintExpr (term);
 187   ret->e1->c1 = VALUE;
 188   /*make this refer to element after preconditions */
 189   fileloc_incColumn (ret->t1->loc);
 190   /*@i1*/ return ret;
 191 }
 192
 193 constraint constraint_makeEnsureMinReadAtMost (exprNode po, exprNode ind, fileloc sequencePoint)
 194 {
 195   constraint ret = constraint_makeNew();
 196   constraintTerm term;
 197
 198   po = exprNode_fakeCopy (po);
 199   ind = exprNode_fakeCopy (ind);
 200
 201   ret->t1 = exprNode_makeConstraintTerm(po);
 202   ret->c1 = MINREAD;
 203   ret->ar = LTE;
 204   ret->post = TRUE;
 205   term = exprNode_makeConstraintTerm (ind);
 206
 207   ret->e1 =  makeConstraintExpr (term);
 208   ret->e1->c1 = VALUE;
 209   /*make this refer to element after preconditions */
 210   fileloc_incColumn (ret->t1->loc);
 211   /*@i1*/ return ret;
 212 }
 213
 214 constraintExpr makePostOpInc (exprNode t1)
 215 {
 216   constraintExpr ret;
 217   constraintTerm term;
 218
 219   t1 = exprNode_fakeCopy (t1);
 220   term =   exprNode_makeConstraintTerm(t1);
 221   ret = makeConstraintExpr (term);
 222   ret->op = PLUS;
 223   ret->c1 = VALUE;
 224   ret->e1 =  makeConstraintExprIntlit (1);
 225   return ret;
 226 }
 227
 228 constraint constraint_makeSideEffectPostIncrement (exprNode t1, fileloc sequencePoint)
 229 {
 230   constraint ret = constraint_makeNew();
 231   //constraintTerm term;
 232   exprNode t2;
 233   t1 = exprNode_fakeCopy(t1);
 234   t2 = exprNode_fakeCopy(t1);
 235
 236   ret->t1 = exprNode_makeConstraintTerm(t1);
 237   ret->c1 = VALUE;
 238   ret->ar = EQ;
 239   ret->post = TRUE;
 240   ret->e1 = makePostOpInc(t2);
 241
 242   fileloc_incColumn (  ret->t1->loc);
 243   fileloc_incColumn (  ret->t1->loc);
 244
 245   /*@i6*/return ret;
 246 }
 247
 248 void constraintType_print (constraintType c1)
 249 {
 250   switch (c1)
 251     {
 252     case VALUE:
 253       printf("VALUE");
 254       break;
 255     case CALLSAFE:
 256       printf("CALLSAFE");
 257       break;
 258     case  MAXSET:
 259       printf ("MAXSET");
 260       break;
 261     case    MINSET:
 262       printf ("MINSET");
 263       break;
 264     case MAXREAD:
 265       printf ("MAXREAD");
 266       break;
 267     case MINREAD:
 268       printf ("MINREAD");
 269       break;
 270     case NULLTERMINATED:
 271       printf ("NULLTERMINATED");
 272       break;
 273     case UNDEFINED:
 274       TPRINTF(("Unhandled value for constraintType"));
 275       llassert(FALSE);
 276       break;
 277     default:
 278       TPRINTF(("Unhandled value for constraintType"));
 279       llassert(FALSE);
 280     }
 281 }
 282 void constraintTerm_print (constraintTerm term)
 283 {
 284   cstring s;
 285
 286   llassert (term != NULL);
 287   switch (term->kind)
 288     {
 289     case EXPRNODE:
 290       s = exprNode_unparse (term->value.expr);
 291       printf(" %s", cstring_toCharsSafe(s) );
 292       s = fileloc_unparse (term->loc);
 293       printf("@ %s", cstring_toCharsSafe(s) );
 294       cstring_free(s);
 295       break;
 296     case INTLITERAL:
 297     {
 298       char * buf = malloc (15);
 299       /*@i1*/snprintf (buf, 14, "intliteral(%d)", term->value.intlit);
 300       /*@i1*/ printf(" %s  ", buf);
 301       free (buf);
 302       break;
 303     }
 304     case SREF:
 305       TPRINTF( ("Not Implemented\n"));
 306       llassert(FALSE);
 307       break;
 308     }
 309     /*@-unreachable*/
 310   return;
 311   /*@=unreachable*/
 312 }
 313
 314 void arithType_print (arithType ar)
 315 {
 316   switch (ar)
 317     {
 318     case LT:
 319       printf(" <  ");
 320       return;
 321     case        LTE:
 322       printf(" <= ");
 323       return;
 324     case        GT:
 325       printf(" >  ");
 326       return;
 327     case        GTE:
 328       printf(" <= ");
 329       return;
 330     case        EQ:
 331       printf(" == ");
 332       return;
 333     case        NONNEGATIVE:
 334       printf(" NONNEGATIVE ");
 335       return;
 336     case        POSITIVE:
 337       printf(" POSITIVE ");
 338       return;
 339     default:
 340       llassert(FALSE);
 341     }
 342 }
 343
 344 void constraintExpr_print (constraintExpr ex)
 345 {
 346   llassert (ex != NULL);
 347   constraintType_print (ex->c1 );
 348   constraintTerm_print (ex->t1);
 349   if (ex->e1 != NULL)
 350     {
 351       if (ex->op == PLUS)
 352         {
 353           printf(" + ");
 354         }
 355       else
 356         {
 357           printf (" - ");
 358         }
 359
 360       constraintExpr_print (ex->e1);
 361     }
 362
 363 }
 364
 365
 366 void constraint_print (constraint c)
 367 {
 368   if (c->post)
 369     {
 370       printf("Ensures: ");
 371     }
 372   else
 373     {
 374       printf("requires: ");
 375     }
 376
 377   constraintType_print (c->c1);
 378   constraintTerm_print (c->t1);
 379   arithType_print(c->ar);
 380   constraintExpr_print(c->e1);
 381   printf("\n");
 382 }
 383
 384 /*@=fcnuse*/
 385 /*@=assignexpose*/
 386 /*@=czechfcns@*/
 387