src/loopHeuristics.c

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