cprover
irep_serialization.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: binary irep conversions with hashing
4 
5 Author: CM Wintersteiger
6 
7 Date: May 2007
8 
9 \*******************************************************************/
10 
13 
14 #include "irep_serialization.h"
15 
16 #include <sstream>
17 #include <iostream>
18 
19 #include "string_hash.h"
20 
22  std::ostream &out,
23  const irept &irep)
24 {
25  write_string_ref(out, irep.id());
26 
27  forall_irep(it, irep.get_sub())
28  {
29  out.put('S');
30  reference_convert(*it, out);
31  }
32 
34  {
35  out.put('N');
36  write_string_ref(out, it->first);
37  reference_convert(it->second, out);
38  }
39 
41  {
42  out.put('C');
43  write_string_ref(out, it->first);
44  reference_convert(it->second, out);
45  }
46 
47  out.put(0); // terminator
48 }
49 
51  std::istream &in,
52  irept &irep)
53 {
54  std::size_t id = read_gb_word(in);
55 
56  if(id < ireps_container.ireps_on_read.size() &&
58  {
59  irep = ireps_container.ireps_on_read[id].second;
60  }
61  else
62  {
63  read_irep(in, irep);
64  insert_on_read(id, irep);
65  }
66 }
67 
69  std::istream &in,
70  irept &irep)
71 {
72  irep.clear();
73  irep.id(read_string_ref(in));
74 
75  while(in.peek()=='S')
76  {
77  in.get();
78  irep.get_sub().push_back(irept());
79  reference_convert(in, irep.get_sub().back());
80  }
81 
82  while(in.peek()=='N')
83  {
84  in.get();
85  irept &r=irep.add(read_string_ref(in));
86  reference_convert(in, r);
87  }
88 
89  while(in.peek()=='C')
90  {
91  in.get();
92  irept &r=irep.add(read_string_ref(in));
93  reference_convert(in, r);
94  }
95 
96  if(in.get()!=0)
97  {
98  std::cerr << "irep not terminated\n";
99  throw 0;
100  }
101 }
102 
104  const irept &irep,
105  std::ostream &out)
106 {
107  std::size_t h=ireps_container.irep_full_hash_container.number(irep);
108 
109  // should be merged with insert
110  ireps_containert::ireps_on_writet::const_iterator fi=
112 
113  if(fi==ireps_container.ireps_on_write.end())
114  {
115  size_t id=insert_on_write(h);
116  write_gb_word(out, id);
117  write_irep(out, irep);
118  }
119  else
120  {
121  write_gb_word(out, fi->second);
122  }
123 }
124 
128 std::size_t irep_serializationt::insert_on_write(std::size_t h)
129 {
130  std::pair<ireps_containert::ireps_on_writet::const_iterator, bool> res=
132  std::make_pair(h, ireps_container.ireps_on_write.size()));
133 
134  if(!res.second)
135  return ireps_container.ireps_on_write.size();
136  else
137  return res.first->second;
138 }
139 
145  std::size_t id,
146  const irept &i)
147 {
148  if(id>=ireps_container.ireps_on_read.size())
149  ireps_container.ireps_on_read.resize(1+id*2,
150  std::pair<bool, irept>(false, get_nil_irep()));
151 
152  if(ireps_container.ireps_on_read[id].first)
153  throw "irep id read twice.";
154  else
155  {
157  std::pair<bool, irept>(true, i);
158  }
159 
160  return id;
161 }
162 
166 void write_gb_word(std::ostream &out, std::size_t u)
167 {
168  // we write 7 bits each time, until we have zero
169 
170  while(true)
171  {
172  unsigned char value=u&0x7f;
173  u>>=7;
174 
175  if(u==0)
176  {
177  out.put(value);
178  break;
179  }
180 
181  out.put(value | 0x80);
182  }
183 }
184 
188 std::size_t irep_serializationt::read_gb_word(std::istream &in)
189 {
190  std::size_t res=0;
191 
192  unsigned shift_distance=0;
193 
194  while(in.good())
195  {
196  unsigned char ch=in.get();
197  res|=(size_t(ch&0x7f))<<shift_distance;
198  shift_distance+=7;
199  if((ch&0x80)==0)
200  break;
201  }
202 
203  return res;
204 }
205 
209 void write_gb_string(std::ostream &out, const std::string &s)
210 {
211  for(std::string::const_iterator it=s.begin();
212  it!=s.end();
213  ++it)
214  {
215  if(*it==0 || *it=='\\')
216  out.put('\\'); // escape specials
217  out << *it;
218  }
219 
220  out.put(0);
221 }
222 
227 {
228  char c;
229  size_t length=0;
230 
231  while((c = in.get()) != 0)
232  {
233  if(length>=read_buffer.size())
234  read_buffer.resize(read_buffer.size()*2, 0);
235 
236  if(c=='\\') // escaped chars
237  read_buffer[length] = in.get();
238  else
239  read_buffer[length] = c;
240 
241  length++;
242  }
243 
244  return irep_idt(std::string(read_buffer.data(), length));
245 }
246 
251  std::ostream &out,
252  const irep_idt &s)
253 {
254  size_t id=irep_id_hash()(s);
255  if(id>=ireps_container.string_map.size())
256  ireps_container.string_map.resize(id+1, false);
257 
259  write_gb_word(out, id);
260  else
261  {
262  ireps_container.string_map[id]=true;
263  write_gb_word(out, id);
264  write_gb_string(out, id2string(s));
265  }
266 }
267 
272 {
273  std::size_t id = read_gb_word(in);
274 
275  if(id>=ireps_container.string_rev_map.size())
276  ireps_container.string_rev_map.resize(1+id*2,
277  std::pair<bool, irep_idt>(false, irep_idt()));
278 
279  if(ireps_container.string_rev_map[id].first)
280  {
281  return ireps_container.string_rev_map[id].second;
282  }
283  else
284  {
285  irep_idt s=read_gb_string(in);
287  std::pair<bool, irep_idt>(true, s);
288  return ireps_container.string_rev_map[id].second;
289  }
290 }
const irept & get_nil_irep()
Definition: irep.cpp:56
static int8_t r
Definition: irep_hash.h:59
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
std::vector< char > read_buffer
void write_gb_word(std::ostream &out, std::size_t u)
outputs 4 characters for a long, most-significant byte first
irep_idt read_string_ref(std::istream &)
reads a string reference from the stream
#define forall_named_irep(it, irep)
Definition: irep.h:70
subt & get_sub()
Definition: irep.h:245
std::size_t insert_on_write(std::size_t h)
inserts an irep into the hashtable
const irep_idt & id() const
Definition: irep.h:189
void reference_convert(std::istream &, irept &irep)
dstring_hash irep_id_hash
Definition: irep.h:35
named_subt & get_comments()
Definition: irep.h:249
irep_full_hash_containert irep_full_hash_container
Base class for tree-like data structures with sharing.
Definition: irep.h:87
void write_irep(std::ostream &, const irept &irep)
ireps_containert & ireps_container
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
binary irep conversions with hashing
named_subt & get_named_sub()
Definition: irep.h:247
irep_idt read_gb_string(std::istream &)
reads a string from the stream
void write_string_ref(std::ostream &, const irep_idt &)
outputs the string reference
void clear()
Definition: irep.h:241
irept & add(const irep_namet &name)
Definition: irep.cpp:306
string hashing
static std::size_t read_gb_word(std::istream &)
reads 4 characters and builds a long int from them
std::size_t insert_on_read(std::size_t id, const irept &)
inserts an irep into the hashtable, but only the id-hashtable (only to be used upon reading ireps fro...
dstringt irep_idt
Definition: irep.h:32
size_t number(const irept &irep)
void read_irep(std::istream &, irept &irep)
#define forall_irep(it, irep)
Definition: irep.h:62