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