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                   else
 346                     constraint_free(temp2);
 347                 }
 348               else
 349                 {
 350                   constraint_free(temp2);
 351                 }
 352             }
 353           constraint_free(temp);
 354         }
 355     } end_constraintList_elements;
 356
 357     DPRINTF((message ("reflectChanges: returning %s", constraintList_print(ret) ) ) );
 358     return ret;
 359 }
 360
 361
 362 static constraint constraint_addOr (/*@returned@*/ constraint orig, /*@observer@*/ constraint or)
 363 {
 364   constraint c;
 365   c = orig;
 366
 367   DPRINTF((message("constraint_addor: oring %s onto %s", constraint_printOr(or), constraint_printOr(orig) ) ));
 368
 369   while (c->or != NULL)
 370     {
 371       c = c->or;
 372     }
 373   c->or = constraint_copy(or);
 374
 375   DPRINTF((message("constraint_addor: returning %s",constraint_printOr(orig) ) ));
 376
 377   return orig;
 378 }
 379
 380
 381 static bool resolveOr (/*@observer@*/ constraint c, /*@observer@*/ constraintList list)
 382 {
 383   constraint temp;
 384
 385   DPRINTF(( message("resolveOr: constraint %s and list %s", constraint_printOr(c), constraintList_print(list) ) ));
 386   temp = c;
 387
 388   do
 389     {
 390       if (resolve (temp, list) )
 391         return TRUE;
 392       temp = temp->or;
 393     }
 394   while (constraint_isDefined(temp));
 395
 396   return FALSE;
 397 }
 398
 399 /*This is a "helper" function for doResolveOr */
 400
 401 static /*@only@*/ constraint doResolve (/*@only@*/ constraint c, constraintList post1, bool * resolved)
 402 {
 403   constraint temp;
 404
 405  if (!resolveOr (c, post1) )
 406         {
 407
 408           temp = substitute (c, post1);
 409
 410           if (!resolveOr (temp, post1) )
 411             {
 412               // try inequality substitution
 413               constraint temp2;
 414
 415               // the inequality substitution may cause us to lose information
 416               //so we don't want to store the result but we do it anyway
 417               temp2 = constraint_copy (c);
 418               //                  if (context_getFlag (FLG_ORCONSTRAINT) )
 419               temp2 = inequalitySubstitute (temp2, post1);
 420               if (!resolveOr (temp2, post1) )
 421                 {
 422                   temp2 = inequalitySubstituteUnsound (temp2, post1);
 423                   if (!resolveOr (temp2, post1) )
 424                     {
 425                       if (!constraint_same (temp, temp2) )
 426                         temp = constraint_addOr (temp, temp2);
 427                       *resolved = FALSE;
 428
 429                       constraint_free(temp2);
 430                       constraint_free(c);
 431
 432                       return temp;
 433                     }
 434                 }
 435
 436               constraint_free(temp2);
 437             }
 438           constraint_free(temp);
 439         }
 440
 441  constraint_free(c);
 442
 443  *resolved = TRUE;
 444  return NULL;
 445
 446
 447
 448 }
 449
 450 static /*@only@*/ constraint doResolveOr (constraint c, constraintList post1, /*@out@*/bool * resolved)
 451 {
 452   constraint ret;
 453   constraint next;
 454   constraint curr;
 455
 456   *resolved = FALSE;
 457   ret = constraint_copy(c);
 458   next = ret->or;
 459   ret->or = NULL;
 460
 461   ret = doResolve (ret, post1, resolved);
 462
 463   if (*resolved)
 464     {
 465       if (next != NULL)
 466         constraint_free(next);
 467
 468       /*we don't need to free ret when resolved is false because ret is null*/
 469       llassert(ret == NULL);
 470
 471        return NULL;
 472     }
 473
 474   while (next != NULL)
 475     {
 476       curr = next;
 477       next = curr->or;
 478       curr->or = NULL;
 479
 480       curr = doResolve (curr, post1, resolved);
 481       if (*resolved)
 482         {
 483           /* curr is null so we don't try to free it*/
 484           llassert(curr == NULL);
 485
 486           if (next != NULL)
 487             constraint_free(next);
 488
 489           constraint_free(ret);
 490           return NULL;
 491         }
 492       ret = constraint_addOr (ret, curr);
 493       constraint_free(curr);
 494     }
 495
 496   return ret;
 497 }
 498
 499
 500
 501
 502
 503 /* tries to resolve constraints in list pr2 using post1 */
 504 /*@only@*/ constraintList reflectChangesOr (constraintList pre2, constraintList post1)
 505 {
 506   bool resolved;
 507   constraintList ret;
 508   constraint temp;
 509   ret = constraintList_makeNew();
 510   DPRINTF((message ("reflectChangesOr: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
 511
 512   constraintList_elements (pre2, el)
 513     {
 514       temp = doResolveOr (el, post1, &resolved);
 515
 516       if (!resolved)
 517         {
 518           ret = constraintList_add(ret, temp);
 519         }
 520       else
 521         {
 522      /*we don't need to free ret when resolved is false because ret is null*/
 523           llassert(temp == NULL);
 524         }
 525
 526     } end_constraintList_elements;
 527
 528     DPRINTF((message ("reflectChangesOr: returning %s", constraintList_print(ret) ) ) );
 529     return ret;
 530 }
 531 static /*@only@*/ constraintList reflectChangesEnsures (/*@observer@*/ constraintList pre2, constraintList post1)
 532 {
 533   constraintList ret;
 534   constraint temp;
 535   ret = constraintList_makeNew();
 536   constraintList_elements (pre2, el)
 537     {
 538       if (!resolve (el, post1) )
 539         {
 540           temp = substitute (el, post1);
 541           llassert (temp != NULL);
 542
 543           if (!resolve (temp, post1) )
 544             ret = constraintList_add (ret, temp);
 545           else
 546             constraint_free(temp);
 547         }
 548       else
 549         {
 550           DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
 551         }
 552     } end_constraintList_elements;
 553
 554     return ret;
 555 }
 556
 557
 558 static /*@only@*/ constraintList reflectChangesEnsuresFree1 (/*@only@*/ constraintList pre2, constraintList post1)
 559 {
 560   constraintList ret;
 561
 562   ret = reflectChangesEnsures (pre2, post1);
 563
 564   constraintList_free(pre2);
 565
 566   return ret;
 567 }
 568
 569
 570 static bool constraint_conflict (constraint c1, constraint c2)
 571 {
 572
 573   if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
 574     {
 575       if (c1->ar == EQ)
 576         if (c1->ar == c2->ar)
 577           {
 578             DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
 579             return TRUE;
 580           }
 581     }
 582
 583   DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
 584
 585   return FALSE;
 586
 587 }
 588
 589 static void constraint_fixConflict ( constraint good, /*@observer@*/ constraint conflicting) /*@modifies good@*/
 590 {
 591   if (conflicting->ar ==EQ )
 592     {
 593       good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
 594       good = constraint_simplify (good);
 595     }
 596
 597
 598 }
 599
 600 static bool conflict (constraint c, constraintList list)
 601 {
 602
 603   constraintList_elements (list, el)
 604     {
 605       if ( constraint_conflict(el, c) )
 606         {
 607           constraint_fixConflict (el, c);
 608           return TRUE;
 609         }
 610     } end_constraintList_elements;
 611
 612     return FALSE;
 613
 614 }
 615
 616 //check if constraint in list1 conflicts with constraints in List2.  If so we
 617 //remove form list1 and change list2.
 618 constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
 619 {
 620   constraintList ret;
 621   ret = constraintList_makeNew();
 622   llassert(constraintList_isDefined(list1) );
 623   constraintList_elements (list1, el)
 624     {
 625       if (! conflict (el, list2) )
 626         {
 627           constraint temp;
 628           temp = constraint_copy(el);
 629           ret = constraintList_add (ret, temp);
 630         }
 631     } end_constraintList_elements;
 632
 633     return ret;
 634 }
 635
 636 /*returns true if constraint post satifies cosntriant pre */
 637 static bool satifies (constraint pre, constraint post)
 638 {
 639   if (constraint_isAlwaysTrue (pre)  )
 640     return TRUE;
 641
 642   if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
 643     {
 644       return FALSE;
 645     }
 646   if (post->expr == NULL)
 647     {
 648       llassert(FALSE);
 649       return FALSE;
 650     }
 651
 652   return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
 653 }
 654
 655
 656 bool resolve (/*@observer@*/ constraint c, /*@observer@*/ constraintList p)
 657 {
 658   constraintList_elements (p, el)
 659     {
 660       if ( satifies (c, el) )
 661         {
 662           DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
 663           return TRUE;
 664         }
 665         DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
 666     }
 667   end_constraintList_elements;
 668   DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
 669   return FALSE;
 670 }
 671
 672 static bool arithType_canResolve (arithType ar1, arithType ar2)
 673 {
 674   switch (ar1)
 675     {
 676     case GTE:
 677     case GT:
 678       if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
 679         {
 680           return TRUE;
 681         }
 682       break;
 683
 684     case EQ:
 685       if (ar2 == EQ)
 686         return TRUE;
 687       break;
 688
 689     case LT:
 690     case LTE:
 691       //      llassert(FALSE);
 692       if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
 693         return TRUE;
 694       break;
 695     default:
 696       return FALSE;
 697     }
 698   return FALSE;
 699 }
 700
 701 /* We look for constraint which are tautologies */
 702
 703 bool constraint_isAlwaysTrue (/*@observer@*/ constraint c)
 704 {
 705   constraintExpr l, r;
 706   bool /*@unused@*/ lHasConstant, rHasConstant;
 707   int /*@unused@*/ lConstant, rConstant;
 708
 709   l = c->lexpr;
 710   r = c->expr;
 711
 712   DPRINTF(( message("constraint_IsAlwaysTrue:examining %s", constraint_print(c) ) ));
 713
 714   if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) )
 715     {
 716       int cmp;
 717       cmp = constraintExpr_compare (l, r);
 718       switch (c->ar)
 719         {
 720         case EQ:
 721           return (cmp == 0);
 722         case GT:
 723           return (cmp > 0);
 724         case GTE:
 725           return (cmp >= 0);
 726         case LTE:
 727           return (cmp <= 0);
 728         case LT:
 729           return (cmp < 0);
 730
 731         default:
 732           BADEXIT;
 733           /*@notreached@*/
 734           break;
 735         }
 736     }
 737
 738   if (constraintExpr_similar (l,r) )
 739     {
 740       switch (c->ar)
 741         {
 742         case EQ:
 743         case GTE:
 744         case LTE:
 745           return TRUE;
 746
 747         case GT:
 748         case LT:
 749           break;
 750         default:
 751           BADEXIT;
 752           /*@notreached@*/
 753           break;
 754         }
 755     }
 756
 757   l = constraintExpr_copy (c->lexpr);
 758   r = constraintExpr_copy (c->expr);
 759
 760   //  l = constraintExpr_propagateConstants (l, &lHasConstant, &lConstant);
 761   r = constraintExpr_propagateConstants (r, &rHasConstant, &rConstant);
 762
 763   if (constraintExpr_similar (l,r) && (rHasConstant ) )
 764     {
 765       DPRINTF(( message("constraint_IsAlwaysTrue: after removing constants  %s and %s are similar", constraintExpr_unparse(l), constraintExpr_unparse(r) ) ));
 766       DPRINTF(( message("constraint_IsAlwaysTrue: rconstant is  %d", rConstant ) ));
 767
 768       constraintExpr_free(l);
 769       constraintExpr_free(r);
 770
 771       switch (c->ar)
 772         {
 773         case EQ:
 774           return (rConstant == 0);
 775         case LT:
 776           return (rConstant > 0);
 777         case LTE:
 778           return (rConstant >= 0);
 779         case GTE:
 780           return (rConstant <= 0);
 781         case GT:
 782           return (rConstant < 0);
 783
 784         default:
 785           BADEXIT;
 786           /*@notreached@*/
 787           break;
 788         }
 789     }
 790       else
 791       {
 792         constraintExpr_free(l);
 793         constraintExpr_free(r);
 794         DPRINTF(( message("Constraint %s is not always true", constraint_print(c) ) ));
 795         return FALSE;
 796       }
 797
 798   BADEXIT;
 799 }
 800
 801 static bool rangeCheck (arithType ar1, /*@observer@*/ constraintExpr expr1, arithType ar2, /*@observer@*/ constraintExpr expr2)
 802
 803 {
 804   DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
 805
 806   if (! arithType_canResolve (ar1, ar2) )
 807     return FALSE;
 808
 809   switch (ar1)
 810  {
 811  case GTE:
 812       if (constraintExpr_similar (expr1, expr2) )
 813          return TRUE;
 814       /*@fallthrough@*/
 815  case GT:
 816    if (!  (constraintExpr_canGetValue (expr1) &&
 817            constraintExpr_canGetValue (expr2) ) )
 818      {
 819        constraintExpr e1, e2;
 820        bool p1, p2;
 821        int const1, const2;
 822
 823        e1 = constraintExpr_copy(expr1);
 824        e2 = constraintExpr_copy(expr2);
 825
 826        e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
 827
 828        e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
 829
 830        if (p1 && p2)
 831          if (const1 <= const2)
 832            if (constraintExpr_similar (e1, e2) )
 833              {
 834                constraintExpr_free(e1);
 835                constraintExpr_free(e2);
 836                return TRUE;
 837              }
 838
 839        DPRINTF( ("Can't Get value"));
 840
 841        constraintExpr_free(e1);
 842        constraintExpr_free(e2);
 843        return FALSE;
 844      }
 845
 846    if (constraintExpr_compare (expr2, expr1) >= 0)
 847      return TRUE;
 848
 849   return FALSE;
 850  case EQ:
 851    if (constraintExpr_similar (expr1, expr2) )
 852          return TRUE;
 853
 854    return FALSE;
 855  case LTE:
 856    if (constraintExpr_similar (expr1, expr2) )
 857          return TRUE;
 858    /*@fallthrough@*/
 859  case LT:
 860     if (!  (constraintExpr_canGetValue (expr1) &&
 861            constraintExpr_canGetValue (expr2) ) )
 862      {
 863       constraintExpr e1, e2;
 864        bool p1, p2;
 865        int const1, const2;
 866
 867        e1 = constraintExpr_copy(expr1);
 868        e2 = constraintExpr_copy(expr2);
 869
 870        e1 = constraintExpr_propagateConstants (e1, &p1, &const1);
 871
 872        e2 = constraintExpr_propagateConstants (e2, &p2, &const2);
 873
 874        if (p1 && p2)
 875          if (const1 >= const2)
 876            if (constraintExpr_similar (e1, e2) )
 877              {
 878                constraintExpr_free(e1);
 879                constraintExpr_free(e2);
 880                return TRUE;
 881              }
 882        constraintExpr_free(e1);
 883        constraintExpr_free(e2);
 884
 885        DPRINTF( ("Can't Get value"));
 886        return FALSE;
 887      }
 888
 889    if (constraintExpr_compare (expr2, expr1) <= 0)
 890      return TRUE;
 891
 892    return FALSE;
 893
 894  default:
 895      llcontbug((message("Unhandled case in switch: %q", arithType_print(ar1) ) ) );
 896  }
 897   BADEXIT;
 898 }
 899
 900
 901 static constraint constraint_searchandreplace (/*@returned@*/ constraint c, constraintExpr old, constraintExpr new)
 902 {
 903   DPRINTF (("Doing replace for lexpr") );
 904   c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
 905   DPRINTF (("Doing replace for expr") );
 906   c->expr = constraintExpr_searchandreplace (c->expr, old, new);
 907   return c;
 908 }
 909
 910 bool constraint_search (constraint c, constraintExpr old) /*@*/
 911 {
 912   bool ret;
 913   ret = FALSE;
 914
 915   ret  = constraintExpr_search (c->lexpr, old);
 916   ret = ret || constraintExpr_search (c->expr, old);
 917   return ret;
 918 }
 919
 920 //adjust file locs and stuff
 921 static constraint constraint_adjust (/*@returned@*/ constraint substitute, /*@observer@*/ constraint old)
 922 {
 923   fileloc loc1, loc2, loc3;
 924
 925   DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
 926                      constraint_print(old))
 927                    ));
 928
 929   loc1 = constraint_getFileloc (old);
 930
 931   loc2 = constraintExpr_getFileloc (substitute->lexpr);
 932
 933   loc3 = constraintExpr_getFileloc (substitute->expr);
 934
 935
 936   // special case of an equality that "contains itself"
 937   if (constraintExpr_search (substitute->expr, substitute->lexpr) )
 938       if (fileloc_closer (loc1, loc3, loc2))
 939       {
 940         constraintExpr temp;
 941         DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
 942                    ));
 943         temp = substitute->lexpr;
 944         substitute->lexpr = substitute->expr;
 945         substitute->expr  = temp;
 946         substitute = constraint_simplify(substitute);
 947       }
 948
 949   fileloc_free (loc1);
 950   fileloc_free (loc2);
 951   fileloc_free (loc3);
 952
 953   return substitute;
 954
 955 }
 956
 957 /* If function preforms substitutes based on inequality
 958
 959    It uses the rule x >= y && b < y  ===> x >= b + 1
 960
 961    Warning this is sound but throws out information
 962  */
 963 constraint  inequalitySubstitute  (/*@returned@*/ constraint c, constraintList p)
 964 {
 965   if (c->ar != GTE)
 966     return c;
 967
 968   constraintList_elements (p, el)
 969     {
 970        if ( el->ar == LT)
 971          //      if (!constraint_conflict (c, el) )
 972            {
 973              //constraint temp;
 974              constraintExpr  temp2;
 975
 976              /*@i22*/
 977
 978              //temp = constraint_copy(el);
 979
 980              //      temp = constraint_adjust(temp, c);
 981
 982              if (constraintExpr_same (el->expr, c->expr) )
 983                {
 984                  DPRINTF((message ("inequalitySubstitute Replacing %s in %s with  %s",
 985                                    constraintExpr_print (c->expr),
 986                                    constraint_print (c),
 987                                    constraintExpr_print (el->expr) )
 988                           ));
 989                  temp2   = constraintExpr_copy (el->lexpr);
 990                  constraintExpr_free(c->expr);
 991                  c->expr =  constraintExpr_makeIncConstraintExpr (temp2);
 992                }
 993
 994            }
 995     }
 996   end_constraintList_elements;
 997
 998   c = constraint_simplify(c);
 999   return c;
1000 }
1001
1002 /* This function performs substitutions based on the rule:
1003    for a constraint of the form expr1 >= expr2;   a < b =>
1004    a = b -1 for all a in expr1.  This will work in most cases.
1005
1006    Like inequalitySubstitute we're throwing away some information
1007 */
1008
1009 static constraint  inequalitySubstituteUnsound  (/*@returned@*/ constraint c, constraintList p)
1010 {
1011   DPRINTF (( message ("Doing inequalitySubstituteUnsound " ) ));
1012
1013   if (c->ar != GTE)
1014     return c;
1015
1016   constraintList_elements (p, el)
1017     {
1018   DPRINTF (( message ("inequalitySubstituteUnsound examining substituting %s on %s", constraint_print(el), constraint_print(c) ) ));
1019        if ( ( el->ar == LTE) || (el->ar == LT) )
1020          //      if (!constraint_conflict (c, el) )
1021            {
1022              // constraint temp;
1023              constraintExpr  temp2;
1024
1025              //temp = constraint_copy(el);
1026
1027              //      temp = constraint_adjust(temp, c);
1028              temp2   = constraintExpr_copy (el->expr);
1029
1030              if (el->ar == LT)
1031                temp2  =  constraintExpr_makeDecConstraintExpr (temp2);
1032
1033              DPRINTF((message ("Replacing %s in %s with  %s",
1034                                constraintExpr_print (el->lexpr),
1035                                constraintExpr_print (c->lexpr),
1036                                constraintExpr_print (temp2) ) ));
1037
1038              c->lexpr = constraintExpr_searchandreplace (c->lexpr, el->lexpr, temp2);
1039              constraintExpr_free(temp2);
1040            }
1041     }
1042   end_constraintList_elements;
1043
1044   c = constraint_simplify(c);
1045   return c;
1046 }
1047
1048 /*@only@*/ constraint substitute (/*@observer@*/ constraint c, constraintList p)
1049 {
1050   constraint ret;
1051
1052   ret = constraint_copy(c);
1053   constraintList_elements (p, el)
1054     {
1055        if ( el->ar == EQ)
1056          if (!constraint_conflict (ret, el) )
1057
1058            {
1059              constraint temp;
1060
1061              temp = constraint_copy(el);
1062
1063              temp = constraint_adjust(temp, ret);
1064
1065              DPRINTF((message ("Substituting %s in the constraint %s",
1066                                constraint_print (temp), constraint_print (ret)
1067                                ) ) );
1068
1069
1070              ret = constraint_searchandreplace (ret, temp->lexpr, temp->expr);
1071              DPRINTF(( message ("The new constraint is %s", constraint_print (ret) ) ));
1072              constraint_free(temp);
1073            }
1074     }
1075   end_constraintList_elements;
1076   DPRINTF(( message ("The finial new constraint is %s", constraint_print (ret) ) ));
1077
1078   ret = constraint_simplify(ret);
1079   return ret;
1080 }
1081
1082
1083 /*@only@*/ constraintList constraintList_substituteFreeTarget (/*@only@*/ constraintList target, /*@observer@*/ constraintList subList)
1084 {
1085 constraintList ret;
1086
1087 ret = constraintList_substitute (target, subList);
1088
1089 constraintList_free(target);
1090
1091 return ret;
1092 }
1093
1094 /* we try to do substitutions on each constraint in target using the constraint in sublist*/
1095
1096 /*@only@*/ constraintList constraintList_substitute (constraintList target,/*2observer@*/  constraintList subList)
1097 {
1098
1099   constraintList ret;
1100
1101   ret = constraintList_makeNew();
1102
1103   constraintList_elements(target, el)
1104   {
1105     constraint temp;
1106     #warning make sure that a side effect is not expected
1107
1108     temp = substitute(el, subList);
1109     ret = constraintList_add (ret, temp);
1110   }
1111   end_constraintList_elements;
1112
1113   return ret;
1114 }
1115
1116 constraint constraint_solve (/*@returned@*/ constraint c)
1117 {
1118   DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
1119   c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
1120   DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
1121
1122   return c;
1123 }
1124
1125 static arithType flipAr (arithType ar)
1126 {
1127   switch (ar)
1128     {
1129     case LT:
1130       return GT;
1131     case LTE:
1132       return GTE;
1133     case EQ:
1134       return EQ;
1135     case GT:
1136       return LT;
1137     case GTE:
1138       return LTE;
1139     default:
1140       llcontbug (message("unexpected value: case not handled"));
1141     }
1142   BADEXIT;
1143 }
1144
1145 static constraint  constraint_swapLeftRight (/*@returned@*/ constraint c)
1146 {
1147   constraintExpr temp;
1148   c->ar = flipAr (c->ar);
1149   temp = c->lexpr;
1150   c->lexpr = c->expr;
1151   c->expr = temp;
1152   DPRINTF(("Swaped left and right sides of constraint"));
1153   return c;
1154 }
1155
1156
1157
1158 constraint constraint_simplify ( /*@returned@*/ constraint c)
1159 {
1160   c->lexpr = constraintExpr_simplify (c->lexpr);
1161   c->expr  = constraintExpr_simplify (c->expr);
1162
1163   if (constraintExpr_isBinaryExpr (c->lexpr) )
1164     {
1165       c = constraint_solve (c);
1166
1167       c->lexpr = constraintExpr_simplify (c->lexpr);
1168       c->expr  = constraintExpr_simplify (c->expr);
1169     }
1170
1171   if (constraintExpr_isLit(c->lexpr) && (!constraintExpr_isLit(c->expr) ) )
1172     {
1173       c = constraint_swapLeftRight(c);
1174       /*I don't think this will be an infinate loop*/
1175       c = constraint_simplify(c);
1176     }
1177   return c;
1178 }
1179
1180
1181
1182
1183 /* returns true  if fileloc for term1 is closer to file for term2 than term3*/
1184
1185 bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3)
1186 {
1187
1188   if  (!fileloc_isDefined (loc1) )
1189     return FALSE;
1190
1191   if  (!fileloc_isDefined (loc2) )
1192     return FALSE;
1193
1194   if  (!fileloc_isDefined (loc3) )
1195     return TRUE;
1196
1197
1198
1199
1200   if (fileloc_equal (loc2, loc3) )
1201     return FALSE;
1202
1203   if (fileloc_equal (loc1, loc2) )
1204     return TRUE;
1205
1206     if (fileloc_equal (loc1, loc3) )
1207     return FALSE;
1208
1209    if ( fileloc_lessthan (loc1, loc2) )
1210      {
1211        if (fileloc_lessthan (loc2, loc3) )
1212          {
1213            llassert (fileloc_lessthan (loc1, loc3) );
1214            return TRUE;
1215          }
1216        else
1217          {
1218            return FALSE;
1219          }
1220      }
1221
1222    if ( !fileloc_lessthan (loc1, loc2) )
1223      {
1224        if (!fileloc_lessthan (loc2, loc3) )
1225          {
1226            llassert (!fileloc_lessthan (loc1, loc3) );
1227            return TRUE;
1228          }
1229        else
1230          {
1231            return FALSE;
1232          }
1233      }
1234
1235    llassert(FALSE);
1236    return FALSE;
1237 }
1238
1239