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