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