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