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