src/stateInfo.c

   1 /*
   2 ** Splint - annotation-assisted static program checker
   3 ** Copyright (C) 1994-2003 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 # include "splintMacros.nf"
  26 # include "basic.h"
  27
  28 static /*@observer@*/ cstring stateAction_unparse (stateAction p_sa) /*@*/ ;
  29
  30 void stateInfo_free (/*@only@*/ stateInfo a)
  31 {
  32   if (a != NULL)
  33     {
  34       fileloc_free (a->loc);
  35       sfree (a);
  36     }
  37 }
  38
  39 /*@only@*/ stateInfo stateInfo_update (/*@only@*/ stateInfo old, stateInfo newinfo)
  40      /*
  41      ** returns an stateInfo with the same value as new.  May reuse the
  42      ** storage of old.  (i.e., same effect as copy, but more
  43      ** efficient.)
  44      */
  45 {
  46   if (old == NULL)
  47     {
  48       DPRINTF (("Update state ==> %s", stateInfo_unparse (newinfo)));
  49       return stateInfo_copy (newinfo);
  50     }
  51   else if (newinfo == NULL)
  52     {
  53       stateInfo_free (old);
  54       return NULL;
  55     }
  56   else
  57     {
  58       if (fileloc_equal (old->loc, newinfo->loc)
  59           && old->action == newinfo->action
  60           /*@-abstractcompare@*/ && old->ref == newinfo->ref /*@=abstractcompare@*/)
  61         {
  62           /*
  63           ** Duplicate (change through alias most likely)
  64           ** don't add this info
  65           */
  66
  67           return old;
  68         }
  69       else
  70         {
  71           stateInfo snew = stateInfo_makeRefLoc (newinfo->ref,
  72                                                  newinfo->loc, newinfo->action);
  73           llassert (snew->previous == NULL);
  74           snew->previous = old;
  75           DPRINTF (("Update state ==> %s", stateInfo_unparse (snew)));
  76           return snew;
  77         }
  78     }
  79 }
  80
  81 static /*@observer@*/ stateInfo stateInfo_sort (/*@temp@*/ stateInfo sinfo)
  82      /* Sorts in reverse location order */
  83 {
  84   DPRINTF (("Sorting: %s", stateInfo_unparse (sinfo)));
  85
  86   if (sinfo == NULL || sinfo->previous == NULL)
  87     {
  88       return sinfo;
  89     }
  90   else
  91     {
  92       stateInfo snext = stateInfo_sort (sinfo->previous);
  93       stateInfo sfirst = snext;
  94
  95       DPRINTF (("sinfo/sext: %s // %s", stateInfo_unparse (sinfo), stateInfo_unparse (snext)));
  96       llassert (snext != NULL);
  97
  98       if (!fileloc_lessthan (sinfo->loc, snext->loc))
  99         {
 100           /*@i2@*/ sinfo->previous = sfirst; /* spurious? */
 101           DPRINTF (("Sorted ==> %s", stateInfo_unparse (sinfo)));
 102           /*@i2@*/ return sinfo; /* spurious? */
 103         }
 104       else
 105         {
 106           while (snext != NULL && fileloc_lessthan (sinfo->loc, snext->loc))
 107             {
 108               /*
 109               ** swap the order
 110               */
 111               fileloc tloc = snext->loc;
 112               stateAction taction = snext->action;
 113               sRef tref = snext->ref;
 114
 115               DPRINTF (("in while: sinfo/sext: %s // %s", stateInfo_unparse (sinfo), stateInfo_unparse (snext)));
 116
 117               snext->loc = sinfo->loc;
 118               snext->action = sinfo->action;
 119               /*@-modobserver@*/
 120               snext->ref = sinfo->ref; /* Doesn't actually modifie sfirst */
 121               /*@=modobserver@*/
 122
 123               sinfo->loc = tloc;
 124               sinfo->action = taction;
 125               sinfo->ref = tref;
 126               /*@-mustfreeonly@*/
 127               sinfo->previous = snext->previous;
 128               /*@=mustfreeonly@*/
 129               snext = snext->previous;
 130               DPRINTF (("in while: sinfo/sext: %s // %s", stateInfo_unparse (sinfo), stateInfo_unparse (snext)));
 131             }
 132
 133           DPRINTF (("Sorted ==> %s", stateInfo_unparse (sfirst)));
 134           /*@-compmempass@*/
 135           return sfirst;
 136           /*@=compmempass@*/
 137         }
 138     }
 139 }
 140
 141 /*@only@*/ stateInfo
 142 stateInfo_updateLoc (/*@only@*/ stateInfo old, stateAction action, fileloc loc)
 143 {
 144   if (fileloc_isUndefined (loc)) {
 145     loc = fileloc_copy (g_currentloc);
 146   }
 147
 148   if (old != NULL && fileloc_equal (old->loc, loc) && old->action == action)
 149     {
 150       /*
 151       ** Duplicate (change through alias most likely)
 152       ** don't add this info
 153       */
 154
 155       return old;
 156     }
 157   else
 158     {
 159       stateInfo snew = stateInfo_makeLoc (loc, action);
 160       llassert (snew->previous == NULL);
 161       snew->previous = old;
 162       DPRINTF (("Update state ==> %s", stateInfo_unparse (snew)));
 163       return snew;
 164     }
 165 }
 166
 167 /*@only@*/ stateInfo
 168 stateInfo_updateRefLoc (/*@only@*/ stateInfo old, /*@exposed@*/ sRef ref,
 169                         stateAction action, fileloc loc)
 170 {
 171   if (fileloc_isUndefined (loc)) {
 172     loc = fileloc_copy (g_currentloc);
 173   }
 174
 175   if (old != NULL && fileloc_equal (old->loc, loc)
 176       && old->action == action
 177       /*@-abstractcompare*/ && old->ref == ref /*@=abstractcompare@*/)
 178     {
 179       /*
 180       ** Duplicate (change through alias most likely)
 181       ** don't add this info
 182       */
 183
 184       return old;
 185     }
 186   else
 187     {
 188       stateInfo snew = stateInfo_makeRefLoc (ref, loc, action);
 189       llassert (snew->previous == NULL);
 190       snew->previous = old;
 191       DPRINTF (("Update state ==> %s", stateInfo_unparse (snew)));
 192       return snew;
 193     }
 194 }
 195
 196 /*@only@*/ stateInfo stateInfo_copy (stateInfo a)
 197 {
 198   if (a == NULL)
 199     {
 200       return NULL;
 201     }
 202   else
 203     {
 204       stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 205
 206       ret->loc = fileloc_copy (a->loc); /*< should report bug without copy! >*/
 207       ret->ref = a->ref;
 208       ret->action = a->action;
 209       ret->previous = stateInfo_copy (a->previous);
 210
 211       return ret;
 212     }
 213 }
 214
 215 /*@only@*/ /*@notnull@*/ stateInfo
 216 stateInfo_currentLoc (void)
 217 {
 218   return stateInfo_makeLoc (g_currentloc, SA_DECLARED);
 219 }
 220
 221 /*@only@*/ /*@notnull@*/ stateInfo
 222 stateInfo_makeLoc (fileloc loc, stateAction action)
 223 {
 224   stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 225
 226   if (fileloc_isUndefined (loc)) {
 227     ret->loc = fileloc_copy (g_currentloc);
 228   } else {
 229     ret->loc = fileloc_copy (loc);
 230   }
 231
 232   ret->ref = sRef_undefined;
 233   ret->action = action;
 234   ret->previous = stateInfo_undefined;
 235
 236   DPRINTF (("Make loc ==> %s", stateInfo_unparse (ret)));
 237   return ret;
 238 }
 239
 240 /*@only@*/ /*@notnull@*/ stateInfo
 241 stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc, stateAction action)
 242      /*@post:isnull result->previous@*/
 243 {
 244   stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 245
 246   if (fileloc_isUndefined (loc)) {
 247     ret->loc = fileloc_copy (g_currentloc);
 248   } else {
 249     ret->loc = fileloc_copy (loc);
 250   }
 251
 252   ret->ref = ref;
 253   ret->action = action;
 254   ret->previous = stateInfo_undefined;
 255
 256   return ret;
 257 }
 258
 259 /*@only@*/ cstring
 260 stateInfo_unparse (stateInfo s)
 261 {
 262   cstring res = cstring_makeLiteral ("");
 263
 264   while (stateInfo_isDefined (s)) {
 265     res = message ("%q%q: ", res, fileloc_unparse (s->loc));
 266     if (sRef_isValid (s->ref)) {
 267       res = message ("%q through alias %q ", res, sRef_unparse (s->ref));
 268     }
 269
 270     res = message ("%q%s; ", res, stateAction_unparse (s->action));
 271     s = s->previous;
 272   }
 273
 274   return res;
 275 }
 276
 277 fileloc stateInfo_getLoc (stateInfo info)
 278 {
 279     if (stateInfo_isDefined (info))
 280       {
 281         return info->loc;
 282       }
 283
 284     return fileloc_undefined;
 285 }
 286
 287 stateAction stateAction_fromNState (nstate ns)
 288 {
 289   switch (ns)
 290     {
 291     case NS_ERROR:
 292     case NS_UNKNOWN:
 293       return SA_UNKNOWN;
 294     case NS_NOTNULL:
 295     case NS_MNOTNULL:
 296       return SA_BECOMESNONNULL;
 297     case NS_RELNULL:
 298     case NS_CONSTNULL:
 299       return SA_DECLARED;
 300     case NS_POSNULL:
 301       return SA_BECOMESPOSSIBLYNULL;
 302     case NS_DEFNULL:
 303       return SA_BECOMESNULL;
 304     case NS_ABSNULL:
 305       return SA_BECOMESPOSSIBLYNULL;
 306     }
 307 }
 308
 309 stateAction stateAction_fromExkind (exkind ex)
 310 {
 311   switch (ex)
 312     {
 313     case XO_UNKNOWN:
 314     case XO_NORMAL:
 315       return SA_UNKNOWN;
 316     case XO_EXPOSED:
 317       return SA_EXPOSED;
 318     case XO_OBSERVER:
 319       return SA_OBSERVER;
 320     }
 321
 322   BADBRANCH;
 323   /*@notreached@*/ return SA_UNKNOWN;
 324 }
 325
 326 stateAction stateAction_fromAlkind (alkind ak)
 327 {
 328   switch (ak)
 329     {
 330     case AK_UNKNOWN:
 331     case AK_ERROR:
 332       return SA_UNKNOWN;
 333     case AK_ONLY:
 334       return SA_ONLY;
 335     case AK_IMPONLY:
 336       return SA_IMPONLY;
 337     case AK_KEEP:
 338       return SA_KEEP;
 339     case AK_KEPT:
 340       return SA_KEPT;
 341     case AK_TEMP:
 342       return SA_TEMP;
 343     case AK_IMPTEMP:
 344       return SA_IMPTEMP;
 345     case AK_SHARED:
 346       return SA_SHARED;
 347     case AK_UNIQUE:
 348     case AK_RETURNED:
 349       return SA_DECLARED;
 350     case AK_FRESH:
 351       return SA_FRESH;
 352     case AK_STACK:
 353       return SA_XSTACK;
 354     case AK_REFCOUNTED:
 355       return SA_REFCOUNTED;
 356     case AK_REFS:
 357       return SA_REFS;
 358     case AK_KILLREF:
 359       return SA_KILLREF;
 360     case AK_NEWREF:
 361       return SA_NEWREF;
 362     case AK_OWNED:
 363       return SA_OWNED;
 364     case AK_DEPENDENT:
 365       return SA_DEPENDENT;
 366     case AK_IMPDEPENDENT:
 367       return SA_IMPDEPENDENT;
 368     case AK_STATIC:
 369       return SA_STATIC;
 370     case AK_LOCAL:
 371       return SA_LOCAL;
 372     }
 373
 374   BADBRANCH;
 375   /*@notreached@*/ return SA_UNKNOWN;
 376 }
 377
 378 stateAction stateAction_fromSState (sstate ss)
 379 {
 380   switch (ss)
 381     {
 382     case SS_UNKNOWN: return SA_DECLARED;
 383     case SS_UNUSEABLE: return SA_KILLED;
 384     case SS_UNDEFINED: return SA_UNDEFINED;
 385     case SS_MUNDEFINED: return SA_MUNDEFINED;
 386     case SS_ALLOCATED: return SA_ALLOCATED;
 387     case SS_PDEFINED: return SA_PDEFINED;
 388     case SS_DEFINED: return SA_DEFINED;
 389     case SS_PARTIAL: return SA_PDEFINED;
 390     case SS_DEAD: return SA_RELEASED;
 391     case SS_HOFFA: return SA_PKILLED;
 392     case SS_SPECIAL: return SA_DECLARED;
 393     case SS_RELDEF: return SA_DECLARED;
 394     case SS_FIXED:
 395     case SS_UNDEFGLOB:
 396     case SS_KILLED:
 397     case SS_UNDEFKILLED:
 398     case SS_LAST:
 399       llbug (message ("Unexpected sstate: %s", sstate_unparse (ss)));
 400       /*@notreached@*/ return SA_UNKNOWN;
 401     }
 402 }
 403
 404 static /*@observer@*/ cstring stateAction_unparse (stateAction sa)
 405 {
 406   switch (sa)
 407     {
 408     case SA_UNKNOWN: return cstring_makeLiteralTemp ("changed <unknown modification>");
 409     case SA_CHANGED: return cstring_makeLiteralTemp ("changed");
 410
 411     case SA_CREATED: return cstring_makeLiteralTemp ("created");
 412     case SA_DECLARED: return cstring_makeLiteralTemp ("declared");
 413     case SA_DEFINED: return cstring_makeLiteralTemp ("defined");
 414     case SA_PDEFINED: return cstring_makeLiteralTemp ("partially defined");
 415     case SA_RELEASED: return cstring_makeLiteralTemp ("released");
 416     case SA_ALLOCATED: return cstring_makeLiteralTemp ("allocated");
 417     case SA_KILLED: return cstring_makeLiteralTemp ("released");
 418     case SA_PKILLED: return cstring_makeLiteralTemp ("possibly released");
 419     case SA_MERGED: return cstring_makeLiteralTemp ("merged");
 420     case SA_UNDEFINED: return cstring_makeLiteralTemp ("becomes undefined");
 421     case SA_MUNDEFINED: return cstring_makeLiteralTemp ("possibly undefined");
 422
 423     case SA_SHARED: return cstring_makeLiteralTemp ("becomes shared");
 424     case SA_ONLY: return cstring_makeLiteralTemp ("becomes only");
 425     case SA_IMPONLY: return cstring_makeLiteralTemp ("becomes implicitly only");
 426     case SA_OWNED: return cstring_makeLiteralTemp ("becomes owned");
 427     case SA_DEPENDENT: return cstring_makeLiteralTemp ("becomes dependent");
 428     case SA_IMPDEPENDENT: return cstring_makeLiteralTemp ("becomes implicitly dependent");
 429     case SA_KEPT: return cstring_makeLiteralTemp ("becomes kept");
 430     case SA_KEEP: return cstring_makeLiteralTemp ("becomes keep");
 431     case SA_FRESH: return cstring_makeLiteralTemp ("becomes fresh");
 432     case SA_TEMP: return cstring_makeLiteralTemp ("becomes temp");
 433     case SA_IMPTEMP: return cstring_makeLiteralTemp ("becomes implicitly temp");
 434     case SA_XSTACK: return cstring_makeLiteralTemp ("becomes stack-allocated storage");
 435     case SA_STATIC: return cstring_makeLiteralTemp ("becomes static");
 436     case SA_LOCAL: return cstring_makeLiteralTemp ("becomes local");
 437
 438     case SA_REFCOUNTED: return cstring_makeLiteralTemp ("becomes refcounted");
 439     case SA_REFS: return cstring_makeLiteralTemp ("becomes refs");
 440     case SA_NEWREF: return cstring_makeLiteralTemp ("becomes newref");
 441     case SA_KILLREF: return cstring_makeLiteralTemp ("becomes killref");
 442
 443     case SA_OBSERVER: return cstring_makeLiteralTemp ("becomes observer");
 444     case SA_EXPOSED: return cstring_makeLiteralTemp ("becomes exposed");
 445
 446     case SA_BECOMESNULL: return cstring_makeLiteralTemp ("becomes null");
 447     case SA_BECOMESNONNULL: return cstring_makeLiteralTemp ("becomes non-null");
 448     case SA_BECOMESPOSSIBLYNULL: return cstring_makeLiteralTemp ("becomes possibly null");
 449     }
 450
 451   DPRINTF (("Bad state action: %d", sa));
 452   BADBRANCH;
 453 }
 454
 455 void stateInfo_display (stateInfo s, cstring sname)
 456 {
 457   bool showdeep = context_flagOn (FLG_SHOWDEEPHISTORY, g_currentloc);
 458
 459   s = stateInfo_sort (s);
 460
 461   while (stateInfo_isDefined (s))
 462     {
 463       cstring msg = message ("%s%s", sname, stateAction_unparse (s->action));
 464
 465       if (sRef_isValid (s->ref)) {
 466         msg = message ("%q (through alias %q)", msg, sRef_unparse (s->ref));
 467       }
 468
 469       llgenindentmsg (msg, s->loc);
 470
 471       if (!showdeep) {
 472         break;
 473       }
 474
 475       s = s->previous;
 476     }
 477
 478   cstring_free (sname);
 479 }
 480
 481