src/constraintList.c

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