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           /*@i888@*/ sinfo->previous = sfirst;
 101           DPRINTF (("Sorted ==> %s", stateInfo_unparse (sinfo)));
 102           /*@i888@*/ return sinfo;
 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               /*@i888@*/ snext->ref = sinfo->ref;
 120
 121               sinfo->loc = tloc;
 122               sinfo->action = taction;
 123               sinfo->ref = tref;
 124               /*@i888@*/ sinfo->previous = snext->previous;
 125               snext = snext->previous;
 126               DPRINTF (("in while: sinfo/sext: %s // %s", stateInfo_unparse (sinfo), stateInfo_unparse (snext)));
 127             }
 128
 129           DPRINTF (("Sorted ==> %s", stateInfo_unparse (sfirst)));
 130           /*@i888@*/ return sfirst;
 131         }
 132     }
 133 }
 134
 135 /*@only@*/ stateInfo
 136 stateInfo_updateLoc (/*@only@*/ stateInfo old, stateAction action, fileloc loc)
 137 {
 138   if (fileloc_isUndefined (loc)) {
 139     loc = fileloc_copy (g_currentloc);
 140   }
 141
 142   if (old != NULL && fileloc_equal (old->loc, loc) && old->action == action)
 143     {
 144       /*
 145       ** Duplicate (change through alias most likely)
 146       ** don't add this info
 147       */
 148
 149       return old;
 150     }
 151   else
 152     {
 153       stateInfo snew = stateInfo_makeLoc (loc, action);
 154       llassert (snew->previous == NULL);
 155       snew->previous = old;
 156       DPRINTF (("Update state ==> %s", stateInfo_unparse (snew)));
 157       return snew;
 158     }
 159 }
 160
 161 /*@only@*/ stateInfo
 162 stateInfo_updateRefLoc (/*@only@*/ stateInfo old, /*@exposed@*/ sRef ref,
 163                         stateAction action, fileloc loc)
 164 {
 165   if (fileloc_isUndefined (loc)) {
 166     loc = fileloc_copy (g_currentloc);
 167   }
 168
 169   if (old != NULL && fileloc_equal (old->loc, loc)
 170       && old->action == action
 171       /*@-abstractcompare*/ && old->ref == ref /*@=abstractcompare@*/)
 172     {
 173       /*
 174       ** Duplicate (change through alias most likely)
 175       ** don't add this info
 176       */
 177
 178       return old;
 179     }
 180   else
 181     {
 182       stateInfo snew = stateInfo_makeRefLoc (ref, loc, action);
 183       llassert (snew->previous == NULL);
 184       snew->previous = old;
 185       DPRINTF (("Update state ==> %s", stateInfo_unparse (snew)));
 186       return snew;
 187     }
 188 }
 189
 190 /*@only@*/ stateInfo stateInfo_copy (stateInfo a)
 191 {
 192   if (a == NULL)
 193     {
 194       return NULL;
 195     }
 196   else
 197     {
 198       stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 199
 200       ret->loc = fileloc_copy (a->loc); /*< should report bug without copy! >*/
 201       ret->ref = a->ref;
 202       ret->action = a->action;
 203       ret->previous = stateInfo_copy (a->previous);
 204
 205       return ret;
 206     }
 207 }
 208
 209 /*@only@*/ /*@notnull@*/ stateInfo
 210 stateInfo_currentLoc (void)
 211 {
 212   return stateInfo_makeLoc (g_currentloc, SA_DECLARED);
 213 }
 214
 215 /*@only@*/ /*@notnull@*/ stateInfo
 216 stateInfo_makeLoc (fileloc loc, stateAction action)
 217 {
 218   stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 219
 220   if (fileloc_isUndefined (loc)) {
 221     ret->loc = fileloc_copy (g_currentloc);
 222   } else {
 223     ret->loc = fileloc_copy (loc);
 224   }
 225
 226   ret->ref = sRef_undefined;
 227   ret->action = action;
 228   ret->previous = stateInfo_undefined;
 229
 230   DPRINTF (("Make loc ==> %s", stateInfo_unparse (ret)));
 231   return ret;
 232 }
 233
 234 /*@only@*/ /*@notnull@*/ stateInfo
 235 stateInfo_makeRefLoc (/*@exposed@*/ sRef ref, fileloc loc, stateAction action)
 236      /*@post:isnull result->previous@*/
 237 {
 238   stateInfo ret = (stateInfo) dmalloc (sizeof (*ret));
 239
 240   if (fileloc_isUndefined (loc)) {
 241     ret->loc = fileloc_copy (g_currentloc);
 242   } else {
 243     ret->loc = fileloc_copy (loc);
 244   }
 245
 246   ret->ref = ref;
 247   ret->action = action;
 248   ret->previous = stateInfo_undefined;
 249
 250   return ret;
 251 }
 252
 253 /*@only@*/ cstring
 254 stateInfo_unparse (stateInfo s)
 255 {
 256   cstring res = cstring_makeLiteral ("");
 257
 258   while (stateInfo_isDefined (s)) {
 259     res = message ("%q%q: ", res, fileloc_unparse (s->loc));
 260     if (sRef_isValid (s->ref)) {
 261       res = message ("%q through alias %q ", res, sRef_unparse (s->ref));
 262     }
 263
 264     res = message ("%q%s; ", res, stateAction_unparse (s->action));
 265     s = s->previous;
 266   }
 267
 268   return res;
 269 }
 270
 271 fileloc stateInfo_getLoc (stateInfo info)
 272 {
 273     if (stateInfo_isDefined (info))
 274       {
 275         return info->loc;
 276       }
 277
 278     return fileloc_undefined;
 279 }
 280
 281 stateAction stateAction_fromNState (nstate ns)
 282 {
 283   switch (ns)
 284     {
 285     case NS_ERROR:
 286     case NS_UNKNOWN:
 287       return SA_UNKNOWN;
 288     case NS_NOTNULL:
 289     case NS_MNOTNULL:
 290       return SA_BECOMESNONNULL;
 291     case NS_RELNULL:
 292     case NS_CONSTNULL:
 293       return SA_DECLARED;
 294     case NS_POSNULL:
 295       return SA_BECOMESPOSSIBLYNULL;
 296     case NS_DEFNULL:
 297       return SA_BECOMESNULL;
 298     case NS_ABSNULL:
 299       return SA_BECOMESPOSSIBLYNULL;
 300     }
 301 }
 302
 303 stateAction stateAction_fromExkind (exkind ex)
 304 {
 305   switch (ex)
 306     {
 307     case XO_UNKNOWN:
 308     case XO_NORMAL:
 309       return SA_UNKNOWN;
 310     case XO_EXPOSED:
 311       return SA_EXPOSED;
 312     case XO_OBSERVER:
 313       return SA_OBSERVER;
 314     }
 315
 316   BADBRANCH;
 317   /*@notreached@*/ return SA_UNKNOWN;
 318 }
 319
 320 stateAction stateAction_fromAlkind (alkind ak)
 321 {
 322   switch (ak)
 323     {
 324     case AK_UNKNOWN:
 325     case AK_ERROR:
 326       return SA_UNKNOWN;
 327     case AK_ONLY:
 328       return SA_ONLY;
 329     case AK_IMPONLY:
 330       return SA_IMPONLY;
 331     case AK_KEEP:
 332       return SA_KEEP;
 333     case AK_KEPT:
 334       return SA_KEPT;
 335     case AK_TEMP:
 336       return SA_TEMP;
 337     case AK_IMPTEMP:
 338       return SA_IMPTEMP;
 339     case AK_SHARED:
 340       return SA_SHARED;
 341     case AK_UNIQUE:
 342     case AK_RETURNED:
 343       return SA_DECLARED;
 344     case AK_FRESH:
 345       return SA_FRESH;
 346     case AK_STACK:
 347       return SA_XSTACK;
 348     case AK_REFCOUNTED:
 349       return SA_REFCOUNTED;
 350     case AK_REFS:
 351       return SA_REFS;
 352     case AK_KILLREF:
 353       return SA_KILLREF;
 354     case AK_NEWREF:
 355       return SA_NEWREF;
 356     case AK_OWNED:
 357       return SA_OWNED;
 358     case AK_DEPENDENT:
 359       return SA_DEPENDENT;
 360     case AK_IMPDEPENDENT:
 361       return SA_IMPDEPENDENT;
 362     case AK_STATIC:
 363       return SA_STATIC;
 364     case AK_LOCAL:
 365       return SA_LOCAL;
 366     }
 367
 368   BADBRANCH;
 369   /*@notreached@*/ return SA_UNKNOWN;
 370 }
 371
 372 stateAction stateAction_fromSState (sstate ss)
 373 {
 374   switch (ss)
 375     {
 376     case SS_UNKNOWN: return SA_DECLARED;
 377     case SS_UNUSEABLE: return SA_KILLED;
 378     case SS_UNDEFINED: return SA_UNDEFINED;
 379     case SS_MUNDEFINED: return SA_MUNDEFINED;
 380     case SS_ALLOCATED: return SA_ALLOCATED;
 381     case SS_PDEFINED: return SA_PDEFINED;
 382     case SS_DEFINED: return SA_DEFINED;
 383     case SS_PARTIAL: return SA_PDEFINED;
 384     case SS_DEAD: return SA_RELEASED;
 385     case SS_HOFFA: return SA_PKILLED;
 386     case SS_SPECIAL: return SA_DECLARED;
 387     case SS_RELDEF: return SA_DECLARED;
 388     case SS_FIXED:
 389     case SS_UNDEFGLOB:
 390     case SS_KILLED:
 391     case SS_UNDEFKILLED:
 392     case SS_LAST:
 393       llbug (message ("Unexpected sstate: %s", sstate_unparse (ss)));
 394       /*@notreached@*/ return SA_UNKNOWN;
 395     }
 396 }
 397
 398 static /*@observer@*/ cstring stateAction_unparse (stateAction sa)
 399 {
 400   switch (sa)
 401     {
 402     case SA_UNKNOWN: return cstring_makeLiteralTemp ("changed <unknown modification>");
 403     case SA_CHANGED: return cstring_makeLiteralTemp ("changed");
 404
 405     case SA_CREATED: return cstring_makeLiteralTemp ("created");
 406     case SA_DECLARED: return cstring_makeLiteralTemp ("declared");
 407     case SA_DEFINED: return cstring_makeLiteralTemp ("defined");
 408     case SA_PDEFINED: return cstring_makeLiteralTemp ("partially defined");
 409     case SA_RELEASED: return cstring_makeLiteralTemp ("released");
 410     case SA_ALLOCATED: return cstring_makeLiteralTemp ("allocated");
 411     case SA_KILLED: return cstring_makeLiteralTemp ("released");
 412     case SA_PKILLED: return cstring_makeLiteralTemp ("possibly released");
 413     case SA_MERGED: return cstring_makeLiteralTemp ("merged");
 414     case SA_UNDEFINED: return cstring_makeLiteralTemp ("becomes undefined");
 415     case SA_MUNDEFINED: return cstring_makeLiteralTemp ("possibly undefined");
 416
 417     case SA_SHARED: return cstring_makeLiteralTemp ("becomes shared");
 418     case SA_ONLY: return cstring_makeLiteralTemp ("becomes only");
 419     case SA_IMPONLY: return cstring_makeLiteralTemp ("becomes implicitly only");
 420     case SA_OWNED: return cstring_makeLiteralTemp ("becomes owned");
 421     case SA_DEPENDENT: return cstring_makeLiteralTemp ("becomes dependent");
 422     case SA_IMPDEPENDENT: return cstring_makeLiteralTemp ("becomes implicitly dependent");
 423     case SA_KEPT: return cstring_makeLiteralTemp ("becomes kept");
 424     case SA_KEEP: return cstring_makeLiteralTemp ("becomes keep");
 425     case SA_FRESH: return cstring_makeLiteralTemp ("becomes fresh");
 426     case SA_TEMP: return cstring_makeLiteralTemp ("becomes temp");
 427     case SA_IMPTEMP: return cstring_makeLiteralTemp ("becomes implicitly temp");
 428     case SA_XSTACK: return cstring_makeLiteralTemp ("becomes stack-allocated storage");
 429     case SA_STATIC: return cstring_makeLiteralTemp ("becomes static");
 430     case SA_LOCAL: return cstring_makeLiteralTemp ("becomes local");
 431
 432     case SA_REFCOUNTED: return cstring_makeLiteralTemp ("becomes refcounted");
 433     case SA_REFS: return cstring_makeLiteralTemp ("becomes refs");
 434     case SA_NEWREF: return cstring_makeLiteralTemp ("becomes newref");
 435     case SA_KILLREF: return cstring_makeLiteralTemp ("becomes killref");
 436
 437     case SA_OBSERVER: return cstring_makeLiteralTemp ("becomes observer");
 438     case SA_EXPOSED: return cstring_makeLiteralTemp ("becomes exposed");
 439
 440     case SA_BECOMESNULL: return cstring_makeLiteralTemp ("becomes null");
 441     case SA_BECOMESNONNULL: return cstring_makeLiteralTemp ("becomes non-null");
 442     case SA_BECOMESPOSSIBLYNULL: return cstring_makeLiteralTemp ("becomes possibly null");
 443     }
 444
 445   DPRINTF (("Bad state action: %d", sa));
 446   BADBRANCH;
 447 }
 448
 449 void stateInfo_display (stateInfo s, cstring sname)
 450 {
 451   bool showdeep = context_flagOn (FLG_SHOWDEEPHISTORY, g_currentloc);
 452
 453   s = stateInfo_sort (s);
 454
 455   while (stateInfo_isDefined (s))
 456     {
 457       cstring msg = message ("%s%s", sname, stateAction_unparse (s->action));
 458
 459       if (sRef_isValid (s->ref)) {
 460         msg = message ("%q (through alias %q)", msg, sRef_unparse (s->ref));
 461       }
 462
 463       llgenindentmsg (msg, s->loc);
 464
 465       if (!showdeep) {
 466         break;
 467       }
 468
 469       s = s->previous;
 470     }
 471
 472   cstring_free (sname);
 473 }
 474
 475