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