cprover
Toggle main menu visibility
Loading...
Searching...
No Matches
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 "
exception_utils.h
"
17
#include "
string_container.h
"
18
19
#include <climits>
20
#include <iostream>
21
22
void
irep_serializationt::write_irep
(
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'
);
31
reference_convert
(sub_irep, out);
32
}
33
34
for
(
const
auto
&sub_irep_entry : irep.
get_named_sub
())
35
{
36
out.put(
'N'
);
37
write_string_ref
(out, sub_irep_entry.first);
38
reference_convert
(sub_irep_entry.second, out);
39
}
40
41
out.put(0);
// terminator
42
}
43
44
const
irept
&
irep_serializationt::reference_convert
(std::istream &in)
45
{
46
std::size_t
id
=
read_gb_word
(in);
47
48
if
(
49
id
>=
ireps_container
.ireps_on_read.size() ||
50
!
ireps_container
.ireps_on_read[
id
].first)
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
67
irept
irep_serializationt::read_irep
(std::istream &in)
68
{
69
irep_idt
id
=
read_string_ref
(in);
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();
82
irep_idt
id
=
read_string_ref
(in);
83
named_sub.emplace(
id
,
reference_convert
(in));
84
}
85
86
while
(in.peek()==
'C'
)
87
{
88
in.get();
89
irep_idt
id
=
read_string_ref
(in);
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
104
void
irep_serializationt::reference_convert
(
105
const
irept
&irep,
106
std::ostream &out)
107
{
108
std::size_t h=
ireps_container
.irep_full_hash_container.number(irep);
109
110
const
auto
res =
ireps_container
.ireps_on_write.insert(
111
{h,
ireps_container
.ireps_on_write.size()});
112
113
write_gb_word
(out, res.first->second);
114
if
(res.second)
115
write_irep
(out, irep);
116
}
117
122
void
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
143
std::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;
156
shift_distance+=7;
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
170
void
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
187
irep_idt
irep_serializationt::read_gb_string
(std::istream &in)
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
211
void
irep_serializationt::write_string_ref
(
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
219
if
(
ireps_container
.string_map[
id
])
220
write_gb_word
(out,
id
);
221
else
222
{
223
ireps_container
.string_map[id]=
true
;
224
write_gb_word
(out,
id
);
225
write_gb_string
(out,
id2string
(s));
226
}
227
}
228
232
irep_idt
irep_serializationt::read_string_ref
(std::istream &in)
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
{
242
irep_idt
s=
read_gb_string
(in);
243
ireps_container
.string_rev_map[id]=
244
std::pair<bool, irep_idt>(
true
, s);
245
}
246
247
return
ireps_container
.string_rev_map[id].second;
248
}
deserialization_exceptiont
Thrown when failing to deserialize a value from some low level format, like JSON or raw bytes.
Definition
exception_utils.h:80
dstringt::get_no
unsigned get_no() const
Definition
dstring.h:182
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:211
irep_serializationt::read_irep
irept read_irep(std::istream &)
Definition
irep_serialization.cpp:67
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:143
irep_serializationt::write_irep
void write_irep(std::ostream &, const irept &irep)
Definition
irep_serialization.cpp:22
irep_serializationt::read_buffer
std::vector< char > read_buffer
Definition
irep_serialization.h:77
irep_serializationt::reference_convert
const irept & reference_convert(std::istream &)
Definition
irep_serialization.cpp:44
irep_serializationt::read_string_ref
irep_idt read_string_ref(std::istream &)
Read a string reference from the stream.
Definition
irep_serialization.cpp:232
irep_serializationt::read_gb_string
irep_idt read_gb_string(std::istream &)
reads a string from the stream
Definition
irep_serialization.cpp:187
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition
irep.h:364
irept::get_sub
subt & get_sub()
Definition
irep.h:448
irept::id
const irep_idt & id() const
Definition
irep.h:388
irept::get_named_sub
named_subt & get_named_sub()
Definition
irep.h:450
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::named_subt
typename dt::named_subt named_subt
Definition
irep.h:153
sharing_treet< irept, forward_list_as_mapt< irep_idt, irept > >::subt
typename dt::subt subt
Definition
irep.h:152
exception_utils.h
get_nil_irep
const irept & get_nil_irep()
Definition
irep.cpp:19
id2string
const std::string & id2string(const irep_idt &d)
Definition
irep.h:44
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:170
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:122
irep_serialization.h
binary irep conversions with hashing
write_gb_word
void write_gb_word(std::ostream &, std::size_t)
Write 7 bits of u each time, least-significant byte first, until we have zero.
Definition
irep_serialization.cpp:122
write_gb_string
void write_gb_string(std::ostream &, const std::string &)
outputs the string and then a zero byte.
Definition
irep_serialization.cpp:170
string_container.h
Container for C-Strings.
irep_idt
dstringt irep_idt
Definition
verification_result.h:16
util
irep_serialization.cpp
Generated by
1.17.0