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