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    { 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 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   //   el = constraint_simplify (el);
  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@*/ 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 extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList s) /*@*/
 164 {
 165   return (constraintList_print(s));
 166
 167
 168 }
 169
 170
 171 /*@only@*/ cstring
 172 constraintList_print (/*@temp@*/ constraintList s) /*@*/
 173 {
 174   int i;
 175   cstring st = cstring_undefined;
 176   bool first = TRUE;
 177
 178   if (!constraintList_isDefined (s))
 179     {
 180       return cstring_makeLiteral ("<undefined>");
 181     }
 182
 183   if (s->nelements == 0)
 184     {
 185       st = cstring_makeLiteral("<List Empty>");
 186       return st;
 187     }
 188
 189   for (i = 0; i < s->nelements; i++)
 190     {
 191       cstring type = cstring_undefined;
 192       constraint current = s->elements[i];
 193
 194       if (constraint_isDefined(current) )
 195         {
 196           cstring temp1;
 197             if ( context_getFlag (FLG_ORCONSTRAINT) )
 198               temp1 = constraint_printOr(current);
 199             else
 200               temp1 = constraint_print(current);
 201           type = message ("%q %q\n", type, temp1 );
 202         }
 203
 204       if (first)
 205         {
 206           st = type;
 207           first = FALSE;
 208         }
 209       else
 210         {
 211           st = message ("%q, %q", st, type);
 212         }
 213     } //end for
 214
 215   return st;
 216 }
 217
 218 void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
 219 {
 220
 221   constraintList_elements (s, elem)
 222     {
 223       if (constraint_isDefined(elem))
 224         {
 225           constraint_printErrorPostCondition (elem, loc);
 226         }
 227     }
 228   end_constraintList_elements;
 229   return;
 230 }
 231
 232 void constraintList_printError (constraintList s, fileloc loc)
 233 {
 234
 235   constraintList_elements (s, elem)
 236     {
 237       if (constraint_isDefined(elem) )
 238         {
 239           constraint_printError (elem, loc);
 240         }
 241     }
 242   end_constraintList_elements;
 243   return;
 244 }
 245
 246
 247 cstring
 248 constraintList_printDetailed (constraintList s)
 249 {
 250   int i;
 251   cstring st = cstring_undefined;
 252   bool first = TRUE;
 253
 254   if (!constraintList_isDefined (s))
 255     {
 256       return cstring_makeLiteral ("<undefined>");
 257     }
 258
 259   if (s->nelements == 0)
 260     {
 261       st = cstring_makeLiteral("<List Empty>");
 262       return st;
 263     }
 264
 265   for (i = 0; i < s->nelements; i++)
 266     {
 267       cstring type = cstring_undefined;
 268       constraint current = s->elements[i];
 269
 270       if (constraint_isDefined(current ) )
 271         {
 272           cstring temp1 = constraint_printDetailed (current);
 273           type = message ("%s %s\n", type, temp1 );
 274           cstring_free(temp1);
 275         }
 276
 277       if (first)
 278         {
 279           st = type;
 280           first = FALSE;
 281           type = NULL;
 282         }
 283       else
 284         {
 285           st = message ("%q %q", st, type);
 286         }
 287     }
 288   return st;
 289 }
 290
 291 /*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
 292 } */
 293
 294 constraintList
 295 constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
 296 {
 297   constraint temp;
 298   constraintList ret;
 299   DPRINTF ( (message ("Logical or on %s and %s",
 300                       constraintList_print(l1),
 301                       constraintList_print(l2)) ) );
 302
 303   ret = constraintList_makeNew();
 304   constraintList_elements (l1, el)
 305     {
 306       temp = constraint_substitute (el, l2);
 307
 308       if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
 309         {   /*avoid redundant constraints*/
 310           if (!constraintList_resolve (el, ret) )
 311             {
 312               constraint temp2;
 313               temp2 = constraint_copy(el);
 314               ret = constraintList_add (ret, temp2);
 315             }
 316         }
 317       constraint_free(temp);
 318     }
 319   end_constraintList_elements;
 320
 321    constraintList_elements (l2, el)
 322     {
 323       temp = constraint_substitute (el, l1);
 324
 325       if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
 326         {
 327           /*avoid redundant constraints*/
 328           if (!constraintList_resolve (el, ret) )
 329             {
 330               constraint temp2;
 331               temp2 = constraint_copy(el);
 332               ret = constraintList_add (ret, temp2);
 333             }
 334         }
 335       constraint_free(temp);
 336     }
 337   end_constraintList_elements;
 338
 339
 340   return ret;
 341 }
 342
 343 void
 344 constraintList_free (/*@only@*/ constraintList s)
 345 {
 346   int i;
 347
 348   llassert(constraintList_isDefined(s) );
 349
 350
 351   for (i = 0; i < s->nelements; i++)
 352     {
 353       constraint_free (s->elements[i]);
 354     }
 355
 356   sfree (s->elements);
 357   s->elements = NULL;
 358   s->nelements = -1;
 359   s->nspace = -1;
 360   sfree (s);
 361   s = NULL;
 362 }
 363
 364 constraintList
 365 constraintList_copy (/*@oberserver@*/ /*@temp@*/ constraintList s)
 366 {
 367   constraintList ret = constraintList_makeNew ();
 368
 369   constraintList_elements (s, el)
 370     {
 371       ret = constraintList_add (ret, constraint_copy (el));
 372     } end_constraintList_elements;
 373
 374   return ret;
 375 }
 376
 377 constraintList constraintList_preserveOrig (constraintList c)
 378 {
 379   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 380
 381   constraintList_elements_private (c, el)
 382   {
 383     el = constraint_preserveOrig (el);
 384   }
 385   end_constraintList_elements_private;
 386   return c;
 387 }
 388
 389 constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@depenent@*/ /*@observer@*/  exprNode fcn)
 390 {
 391   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 392
 393   constraintList_elements_private (c, el)
 394   {
 395     //  el = constraint_preserveOrig (el);
 396     el = constraint_setFcnPre(el);
 397     el = constraint_origAddGeneratingExpr (el, fcn);
 398   }
 399   end_constraintList_elements_private;
 400   return c;
 401 }
 402
 403
 404
 405 constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e)
 406 {
 407   DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
 408
 409   constraintList_elements_private (c, el)
 410   {
 411     DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) )  ));
 412     el = constraint_addGeneratingExpr (el, e);
 413   }
 414   end_constraintList_elements_private;
 415   return c;
 416 }
 417
 418 /*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
 419 {
 420   constraintList ret;
 421   ret = constraintList_makeNew();
 422   constraintList_elements_private (postconditions, el)
 423     {
 424       ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
 425     }
 426   end_constraintList_elements_private;
 427
 428   constraintList_free(postconditions);
 429   return ret;
 430 }
 431
 432 /*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
 433 {
 434   constraintList ret;
 435   ret = constraintList_makeNew();
 436
 437   constraintList_elements (preconditions, el)
 438     {
 439       ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
 440     }
 441   end_constraintList_elements;
 442
 443   constraintList_free (preconditions);
 444
 445   return ret;
 446 }
 447 constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
 448                                                    exprNodeList arglist)
 449 {
 450   constraintList ret;
 451   constraint temp;
 452   ret = constraintList_makeNew();
 453
 454   constraintList_elements (preconditions, el)
 455     {
 456       temp = constraint_copy(el);
 457       ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
 458     }
 459   end_constraintList_elements;
 460
 461   return ret;
 462 }
 463
 464 constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
 465 {
 466   constraintList_elements_private (c, el)
 467     {
 468       el = constraint_togglePost(el);
 469       if (constraint_hasOrig(el) )
 470         {
 471           el = constraint_togglePostOrig (el);
 472         }
 473     }
 474   end_constraintList_elements_private;
 475   return c;
 476 }
 477
 478 /*@only@*/ constraintList constraintList_undump (FILE *f)
 479 {
 480   constraintList ret;
 481   char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
 482   char *os;
 483
 484   ret = constraintList_makeNew();
 485
 486   os = s;
 487   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 488
 489   while (s != NULL && *s != ';')
 490     {
 491       constraint temp;
 492       char * c;
 493
 494       c =  reader_getWord(&s);
 495
 496       if (strcmp (c, "C") != 0)
 497         {
 498           llfatalbug(message("Error reading library.  File may be corrupted"));
 499         }
 500
 501       temp = constraint_undump (f);
 502       ret = constraintList_add (ret, temp);
 503       s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 504       free(c);
 505     }
 506   free(s);
 507
 508   return ret;
 509 }
 510
 511
 512 void constraintList_dump (/*@observer@*/ constraintList c,  FILE *f)
 513 {
 514   constraintList_elements (c, el)
 515     {
 516       fprintf(f, "C\n");
 517       constraint_dump (el, f);
 518     }
 519   end_constraintList_elements; ;
 520 }
 521
 522