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