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