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