src/constraintGeneration.c

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