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 /*@-nullderef@*/ /* !!! DRL needs to fix this code! */
  37 /*@-nullstate@*/ /* !!! DRL needs to fix this code! */
  38 /*@-nullpass@*/ /* !!! DRL needs to fix this code! */
  39 /*@-temptrans@*/ /* !!! DRL needs to fix this code! */
  40
  41 /*@iter constraintList_elements_private_only (sef constraintList x, yield only constraint el); @*/
  42 # define constraintList_elements_private_only(x, m_el) \
  43    { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
  44      for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  45        { constraint m_el = *(m_elements++);
  46
  47 # define end_constraintList_elements_private_only }}}
  48
  49
  50 /*@iter constraintList_elements_private (sef constraintList x, yield  constraint el); @*/
  51 # define constraintList_elements_private(x, m_el) \
  52    { if (constraintList_isDefined (x)) { int m_ind; constraint *m_elements = &((x)->elements[0]); \
  53      for (m_ind = 0 ; m_ind < (x)->nelements; m_ind++) \
  54        { constraint m_el = *(m_elements++);
  55
  56 # define end_constraintList_elements_private }}}
  57
  58
  59 /*@only@*/ constraintList constraintList_makeNew ()
  60 {
  61   constraintList s = (constraintList) dmalloc (sizeof (*s));
  62
  63   s->nelements = 0;
  64   s->nspace = constraintListBASESIZE;
  65   s->elements = (constraint *)
  66     dmalloc (sizeof (*s->elements) * constraintListBASESIZE);
  67
  68   return (s);
  69 }
  70
  71 static void
  72 constraintList_grow (constraintList s)
  73 {
  74   int i;
  75   constraint *newelements;
  76
  77   llassert (constraintList_isDefined (s));
  78
  79   s->nspace += constraintListBASESIZE;
  80   newelements = (constraint *) dmalloc (sizeof (*newelements)
  81                                      * (s->nelements + s->nspace));
  82
  83   for (i = 0; i < s->nelements; i++)
  84     {
  85       newelements[i] = s->elements[i];
  86     }
  87
  88   sfree (s->elements);
  89   s->elements = newelements;
  90 }
  91
  92
  93 constraintList
  94 constraintList_add (/*@returned@*/ constraintList s, /*@only@*/ constraint el)
  95 {
  96   llassert (constraintList_isDefined (s));
  97
  98   /*drl7x */
  99
 100   if (constraintList_resolve (el, s) )
 101     {
 102       constraint_free (el);
 103       return s;
 104     }
 105
 106   if (s->nspace <= 0)
 107     constraintList_grow (s);
 108
 109   s->nspace--;
 110   s->elements[s->nelements] = el;
 111   s->nelements++;
 112   return s;
 113 }
 114
 115 /* frees everything but actual constraints */
 116 /* This function should only be used if you have
 117    other references to unshared constraints
 118 */
 119 static void constraintList_freeShallow (/*@only@*/ constraintList c)
 120 {
 121   if (constraintList_isDefined(c) )
 122     {
 123       free (c->elements);
 124       c->elements = NULL;
 125       c->nelements = -1;
 126       c->nspace = -1;
 127     }
 128   free (c);
 129   c = NULL;
 130 }
 131
 132 /*@only@*/ constraintList constraintList_addList (/*@only@*/ /*@returned@*/ constraintList s, /*@observer@*/ /*@temp@*/ constraintList newList)
 133 {
 134   llassert(constraintList_isDefined(s) );
 135   llassert(constraintList_isDefined(newList) );
 136
 137   if (newList == constraintList_undefined)
 138     return s;
 139
 140   constraintList_elements (newList, elem)
 141     {
 142     s = constraintList_add (s, constraint_copy(elem) );
 143     }
 144   end_constraintList_elements;
 145
 146   return s;
 147 }
 148
 149 constraintList constraintList_addListFree (/*@returned@*/ constraintList s, /*@only@*/ constraintList newList)
 150 {
 151   llassert(constraintList_isDefined(s) );
 152   llassert(constraintList_isDefined(newList) );
 153
 154   if (constraintList_isUndefined(newList) )
 155     return s;
 156
 157   constraintList_elements_private_only(newList, elem)
 158     {
 159     s = constraintList_add (s, elem);
 160     }
 161   end_constraintList_elements_private_only
 162
 163     constraintList_freeShallow(newList);
 164     return s;
 165 }
 166
 167
 168 constraintList constraintList_removeSurpressed (/*@only@*/ constraintList s)
 169 {
 170   constraintList ret;
 171   fileloc loc;
 172   llassert(constraintList_isDefined(s) );
 173
 174   ret = constraintList_makeNew();
 175
 176   constraintList_elements_private_only(s, elem)
 177     {
 178       loc = constraint_getFileloc(elem);
 179
 180       if (fileloc_isUndefined(loc))
 181         {
 182           ret = constraintList_add (ret, elem);
 183         }
 184
 185       else if (context_suppressFlagMsg(FLG_BOUNDSWRITE, loc) )
 186         {
 187           DPRINTF ((message ("constraintList_removeSurpressed getting rid of surpressed constraint %q",
 188                              constraint_print(elem))));
 189           constraint_free(elem);
 190         }
 191
 192       else if (!constraint_hasMaxSet(elem) && context_suppressFlagMsg(FLG_BOUNDSREAD, loc))
 193         {
 194           DPRINTF ((message("constraintList_removeSurpressed getting rid of surpressed constraint %q",
 195                             constraint_print(elem))));
 196           constraint_free(elem);
 197         }
 198       else
 199         {
 200           ret = constraintList_add (ret, elem);
 201         }
 202       fileloc_free(loc);
 203     }
 204   end_constraintList_elements_private_only;
 205
 206   constraintList_freeShallow(s);
 207
 208   return ret;
 209 }
 210
 211
 212 extern /*@only@*/ cstring constraintList_unparse ( /*@observer@*/ constraintList s) /*@*/
 213 {
 214   return (constraintList_print(s));
 215 }
 216
 217 # if 0
 218 static /*@only@*/ cstring
 219 constraintList_printLocation (/*@temp@*/ constraintList s) /*@*/
 220 {
 221   int i;
 222   cstring st = cstring_undefined;
 223   bool first = TRUE;
 224
 225   if (!constraintList_isDefined (s))
 226     {
 227       return cstring_makeLiteral ("<undefined>");
 228     }
 229
 230   if (s->nelements == 0)
 231     {
 232       st = cstring_makeLiteral("<List Empty>");
 233       return st;
 234     }
 235
 236   for (i = 0; i < s->nelements; i++)
 237     {
 238       cstring type = cstring_undefined;
 239       constraint current = s->elements[i];
 240
 241       if (constraint_isDefined(current) )
 242         {
 243           cstring temp1;
 244               temp1 = constraint_printLocation(current);
 245           type = message ("%q %q\n", type, temp1 );
 246         }
 247
 248       if (first)
 249         {
 250           st = type;
 251           first = FALSE;
 252         }
 253       else
 254         {
 255           st = message ("%q, %q", st, type);
 256         }
 257     }
 258
 259   return st;
 260 }
 261 # endif
 262
 263 /*@only@*/ cstring
 264 constraintList_print (/*@temp@*/ constraintList s) /*@*/
 265 {
 266   int i;
 267   cstring st = cstring_undefined;
 268   bool first = TRUE;
 269
 270   if (!constraintList_isDefined (s))
 271     {
 272       return cstring_makeLiteral ("<undefined>");
 273     }
 274
 275   if (s->nelements == 0)
 276     {
 277       st = cstring_makeLiteral("<List Empty>");
 278       return st;
 279     }
 280
 281   for (i = 0; i < s->nelements; i++)
 282     {
 283       cstring type = cstring_undefined;
 284       constraint current = s->elements[i];
 285
 286       if (constraint_isDefined(current) )
 287         {
 288           cstring temp1;
 289
 290           if (context_getFlag (FLG_ORCONSTRAINT))
 291             {
 292               temp1 = constraint_printOr(current);
 293             }
 294           else
 295             {
 296               temp1 = constraint_print (current);
 297             }
 298           type = message ("%q %q\n", type, temp1 );
 299         }
 300
 301       if (first)
 302         {
 303           st = type;
 304           first = FALSE;
 305         }
 306       else
 307         {
 308           st = message ("%q, %q", st, type);
 309         }
 310     }
 311
 312   return st;
 313 }
 314
 315 void constraintList_printErrorPostConditions (constraintList s, fileloc loc)
 316 {
 317
 318   constraintList_elements (s, elem)
 319     {
 320       if (constraint_isDefined(elem))
 321         {
 322           constraint_printErrorPostCondition (elem, loc);
 323         }
 324     }
 325   end_constraintList_elements;
 326   return;
 327 }
 328
 329 void constraintList_printError (constraintList s, fileloc loc)
 330 {
 331
 332   constraintList_elements (s, elem)
 333     {
 334       if (constraint_isDefined(elem) )
 335         {
 336           if (constraint_isPost(elem) )
 337             constraint_printErrorPostCondition (elem, loc);
 338           else
 339             constraint_printError (elem, loc);
 340         }
 341     }
 342   end_constraintList_elements;
 343   return;
 344 }
 345
 346
 347 cstring
 348 constraintList_printDetailed (constraintList s)
 349 {
 350   int i;
 351   cstring st = cstring_undefined;
 352   bool first = TRUE;
 353
 354   if (!constraintList_isDefined (s))
 355     {
 356       return cstring_makeLiteral ("<undefined>");
 357     }
 358
 359   if (s->nelements == 0)
 360     {
 361       st = cstring_makeLiteral("<List Empty>");
 362       return st;
 363     }
 364
 365   for (i = 0; i < s->nelements; i++)
 366     {
 367       cstring type = cstring_undefined;
 368       constraint current = s->elements[i];
 369
 370       if (constraint_isDefined(current ) )
 371         {
 372           cstring temp1 = constraint_printDetailed (current);
 373           type = message ("%s %s\n", type, temp1 );
 374           cstring_free(temp1);
 375         }
 376
 377       if (first)
 378         {
 379           st = type;
 380           first = FALSE;
 381           type = NULL;
 382         }
 383       else
 384         {
 385           st = message ("%q %q", st, type);
 386         }
 387     }
 388   return st;
 389 }
 390
 391 /*{ x: constraint | (x in l1 -> resolve (x, l2) || (x in l2 -> resolve (x, l1)
 392 } */
 393
 394 constraintList
 395 constraintList_logicalOr (/*@observer@*/ constraintList l1, /*@observer@*/ constraintList l2)
 396 {
 397   constraint temp;
 398   constraintList ret;
 399   DPRINTF ((message ("Logical or on %s and %s",
 400                       constraintList_print(l1),
 401                       constraintList_print(l2)) ) );
 402
 403   ret = constraintList_makeNew();
 404   constraintList_elements (l1, el)
 405     {
 406       temp = constraint_substitute (el, l2);
 407
 408       if (constraintList_resolve (el, l2) || constraintList_resolve(temp,l2) )
 409         {   /*avoid redundant constraints*/
 410           if (!constraintList_resolve (el, ret) )
 411             {
 412               constraint temp2;
 413               temp2 = constraint_copy(el);
 414               ret = constraintList_add (ret, temp2);
 415             }
 416         }
 417       constraint_free(temp);
 418     }
 419   end_constraintList_elements;
 420
 421    constraintList_elements (l2, el)
 422     {
 423       temp = constraint_substitute (el, l1);
 424
 425       if (constraintList_resolve (el, l1) || constraintList_resolve(temp,l1) )
 426         {
 427           /*avoid redundant constraints*/
 428           if (!constraintList_resolve (el, ret) )
 429             {
 430               constraint temp2;
 431               temp2 = constraint_copy(el);
 432               ret = constraintList_add (ret, temp2);
 433             }
 434         }
 435       constraint_free(temp);
 436     }
 437   end_constraintList_elements;
 438
 439
 440   return ret;
 441 }
 442
 443 void
 444 constraintList_free (/*@only@*/ constraintList s)
 445 {
 446   int i;
 447
 448   llassert(constraintList_isDefined(s) );
 449
 450
 451   for (i = 0; i < s->nelements; i++)
 452     {
 453       constraint_free (s->elements[i]);
 454     }
 455
 456   sfree (s->elements);
 457   s->elements = NULL;
 458   s->nelements = -1;
 459   s->nspace = -1;
 460   sfree (s);
 461   s = NULL;
 462 }
 463
 464 constraintList
 465 constraintList_copy (/*@observer@*/ /*@temp@*/ constraintList s)
 466 {
 467   constraintList ret = constraintList_makeNew ();
 468
 469   constraintList_elements (s, el)
 470     {
 471       ret = constraintList_add (ret, constraint_copy (el));
 472     } end_constraintList_elements;
 473
 474   return ret;
 475 }
 476
 477 constraintList constraintList_preserveOrig (constraintList c)
 478 {
 479   DPRINTF((message("constraintList_preserveOrig preserving the originial constraints for %s ", constraintList_print (c) ) ));
 480
 481   constraintList_elements_private (c, el)
 482   {
 483     el = constraint_preserveOrig (el);
 484   }
 485   end_constraintList_elements_private;
 486   return c;
 487 }
 488
 489 constraintList constraintList_preserveCallInfo (/*@returned@*/ constraintList c,/*@observer@*/ /*@dependent@*/ /*@observer@*/  exprNode fcn)
 490 {
 491   DPRINTF((message("constraintList_preserveCallInfo %s ", constraintList_print (c) ) ));
 492
 493   constraintList_elements_private (c, el)
 494   {
 495     el = constraint_setFcnPre(el);
 496     el = constraint_origAddGeneratingExpr (el, fcn);
 497   }
 498   end_constraintList_elements_private;
 499   return c;
 500 }
 501
 502 constraintList constraintList_single (constraint c)
 503 {
 504   constraintList res;
 505   res = constraintList_makeNew();
 506   res = constraintList_add (res, c);
 507   return res;
 508 }
 509
 510 constraintList constraintList_addGeneratingExpr (constraintList c,/*@dependent@*/ exprNode e)
 511 {
 512   DPRINTF ((message ("entering constraintList_addGeneratingExpr for %s ", exprNode_unparse(e) ) ));
 513
 514   constraintList_elements_private (c, el)
 515   {
 516     DPRINTF ((message ("setting generatingExpr for %s to %s", constraint_print(el), exprNode_unparse(e) )  ));
 517     el = constraint_addGeneratingExpr (el, e);
 518   }
 519   end_constraintList_elements_private;
 520   return c;
 521 }
 522
 523 /*@only@*/ constraintList constraintList_doFixResult (/*@only@*/constraintList postconditions, exprNode fcnCall)
 524 {
 525   constraintList ret;
 526   ret = constraintList_makeNew();
 527   constraintList_elements_private (postconditions, el)
 528     {
 529       ret = constraintList_add (ret, constraint_doFixResult (el, fcnCall) );
 530     }
 531   end_constraintList_elements_private;
 532
 533   constraintList_free(postconditions);
 534   return ret;
 535 }
 536 /*
 537 Commenting out because function is not yet stable
 538
 539 / *@only@* / constraintList constraintList_doSRefFixStructConstraint(constraintList invars, sRef s, ctype ct )
 540 {
 541   constraintList ret;
 542   ret = constraintList_makeNew();
 543
 544   constraintList_elements (invars, el)
 545     {
 546       ret = constraintList_add(ret, constraint_doSRefFixInvarConstraint (el, s, ct) );
 547     }
 548   end_constraintList_elements;
 549
 550   / *  constraintList_free (invars);* /
 551
 552   return ret;
 553 }
 554 */
 555
 556 /*@only@*/ constraintList constraintList_doSRefFixConstraintParam (constraintList preconditions, /*@temp@*/ /*@observer@*/ exprNodeList arglist)
 557 {
 558   constraintList ret;
 559   ret = constraintList_makeNew();
 560
 561   constraintList_elements (preconditions, el)
 562     {
 563       ret = constraintList_add(ret, constraint_doSRefFixConstraintParam (el, arglist) );
 564     }
 565   end_constraintList_elements;
 566
 567   constraintList_free (preconditions);
 568
 569   return ret;
 570 }
 571 constraintList constraintList_doSRefFixBaseParam (constraintList preconditions, /*@observer@*/
 572                                                    exprNodeList arglist)
 573 {
 574   constraintList ret;
 575   constraint temp;
 576   ret = constraintList_makeNew();
 577
 578   constraintList_elements (preconditions, el)
 579     {
 580       temp = constraint_copy(el);
 581       ret = constraintList_add(ret, constraint_doSRefFixBaseParam (temp, arglist) );
 582     }
 583   end_constraintList_elements;
 584
 585   return ret;
 586 }
 587
 588 constraintList constraintList_togglePost (/*@returned@*/ constraintList c)
 589 {
 590   constraintList_elements_private (c, el)
 591     {
 592       el = constraint_togglePost(el);
 593       if (constraint_hasOrig(el) )
 594         {
 595           el = constraint_togglePostOrig (el);
 596         }
 597     }
 598   end_constraintList_elements_private;
 599   return c;
 600 }
 601
 602 /*@only@*/ constraintList constraintList_undump (FILE *f)
 603 {
 604   constraintList ret;
 605   char *s;
 606   char *os;
 607
 608   ret = constraintList_makeNew();
 609
 610   os =  mstring_create (MAX_DUMP_LINE_LENGTH);
 611   s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 612
 613   while (s != NULL && *s != ';')
 614     {
 615       constraint temp;
 616       char * c;
 617
 618       c =  reader_getWord(&s);
 619
 620       if (strcmp (c, "C") != 0)
 621         {
 622           llfatalbug(message("Error reading library.  File may be corrupted"));
 623         }
 624
 625       temp = constraint_undump (f);
 626       ret = constraintList_add (ret, temp);
 627       s = fgets (os, MAX_DUMP_LINE_LENGTH, f);
 628       free(c);
 629     }
 630   free(s);
 631
 632   return ret;
 633 }
 634
 635
 636 void constraintList_dump (/*@observer@*/ constraintList c,  FILE *f)
 637 {
 638   constraintList_elements (c, el)
 639     {
 640       fprintf(f, "C\n");
 641       constraint_dump (el, f);
 642     }
 643   end_constraintList_elements; ;
 644 }
 645
 646
 647 constraintList constraintList_sort (/*@returned@*/ constraintList 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