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