src/constraintResolve.c

   1 /*
   2 *
   3 ** constraintResolve.c
   4 */
   5
   6 //#define DEBUGPRINT 1
   7
   8 # include <ctype.h> /* for isdigit */
   9 # include "lclintMacros.nf"
  10 # include "basic.h"
  11 # include "cgrammar.h"
  12 # include "cgrammar_tokens.h"
  13
  14 # include "exprChecks.h"
  15 # include "aliasChecks.h"
  16 # include "exprNodeSList.h"
  17 //# include "exprData.i"
  18
  19 #include "constraintExpr.h"
  20
  21
  22
  23
  24
  25 constraintList reflectChanges (constraintList pre2, constraintList post1);
  26 constraint substitute (constraint c, constraintList p);
  27 constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
  28 bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
  29 bool satifies (constraint pre, constraint post);
  30 bool resolve (constraint c, constraintList p);
  31 constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
  32 constraint constraint_simplify (constraint c);
  33
  34 constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
  35
  36 constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
  37
  38 constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
  39 constraint  inequalitySubstitute  (constraint c, constraintList p);
  40
  41 /*********************************************/
  42
  43
  44 constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
  45 {
  46   constraintList ret;
  47   constraintList temp;
  48   ret = constraintList_new();
  49
  50   ret = reflectChangesEnsures (list1, list2);
  51   ret = constraintList_fixConflicts (ret, list2);
  52   ret = constraintList_subsumeEnsures (ret, list2);
  53   list2 = constraintList_subsumeEnsures (list2, ret);
  54   temp = constraintList_copy(list2);
  55
  56   temp = constraintList_addList (temp, ret);
  57   return temp;
  58   //ret = constraintList_addList (ret, list2);
  59   //return ret;
  60 }
  61
  62
  63 /* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */
  64 /* { */
  65
  66 /*   constraintList ret; */
  67 /*   constraintList temp; */
  68 /*   ret = constraintList_new(); */
  69
  70 /*   ret = reflectChangesEnsures (list1, list2); */
  71 /*   ret = constraintList_fixConflicts (ret, list2); */
  72 /*   ret = constraintList_subsumeEnsures (ret, list2); */
  73 /*   list2 = constraintList_subsumeEnsures (list2, ret); */
  74 /*   temp = constraintList_copy(list2); */
  75
  76 /*   temp = constraintList_addList (temp, ret); */
  77 /*   return temp; */
  78 /*   //ret = constraintList_addList (ret, list2); */
  79 /*   //return ret; */
  80 /* } */
  81
  82
  83 constraintList checkCall (exprNode fcn, exprNodeList arglist)
  84 {
  85   constraintList preconditions;
  86   uentry temp;
  87   DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
  88
  89   temp = exprNode_getUentry (fcn);
  90
  91   preconditions = uentry_getFcnPreconditions (temp);
  92
  93   if (preconditions)
  94     {
  95       preconditions = constraintList_copy(preconditions);
  96       preconditions= constraintList_togglePost (preconditions);
  97       preconditions = constraintList_doSRefFixConstraintParam (preconditions, arglist);
  98     }
  99   else
 100     {
 101       preconditions = constraintList_new();
 102     }
 103
 104   return preconditions;
 105 }
 106
 107 constraintList getPostConditions (exprNode fcn, exprNodeList arglist, exprNode fcnCall)
 108 {
 109   constraintList postconditions;
 110   uentry temp;
 111   DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
 112
 113   temp = exprNode_getUentry (fcn);
 114
 115   postconditions = uentry_getFcnPostconditions (temp);
 116
 117   if (postconditions)
 118     {
 119       postconditions = constraintList_copy(postconditions);
 120       postconditions = constraintList_doFixResult (postconditions, fcnCall);
 121       postconditions = constraintList_doSRefFixConstraintParam (postconditions, arglist);
 122     }
 123   else
 124     {
 125       postconditions = constraintList_new();
 126     }
 127
 128   return postconditions;
 129 }
 130
 131 void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 132 {
 133   constraintList temp;
 134
 135   DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
 136
 137   DPRINTF( (message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
 138
 139   if (exprNode_isError (child1)  || exprNode_isError(child2) )
 140      {
 141        if (exprNode_isError (child1) && !exprNode_isError(child2) )
 142          {
 143            parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
 144            parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
 145            DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
 146                              constraintList_print( child2->requiresConstraints),
 147                              constraintList_print (child2->ensuresConstraints)
 148                              )
 149                     ));
 150            return;
 151          }
 152        else
 153          {
 154            llassert(exprNode_isError(child2) );
 155            parent->requiresConstraints = constraintList_new();
 156            parent->ensuresConstraints = constraintList_new();
 157            return;
 158          }
 159      }
 160
 161    llassert(!exprNode_isError (child1)  && ! exprNode_isError(child2) );
 162
 163   DPRINTF( (message ("Child constraints are %s %s and %s %s",
 164                      constraintList_print (child1->requiresConstraints),
 165                      constraintList_print (child1->ensuresConstraints),
 166                      constraintList_print (child2->requiresConstraints),
 167                      constraintList_print (child2->ensuresConstraints)
 168                      ) ) );
 169
 170   parent->requiresConstraints = constraintList_new();
 171   parent->ensuresConstraints = constraintList_new();
 172
 173   parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
 174
 175   temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
 176   parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);
 177
 178   parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
 179                                                            child2->ensuresConstraints);
 180
 181   DPRINTF( (message ("Parent constraints are %s and %s ",
 182                      constraintList_print (parent->requiresConstraints),
 183                      constraintList_print (parent->ensuresConstraints)
 184                      ) ) );
 185
 186 }
 187
 188
 189
 190
 191 constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
 192 {
 193   constraintList ret;
 194   ret = constraintList_new();
 195   constraintList_elements (list1, el)
 196     {
 197
 198       DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
 199       if (!resolve (el, list2) )
 200         {
 201             ret = constraintList_add (ret, el);
 202         }
 203       else
 204         {
 205           DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
 206         }
 207     } end_constraintList_elements;
 208
 209     return ret;
 210 }
 211
 212
 213 constraintList reflectChanges (constraintList pre2, constraintList post1)
 214 {
 215
 216   constraintList ret;
 217   constraint temp;
 218   ret = constraintList_new();
 219   DPRINTF((message ("reflectChanges: lists %s and %s", constraintList_print(pre2), constraintList_print(post1) )));
 220
 221   constraintList_elements (pre2, el)
 222     {
 223       if (!resolve (el, post1) )
 224         {
 225           temp = substitute (el, post1);
 226           if (!resolve (temp, post1) )
 227             {
 228               // try inequality substitution
 229               constraint temp2;
 230
 231               // the inequality substitution may cause us to lose information
 232               //so we don't want to store the result but we do it anyway
 233               temp2 = constraint_copy (temp);
 234               temp2 = inequalitySubstitute (temp, post1);
 235               if (!resolve (temp2, post1) )
 236                   ret = constraintList_add (ret, temp2);
 237             }
 238         }
 239     } end_constraintList_elements;
 240
 241     DPRINTF((message ("reflectChanges: returning %s", constraintList_print(ret) ) ) );
 242     return ret;
 243 }
 244
 245
 246
 247 constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
 248 {
 249   constraintList ret;
 250   constraint temp;
 251   ret = constraintList_new();
 252   constraintList_elements (pre2, el)
 253     {
 254       if (!resolve (el, post1) )
 255         {
 256           temp = substitute (el, post1);
 257           llassert (temp != NULL);
 258
 259           if (!resolve (temp, post1) )
 260             ret = constraintList_add (ret, temp);
 261         }
 262       else
 263         {
 264           DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
 265         }
 266     } end_constraintList_elements;
 267
 268     return ret;
 269 }
 270
 271
 272 bool constraint_conflict (constraint c1, constraint c2)
 273 {
 274
 275   if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
 276     {
 277       if (c1->ar == EQ)
 278         if (c1->ar == c2->ar)
 279           {
 280             DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
 281             return TRUE;
 282           }
 283     }
 284
 285   DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
 286
 287   return FALSE;
 288
 289 }
 290
 291 void constraint_fixConflict (constraint good, constraint conflicting)
 292 {
 293   constraint temp;
 294   if (conflicting->ar ==EQ )
 295     {
 296       good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
 297       temp = constraint_simplify (good);
 298       constraint_overWrite (good, temp);
 299     }
 300
 301
 302 }
 303
 304 bool conflict (constraint c, constraintList list)
 305 {
 306
 307    constraintList_elements (list, el)
 308     {
 309       if ( constraint_conflict(el, c) )
 310         {
 311           constraint_fixConflict (el, c);
 312           return TRUE;
 313         }
 314     } end_constraintList_elements;
 315
 316     return FALSE;
 317
 318
 319 }
 320
 321 //check if constraint in list1 and conflict with constraints in List2.  If so we
 322 //remove form list1 and (optionally) change list2.
 323 constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
 324 {
 325   constraintList ret;
 326   ret = constraintList_new();
 327   constraintList_elements (list1, el)
 328     {
 329       if (! conflict (el, list2) )
 330         {
 331             ret = constraintList_add (ret, el);
 332         }
 333     } end_constraintList_elements;
 334
 335     return ret;
 336
 337
 338 }
 339
 340 bool resolve (constraint c, constraintList p)
 341 {
 342   constraintList_elements (p, el)
 343     {
 344       if ( satifies (c, el) )
 345         {
 346           DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
 347           return TRUE;
 348         }
 349         DPRINTF ( (message ("\n%s does not satify %s\n ", constraint_print(el), constraint_print(c) ) ) );
 350     }
 351   end_constraintList_elements;
 352   DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
 353   return FALSE;
 354 }
 355
 356
 357 /*returns true if cosntraint post satifies cosntriant pre */
 358 bool satifies (constraint pre, constraint post)
 359 {
 360   if (constraint_isAlwaysTrue (pre)  )
 361     return TRUE;
 362
 363   if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
 364     {
 365       return FALSE;
 366     }
 367   if (post->expr == NULL)
 368     {
 369       llassert(FALSE);
 370       return FALSE;
 371     }
 372
 373   return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
 374 }
 375
 376 bool arithType_canResolve (arithType ar1, arithType ar2)
 377 {
 378   switch (ar1)
 379     {
 380     case GTE:
 381     case GT:
 382       if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
 383         {
 384           return TRUE;
 385         }
 386       break;
 387
 388     case EQ:
 389       if (ar2 == EQ)
 390         return TRUE;
 391       break;
 392
 393     case LT:
 394     case LTE:
 395       //      llassert(FALSE);
 396       if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
 397         return TRUE;
 398     default:
 399       return FALSE;
 400     }
 401   return FALSE;
 402 }
 403
 404 bool constraint_isAlwaysTrue (constraint c)
 405 {
 406   constraintExpr l, r;
 407   l = c->lexpr;
 408   r = c->expr;
 409
 410   if (constraintExpr_canGetValue(l) && constraintExpr_canGetValue(r) )
 411     {
 412       int cmp;
 413       cmp = constraintExpr_compare (l, r);
 414       switch (c->ar)
 415         {
 416         case EQ:
 417           return (cmp == 0);
 418         case GT:
 419           return (cmp > 0);
 420         case GTE:
 421           return (cmp >= 0);
 422         case LTE:
 423           return (cmp <= 0);
 424         case LT:
 425           return (cmp < 0);
 426
 427         default:
 428           llassert(FALSE);
 429           break;
 430         }
 431     }
 432   else
 433     {
 434       return FALSE;
 435     }
 436       BADEXIT;
 437 }
 438
 439 bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)
 440
 441 {
 442   DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
 443
 444   if (! arithType_canResolve (ar1, ar2) )
 445     return FALSE;
 446
 447   switch (ar1)
 448  {
 449  case GTE:
 450       if (constraintExpr_similar (expr1, expr2) )
 451          return TRUE;
 452  case GT:
 453    if (!  (constraintExpr_canGetValue (expr1) &&
 454            constraintExpr_canGetValue (expr2) ) )
 455      {
 456        DPRINTF( ("Can't Get value"));
 457        return FALSE;
 458      }
 459
 460    if (constraintExpr_compare (expr2, expr1) >= 0)
 461      return TRUE;
 462
 463   return FALSE;
 464  case EQ:
 465    if (constraintExpr_similar (expr1, expr2) )
 466          return TRUE;
 467
 468    return FALSE;
 469  case LTE:
 470    if (constraintExpr_similar (expr1, expr2) )
 471          return TRUE;
 472  case LT:
 473     if (!  (constraintExpr_canGetValue (expr1) &&
 474            constraintExpr_canGetValue (expr2) ) )
 475      {
 476        DPRINTF( ("Can't Get value"));
 477        return FALSE;
 478      }
 479
 480    if (constraintExpr_compare (expr2, expr1) <= 0)
 481      return TRUE;
 482
 483    return FALSE;
 484
 485  default:
 486      llcontbug((message("Unhandled case in switch: %s", arithType_print(ar1) ) ) );
 487  }
 488   BADEXIT;
 489   return FALSE;
 490 }
 491
 492
 493 constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
 494 {
 495   DPRINTF (("Doing replace for lexpr") );
 496   c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
 497   DPRINTF (("Doing replace for expr") );
 498   c->expr = constraintExpr_searchandreplace (c->expr, old, new);
 499   return c;
 500 }
 501
 502 bool constraint_search (constraint c, constraintExpr old)
 503 {
 504   bool ret;
 505   ret = FALSE;
 506
 507   ret  = constraintExpr_search (c->lexpr, old);
 508   ret = ret || constraintExpr_search (c->expr, old);
 509   return ret;
 510 }
 511
 512 //adjust file locs and stuff
 513 constraint constraint_adjust (constraint substitute, constraint old)
 514 {
 515   fileloc loc1, loc2, loc3;
 516
 517   DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
 518                      constraint_print(old))
 519                    ));
 520
 521   loc1 = constraint_getFileloc (old);
 522
 523   loc2 = constraintExpr_getFileloc (substitute->lexpr);
 524
 525   loc3 = constraintExpr_getFileloc (substitute->expr);
 526
 527
 528   // special case of an equality that "contains itself"
 529   if (constraintExpr_search (substitute->expr, substitute->lexpr) )
 530       if (fileloc_closer (loc1, loc3, loc2))
 531       {
 532         constraintExpr temp;
 533         DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
 534                    ));
 535         temp = substitute->lexpr;
 536         substitute->lexpr = substitute->expr;
 537         substitute->expr  = temp;
 538         substitute = constraint_simplify(substitute);
 539       }
 540
 541   return substitute;
 542
 543 }
 544
 545 constraint  inequalitySubstitute  (constraint c, constraintList p)
 546 {
 547   if (c->ar != GTE)
 548     return c;
 549
 550   constraintList_elements (p, el)
 551     {
 552        if ( el->ar == LT)
 553          //      if (!constraint_conflict (c, el) )
 554            {
 555              constraint temp;
 556              temp = constraint_copy(el);
 557
 558              //      temp = constraint_adjust(temp, c);
 559
 560              if (constraintExpr_same (el->lexpr, c->expr) )
 561                {
 562                  DPRINTF((message ("Replacing %s in %s with  %s",
 563                                    constraintExpr_print (c->expr),
 564                                    constraint_print (c),
 565                                    constraintExpr_print (el->expr) )
 566                           ));
 567                  c->expr = constraintExpr_copy (el->expr);
 568                }
 569
 570            }
 571     }
 572   end_constraintList_elements;
 573
 574   c = constraint_simplify(c);
 575   return c;
 576 }
 577
 578 constraint substitute (constraint c, constraintList p)
 579 {
 580   constraintList_elements (p, el)
 581     {
 582        if ( el->ar == EQ)
 583          if (!constraint_conflict (c, el) )
 584
 585            {
 586              constraint temp;
 587              temp = constraint_copy(el);
 588
 589              temp = constraint_adjust(temp, c);
 590
 591              DPRINTF((message ("Substituting %s for %s",
 592                                constraint_print (temp), constraint_print (c)
 593                                ) ) );
 594
 595
 596              c = constraint_searchandreplace (c, temp->lexpr, temp->expr);
 597            }
 598     }
 599   end_constraintList_elements;
 600
 601   c = constraint_simplify(c);
 602   return c;
 603 }
 604
 605
 606 constraint constraint_solve (constraint c)
 607 {
 608   DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
 609   c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
 610   DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
 611
 612   return c;
 613 }
 614
 615 static arithType flipAr (arithType ar)
 616 {
 617   switch (ar)
 618     {
 619     case LT:
 620       return GT;
 621     case LTE:
 622       return GTE;
 623     case EQ:
 624       return EQ;
 625     case GT:
 626       return LT;
 627     case GTE:
 628       return LTE;
 629     default:
 630       llcontbug (("unexpected value: case not handled"));
 631     }
 632   BADEXIT;
 633 }
 634
 635 static constraint  constraint_swapLeftRight (constraint c)
 636 {
 637   constraintExpr temp;
 638   c->ar = flipAr (c->ar);
 639   temp = c->lexpr;
 640   c->lexpr = c->expr;
 641   c->expr = temp;
 642   DPRINTF(("Swaped left and right sides of constraint"));
 643   return c;
 644 }
 645
 646 constraint constraint_simplify (constraint c)
 647 {
 648   c->lexpr = constraintExpr_simplify (c->lexpr);
 649   c->expr  = constraintExpr_simplify (c->expr);
 650
 651   c = constraint_solve (c);
 652
 653   c->lexpr = constraintExpr_simplify (c->lexpr);
 654   c->expr  = constraintExpr_simplify (c->expr);
 655
 656   if (constraintExpr_isLit(c->lexpr) && (!constraintExpr_isLit(c->expr) ) )
 657     {
 658       c = constraint_swapLeftRight(c);
 659       /*I don't think this will be an infinate loop*/
 660       constraint_simplify(c);
 661     }
 662   return c;
 663 }
 664
 665
 666
 667
 668 /* returns true  if fileloc for term1 is closer to file for term2 than term3*/
 669
 670 bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3)
 671 {
 672    if ( fileloc_lessthan (loc1, loc2) )
 673      {
 674        if (fileloc_lessthan (loc2, loc3) )
 675          {
 676            llassert (fileloc_lessthan (loc1, loc3) );
 677            return TRUE;
 678          }
 679        else
 680          {
 681            return FALSE;
 682          }
 683      }
 684
 685    if ( !fileloc_lessthan (loc1, loc2) )
 686      {
 687        if (!fileloc_lessthan (loc2, loc3) )
 688          {
 689            llassert (!fileloc_lessthan (loc1, loc3) );
 690            return TRUE;
 691          }
 692        else
 693          {
 694            return FALSE;
 695          }
 696      }
 697
 698    llassert(FALSE);
 699    return FALSE;
 700 }
 701
 702