src/loopHeuristics.c

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