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   /*@i32 free os? @*/
 124 }
 125
 126 static void tistable_grow (void)
 127 {
 128   o_usymIdSet *oldtable = tistable;
 129   int newsize = tistableentries + TISTABLEBASESIZE;
 130   int i;
 131
 132   llassert (tistablefree == 0);
 133
 134   tistable = (usymIdSet *) dmalloc (sizeof (tistable) * newsize);
 135
 136   for (i = 0; i < tistableentries; i++)
 137     {
 138       tistable[i] = oldtable[i];
 139     }
 140
 141   tistablefree = TISTABLEBASESIZE;
 142   sfree (oldtable);
 143 }
 144
 145 static void tistable_addDirectEntry (/*@only@*/ usymIdSet s)
 146 {
 147   if (tistablefree == 0)
 148     {
 149       tistable_grow ();
 150     }
 151
 152   tistable[tistableentries] = s;
 153   tistableentries++;
 154   tistablefree--;
 155 }
 156
 157 static int tistable_addEntry (/*@only@*/ usymIdSet s)
 158 {
 159   int i;
 160
 161
 162   for (i = 0; i < tistableentries; i++)
 163     {
 164       if (usymIdSet_compare (tistable[i], s) == 0)
 165         {
 166           /*@access usymIdSet@*/
 167           llassert (i == 0 || s != tistable[i]);
 168           /*@noaccess usymIdSet@*/
 169
 170           usymIdSet_free (s);
 171                   return i;
 172         }
 173     }
 174
 175   tistable_addDirectEntry (s);
 176   return (tistableentries - 1);
 177 }
 178
 179 static /*@observer@*/ usymIdSet tistable_fetch (typeIdSet t)
 180    /*@globals tistableentries, tistable@*/
 181    /*@modifies nothing;@*/
 182 {
 183   llassert (t >= 0 && t < tistableentries);
 184
 185   return tistable[t];
 186 }
 187
 188 typeIdSet typeIdSet_emptySet (void)
 189 {
 190   if (tistableentries == 0)
 191     {
 192       int val = tistable_addEntry (usymIdSet_new ());
 193
 194       llassert (val == 0);
 195     }
 196
 197   llassert (usymIdSet_isUndefined (tistable[0]));
 198   return 0;
 199 }
 200
 201 bool typeIdSet_member (typeIdSet t, typeId el)
 202 {
 203   usymIdSet u = tistable_fetch (t);
 204
 205   return usymIdSet_member (u, el);
 206 }
 207
 208 bool typeIdSet_isEmpty (typeIdSet t)
 209 {
 210   return (t == 0);
 211 }
 212
 213 typeIdSet typeIdSet_single (typeId t)
 214 {
 215   return (tistable_addEntry (usymIdSet_single (t)));
 216 }
 217
 218 typeIdSet typeIdSet_singleOpt (typeId t)
 219 {
 220   if (typeId_isValid (t))
 221     {
 222       return (tistable_addEntry (usymIdSet_single (t)));
 223     }
 224   else
 225     {
 226       return typeIdSet_empty;
 227     }
 228 }
 229
 230 typeIdSet typeIdSet_insert (typeIdSet t, typeId el)
 231 {
 232   usymIdSet u = tistable_fetch (t);
 233
 234   if (usymIdSet_member (u, el))
 235     {
 236       return t;
 237     }
 238   else
 239     {
 240       return (tistable_addEntry (usymIdSet_add (u, el)));
 241     }
 242 }
 243
 244 typeIdSet typeIdSet_removeFresh (typeIdSet t, typeId el)
 245 {
 246   return (tistable_addEntry (usymIdSet_removeFresh (tistable_fetch (t), el)));
 247 }
 248
 249 cstring typeIdSet_unparse (typeIdSet t)
 250 {
 251   return (usymIdSet_unparse (tistable_fetch (t)));
 252 }
 253
 254 int typeIdSet_compare (typeIdSet t1, typeIdSet t2)
 255 {
 256   return (int_compare (t1, t2));
 257 }
 258
 259 typeIdSet typeIdSet_subtract (typeIdSet s, typeIdSet t)
 260 {
 261   if (typeIdSet_isEmpty (t))
 262     {
 263       return s;
 264     }
 265   else
 266     {
 267       return (tistable_addEntry (usymIdSet_subtract (tistable_fetch (s),
 268                                                      tistable_fetch (t))));
 269     }
 270 }
 271
 272 cstring typeIdSet_dump (typeIdSet t)
 273 {
 274   return (message ("%d", t));
 275 }
 276
 277 typeIdSet typeIdSet_undump (char **s)
 278 {
 279   int i;
 280
 281
 282   i = reader_getInt (s);
 283
 284   llassert (i >= 0 && i < tistableentries);
 285   return (typeIdSet) i;
 286 }
 287
 288 typeIdSet typeIdSet_union (typeIdSet t1, typeIdSet t2)
 289 {
 290   if (t1 == typeIdSet_undefined)
 291     {
 292       return t2;
 293     }
 294   else if (t2 == typeIdSet_undefined)
 295     {
 296       return t1;
 297     }
 298   else
 299     {
 300       return (tistable_addEntry (usymIdSet_newUnion (tistable_fetch (t1),
 301                                                      tistable_fetch (t2))));
 302     }
 303 }