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_getfileloc(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 long constraintTerm_getValue (constraintTerm term)
 390 {
 391   llassert (constraintTerm_canGetValue (term));
 392
 393   if (term->kind == CTT_INTLITERAL)
 394     {
 395       return term->value.intlit;
 396     }
 397   else if (term->kind == CTT_SREF)
 398     {
 399       if (sRef_hasValue (term->value.sref))
 400         {
 401           multiVal mval = sRef_getValue (term->value.sref);
 402
 403           return multiVal_forceInt (mval); /* for now, only try to deal with int values */
 404         }
 405       else
 406         {
 407           BADBRANCH;
 408         }
 409     }
 410   else if (term->kind == CTT_EXPR)
 411     {
 412       BADBRANCH;
 413     }
 414   else
 415     {
 416       BADBRANCH;
 417     }
 418
 419   BADEXIT;
 420 }
 421
 422 /*drl added this 10.30.001
 423  */
 424
 425 /*@exposed@*/ exprNode constraintTerm_getExprNode (constraintTerm t)
 426 {
 427   llassert (t != NULL);
 428
 429   llassert (t->kind == CTT_EXPR);
 430
 431   return t->value.expr;
 432
 433 }
 434
 435  /*@exposed@*/ sRef constraintTerm_getsRef (constraintTerm t)
 436 {
 437   llassert (t != NULL);
 438   if (t->kind == CTT_EXPR)
 439     {
 440       return exprNode_getSref(t->value.expr);
 441     }
 442
 443   if (t->kind == CTT_SREF)
 444     {
 445       return t->value.sref;
 446     }
 447
 448   return sRef_undefined;
 449 }
 450
 451 bool constraintTerm_probSame (constraintTerm term1, constraintTerm term2)
 452 {
 453   cstring s1, s2;
 454
 455   llassert (term1 !=NULL && term2 !=NULL);
 456
 457  DPRINTF ((message
 458             ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
 459              )
 460             )
 461            );
 462
 463   s1 = constraintTerm_getName (term1);
 464   s2 = constraintTerm_getName (term2);
 465
 466   if (cstring_equal (s1, s2) )
 467     {
 468       DPRINTF ((message (" %q and %q are same", s1, s2 ) ) );
 469      return TRUE;
 470    }
 471   else
 472      {
 473      DPRINTF ((message (" %q and %q are not same", s1, s2 ) ) );
 474      return FALSE;
 475    }
 476 }
 477
 478 bool constraintTerm_similar (constraintTerm term1, constraintTerm term2)
 479 {
 480   sRef s1, s2;
 481
 482   llassert (term1 !=NULL && term2 !=NULL);
 483
 484   if (constraintTerm_canGetValue (term1) && constraintTerm_canGetValue (term2))
 485
 486     /*3/30/2003 comment updated to reflect name change form INTLITERAL to CTT_INTLITERAL*/
 487     /* evans 2001-07-24: was (term1->kind == CTT_INTLITERAL) && (term2->kind == CTT_INTLITERAL) ) */
 488     {
 489       long t1, t2;
 490
 491       t1 = constraintTerm_getValue (term1);
 492       t2 = constraintTerm_getValue (term2);
 493
 494       return (t1 == t2);
 495     }
 496
 497   if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2))
 498     {
 499       /* evans 2001-07-24: is this right? */ /*@i534@*/
 500       return FALSE;
 501     }
 502
 503   s1 = constraintTerm_getsRef (term1);
 504   s2 = constraintTerm_getsRef (term2);
 505
 506   if (!(sRef_isValid(s1) && sRef_isValid(s2)))
 507     {
 508       return FALSE;
 509     }
 510
 511   DPRINTF((message
 512             ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
 513              )
 514             )
 515            );
 516
 517   if (sRef_similarRelaxed(s1, s2)   || sRef_sameName (s1, s2) )
 518     {
 519       DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
 520       return TRUE;
 521     }
 522   else
 523     {
 524       DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
 525       return FALSE;
 526     }
 527 }
 528
 529 void constraintTerm_dump (/*@observer@*/ constraintTerm t,  FILE *f)
 530 {
 531   fileloc loc;
 532   constraintTermValue value;
 533   constraintTermType kind;
 534   uentry u;
 535
 536   loc = t->loc;
 537
 538   value = t->value;
 539
 540   kind  = t->kind;
 541
 542   fprintf(f, "%d\n", (int) kind);
 543
 544   switch (kind)
 545     {
 546
 547     case CTT_EXPR:
 548       u = exprNode_getUentry(t->value.expr);
 549       fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
 550       break;
 551
 552     case CTT_SREF:
 553       {
 554         sRef s;
 555
 556         s =  t->value.sref;
 557
 558         if (sRef_isResult (s ) )
 559           {
 560             fprintf(f, "Result\n");
 561           }
 562         else if (sRef_isParam (s))
 563           {
 564             int param;
 565             ctype ct;
 566             cstring ctString;
 567
 568
 569             ct =  sRef_getType (s);
 570             param = sRef_getParam(s);
 571
 572             ctString =  ctype_dump(ct);
 573
 574             fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param );
 575             cstring_free(ctString);
 576           }
 577         else if (sRef_isField (s) )
 578           {
 579             fprintf(f, "sRef_dump %s\n", cstring_toCharsSafe(sRef_dump(s)) );
 580           }
 581         else
 582           {
 583             u = sRef_getUentry(s);
 584             fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
 585           }
 586
 587       }
 588       break;
 589
 590     case CTT_INTLITERAL:
 591       fprintf (f, "%ld\n", t->value.intlit);
 592       break;
 593
 594     default:
 595       BADEXIT;
 596     }
 597
 598 }
 599
 600
 601 /*@only@*/ constraintTerm constraintTerm_undump (FILE *f)
 602 {
 603   constraintTermType kind;
 604   constraintTerm ret;
 605
 606   uentry ue;
 607
 608   char *str;
 609   char *os;
 610
 611   os = mstring_create (MAX_DUMP_LINE_LENGTH);
 612
 613   str = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 614
 615   llassert (str != NULL);
 616
 617   kind = (constraintTermType) reader_getInt(&str);
 618   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 619
 620   llassert (str != NULL);
 621
 622   switch (kind)
 623     {
 624
 625     case CTT_SREF:
 626       {
 627         sRef s;
 628         char * term;
 629         term = reader_getWord(&str);
 630
 631         if (term == NULL)
 632           {
 633             llfatalbug (message ("Library file appears to be corrupted.") );
 634           }
 635         if (strcmp (term, "Result") == 0 )
 636           {
 637             s = sRef_makeResult (ctype_unknown);
 638           }
 639         else if (strcmp (term, "Param" ) == 0 )
 640           {
 641             int param;
 642             char *str2, *ostr2;
 643
 644             ctype t;
 645
 646             reader_checkChar(&str, ' ');
 647             str2  = reader_getWord(&str);
 648             param = reader_getInt(&str);
 649
 650         if (str2 == NULL)
 651           {
 652             llfatalbug (message ("Library file appears to be corrupted.") );
 653           }
 654
 655             ostr2 = str2;
 656             t = ctype_undump(&str2) ;
 657             s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED));
 658             free (ostr2);
 659           }
 660         else if (strcmp (term, "sRef_dump" ) == 0 )
 661           {
 662             reader_checkChar(&str, ' ');
 663             s = sRef_undump (&str);
 664           }
 665         else  /* This must be an identified that we can search for in usymTab */
 666           {
 667             cstring termStr = cstring_makeLiteralTemp(term);
 668
 669             ue = usymtab_lookup (termStr);
 670             s = uentry_getSref(ue);
 671           }
 672
 673         ret = constraintTerm_makesRef(s);
 674
 675         free(term);
 676       }
 677       break;
 678
 679     case CTT_EXPR:
 680       {
 681         sRef s;
 682         char * term;
 683         cstring termStr;
 684
 685         term = reader_getWord(&str);
 686
 687         if (term == NULL)
 688           {
 689             llfatalbug (message ("Library file appears to be corrupted.") );
 690           }
 691
 692         /* This must be an identifier that we can search for in usymTab */
 693         termStr = cstring_makeLiteralTemp(term);
 694
 695         ue = usymtab_lookup (termStr);
 696         s = uentry_getSref(ue);
 697         ret = constraintTerm_makesRef(s);
 698
 699         free (term);
 700       }
 701       break;
 702
 703
 704     case CTT_INTLITERAL:
 705       {
 706         int i;
 707
 708         i = reader_getInt(&str);
 709         ret = constraintTerm_makeIntLiteral (i);
 710       }
 711       break;
 712
 713     default:
 714       BADEXIT;
 715     }
 716   free (os);
 717
 718   return ret;
 719 }
 720
 721
 722
 723 /* drl added sometime before 10/17/001*/
 724 ctype constraintTerm_getCType (constraintTerm term)
 725 {
 726   ctype ct;
 727
 728   switch (term->kind)
 729     {
 730     case CTT_EXPR:
 731       ct = exprNode_getType (term->value.expr);
 732       break;
 733
 734     case CTT_INTLITERAL:
 735       /*@i888*/ /* hack */
 736       ct = ctype_signedintegral;
 737       break;
 738
 739     case CTT_SREF:
 740       ct = sRef_getType (term->value.sref) ;
 741       break;
 742     default:
 743       BADEXIT;
 744     }
 745   return ct;
 746 }
 747
 748 bool constraintTerm_isConstantOnly (constraintTerm term)
 749 {
 750   switch (term->kind)
 751     {
 752     case CTT_EXPR:
 753       if (exprNode_isNumLiteral (term->value.expr) ||
 754           exprNode_isStringLiteral (term->value.expr) ||
 755           exprNode_isCharLiteral  (term->value.expr) )
 756         {
 757           return TRUE;
 758         }
 759       else
 760         {
 761           return FALSE;
 762         }
 763
 764     case CTT_INTLITERAL:
 765       return TRUE;
 766
 767     case CTT_SREF:
 768       if ( sRef_isConst (term->value.sref) )
 769         {
 770           return TRUE;
 771         }
 772       else
 773         {
 774           return FALSE;
 775         }
 776     default:
 777       BADEXIT;
 778     }
 779
 780   BADEXIT;
 781 }