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