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 "llbasic.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   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_BOUNDSWRITE, loc) )
 181         {
 182           DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q",
 183                              constraint_unparse(elem))));
 184           constraint_free(elem);
 185         }
 186
 187       else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc))
 188         {
 189           DPRINTF ((message("constraintList_removeSurpressed getting rid of surpressed constraint %q",
 190                             constraint_unparse(elem))));
 191           constraint_free(elem);
 192         }
 193       else
 194         {
 195           ret = constraintList_add (ret, elem);
 196         }
 197       fileloc_free(loc);
 198     }
 199   end_constraintList_elements_private_only;
 200
 201   constraintList_freeShallow(s);
 202
 203   return ret;
 204 }
 205
 206 # if 0
 207 static /*@only@*/ cstring
 208 constraintList_unparseLocation (/*@temp@*/ constraintList s) /*@*/
 209 {
 210   int i;
 211   cstring st = cstring_undefined;
 212   bool first = TRUE;
 213
 214   if (!constraintList_isDefined (s))
 215     {
 216       return cstring_makeLiteral ("<undefined>");
 217     }
 218
 219   if (s->nelements == 0)
 220     {
 221       st = cstring_makeLiteral("<List Empty>");
 222       return st;
 223     }
 224
 225   for (i = 0; i < s->nelements; i++)
 226     {
 227       cstring type = cstring_undefined;
 228       constraint current = s->elements[i];
 229
 230       if (constraint_isDefined(current) )
 231         {
 232           cstring temp1;
 233               temp1 = constraint_unparseLocation(current);
 234           type = message ("%q %q\n", type, temp1 );
 235         }
 236
 237       if (first)
 238         {
 239           st = type;
 240           first = FALSE;
 241         }
 242       else
 243         {
 244           st = message ("%q, %q", st, type);
 245         }
 246     }
 247
 248   return st;
 249 }
 250 # endif
 251
 252 /*@only@*/ cstring
 253 constraintList_unparse (/*@temp@*/ constraintList s) /*@*/
 254 {
 255   int i;
 256   cstring st = cstring_undefined;
 257   bool first = TRUE;
 258
 259   if (!constraintList_isDefined (s))
 260     {
 261       return cstring_makeLiteral ("<undefined>");
 262     }
 263
 264   if (s->nelements == 0)
 265     {
 266       st = cstring_makeLiteral("<List Empty>");
 267       return st;
 268     }
 269
 270   for (i = 0; i < s->nelements; i++)
 271     {
 272       cstring type = cstring_undefined;
 273       constraint current = s->elements[i];
 274
 275       if (constraint_isDefined(current) )
 276         {
 277           cstring temp1;
 278
 279           if (context_getFlag (FLG_ORCONSTRAINT))
 280             {
 281               temp1 = constraint_unparseOr(current);
 282             }
 283           else
 284             {
 285               temp1 = constraint_unparse (current);
 286             }
 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_unparseErrorPostConditions (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_unparseError (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_unparseDetailed (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_unparseDetailed (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_unparse(l1),
 390                       constraintList_unparse(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   if (constraintList_isDefined (s))
 436     {
 437       int i;
 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
 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_unparse (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_unparse (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_unparse(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 Commenting out because function is not yet stable
 527
 528 / *@only@* / constraintList constraintList_doSRefFixStructConstraint(constraintList invars, sRef s, ctype ct )
 529 {
 530   constraintList ret;
 531   ret = constraintList_makeNew();
 532
 533   constraintList_elements (invars, el)
 534     {
 535       ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) );
 536     }
 537   end_constraintList_elements;
 538
 539   / *  constraintList_free (invars);* /
 540
 541   return ret;
 542 }
 543 */
 544
 545 /*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
 546 {
 547   constraintList ret;
 548   ret = constraintList_makeNew();
 549
 550   constraintList_elements (preconditions, el)
 551     {
 552       ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
 553     }
 554   end_constraintList_elements;
 555
 556   constraintList_free (preconditions);
 557
 558   return ret;
 559 }
 560 constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
 561                                                    exprNodeList arglist)
 562 {
 563   constraintList ret;
 564   constraint temp;
 565   ret = constraintList_makeNew();
 566
 567   constraintList_elements (preconditions, el)
 568     {
 569       temp = constraint_copy(el);
 570       ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
 571     }
 572   end_constraintList_elements;
 573
 574   return ret;
 575 }
 576
 577 constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
 578 {
 579   constraintList_elements_private (c, el)
 580     {
 581       el = constraint_togglePost(el);
 582       if (constraint_hasOrig(el) )
 583         {
 584           el = constraint_togglePostOrig (el);
 585         }
 586     }
 587   end_constraintList_elements_private;
 588   return c;
 589 }
 590
 591 /*@only@*/ constraintList constraintList_undump (FILE *f)
 592 {
 593   constraintList ret;
 594   char *s;
 595   char *os;
 596
 597   ret = constraintList_makeNew();
 598
 599   os =  mstring_create (MAX_DUMP_LINE_LENGTH);
 600   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 601
 602   while (s != NULL && *s != ';')
 603     {
 604       constraint temp;
 605       char * c;
 606
 607       c =  reader_getWord(&s);
 608
 609       if (! mstring_isDefined(c) )
 610         {
 611           llfatalbug(message("Library file is corrupted") );
 612         }
 613
 614
 615       if (strcmp (c, "C") != 0)
 616         {
 617           llfatalbug(message("Error reading library.  File may be corrupted"));
 618         }
 619
 620       temp = constraint_undump (f);
 621       ret = constraintList_add (ret, temp);
 622       s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 623       free(c);
 624     }
 625   free(s);
 626
 627   return ret;
 628 }
 629
 630
 631 void constraintList_dump (/*@observer@*/ constraintList c,  FILE *f)
 632 {
 633   constraintList_elements (c, el)
 634     {
 635       fprintf(f, "C\n");
 636       constraint_dump (el, f);
 637     }
 638   end_constraintList_elements; ;
 639 }
 640
 641
 642 constraintList constraintList_sort (/*@returned@*/ constraintList ret)
 643 {
 644   if (constraintList_isUndefined(ret) )
 645     {
 646       llassert(FALSE);
 647       return ret;
 648     }
 649   qsort (ret->elements, (size_t) ret->nelements,
 650          (sizeof (*ret->elements)),
 651          (int (*)(const void *, const void *)) constraint_compare);
 652
 653   DPRINTF((message("onstraint_sort returning") ));
 654   return ret;
 655 }
 656
 657