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