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