src/constraintList.c

   1 /*
   2 ** LCLint - 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://lclint.cs.virginia.edu
  23 */
  24 /*
  25 ** constraintList.c
  26 **
  27 ** based on list_template.c
  28 **
  29 ** where T has T_equal (or change this) and T_unparse
  30 */
  31
  32 # include "lclintMacros.nf"
  33 # include "llbasic.h"
  34
  35
  36 /*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
  37 # define constraintList_elements_private_only(x, m_el) \
  38    { 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    { 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 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   s->nspace += constraintListBASESIZE;
  73   newelements = (constraint *) dmalloc (sizeof (*newelements)
  74                                      * (s->nelements + s->nspace));
  75
  76   for (i = 0; i < s->nelements; i++)
  77     {
  78       newelements[i] = s->elements[i];
  79     }
  80
  81   sfree (s->elements);
  82   s->elements = newelements;
  83 }
  84
  85
  86 constraintList
  87 constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
  88 {
  89   /*drl7x */
  90   //   el = constraint_simplify (el);
  91   if (constraintList_resolve (el, s) )
  92     {
  93       constraint_free (el);
  94       return s;
  95     }
  96
  97   if (s->nspace <= 0)
  98     constraintList_grow (s);
  99
 100   s->nspace--;
 101   s->elements[s->nelements] = el;
 102   s->nelements++;
 103   return s;
 104 }
 105
 106 /* frees everything but actual constraints */
 107 /* This function should only be used if you have
 108    other references to unshared constraints
 109 */
 110 static void constraintList_freeShallow (/*@only@*/ constraintList c)
 111 {
 112   if (constraintList_isDefined(c) )
 113     {
 114       free (c->elements);
 115       c->elements = NULL;
 116       c->nelements = -1;
 117       c->nspace = -1;
 118     }
 119   free (c);
 120   c = NULL;
 121 }
 122
 123 /*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ constraintList newList)
 124 {
 125   llassert(constraintList_isDefined(s) );
 126   llassert(constraintList_isDefined(newList) );
 127
 128   if (newList == constraintList_undefined)
 129     return s;
 130
 131   constraintList_elements (newList, elem)
 132     {
 133     s = constraintList_add (s, constraint_copy(elem) );
 134     }
 135   end_constraintList_elements;
 136
 137   return s;
 138 }
 139
 140 constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
 141 {
 142   llassert(constraintList_isDefined(s) );
 143   llassert(constraintList_isDefined(newList) );
 144
 145   if (constraintList_isUndefined(newList) )
 146     return s;
 147
 148   constraintList_elements_private_only(newList, elem)
 149     {
 150     s = constraintList_add (s, elem);
 151     }
 152   end_constraintList_elements_private_only
 153
 154     constraintList_freeShallow(newList);
 155     return s;
 156 }
 157
 158
 159 extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList s) /*@*/
 160 {
 161   return (constraintList_print(s));
 162
 163
 164 }
 165
 166
 167 /*@only@*/ cstring
 168 constraintList_print (/*@temp@*/ constraintList s) /*@*/
 169 {
 170   int i;
 171   cstring st = cstring_undefined;
 172   bool first = TRUE;
 173
 174   if (s->nelements == 0)
 175     {
 176       st = cstring_makeLiteral("<List Empty>");
 177       return st;
 178     }
 179
 180   for (i = 0; i < s->nelements; i++)
 181     {
 182       cstring type = cstring_undefined;
 183       constraint current = s->elements[i];
 184
 185       if (constraint_isDefined(current) )
 186         {
 187           cstring temp1;
 188             if ( context_getFlag (FLG_ORCONSTRAINT) )
 189               temp1 = constraint_printOr(current);
 190             else
 191               temp1 = constraint_print(current);
 192           type = message ("%q %q\n", type, temp1 );
 193         }
 194
 195       if (first)
 196         {
 197           st = type;
 198           first = FALSE;
 199         }
 200       else
 201         {
 202           st = message ("%q, %q", st, type);
 203         }
 204     } //end for
 205
 206   return st;
 207 }
 208
 209 void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
 210 {
 211
 212   constraintList_elements (s, elem)
 213     {
 214       if (constraint_isDefined(elem))
 215         {
 216           constraint_printErrorPostCondition (elem, loc);
 217         }
 218     }
 219   end_constraintList_elements;
 220   return;
 221 }
 222
 223 void constraintList_printError (constraintList s, fileloc loc)
 224 {
 225
 226   constraintList_elements (s, elem)
 227     {
 228       if (constraint_isDefined(elem) )
 229         {
 230           constraint_printError (elem, loc);
 231         }
 232     }
 233   end_constraintList_elements;
 234   return;
 235 }
 236
 237
 238 cstring
 239 constraintList_printDetailed (constraintList s)
 240 {
 241   int i;
 242   cstring st = cstring_undefined;
 243   bool first = TRUE;
 244
 245   if (s->nelements == 0)
 246     {
 247       st = cstring_makeLiteral("<List Empty>");
 248       return st;
 249     }
 250
 251   for (i = 0; i < s->nelements; i++)
 252     {
 253       cstring type = cstring_undefined;
 254       constraint current = s->elements[i];
 255
 256       if (constraint_isDefined(current ) )
 257         {
 258           cstring temp1 = constraint_printDetailed (current);
 259           type = message ("%s %s\n", type, temp1 );
 260           cstring_free(temp1);
 261         }
 262
 263       if (first)
 264         {
 265           st = type;
 266           first = FALSE;
 267           type = NULL;
 268         }
 269       else
 270         {
 271           st = message ("%q %q", st, type);
 272         }
 273     }
 274   return st;
 275 }
 276
 277 /*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
 278 } */
 279
 280 constraintList
 281 constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
 282 {
 283   constraint temp;
 284   constraintList ret;
 285   DPRINTF ( (message ("Logical or on %s and %s",
 286                       constraintList_print(l1),
 287                       constraintList_print(l2)) ) );
 288
 289   ret = constraintList_makeNew();
 290   constraintList_elements (l1, el)
 291     {
 292       temp = constraint_substitute (el, l2);
 293
 294       if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
 295         {   /*avoid redundant constraints*/
 296           if (!constraintList_resolve (el, ret) )
 297             {
 298               constraint temp2;
 299               temp2 = constraint_copy(el);
 300               ret = constraintList_add (ret, temp2);
 301             }
 302         }
 303       constraint_free(temp);
 304     }
 305   end_constraintList_elements;
 306
 307    constraintList_elements (l2, el)
 308     {
 309       temp = constraint_substitute (el, l1);
 310
 311       if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
 312         {
 313           /*avoid redundant constraints*/
 314           if (!constraintList_resolve (el, ret) )
 315             {
 316               constraint temp2;
 317               temp2 = constraint_copy(el);
 318               ret = constraintList_add (ret, temp2);
 319             }
 320         }
 321       constraint_free(temp);
 322     }
 323   end_constraintList_elements;
 324
 325
 326   return ret;
 327 }
 328
 329 void
 330 constraintList_free (/*@only@*/ constraintList s)
 331 {
 332   int i;
 333
 334   llassert(constraintList_isDefined(s) );
 335
 336
 337   for (i = 0; i < s->nelements; i++)
 338     {
 339       constraint_free (s->elements[i]);
 340     }
 341
 342   sfree (s->elements);
 343   s->elements = NULL;
 344   s->nelements = -1;
 345   s->nspace = -1;
 346   sfree (s);
 347   s = NULL;
 348 }
 349
 350 constraintList
 351 constraintList_copy (/*@oberserver@*/ /*@temp@*/ constraintList s)
 352 {
 353   constraintList ret = constraintList_makeNew ();
 354
 355   constraintList_elements (s, el)
 356     {
 357       ret = constraintList_add (ret, constraint_copy (el));
 358     } end_constraintList_elements;
 359
 360   return ret;
 361 }
 362
 363 constraintList constraintList_preserveOrig (constraintList c)
 364 {
 365   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 366
 367   constraintList_elements_private (c, el)
 368   {
 369     el = constraint_preserveOrig (el);
 370   }
 371   end_constraintList_elements_private;
 372   return c;
 373 }
 374
 375 constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@depenent@*/ /*@observer@*/  exprNode fcn)
 376 {
 377   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 378
 379   constraintList_elements_private (c, el)
 380   {
 381     //  el = constraint_preserveOrig (el);
 382     el = constraint_setFcnPre(el);
 383     el = constraint_origAddGeneratingExpr (el, fcn);
 384   }
 385   end_constraintList_elements_private;
 386   return c;
 387 }
 388
 389
 390
 391 constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e)
 392 {
 393   DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
 394
 395   constraintList_elements_private (c, el)
 396   {
 397     DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) )  ));
 398     el = constraint_addGeneratingExpr (el, e);
 399   }
 400   end_constraintList_elements_private;
 401   return c;
 402 }
 403
 404 /*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
 405 {
 406   constraintList ret;
 407   ret = constraintList_makeNew();
 408   constraintList_elements_private (postconditions, el)
 409     {
 410       ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
 411     }
 412   end_constraintList_elements_private;
 413
 414   constraintList_free(postconditions);
 415   return ret;
 416 }
 417
 418 /*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
 419 {
 420   constraintList ret;
 421   ret = constraintList_makeNew();
 422
 423   constraintList_elements (preconditions, el)
 424     {
 425       ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
 426     }
 427   end_constraintList_elements;
 428
 429   constraintList_free (preconditions);
 430
 431   return ret;
 432 }
 433 constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
 434                                                    exprNodeList arglist)
 435 {
 436   constraintList ret;
 437   constraint temp;
 438   ret = constraintList_makeNew();
 439
 440   constraintList_elements (preconditions, el)
 441     {
 442       temp = constraint_copy(el);
 443       ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
 444     }
 445   end_constraintList_elements;
 446
 447   return ret;
 448 }
 449
 450 constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
 451 {
 452   constraintList_elements_private (c, el)
 453     {
 454       el = constraint_togglePost(el);
 455       if (constraint_hasOrig(el) )
 456         {
 457           el = constraint_togglePostOrig (el);
 458         }
 459     }
 460   end_constraintList_elements_private;
 461   return c;
 462 }
 463
 464 /*@only@*/ constraintList constraintList_undump (FILE *f)
 465 {
 466   constraintList ret;
 467   char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
 468   char *os;
 469
 470   ret = constraintList_makeNew();
 471
 472   os = s;
 473   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 474
 475   while (s != NULL && *s != ';')
 476     {
 477       constraint temp;
 478       char * c;
 479
 480       c =  reader_getWord(&s);
 481
 482       if (strcmp (c, "C") != 0)
 483         {
 484           llfatalbug(message("Error reading library.  File may be corrupted"));
 485         }
 486
 487       temp = constraint_undump (f);
 488       ret = constraintList_add (ret, temp);
 489       s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 490       free(c);
 491     }
 492   free(s);
 493
 494   return ret;
 495 }
 496
 497
 498 void constraintList_dump (/*@observer@*/ constraintList c,  FILE *f)
 499 {
 500   constraintList_elements (c, el)
 501     {
 502       fprintf(f, "C\n");
 503       constraint_dump (el, f);
 504     }
 505   end_constraintList_elements; ;
 506 }
 507
 508