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