src/constraintResolve.c

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