CBMC
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 <climits>
17 #include <iostream>
18 
19 #include "exception_utils.h"
20 
22  std::ostream &out,
23  const irept &irep)
24 {
25  write_string_ref(out, irep.id());
26 
27  for(const auto &sub_irep : irep.get_sub())
28  {
29  out.put('S');
30  reference_convert(sub_irep, out);
31  }
32 
33  for(const auto &sub_irep_entry : irep.get_named_sub())
34  {
35  out.put('N');
36  write_string_ref(out, sub_irep_entry.first);
37  reference_convert(sub_irep_entry.second, out);
38  }
39 
40  out.put(0); // terminator
41 }
42 
44 {
45  std::size_t id=read_gb_word(in);
46 
47  if(
48  id >= ireps_container.ireps_on_read.size() ||
49  !ireps_container.ireps_on_read[id].first)
50  {
51  irept irep = read_irep(in);
52 
53  if(id >= ireps_container.ireps_on_read.size())
54  ireps_container.ireps_on_read.resize(1 + id * 2, {false, get_nil_irep()});
55 
56  // guard against self-referencing ireps
57  if(ireps_container.ireps_on_read[id].first)
58  throw deserialization_exceptiont("irep id read twice.");
59 
60  ireps_container.ireps_on_read[id] = {true, std::move(irep)};
61  }
62 
63  return ireps_container.ireps_on_read[id].second;
64 }
65 
67 {
68  irep_idt id = read_string_ref(in);
69  irept::subt sub;
70  irept::named_subt named_sub;
71 
72  while(in.peek()=='S')
73  {
74  in.get();
75  sub.push_back(reference_convert(in));
76  }
77 
78 #if NAMED_SUB_IS_FORWARD_LIST
79  irept::named_subt::iterator before = named_sub.before_begin();
80 #endif
81  while(in.peek()=='N')
82  {
83  in.get();
84  irep_idt id = read_string_ref(in);
85 #if NAMED_SUB_IS_FORWARD_LIST
86  named_sub.emplace_after(before, id, reference_convert(in));
87  ++before;
88 #else
89  named_sub.emplace(id, reference_convert(in));
90 #endif
91  }
92 
93  while(in.peek()=='C')
94  {
95  in.get();
96  irep_idt id = read_string_ref(in);
97 #if NAMED_SUB_IS_FORWARD_LIST
98  named_sub.emplace_after(before, id, reference_convert(in));
99  ++before;
100 #else
101  named_sub.emplace(id, reference_convert(in));
102 #endif
103  }
104 
105  if(in.get()!=0)
106  {
107  throw deserialization_exceptiont("irep not terminated");
108  }
109 
110  return irept(std::move(id), std::move(named_sub), std::move(sub));
111 }
112 
117  const irept &irep,
118  std::ostream &out)
119 {
120  std::size_t h=ireps_container.irep_full_hash_container.number(irep);
121 
122  const auto res = ireps_container.ireps_on_write.insert(
123  {h, ireps_container.ireps_on_write.size()});
124 
125  write_gb_word(out, res.first->second);
126  if(res.second)
127  write_irep(out, irep);
128 }
129 
134 void write_gb_word(std::ostream &out, std::size_t u)
135 {
136 
137  while(true)
138  {
139  unsigned char value=u&0x7f;
140  u>>=7;
141 
142  if(u==0)
143  {
144  out.put(value);
145  break;
146  }
147 
148  out.put(value | 0x80);
149  }
150 }
151 
155 std::size_t irep_serializationt::read_gb_word(std::istream &in)
156 {
157  std::size_t res=0;
158 
159  unsigned shift_distance=0;
160 
161  while(in.good())
162  {
163  if(shift_distance >= sizeof(res) * CHAR_BIT)
164  throw deserialization_exceptiont("input number too large");
165 
166  unsigned char ch=static_cast<unsigned char>(in.get());
167  res|=(size_t(ch&0x7f))<<shift_distance;
168  shift_distance+=7;
169  if((ch&0x80)==0)
170  break;
171  }
172 
173  if(!in.good())
174  throw deserialization_exceptiont("unexpected end of input stream");
175 
176  return res;
177 }
178 
182 void write_gb_string(std::ostream &out, const std::string &s)
183 {
184  for(std::string::const_iterator it=s.begin();
185  it!=s.end();
186  ++it)
187  {
188  if(*it==0 || *it=='\\')
189  out.put('\\'); // escape specials
190  out << *it;
191  }
192 
193  out.put(0);
194 }
195 
200 {
201  char c;
202  size_t length=0;
203 
204  while((c=static_cast<char>(in.get()))!=0)
205  {
206  if(length>=read_buffer.size())
207  read_buffer.resize(read_buffer.size()*2, 0);
208 
209  if(c=='\\') // escaped chars
210  read_buffer[length]=static_cast<char>(in.get());
211  else
212  read_buffer[length]=c;
213 
214  length++;
215  }
216 
217  return irep_idt(std::string(read_buffer.data(), length));
218 }
219 
224  std::ostream &out,
225  const irep_idt &s)
226 {
227  size_t id=irep_id_hash()(s);
228  if(id>=ireps_container.string_map.size())
229  ireps_container.string_map.resize(id+1, false);
230 
232  write_gb_word(out, id);
233  else
234  {
235  ireps_container.string_map[id]=true;
236  write_gb_word(out, id);
237  write_gb_string(out, id2string(s));
238  }
239 }
240 
245 {
246  std::size_t id=read_gb_word(in);
247 
248  if(id>=ireps_container.string_rev_map.size())
249  ireps_container.string_rev_map.resize(1+id*2,
250  std::pair<bool, irep_idt>(false, irep_idt()));
251 
252  if(!ireps_container.string_rev_map[id].first)
253  {
254  irep_idt s=read_gb_string(in);
256  std::pair<bool, irep_idt>(true, s);
257  }
258 
259  return ireps_container.string_rev_map[id].second;
260 }
exception_utils.h
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
irep_serialization.h
irep_serializationt::read_gb_string
irep_idt read_gb_string(std::istream &)
reads a string from the stream
Definition: irep_serialization.cpp:199
irep_serializationt::read_buffer
std::vector< char > read_buffer
Definition: irep_serialization.h:77
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition: exception_utils.h:79
irep_serializationt::ireps_containert::ireps_on_read
ireps_on_readt ireps_on_read
Definition: irep_serialization.h:35
irep_serializationt::reference_convert
const irept & reference_convert(std::istream &)
Definition: irep_serialization.cpp:43
irep_serializationt::ireps_containert::string_map
string_mapt string_map
Definition: irep_serialization.h:42
irep_serializationt::read_gb_word
static std::size_t read_gb_word(std::istream &)
Interpret a stream of byte as a 7-bit encoded unsigned number.
Definition: irep_serialization.cpp:155
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::named_subt
typename dt::named_subt named_subt
Definition: irep.h:161
irep_idt
dstringt irep_idt
Definition: irep.h:37
irep_serializationt::read_irep
irept read_irep(std::istream &)
Definition: irep_serialization.cpp:66
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:458
write_gb_string
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
Definition: irep_serialization.cpp:182
irep_serializationt::ireps_containert::ireps_on_write
ireps_on_writet ireps_on_write
Definition: irep_serialization.h:39
irep_serializationt::write_irep
void write_irep(std::ostream &, const irept &irep)
Definition: irep_serialization.cpp:21
write_gb_word
void write_gb_word(std::ostream &out, std::size_t u)
Write 7 bits of u each time, least-significant byte first, until we have zero.
Definition: irep_serialization.cpp:134
irept::id
const irep_idt & id() const
Definition: irep.h:396
irep_serializationt::ireps_containert::irep_full_hash_container
irep_full_hash_containert irep_full_hash_container
Definition: irep_serialization.h:37
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::subt
typename dt::subt subt
Definition: irep.h:160
irep_id_hash
dstring_hash irep_id_hash
Definition: irep.h:39
irep_hash_container_baset::number
std::size_t number(const irept &irep)
Definition: irep_hash_container.cpp:17
irep_serializationt::ireps_containert::string_rev_map
string_rev_mapt string_rev_map
Definition: irep_serialization.h:45
irept::get_sub
subt & get_sub()
Definition: irep.h:456
irep_serializationt::read_string_ref
irep_idt read_string_ref(std::istream &)
Read a string reference from the stream.
Definition: irep_serialization.cpp:244
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:359
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:20
irep_serializationt::ireps_container
ireps_containert & ireps_container
Definition: irep_serialization.h:76
irep_serializationt::write_string_ref
void write_string_ref(std::ostream &, const irep_idt &)
Output a string and maintain a reference to it.
Definition: irep_serialization.cpp:223