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 EXPRNODE:
  54       /* we don't free an exprNode*/
  55       break;
  56     case SREF:
  57       /* sref */
  58       sRef_free (term->value.sref);
  59       break;
  60     case INTLITERAL:
  61       /* don't free an int */
  62       break;
  63     case  ERRORBADCONSTRAINTTERMTYPE:
  64     default:
  65       /* type was set incorrectly */
  66       llcontbug (message("constraintTerm_free type was set incorrectly"));
  67     }
  68
  69   term->kind =  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 == 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   if (c->kind == EXPRNODE)
  97     {
  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   if (c->kind == EXPRNODE)
 112     {
 113       return TRUE;
 114     }
 115   return FALSE;
 116 }
 117
 118 /*@access exprNode@*/
 119 int constraintTerm_getInitBlockLength (/*@observer@*/ /*@temp@*/ constraintTerm c) /*@*/
 120 {
 121
 122   exprNodeList  list;
 123   int ret;
 124   llassert (c != NULL);
 125   llassert (constraintTerm_isInitBlock (c) );
 126   llassert (c->kind == EXPRNODE);
 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 == EXPRNODE)
 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 == EXPRNODE);
 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 == EXPRNODE)
 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 = 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 == 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 = EXPRNODE;
 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 = 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 EXPRNODE:
 240       ret->value.expr = term->value.expr;
 241       break;
 242     case INTLITERAL:
 243       ret->value.intlit = term->value.intlit;
 244       break;
 245
 246     case 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 EXPRNODE:
 278
 279       s = message ("%s", exprNode_unparse (term->value.expr) );
 280       break;
 281     case INTLITERAL:
 282       s = message (" %d ", (int) term->value.intlit);
 283       break;
 284
 285     case 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 EXPRNODE:
 306
 307       break;
 308     case INTLITERAL:
 309       break;
 310
 311     case 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_print (constraintTerm term)  /*@*/
 322 {
 323   cstring s;
 324   s = cstring_undefined;
 325
 326   llassert (term != NULL);
 327
 328   switch (term->kind)
 329     {
 330     case EXPRNODE:
 331
 332       s = message ("%s @ %q", exprNode_unparse (term->value.expr),
 333                    fileloc_unparse (term->loc) );
 334       break;
 335     case INTLITERAL:
 336       s = message ("%d", (int)term->value.intlit);
 337       break;
 338
 339     case 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 = INTLITERAL;
 356   ret->loc =  fileloc_undefined;
 357   return ret;
 358 }
 359
 360 bool constraintTerm_canGetValue (constraintTerm term)
 361 {
 362   if (term->kind == INTLITERAL)
 363     {
 364       return TRUE;
 365     }
 366   else if (term->kind == 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 == EXPRNODE)
 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 == INTLITERAL)
 394     {
 395       return term->value.intlit;
 396     }
 397   else if (term->kind == 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 == EXPRNODE)
 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 == EXPRNODE);
 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 == EXPRNODE)
 439     {
 440       return exprNode_getSref(t->value.expr);
 441     }
 442
 443   if (t->kind == 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     /* evans 2001-07-24: was (term1->kind == INTLITERAL) && (term2->kind == INTLITERAL) ) */
 486     {
 487       long t1, t2;
 488
 489       t1 = constraintTerm_getValue (term1);
 490       t2 = constraintTerm_getValue (term2);
 491
 492       return (t1 == t2);
 493     }
 494
 495   if (constraintTerm_canGetValue (term1) || constraintTerm_canGetValue (term2))
 496     {
 497       /* evans 2001-07-24: is this right? */ /*@i534@*/
 498       return FALSE;
 499     }
 500
 501   s1 = constraintTerm_getsRef (term1);
 502   s2 = constraintTerm_getsRef (term2);
 503
 504   if (!(sRef_isValid(s1) && sRef_isValid(s2)))
 505     {
 506       return FALSE;
 507     }
 508
 509   DPRINTF((message
 510             ("Comparing srefs for %s and  %s ", constraintTerm_print(term1), constraintTerm_print(term2)
 511              )
 512             )
 513            );
 514
 515   if (sRef_similarRelaxed(s1, s2)   || sRef_sameName (s1, s2) )
 516     {
 517       DPRINTF ((message (" %s and %s are same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
 518       return TRUE;
 519     }
 520   else
 521     {
 522       DPRINTF ((message (" %s and %s are not same", constraintTerm_print(term1), constraintTerm_print(term2)  )  ));
 523       return FALSE;
 524     }
 525 }
 526
 527 void constraintTerm_dump (/*@observer@*/ constraintTerm t,  FILE *f)
 528 {
 529   fileloc loc;
 530   constraintTermValue value;
 531   constraintTermType kind;
 532   uentry u;
 533
 534   loc = t->loc;
 535
 536   value = t->value;
 537
 538   kind  = t->kind;
 539
 540   fprintf(f, "%d\n", (int) kind);
 541
 542   switch (kind)
 543     {
 544
 545     case EXPRNODE:
 546       u = exprNode_getUentry(t->value.expr);
 547       fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
 548       break;
 549
 550     case SREF:
 551       {
 552         sRef s;
 553
 554         s =  t->value.sref;
 555
 556         if (sRef_isResult (s ) )
 557           {
 558             fprintf(f, "Result\n");
 559           }
 560         else if (sRef_isParam (s))
 561           {
 562             int param;
 563             ctype ct;
 564             cstring ctString;
 565
 566
 567             ct =  sRef_getType (s);
 568             param = sRef_getParam(s);
 569
 570             ctString =  ctype_dump(ct);
 571
 572             fprintf(f, "Param %s %d\n", cstring_toCharsSafe(ctString), (int) param );
 573             cstring_free(ctString);
 574           }
 575         else if (sRef_isField (s) )
 576           {
 577             fprintf(f, "sRef_dump %s\n", cstring_toCharsSafe(sRef_dump(s)) );
 578           }
 579         else
 580           {
 581             u = sRef_getUentry(s);
 582             fprintf (f, "%s\n", cstring_toCharsSafe (uentry_rawName (u)));
 583           }
 584
 585       }
 586       break;
 587
 588     case INTLITERAL:
 589       fprintf (f, "%ld\n", t->value.intlit);
 590       break;
 591
 592     default:
 593       BADEXIT;
 594     }
 595
 596 }
 597
 598
 599 /*@only@*/ constraintTerm constraintTerm_undump (FILE *f)
 600 {
 601   constraintTermType kind;
 602   constraintTerm ret;
 603
 604   uentry ue;
 605
 606   char *str;
 607   char *os;
 608
 609   os = mstring_create (MAX_DUMP_LINE_LENGTH);
 610
 611   str = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 612
 613   llassert (str != NULL);
 614
 615   kind = (constraintTermType) reader_getInt(&str);
 616   str = fgets(os, MAX_DUMP_LINE_LENGTH, f);
 617
 618   llassert (str != NULL);
 619
 620   switch (kind)
 621     {
 622
 623     case SREF:
 624       {
 625         sRef s;
 626         char * term;
 627         term = reader_getWord(&str);
 628
 629         if (term == NULL)
 630           {
 631             llfatalbug (message ("Library file appears to be corrupted.") );
 632           }
 633         if (strcmp (term, "Result") == 0 )
 634           {
 635             s = sRef_makeResult (ctype_unknown);
 636           }
 637         else if (strcmp (term, "Param" ) == 0 )
 638           {
 639             int param;
 640             char *str2, *ostr2;
 641
 642             ctype t;
 643
 644             reader_checkChar(&str, ' ');
 645             str2  = reader_getWord(&str);
 646             param = reader_getInt(&str);
 647
 648         if (str2 == NULL)
 649           {
 650             llfatalbug (message ("Library file appears to be corrupted.") );
 651           }
 652
 653             ostr2 = str2;
 654             t = ctype_undump(&str2) ;
 655             s = sRef_makeParam (param, t, stateInfo_makeLoc (g_currentloc, SA_CREATED));
 656             free (ostr2);
 657           }
 658         else if (strcmp (term, "sRef_dump" ) == 0 )
 659           {
 660             reader_checkChar(&str, ' ');
 661             s = sRef_undump (&str);
 662           }
 663         else  /* This must be an identified that we can search for in usymTab */
 664           {
 665             cstring termStr = cstring_makeLiteralTemp(term);
 666
 667             ue = usymtab_lookup (termStr);
 668             s = uentry_getSref(ue);
 669           }
 670
 671         ret = constraintTerm_makesRef(s);
 672
 673         free(term);
 674       }
 675       break;
 676
 677     case EXPRNODE:
 678       {
 679         sRef s;
 680         char * term;
 681         cstring termStr;
 682
 683         term = reader_getWord(&str);
 684
 685         if (term == NULL)
 686           {
 687             llfatalbug (message ("Library file appears to be corrupted.") );
 688           }
 689
 690         /* This must be an identifier that we can search for in usymTab */
 691         termStr = cstring_makeLiteralTemp(term);
 692
 693         ue = usymtab_lookup (termStr);
 694         s = uentry_getSref(ue);
 695         ret = constraintTerm_makesRef(s);
 696
 697         free (term);
 698       }
 699       break;
 700
 701
 702     case INTLITERAL:
 703       {
 704         int i;
 705
 706         i = reader_getInt(&str);
 707         ret = constraintTerm_makeIntLiteral (i);
 708       }
 709       break;
 710
 711     default:
 712       BADEXIT;
 713     }
 714   free (os);
 715
 716   return ret;
 717 }
 718
 719
 720
 721 /* drl added sometime before 10/17/001*/
 722 ctype constraintTerm_getCType (constraintTerm term)
 723 {
 724   ctype ct;
 725
 726   switch (term->kind)
 727     {
 728     case EXPRNODE:
 729       ct = exprNode_getType (term->value.expr);
 730       break;
 731
 732     case INTLITERAL:
 733       /*@i888*/ /* hack */
 734       ct = ctype_signedintegral;
 735       break;
 736
 737     case SREF:
 738       ct = sRef_getType (term->value.sref) ;
 739       break;
 740     default:
 741       BADEXIT;
 742     }
 743   return ct;
 744 }
 745
 746 bool constraintTerm_isConstantOnly (constraintTerm term)
 747 {
 748   switch (term->kind)
 749     {
 750     case EXPRNODE:
 751       if (exprNode_isNumLiteral (term->value.expr) ||
 752           exprNode_isStringLiteral (term->value.expr) ||
 753           exprNode_isCharLiteral  (term->value.expr) )
 754         {
 755           return TRUE;
 756         }
 757       else
 758         {
 759           return FALSE;
 760         }
 761
 762     case INTLITERAL:
 763       return TRUE;
 764
 765     case SREF:
 766       if ( sRef_isConst (term->value.sref) )
 767         {
 768           return TRUE;
 769         }
 770       else
 771         {
 772           return FALSE;
 773         }
 774     default:
 775       BADEXIT;
 776     }
 777
 778   BADEXIT;
 779 }