src/constraintResolve.c

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