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