src/constraintTerm.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: splint@cs.virginia.edu
  21 ** To report a bug: splint-bug@cs.virginia.edu
  22 ** For more information: http://www.splint.org
  23 */
  24
  25 /*
  26 ** constraintTerm.c
  27 */
  28
  29 /* #define DEBUGPRINT 1 */
  30
  31 # include <ctype.h> /* for isdigit */
  32 # include "splintMacros.nf"
  33 # include "basic.h"
  34 # include "cgrammar.h"
  35 # include "cgrammar_tokens.h"
  36
  37 # include "exprChecks.h"
  38 # include "exprNodeSList.h"
  39
  40 /*@-czechfcns@*/
  41
  42 /*@access exprNode @*/
  43
  44 bool constraintTerm_isDefined (constraintTerm t)
  45 {
  46   return t != NULL;
  47 }
  48
  49 void constraintTerm_free (/*@only@*/ constraintTerm term)
  50 {
  51   llassert (constraintTerm_isDefined (term));
  52
  53   fileloc_free (term->loc);
  54
  55   switch (term->kind)
  56     {
  57     case EXPRNODE:
  58       /* we don't free an exprNode*/
  59       break;
  60     case SREF:
  61       /* sref */
  62       sRef_free (term->value.sref);
  63       break;
  64     case INTLITERAL:
  65       /* don't free an int */
  66       break;
  67     case  ERRORBADCONSTRAINTTERMTYPE:
  68     default:
  69       /* type was set incorrectly */
  70       llcontbug (message("constraintTerm_free type was set incorrectly"));
  71     }
  72
  73   term->kind =  ERRORBADCONSTRAINTTERMTYPE;
  74   free (term);
  75 }
  76
  77 /*@only@*/ static/*@out@*/ constraintTerm new_constraintTermExpr (void)
  78 {
  79   constraintTerm ret;
  80   ret = dmalloc (sizeof (* ret ) );
  81   ret->value.intlit = 0;
  82   return ret;
  83 }
  84
  85
  86 bool constraintTerm_isIntLiteral (constraintTerm term)
  87 {
  88   llassert(term != NULL);
  89
  90   if (term->kind == INTLITERAL)
  91     return TRUE;
  92
  93   return FALSE;
  94 }
  95
  96
  97 bool constraintTerm_isInitBlock (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
  98 {
  99   llassert (c != NULL);
 100   if (c->kind == EXPRNODE)
 101     {
 102
 103       if (exprNode_isInitBlock(c->value.expr) )
 104         {
 105           return TRUE;
 106         }
 107     }
 108   return FALSE;
 109 }
 110
 111
 112 bool constraintTerm_isExprNode (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
 113 {
 114   llassert (c != NULL);
 115   if (c->kind == EXPRNODE)
 116     {
 117       return TRUE;
 118     }
 119   return FALSE;
 120 }
 121
 122
 123 int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
 124 {
 125
 126   exprNodeList  list;
 127   int ret;
 128   llassert (c != NULL);
 129   llassert (constraintTerm_isInitBlock (c) );
 130   llassert (c->kind == EXPRNODE);
 131
 132   llassert(exprNode_isDefined(c->value.expr) );
 133
 134   if (exprNode_isUndefined(c->value.expr) )
 135     {
 136       return 1;
 137     }
 138
 139   if (c->value.expr->edata == exprData_undefined)
 140     {
 141       return 1;
 142     }
 143   list = exprData_getArgs(c->value.expr->edata);
 144
 145   ret = exprNodeList_size(list);
 146
 147   return ret;
 148 }
 149
 150
 151
 152 bool constraintTerm_isStringLiteral (constraintTerm c) /*@*/
 153 {
 154   llassert (c != NULL);
 155   if (c->kind == EXPRNODE)
 156     {
 157       if (exprNode_knownStringValue(c->value.expr) )
 158         {
 159           return TRUE;
 160         }
 161     }
 162   return FALSE;
 163 }
 164
 165
 166
 167 cstring constraintTerm_getStringLiteral (constraintTerm c)
 168 {
 169   llassert (c != NULL);
 170   llassert (constraintTerm_isStringLiteral (c) );
 171   llassert (c->kind == EXPRNODE);
 172
 173   return (cstring_copy ( multiVal_forceString (exprNode_getValue (c->value.expr) ) ) );
 174 }
 175
 176 constraintTerm constraintTerm_simplify (/*@returned@*/ constraintTerm term) /*@modifies term@*/
 177 {
 178   if (term->kind == EXPRNODE)
 179     {
 180       if ( exprNode_knownIntValue (term->value.expr ) )
 181         {
 182           long int temp;
 183
 184           temp  = exprNode_getLongValue (term->value.expr);
 185           term->value.intlit = (int)temp;
 186           term->kind = INTLITERAL;
 187         }
 188     }
 189   return term;
 190 }
 191
 192 fileloc constraintTerm_getFileloc (constraintTerm t)
 193 {
 194   llassert (constraintTerm_isDefined (t));
 195   return (fileloc_copy (t->loc) );
 196 }
 197
 198 constraintTermType constraintTerm_getKind (constraintTerm t)
 199 {
 200   llassert (constraintTerm_isDefined(t) );
 201
 202   return (t->kind);
 203 }
 204
 205 /*@exposed@*/ sRef constraintTerm_getSRef (constraintTerm t)
 206 {
 207   llassert (constraintTerm_isDefined(t) );
 208   llassert (t->kind == SREF);
 209
 210   return (t->value.sref);
 211 }
 212
 213 /*@only@*/ constraintTerm constraintTerm_makeExprNode (/*@dependent@*/  exprNode e)
 214 {
 215   constraintTerm ret = new_constraintTermExpr();
 216   ret->loc =  fileloc_copy(exprNode_getfileloc(e));
 217   ret->value.expr = e;
 218   ret->kind = EXPRNODE;
 219   ret = constraintTerm_simplify(ret);
 220   return ret;
 221 }
 222
 223 /*@only@*/ constraintTerm constraintTerm_makesRef  (/*@temp@*/ /*@observer@*/ sRef s)
 224 {
 225   constraintTerm ret = new_constraintTermExpr();
 226   ret->loc =  fileloc_undefined;
 227   ret->value.sref = sRef_saveCopy(s);
 228   ret->kind = SREF;
 229   ret = constraintTerm_simplify(ret);
 230   return ret;
 231 }
 232
 233
 234
 235 constraintTerm constraintTerm_copy (constraintTerm term)
 236 {
 237   constraintTerm ret;
 238   ret = new_constraintTermExpr();
 239   ret->loc = fileloc_copy (term->loc);
 240
 241   switch (term->kind)
 242     {
 243     case EXPRNODE:
 244       ret->value.expr = term->value.expr;
 245       break;
 246     case INTLITERAL:
 247       ret->value.intlit = term->value.intlit;
 248       break;
 249
 250     case SREF:
 251       ret->value.sref = sRef_saveCopy(term->value.sref);
 252       break;
 253     default:
 254       BADEXIT;
 255     }
 256   ret->kind = term->kind;
 257   return ret;
 258 }
 259
 260 constraintTerm constraintTerm_setFileloc (/*@returned@*/ constraintTerm term, fileloc loc)
 261 {
 262   llassert(term != NULL);
 263
 264   if ( fileloc_isDefined(  term->loc ) )
 265     fileloc_free(term->loc);
 266
 267   term->loc = fileloc_copy(loc);
 268   return term;
 269 }
 270
 271
 272 static cstring constraintTerm_getName (constraintTerm term)
 273 {
 274   cstring s;
 275   s = cstring_undefined;
 276
 277   llassert (term != NULL);
 278
 279   switch (term->kind)
 280     {
 281     case EXPRNODE:
 282       /*@i334*/  /*wtf*/
 283       s = message ("%s", exprNode_unparse (term->value.expr) );
 284       break;
 285     case INTLITERAL:
 286       s = message (" %d ", (int) term->value.intlit);
 287       break;
 288
 289     case SREF:
 290       s = message ("%q", sRef_unparse (term->value.sref) );
 291
 292       break;
 293     default:
 294       BADEXIT;
 295       /*@notreached@*/
 296       break;
 297     }
 298
 299   return s;
 300 }
 301
 302 constraintTerm
 303 constraintTerm_doSRefFixBaseParam (/*@returned@*/constraintTerm term, exprNodeList arglist) /*@modifies term@*/
 304 {
 305   llassert (term != NULL);
 306
 307   switch (term->kind)
 308     {
 309     case EXPRNODE:
 310       /*@i334*/  /*wtf*/
 311       break;
 312     case INTLITERAL:
 313       break;
 314
 315     case SREF:
 316       term->value.sref = sRef_fixBaseParam (term->value.sref, arglist);
 317       break;
 318     default:
 319       BADEXIT;
 320     }
 321   return term;
 322
 323 }
 324
 325 cstring constraintTerm_print (constraintTerm term)  /*@*/
 326 {
 327   cstring s;
 328   s = cstring_undefined;
 329
 330   llassert (term != NULL);
 331
 332   switch (term->kind)
 333     {
 334     case EXPRNODE:
 335       /*@i334*/  /*wtf*/
 336       s = message ("%s @ %q", exprNode_unparse (term->value.expr),
 337                    fileloc_unparse (term->loc) );
 338       break;
 339     case INTLITERAL:
 340       s = message ("%d", (int)term->value.intlit);
 341       break;
 342
 343     case SREF:
 344       s = message ("%q", sRef_unparseDebug (term->value.sref) );
 345
 346       break;
 347     default:
 348       BADEXIT;
 349     }
 350
 351   return s;
 352 }
 353
 354
 355 constraintTerm constraintTerm_makeIntLiteral (long i)
 356 {
 357   constraintTerm ret = new_constraintTermExpr();
 358   ret->value.intlit = i;
 359   ret->kind = INTLITERAL;
 360   ret->loc =  fileloc_undefined;
 361   return ret;
 362 }
 363
 364 bool constraintTerm_canGetValue (constraintTerm term)
 365 {
 366   if (term->kind == INTLITERAL)
 367     {
 368       return TRUE;
 369     }
 370   else if (term->kind == SREF)
 371     {
 372       if (sRef_hasValue (term->value.sref))
 373         {
 374           multiVal mval = sRef_getValue (term->value.sref);
 375
 376           return multiVal_isInt (mval); /* for now, only try to deal with int values */
 377         }
 378       else
 379         {
 380           return FALSE;
 381         }
 382     }
 383   else if (term->kind == EXPRNODE)
 384     {
 385       return FALSE;
 386     }
 387   else
 388     {
 389       return FALSE;
 390     }
 391 }
 392
 393 long constraintTerm_getValue (constraintTerm term)
 394 {
 395   llassert (constraintTerm_canGetValue (term));
 396
 397   if (term->kind == INTLITERAL)
 398     {
 399       return term->value.intlit;
 400     }
 401   else if (term->kind == SREF)
 402     {
 403       if (sRef_hasValue (term->value.sref))
 404         {
 405           multiVal mval = sRef_getValue (term->value.sref);
 406
 407           return multiVal_forceInt (mval); /* for now, only try to deal with int values */
 408         }
 409       else
 410         {
 411           BADBRANCH;
 412         }
 413     }
 414   else if (term->kind == EXPRNODE)
 415     {
 416       BADBRANCH;
 417     }
 418   else
 419     {
 420       BADBRANCH;
 421     }
 422
 423   BADEXIT;
 424 }
 425
 426 /*drl added this 10.30.001
 427  */
 428
 429 /*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t)
 430 {
 431   llassert (t != NULL);
 432
 433   llassert (t->kind == EXPRNODE);
 434
 435   return t->value.expr;
 436
 437 }
 438
 439  /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t)
 440 {
 441   llassert (t != NULL);
 442   if (t->kind == EXPRNODE)
 443     {
 444       return exprNode_getSref(t->value.expr);
 445     }
 446
 447   if (t->kind == SREF)
 448     {
 449       return t->value.sref;
 450     }
 451
 452   return sRef_undefined;
 453 }
 454
 455 bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2)
 456 {
 457   cstring s1, s2;
 458
 459   llassert (term1 !=NULL && term2 !=NULL);
 460
 461  DPRINTF ((message
 462             ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
 463              )
 464             )
 465            );
 466
 467   s1 = constraintTerm_getName (term1);
 468   s2 = constraintTerm_getName (term2);
 469
 470   if (cstring_equal (s1, s2) )
 471     {
 472       DPRINTF ((message (" %q and %q are same", s1, s2 ) ) );
 473      return TRUE;
 474    }
 475   else
 476      {
 477      DPRINTF ((message (" %q and %q are not same", s1, s2 ) ) );
 478      return FALSE;
 479    }
 480 }
 481
 482 bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
 483 {
 484   sRef s1, s2;
 485
 486   llassert (term1 !=NULL && term2 !=NULL);
 487
 488   if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2))
 489     /* evans 2001-07-24: was (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) */
 490     {
 491       long t1, t2;
 492
 493       t1 = constraintTerm_getValue (term1);
 494       t2 = constraintTerm_getValue (term2);
 495
 496       return (t1 == t2);
 497     }
 498
 499   if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2))
 500     {
 501       /* evans 2001-07-24: is this right? */ /*@i534@*/
 502       return FALSE;
 503     }
 504
 505   s1 = constraintTerm_getsRef (term1);
 506   s2 = constraintTerm_getsRef (term2);
 507
 508   if (!(sRef_isValid(s1) && sRef_isValid(s2)))
 509     {
 510       return FALSE;
 511     }
 512
 513   DPRINTF((message
 514             ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
 515              )
 516             )
 517            );
 518
 519   if (sRef_similarRelaxed(s1, s2)   || sRef_sameName (s1, s2) )
 520     {
 521       DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
 522       return TRUE;
 523     }
 524   else
 525     {
 526       DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
 527       return FALSE;
 528     }
 529 }
 530
 531 void constraintTerm_dump ( /*@observer@*/ constraintTerm t,  FILE *f)
 532 {
 533   fileloc loc;
 534   constraintTermValue value;
 535   constraintTermType kind;
 536   uentry u;
 537
 538   loc = t->loc;
 539
 540   value = t->value;
 541
 542   kind  = t->kind;
 543
 544   fprintf(f, "%d\n", (int) kind);
 545
 546   switch (kind)
 547     {
 548
 549     case EXPRNODE:
 550       u = exprNode_getUentry(t->value.expr);
 551       fprintf(f, "%s\n", cstring_toCharsSafe( uentry_rawName (u) )
 552               );
 553       break;
 554
 555     case SREF:
 556       {
 557         sRef s;
 558
 559         s =  t->value.sref;
 560
 561         if (sRef_isResult (s ) )
 562           {
 563             fprintf(f, "Result\n");
 564           }
 565         else if (sRef_isParam (s ) )
 566           {
 567             int param;
 568             ctype ct;
 569             cstring ctString;
 570
 571
 572             ct =  sRef_getType (s);
 573             param = sRef_getParam(s);
 574
 575             ctString =  ctype_dump(ct);
 576
 577             fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param );
 578             cstring_free(ctString);
 579           }
 580         else
 581           {
 582             u = sRef_getUentry(s);
 583             fprintf(f, "%s\n", cstring_toCharsSafe(uentry_rawName (u) ) );
 584           }
 585
 586       }
 587       break;
 588
 589     case INTLITERAL:
 590       fprintf (f, "%ld\n", t->value.intlit);
 591       break;
 592
 593     default:
 594       BADEXIT;
 595     }
 596
 597 }
 598
 599
 600 /*@only@*/ constraintTerm constraintTerm_undump ( FILE *f)
 601 {
 602   constraintTermType kind;
 603   constraintTerm ret;
 604
 605   uentry ue;
 606
 607   char *str;
 608   char *os;
 609
 610   os = mstring_create (MAX_DUMP_LINE_LENGTH);
 611
 612   str = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 613
 614   kind = (constraintTermType) reader_getInt(&str);
 615   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 616
 617   switch (kind)
 618     {
 619
 620     case SREF:
 621       {
 622         sRef s;
 623         char * term;
 624         term = reader_getWord(&str);
 625
 626         if (strcmp (term, "Result") == 0 )
 627           {
 628             s = sRef_makeResult (ctype_unknown);
 629           }
 630         else if (strcmp (term, "Param" ) == 0 )
 631           {
 632             int param;
 633             char *str2, *ostr2;
 634
 635             ctype t;
 636
 637             reader_checkChar(&str, ' ');
 638             str2  = reader_getWord(&str);
 639             param = reader_getInt(&str);
 640
 641             ostr2 = str2;
 642             t = ctype_undump(&str2) ;
 643             s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc));
 644             free (ostr2);
 645           }
 646         else  /* This must be an identified that we can search for in usymTab */
 647           {
 648             cstring termStr = cstring_makeLiteralTemp(term);
 649
 650             ue = usymtab_lookup (termStr);
 651             s = uentry_getSref(ue);
 652           }
 653
 654         ret = constraintTerm_makesRef(s);
 655
 656         free(term);
 657       }
 658       break;
 659
 660     case EXPRNODE:
 661       {
 662         sRef s;
 663         char * term;
 664         cstring termStr;
 665
 666         term = reader_getWord(&str);
 667         /* This must be an identifier that we can search for in usymTab */
 668         termStr = cstring_makeLiteralTemp(term);
 669
 670         ue = usymtab_lookup (termStr);
 671         s = uentry_getSref(ue);
 672         ret = constraintTerm_makesRef(s);
 673
 674         free (term);
 675       }
 676       break;
 677
 678
 679     case INTLITERAL:
 680       {
 681         int i;
 682
 683         i = reader_getInt(&str);
 684         ret = constraintTerm_makeIntLiteral (i);
 685       }
 686       break;
 687
 688     default:
 689       BADEXIT;
 690     }
 691   free (os);
 692
 693   return ret;
 694 }
 695
 696
 697
 698