src/constraintResolve.c

   1 /*
   2 *
   3 ** constraintResolve.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 //# include "exprData.i"
  18
  19
  20 /*@access constraint, exprNode @*/
  21
  22 static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arithType ar2, /*@observer@*/ constraintExpr expr2);
  23
  24 static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint c, constraintList p);
  25
  26 static constraint constraint_searchandreplace (/*@returned@*/ constraint c, constraintExpr old, constraintExpr new);
  27
  28
  29 static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint or);
  30
  31 static bool resolveOr (/*@observer@*/ constraint c, /*@observer@*/ constraintList list);
  32
  33 static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constraintList pre2, constraintList post1);
  34
  35 /*********************************************/
  36
  37
  38
  39
  40 /*@only@*/ constraintList constraintList_mergeEnsuresFreeFirst (constraintList list1, constraintList list2)
  41 {
  42   constraintList ret;
  43
  44   ret = constraintList_mergeEnsures (list1, list2);
  45
  46   constraintList_free(list1);
  47   return ret;
  48 }
  49
  50 /*@only@*/ constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
  51 {
  52   constraintList ret;
  53   constraintList temp;
  54
  55   //ret = constraintList_makeNew();
  56
  57   llassert(constraintList_isDefined(list1) );
  58   llassert(constraintList_isDefined(list2) );
  59
  60   DPRINTF(( message ("constraintList_mergeEnsures: list1 %s list2 %s",
  61                      constraintList_print(list1), constraintList_print(list2)
  62                      )));
  63
  64   ret = constraintList_fixConflicts (list1, list2);
  65   ret = reflectChangesEnsuresFree1 (ret, list2);
  66   temp = constraintList_subsumeEnsures (ret, list2);
  67   constraintList_free(ret);
  68   ret = temp;
  69
  70   temp = constraintList_subsumeEnsures (list2, ret);
  71
  72   temp = constraintList_addList (temp, ret);
  73
  74   DPRINTF(( message ("constraintList_mergeEnsures: returning %s ",
  75                      constraintList_print(temp) )
  76                      ));
  77
  78
  79   return temp;
  80   //ret = constraintList_addList (ret, list2);
  81   //return ret;
  82 }
  83
  84
  85 /*@only@*/ constraintList constraintList_mergeRequiresFreeFirst (/*@only@*/ constraintList list1, constraintList list2)
  86 {
  87   constraintList ret;
  88
  89   ret = constraintList_mergeRequires(list1, list2);
  90
  91   constraintList_free(list1);
  92
  93   return ret;
  94 }
  95
  96 /*@only@*/ constraintList constraintList_mergeRequires (constraintList list1, constraintList list2)
  97 {
  98   constraintList ret;
  99   constraintList temp;
 100
 101   DPRINTF((message ("constraintList_mergeRequires: merging  %s and %s ", constraintList_print (list1), constraintList_print(list2) ) ) );
 102
 103   /* get constraints in list1 not satified by list2 */
 104   temp = reflectChanges (list1, list2);
 105   DPRINTF((message ("constraintList_mergeRequires: temp = %s", constraintList_print(temp) ) ) );
 106
 107 /*get constraints in list2 not satified by temp*/
 108   ret = reflectChanges (list2, temp);
 109
 110   DPRINTF((message ("constraintList_mergeRequires: ret =  %s", constraintList_print(ret) ) ) );
 111
 112   ret = constraintList_addList (ret, temp);
 113
 114   DPRINTF((message ("constraintList_mergeRequires: returning  %s", constraintList_print(ret) ) ) );
 115
 116   return ret;
 117 }
 118
 119 void checkArgumentList (/*@out@*/ exprNode temp, exprNodeList arglist, fileloc sequencePoint)
 120 {
 121   temp->requiresConstraints = constraintList_makeNew();
 122   temp->ensuresConstraints = constraintList_makeNew();
 123   temp->trueEnsuresConstraints = constraintList_makeNew();
 124   temp->falseEnsuresConstraints = constraintList_makeNew();
 125
 126   exprNodeList_elements (arglist, el)
 127     {
 128       constraintList temp2;
 129       exprNode_exprTraverse (el, FALSE, FALSE, sequencePoint);
 130       temp2 = el->requiresConstraints;
 131       el->requiresConstraints = exprNode_traversRequiresConstraints(el);
 132       constraintList_free(temp2);
 133
 134       temp2 = el->ensuresConstraints;
 135       el->ensuresConstraints  = exprNode_traversEnsuresConstraints(el);
 136       constraintList_free(temp2);
 137
 138       temp->requiresConstraints = constraintList_addList(temp->requiresConstraints,
 139                                                             el->requiresConstraints);
 140
 141       temp->ensuresConstraints = constraintList_addList(temp->ensuresConstraints,
 142                                                            el->ensuresConstraints);
 143     }
 144   end_exprNodeList_elements;
 145
 146 }
 147
 148 constraintList checkCall (exprNode fcn, exprNodeList arglist)
 149 {
 150   constraintList preconditions;
 151   uentry temp;
 152   DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
 153
 154   temp = exprNode_getUentry (fcn);
 155
 156   preconditions = uentry_getFcnPreconditions (temp);
 157
 158   if (preconditions != constraintList_undefined)
 159     {
 160       preconditions= constraintList_togglePost (preconditions);
 161       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
 162     }
 163   else
 164     {
 165       if (preconditions == NULL)
 166         preconditions = constraintList_makeNew();
 167     }
 168
 169   return preconditions;
 170 }
 171
 172 constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
 173 {
 174   constraintList postconditions;
 175   uentry temp;
 176   DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
 177
 178   temp = exprNode_getUentry (fcn);
 179
 180   postconditions = uentry_getFcnPostconditions (temp);
 181
 182   if (postconditions != constraintList_undefined)
 183     {
 184       postconditions = constraintList_doFixResult (postconditions, fcnCall);
 185       postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
 186     }
 187   else
 188     {
 189       postconditions = constraintList_makeNew();
 190     }
 191
 192   return postconditions;
 193 }
 194
 195 void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 196 {
 197   constraintList temp, temp2;
 198
 199   DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )) );
 200
 201   DPRINTF( (message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
 202
 203   if (exprNode_isError (child1)  || exprNode_isError(child2) )
 204     {
 205       if (exprNode_isError (child1) && !exprNode_isError(child2) )
 206          {
 207            constraintList_free(parent->requiresConstraints);
 208
 209            parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
 210            constraintList_free(parent->ensuresConstraints);
 211
 212            parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
 213            DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
 214                              constraintList_print( child2->requiresConstraints),
 215                              constraintList_print (child2->ensuresConstraints)
 216                              )
 217                     ));
 218            return;
 219          }
 220        else
 221          {
 222            llassert(exprNode_isError(child2) );
 223            //parent->requiresConstraints = constraintList_makeNew();
 224            //parent->ensuresConstraints = constraintList_makeNew();
 225            return;
 226          }
 227      }
 228
 229    llassert(!exprNode_isError (child1)  && ! exprNode_isError(child2) );
 230
 231    DPRINTF( (message ("Child constraints are %s %s and %s %s",
 232                      constraintList_print (child1->requiresConstraints),
 233                      constraintList_print (child1->ensuresConstraints),
 234                      constraintList_print (child2->requiresConstraints),
 235                      constraintList_print (child2->ensuresConstraints)
 236                      ) ) );
 237
 238
 239    constraintList_free(parent->requiresConstraints);
 240
 241   parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
 242
 243   if ( context_getFlag (FLG_ORCONSTRAINT) )
 244     temp = reflectChangesOr (child2->requiresConstraints, child1->ensuresConstraints);
 245   else
 246     temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
 247
 248   temp2 = constraintList_mergeRequires (parent->requiresConstraints, temp);
 249   constraintList_free(parent->requiresConstraints);
 250   constraintList_free(temp);
 251
 252   parent->requiresConstraints = temp2;
 253
 254   DPRINTF( (message ("Parent requires constraints are %s  ",
 255                      constraintList_print (parent->requiresConstraints)
 256                      ) ) );
 257
 258    constraintList_free(parent->ensuresConstraints);
 259
 260   parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
 261                                                            child2->ensuresConstraints);
 262
 263
 264   DPRINTF( (message ("Parent constraints are %s and %s ",
 265                      constraintList_print (parent->requiresConstraints),
 266                      constraintList_print (parent->ensuresConstraints)
 267                      ) ) );
 268
 269 }
 270
 271
 272
 273
 274 /*@only@*/ constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
 275 {
 276   constraintList ret;
 277   ret = constraintList_makeNew();
 278   constraintList_elements (list1, el)
 279     {
 280
 281       DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
 282       if (!resolve (el, list2) )
 283         {
 284           constraint temp;
 285           temp = constraint_copy(el);
 286           ret = constraintList_add (ret, temp);
 287         }
 288       else
 289         {
 290           DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
 291         }
 292     } end_constraintList_elements;
 293
 294     return ret;
 295 }
 296
 297
 298
 299 /* tries to resolve constraints in list pre2 using post1 */
 300 /*@only@*/ constraintList reflectChangesFreePre (/*@only@*/ constraintList pre2, /*@observer@*/ constraintList post1)
 301 {
 302   constraintList ret;
 303
 304   ret = reflectChanges (pre2, post1);
 305
 306   constraintList_free (pre2);
 307
 308   return ret;
 309 }
 310
 311
 312 /* tries to resolve constraints in list pre2 using post1 */
 313 /*@only@*/ constraintList reflectChanges (/*@observer@*/ constraintList pre2, /*@observer@*/ constraintList post1)
 314 {
 315
 316   constraintList ret;
 317   constraint temp;
 318   constraint temp2;
 319
 320   ret = constraintList_makeNew();
 321   DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
 322
 323   constraintList_elements (pre2, el)
 324     {
 325       if (!resolve (el, post1) )
 326         {
 327           temp = substitute (el, post1);
 328           if (!resolve (temp, post1) )
 329             {
 330               // try inequality substitution
 331               //constraint temp2;
 332
 333               // the inequality substitution may cause us to lose information
 334               //so we don't want to store the result but we do it anyway
 335               temp2 = constraint_copy (temp);
 336               //                  if (context_getFlag (FLG_ORCONSTRAINT) )
 337                  temp2 = inequalitySubstitute (temp2, post1);
 338                       if (!resolve (temp2, post1) )
 339                         {
 340                           temp2 = inequalitySubstituteUnsound (temp2, post1);
 341                           if (!resolve (temp2, post1) )
 342                               ret = constraintList_add (ret, temp2);
 343                         }
 344             }
 345           constraint_free(temp);
 346         }
 347     } end_constraintList_elements;
 348
 349     DPRINTF((message ("reflectChanges: returning %s", constraintList_print(ret) ) ) );
 350     return ret;
 351 }
 352
 353
 354 static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint or)
 355 {
 356   constraint c;
 357   c = orig;
 358
 359   DPRINTF((message("constraint_addor: oring %s onto %s", constraint_printOr(or), constraint_printOr(orig) ) ));
 360
 361   while (c->or != NULL)
 362     {
 363       c = c->or;
 364     }
 365   c->or = constraint_copy(or);
 366
 367   DPRINTF((message("constraint_addor: returning %s",constraint_printOr(orig) ) ));
 368
 369   return orig;
 370 }
 371
 372
 373 static bool resolveOr (/*@observer@*/ constraint c, /*@observer@*/ constraintList list)
 374 {
 375   constraint temp;
 376
 377   DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(list) ) ));
 378   temp = c;
 379
 380   do
 381     {
 382       if (resolve (temp, list) )
 383         return TRUE;
 384       temp = temp->or;
 385     }
 386   while (constraint_isDefined(temp));
 387
 388   return FALSE;
 389 }
 390
 391 /*This is a "helper" function for doResolveOr */
 392
 393 static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList post1, bool * resolved)
 394 {
 395   constraint temp;
 396
 397  if (!resolveOr (c, post1) )
 398         {
 399
 400           temp = substitute (c, post1);
 401
 402           if (!resolveOr (temp, post1) )
 403             {
 404               // try inequality substitution
 405               constraint temp2;
 406
 407               // the inequality substitution may cause us to lose information
 408               //so we don't want to store the result but we do it anyway
 409               temp2 = constraint_copy (c);
 410               //                  if (context_getFlag (FLG_ORCONSTRAINT) )
 411               temp2 = inequalitySubstitute (temp2, post1);
 412               if (!resolveOr (temp2, post1) )
 413                 {
 414                   temp2 = inequalitySubstituteUnsound (temp2, post1);
 415                   if (!resolveOr (temp2, post1) )
 416                     {
 417                       if (!constraint_same (temp, temp2) )
 418                         temp = constraint_addOr (temp, temp2);
 419                       *resolved = FALSE;
 420
 421                       constraint_free(temp2);
 422                       constraint_free(c);
 423
 424                       return temp;
 425                     }
 426                 }
 427
 428               constraint_free(temp2);
 429             }
 430           constraint_free(temp);
 431         }
 432
 433  constraint_free(c);
 434
 435  *resolved = TRUE;
 436  return NULL;
 437
 438
 439
 440 }
 441
 442 static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * resolved)
 443 {
 444   constraint ret;
 445   constraint next;
 446   constraint curr;
 447
 448   *resolved = FALSE;
 449   ret = constraint_copy(c);
 450   next = ret->or;
 451   ret->or = NULL;
 452
 453   ret = doResolve (ret, post1, resolved);
 454
 455   if (*resolved)
 456     {
 457       constraint_free(next);
 458       constraint_free(ret);
 459       return NULL;
 460     }
 461
 462   while (next != NULL)
 463     {
 464       curr = next;
 465       next = curr->or;
 466       curr->or = NULL;
 467
 468       curr = doResolve (curr, post1, resolved);
 469       if (*resolved)
 470         {
 471           constraint_free(curr);
 472           constraint_free(next);
 473           constraint_free(ret);
 474           return NULL;
 475         }
 476       ret = constraint_addOr (ret, curr);
 477     }
 478   constraint_free(curr);
 479   return ret;
 480 }
 481
 482
 483
 484
 485
 486 /* tries to resolve constraints in list pr2 using post1 */
 487 /*@only@*/ constraintList reflectChangesOr (constraintList pre2, constraintList post1)
 488 {
 489   bool resolved;
 490   constraintList ret;
 491   constraint temp;
 492   ret = constraintList_makeNew();
 493   DPRINTF((message ("reflectChangesOr: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
 494
 495   constraintList_elements (pre2, el)
 496     {
 497       temp = doResolveOr (el, post1, &resolved);
 498
 499       if (!resolved)
 500         {
 501           ret = constraintList_add(ret, temp);
 502         }
 503     } end_constraintList_elements;
 504
 505     DPRINTF((message ("reflectChangesOr: returning %s", constraintList_print(ret) ) ) );
 506     return ret;
 507 }
 508 static /*@only@*/ constraintList reflectChangesEnsures (/*@observer@*/ constraintList pre2, constraintList post1)
 509 {
 510   constraintList ret;
 511   constraint temp;
 512   ret = constraintList_makeNew();
 513   constraintList_elements (pre2, el)
 514     {
 515       if (!resolve (el, post1) )
 516         {
 517           temp = substitute (el, post1);
 518           llassert (temp != NULL);
 519
 520           if (!resolve (temp, post1) )
 521             ret = constraintList_add (ret, temp);
 522         }
 523       else
 524         {
 525           DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
 526         }
 527     } end_constraintList_elements;
 528
 529     return ret;
 530 }
 531
 532
 533 static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constraintList pre2, constraintList post1)
 534 {
 535   constraintList ret;
 536
 537   ret = reflectChangesEnsures (pre2, post1);
 538
 539   constraintList_free(pre2);
 540
 541   return ret;
 542 }
 543
 544
 545 static bool constraint_conflict (constraint c1, constraint c2)
 546 {
 547
 548   if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
 549     {
 550       if (c1->ar == EQ)
 551         if (c1->ar == c2->ar)
 552           {
 553             DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
 554             return TRUE;
 555           }
 556     }
 557
 558   DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
 559
 560   return FALSE;
 561
 562 }
 563
 564 static void constraint_fixConflict ( constraint good, /*@observer@*/ constraint conflicting) /*@modifies good@*/
 565 {
 566   if (conflicting->ar ==EQ )
 567     {
 568       good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
 569       good = constraint_simplify (good);
 570     }
 571
 572
 573 }
 574
 575 static bool conflict (constraint c, constraintList list)
 576 {
 577
 578   constraintList_elements (list, el)
 579     {
 580       if ( constraint_conflict(el, c) )
 581         {
 582           constraint_fixConflict (el, c);
 583           return TRUE;
 584         }
 585     } end_constraintList_elements;
 586
 587     return FALSE;
 588
 589 }
 590
 591 //check if constraint in list1 conflicts with constraints in List2.  If so we
 592 //remove form list1 and change list2.
 593 constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
 594 {
 595   constraintList ret;
 596   ret = constraintList_makeNew();
 597   llassert(constraintList_isDefined(list1) );
 598   constraintList_elements (list1, el)
 599     {
 600       if (! conflict (el, list2) )
 601         {
 602           constraint temp;
 603           temp = constraint_copy(el);
 604           ret = constraintList_add (ret, temp);
 605         }
 606     } end_constraintList_elements;
 607
 608     return ret;
 609 }
 610
 611 /*returns true if constraint post satifies cosntriant pre */
 612 static bool satifies (constraint pre, constraint post)
 613 {
 614   if (constraint_isAlwaysTrue (pre)  )
 615     return TRUE;
 616
 617   if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
 618     {
 619       return FALSE;
 620     }
 621   if (post->expr == NULL)
 622     {
 623       llassert(FALSE);
 624       return FALSE;
 625     }
 626
 627   return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
 628 }
 629
 630
 631 bool resolve (/*@observer@*/ constraint c, /*@observer@*/ constraintList p)
 632 {
 633   constraintList_elements (p, el)
 634     {
 635       if ( satifies (c, el) )
 636         {
 637           DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
 638           return TRUE;
 639         }
 640         DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
 641     }
 642   end_constraintList_elements;
 643   DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
 644   return FALSE;
 645 }
 646
 647 static bool arithType_canResolve (arithType ar1, arithType ar2)
 648 {
 649   switch (ar1)
 650     {
 651     case GTE:
 652     case GT:
 653       if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
 654         {
 655           return TRUE;
 656         }
 657       break;
 658
 659     case EQ:
 660       if (ar2 == EQ)
 661         return TRUE;
 662       break;
 663
 664     case LT:
 665     case LTE:
 666       //      llassert(FALSE);
 667       if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
 668         return TRUE;
 669       break;
 670     default:
 671       return FALSE;
 672     }
 673   return FALSE;
 674 }
 675
 676 /* We look for constraint which are tautologies */
 677
 678 bool constraint_isAlwaysTrue (/*@observer@*/ constraint c)
 679 {
 680   constraintExpr l, r;
 681   bool /*@unused@*/ lHasConstant, rHasConstant;
 682   int /*@unused@*/ lConstant, rConstant;
 683
 684   l = c->lexpr;
 685   r = c->expr;
 686
 687   DPRINTF(( message("constraint_IsAlwaysTrue:examining %s", constraint_print(c) ) ));
 688
 689   if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) )
 690     {
 691       int cmp;
 692       cmp = constraintExpr_compare (l, r);
 693       switch (c->ar)
 694         {
 695         case EQ:
 696           return (cmp == 0);
 697         case GT:
 698           return (cmp > 0);
 699         case GTE:
 700           return (cmp >= 0);
 701         case LTE:
 702           return (cmp <= 0);
 703         case LT:
 704           return (cmp < 0);
 705
 706         default:
 707           BADEXIT;
 708           /*@notreached@*/
 709           break;
 710         }
 711     }
 712
 713   if (constraintExpr_similar (l,r) )
 714     {
 715       switch (c->ar)
 716         {
 717         case EQ:
 718         case GTE:
 719         case LTE:
 720           return TRUE;
 721
 722         case GT:
 723         case LT:
 724           break;
 725         default:
 726           BADEXIT;
 727           /*@notreached@*/
 728           break;
 729         }
 730     }
 731
 732   l = constraintExpr_copy (c->lexpr);
 733   r = constraintExpr_copy (c->expr);
 734
 735   //  l = constraintExpr_propagateConstants (l, &lHasConstant, &lConstant);
 736   r = constraintExpr_propagateConstants (r, &rHasConstant, &rConstant);
 737
 738   if (constraintExpr_similar (l,r) && (rHasConstant ) )
 739     {
 740       DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants  %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) ));
 741       DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is  %d", rConstant ) ));
 742
 743       constraintExpr_free(l);
 744       constraintExpr_free(r);
 745
 746       switch (c->ar)
 747         {
 748         case EQ:
 749           return (rConstant == 0);
 750         case LT:
 751           return (rConstant > 0);
 752         case LTE:
 753           return (rConstant >= 0);
 754         case GTE:
 755           return (rConstant <= 0);
 756         case GT:
 757           return (rConstant < 0);
 758
 759         default:
 760           BADEXIT;
 761           /*@notreached@*/
 762           break;
 763         }
 764     }
 765       else
 766       {
 767         constraintExpr_free(l);
 768         constraintExpr_free(r);
 769         DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) ));
 770         return FALSE;
 771       }
 772
 773   BADEXIT;
 774 }
 775
 776 static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arithType ar2, /*@observer@*/ constraintExpr expr2)
 777
 778 {
 779   DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
 780
 781   if (! arithType_canResolve (ar1, ar2) )
 782     return FALSE;
 783
 784   switch (ar1)
 785  {
 786  case GTE:
 787       if (constraintExpr_similar (expr1, expr2) )
 788          return TRUE;
 789       /*@fallthrough@*/
 790  case GT:
 791    if (!  (constraintExpr_canGetValue (expr1) &&
 792            constraintExpr_canGetValue (expr2) ) )
 793      {
 794        constraintExpr e1, e2;
 795        bool p1, p2;
 796        int const1, const2;
 797
 798        e1 = constraintExpr_copy(expr1);
 799        e2 = constraintExpr_copy(expr2);
 800
 801        e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
 802
 803        e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
 804
 805        if (p1 && p2)
 806          if (const1 <= const2)
 807            if (constraintExpr_similar (e1, e2) )
 808              {
 809                constraintExpr_free(e1);
 810                constraintExpr_free(e2);
 811                return TRUE;
 812              }
 813
 814        DPRINTF( ("Can't Get value"));
 815
 816        constraintExpr_free(e1);
 817        constraintExpr_free(e2);
 818        return FALSE;
 819      }
 820
 821    if (constraintExpr_compare (expr2, expr1) >= 0)
 822      return TRUE;
 823
 824   return FALSE;
 825  case EQ:
 826    if (constraintExpr_similar (expr1, expr2) )
 827          return TRUE;
 828
 829    return FALSE;
 830  case LTE:
 831    if (constraintExpr_similar (expr1, expr2) )
 832          return TRUE;
 833    /*@fallthrough@*/
 834  case LT:
 835     if (!  (constraintExpr_canGetValue (expr1) &&
 836            constraintExpr_canGetValue (expr2) ) )
 837      {
 838       constraintExpr e1, e2;
 839        bool p1, p2;
 840        int const1, const2;
 841
 842        e1 = constraintExpr_copy(expr1);
 843        e2 = constraintExpr_copy(expr2);
 844
 845        e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
 846
 847        e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
 848
 849        if (p1 && p2)
 850          if (const1 >= const2)
 851            if (constraintExpr_similar (e1, e2) )
 852              {
 853                constraintExpr_free(e1);
 854                constraintExpr_free(e2);
 855                return TRUE;
 856              }
 857        constraintExpr_free(e1);
 858        constraintExpr_free(e2);
 859
 860        DPRINTF( ("Can't Get value"));
 861        return FALSE;
 862      }
 863
 864    if (constraintExpr_compare (expr2, expr1) <= 0)
 865      return TRUE;
 866
 867    return FALSE;
 868
 869  default:
 870      llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1) ) ) );
 871  }
 872   BADEXIT;
 873 }
 874
 875
 876 static constraint constraint_searchandreplace (/*@returned@*/ constraint c, constraintExpr old, constraintExpr new)
 877 {
 878   DPRINTF (("Doing replace for lexpr") );
 879   c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
 880   DPRINTF (("Doing replace for expr") );
 881   c->expr = constraintExpr_searchandreplace (c->expr, old, new);
 882   return c;
 883 }
 884
 885 bool constraint_search (constraint c, constraintExpr old) /*@*/
 886 {
 887   bool ret;
 888   ret = FALSE;
 889
 890   ret  = constraintExpr_search (c->lexpr, old);
 891   ret = ret || constraintExpr_search (c->expr, old);
 892   return ret;
 893 }
 894
 895 //adjust file locs and stuff
 896 static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@observer@*/ constraint old)
 897 {
 898   fileloc loc1, loc2, loc3;
 899
 900   DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
 901                      constraint_print(old))
 902                    ));
 903
 904   loc1 = constraint_getFileloc (old);
 905
 906   loc2 = constraintExpr_getFileloc (substitute->lexpr);
 907
 908   loc3 = constraintExpr_getFileloc (substitute->expr);
 909
 910
 911   // special case of an equality that "contains itself"
 912   if (constraintExpr_search (substitute->expr, substitute->lexpr) )
 913       if (fileloc_closer (loc1, loc3, loc2))
 914       {
 915         constraintExpr temp;
 916         DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
 917                    ));
 918         temp = substitute->lexpr;
 919         substitute->lexpr = substitute->expr;
 920         substitute->expr  = temp;
 921         substitute = constraint_simplify(substitute);
 922       }
 923
 924   fileloc_free (loc1);
 925   fileloc_free (loc2);
 926   fileloc_free (loc3);
 927
 928   return substitute;
 929
 930 }
 931
 932 /* If function preforms substitutes based on inequality
 933
 934    It uses the rule x >= y && b < y  ===> x >= b + 1
 935
 936    Warning this is sound but throws out information
 937  */
 938 constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p)
 939 {
 940   if (c->ar != GTE)
 941     return c;
 942
 943   constraintList_elements (p, el)
 944     {
 945        if ( el->ar == LT)
 946          //      if (!constraint_conflict (c, el) )
 947            {
 948              //constraint temp;
 949              constraintExpr  temp2;
 950
 951              /*@i22*/
 952
 953              //temp = constraint_copy(el);
 954
 955              //      temp = constraint_adjust(temp, c);
 956
 957              if (constraintExpr_same (el->expr, c->expr) )
 958                {
 959                  DPRINTF((message ("inequalitySubstitute Replacing %s in %s with  %s",
 960                                    constraintExpr_print (c->expr),
 961                                    constraint_print (c),
 962                                    constraintExpr_print (el->expr) )
 963                           ));
 964                  temp2   = constraintExpr_copy (el->lexpr);
 965                  constraintExpr_free(c->expr);
 966                  c->expr =  constraintExpr_makeIncConstraintExpr (temp2);
 967                }
 968
 969            }
 970     }
 971   end_constraintList_elements;
 972
 973   c = constraint_simplify(c);
 974   return c;
 975 }
 976
 977 /* This function performs substitutions based on the rule:
 978    for a constraint of the form expr1 >= expr2;   a < b =>
 979    a = b -1 for all a in expr1.  This will work in most cases.
 980
 981    Like inequalitySubstitute we're throwing away some information
 982 */
 983
 984 static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint c, constraintList p)
 985 {
 986   DPRINTF (( message ("Doing inequalitySubstituteUnsound " ) ));
 987
 988   if (c->ar != GTE)
 989     return c;
 990
 991   constraintList_elements (p, el)
 992     {
 993   DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_print(el), constraint_print(c) ) ));
 994        if ( ( el->ar == LTE) || (el->ar == LT) )
 995          //      if (!constraint_conflict (c, el) )
 996            {
 997              // constraint temp;
 998              constraintExpr  temp2;
 999
1000              //temp = constraint_copy(el);
1001
1002              //      temp = constraint_adjust(temp, c);
1003              temp2   = constraintExpr_copy (el->expr);
1004
1005              if (el->ar == LT)
1006                temp2  =  constraintExpr_makeDecConstraintExpr (temp2);
1007
1008              DPRINTF((message ("Replacing %s in %s with  %s",
1009                                constraintExpr_print (el->lexpr),
1010                                constraintExpr_print (c->lexpr),
1011                                constraintExpr_print (temp2) ) ));
1012
1013              c->lexpr = constraintExpr_searchandreplace (c->lexpr, el->lexpr, temp2);
1014              constraintExpr_free(temp2);
1015            }
1016     }
1017   end_constraintList_elements;
1018
1019   c = constraint_simplify(c);
1020   return c;
1021 }
1022
1023 /*@only@*/ constraint substitute (/*@observer@*/ constraint c, constraintList p)
1024 {
1025   constraint ret;
1026
1027   ret = constraint_copy(c);
1028   constraintList_elements (p, el)
1029     {
1030        if ( el->ar == EQ)
1031          if (!constraint_conflict (ret, el) )
1032
1033            {
1034              constraint temp;
1035
1036              temp = constraint_copy(el);
1037
1038              temp = constraint_adjust(temp, ret);
1039
1040              DPRINTF((message ("Substituting %s in the constraint %s",
1041                                constraint_print (temp), constraint_print (ret)
1042                                ) ) );
1043
1044
1045              ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr);
1046              DPRINTF(( message ("The new constraint is %s", constraint_print (ret) ) ));
1047              constraint_free(temp);
1048            }
1049     }
1050   end_constraintList_elements;
1051   DPRINTF(( message ("The finial new constraint is %s", constraint_print (ret) ) ));
1052
1053   ret = constraint_simplify(ret);
1054   return ret;
1055 }
1056
1057
1058 /*@only@*/ constraintList constraintList_substituteFreeTarget (/*@only@*/ constraintList target, /*@observer@*/ constraintList subList)
1059 {
1060 constraintList ret;
1061
1062 ret = constraintList_substitute (target, subList);
1063
1064 constraintList_free(target);
1065
1066 return ret;
1067 }
1068
1069 /* we try to do substitutions on each constraint in target using the constraint in sublist*/
1070
1071 /*@only@*/ constraintList constraintList_substitute (constraintList target,/*2observer@*/  constraintList subList)
1072 {
1073
1074   constraintList ret;
1075
1076   ret = constraintList_makeNew();
1077
1078   constraintList_elements(target, el)
1079   {
1080     constraint temp;
1081     #warning make sure this side effect is the right things
1082     #warning make sure that a side effect is not expected
1083
1084     temp = substitute(el, subList);
1085     ret = constraintList_add (ret, temp);
1086   }
1087   end_constraintList_elements;
1088
1089   return ret;
1090 }
1091
1092 constraint constraint_solve (constraint c)
1093 {
1094   DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
1095   c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
1096   DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
1097
1098   return c;
1099 }
1100
1101 static arithType flipAr (arithType ar)
1102 {
1103   switch (ar)
1104     {
1105     case LT:
1106       return GT;
1107     case LTE:
1108       return GTE;
1109     case EQ:
1110       return EQ;
1111     case GT:
1112       return LT;
1113     case GTE:
1114       return LTE;
1115     default:
1116       llcontbug (message("unexpected value: case not handled"));
1117     }
1118   BADEXIT;
1119 }
1120
1121 static constraint  constraint_swapLeftRight (/*@returned@*/ constraint c)
1122 {
1123   constraintExpr temp;
1124   c->ar = flipAr (c->ar);
1125   temp = c->lexpr;
1126   c->lexpr = c->expr;
1127   c->expr = temp;
1128   DPRINTF(("Swaped left and right sides of constraint"));
1129   return c;
1130 }
1131
1132
1133
1134 constraint constraint_simplify ( /*@returned@*/ constraint c)
1135 {
1136   c->lexpr = constraintExpr_simplify (c->lexpr);
1137   c->expr  = constraintExpr_simplify (c->expr);
1138
1139   if (constraintExpr_isBinaryExpr (c->lexpr) )
1140     {
1141       c = constraint_solve (c);
1142
1143       c->lexpr = constraintExpr_simplify (c->lexpr);
1144       c->expr  = constraintExpr_simplify (c->expr);
1145     }
1146
1147   if (constraintExpr_isLit(c->lexpr) && (!constraintExpr_isLit(c->expr) ) )
1148     {
1149       c = constraint_swapLeftRight(c);
1150       /*I don't think this will be an infinate loop*/
1151       c = constraint_simplify(c);
1152     }
1153   return c;
1154 }
1155
1156
1157
1158
1159 /* returns true  if fileloc for term1 is closer to file for term2 than term3*/
1160
1161 bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3)
1162 {
1163
1164   if  (!fileloc_isDefined (loc1) )
1165     return FALSE;
1166
1167   if  (!fileloc_isDefined (loc2) )
1168     return FALSE;
1169
1170   if  (!fileloc_isDefined (loc3) )
1171     return TRUE;
1172
1173
1174
1175
1176   if (fileloc_equal (loc2, loc3) )
1177     return FALSE;
1178
1179   if (fileloc_equal (loc1, loc2) )
1180     return TRUE;
1181
1182     if (fileloc_equal (loc1, loc3) )
1183     return FALSE;
1184
1185    if ( fileloc_lessthan (loc1, loc2) )
1186      {
1187        if (fileloc_lessthan (loc2, loc3) )
1188          {
1189            llassert (fileloc_lessthan (loc1, loc3) );
1190            return TRUE;
1191          }
1192        else
1193          {
1194            return FALSE;
1195          }
1196      }
1197
1198    if ( !fileloc_lessthan (loc1, loc2) )
1199      {
1200        if (!fileloc_lessthan (loc2, loc3) )
1201          {
1202            llassert (!fileloc_lessthan (loc1, loc3) );
1203            return TRUE;
1204          }
1205        else
1206          {
1207            return FALSE;
1208          }
1209      }
1210
1211    llassert(FALSE);
1212    return FALSE;
1213 }
1214
1215