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 /*
  26 ** constraintList.c
  27 **
  28 ** based on list_template.c
  29 **
  30 ** where T has T_equal (or change this) and T_unparse
  31 */
  32
  33 # include "lclintMacros.nf"
  34 # include "llbasic.h"
  35
  36
  37 /*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
  38 # define constraintList_elements_private_only(x, m_el) \
  39    { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
  40      for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  41        { constraint m_el = *(m_elements++);
  42
  43 # define end_constraintList_elements_private_only }}}
  44
  45
  46 /*@iter constraintList_elements_private (sef constraintList x, yield  constraint el); @*/
  47 # define constraintList_elements_private(x, m_el) \
  48    { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
  49      for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  50        { constraint m_el = *(m_elements++);
  51
  52 # define end_constraintList_elements_private }}}
  53
  54
  55 /*@only@*/ constraintList constraintList_makeNew ()
  56 {
  57   constraintList s = (constraintList) dmalloc (sizeof (*s));
  58
  59   s->nelements = 0;
  60   s->nspace = constraintListBASESIZE;
  61   s->elements = (constraint *)
  62     dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
  63
  64   return (s);
  65 }
  66
  67 static void
  68 constraintList_grow (constraintList s)
  69 {
  70   int i;
  71   constraint *newelements;
  72
  73   llassert (constraintList_isDefined (s));
  74
  75   s->nspace += constraintListBASESIZE;
  76   newelements = (constraint *) dmalloc (sizeof (*newelements)
  77                                      * (s->nelements + s->nspace));
  78
  79   for (i = 0; i < s->nelements; i++)
  80     {
  81       newelements[i] = s->elements[i];
  82     }
  83
  84   sfree (s->elements);
  85   s->elements = newelements;
  86 }
  87
  88
  89 constraintList
  90 constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
  91 {
  92   llassert (constraintList_isDefined (s));
  93
  94   /*drl7x */
  95
  96   if (constraintList_resolve (el, s) )
  97     {
  98       constraint_free (el);
  99       return s;
 100     }
 101
 102   if (s->nspace <= 0)
 103     constraintList_grow (s);
 104
 105   s->nspace--;
 106   s->elements[s->nelements] = el;
 107   s->nelements++;
 108   return s;
 109 }
 110
 111 /* frees everything but actual constraints */
 112 /* This function should only be used if you have
 113    other references to unshared constraints
 114 */
 115 static void constraintList_freeShallow (/*@only@*/ constraintList c)
 116 {
 117   if (constraintList_isDefined(c) )
 118     {
 119       free (c->elements);
 120       c->elements = NULL;
 121       c->nelements = -1;
 122       c->nspace = -1;
 123     }
 124   free (c);
 125   c = NULL;
 126 }
 127
 128 /*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ constraintList newList)
 129 {
 130   llassert(constraintList_isDefined(s) );
 131   llassert(constraintList_isDefined(newList) );
 132
 133   if (newList == constraintList_undefined)
 134     return s;
 135
 136   constraintList_elements (newList, elem)
 137     {
 138     s = constraintList_add (s, constraint_copy(elem) );
 139     }
 140   end_constraintList_elements;
 141
 142   return s;
 143 }
 144
 145 constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
 146 {
 147   llassert(constraintList_isDefined(s) );
 148   llassert(constraintList_isDefined(newList) );
 149
 150   if (constraintList_isUndefined(newList) )
 151     return s;
 152
 153   constraintList_elements_private_only(newList, elem)
 154     {
 155     s = constraintList_add (s, elem);
 156     }
 157   end_constraintList_elements_private_only
 158
 159     constraintList_freeShallow(newList);
 160     return s;
 161 }
 162
 163
 164 constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s)
 165 {
 166   constraintList ret;
 167   fileloc loc;
 168   llassert(constraintList_isDefined(s) );
 169
 170   ret = constraintList_makeNew();
 171
 172   constraintList_elements_private_only(s, elem)
 173     {
 174       loc = constraint_getFileloc(elem);
 175
 176       if(fileloc_isUndefined(loc) )
 177         {
 178           ret = constraintList_add (ret, elem);
 179         }
 180
 181       else if (context_suppressFlagMsg(FLG_ARRAYBOUNDS, loc) )
 182         {
 183           DPRINTF(( message("constraintList_removeSurpressed getting rid of surpressed constraint %q", constraint_print(elem) ) ));
 184           constraint_free(elem);
 185         }
 186
 187       else if ( (! constraint_hasMaxSet(elem) ) && context_suppressFlagMsg(FLG_ARRAYBOUNDSREAD, loc) )
 188         {
 189           DPRINTF(( message("constraintList_removeSurpressed getting rid of surpressed constraint %q", constraint_print(elem) ) ));
 190           constraint_free(elem);
 191         }
 192       else
 193         {
 194           ret = constraintList_add (ret, elem);
 195         }
 196       fileloc_free(loc);
 197     }
 198   end_constraintList_elements_private_only;
 199
 200   constraintList_freeShallow(s);
 201
 202   return ret;
 203 }
 204
 205
 206 extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList s) /*@*/
 207 {
 208   return (constraintList_print(s));
 209 }
 210
 211 # if 0
 212 static /*@only@*/ cstring
 213 constraintList_printLocation (/*@temp@*/ constraintList s) /*@*/
 214 {
 215   int i;
 216   cstring st = cstring_undefined;
 217   bool first = TRUE;
 218
 219   if (!constraintList_isDefined (s))
 220     {
 221       return cstring_makeLiteral ("<undefined>");
 222     }
 223
 224   if (s->nelements == 0)
 225     {
 226       st = cstring_makeLiteral("<List Empty>");
 227       return st;
 228     }
 229
 230   for (i = 0; i < s->nelements; i++)
 231     {
 232       cstring type = cstring_undefined;
 233       constraint current = s->elements[i];
 234
 235       if (constraint_isDefined(current) )
 236         {
 237           cstring temp1;
 238               temp1 = constraint_printLocation(current);
 239           type = message ("%q %q\n", type, temp1 );
 240         }
 241
 242       if (first)
 243         {
 244           st = type;
 245           first = FALSE;
 246         }
 247       else
 248         {
 249           st = message ("%q, %q", st, type);
 250         }
 251     }
 252
 253   return st;
 254 }
 255 # endif
 256
 257 /*@only@*/ cstring
 258 constraintList_print (/*@temp@*/ constraintList s) /*@*/
 259 {
 260   int i;
 261   cstring st = cstring_undefined;
 262   bool first = TRUE;
 263
 264   if (!constraintList_isDefined (s))
 265     {
 266       return cstring_makeLiteral ("<undefined>");
 267     }
 268
 269   if (s->nelements == 0)
 270     {
 271       st = cstring_makeLiteral("<List Empty>");
 272       return st;
 273     }
 274
 275   for (i = 0; i < s->nelements; i++)
 276     {
 277       cstring type = cstring_undefined;
 278       constraint current = s->elements[i];
 279
 280       if (constraint_isDefined(current) )
 281         {
 282           cstring temp1;
 283             if ( context_getFlag (FLG_ORCONSTRAINT) )
 284               temp1 = constraint_printOr(current);
 285             else
 286               temp1 = constraint_print(current);
 287           type = message ("%q %q\n", type, temp1 );
 288         }
 289
 290       if (first)
 291         {
 292           st = type;
 293           first = FALSE;
 294         }
 295       else
 296         {
 297           st = message ("%q, %q", st, type);
 298         }
 299     }
 300
 301   return st;
 302 }
 303
 304 void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
 305 {
 306
 307   constraintList_elements (s, elem)
 308     {
 309       if (constraint_isDefined(elem))
 310         {
 311           constraint_printErrorPostCondition (elem, loc);
 312         }
 313     }
 314   end_constraintList_elements;
 315   return;
 316 }
 317
 318 void constraintList_printError (constraintList s, fileloc loc)
 319 {
 320
 321   constraintList_elements (s, elem)
 322     {
 323       if (constraint_isDefined(elem) )
 324         {
 325           if (constraint_isPost(elem) )
 326             constraint_printErrorPostCondition (elem, loc);
 327           else
 328             constraint_printError (elem, loc);
 329         }
 330     }
 331   end_constraintList_elements;
 332   return;
 333 }
 334
 335
 336 cstring
 337 constraintList_printDetailed (constraintList s)
 338 {
 339   int i;
 340   cstring st = cstring_undefined;
 341   bool first = TRUE;
 342
 343   if (!constraintList_isDefined (s))
 344     {
 345       return cstring_makeLiteral ("<undefined>");
 346     }
 347
 348   if (s->nelements == 0)
 349     {
 350       st = cstring_makeLiteral("<List Empty>");
 351       return st;
 352     }
 353
 354   for (i = 0; i < s->nelements; i++)
 355     {
 356       cstring type = cstring_undefined;
 357       constraint current = s->elements[i];
 358
 359       if (constraint_isDefined(current ) )
 360         {
 361           cstring temp1 = constraint_printDetailed (current);
 362           type = message ("%s %s\n", type, temp1 );
 363           cstring_free(temp1);
 364         }
 365
 366       if (first)
 367         {
 368           st = type;
 369           first = FALSE;
 370           type = NULL;
 371         }
 372       else
 373         {
 374           st = message ("%q %q", st, type);
 375         }
 376     }
 377   return st;
 378 }
 379
 380 /*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
 381 } */
 382
 383 constraintList
 384 constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
 385 {
 386   constraint temp;
 387   constraintList ret;
 388   DPRINTF ( (message ("Logical or on %s and %s",
 389                       constraintList_print(l1),
 390                       constraintList_print(l2)) ) );
 391
 392   ret = constraintList_makeNew();
 393   constraintList_elements (l1, el)
 394     {
 395       temp = constraint_substitute (el, l2);
 396
 397       if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
 398         {   /*avoid redundant constraints*/
 399           if (!constraintList_resolve (el, ret) )
 400             {
 401               constraint temp2;
 402               temp2 = constraint_copy(el);
 403               ret = constraintList_add (ret, temp2);
 404             }
 405         }
 406       constraint_free(temp);
 407     }
 408   end_constraintList_elements;
 409
 410    constraintList_elements (l2, el)
 411     {
 412       temp = constraint_substitute (el, l1);
 413
 414       if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
 415         {
 416           /*avoid redundant constraints*/
 417           if (!constraintList_resolve (el, ret) )
 418             {
 419               constraint temp2;
 420               temp2 = constraint_copy(el);
 421               ret = constraintList_add (ret, temp2);
 422             }
 423         }
 424       constraint_free(temp);
 425     }
 426   end_constraintList_elements;
 427
 428
 429   return ret;
 430 }
 431
 432 void
 433 constraintList_free (/*@only@*/ constraintList s)
 434 {
 435   int i;
 436
 437   llassert(constraintList_isDefined(s) );
 438
 439
 440   for (i = 0; i < s->nelements; i++)
 441     {
 442       constraint_free (s->elements[i]);
 443     }
 444
 445   sfree (s->elements);
 446   s->elements = NULL;
 447   s->nelements = -1;
 448   s->nspace = -1;
 449   sfree (s);
 450   s = NULL;
 451 }
 452
 453 constraintList
 454 constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
 455 {
 456   constraintList ret = constraintList_makeNew ();
 457
 458   constraintList_elements (s, el)
 459     {
 460       ret = constraintList_add (ret, constraint_copy (el));
 461     } end_constraintList_elements;
 462
 463   return ret;
 464 }
 465
 466 constraintList constraintList_preserveOrig (constraintList c)
 467 {
 468   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 469
 470   constraintList_elements_private (c, el)
 471   {
 472     el = constraint_preserveOrig (el);
 473   }
 474   end_constraintList_elements_private;
 475   return c;
 476 }
 477
 478 constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/  exprNode fcn)
 479 {
 480   DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_print (c) ) ));
 481
 482   constraintList_elements_private (c, el)
 483   {
 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