src/typeIdSet.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 ** typeIdSet.c
  26 */
  27
  28 # include "splintMacros.nf"
  29 # include "basic.h"
  30
  31 /*@constant int TISTABLEBASESIZE;@*/
  32 # define TISTABLEBASESIZE LARGEBASESIZE
  33
  34 static int tistableentries = 0;
  35 static int tistablefree = 0;
  36 typedef /*@only@*/ usymIdSet o_usymIdSet;
  37 static /*@only@*/ o_usymIdSet *tistable;
  38 static void tistable_addDirectEntry (/*@only@*/ usymIdSet p_s)
  39    /*@modifies tistable, tistableentries, tistablefree@*/;
  40
  41 void typeIdSet_initMod (void)
  42    /*@globals undef tistable;@*/
  43    /*@modifies tistable, tistablefree;@*/
  44 {
  45   llassert (tistableentries == 0 && tistablefree == 0);
  46
  47   tistablefree = TISTABLEBASESIZE;
  48   tistable = (usymIdSet *) dmalloc (sizeof (tistable) * tistablefree);
  49   tistable[0] = usymIdSet_undefined;
  50   tistableentries = 1;
  51   tistablefree--;
  52 }
  53
  54 void typeIdSet_destroyMod (void)
  55    /*@globals killed tistable, tistableentries@*/
  56 {
  57   int i;
  58
  59   for (i = 0; i < tistableentries; i++)
  60     {
  61       usymIdSet_free (tistable[i]);
  62     }
  63
  64   sfree (tistable);
  65   tistableentries = 0;
  66 }
  67
  68 void typeIdSet_dumpTable (FILE *fout)
  69 {
  70   int i;
  71
  72   /*
  73   ** Don't dump 0th entry
  74   */
  75
  76   for (i = 1; i < tistableentries; i++)
  77     {
  78       cstring s = usymIdSet_dump (tistable[i]);
  79
  80       fprintf (fout, "%s\n", cstring_toCharsSafe (s));
  81       cstring_free (s);
  82     }
  83 }
  84
  85 # if 0
  86 static /*@unused@*/ void tistable_printOut (void)
  87 {
  88   int i;
  89
  90   /*
  91   ** Don't dump 0th entry
  92   */
  93
  94   for (i = 1; i < tistableentries; i++)
  95     {
  96       cstring s = usymIdSet_unparse (tistable[i]);
  97
  98       fprintf (g_warningstream, "%d: %s\n", i, cstring_toCharsSafe (s));
  99       cstring_free (s);
 100     }
 101 }
 102 # endif
 103
 104 void typeIdSet_loadTable (FILE *fin)
 105 {
 106   char *s = mstring_create (MAX_DUMP_LINE_LENGTH);
 107   char *os = s;
 108
 109   llassert (tistableentries == 1);
 110
 111   s = reader_readLine (fin, s, MAX_DUMP_LINE_LENGTH);
 112
 113   while (s != NULL && *s != ';')
 114     {
 115       usymIdSet u = usymIdSet_undump (&s);
 116
 117       llassert (*s == '\0' || *s == '\n');
 118
 119       tistable_addDirectEntry (u);
 120       s = reader_readLine (fin, os, MAX_DUMP_LINE_LENGTH);
 121     }
 122 }
 123
 124 static void tistable_grow (void)
 125 {
 126   o_usymIdSet *oldtable = tistable;
 127   int newsize = tistableentries + TISTABLEBASESIZE;
 128   int i;
 129
 130   llassert (tistablefree == 0);
 131
 132   tistable = (usymIdSet *) dmalloc (sizeof (tistable) * newsize);
 133
 134   for (i = 0; i < tistableentries; i++)
 135     {
 136       tistable[i] = oldtable[i];
 137     }
 138
 139   tistablefree = TISTABLEBASESIZE;
 140   sfree (oldtable);
 141 }
 142
 143 static void tistable_addDirectEntry (/*@only@*/ usymIdSet s)
 144 {
 145   if (tistablefree == 0)
 146     {
 147       tistable_grow ();
 148     }
 149
 150   tistable[tistableentries] = s;
 151   tistableentries++;
 152   tistablefree--;
 153 }
 154
 155 static int tistable_addEntry (/*@only@*/ usymIdSet s)
 156 {
 157   int i;
 158
 159
 160   for (i = 0; i < tistableentries; i++)
 161     {
 162       if (usymIdSet_compare (tistable[i], s) == 0)
 163         {
 164           /*@access usymIdSet@*/
 165           llassert (i == 0 || s != tistable[i]);
 166           /*@noaccess usymIdSet@*/
 167
 168           usymIdSet_free (s);
 169                   return i;
 170         }
 171     }
 172
 173   tistable_addDirectEntry (s);
 174   return (tistableentries - 1);
 175 }
 176
 177 static /*@observer@*/ usymIdSet tistable_fetch (typeIdSet t)
 178    /*@globals tistableentries, tistable@*/
 179    /*@modifies nothing;@*/
 180 {
 181   llassert (t >= 0 && t < tistableentries);
 182
 183   return tistable[t];
 184 }
 185
 186 typeIdSet typeIdSet_emptySet (void)
 187 {
 188   if (tistableentries == 0)
 189     {
 190       int val = tistable_addEntry (usymIdSet_new ());
 191
 192       llassert (val == 0);
 193     }
 194
 195   llassert (usymIdSet_isUndefined (tistable[0]));
 196   return 0;
 197 }
 198
 199 bool typeIdSet_member (typeIdSet t, typeId el)
 200 {
 201   usymIdSet u = tistable_fetch (t);
 202   return usymIdSet_member (u, typeId_toUsymId (el));
 203 }
 204
 205 bool typeIdSet_isEmpty (typeIdSet t)
 206 {
 207   return (t == 0);
 208 }
 209
 210 typeIdSet typeIdSet_single (typeId t)
 211 {
 212   return (tistable_addEntry (usymIdSet_single (typeId_toUsymId (t))));
 213 }
 214
 215 typeIdSet typeIdSet_singleOpt (typeId t)
 216 {
 217   if (typeId_isValid (t))
 218     {
 219       return (tistable_addEntry (usymIdSet_single (typeId_toUsymId (t))));
 220     }
 221   else
 222     {
 223       return typeIdSet_empty;
 224     }
 225 }
 226
 227 typeIdSet typeIdSet_insert (typeIdSet t, typeId el)
 228 {
 229   usymIdSet u = tistable_fetch (t);
 230
 231   if (usymIdSet_member (u, typeId_toUsymId (el)))
 232     {
 233       return t;
 234     }
 235   else
 236     {
 237       return (tistable_addEntry (usymIdSet_add (u, typeId_toUsymId (el))));
 238     }
 239 }
 240
 241 typeIdSet typeIdSet_removeFresh (typeIdSet t, typeId el)
 242 {
 243   return (tistable_addEntry (usymIdSet_removeFresh (tistable_fetch (t), typeId_toUsymId (el))));
 244 }
 245
 246 cstring typeIdSet_unparse (typeIdSet t)
 247 {
 248   return (usymIdSet_unparse (tistable_fetch (t)));
 249 }
 250
 251 int typeIdSet_compare (typeIdSet t1, typeIdSet t2)
 252 {
 253   return (int_compare (t1, t2));
 254 }
 255
 256 typeIdSet typeIdSet_subtract (typeIdSet s, typeIdSet t)
 257 {
 258   if (typeIdSet_isEmpty (t))
 259     {
 260       return s;
 261     }
 262   else
 263     {
 264       return (tistable_addEntry (usymIdSet_subtract (tistable_fetch (s),
 265                                                      tistable_fetch (t))));
 266     }
 267 }
 268
 269 cstring typeIdSet_dump (typeIdSet t)
 270 {
 271   return (message ("%d", t));
 272 }
 273
 274 typeIdSet typeIdSet_undump (char **s)
 275 {
 276   int i;
 277
 278
 279   i = reader_getInt (s);
 280
 281   llassert (i >= 0 && i < tistableentries);
 282   return (typeIdSet) i;
 283 }
 284
 285 typeIdSet typeIdSet_union (typeIdSet t1, typeIdSet t2)
 286 {
 287   if (t1 == typeIdSet_undefined)
 288     {
 289       return t2;
 290     }
 291   else if (t2 == typeIdSet_undefined)
 292     {
 293       return t1;
 294     }
 295   else
 296     {
 297       return (tistable_addEntry (usymIdSet_newUnion (tistable_fetch (t1),
 298                                                      tistable_fetch (t2))));
 299     }
 300 }