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
 132
 133 /*@only@*/ constraintList constraintList_addListFree (/*@only@*/ constraintList s, /*@only@*/ constraintList new)
 134 {
 135   llassert(constraintList_isDefined(s) );
 136   llassert(constraintList_isDefined(new) );
 137
 138   if (new == constraintList_undefined)
 139     return s;
 140
 141   constraintList_elements_private(new, elem)
 142     {
 143     s = constraintList_add (s, elem);
 144     }
 145   end_constraintList_elements_private
 146
 147     constraintList_freeShallow(new);
 148     return s;
 149 }
 150
 151 cstring
 152 constraintList_print (constraintList s) /*@*/
 153 {
 154   int i;
 155   cstring st = cstring_undefined;
 156   bool first = TRUE;
 157
 158   if (s->nelements == 0)
 159     {
 160       st = cstring_makeLiteral("<List Empty>");
 161       return st;
 162     }
 163
 164   for (i = 0; i < s->nelements; i++)
 165     {
 166       cstring type = cstring_undefined;
 167       constraint current = s->elements[i];
 168
 169       if (current != NULL)
 170         {
 171           cstring temp1;
 172             if ( context_getFlag (FLG_ORCONSTRAINT) )
 173               temp1 = constraint_printOr(current);
 174             else
 175               temp1 = constraint_print(current);
 176           type = message ("%q %q\n", type, temp1 );
 177         }
 178
 179       if (first)
 180         {
 181           st = type;
 182           first = FALSE;
 183         }
 184       else
 185         {
 186           st = message ("%q, %q", st, type);
 187         }
 188     } //end for
 189
 190   return st;
 191 }
 192
 193 void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
 194 {
 195
 196   constraintList_elements (s, elem)
 197     {
 198       if (elem != NULL)
 199         {
 200           constraint_printErrorPostCondition (elem, loc);
 201         }
 202     }
 203   end_constraintList_elements;
 204   return;
 205 }
 206
 207
 208 void constraintList_printError (constraintList s, fileloc loc)
 209 {
 210
 211   constraintList_elements (s, elem)
 212     {
 213       if (elem != NULL)
 214         {
 215           constraint_printError (elem, loc);
 216         }
 217     }
 218   end_constraintList_elements;
 219   return;
 220 }
 221
 222
 223 cstring
 224 constraintList_printDetailed (constraintList s)
 225 {
 226   int i;
 227   cstring st = cstring_undefined;
 228   bool first = TRUE;
 229
 230   if (s->nelements == 0)
 231     {
 232       st = cstring_makeLiteral("<List Empty>");
 233       return st;
 234     }
 235
 236   for (i = 0; i < s->nelements; i++)
 237     {
 238       cstring type = cstring_undefined;
 239       constraint current = s->elements[i];
 240
 241       if (current != NULL)
 242         {
 243           cstring temp1 = constraint_printDetailed (current);
 244           type = message ("%s %s\n", type, temp1 );
 245           cstring_free(temp1);
 246         }
 247
 248       if (first)
 249         {
 250           st = type;
 251           first = FALSE;
 252         }
 253       else
 254         {
 255           st = message ("%s %s", st, type);
 256         }
 257     }
 258   return st;
 259 }
 260
 261 /*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
 262 } */
 263
 264 constraintList
 265 constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
 266 {
 267   constraint temp;
 268   constraintList ret;
 269   DPRINTF ( (message ("Logical or on %s and %s",
 270                       constraintList_print(l1),
 271                       constraintList_print(l2)) ) );
 272
 273   ret = constraintList_makeNew();
 274   constraintList_elements (l1, el)
 275     {
 276       temp = substitute (el, l2);
 277
 278       if (resolve (el, l2) || resolve(temp,l2) )
 279         {   /*avoid redundant constraints*/
 280           if (!resolve (el, ret) )
 281             {
 282               constraint temp2;
 283               temp2 = constraint_copy(el);
 284               ret = constraintList_add (ret, temp2);
 285             }
 286         }
 287       constraint_free(temp);
 288     }
 289   end_constraintList_elements;
 290
 291    constraintList_elements (l2, el)
 292     {
 293       temp = substitute (el, l1);
 294
 295       if (resolve (el, l1) || resolve(temp,l1) )
 296         {
 297           /*avoid redundant constraints*/
 298           if (!resolve (el, ret) )
 299             {
 300               constraint temp2;
 301               temp2 = constraint_copy(el);
 302               ret = constraintList_add (ret, temp2);
 303             }
 304         }
 305       constraint_free(temp);
 306     }
 307   end_constraintList_elements;
 308
 309
 310   return ret;
 311 }
 312
 313 void
 314 constraintList_free (/*@only@*/ constraintList s)
 315 {
 316   int i;
 317
 318   llassert(constraintList_isDefined(s) );
 319
 320
 321   for (i = 0; i < s->nelements; i++)
 322     {
 323       constraint_free (s->elements[i]);
 324     }
 325
 326   sfree (s->elements);
 327   s->elements = NULL;
 328   s->nelements = -1;
 329   s->nspace = -1;
 330   sfree (s);
 331   s = NULL;
 332 }
 333
 334 constraintList
 335 constraintList_copy (constraintList s)
 336 {
 337   constraintList ret = constraintList_makeNew ();
 338
 339   constraintList_elements (s, el)
 340     {
 341       ret = constraintList_add (ret, constraint_copy (el));
 342     } end_constraintList_elements;
 343
 344   return ret;
 345 }
 346
 347 constraintList constraintList_preserveOrig (constraintList c)
 348 {
 349   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 350
 351   constraintList_elements_private (c, el)
 352   {
 353     el = constraint_preserveOrig (el);
 354   }
 355   end_constraintList_elements_private;
 356   return c;
 357 }
 358
 359 constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c, exprNode fcn)
 360 {
 361   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 362
 363   constraintList_elements_private (c, el)
 364   {
 365     //  el = constraint_preserveOrig (el);
 366     el = constraint_setFcnPre(el);
 367     el = constraint_origAddGeneratingExpr (el, fcn);
 368   }
 369   end_constraintList_elements_private;
 370   return c;
 371 }
 372
 373
 374
 375 constraintList constraintList_addGeneratingExpr (constraintList c, exprNode e)
 376 {
 377   DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
 378
 379   constraintList_elements_private (c, el)
 380   {
 381     DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) )  ));
 382     el = constraint_addGeneratingExpr (el, e);
 383   }
 384   end_constraintList_elements_private;
 385   return c;
 386 }
 387
 388 /*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
 389 {
 390   constraintList ret;
 391   ret = constraintList_makeNew();
 392   constraintList_elements_private (postconditions, el)
 393     {
 394       ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
 395     }
 396   end_constraintList_elements_private;
 397
 398   constraintList_free(postconditions);
 399   return ret;
 400 }
 401
 402 /*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, exprNodeList arglist)
 403 {
 404   constraintList ret;
 405   ret = constraintList_makeNew();
 406
 407   constraintList_elements (preconditions, el)
 408     {
 409       ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
 410     }
 411   end_constraintList_elements;
 412
 413   constraintList_free (preconditions);
 414
 415   return ret;
 416 }
 417 constraintList constraintList_doSRefFixBaseParam (/*@observer@*/ constraintList preconditions, /*@observer@*/
 418                                                    exprNodeList arglist)
 419 {
 420   constraintList ret;
 421   constraint temp;
 422   ret = constraintList_makeNew();
 423
 424   constraintList_elements (preconditions, el)
 425     {
 426       temp = constraint_copy(el);
 427       ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
 428     }
 429   end_constraintList_elements;
 430
 431   return ret;
 432 }
 433
 434 constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
 435 {
 436   constraintList_elements_private (c, el)
 437     {
 438       el = constraint_togglePost(el);
 439       if (el->orig)
 440         {
 441           el->orig = constraint_togglePost(el->orig);
 442         }
 443     }
 444   end_constraintList_elements_private;
 445   return c;
 446 }
 447
 448