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