cprover
Loading...
Searching...
No Matches
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 <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');
31 }
32
33 for(const auto &sub_irep_entry : irep.get_named_sub())
34 {
35 out.put('N');
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() ||
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{
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();
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();
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{
121
122 const auto res = ireps_container.ireps_on_write.insert(
124
125 write_gb_word(out, res.first->second);
126 if(res.second)
127 write_irep(out, irep);
128}
129
134void 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
155std::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;
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
182void 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 {
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 {
256 std::pair<bool, irep_idt>(true, s);
257 }
258
259 return ireps_container.string_rev_map[id].second;
260}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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:37
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:372
subt & get_sub()
Definition irep.h:456
const irep_idt & id() const
Definition irep.h:396
named_subt & get_named_sub()
Definition irep.h:458
const irept & get_nil_irep()
Definition irep.cpp:20
dstring_hash irep_id_hash
Definition irep.h:39
dstringt irep_idt
Definition irep.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
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.