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