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 while(in.peek()=='N')
79 {
80 in.get();
82 named_sub.emplace(id, reference_convert(in));
83 }
84
85 while(in.peek()=='C')
86 {
87 in.get();
89 named_sub.emplace(id, reference_convert(in));
90 }
91
92 if(in.get()!=0)
93 {
94 throw deserialization_exceptiont("irep not terminated");
95 }
96
97 return irept(std::move(id), std::move(named_sub), std::move(sub));
98}
99
104 const irept &irep,
105 std::ostream &out)
106{
108
109 const auto res = ireps_container.ireps_on_write.insert(
111
112 write_gb_word(out, res.first->second);
113 if(res.second)
114 write_irep(out, irep);
115}
116
121void write_gb_word(std::ostream &out, std::size_t u)
122{
123
124 while(true)
125 {
126 unsigned char value=u&0x7f;
127 u>>=7;
128
129 if(u==0)
130 {
131 out.put(value);
132 break;
133 }
134
135 out.put(value | 0x80);
136 }
137}
138
142std::size_t irep_serializationt::read_gb_word(std::istream &in)
143{
144 std::size_t res=0;
145
146 unsigned shift_distance=0;
147
148 while(in.good())
149 {
150 if(shift_distance >= sizeof(res) * CHAR_BIT)
151 throw deserialization_exceptiont("input number too large");
152
153 unsigned char ch=static_cast<unsigned char>(in.get());
154 res|=(size_t(ch&0x7f))<<shift_distance;
156 if((ch&0x80)==0)
157 break;
158 }
159
160 if(!in.good())
161 throw deserialization_exceptiont("unexpected end of input stream");
162
163 return res;
164}
165
169void write_gb_string(std::ostream &out, const std::string &s)
170{
171 for(std::string::const_iterator it=s.begin();
172 it!=s.end();
173 ++it)
174 {
175 if(*it==0 || *it=='\\')
176 out.put('\\'); // escape specials
177 out << *it;
178 }
179
180 out.put(0);
181}
182
187{
188 char c;
189 size_t length=0;
190
191 while((c=static_cast<char>(in.get()))!=0)
192 {
193 if(length>=read_buffer.size())
194 read_buffer.resize(read_buffer.size()*2, 0);
195
196 if(c=='\\') // escaped chars
197 read_buffer[length]=static_cast<char>(in.get());
198 else
199 read_buffer[length]=c;
200
201 length++;
202 }
203
204 return irep_idt(std::string(read_buffer.data(), length));
205}
206
211 std::ostream &out,
212 const irep_idt &s)
213{
214 size_t id=irep_id_hash()(s);
215 if(id>=ireps_container.string_map.size())
216 ireps_container.string_map.resize(id+1, false);
217
219 write_gb_word(out, id);
220 else
221 {
223 write_gb_word(out, id);
224 write_gb_string(out, id2string(s));
225 }
226}
227
232{
233 std::size_t id=read_gb_word(in);
234
235 if(id>=ireps_container.string_rev_map.size())
236 ireps_container.string_rev_map.resize(1+id*2,
237 std::pair<bool, irep_idt>(false, irep_idt()));
238
239 if(!ireps_container.string_rev_map[id].first)
240 {
243 std::pair<bool, irep_idt>(true, s);
244 }
245
246 return ireps_container.string_rev_map[id].second;
247}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
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:39
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:19
dstring_hash irep_id_hash
Definition irep.h:39
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.
dstringt irep_idt