src/constraintList.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2000 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 ** constraintList.c
  27 **
  28 ** based on list_template.c
  29 **
  30 ** where T has T_equal (or change this) and T_unparse
  31 */
  32
  33 # include "splintMacros.nf"
  34 # include "llbasic.h"
  35
  36 /*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
  37 # define constraintList_elements_private_only(x, m_el) \
  38    { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
  39      for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  40        { constraint m_el = *(m_elements++);
  41
  42 # define end_constraintList_elements_private_only }}}
  43
  44
  45 /*@iter constraintList_elements_private (sef constraintList x, yield  constraint el); @*/
  46 # define constraintList_elements_private(x, m_el) \
  47    { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
  48      for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  49        { constraint m_el = *(m_elements++);
  50
  51 # define end_constraintList_elements_private }}}
  52
  53
  54 /*@only@*/ constraintList constraintList_makeNew ()
  55 {
  56   constraintList s = (constraintList) dmalloc (sizeof (*s));
  57
  58   s->nelements = 0;
  59   s->nspace = constraintListBASESIZE;
  60   s->elements = (constraint *)
  61     dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
  62
  63   return (s);
  64 }
  65
  66 static void
  67 constraintList_grow (constraintList s)
  68 {
  69   int i;
  70   constraint *newelements;
  71
  72   llassert (constraintList_isDefined (s));
  73
  74   s->nspace += constraintListBASESIZE;
  75   newelements = (constraint *) dmalloc (sizeof (*newelements)
  76                                      * (s->nelements + s->nspace));
  77
  78   for (i = 0; i < s->nelements; i++)
  79     {
  80       newelements[i] = s->elements[i];
  81     }
  82
  83   sfree (s->elements);
  84   s->elements = newelements;
  85 }
  86
  87
  88 constraintList
  89 constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
  90 {
  91   llassert (constraintList_isDefined (s));
  92
  93   /*drl7x */
  94
  95   if (constraintList_resolve (el, s) )
  96     {
  97       constraint_free (el);
  98       return s;
  99     }
 100
 101   if (s->nspace <= 0)
 102     constraintList_grow (s);
 103
 104   s->nspace--;
 105   s->elements[s->nelements] = el;
 106   s->nelements++;
 107   return s;
 108 }
 109
 110 /* frees everything but actual constraints */
 111 /* This function should only be used if you have
 112    other references to unshared constraints
 113 */
 114 static void constraintList_freeShallow (/*@only@*/ constraintList c)
 115 {
 116   if (constraintList_isDefined(c) )
 117     {
 118       free (c->elements);
 119       c->elements = NULL;
 120       c->nelements = -1;
 121       c->nspace = -1;
 122     }
 123   free (c);
 124   c = NULL;
 125 }
 126
 127 /*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ /*@temp@*/ constraintList newList)
 128 {
 129   llassert(constraintList_isDefined(s) );
 130   llassert(constraintList_isDefined(newList) );
 131
 132   if (newList == constraintList_undefined)
 133     return s;
 134
 135   constraintList_elements (newList, elem)
 136     {
 137     s = constraintList_add (s, constraint_copy(elem) );
 138     }
 139   end_constraintList_elements;
 140
 141   return s;
 142 }
 143
 144 constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
 145 {
 146   llassert(constraintList_isDefined(s) );
 147   llassert(constraintList_isDefined(newList) );
 148
 149   if (constraintList_isUndefined(newList) )
 150     return s;
 151
 152   constraintList_elements_private_only(newList, elem)
 153     {
 154     s = constraintList_add (s, elem);
 155     }
 156   end_constraintList_elements_private_only
 157
 158     constraintList_freeShallow(newList);
 159     return s;
 160 }
 161
 162
 163 constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s)
 164 {
 165   constraintList ret;
 166   fileloc loc;
 167   llassert(constraintList_isDefined(s) );
 168
 169   ret = constraintList_makeNew();
 170
 171   constraintList_elements_private_only(s, elem)
 172     {
 173       loc = constraint_getFileloc(elem);
 174
 175       if (fileloc_isUndefined(loc))
 176         {
 177           ret = constraintList_add (ret, elem);
 178         }
 179
 180       else if (context_suppressFlagMsg(FLG_BOUNDSWRITE, loc) )
 181         {
 182           DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q",
 183                              constraint_print(elem))));
 184           constraint_free(elem);
 185         }
 186
 187       else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc))
 188         {
 189           DPRINTF ((message("constraintList_removeSurpressed getting rid of surpressed constraint %q",
 190                             constraint_print(elem))));
 191           constraint_free(elem);
 192         }
 193       else
 194         {
 195           ret = constraintList_add (ret, elem);
 196         }
 197       fileloc_free(loc);
 198     }
 199   end_constraintList_elements_private_only;
 200
 201   constraintList_freeShallow(s);
 202
 203   return ret;
 204 }
 205
 206
 207 extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList s) /*@*/
 208 {
 209   return (constraintList_print(s));
 210 }
 211
 212 # if 0
 213 static /*@only@*/ cstring
 214 constraintList_printLocation (/*@temp@*/ constraintList s) /*@*/
 215 {
 216   int i;
 217   cstring st = cstring_undefined;
 218   bool first = TRUE;
 219
 220   if (!constraintList_isDefined (s))
 221     {
 222       return cstring_makeLiteral ("<undefined>");
 223     }
 224
 225   if (s->nelements == 0)
 226     {
 227       st = cstring_makeLiteral("<List Empty>");
 228       return st;
 229     }
 230
 231   for (i = 0; i < s->nelements; i++)
 232     {
 233       cstring type = cstring_undefined;
 234       constraint current = s->elements[i];
 235
 236       if (constraint_isDefined(current) )
 237         {
 238           cstring temp1;
 239               temp1 = constraint_printLocation(current);
 240           type = message ("%q %q\n", type, temp1 );
 241         }
 242
 243       if (first)
 244         {
 245           st = type;
 246           first = FALSE;
 247         }
 248       else
 249         {
 250           st = message ("%q, %q", st, type);
 251         }
 252     }
 253
 254   return st;
 255 }
 256 # endif
 257
 258 /*@only@*/ cstring
 259 constraintList_print (/*@temp@*/ constraintList s) /*@*/
 260 {
 261   int i;
 262   cstring st = cstring_undefined;
 263   bool first = TRUE;
 264
 265   if (!constraintList_isDefined (s))
 266     {
 267       return cstring_makeLiteral ("<undefined>");
 268     }
 269
 270   if (s->nelements == 0)
 271     {
 272       st = cstring_makeLiteral("<List Empty>");
 273       return st;
 274     }
 275
 276   for (i = 0; i < s->nelements; i++)
 277     {
 278       cstring type = cstring_undefined;
 279       constraint current = s->elements[i];
 280
 281       if (constraint_isDefined(current) )
 282         {
 283           cstring temp1;
 284
 285           if (context_getFlag (FLG_ORCONSTRAINT))
 286             {
 287               temp1 = constraint_printOr(current);
 288             }
 289           else
 290             {
 291               temp1 = constraint_print (current);
 292             }
 293           type = message ("%q %q\n", type, temp1 );
 294         }
 295
 296       if (first)
 297         {
 298           st = type;
 299           first = FALSE;
 300         }
 301       else
 302         {
 303           st = message ("%q, %q", st, type);
 304         }
 305     }
 306
 307   return st;
 308 }
 309
 310 void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
 311 {
 312
 313   constraintList_elements (s, elem)
 314     {
 315       if (constraint_isDefined(elem))
 316         {
 317           constraint_printErrorPostCondition (elem, loc);
 318         }
 319     }
 320   end_constraintList_elements;
 321   return;
 322 }
 323
 324 void constraintList_printError (constraintList s, fileloc loc)
 325 {
 326
 327   constraintList_elements (s, elem)
 328     {
 329       if (constraint_isDefined(elem) )
 330         {
 331           if (constraint_isPost(elem) )
 332             constraint_printErrorPostCondition (elem, loc);
 333           else
 334             constraint_printError (elem, loc);
 335         }
 336     }
 337   end_constraintList_elements;
 338   return;
 339 }
 340
 341
 342 cstring
 343 constraintList_printDetailed (constraintList s)
 344 {
 345   int i;
 346   cstring st = cstring_undefined;
 347   bool first = TRUE;
 348
 349   if (!constraintList_isDefined (s))
 350     {
 351       return cstring_makeLiteral ("<undefined>");
 352     }
 353
 354   if (s->nelements == 0)
 355     {
 356       st = cstring_makeLiteral("<List Empty>");
 357       return st;
 358     }
 359
 360   for (i = 0; i < s->nelements; i++)
 361     {
 362       cstring type = cstring_undefined;
 363       constraint current = s->elements[i];
 364
 365       if (constraint_isDefined(current ) )
 366         {
 367           cstring temp1 = constraint_printDetailed (current);
 368           type = message ("%s %s\n", type, temp1 );
 369           cstring_free(temp1);
 370         }
 371
 372       if (first)
 373         {
 374           st = type;
 375           first = FALSE;
 376           type = NULL;
 377         }
 378       else
 379         {
 380           st = message ("%q %q", st, type);
 381         }
 382     }
 383   return st;
 384 }
 385
 386 /*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
 387 } */
 388
 389 constraintList
 390 constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
 391 {
 392   constraint temp;
 393   constraintList ret;
 394   DPRINTF ((message ("Logical or on %s and %s",
 395                       constraintList_print(l1),
 396                       constraintList_print(l2)) ) );
 397
 398   ret = constraintList_makeNew();
 399   constraintList_elements (l1, el)
 400     {
 401       temp = constraint_substitute (el, l2);
 402
 403       if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
 404         {   /*avoid redundant constraints*/
 405           if (!constraintList_resolve (el, ret) )
 406             {
 407               constraint temp2;
 408               temp2 = constraint_copy(el);
 409               ret = constraintList_add (ret, temp2);
 410             }
 411         }
 412       constraint_free(temp);
 413     }
 414   end_constraintList_elements;
 415
 416    constraintList_elements (l2, el)
 417     {
 418       temp = constraint_substitute (el, l1);
 419
 420       if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
 421         {
 422           /*avoid redundant constraints*/
 423           if (!constraintList_resolve (el, ret) )
 424             {
 425               constraint temp2;
 426               temp2 = constraint_copy(el);
 427               ret = constraintList_add (ret, temp2);
 428             }
 429         }
 430       constraint_free(temp);
 431     }
 432   end_constraintList_elements;
 433
 434
 435   return ret;
 436 }
 437
 438 void
 439 constraintList_free (/*@only@*/ constraintList s)
 440 {
 441   int i;
 442
 443   llassert(constraintList_isDefined(s) );
 444
 445
 446   for (i = 0; i < s->nelements; i++)
 447     {
 448       constraint_free (s->elements[i]);
 449     }
 450
 451   sfree (s->elements);
 452   s->elements = NULL;
 453   s->nelements = -1;
 454   s->nspace = -1;
 455   sfree (s);
 456   s = NULL;
 457 }
 458
 459 constraintList
 460 constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
 461 {
 462   constraintList ret = constraintList_makeNew ();
 463
 464   constraintList_elements (s, el)
 465     {
 466       ret = constraintList_add (ret, constraint_copy (el));
 467     } end_constraintList_elements;
 468
 469   return ret;
 470 }
 471
 472 constraintList constraintList_preserveOrig (constraintList c)
 473 {
 474   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 475
 476   constraintList_elements_private (c, el)
 477   {
 478     el = constraint_preserveOrig (el);
 479   }
 480   end_constraintList_elements_private;
 481   return c;
 482 }
 483
 484 constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/  exprNode fcn)
 485 {
 486   DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_print (c) ) ));
 487
 488   constraintList_elements_private (c, el)
 489   {
 490     el = constraint_setFcnPre(el);
 491     el = constraint_origAddGeneratingExpr (el, fcn);
 492   }
 493   end_constraintList_elements_private;
 494   return c;
 495 }
 496
 497 constraintList constraintList_single (constraint c)
 498 {
 499   constraintList res;
 500   res = constraintList_makeNew();
 501   res = constraintList_add (res, c);
 502   return res;
 503 }
 504
 505 constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e)
 506 {
 507   DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
 508
 509   constraintList_elements_private (c, el)
 510   {
 511     DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) )  ));
 512     el = constraint_addGeneratingExpr (el, e);
 513   }
 514   end_constraintList_elements_private;
 515   return c;
 516 }
 517
 518 /*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
 519 {
 520   constraintList ret;
 521   ret = constraintList_makeNew();
 522   constraintList_elements_private (postconditions, el)
 523     {
 524       ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
 525     }
 526   end_constraintList_elements_private;
 527
 528   constraintList_free(postconditions);
 529   return ret;
 530 }
 531 /*
 532 Commenting out because function is not yet stable
 533
 534 / *@only@* / constraintList constraintList_doSRefFixStructConstraint(constraintList invars, sRef s, ctype ct )
 535 {
 536   constraintList ret;
 537   ret = constraintList_makeNew();
 538
 539   constraintList_elements (invars, el)
 540     {
 541       ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) );
 542     }
 543   end_constraintList_elements;
 544
 545   / *  constraintList_free (invars);* /
 546
 547   return ret;
 548 }
 549 */
 550
 551 /*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
 552 {
 553   constraintList ret;
 554   ret = constraintList_makeNew();
 555
 556   constraintList_elements (preconditions, el)
 557     {
 558       ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
 559     }
 560   end_constraintList_elements;
 561
 562   constraintList_free (preconditions);
 563
 564   return ret;
 565 }
 566 constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
 567                                                    exprNodeList arglist)
 568 {
 569   constraintList ret;
 570   constraint temp;
 571   ret = constraintList_makeNew();
 572
 573   constraintList_elements (preconditions, el)
 574     {
 575       temp = constraint_copy(el);
 576       ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
 577     }
 578   end_constraintList_elements;
 579
 580   return ret;
 581 }
 582
 583 constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
 584 {
 585   constraintList_elements_private (c, el)
 586     {
 587       el = constraint_togglePost(el);
 588       if (constraint_hasOrig(el) )
 589         {
 590           el = constraint_togglePostOrig (el);
 591         }
 592     }
 593   end_constraintList_elements_private;
 594   return c;
 595 }
 596
 597 /*@only@*/ constraintList constraintList_undump (FILE *f)
 598 {
 599   constraintList ret;
 600   char *s;
 601   char *os;
 602
 603   ret = constraintList_makeNew();
 604
 605   os =  mstring_create (MAX_DUMP_LINE_LENGTH);
 606   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 607
 608   while (s != NULL && *s != ';')
 609     {
 610       constraint temp;
 611       char * c;
 612
 613       c =  reader_getWord(&s);
 614
 615       if (! mstring_isDefined(c) )
 616         {
 617           llfatalbug(message("Library file is corrupted") );
 618         }
 619
 620
 621       if (strcmp (c, "C") != 0)
 622         {
 623           llfatalbug(message("Error reading library.  File may be corrupted"));
 624         }
 625
 626       temp = constraint_undump (f);
 627       ret = constraintList_add (ret, temp);
 628       s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 629       free(c);
 630     }
 631   free(s);
 632
 633   return ret;
 634 }
 635
 636
 637 void constraintList_dump (/*@observer@*/ constraintList c,  FILE *f)
 638 {
 639   constraintList_elements (c, el)
 640     {
 641       fprintf(f, "C\n");
 642       constraint_dump (el, f);
 643     }
 644   end_constraintList_elements; ;
 645 }
 646
 647
 648 constraintList constraintList_sort (/*@returned@*/ constraintList ret)
 649 {
 650   if (constraintList_isUndefined(ret) )
 651     {
 652       llassert(FALSE);
 653       return ret;
 654     }
 655   qsort (ret->elements, (size_t) ret->nelements,
 656          (sizeof (*ret->elements)),
 657          (int (*)(const void *, const void *)) constraint_compare);
 658
 659   DPRINTF((message("onstraint_sort returning") ));
 660   return ret;
 661 }
 662
 663