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         /*drl this if statement handles the case where constraintTerm_canGetValue only returns
 498           true for term1 or term2 but no both
 499           if constraintTerm_canGetValue returned tru for both we would have returned in the previous if statement
 500           I suppose this could be done with xor but I've never used xor and don't feel like starting now
 501           besides this way is more effecient.
 502         */
 503   if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2))
 504     {
 505
 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 CTT_EXPR:
 554       u = exprNode_getUentry(t->value.expr);
 555       fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
 556       break;
 557
 558     case CTT_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 CTT_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 CTT_SREF:
 632       {
 633         sRef s;
 634         char * term;
 635         term = reader_getWord(&str);
 636
 637         if (term == NULL)
 638           {
 639             llfatalbug (message ("Library file appears to be corrupted.") );
 640           }
 641         if (strcmp (term, "Result") == 0 )
 642           {
 643             s = sRef_makeResult (ctype_unknown);
 644           }
 645         else if (strcmp (term, "Param" ) == 0 )
 646           {
 647             int param;
 648             char *str2, *ostr2;
 649
 650             ctype t;
 651
 652             reader_checkChar(&str, ' ');
 653             str2  = reader_getWord(&str);
 654             param = reader_getInt(&str);
 655
 656         if (str2 == NULL)
 657           {
 658             llfatalbug (message ("Library file appears to be corrupted.") );
 659           }
 660
 661             ostr2 = str2;
 662             t = ctype_undump(&str2) ;
 663             s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED));
 664             free (ostr2);
 665           }
 666         else if (strcmp (term, "sRef_dump" ) == 0 )
 667           {
 668             reader_checkChar(&str, ' ');
 669             s = sRef_undump (&str);
 670           }
 671         else  /* This must be an identified that we can search for in usymTab */
 672           {
 673             cstring termStr = cstring_makeLiteralTemp(term);
 674
 675             ue = usymtab_lookup (termStr);
 676             s = uentry_getSref(ue);
 677           }
 678
 679         ret = constraintTerm_makesRef(s);
 680
 681         free(term);
 682       }
 683       break;
 684
 685     case CTT_EXPR:
 686       {
 687         sRef s;
 688         char * term;
 689         cstring termStr;
 690
 691         term = reader_getWord(&str);
 692
 693         if (term == NULL)
 694           {
 695             llfatalbug (message ("Library file appears to be corrupted.") );
 696           }
 697
 698         /* This must be an identifier that we can search for in usymTab */
 699         termStr = cstring_makeLiteralTemp(term);
 700
 701         ue = usymtab_lookup (termStr);
 702         s = uentry_getSref(ue);
 703         ret = constraintTerm_makesRef(s);
 704
 705         free (term);
 706       }
 707       break;
 708
 709
 710     case CTT_INTLITERAL:
 711       {
 712         int i;
 713
 714         i = reader_getInt(&str);
 715         ret = constraintTerm_makeIntLiteral (i);
 716       }
 717       break;
 718
 719     default:
 720       BADEXIT;
 721     }
 722   free (os);
 723
 724   return ret;
 725 }
 726
 727
 728
 729 /* drl added sometime before 10/17/001*/
 730 ctype constraintTerm_getCType (constraintTerm term)
 731 {
 732   ctype ct;
 733
 734   switch (term->kind)
 735     {
 736     case CTT_EXPR:
 737       ct = exprNode_getType (term->value.expr);
 738       break;
 739
 740     case CTT_INTLITERAL:
 741       ct = ctype_signedintegral;
 742       break;
 743
 744     case CTT_SREF:
 745       ct = sRef_getType (term->value.sref) ;
 746       break;
 747     default:
 748       BADEXIT;
 749     }
 750   return ct;
 751 }
 752
 753 bool constraintTerm_isConstantOnly (constraintTerm term)
 754 {
 755   switch (term->kind)
 756     {
 757     case CTT_EXPR:
 758       if (exprNode_isNumLiteral (term->value.expr) ||
 759           exprNode_isStringLiteral (term->value.expr) ||
 760           exprNode_isCharLiteral  (term->value.expr) )
 761         {
 762           return TRUE;
 763         }
 764       else
 765         {
 766           return FALSE;
 767         }
 768
 769     case CTT_INTLITERAL:
 770       return TRUE;
 771
 772     case CTT_SREF:
 773       if ( sRef_isConst (term->value.sref) )
 774         {
 775           return TRUE;
 776         }
 777       else
 778         {
 779           return FALSE;
 780         }
 781     default:
 782       BADEXIT;
 783     }
 784
 785   BADEXIT;
 786 }