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