CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
irep_serialization.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: binary irep conversions with hashing
4
5Author: CM Wintersteiger
6
7Date: May 2007
8
9\*******************************************************************/
10
13
14#include "irep_serialization.h"
15
16#include "exception_utils.h"
17#include "string_container.h"
18
19#include <climits>
20#include <iostream>
21
23 std::ostream &out,
24 const irept &irep)
25{
26 write_string_ref(out, irep.id());
27
28 for(const auto &sub_irep : irep.get_sub())
29 {
30 out.put('S');
32 }
33
34 for(const auto &sub_irep_entry : irep.get_named_sub())
35 {
36 out.put('N');
39 }
40
41 out.put(0); // terminator
42}
43
45{
46 std::size_t id=read_gb_word(in);
47
48 if(
49 id >= ireps_container.ireps_on_read.size() ||
51 {
52 irept irep = read_irep(in);
53
54 if(id >= ireps_container.ireps_on_read.size())
55 ireps_container.ireps_on_read.resize(1 + id * 2, {false, get_nil_irep()});
56
57 // guard against self-referencing ireps
58 if(ireps_container.ireps_on_read[id].first)
59 throw deserialization_exceptiont("irep id read twice.");
60
61 ireps_container.ireps_on_read[id] = {true, std::move(irep)};
62 }
63
64 return ireps_container.ireps_on_read[id].second;
65}
66
68{
70 irept::subt sub;
71 irept::named_subt named_sub;
72
73 while(in.peek()=='S')
74 {
75 in.get();
76 sub.push_back(reference_convert(in));
77 }
78
79 while(in.peek()=='N')
80 {
81 in.get();
83 named_sub.emplace(id, reference_convert(in));
84 }
85
86 while(in.peek()=='C')
87 {
88 in.get();
90 named_sub.emplace(id, reference_convert(in));
91 }
92
93 if(in.get()!=0)
94 {
95 throw deserialization_exceptiont("irep not terminated");
96 }
97
98 return irept(std::move(id), std::move(named_sub), std::move(sub));
99}
100
105 const irept &irep,
106 std::ostream &out)
107{
109
110 const auto res = ireps_container.ireps_on_write.insert(
112
113 write_gb_word(out, res.first->second);
114 if(res.second)
115 write_irep(out, irep);
116}
117
122void write_gb_word(std::ostream &out, std::size_t u)
123{
124
125 while(true)
126 {
127 unsigned char value=u&0x7f;
128 u>>=7;
129
130 if(u==0)
131 {
132 out.put(value);
133 break;
134 }
135
136 out.put(value | 0x80);
137 }
138}
139
143std::size_t irep_serializationt::read_gb_word(std::istream &in)
144{
145 std::size_t res=0;
146
147 unsigned shift_distance=0;
148
149 while(in.good())
150 {
151 if(shift_distance >= sizeof(res) * CHAR_BIT)
152 throw deserialization_exceptiont("input number too large");
153
154 unsigned char ch=static_cast<unsigned char>(in.get());
155 res|=(size_t(ch&0x7f))<<shift_distance;
157 if((ch&0x80)==0)
158 break;
159 }
160
161 if(!in.good())
162 throw deserialization_exceptiont("unexpected end of input stream");
163
164 return res;
165}
166
170void write_gb_string(std::ostream &out, const std::string &s)
171{
172 for(std::string::const_iterator it=s.begin();
173 it!=s.end();
174 ++it)
175 {
176 if(*it==0 || *it=='\\')
177 out.put('\\'); // escape specials
178 out << *it;
179 }
180
181 out.put(0);
182}
183
188{
189 char c;
190 size_t length=0;
191
192 while((c=static_cast<char>(in.get()))!=0)
193 {
194 if(length>=read_buffer.size())
195 read_buffer.resize(read_buffer.size()*2, 0);
196
197 if(c=='\\') // escaped chars
198 read_buffer[length]=static_cast<char>(in.get());
199 else
200 read_buffer[length]=c;
201
202 length++;
203 }
204
205 return irep_idt(std::string(read_buffer.data(), length));
206}
207
212 std::ostream &out,
213 const irep_idt &s)
214{
215 size_t id = s.get_no();
216 if(id>=ireps_container.string_map.size())
217 ireps_container.string_map.resize(id+1, false);
218
220 write_gb_word(out, id);
221 else
222 {
224 write_gb_word(out, id);
225 write_gb_string(out, id2string(s));
226 }
227}
228
233{
234 std::size_t id=read_gb_word(in);
235
236 if(id>=ireps_container.string_rev_map.size())
237 ireps_container.string_rev_map.resize(1+id*2,
238 std::pair<bool, irep_idt>(false, irep_idt()));
239
240 if(!ireps_container.string_rev_map[id].first)
241 {
244 std::pair<bool, irep_idt>(true, s);
245 }
246
247 return ireps_container.string_rev_map[id].second;
248}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
unsigned get_no() const
Definition dstring.h:182
std::size_t number(const irept &irep)
irep_full_hash_containert irep_full_hash_container
ireps_containert & ireps_container
void write_string_ref(std::ostream &, const irep_idt &)
Output a string and maintain a reference to it.
irept read_irep(std::istream &)
static std::size_t read_gb_word(std::istream &)
Interpret a stream of byte as a 7-bit encoded unsigned number.
void write_irep(std::ostream &, const irept &irep)
std::vector< char > read_buffer
const irept & reference_convert(std::istream &)
irep_idt read_string_ref(std::istream &)
Read a string reference from the stream.
irep_idt read_gb_string(std::istream &)
reads a string from the stream
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition irep.h:364
subt & get_sub()
Definition irep.h:448
const irep_idt & id() const
Definition irep.h:388
named_subt & get_named_sub()
Definition irep.h:450
const irept & get_nil_irep()
Definition irep.cpp:19
const std::string & id2string(const irep_idt &d)
Definition irep.h:44
void write_gb_string(std::ostream &out, const std::string &s)
outputs the string and then a zero byte.
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.
binary irep conversions with hashing
void write_gb_word(std::ostream &, std::size_t)
Write 7 bits of u each time, least-significant byte first, until we have zero.
void write_gb_string(std::ostream &, const std::string &)
outputs the string and then a zero byte.
Container for C-Strings.
dstringt irep_idt