Skip to content

Commit e8728fc

Browse files
kroeningkroening
authored
Merge pull request #8182 from diffblue/update_bits_exprt
update_bits_exprt
2 parents e18fead + cefb96a commit e8728fc

File tree

9 files changed

+229
-124
lines changed

9 files changed

+229
-124
lines changed

‎src/solvers/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -128,6 +128,7 @@ SRC = $(BOOLEFORCE_SRC) \
128128
flattening/boolbv_unary_minus.cpp \
129129
flattening/boolbv_union.cpp \
130130
flattening/boolbv_update.cpp \
131+
flattening/boolbv_update_bits.cpp \
131132
flattening/boolbv_width.cpp \
132133
flattening/boolbv_with.cpp \
133134
flattening/bv_dimacs.cpp \

‎src/solvers/flattening/boolbv.h‎

Lines changed: 13 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ class overflow_result_exprt;
3939
class replication_exprt;
4040
class unary_overflow_exprt;
4141
class union_typet;
42+
class update_bits_exprt;
4243

4344
class boolbvt:public arrayst
4445
{
@@ -176,6 +177,7 @@ class boolbvt:public arrayst
176177
virtual bvt convert_member(const member_exprt &expr);
177178
virtual bvt convert_with(const with_exprt &expr);
178179
virtual bvt convert_update(const update_exprt &);
180+
virtual bvt convert_update_bits(const update_bits_exprt &);
179181
virtual bvt convert_case(const exprt &expr);
180182
virtual bvt convert_cond(const cond_exprt &);
181183
virtual bvt convert_shift(const binary_exprt &expr);
@@ -196,36 +198,38 @@ class boolbvt:public arrayst
196198
virtual bvt convert_saturating_add_sub(const binary_exprt &expr);
197199
virtual bvt convert_overflow_result(const overflow_result_exprt &expr);
198200

201+
bvt convert_update_bits(bvt src, const exprt &index, const bvt &new_value);
202+
199203
void convert_with(
200204
const typet &type,
201-
const exprt &op1,
202-
const exprt &op2,
205+
const exprt &where,
206+
const exprt &new_value,
203207
const bvt &prev_bv,
204208
bvt &next_bv);
205209

206210
void convert_with_bv(
207-
const exprt &op1,
208-
const exprt &op2,
211+
const exprt &index,
212+
const exprt &new_value,
209213
const bvt &prev_bv,
210214
bvt &next_bv);
211215

212216
void convert_with_array(
213217
const array_typet &type,
214-
const exprt &op1,
215-
const exprt &op2,
218+
const exprt &index,
219+
const exprt &new_value,
216220
const bvt &prev_bv,
217221
bvt &next_bv);
218222

219223
void convert_with_union(
220224
const union_typet &type,
221-
const exprt &op2,
225+
const exprt &new_value,
222226
const bvt &prev_bv,
223227
bvt &next_bv);
224228

225229
void convert_with_struct(
226230
const struct_typet &type,
227-
const exprt &op1,
228-
const exprt &op2,
231+
const exprt &where,
232+
const exprt &new_value,
229233
const bvt &prev_bv,
230234
bvt &next_bv);
231235

‎src/solvers/flattening/boolbv_update_bits.cpp‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
/*******************************************************************\
2+
3+
Module:
4+
5+
Author: Daniel Kroening, dkr@amazon.com
6+
7+
\*******************************************************************/
8+
9+
#include <util/bitvector_expr.h>
10+
11+
#include "boolbv.h"
12+
13+
bvt boolbvt::convert_update_bits(const update_bits_exprt &expr)
14+
{
15+
return convert_bv(expr.lower());
16+
}

‎src/solvers/flattening/boolbv_with.cpp‎

Lines changed: 69 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -6,18 +6,30 @@ Author: Daniel Kroening, kroening@kroening.com
66
77
\*******************************************************************/
88

9-
#include "boolbv.h"
10-
119
#include <util/arith_tools.h>
10+
#include <util/bitvector_expr.h>
1211
#include <util/c_types.h>
1312
#include <util/namespace.h>
1413
#include <util/std_expr.h>
1514

15+
#include "boolbv.h"
16+
1617
bvt boolbvt::convert_with(const with_exprt &expr)
1718
{
19+
auto &type = expr.type();
20+
21+
if(
22+
type.id() == ID_bv || type.id() == ID_unsignedbv ||
23+
type.id() == ID_signedbv)
24+
{
25+
PRECONDITION(expr.operands().size() == 3);
26+
return convert_bv(
27+
update_bits_exprt(expr.old(), expr.where(), expr.new_value()));
28+
}
29+
1830
bvt bv = convert_bv(expr.old());
1931

20-
std::size_t width=boolbv_width(expr.type());
32+
std::size_t width = boolbv_width(type);
2133

2234
if(width==0)
2335
{
@@ -47,8 +59,8 @@ bvt boolbvt::convert_with(const with_exprt &expr)
4759

4860
void boolbvt::convert_with(
4961
const typet &type,
50-
const exprt &op1,
51-
const exprt &op2,
62+
const exprt &where,
63+
const exprt &new_value,
5264
const bvt &prev_bv,
5365
bvt &next_bv)
5466
{
@@ -57,31 +69,43 @@ void boolbvt::convert_with(
5769
next_bv.resize(prev_bv.size());
5870

5971
if(type.id()==ID_array)
60-
return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
72+
return convert_with_array(
73+
to_array_type(type), where, new_value, prev_bv, next_bv);
6174
else if(type.id()==ID_bv ||
6275
type.id()==ID_unsignedbv ||
6376
type.id()==ID_signedbv)
64-
return convert_with_bv(op1, op2, prev_bv, next_bv);
77+
{
78+
// already done
79+
PRECONDITION(false);
80+
}
6581
else if(type.id()==ID_struct)
66-
return
67-
convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
82+
return convert_with_struct(
83+
to_struct_type(type), where, new_value, prev_bv, next_bv);
6884
else if(type.id() == ID_struct_tag)
6985
return convert_with(
70-
ns.follow_tag(to_struct_tag_type(type)), op1, op2, prev_bv, next_bv);
86+
ns.follow_tag(to_struct_tag_type(type)),
87+
where,
88+
new_value,
89+
prev_bv,
90+
next_bv);
7191
else if(type.id()==ID_union)
72-
return convert_with_union(to_union_type(type), op2, prev_bv, next_bv);
92+
return convert_with_union(to_union_type(type), new_value, prev_bv, next_bv);
7393
else if(type.id() == ID_union_tag)
7494
return convert_with(
75-
ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
95+
ns.follow_tag(to_union_tag_type(type)),
96+
where,
97+
new_value,
98+
prev_bv,
99+
next_bv);
76100

77101
DATA_INVARIANT_WITH_DIAGNOSTICS(
78102
false, "unexpected with type", irep_pretty_diagnosticst{type});
79103
}
80104

81105
void boolbvt::convert_with_array(
82106
const array_typet &type,
83-
const exprt &op1,
84-
const exprt &op2,
107+
const exprt &index,
108+
const exprt &new_value,
85109
const bvt &prev_bv,
86110
bvt &next_bv)
87111
{
@@ -100,89 +124,60 @@ void boolbvt::convert_with_array(
100124
"convert_with_array expects constant array size",
101125
irep_pretty_diagnosticst{type});
102126

103-
const bvt &op2_bv=convert_bv(op2);
127+
const bvt &new_value_bv = convert_bv(new_value);
104128

105129
DATA_INVARIANT_WITH_DIAGNOSTICS(
106-
*size * op2_bv.size() == prev_bv.size(),
107-
"convert_with_array: unexpected operand 2 width",
130+
*size * new_value_bv.size() == prev_bv.size(),
131+
"convert_with_array: unexpected new_value operand width",
108132
irep_pretty_diagnosticst{type});
109133

110134
// Is the index a constant?
111-
if(const auto op1_value = numeric_cast<mp_integer>(op1))
135+
if(const auto index_value_opt = numeric_cast<mp_integer>(index))
112136
{
113137
// Yes, it is!
114138
next_bv=prev_bv;
115139

116-
if(*op1_value >= 0 && *op1_value < *size) // bounds check
140+
if(*index_value_opt >= 0 && *index_value_opt < *size) // bounds check
117141
{
118142
const std::size_t offset =
119-
numeric_cast_v<std::size_t>(*op1_value * op2_bv.size());
143+
numeric_cast_v<std::size_t>(*index_value_opt * new_value_bv.size());
120144

121-
for(std::size_t j=0; j<op2_bv.size(); j++)
122-
next_bv[offset+j]=op2_bv[j];
145+
for(std::size_t j = 0; j < new_value_bv.size(); j++)
146+
next_bv[offset + j] = new_value_bv[j];
123147
}
124148

125149
return;
126150
}
127151

128-
typet counter_type=op1.type();
152+
typet counter_type = index.type();
129153

130154
for(mp_integer i=0; i<size; i=i+1)
131155
{
132156
exprt counter=from_integer(i, counter_type);
133157

134-
literalt eq_lit=convert(equal_exprt(op1, counter));
135-
136-
const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
137-
138-
for(std::size_t j=0; j<op2_bv.size(); j++)
139-
next_bv[offset+j]=
140-
prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
141-
}
142-
}
143-
144-
void boolbvt::convert_with_bv(
145-
const exprt &op1,
146-
const exprt &op2,
147-
const bvt &prev_bv,
148-
bvt &next_bv)
149-
{
150-
literalt l=convert(op2);
151-
152-
if(const auto op1_value = numeric_cast<mp_integer>(op1))
153-
{
154-
next_bv=prev_bv;
155-
156-
if(*op1_value < next_bv.size())
157-
next_bv[numeric_cast_v<std::size_t>(*op1_value)] = l;
158-
159-
return;
160-
}
161-
162-
typet counter_type=op1.type();
163-
164-
for(std::size_t i=0; i<prev_bv.size(); i++)
165-
{
166-
exprt counter=from_integer(i, counter_type);
158+
literalt eq_lit = convert(equal_exprt(index, counter));
167159

168-
literalt eq_lit=convert(equal_exprt(op1, counter));
160+
const std::size_t offset =
161+
numeric_cast_v<std::size_t>(i * new_value_bv.size());
169162

170-
next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
163+
for(std::size_t j = 0; j < new_value_bv.size(); j++)
164+
next_bv[offset + j] =
165+
prop.lselect(eq_lit, new_value_bv[j], prev_bv[offset + j]);
171166
}
172167
}
173168

174169
void boolbvt::convert_with_struct(
175170
const struct_typet &type,
176-
const exprt &op1,
177-
const exprt &op2,
171+
const exprt &where,
172+
const exprt &new_value,
178173
const bvt &prev_bv,
179174
bvt &next_bv)
180175
{
181176
next_bv=prev_bv;
182177

183-
const bvt &op2_bv=convert_bv(op2);
178+
const bvt &new_value_bv = convert_bv(new_value);
184179

185-
const irep_idt &component_name=op1.get(ID_component_name);
180+
const irep_idt &component_name = where.get(ID_component_name);
186181
const struct_typet::componentst &components=
187182
type.components();
188183

@@ -197,19 +192,19 @@ void boolbvt::convert_with_struct(
197192
if(c.get_name() == component_name)
198193
{
199194
DATA_INVARIANT_WITH_DIAGNOSTICS(
200-
subtype == op2.type(),
195+
subtype == new_value.type(),
201196
"with/struct: component '" + id2string(component_name) +
202197
"' type does not match",
203198
irep_pretty_diagnosticst{subtype},
204-
irep_pretty_diagnosticst{op2.type()});
199+
irep_pretty_diagnosticst{new_value.type()});
205200

206201
DATA_INVARIANT_WITH_DIAGNOSTICS(
207-
sub_width == op2_bv.size(),
208-
"convert_with_struct: unexpected operand op2 width",
202+
sub_width == new_value_bv.size(),
203+
"convert_with_struct: unexpected new_value operand width",
209204
irep_pretty_diagnosticst{type});
210205

211206
for(std::size_t i=0; i<sub_width; i++)
212-
next_bv[offset+i]=op2_bv[i];
207+
next_bv[offset + i] = new_value_bv[i];
213208

214209
break; // done
215210
}
@@ -220,22 +215,22 @@ void boolbvt::convert_with_struct(
220215

221216
void boolbvt::convert_with_union(
222217
const union_typet &type,
223-
const exprt &op2,
218+
const exprt &new_value,
224219
const bvt &prev_bv,
225220
bvt &next_bv)
226221
{
227222
next_bv=prev_bv;
228223

229-
const bvt &op2_bv=convert_bv(op2);
224+
const bvt &new_value_bv = convert_bv(new_value);
230225

231226
DATA_INVARIANT_WITH_DIAGNOSTICS(
232-
next_bv.size() >= op2_bv.size(),
233-
"convert_with_union: unexpected operand op2 width",
227+
next_bv.size() >= new_value_bv.size(),
228+
"convert_with_union: unexpected new_value operand width",
234229
irep_pretty_diagnosticst{type});
235230

236231
endianness_mapt map_u = endianness_map(type);
237-
endianness_mapt map_op2 = endianness_map(op2.type());
232+
endianness_mapt map_new_value = endianness_map(new_value.type());
238233

239-
for(std::size_t i = 0; i < op2_bv.size(); i++)
240-
next_bv[map_u.map_bit(i)] = op2_bv[map_op2.map_bit(i)];
234+
for(std::size_t i = 0; i < new_value_bv.size(); i++)
235+
next_bv[map_u.map_bit(i)] = new_value_bv[map_new_value.map_bit(i)];
241236
}

0 commit comments

Comments
 (0)