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