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