src/forjunk.c

   1 /*
   2 ** forjunk.c
   3 */
   4
   5 //#define DEBUGPRINT 1
   6
   7 # include <ctype.h> /* for isdigit */
   8 # include "lclintMacros.nf"
   9 # include "basic.h"
  10 # include "cgrammar.h"
  11 # include "cgrammar_tokens.h"
  12
  13 # include "exprChecks.h"
  14 # include "exprNodeSList.h"
  15
  16 # include "exprDataQuite.i"
  17
  18 /*@access constraint, exprNode @*/
  19
  20 /*@access constraintExpr @*/
  21
  22 static bool isInc (/*@observer@*/ constraintExpr c) /*@*/
  23 {
  24
  25   llassert(constraintExpr_isDefined(c) );
  26  if (c->kind == binaryexpr )
  27     {
  28       constraintExprBinaryOpKind binOP;
  29       constraintExpr t1, t2;
  30       t1 = constraintExprData_binaryExprGetExpr1 (c->data);
  31       t2 = constraintExprData_binaryExprGetExpr2 (c->data);
  32
  33       binOP = constraintExprData_binaryExprGetOp (c->data);
  34       if (binOP == PLUS)
  35         if (constraintExpr_isLit (t2) && constraintExpr_getValue (t2) == 1 )
  36           {
  37             return TRUE;
  38           }
  39     }
  40
  41  return FALSE;
  42 }
  43
  44
  45
  46 // look for constraints like cexrp = cexrp + 1
  47 static bool incVar (/*@notnull@*/ constraint c) /*@*/
  48 {
  49   constraintExpr t1;
  50   if (c->ar != EQ)
  51     {
  52       return FALSE;
  53     }
  54   if (! isInc (c->expr ) )
  55     return FALSE;
  56
  57   llassert (constraintExpr_isDefined(c->expr) );
  58   llassert (c->expr->kind == binaryexpr);
  59
  60   t1 = constraintExprData_binaryExprGetExpr1 (c->expr->data);
  61   if (constraintExpr_similar (c->lexpr, t1) )
  62     return TRUE;
  63
  64   return FALSE;
  65 }
  66 /*@noaccess constraintExpr @*/
  67
  68
  69 static bool increments (/*@observer@*/ constraint c,
  70                         /*@observer@*/ constraintExpr var)
  71 {
  72   llassert(constraint_isDefined(c) );
  73
  74   if (constraint_isUndefined(c) )
  75     {
  76       return FALSE;
  77     }
  78
  79   llassert (incVar (c));
  80   if (constraintExpr_similar (c->lexpr, var) )
  81     return TRUE;
  82   else
  83     return FALSE;
  84 }
  85
  86 static bool canGetForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
  87 {
  88
  89   exprNode init, test, inc, t1, t2;
  90   lltok tok;
  91
  92   llassert(exprNode_isDefined (forPred) );
  93   llassert(exprNode_isDefined (forBody) );
  94
  95   init  =  exprData_getTripleInit (forPred->edata);
  96   test  =   exprData_getTripleTest (forPred->edata);
  97   inc   =   exprData_getTripleInc (forPred->edata);
  98
  99   llassert(exprNode_isDefined(test) );
 100
 101   if (exprNode_isUndefined(test) )
 102     {
 103       return FALSE;
 104     }
 105
 106   llassert(exprNode_isDefined(inc) );
 107
 108   if (exprNode_isUndefined(inc) )
 109     {
 110       return FALSE;
 111     }
 112
 113   if (test->kind != XPR_PREOP)
 114     return FALSE;
 115
 116   tok = (exprData_getUopTok (test->edata));
 117   if (!lltok_isMult (tok) )
 118     {
 119       return FALSE;
 120     }
 121
 122   //should check preop too
 123   if (inc->kind != XPR_POSTOP)
 124     {
 125       return FALSE;
 126     }
 127
 128   tok = (exprData_getUopTok (inc->edata));
 129   if (lltok_isInc_Op (tok) )
 130       {
 131         t1 = exprData_getUopNode (test->edata);
 132         t2 = exprData_getUopNode (inc->edata);
 133         llassert(exprNode_isDefined(t2) && exprNode_isDefined(t2)  );
 134
 135         if (exprNode_isUndefined(t1) || exprNode_isUndefined(t2)  )
 136           {
 137             return FALSE;
 138           }
 139
 140         if (sRef_sameName (t1->sref, t2->sref) )
 141           {
 142             return TRUE;
 143           }
 144       }
 145   return FALSE;
 146 }
 147
 148 static /*@only@*/ constraintList getLessThanConstraints (/*@observer@*/ constraintList c)
 149 {
 150   constraintList ret;
 151
 152   ret = constraintList_makeNew();
 153   constraintList_elements (c, el)
 154     {
 155       llassert(constraint_isDefined(el));
 156       if ( constraint_isUndefined(el)  )
 157         continue;
 158
 159       if (el->ar == LT || el->ar == LTE)
 160         {
 161           constraint temp;
 162           temp = constraint_copy(el);
 163
 164           ret = constraintList_add (ret, temp);
 165         }
 166     }
 167   end_constraintList_elements;
 168
 169   return ret;
 170 }
 171
 172 static /*@only@*/ constraintList getIncConstraints (/*@observer@*/ constraintList c)
 173 {
 174   constraintList ret;
 175
 176   ret = constraintList_makeNew();
 177   constraintList_elements (c, el)
 178     {
 179       llassert (constraint_isDefined (el));
 180
 181       if (incVar (el) )
 182         {
 183           constraint temp;
 184           temp = constraint_copy(el);
 185           ret = constraintList_add (ret, temp);
 186         }
 187     }
 188   end_constraintList_elements;
 189
 190   return ret;
 191 }
 192
 193 static /*@only@*/ constraintExpr getForTimes (/*@notnull@*/ exprNode forPred, /*@notnull@*/ exprNode forBody)
 194 {
 195
 196   exprNode init, test, inc, t1, t2;
 197   constraintList ltCon;
 198   constraintList incCon;
 199   constraintExpr ret;
 200
 201   lltok tok;
 202
 203   init  =  exprData_getTripleInit (forPred->edata);
 204   test  =  exprData_getTripleTest (forPred->edata);
 205   inc   =  exprData_getTripleInc (forPred->edata);
 206
 207   llassert(exprNode_isDefined(test) );
 208   llassert(exprNode_isDefined(inc) );
 209
 210   ltCon =  getLessThanConstraints (test->trueEnsuresConstraints);
 211   incCon = getIncConstraints (inc->ensuresConstraints);
 212
 213   DPRINTF(( message ("getForTimes: ltCon: %s from %s", constraintList_print(ltCon), constraintList_print(test->trueEnsuresConstraints) ) ));
 214
 215   DPRINTF(( message ("getForTimes: incCon: %s from %s", constraintList_print(incCon), constraintList_print(inc->ensuresConstraints) ) ));
 216
 217   constraintList_elements (ltCon, el)
 218     {
 219       constraintList_elements(incCon, el2)
 220       {
 221         if ( increments(el2, el->lexpr) )
 222           {
 223             DPRINTF(( message ("getForTimes: %s increments %s", constraint_print(el2), constraint_print(el) ) ));
 224             ret =  constraintExpr_copy (el->expr);
 225             constraintList_free(ltCon);
 226             constraintList_free(incCon);
 227             return ret;
 228
 229           }
 230         else
 231           DPRINTF(( message ("getForTimes: %s doesn't increment %s", constraint_print(el2), constraint_print(el) )   ));
 232       }
 233       end_constraintList_elements;
 234     }
 235
 236   end_constraintList_elements;
 237
 238   constraintList_free(ltCon);
 239   constraintList_free(incCon);
 240
 241   DPRINTF (( message ("getForTimes: %s  %s resorting to ugly hack", exprNode_unparse(forPred), exprNode_unparse(forBody) ) ));
 242   if (! canGetForTimes (forPred, forBody) )
 243     {
 244       return NULL;
 245     }
 246
 247
 248   if (test->kind != XPR_PREOP)
 249     llassert (FALSE);
 250
 251   tok = (exprData_getUopTok (test->edata));
 252   if (!lltok_isMult (tok) )
 253     {
 254       llassert ( FALSE );
 255     }
 256
 257   //should check preop too
 258   if (inc->kind != XPR_POSTOP)
 259     {
 260       llassert (FALSE );
 261     }
 262
 263   tok = (exprData_getUopTok (inc->edata));
 264   if (lltok_isInc_Op (tok) )
 265       {
 266         t1 = exprData_getUopNode (test->edata);
 267         t2 = exprData_getUopNode (inc->edata);
 268         if (sRef_sameName (t1->sref, t2->sref) )
 269           {
 270             return (constraintExpr_makeMaxSetExpr (t1) );
 271           }
 272       }
 273   llassert( FALSE);
 274   BADEXIT;
 275 }
 276
 277 /*@access constraintExpr @*/
 278
 279 static /*@only@*/ constraintExpr constraintExpr_searchAndAdd (/*@only@*/ constraintExpr c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
 280 {
 281   constraintExprKind kind;
 282   constraintExpr temp;
 283
 284   DPRINTF(( message ("Doing constraintExpr_searchAndAdd  %s %s %s ",
 285                      constraintExpr_unparse(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
 286
 287   if ( constraintExpr_similar (c, find) )
 288     {
 289
 290       constraintExpr newExpr;
 291
 292       cstring cPrint;
 293
 294       cPrint = constraintExpr_unparse(c);
 295
 296
 297       newExpr = constraintExpr_makeAddExpr (c, constraintExpr_copy(add) );
 298
 299       DPRINTF((message ("Replacing %q with %q",
 300                         cPrint, constraintExpr_unparse(newExpr)
 301                         )));
 302       return newExpr;
 303     }
 304
 305   kind = c->kind;
 306
 307   switch (kind)
 308     {
 309     case term:
 310       break;
 311     case unaryExpr:
 312       temp = constraintExprData_unaryExprGetExpr (c->data);
 313       temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
 314       c->data = constraintExprData_unaryExprSetExpr (c->data, temp);
 315       break;
 316     case binaryexpr:
 317
 318       temp = constraintExprData_binaryExprGetExpr1 (c->data);
 319       temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
 320       c->data = constraintExprData_binaryExprSetExpr1 (c->data, temp);
 321
 322       temp = constraintExprData_binaryExprGetExpr2 (c->data);
 323       temp = constraintExpr_searchAndAdd (constraintExpr_copy(temp), find, add);
 324       c->data = constraintExprData_binaryExprSetExpr2 (c->data, temp);
 325       break;
 326     default:
 327       llassert(FALSE);
 328     }
 329   return c;
 330
 331 }
 332
 333 /*@noaccess constraintExpr @*/
 334
 335 static constraint  constraint_searchAndAdd (/*@returned@*/ constraint c, /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
 336 {
 337
 338   llassert (constraint_search (c, find)  );
 339   DPRINTF(( message ("Doing constraint_searchAndAdd  %s %s %s ",
 340                      constraint_print(c), constraintExpr_unparse(find), constraintExpr_unparse(add) ) ) );
 341
 342   c->lexpr = constraintExpr_searchAndAdd (c->lexpr, find, add);
 343   c->expr =  constraintExpr_searchAndAdd (c->expr, find, add);
 344
 345    c = constraint_simplify (c);
 346    c = constraint_simplify (c);
 347
 348   return c;
 349
 350 }
 351
 352  static constraintList constraintList_searchAndAdd (/*@returned@*/ constraintList list,
 353                                                    /*@observer@*/ constraintExpr find, /*@observer@*/ constraintExpr add)
 354 {
 355   constraintList newConstraints;
 356   constraintList ret;
 357
 358   newConstraints = constraintList_makeNew();
 359
 360   constraintList_elements (list, el)
 361     {
 362       if (constraint_search (el, find) )
 363         {
 364           constraint newExpr;
 365           newExpr = constraint_copy (el);
 366
 367           newExpr = constraint_searchAndAdd (newExpr, find, add);
 368                   DPRINTF (( (message ("Adding constraint %s ", constraint_print (newExpr)) )  ));
 369           newConstraints = constraintList_add (newConstraints, newExpr);
 370         }
 371
 372     }
 373   end_constraintList_elements;
 374
 375   ret =  constraintList_addListFree (list, newConstraints);
 376   return ret;
 377 }
 378
 379 static void doAdjust(/*@unused@*/ exprNode e, /*@unused@*/ exprNode forPred, /*@observer@*/ exprNode forBody, /*@observer@*/ constraintExpr iterations)
 380 {
 381
 382   constraintList_elements (forBody->ensuresConstraints, el)
 383     {
 384       // look for var = var + 1
 385       if (incVar(el) )
 386         {
 387           DPRINTF((message ("Found inc variable constraint : %s", constraint_print (el) )  ));
 388           forBody->requiresConstraints = constraintList_searchAndAdd(forBody->requiresConstraints, el->lexpr, iterations);
 389         }
 390     }
 391   end_constraintList_elements;
 392 }
 393
 394 void exprNode_forLoopHeuristics( exprNode e, exprNode forPred, exprNode forBody)
 395 {
 396   exprNode init, test, inc;
 397
 398   constraintExpr iterations;
 399
 400   init  =  exprData_getTripleInit (forPred->edata);
 401   test =   exprData_getTripleTest (forPred->edata);
 402   inc  =   exprData_getTripleInc (forPred->edata);
 403
 404   if (exprNode_isError (test) || exprNode_isError (inc) )
 405     return;
 406
 407   iterations = getForTimes (forPred, forBody );
 408
 409   if (constraintExpr_isDefined (iterations) )
 410     {
 411       doAdjust ( e, forPred, forBody, iterations);
 412       constraintExpr_free(iterations);
 413     }
 414 }
 415
 416
 417 /*    else */
 418 /*      { */
 419 /*        DPRINTF (("Can't get for time ")); */
 420 /*      } */
 421
 422 /*    if (exprNode_isError(init) ) */
 423 /*      { */
 424 /*        return; */
 425 /*      } */
 426
 427 /*    if (init->kind == XPR_ASSIGN) */
 428 /*      { */
 429 /*        t1 = exprData_getOpA (init->edata); */
 430 /*        t2 = exprData_getOpB (init->edata); */
 431
 432 /*        if (! (t1->kind == XPR_VAR) ) */
 433 /*      return; */
 434 /*      } */
 435 /*    else */
 436 /*      return; */
 437
 438 /*    if (test->kind == XPR_FETCH) */
 439 /*      { */
 440 /*        t3 = exprData_getPairA (test->edata); */
 441 /*        t4 = exprData_getPairB (test->edata); */
 442
 443 /*        if (sRef_sameName(t1->sref, t4->sref) ) */
 444 /*      { */
 445 /*        DPRINTF((message ("Found a for loop matching heuristic:%s", exprNode_unparse (forPred) ) )); */
 446 /*        con = constraint_makeEnsureLteMaxRead(t1, t3); */
 447 /*        forPred->ensuresConstraints = constraintList_add(forPred->ensuresConstraints, con);      */
 448 /*      } */
 449 /*        else */
 450 /*      { */
 451 /*        DPRINTF((message ("Didn't Find a for loop matching heuristic:%s %s and %s differ", exprNode_unparse (forPred), exprNode_unparse(t1), exprNode_unparse(t3) ) )); */
 452 /*      } */
 453 /*        return; */
 454 /*      } */