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