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