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 constraintList reflectChanges (constraintList pre2, constraintList post1);
  24 constraint substitute (constraint c, constraintList p);
  25 constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new);
  26 bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2);
  27 bool satifies (constraint pre, constraint post);
  28 bool resolve (constraint c, constraintList p);
  29 constraintList reflectChangesEnsures (constraintList pre2, constraintList post1);
  30 constraint constraint_simplify (constraint c);
  31
  32 constraintList constraintList_fixConflicts (constraintList list1, constraintList list2);
  33
  34 constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2);
  35
  36 constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2);
  37 constraint  inequalitySubstitute  (constraint c, constraintList p);
  38
  39 /*********************************************/
  40
  41
  42 constraintList constraintList_mergeEnsures (constraintList list1, constraintList list2)
  43 {
  44   constraintList ret;
  45   constraintList temp;
  46   ret = constraintList_new();
  47
  48   ret = reflectChangesEnsures (list1, list2);
  49   ret = constraintList_fixConflicts (ret, list2);
  50   ret = constraintList_subsumeEnsures (ret, list2);
  51   list2 = constraintList_subsumeEnsures (list2, ret);
  52   temp = constraintList_copy(list2);
  53
  54   temp = constraintList_addList (temp, ret);
  55   return temp;
  56   //ret = constraintList_addList (ret, list2);
  57   //return ret;
  58 }
  59
  60
  61 /* constraintList constraintList_resolveRequires (constraintList requires, constraintList ensures) */
  62 /* { */
  63
  64 /*   constraintList ret; */
  65 /*   constraintList temp; */
  66 /*   ret = constraintList_new(); */
  67
  68 /*   ret = reflectChangesEnsures (list1, list2); */
  69 /*   ret = constraintList_fixConflicts (ret, list2); */
  70 /*   ret = constraintList_subsumeEnsures (ret, list2); */
  71 /*   list2 = constraintList_subsumeEnsures (list2, ret); */
  72 /*   temp = constraintList_copy(list2); */
  73
  74 /*   temp = constraintList_addList (temp, ret); */
  75 /*   return temp; */
  76 /*   //ret = constraintList_addList (ret, list2); */
  77 /*   //return ret; */
  78 /* } */
  79
  80
  81 constraintList checkCall (exprNode fcn, exprNodeList arglist)
  82 {
  83   constraintList preconditions;
  84   uentry temp;
  85   DPRINTF ( (message ("Got call that %s ( %s) ",  exprNode_unparse(fcn),   exprNodeList_unparse (arglist ) ) ) );
  86
  87   temp = exprNode_getUentry (fcn);
  88
  89   preconditions = uentry_getFcnPreconditions (temp);
  90
  91   if (preconditions)
  92     {
  93       preconditions = constraintList_copy(preconditions);
  94       preconditions = constraintList_doSRefFixBaseParam (preconditions, arglist);
  95     }
  96   else
  97     {
  98       preconditions = constraintList_new();
  99     }
 100
 101   return preconditions;
 102 }
 103
 104 void mergeResolve (exprNode parent, exprNode child1, exprNode child2)
 105 {
 106   constraintList temp;
 107
 108   DPRINTF( (message ("magically merging constraint into parent:%s for", exprNode_unparse (parent) )));
 109
 110   DPRINTF( (message (" children:  %s and %s", exprNode_unparse (child1), exprNode_unparse(child2) ) ) );
 111
 112   if (exprNode_isError (child1)  || exprNode_isError(child2) )
 113      {
 114        if (exprNode_isError (child1) && !exprNode_isError(child2) )
 115          {
 116            parent->requiresConstraints = constraintList_copy (child2->requiresConstraints);
 117            parent->ensuresConstraints = constraintList_copy (child2->ensuresConstraints);
 118            DPRINTF((message ("Copied child constraints: pre: %s and post: %s",
 119                              constraintList_print( child2->requiresConstraints),
 120                              constraintList_print (child2->ensuresConstraints)
 121                              )
 122                     ));
 123            return;
 124          }
 125        else
 126          {
 127            llassert(exprNode_isError(child2) );
 128            parent->requiresConstraints = constraintList_new();
 129            parent->ensuresConstraints = constraintList_new();
 130            return;
 131          }
 132      }
 133
 134    llassert(!exprNode_isError (child1)  && ! exprNode_isError(child2) );
 135
 136   DPRINTF( (message ("Child constraints are %s %s and %s %s",
 137                      constraintList_print (child1->requiresConstraints),
 138                      constraintList_print (child1->ensuresConstraints),
 139                      constraintList_print (child2->requiresConstraints),
 140                      constraintList_print (child2->ensuresConstraints)
 141                      ) ) );
 142
 143   parent->requiresConstraints = constraintList_new();
 144   parent->ensuresConstraints = constraintList_new();
 145
 146   parent->requiresConstraints = constraintList_copy (child1->requiresConstraints);
 147
 148   temp = reflectChanges (child2->requiresConstraints, child1->ensuresConstraints);
 149   parent->requiresConstraints = constraintList_addList (parent->requiresConstraints, temp);
 150
 151   parent->ensuresConstraints = constraintList_mergeEnsures(child1->ensuresConstraints,
 152                                                            child2->ensuresConstraints);
 153
 154   DPRINTF( (message ("Parent constraints are %s and %s ",
 155                      constraintList_print (parent->requiresConstraints),
 156                      constraintList_print (parent->ensuresConstraints)
 157                      ) ) );
 158
 159 }
 160
 161
 162
 163
 164 constraintList constraintList_subsumeEnsures (constraintList list1, constraintList list2)
 165 {
 166   constraintList ret;
 167   ret = constraintList_new();
 168   constraintList_elements (list1, el)
 169     {
 170
 171       DPRINTF ((message ("Examining %s", constraint_print (el) ) ) );
 172       if (!resolve (el, list2) )
 173         {
 174             ret = constraintList_add (ret, el);
 175         }
 176       else
 177         {
 178           DPRINTF ( (message ("Subsuming %s", constraint_print (el) ) ) );
 179         }
 180     } end_constraintList_elements;
 181
 182     return ret;
 183 }
 184
 185
 186 constraintList reflectChanges (constraintList pre2, constraintList post1)
 187 {
 188
 189   constraintList ret;
 190   constraint temp;
 191   ret = constraintList_new();
 192   constraintList_elements (pre2, el)
 193     {
 194       if (!resolve (el, post1) )
 195         {
 196           temp = substitute (el, post1);
 197           if (!resolve (temp, post1) )
 198             {
 199               // try inequality substitution
 200               constraint temp2;
 201
 202               // the inequality substitution may cause us to lose information
 203               //so we don't want to store the result but we do it anyway
 204               temp2 = constraint_copy (temp);
 205               temp2 = inequalitySubstitute (temp, post1);
 206               if (!resolve (temp2, post1) )
 207                   ret = constraintList_add (ret, temp2);
 208             }
 209         }
 210     } end_constraintList_elements;
 211
 212     return ret;
 213 }
 214
 215
 216
 217 constraintList reflectChangesEnsures (constraintList pre2, constraintList post1)
 218 {
 219   constraintList ret;
 220   constraint temp;
 221   ret = constraintList_new();
 222   constraintList_elements (pre2, el)
 223     {
 224       if (!resolve (el, post1) )
 225         {
 226           temp = substitute (el, post1);
 227           llassert (temp != NULL);
 228
 229           if (!resolve (temp, post1) )
 230             ret = constraintList_add (ret, temp);
 231         }
 232       else
 233         {
 234           DPRINTF ( (message ("Resolved away %s ", constraint_print(el) ) ) );
 235         }
 236     } end_constraintList_elements;
 237
 238     return ret;
 239 }
 240
 241
 242 bool constraint_conflict (constraint c1, constraint c2)
 243 {
 244
 245   if (constraintExpr_similar(c1->lexpr, c2->lexpr) )
 246     {
 247       if (c1->ar == EQ)
 248         if (c1->ar == c2->ar)
 249           {
 250             DPRINTF ( (message ("%s conflicts with %s ", constraint_print (c1), constraint_print(c2) ) ) );
 251             return TRUE;
 252           }
 253     }
 254
 255   DPRINTF ( (message ("%s doesn't conflict with %s ", constraint_print (c1), constraint_print(c2) ) ) );
 256
 257   return FALSE;
 258
 259 }
 260
 261 void constraint_fixConflict (constraint good, constraint conflicting)
 262 {
 263   constraint temp;
 264   if (conflicting->ar ==EQ )
 265     {
 266       good->expr = constraintExpr_searchandreplace (good->expr, conflicting->lexpr, conflicting->expr);
 267       temp = constraint_simplify (good);
 268       constraint_overWrite (good, temp);
 269     }
 270
 271
 272 }
 273
 274 bool conflict (constraint c, constraintList list)
 275 {
 276
 277    constraintList_elements (list, el)
 278     {
 279       if ( constraint_conflict(el, c) )
 280         {
 281           constraint_fixConflict (el, c);
 282           return TRUE;
 283         }
 284     } end_constraintList_elements;
 285
 286     return FALSE;
 287
 288
 289 }
 290
 291 //check if constraint in list1 and conflict with constraints in List2.  If so we
 292 //remove form list1 and (optionally) change list2.
 293 constraintList constraintList_fixConflicts (constraintList list1, constraintList list2)
 294 {
 295   constraintList ret;
 296   ret = constraintList_new();
 297   constraintList_elements (list1, el)
 298     {
 299       if (! conflict (el, list2) )
 300         {
 301             ret = constraintList_add (ret, el);
 302         }
 303     } end_constraintList_elements;
 304
 305     return ret;
 306
 307
 308 }
 309
 310 bool resolve (constraint c, constraintList p)
 311 {
 312   constraintList_elements (p, el)
 313     {
 314       if ( satifies (c, el) )
 315         {
 316           DPRINTF ( (message ("\n%s Satifies %s\n ", constraint_print(el), constraint_print(c) ) ) );
 317           return TRUE;
 318         }
 319     }
 320   end_constraintList_elements;
 321   DPRINTF ( (message ("no constraints satify %s", constraint_print(c) ) ));
 322   return FALSE;
 323 }
 324
 325
 326 /*returns true if cosntraint post satifies cosntriant pre */
 327 bool satifies (constraint pre, constraint post)
 328 {
 329   if (!constraintExpr_similar (pre->lexpr, post->lexpr) )
 330     {
 331       return FALSE;
 332     }
 333   if (post->expr == NULL)
 334     {
 335       llassert(FALSE);
 336       return FALSE;
 337     }
 338
 339   return rangeCheck (pre->ar, pre->expr, post->ar, post->expr);
 340 }
 341
 342 bool arithType_canResolve (arithType ar1, arithType ar2)
 343 {
 344   switch (ar1)
 345     {
 346     case GTE:
 347     case GT:
 348       if ( (ar2 == GT) || (ar2 == GTE) || (ar2 == EQ) )
 349         {
 350           return TRUE;
 351         }
 352       break;
 353
 354     case EQ:
 355       if (ar2 == EQ)
 356         return TRUE;
 357       break;
 358
 359     case LT:
 360     case LTE:
 361       //      llassert(FALSE);
 362       if ( (ar2 == LT) || (ar2 == LTE) || (ar2 == EQ) )
 363         return TRUE;
 364     }
 365   return FALSE;
 366 }
 367
 368 bool rangeCheck (arithType ar1, constraintExpr expr1, arithType ar2, constraintExpr expr2)
 369
 370 {
 371   DPRINTF ((message ("Doing Range CHECK %s and %s", constraintExpr_unparse(expr1), constraintExpr_unparse(expr2) ) ));
 372
 373   if (! arithType_canResolve (ar1, ar2) )
 374     return FALSE;
 375
 376   switch (ar1)
 377  {
 378  case GTE:
 379  case GT:
 380    if (!  (constraintExpr_canGetValue (expr1) &&
 381            constraintExpr_canGetValue (expr2) ) )
 382      {
 383        DPRINTF( ("Can't Get value"));
 384        return FALSE;
 385      }
 386
 387    if (constraintExpr_compare (expr2, expr1) >= 0)
 388      return TRUE;
 389
 390   return FALSE;
 391  case EQ:
 392    if (constraintExpr_similar (expr1, expr2) )
 393          return TRUE;
 394
 395    return FALSE;
 396
 397  default:
 398    DPRINTF(("case not handled"));
 399  }
 400   return FALSE;
 401 }
 402
 403
 404 constraint constraint_searchandreplace (constraint c, constraintExpr old, constraintExpr new)
 405 {
 406   DPRINTF (("Doing replace for lexpr") );
 407   c->lexpr = constraintExpr_searchandreplace (c->lexpr, old, new);
 408   DPRINTF (("Doing replace for expr") );
 409   c->expr = constraintExpr_searchandreplace (c->expr, old, new);
 410   return c;
 411 }
 412
 413 bool constraint_search (constraint c, constraintExpr old)
 414 {
 415   bool ret;
 416   ret = FALSE;
 417
 418   ret  = constraintExpr_search (c->lexpr, old);
 419   ret = ret || constraintExpr_search (c->expr, old);
 420   return ret;
 421 }
 422
 423 //adjust file locs and stuff
 424 constraint constraint_adjust (constraint substitute, constraint old)
 425 {
 426   fileloc loc1, loc2, loc3;
 427
 428   DPRINTF ( (message("Start adjust on %s and %s", constraint_print(substitute),
 429                      constraint_print(old))
 430                    ));
 431
 432   loc1 = constraint_getFileloc (old);
 433
 434   loc2 = constraintExpr_getFileloc (substitute->lexpr);
 435
 436   loc3 = constraintExpr_getFileloc (substitute->expr);
 437
 438
 439   // special case of an equality that "contains itself"
 440   if (constraintExpr_search (substitute->expr, substitute->lexpr) )
 441       if (fileloc_closer (loc1, loc3, loc2))
 442       {
 443         constraintExpr temp;
 444         DPRINTF ( (message("Doing adjust on %s", constraint_print(substitute) )
 445                    ));
 446         temp = substitute->lexpr;
 447         substitute->lexpr = substitute->expr;
 448         substitute->expr  = temp;
 449         substitute = constraint_simplify(substitute);
 450       }
 451
 452   return substitute;
 453
 454 }
 455
 456 constraint  inequalitySubstitute  (constraint c, constraintList p)
 457 {
 458   if (c->ar != GTE)
 459     return c;
 460
 461   constraintList_elements (p, el)
 462     {
 463        if ( el->ar == LT)
 464          //      if (!constraint_conflict (c, el) )
 465            {
 466              constraint temp;
 467              temp = constraint_copy(el);
 468
 469              //      temp = constraint_adjust(temp, c);
 470
 471              if (constraintExpr_same (el->lexpr, c->expr) )
 472                {
 473                  DPRINTF((message ("Replacing %s in %s with  %s",
 474                                    constraintExpr_print (c->expr),
 475                                    constraint_print (c),
 476                                    constraintExpr_print (el->expr) )
 477                           ));
 478                  c->expr = constraintExpr_copy (el->expr);
 479                }
 480
 481            }
 482     }
 483   end_constraintList_elements;
 484
 485   c = constraint_simplify(c);
 486   return c;
 487 }
 488
 489 constraint substitute (constraint c, constraintList p)
 490 {
 491   constraintList_elements (p, el)
 492     {
 493        if ( el->ar == EQ)
 494          if (!constraint_conflict (c, el) )
 495
 496            {
 497              constraint temp;
 498              temp = constraint_copy(el);
 499
 500              temp = constraint_adjust(temp, c);
 501
 502              DPRINTF((message ("Substituting %s for %s",
 503                                constraint_print (temp), constraint_print (c)
 504                                ) ) );
 505
 506
 507              c = constraint_searchandreplace (c, temp->lexpr, temp->expr);
 508            }
 509     }
 510   end_constraintList_elements;
 511
 512   c = constraint_simplify(c);
 513   return c;
 514 }
 515
 516
 517 constraint constraint_solve (constraint c)
 518 {
 519   DPRINTF( (message ("Solving %s\n", constraint_print(c) ) ) );
 520   c->expr = constraintExpr_solveBinaryExpr (c->lexpr, c->expr);
 521   DPRINTF( (message ("Solved and got %s\n", constraint_print(c) ) ) );
 522
 523   return c;
 524 }
 525
 526
 527 constraint constraint_simplify (constraint c)
 528 {
 529   c->lexpr = constraintExpr_simplify (c->lexpr);
 530   c->expr  = constraintExpr_simplify (c->expr);
 531
 532   c = constraint_solve (c);
 533
 534   c->lexpr = constraintExpr_simplify (c->lexpr);
 535   c->expr  = constraintExpr_simplify (c->expr);
 536
 537   return c;
 538 }
 539
 540
 541
 542
 543 /* returns true  if fileloc for term1 is closer to file for term2 than term3*/
 544
 545 bool fileloc_closer (fileloc  loc1, fileloc  loc2, fileloc  loc3)
 546 {
 547    if ( fileloc_lessthan (loc1, loc2) )
 548      {
 549        if (fileloc_lessthan (loc2, loc3) )
 550          {
 551            llassert (fileloc_lessthan (loc1, loc3) );
 552            return TRUE;
 553          }
 554        else
 555          {
 556            return FALSE;
 557          }
 558      }
 559
 560    if ( !fileloc_lessthan (loc1, loc2) )
 561      {
 562        if (!fileloc_lessthan (loc2, loc3) )
 563          {
 564            llassert (!fileloc_lessthan (loc1, loc3) );
 565            return TRUE;
 566          }
 567        else
 568          {
 569            return FALSE;
 570          }
 571      }
 572
 573    llassert(FALSE);
 574    return FALSE;
 575 }
 576
 577