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 "exception_utils.h"
20 #include "string_hash.h"
21 
23  std::ostream &out,
24  const irept &irep)
25 {
26  write_string_ref(out, irep.id());
27 
28  forall_irep(it, irep.get_sub())
29  {
30  out.put('S');
31  reference_convert(*it, out);
32  }
33 
35  {
36  out.put('N');
37  write_string_ref(out, it->first);
38  reference_convert(it->second, out);
39  }
40 
42  {
43  out.put('C');
44  write_string_ref(out, it->first);
45  reference_convert(it->second, out);
46  }
47 
48  out.put(0); // terminator
49 }
50 
52  std::istream &in,
53  irept &irep)
54 {
55  std::size_t id=read_gb_word(in);
56 
57  if(id<ireps_container.ireps_on_read.size() &&
59  {
60  irep=ireps_container.ireps_on_read[id].second;
61  }
62  else
63  {
64  read_irep(in, irep);
65 
66  if(id >= ireps_container.ireps_on_read.size())
67  ireps_container.ireps_on_read.resize(1 + id * 2, {false, get_nil_irep()});
68 
69  // guard against self-referencing ireps
70  if(ireps_container.ireps_on_read[id].first)
71  throw deserialization_exceptiont("irep id read twice.");
72 
73  ireps_container.ireps_on_read[id] = {true, irep};
74  }
75 }
76 
78  std::istream &in,
79  irept &irep)
80 {
81  irep.clear();
82  irep.id(read_string_ref(in));
83 
84  while(in.peek()=='S')
85  {
86  in.get();
87  irep.get_sub().push_back(irept());
88  reference_convert(in, irep.get_sub().back());
89  }
90 
91  while(in.peek()=='N')
92  {
93  in.get();
94  irept &r=irep.add(read_string_ref(in));
95  reference_convert(in, r);
96  }
97 
98  while(in.peek()=='C')
99  {
100  in.get();
101  irept &r=irep.add(read_string_ref(in));
102  reference_convert(in, r);
103  }
104 
105  if(in.get()!=0)
106  {
107  throw deserialization_exceptiont("irep not terminated");
108  }
109 }
110 
115  const irept &irep,
116  std::ostream &out)
117 {
118  std::size_t h=ireps_container.irep_full_hash_container.number(irep);
119 
120  const auto res = ireps_container.ireps_on_write.insert(
121  {h, ireps_container.ireps_on_write.size()});
122 
123  write_gb_word(out, res.first->second);
124  if(res.second)
125  write_irep(out, irep);
126 }
127 
132 void write_gb_word(std::ostream &out, std::size_t u)
133 {
134 
135  while(true)
136  {
137  unsigned char value=u&0x7f;
138  u>>=7;
139 
140  if(u==0)
141  {
142  out.put(value);
143  break;
144  }
145 
146  out.put(value | 0x80);
147  }
148 }
149 
153 std::size_t irep_serializationt::read_gb_word(std::istream &in)
154 {
155  std::size_t res=0;
156 
157  unsigned shift_distance=0;
158 
159  while(in.good())
160  {
161  if(shift_distance >= sizeof(res) * 8)
162  throw deserialization_exceptiont("input number too large");
163 
164  unsigned char ch=static_cast<unsigned char>(in.get());
165  res|=(size_t(ch&0x7f))<<shift_distance;
166  shift_distance+=7;
167  if((ch&0x80)==0)
168  break;
169  }
170 
171  if(!in.good())
172  throw deserialization_exceptiont("unexpected end of input stream");
173 
174  return res;
175 }
176 
180 void write_gb_string(std::ostream &out, const std::string &s)
181 {
182  for(std::string::const_iterator it=s.begin();
183  it!=s.end();
184  ++it)
185  {
186  if(*it==0 || *it=='\\')
187  out.put('\\'); // escape specials
188  out << *it;
189  }
190 
191  out.put(0);
192 }
193 
198 {
199  char c;
200  size_t length=0;
201 
202  while((c=static_cast<char>(in.get()))!=0)
203  {
204  if(length>=read_buffer.size())
205  read_buffer.resize(read_buffer.size()*2, 0);
206 
207  if(c=='\\') // escaped chars
208  read_buffer[length]=static_cast<char>(in.get());
209  else
210  read_buffer[length]=c;
211 
212  length++;
213  }
214 
215  return irep_idt(std::string(read_buffer.data(), length));
216 }
217 
222  std::ostream &out,
223  const irep_idt &s)
224 {
225  size_t id=irep_id_hash()(s);
226  if(id>=ireps_container.string_map.size())
227  ireps_container.string_map.resize(id+1, false);
228 
230  write_gb_word(out, id);
231  else
232  {
233  ireps_container.string_map[id]=true;
234  write_gb_word(out, id);
235  write_gb_string(out, id2string(s));
236  }
237 }
238 
243 {
244  std::size_t id=read_gb_word(in);
245 
246  if(id>=ireps_container.string_rev_map.size())
247  ireps_container.string_rev_map.resize(1+id*2,
248  std::pair<bool, irep_idt>(false, irep_idt()));
249 
250  if(!ireps_container.string_rev_map[id].first)
251  {
252  irep_idt s=read_gb_string(in);
254  std::pair<bool, irep_idt>(true, s);
255  }
256 
257  return ireps_container.string_rev_map[id].second;
258 }
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:35
irep_serialization.h
irep_serializationt::reference_convert
void reference_convert(std::istream &, irept &irep)
Definition: irep_serialization.cpp:51
irept::clear
void clear()
Definition: irep.h:313
irep_serializationt::read_gb_string
irep_idt read_gb_string(std::istream &)
reads a string from the stream
Definition: irep_serialization.cpp:197
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:72
irept::add
irept & add(const irep_namet &name)
Definition: irep.cpp:305
irep_serializationt::ireps_containert::ireps_on_read
ireps_on_readt ireps_on_read
Definition: irep_serialization.h:35
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:153
irep_idt
dstringt irep_idt
Definition: irep.h:32
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
irept::get_named_sub
named_subt & get_named_sub()
Definition: irep.h:319
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:180
irep_serializationt::ireps_containert::ireps_on_write
ireps_on_writet ireps_on_write
Definition: irep_serialization.h:39
string_hash.h
irep_serializationt::write_irep
void write_irep(std::ostream &, const irept &irep)
Definition: irep_serialization.cpp:22
forall_named_irep
#define forall_named_irep(it, irep)
Definition: irep.h:70
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:132
irep_serializationt::read_irep
void read_irep(std::istream &, irept &irep)
Definition: irep_serialization.cpp:77
irept::id
const irep_idt & id() const
Definition: irep.h:259
irep_serializationt::ireps_containert::irep_full_hash_container
irep_full_hash_containert irep_full_hash_container
Definition: irep_serialization.h:37
irep_id_hash
dstring_hash irep_id_hash
Definition: irep.h:35
forall_irep
#define forall_irep(it, irep)
Definition: irep.h:62
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:317
irept::get_comments
named_subt & get_comments()
Definition: irep.h:321
irep_serializationt::read_string_ref
irep_idt read_string_ref(std::istream &)
Read a string reference from the stream.
Definition: irep_serialization.cpp:242
irept
Base class for tree-like data structures with sharing.
Definition: irep.h:156
get_nil_irep
const irept & get_nil_irep()
Definition: irep.cpp:55
r
static int8_t r
Definition: irep_hash.h:59
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:221