src/constraintGeneration.c

   1
   2 /*
   3 ** constraintList.c
   4 */
   5
   6 //#define DEBUGPRINT 1
   7
   8 # include <ctype.h> /* for isdigit */
   9 # include "lclintMacros.nf"
  10 # include "basic.h"
  11 # include "cgrammar.h"
  12 # include "cgrammar_tokens.h"
  13
  14 # include "exprChecks.h"
  15 # include "aliasChecks.h"
  16 # include "exprNodeSList.h"
  17
  18 # include "exprData.i"
  19 //# include "exprDataQuite.i"
  20
  21 #ifndef exprNode_isError
  22 #warning wtf
  23 # define exprNode_isError(e)          ((e) == exprNode_undefined)
  24 #else
  25 #warning strange
  26 #endif
  27
  28 #define myexprNode_isError(e)        ((e) == exprNode_undefined)
  29
  30
  31
  32 bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e);
  33 static bool exprNode_handleError( exprNode p_e);
  34
  35 //static cstring exprNode_findConstraints ( exprNode p_e);
  36 static bool exprNode_isMultiStatement(exprNode p_e);
  37 static bool exprNode_multiStatement (exprNode p_e);
  38 bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint);
  39 //static void exprNode_constraintPropagateUp (exprNode p_e);
  40 constraintList exprNode_traversRequiresConstraints (exprNode e);
  41 constraintList exprNode_traversEnsuresConstraints (exprNode e);
  42
  43 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e);
  44
  45 extern constraintList reflectChanges (constraintList pre2, constraintList post1);
  46
  47 void mergeResolve (exprNode parent, exprNode child1, exprNode child2);
  48 exprNode makeDataTypeConstraints (exprNode e);
  49 constraintList constraintList_makeFixedArrayConstraints (sRefSet s);
  50 constraintList checkCall (exprNode fcn, exprNodeList arglist);
  51
  52 bool exprNode_testd()
  53 {
  54   /*        if ( ( (exprNode_isError  ) ) )
  55           {
  56           }
  57         if ( ( (e_1  ) ) )
  58           {
  59           }
  60   */
  61 }
  62
  63 bool exprNode_isUnhandled (exprNode e)
  64 {
  65   llassert( exprNode_isDefined(e) );
  66   switch (e->kind)
  67     {
  68     case XPR_INITBLOCK:
  69     case XPR_EMPTY:
  70     case XPR_LABEL:
  71     case XPR_CONST:
  72     case XPR_VAR:
  73     case XPR_BODY:
  74     case XPR_OFFSETOF:
  75     case XPR_ALIGNOFT:
  76     case XPR_ALIGNOF:
  77     case XPR_VAARG:
  78     case XPR_ITERCALL:
  79     case XPR_ITER:
  80     case XPR_CAST:
  81     case XPR_GOTO:
  82     case XPR_CONTINUE:
  83     case XPR_BREAK:
  84     case XPR_COMMA:
  85     case XPR_COND:
  86     case XPR_TOK:
  87     case XPR_FTDEFAULT:
  88     case XPR_DEFAULT:
  89     case XPR_SWITCH:
  90     case XPR_FTCASE:
  91     case XPR_CASE:
  92     case XPR_INIT:
  93     case XPR_NODE:
  94       DPRINTF((message ("Warning current constraint generation does not handle expression %s", exprNode_unparse(e)) ) );
  95       return TRUE;
  96       /*@notreached@*/
  97       break;
  98     default:
  99       return FALSE;
 100
 101     }
 102   /*not reached*/
 103   return FALSE;
 104 }
 105
 106 bool exprNode_handleError( exprNode e)
 107 {
 108    if (exprNode_isError (e) || exprNode_isUnhandled(e) )
 109     {
 110       static /*@only@*/ cstring error = cstring_undefined;
 111
 112       if (!cstring_isDefined (error))
 113         {
 114           error = cstring_makeLiteral ("<error>");
 115         }
 116
 117       /*@-unqualifiedtrans*/ return TRUE; /*@=unqualifiedtrans*/
 118     }
 119    return FALSE;
 120 }
 121
 122 bool /*@alt void@*/ exprNode_generateConstraints (/*@temp@*/ exprNode e)
 123 {
 124   if (exprNode_isError (e) )
 125     return FALSE;
 126
 127   if (exprNode_isUnhandled (e) )
 128     {
 129       DPRINTF( (message("Warning ignoring %s", exprNode_unparse (e) ) ) );
 130       e->requiresConstraints = constraintList_new();
 131       e->ensuresConstraints = constraintList_new();
 132       e->trueEnsuresConstraints = constraintList_new();
 133       e->falseEnsuresConstraints = constraintList_new();
 134       //  llassert(FALSE);
 135       return FALSE;
 136     }
 137
 138
 139   //  e = makeDataTypeConstraints (e);
 140
 141   DPRINTF((message ("exprNode_generateConstraints Analysising %s at %s", exprNode_unparse( e),
 142                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 143
 144   if (exprNode_isMultiStatement ( e) )
 145     {
 146       exprNode_multiStatement(e);
 147     }
 148   else
 149     {
 150       //    llassert(FALSE);
 151       return FALSE;
 152     }
 153
 154   {
 155     constraintList c;
 156
 157     c = constraintList_makeFixedArrayConstraints (e->uses);
 158   e->requiresConstraints = reflectChanges (e->requiresConstraints, c);
 159
 160   //  e->ensuresConstraints = constraintList_mergeEnsures(c, e->ensuresConstraints);
 161
 162   }
 163
 164   /*  printf ("%s", (message ("%s", constraintList_printDetailed (e->requiresConstraints) ) ) );
 165       printf ("%s", (message ("%s", constraintList_printDetailed (e->ensuresConstraints) ) ) ); */
 166   return FALSE;
 167 }
 168
 169
 170 /* handles multiple statements */
 171
 172 bool exprNode_isMultiStatement(exprNode e)
 173 {
 174 if (exprNode_handleError (e) != NULL)
 175   return FALSE;
 176
 177   switch (e->kind)
 178     {
 179     case XPR_FOR:
 180     case XPR_FORPRED:
 181     case XPR_IF:
 182     case XPR_IFELSE:
 183     case XPR_WHILE:
 184     case XPR_WHILEPRED:
 185     case XPR_DOWHILE:
 186     case XPR_BLOCK:
 187     case XPR_STMT:
 188     case XPR_STMTLIST:
 189       return TRUE;
 190     default:
 191       return FALSE;
 192     }
 193
 194 }
 195
 196 bool exprNode_stmt (exprNode e)
 197 {
 198   exprNode snode;
 199   fileloc loc;
 200   bool notError;
 201
 202   if (exprNode_isError(e) )
 203     {
 204       return FALSE;
 205     }
 206   e->requiresConstraints = constraintList_new();
 207   e->ensuresConstraints  = constraintList_new();
 208   //  e = makeDataTypeConstraints(e);
 209
 210
 211   DPRINTF(( "STMT:") );
 212   DPRINTF ( ( cstring_toCharsSafe ( exprNode_unparse(e)) )
 213            );
 214   if (e->kind != XPR_STMT)
 215     {
 216
 217       DPRINTF (("Not Stmt") );
 218       DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
 219       if (exprNode_isMultiStatement (e) )
 220         {
 221           return exprNode_multiStatement (e );
 222         }
 223       BPRINTF( (message ("Ignoring non-statement %s", exprNode_unparse(e) ) ) );
 224       return TRUE;
 225       //      llassert(FALSE);
 226     }
 227
 228   DPRINTF (("Stmt") );
 229   DPRINTF ( (message ("%s ", exprNode_unparse (e)) ) );
 230
 231   snode = exprData_getUopNode (e->edata);
 232
 233   /* could be stmt involving multiple statements:
 234      i.e. if, while for ect.
 235   */
 236
 237   if (exprNode_isMultiStatement (snode))
 238     {
 239       //      llassert(FALSE);
 240       return exprNode_multiStatement (snode);
 241     }
 242
 243   loc = exprNode_getNextSequencePoint(e); /* reduces to an expression */
 244   notError = exprNode_exprTraverse (snode, FALSE, FALSE, loc);
 245   e->requiresConstraints = exprNode_traversRequiresConstraints(snode);
 246   //  printf ("For: %s \n", exprNode_unparse (e) );
 247   // printf ("%s\n", constraintList_print(e->requiresConstraints) );
 248   e->ensuresConstraints  = exprNode_traversEnsuresConstraints(snode);
 249   // printf ("Ensures that:\n %s\n", constraintList_print(e->ensuresConstraints) );
 250   //  llassert(notError);
 251   return notError;
 252
 253 }
 254
 255
 256 bool exprNode_stmtList  (exprNode e)
 257 {
 258   exprNode stmt1, stmt2;
 259   if (exprNode_isError (e) )
 260     {
 261       return FALSE;
 262     }
 263
 264   e->requiresConstraints = constraintList_new();
 265   e->ensuresConstraints  = constraintList_new();
 266   //  e = makeDataTypeConstraints(e);
 267
 268   /*Handle case of stmtList with only one statement:
 269    The parse tree stores this as stmt instead of stmtList*/
 270   if (e->kind != XPR_STMTLIST)
 271     {
 272       return exprNode_stmt(e);
 273     }
 274   llassert (e->kind == XPR_STMTLIST);
 275   DPRINTF(( "STMTLIST:") );
 276   DPRINTF ((cstring_toCharsSafe (exprNode_unparse(e)) ) );
 277   stmt1 = exprData_getPairA (e->edata);
 278   stmt2 = exprData_getPairB (e->edata);
 279
 280
 281   DPRINTF(("        stmtlist       ") );
 282   DPRINTF ((message("XW%s    |        %s", exprNode_unparse(stmt1), exprNode_unparse(stmt2) ) ) );
 283
 284   exprNode_stmt (stmt1);
 285   DPRINTF(("\nstmt after stmtList call " ));
 286
 287   exprNode_stmt (stmt2);
 288   mergeResolve (e, stmt1, stmt2 );
 289
 290   DPRINTF ( (message ("smtlist constraints are: pre: %s \n and \t post %s\n",
 291                       constraintList_print(e->requiresConstraints),
 292                       constraintList_print(e->ensuresConstraints) ) ) );
 293   return TRUE;
 294 }
 295
 296
 297 exprNode doIf (exprNode e, exprNode test, exprNode body)
 298 {
 299   test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 300   e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
 301   e->requiresConstraints = reflectChanges (e->requiresConstraints,
 302                                            test->ensuresConstraints);
 303 #warning bad
 304   e->ensuresConstraints = constraintList_copy (test->ensuresConstraints);
 305   return e;
 306 }
 307
 308 constraintList constraintList_makeFixedArrayConstraints (sRefSet s)
 309 {
 310   constraintList ret;
 311   ret = constraintList_new();
 312
 313   sRefSet_elements (s, el)
 314     {
 315       //    llassert (el);
 316     if (sRef_isFixedArray(el) )
 317       {
 318         int s;
 319         constraint con;
 320         s = sRef_getArraySize(el);
 321         DPRINTF( (message("%s is a fixed array with size %d",
 322                           sRef_unparse(el), s) ) );
 323         con = constraint_makeSRefWriteSafeInt (el, (s - 1));
 324         ret = constraintList_add(ret, con);
 325       }
 326     else
 327       {
 328         DPRINTF( (message("%s is not a fixed array",
 329                           sRef_unparse(el)) ) );
 330       }
 331     }
 332   end_sRefSet_elements
 333
 334     return ret;
 335 }
 336
 337 exprNode makeDataTypeConstraints (exprNode e)
 338 {
 339   constraintList c;
 340   DPRINTF(("makeDataTypeConstraints"));
 341
 342   c = constraintList_makeFixedArrayConstraints (e->uses);
 343
 344   e->ensuresConstraints = constraintList_addList (e->ensuresConstraints, c);
 345
 346 /*   sRefSet_elements (e->uses, el) */
 347 /*     llassert (el); */
 348 /*     if (sRef_isFixedArray(el) ) */
 349 /*       { */
 350 /*      int s; */
 351 /*      constraint con; */
 352 /*      s = sRef_getArraySize(el); */
 353 /*      DPRINTF( (message("%s is a fixed array with size %d", */
 354 /*                        sRef_unparse(el), s) ) ); */
 355 /*      con = constraint_makeSRefWriteSafeInt (el, (s - 1)); */
 356 /*      e->ensuresConstraints = constraintList_add(e->ensuresConstraints, */
 357 /*                                                 con); */
 358 /*       } */
 359 /*     else */
 360 /*       { */
 361 /*      DPRINTF( (message("%s is not a fixed array", */
 362 /*                        sRef_unparse(el)) ) ); */
 363 /*       } */
 364 /*   end_sRefSet_elements */
 365
 366  return e;
 367 }
 368
 369
 370 bool exprNode_multiStatement (exprNode e)
 371 {
 372
 373   bool ret;
 374   exprData data;
 375   exprNode e1, e2;
 376   exprNode p, trueBranch, falseBranch;
 377   exprNode forPred, forBody;
 378   exprNode init, test, inc;
 379   constraintList cons;
 380   constraintList t, f;
 381   e->requiresConstraints = constraintList_new();
 382   e->ensuresConstraints = constraintList_new();
 383   e->trueEnsuresConstraints = constraintList_new();
 384   e->falseEnsuresConstraints = constraintList_new();
 385
 386   //  e = makeDataTypeConstraints(e);
 387
 388   DPRINTF((message ("exprNode_multistatement Analysising %s %s at", exprNode_unparse( e),
 389                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 390
 391   if (exprNode_handleError (e))
 392     {
 393       return FALSE;
 394     }
 395
 396   data = e->edata;
 397
 398   ret = TRUE;
 399
 400   switch (e->kind)
 401     {
 402
 403     case XPR_FOR:
 404       // ret = message ("%s %s",
 405       forPred = exprData_getPairA (data);
 406       forBody = exprData_getPairB (data);
 407
 408
 409       //first generate the constraints
 410       exprNode_generateConstraints (forPred);
 411       exprNode_generateConstraints (forBody);
 412
 413       //merge the constraints: modle as if statement
 414       /* init
 415         if (test)
 416            for body
 417            inc        */
 418       init  =  exprData_getTripleInit (forPred->edata);
 419       test =   exprData_getTripleTest (forPred->edata);
 420       inc  =   exprData_getTripleInc (forPred->edata);
 421
 422       //      if ( ( (exprNode_isError (test) || (exprNode_isError(init) ) || (exprNode_isError) ) ) )
 423       //            if ( ( (myexprNode_isError (test) || (myexprNode_isError(init) ) || (myexprNode_isError) ) ) )
 424
 425       //if ( ( (exprNode_isError  ) ) )
 426             if ( ( (exprNode_isError (test) || (exprNode_isError(init) ) ) || (exprNode_isError (inc) ) ) )
 427         {
 428           BPRINTF ((message ("strange for statement:%s, ignoring it", exprNode_unparse(e) ) ) );
 429           return ret;
 430         }
 431
 432       test->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(test);
 433       //      e->requiresConstraints = reflectChanges (body->requiresConstraints, test->trueEnsuresConstraints);
 434       e->requiresConstraints = reflectChanges (e->requiresConstraints, test->ensuresConstraints);
 435
 436       break;
 437
 438     case XPR_FORPRED:
 439       //            ret = message ("for (%s; %s; %s)",
 440       exprNode_generateConstraints (exprData_getTripleInit (data) );
 441       exprNode_exprTraverse (exprData_getTripleTest (data),FALSE, FALSE, exprNode_loc(e));
 442       exprNode_generateConstraints (exprData_getTripleInc (data));
 443       break;
 444     case XPR_IF:
 445       DPRINTF(( "IF:") );
 446       DPRINTF ((exprNode_unparse(e) ) );
 447       //      ret = message ("if (%s) %s",
 448       e1 = exprData_getPairA (data);
 449       e2 = exprData_getPairB (data);
 450
 451       exprNode_exprTraverse (e1,
 452                              FALSE, FALSE, exprNode_loc(e1));
 453
 454       exprNode_generateConstraints (e2);
 455
 456       e = doIf (e, e1, e2);
 457
 458
 459       //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data),exprData_getPairB(data));
 460       break;
 461
 462     case XPR_IFELSE:
 463       DPRINTF(("Starting IFELSE"));
 464       //      ret = message ("if (%s) %s else %s",
 465       p = exprData_getTriplePred (data);
 466       trueBranch = exprData_getTripleTrue (data);
 467       falseBranch = exprData_getTripleFalse (data);
 468
 469       exprNode_exprTraverse (p,
 470                              FALSE, FALSE, exprNode_loc(p));
 471       exprNode_generateConstraints (trueBranch);
 472       exprNode_generateConstraints (falseBranch);
 473
 474       // do requires clauses
 475
 476       cons = reflectChanges (trueBranch->requiresConstraints, p->trueEnsuresConstraints);
 477       cons  = reflectChanges (cons,
 478                               p->ensuresConstraints);
 479       e->requiresConstraints = constraintList_copy (cons);
 480
 481       cons = reflectChanges (falseBranch->requiresConstraints, p->falseEnsuresConstraints);
 482       cons  = reflectChanges (cons,
 483                               p->ensuresConstraints);
 484       e->requiresConstraints = constraintList_addList (e->requiresConstraints,
 485                                                        cons);
 486       e->requiresConstraints = constraintList_addList (e->requiresConstraints,
 487                                                        p->requiresConstraints);
 488
 489       // do ensures clauses
 490       // find the  the ensures lists for each subbranch
 491       t = constraintList_mergeEnsures (p->trueEnsuresConstraints, trueBranch->ensuresConstraints);
 492       t = constraintList_mergeEnsures (p->ensuresConstraints, t);
 493
 494       f = constraintList_mergeEnsures (p->falseEnsuresConstraints, falseBranch->ensuresConstraints);
 495       f = constraintList_mergeEnsures (p->ensuresConstraints, f);
 496
 497       // find ensures for whole if/else statement
 498
 499       e->ensuresConstraints = constraintList_logicalOr (t, f);
 500       DPRINTF( ("Done IFELSE") );
 501       break;
 502     case XPR_WHILE:
 503        e1 = exprData_getPairA (data);
 504        e2 = exprData_getPairB (data);
 505       exprNode_exprTraverse (e1,
 506                              FALSE, FALSE, exprNode_loc(e1));
 507
 508       exprNode_generateConstraints (e2);
 509
 510       e1->trueEnsuresConstraints =  exprNode_traversTrueEnsuresConstraints(e1);
 511
 512       e->requiresConstraints = reflectChanges (e2->requiresConstraints, e1->trueEnsuresConstraints);
 513
 514       e->requiresConstraints = reflectChanges (e->requiresConstraints,
 515                                                e1->ensuresConstraints);
 516 #warning bad
 517       e->ensuresConstraints = constraintList_copy (e1->ensuresConstraints);
 518
 519       //      ret = message ("while (%s) %s",
 520                      exprNode_generateConstraints (exprData_getPairA (data));
 521                      exprNode_generateConstraints (exprData_getPairB (data));
 522                      //      e->constraints = constraintList_exprNodemerge (exprData_getPairA (data), exprData_getPairB (data) );
 523       break;
 524
 525     case XPR_DOWHILE:
 526       // ret = message ("do { %s } while (%s)",
 527                      exprNode_generateConstraints (exprData_getPairB (data));
 528                      exprNode_generateConstraints (exprData_getPairA (data));
 529       break;
 530
 531     case XPR_BLOCK:
 532       //      ret = message ("{ %s }",
 533                      exprNode_generateConstraints (exprData_getSingle (data));
 534                      e->requiresConstraints = constraintList_copy ( (exprData_getSingle (data))->requiresConstraints );
 535                      e->ensuresConstraints = constraintList_copy ( (exprData_getSingle (data))->ensuresConstraints );
 536                      //      e->constraints = (exprData_getSingle (data))->constraints;
 537       break;
 538
 539     case XPR_STMT:
 540     case XPR_STMTLIST:
 541       return exprNode_stmtList (e);
 542       /*@notreached@*/
 543       break;
 544     default:
 545       ret=FALSE;
 546     }
 547   return ret;
 548 }
 549
 550 bool lltok_isBoolean_Op (lltok tok)
 551 {
 552   /*this should really be a switch statement but
 553     I don't want to violate the abstraction
 554     maybe this should go in lltok.c */
 555
 556   if (lltok_isEq_Op (tok) )
 557         {
 558           return TRUE;
 559         }
 560       if (lltok_isAnd_Op (tok) )
 561
 562         {
 563
 564           return TRUE;
 565         }
 566    if (lltok_isOr_Op (tok) )
 567         {
 568           return TRUE;
 569         }
 570
 571    if (lltok_isGt_Op (tok) )
 572      {
 573        return TRUE;
 574      }
 575    if (lltok_isLt_Op (tok) )
 576      {
 577        return TRUE;
 578      }
 579
 580    if (lltok_isLe_Op (tok) )
 581      {
 582        return TRUE;
 583      }
 584
 585    if (lltok_isGe_Op (tok) )
 586      {
 587        return TRUE;
 588      }
 589
 590    return FALSE;
 591
 592 }
 593
 594
 595 void exprNode_booleanTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint)
 596 {
 597  constraint cons;
 598 exprNode t1, t2;
 599 exprData data;
 600 lltok tok;
 601 constraintList tempList;
 602 data = e->edata;
 603
 604 tok = exprData_getOpTok (data);
 605
 606
 607 t1 = exprData_getOpA (data);
 608 t2 = exprData_getOpB (data);
 609
 610
 611 /* arithmetic tests */
 612
 613 if (lltok_isEq_Op (tok) )
 614 {
 615   cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
 616   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 617 }
 618
 619
 620  if (lltok_isLt_Op (tok) )
 621    {
 622      cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
 623      e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 624      cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
 625      e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
 626    }
 627
 628
 629 if (lltok_isGe_Op (tok) )
 630 {
 631
 632   cons = constraint_makeEnsureGreaterThanEqual (t1, t2, sequencePoint);
 633   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 634
 635   cons =  constraint_makeEnsureLessThan (t1, t2, sequencePoint);
 636   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
 637
 638 }
 639
 640
 641   if (lltok_isGt_Op (tok) )
 642 {
 643   cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
 644   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 645   cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
 646   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
 647 }
 648
 649 if (lltok_isLe_Op (tok) )
 650 {
 651    cons = constraint_makeEnsureLessThanEqual (t1, t2, sequencePoint);
 652   e->trueEnsuresConstraints = constraintList_add(e->trueEnsuresConstraints, cons);
 653
 654   cons =  constraint_makeEnsureGreaterThan (t1, t2, sequencePoint);
 655   e->falseEnsuresConstraints = constraintList_add(e->falseEnsuresConstraints, cons);
 656 }
 657
 658
 659
 660 /*Logical operations */
 661
 662  if (lltok_isAnd_Op (tok) )
 663
 664    {
 665      //true ensures
 666      tempList = constraintList_copy (t1->trueEnsuresConstraints);
 667      tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
 668      e->trueEnsuresConstraints = constraintList_addList(e->trueEnsuresConstraints, tempList);
 669
 670       //false ensures: fens t1 or tens t1 and fens t2
 671      tempList = constraintList_copy (t1->trueEnsuresConstraints);
 672      tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
 673      tempList = constraintList_logicalOr (tempList, t1->falseEnsuresConstraints);
 674       e->falseEnsuresConstraints =constraintList_addList(e->falseEnsuresConstraints, tempList);
 675
 676    }
 677
 678   if (lltok_isOr_Op (tok) )
 679     {
 680       //false ensures
 681       tempList = constraintList_copy (t1->falseEnsuresConstraints);
 682       tempList = constraintList_addList (tempList, t2->falseEnsuresConstraints);
 683       e->falseEnsuresConstraints = constraintList_addList(e->falseEnsuresConstraints, tempList);
 684
 685       //true ensures: tens t1 or fens t1 and tens t2
 686       tempList = constraintList_copy (t1->falseEnsuresConstraints);
 687       tempList = constraintList_addList (tempList, t2->trueEnsuresConstraints);
 688       tempList = constraintList_logicalOr (tempList, t1->trueEnsuresConstraints);
 689       e->trueEnsuresConstraints =constraintList_addList(e->trueEnsuresConstraints, tempList);
 690
 691     }
 692
 693 }
 694
 695 bool exprNode_exprTraverse (exprNode e, bool definatelv, bool definaterv,  fileloc sequencePoint)
 696 {
 697   exprNode t1, t2;
 698   lltok tok;
 699   bool handledExprNode;
 700   exprData data;
 701   constraint cons;
 702
 703      if (exprNode_isError(e) )
 704      {
 705        return FALSE;
 706      }
 707
 708    DPRINTF((message ("exprNode_exprTraverset Analysising %s %s at", exprNode_unparse( e),
 709                     fileloc_unparse(exprNode_getfileloc(e) ) ) ) );
 710
 711    e->requiresConstraints = constraintList_new();
 712    e->ensuresConstraints = constraintList_new();
 713    e->trueEnsuresConstraints = constraintList_new();;
 714    e->falseEnsuresConstraints = constraintList_new();;
 715
 716    if (exprNode_isUnhandled (e) )
 717      {
 718        return FALSE;
 719      }
 720    //   e = makeDataTypeConstraints (e);
 721
 722    handledExprNode = TRUE;
 723
 724   data = e->edata;
 725
 726   switch (e->kind)
 727     {
 728
 729
 730     case XPR_WHILEPRED:
 731       t1 = exprData_getSingle (data);
 732       exprNode_exprTraverse (t1,  definatelv, definaterv, sequencePoint);
 733       e = exprNode_copyConstraints (e, t1);
 734       break;
 735
 736     case XPR_FETCH:
 737
 738       if (definatelv )
 739         {
 740           t1 =  (exprData_getPairA (data) );
 741           t2 =  (exprData_getPairB (data) );
 742           cons =  constraint_makeWriteSafeExprNode (t1, t2);
 743         }
 744       else
 745         {
 746           t1 =  (exprData_getPairA (data) );
 747           t2 =  (exprData_getPairB (data) );
 748           cons = constraint_makeReadSafeExprNode (t1, t2 );
 749         }
 750
 751       e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
 752       cons = constraint_makeEnsureMaxReadAtLeast (t1, t2, sequencePoint);
 753       e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 754       //      cons = constraint_makeEnsureMinReadAtMost (t1, t2, sequencePoint);
 755       // e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 756
 757       exprNode_exprTraverse (exprData_getPairA (data), FALSE, TRUE, sequencePoint);
 758       exprNode_exprTraverse (exprData_getPairB (data), FALSE, TRUE, sequencePoint);
 759
 760             /*@i325 Should check which is array/index. */
 761       break;
 762     case XPR_PREOP:
 763       t1 = exprData_getUopNode(data);
 764       //lltok_unparse (exprData_getUopTok (data));
 765       exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
 766       /*handle * pointer access */
 767
 768       /*@ i 325 do ++ and -- */
 769       if (lltok_isMult( exprData_getUopTok (data) ) )
 770         {
 771           if (definatelv)
 772             {
 773               cons = constraint_makeWriteSafeInt (t1, 0);
 774             }
 775           else
 776             {
 777               cons = constraint_makeReadSafeInt (t1, 0);
 778             }
 779               e->requiresConstraints = constraintList_add(e->requiresConstraints, cons);
 780         }
 781
 782       /* ! expr */
 783       if (lltok_isNot_Op (exprData_getUopTok (data) ) )
 784         {
 785           e->trueEnsuresConstraints  = constraintList_copy (t1->falseEnsuresConstraints);
 786           e->falseEnsuresConstraints = constraintList_copy (t1->trueEnsuresConstraints);
 787         }
 788       break;
 789
 790     case XPR_PARENS:
 791       exprNode_exprTraverse (exprData_getUopNode (e->edata), definatelv, definaterv, sequencePoint);
 792       //    e->constraints = constraintList_exprNodemerge (exprData_getUopNode (e->edata), exprNode_undefined);
 793       break;
 794     case XPR_ASSIGN:
 795       t1 = exprData_getOpA (data);
 796       t2 = exprData_getOpB (data);
 797       exprNode_exprTraverse (t1, TRUE, definaterv, sequencePoint );
 798       lltok_unparse (exprData_getOpTok (data));
 799       exprNode_exprTraverse (t2, definatelv, TRUE, sequencePoint );
 800
 801       /* this test is nessecary because some expressions generate a null expression node.  function pointer do that -- drl */
 802       if ( (!exprNode_isError (t1))  &&  (!exprNode_isError(t2)) )
 803         {
 804           cons =  constraint_makeEnsureEqual (t1, t2, sequencePoint);
 805           e->ensuresConstraints = constraintList_add(e->ensuresConstraints, cons);
 806         }
 807
 808       break;
 809     case XPR_OP:
 810       t1 = exprData_getOpA (data);
 811       t2 = exprData_getOpB (data);
 812
 813        exprNode_exprTraverse (t1, definatelv, definaterv, sequencePoint );
 814       tok = exprData_getOpTok (data);
 815       exprNode_exprTraverse (t2, definatelv, definaterv, sequencePoint );
 816
 817       if (lltok_isBoolean_Op (tok) )
 818         exprNode_booleanTraverse (e, definatelv, definaterv, sequencePoint);
 819
 820       //      e->constraints  = constraintList_exprNodemerge (exprData_getOpA (data), exprData_getOpB (data));
 821       break;
 822     case XPR_SIZEOFT:
 823       ctype_unparse (qtype_getType (exprData_getType (data) ) );
 824
 825       break;
 826
 827     case XPR_SIZEOF:
 828       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
 829       //      e->constraints = constraintList_exprNodemerge (exprData_getSingle (e->edata), exprNode_undefined);
 830       break;
 831
 832     case XPR_CALL:
 833       exprNode_exprTraverse (exprData_getFcn (data), definatelv, definaterv, sequencePoint );
 834       exprNodeList_unparse (exprData_getArgs (data) );
 835       DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(exprData_getFcn(data) ),   exprNodeList_unparse (exprData_getArgs (data) ) ) ) );
 836
 837
 838
 839       e->requiresConstraints = constraintList_addList (e->requiresConstraints,
 840                                                  checkCall (exprData_getFcn (data), exprData_getArgs (data)  ) );
 841       //      e->constraints = constraintList_add (e->constraints, constraint_create (e,exprNode_undefined, GT,  CALLSAFE ) );
 842       break;
 843
 844     case XPR_RETURN:
 845       exprNode_exprTraverse (exprData_getSingle (data), definatelv, definaterv, sequencePoint );
 846       break;
 847
 848     case XPR_NULLRETURN:
 849       cstring_makeLiteral ("return");;
 850       break;
 851
 852
 853     case XPR_FACCESS:
 854       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
 855       exprData_getFieldName (data) ;
 856       break;
 857
 858     case XPR_ARROW:
 859       exprNode_exprTraverse (exprData_getFieldNode (data), definatelv, definaterv, sequencePoint );
 860       exprData_getFieldName (data);
 861       break;
 862
 863     case XPR_STRINGLITERAL:
 864       cstring_copy (exprData_getLiteral (data));
 865       break;
 866
 867     case XPR_NUMLIT:
 868       cstring_copy (exprData_getLiteral (data));
 869       break;
 870     case XPR_POSTOP:
 871
 872       exprNode_exprTraverse (exprData_getUopNode (data), TRUE, definaterv, sequencePoint );
 873       lltok_unparse (exprData_getUopTok (data));
 874       if (lltok_isInc_Op (exprData_getUopTok (data) ) )
 875         {
 876           DPRINTF(("doing ++"));
 877           t1 = exprData_getUopNode (data);
 878           cons = constraint_makeMaxSetSideEffectPostIncrement (t1, sequencePoint );
 879           e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 880           //      cons = constraint_makeMaxReadSideEffectPostIncrement (t1, sequencePoint );
 881           //e->ensuresConstraints = constraintList_add (e->ensuresConstraints, cons);
 882         }
 883       break;
 884     default:
 885       handledExprNode = FALSE;
 886     }
 887
 888   e->requiresConstraints =  constraintList_preserveOrig ( e->requiresConstraints);
 889   e->ensuresConstraints  =  constraintList_preserveOrig ( e->ensuresConstraints);
 890
 891   return handledExprNode;
 892 }
 893
 894
 895 constraintList exprNode_traversTrueEnsuresConstraints (exprNode e)
 896 {
 897   //  exprNode t1, t2;
 898
 899   bool handledExprNode;
 900   //  char * mes;
 901   exprData data;
 902   constraintList ret;
 903
 904    if (exprNode_handleError (e))
 905      {
 906        ret = constraintList_new();
 907        return ret;
 908      }
 909   ret = constraintList_copy (e->trueEnsuresConstraints );
 910
 911    handledExprNode = TRUE;
 912
 913   data = e->edata;
 914
 915   switch (e->kind)
 916     {
 917
 918     case XPR_FETCH:
 919
 920       ret = constraintList_addList (ret,
 921                                     exprNode_traversTrueEnsuresConstraints
 922                                     (exprData_getPairA (data) ) );
 923
 924       ret = constraintList_addList (ret,
 925                                     exprNode_traversTrueEnsuresConstraints
 926                                     (exprData_getPairB (data) ) );
 927       break;
 928     case XPR_PREOP:
 929
 930       ret = constraintList_addList (ret,
 931                                     exprNode_traversTrueEnsuresConstraints
 932                                     (exprData_getUopNode (data) ) );
 933       break;
 934
 935     case XPR_PARENS:
 936       ret = constraintList_addList (ret, exprNode_traversTrueEnsuresConstraints
 937                                     (exprData_getUopNode (data) ) );
 938       break;
 939     case XPR_ASSIGN:
 940         ret = constraintList_addList (ret,
 941                                     exprNode_traversTrueEnsuresConstraints
 942                                     (exprData_getOpA (data) ) );
 943
 944        ret = constraintList_addList (ret,
 945                                     exprNode_traversTrueEnsuresConstraints
 946                                     (exprData_getOpB (data) ) );
 947        break;
 948     case XPR_OP:
 949        ret = constraintList_addList (ret,
 950                                     exprNode_traversTrueEnsuresConstraints
 951                                     (exprData_getOpA (data) ) );
 952
 953        ret = constraintList_addList (ret,
 954                                     exprNode_traversTrueEnsuresConstraints
 955                                     (exprData_getOpB (data) ) );
 956        break;
 957     case XPR_SIZEOFT:
 958
 959       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
 960
 961       break;
 962
 963     case XPR_SIZEOF:
 964
 965        ret = constraintList_addList (ret,
 966                                     exprNode_traversTrueEnsuresConstraints
 967                                      (exprData_getSingle (data) ) );
 968        break;
 969
 970     case XPR_CALL:
 971       ret = constraintList_addList (ret,
 972                                      exprNode_traversTrueEnsuresConstraints
 973                                     (exprData_getFcn (data) ) );
 974       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
 975          break;
 976
 977     case XPR_RETURN:
 978       ret = constraintList_addList (ret,
 979                                     exprNode_traversTrueEnsuresConstraints
 980                                     (exprData_getSingle (data) ) );
 981       break;
 982
 983     case XPR_NULLRETURN:
 984       //      cstring_makeLiteral ("return");;
 985       break;
 986
 987     case XPR_FACCESS:
 988           ret = constraintList_addList (ret,
 989                                     exprNode_traversTrueEnsuresConstraints
 990                                     (exprData_getFieldNode (data) ) );
 991        //exprData_getFieldName (data) ;
 992       break;
 993
 994     case XPR_ARROW:
 995         ret = constraintList_addList (ret,
 996                                     exprNode_traversTrueEnsuresConstraints
 997                                     (exprData_getFieldNode (data) ) );
 998         //      exprData_getFieldName (data);
 999       break;
1000
1001     case XPR_STRINGLITERAL:
1002       //      cstring_copy (exprData_getLiteral (data));
1003       break;
1004
1005     case XPR_NUMLIT:
1006       //      cstring_copy (exprData_getLiteral (data));
1007       break;
1008     case XPR_POSTOP:
1009
1010            ret = constraintList_addList (ret,
1011                                     exprNode_traversTrueEnsuresConstraints
1012                                     (exprData_getUopNode (data) ) );
1013            break;
1014     default:
1015       break;
1016     }
1017
1018   return ret;
1019 }
1020
1021
1022 /* walk down the tree and get all requires Constraints in each subexpression*/
1023 constraintList exprNode_traversRequiresConstraints (exprNode e)
1024 {
1025   //  exprNode t1, t2;
1026
1027   bool handledExprNode;
1028   //  char * mes;
1029   exprData data;
1030   constraintList ret;
1031
1032    if (exprNode_handleError (e))
1033      {
1034        ret = constraintList_new();
1035        return ret;
1036      }
1037   ret = constraintList_copy (e->requiresConstraints );
1038
1039    handledExprNode = TRUE;
1040
1041   data = e->edata;
1042
1043   switch (e->kind)
1044     {
1045
1046     case XPR_FETCH:
1047
1048       ret = constraintList_addList (ret,
1049                                     exprNode_traversRequiresConstraints
1050                                     (exprData_getPairA (data) ) );
1051
1052       ret = constraintList_addList (ret,
1053                                     exprNode_traversRequiresConstraints
1054                                     (exprData_getPairB (data) ) );
1055       break;
1056     case XPR_PREOP:
1057
1058       ret = constraintList_addList (ret,
1059                                     exprNode_traversRequiresConstraints
1060                                     (exprData_getUopNode (data) ) );
1061       break;
1062
1063     case XPR_PARENS:
1064       ret = constraintList_addList (ret, exprNode_traversRequiresConstraints
1065                                     (exprData_getUopNode (data) ) );
1066       break;
1067     case XPR_ASSIGN:
1068         ret = constraintList_addList (ret,
1069                                     exprNode_traversRequiresConstraints
1070                                     (exprData_getOpA (data) ) );
1071
1072        ret = constraintList_addList (ret,
1073                                     exprNode_traversRequiresConstraints
1074                                     (exprData_getOpB (data) ) );
1075        break;
1076     case XPR_OP:
1077        ret = constraintList_addList (ret,
1078                                     exprNode_traversRequiresConstraints
1079                                     (exprData_getOpA (data) ) );
1080
1081        ret = constraintList_addList (ret,
1082                                     exprNode_traversRequiresConstraints
1083                                     (exprData_getOpB (data) ) );
1084        break;
1085     case XPR_SIZEOFT:
1086
1087       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1088
1089       break;
1090
1091     case XPR_SIZEOF:
1092
1093        ret = constraintList_addList (ret,
1094                                     exprNode_traversRequiresConstraints
1095                                      (exprData_getSingle (data) ) );
1096        break;
1097
1098     case XPR_CALL:
1099       ret = constraintList_addList (ret,
1100                                      exprNode_traversRequiresConstraints
1101                                     (exprData_getFcn (data) ) );
1102       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1103          break;
1104
1105     case XPR_RETURN:
1106       ret = constraintList_addList (ret,
1107                                     exprNode_traversRequiresConstraints
1108                                     (exprData_getSingle (data) ) );
1109       break;
1110
1111     case XPR_NULLRETURN:
1112       //      cstring_makeLiteral ("return");;
1113       break;
1114
1115     case XPR_FACCESS:
1116           ret = constraintList_addList (ret,
1117                                     exprNode_traversRequiresConstraints
1118                                     (exprData_getFieldNode (data) ) );
1119        //exprData_getFieldName (data) ;
1120       break;
1121
1122     case XPR_ARROW:
1123         ret = constraintList_addList (ret,
1124                                     exprNode_traversRequiresConstraints
1125                                     (exprData_getFieldNode (data) ) );
1126         //      exprData_getFieldName (data);
1127       break;
1128
1129     case XPR_STRINGLITERAL:
1130       //      cstring_copy (exprData_getLiteral (data));
1131       break;
1132
1133     case XPR_NUMLIT:
1134       //      cstring_copy (exprData_getLiteral (data));
1135       break;
1136     case XPR_POSTOP:
1137
1138            ret = constraintList_addList (ret,
1139                                     exprNode_traversRequiresConstraints
1140                                     (exprData_getUopNode (data) ) );
1141            break;
1142     default:
1143       break;
1144     }
1145
1146   return ret;
1147 }
1148
1149
1150 /* walk down the tree and get all Ensures Constraints in each subexpression*/
1151 constraintList exprNode_traversEnsuresConstraints (exprNode e)
1152 {
1153   //  exprNode t1, t2;
1154
1155   bool handledExprNode;
1156   //  char * mes;
1157   exprData data;
1158   //  constraintExpr tmp;
1159   //  constraint cons;
1160   constraintList ret;
1161
1162
1163    if (exprNode_handleError (e))
1164      {
1165        ret = constraintList_new();
1166        return ret;
1167      }
1168
1169   ret = constraintList_copy (e->ensuresConstraints );
1170    handledExprNode = TRUE;
1171
1172   data = e->edata;
1173
1174   DPRINTF( (message (
1175                      "exprnode_traversEnsuresConstraints call for %s with constraintList of %s",
1176                      exprNode_unparse (e),
1177                      constraintList_print(e->ensuresConstraints)
1178                      )
1179             ));
1180
1181
1182   switch (e->kind)
1183     {
1184
1185     case XPR_FETCH:
1186
1187       ret = constraintList_addList (ret,
1188                                     exprNode_traversEnsuresConstraints
1189                                     (exprData_getPairA (data) ) );
1190
1191       ret = constraintList_addList (ret,
1192                                     exprNode_traversEnsuresConstraints
1193                                     (exprData_getPairB (data) ) );
1194       break;
1195     case XPR_PREOP:
1196
1197       ret = constraintList_addList (ret,
1198                                     exprNode_traversEnsuresConstraints
1199                                     (exprData_getUopNode (data) ) );
1200       break;
1201
1202     case XPR_PARENS:
1203       ret = constraintList_addList (ret, exprNode_traversEnsuresConstraints
1204                                     (exprData_getUopNode (data) ) );
1205       break;
1206     case XPR_ASSIGN:
1207         ret = constraintList_addList (ret,
1208                                     exprNode_traversEnsuresConstraints
1209                                     (exprData_getOpA (data) ) );
1210
1211        ret = constraintList_addList (ret,
1212                                     exprNode_traversEnsuresConstraints
1213                                     (exprData_getOpB (data) ) );
1214        break;
1215     case XPR_OP:
1216        ret = constraintList_addList (ret,
1217                                     exprNode_traversEnsuresConstraints
1218                                     (exprData_getOpA (data) ) );
1219
1220        ret = constraintList_addList (ret,
1221                                     exprNode_traversEnsuresConstraints
1222                                     (exprData_getOpB (data) ) );
1223        break;
1224     case XPR_SIZEOFT:
1225
1226       //      ctype_unparse (qtype_getType (exprData_getType (data) ) );
1227
1228       break;
1229
1230     case XPR_SIZEOF:
1231
1232        ret = constraintList_addList (ret,
1233                                     exprNode_traversEnsuresConstraints
1234                                      (exprData_getSingle (data) ) );
1235        break;
1236
1237     case XPR_CALL:
1238       ret = constraintList_addList (ret,
1239                                      exprNode_traversEnsuresConstraints
1240                                     (exprData_getFcn (data) ) );
1241       /*@i11*/      //   exprNodeList_unparse (exprData_getArgs (data) );
1242          break;
1243
1244     case XPR_RETURN:
1245       ret = constraintList_addList (ret,
1246                                     exprNode_traversEnsuresConstraints
1247                                     (exprData_getSingle (data) ) );
1248       break;
1249
1250     case XPR_NULLRETURN:
1251       //      cstring_makeLiteral ("return");;
1252       break;
1253
1254     case XPR_FACCESS:
1255           ret = constraintList_addList (ret,
1256                                     exprNode_traversEnsuresConstraints
1257                                     (exprData_getFieldNode (data) ) );
1258        //exprData_getFieldName (data) ;
1259       break;
1260
1261     case XPR_ARROW:
1262         ret = constraintList_addList (ret,
1263                                     exprNode_traversEnsuresConstraints
1264                                     (exprData_getFieldNode (data) ) );
1265         //      exprData_getFieldName (data);
1266       break;
1267
1268     case XPR_STRINGLITERAL:
1269       //      cstring_copy (exprData_getLiteral (data));
1270       break;
1271
1272     case XPR_NUMLIT:
1273       //      cstring_copy (exprData_getLiteral (data));
1274       break;
1275     case XPR_POSTOP:
1276
1277            ret = constraintList_addList (ret,
1278                                     exprNode_traversEnsuresConstraints
1279                                     (exprData_getUopNode (data) ) );
1280            break;
1281     default:
1282       break;
1283     }
1284 DPRINTF( (message (
1285                      "exprnode_traversEnsuresConstraints call for %s with constraintList of  is returning %s",
1286                      exprNode_unparse (e),
1287              //              constraintList_print(e->ensuresConstraints),
1288                      constraintList_print(ret)
1289                      )
1290             ));
1291
1292
1293   return ret;
1294 }
1295
1296
1297 #ifndef exprNode_isError
1298 #warning wtf
1299 # define exprNode_isError(e)          ((e) == exprNode_undefined)
1300 #else
1301 #warning strange
1302 #endif