CBMC: /home/runner/work/cbmc/cbmc/src/solvers/flattening/boolbv_index.cpp Source File

CBMC
Loading...
Searching...
No Matches
boolbv_index.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#include "boolbv.h"
10
11#include <algorithm>
12
13#include <util/arith_tools.h>
14#include <util/byte_operators.h>
15#include <util/cprover_prefix.h>
16#include <util/pointer_expr.h>
17#include <util/pointer_offset_size.h>
18#include <util/simplify_expr.h>
19#include <util/std_expr.h>
20
22{
23 const exprt &array=expr.array();
24 const exprt &index=expr.index();
25
26 const typet &array_op_type = array.type();
27
28 bvt bv;
29
30 if(array_op_type.id()==ID_array)
31 {
34
35 // see if the array size is constant
36
38 {
39 // use array decision procedure
40
41 if(has_byte_operator(expr))
42 {
45 CHECK_RETURN(final_expr != expr);
47
48 // record type if array is a symbol
49 const exprt &final_array = final_expr.array();
50 if(
52 {
57 array_width_opt.value_or(0));
58 }
59
60 // make sure we have the index in the cache
61 convert_bv(final_expr.index());
62 }
63 else
64 {
65 // free variables
66 bv = prop.new_variables(boolbv_width(expr.type()));
67
69
70 // record type if array is a symbol
71 if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
72 {
75 array.get(ID_identifier), array_type, array_width_opt.value_or(0));
76 }
77
78 // make sure we have the index in the cache
79 convert_bv(index);
80 }
81
82 return bv;
83 }
84
85 // Must have a finite size
88
89 {
90 // see if the index address is constant
91 // many of these are compacted by simplify_expr
92 // but variable location writes will block this
94 if(maybe_index_value.has_value())
95 {
96 return convert_index(array, maybe_index_value.value());
97 }
98 }
99
100 // Special case : arrays of one thing (useful for constants)
101 // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same
102 // value, bit-patterns with the same value, etc. are treated like
103 // this rather than as a series of individual options.
104 #define UNIFORM_ARRAY_HACK
105 #ifdef UNIFORM_ARRAY_HACK
106 bool is_uniform = array.id() == ID_array_of;
107
108 if(array.is_constant() || array.id() == ID_array)
109 {
110 is_uniform = array.operands().size() <= 1 ||
111 std::all_of(
112 ++array.operands().begin(),
113 array.operands().end(),
114 [&array](const exprt &expr) {
115 return expr == to_multi_ary_expr(array).op0();
116 });
117 }
118
119 if(is_uniform && prop.has_set_to())
120 {
121 static int uniform_array_counter; // Temporary hack
122
123 const std::string identifier = CPROVER_PREFIX "internal_uniform_array_" +
124 std::to_string(uniform_array_counter++);
125
126 symbol_exprt result(identifier, expr.type());
127 bv = convert_bv(result);
128
129 // return an unconstrained value in case of an empty array (the access is
130 // necessarily out-of-bounds)
131 if(!array.has_operands())
132 return bv;
133
134 equal_exprt value_equality(result, to_multi_ary_expr(array).op0());
135
136 binary_relation_exprt lower_bound(
137 from_integer(0, index.type()), ID_le, index);
138 binary_relation_exprt upper_bound(
139 index, ID_lt, from_integer(array_size, index.type()));
140
141 and_exprt range_condition(std::move(lower_bound), std::move(upper_bound));
143 std::move(range_condition), std::move(value_equality));
144
145 // Simplify may remove the lower bound if the type
146 // is correct.
148
149 return bv;
150 }
151 #endif
152
153 #define ACTUAL_ARRAY_HACK
154 #ifdef ACTUAL_ARRAY_HACK
155 // More useful when updates to concrete locations in
156 // actual arrays are compacted by simplify_expr
157 if((array.is_constant() || array.id() == ID_array) && prop.has_set_to())
158 {
159 #ifdef CONSTANT_ARRAY_HACK
160 // TODO : Compile the whole array into a single relation
161 #endif
162
163 // Symbol for output
164 static int actual_array_counter; // Temporary hack
165
166 const std::string identifier = CPROVER_PREFIX "internal_actual_array_" +
167 std::to_string(actual_array_counter++);
168
169 symbol_exprt result(identifier, expr.type());
170 bv = convert_bv(result);
171
172 // add implications
173
174#ifdef COMPACT_EQUAL_CONST
175 bv_utils.equal_const_register(convert_bv(index)); // Definitely
176 bv_utils.equal_const_register(convert_bv(result)); // Maybe
177#endif
178
179 exprt::operandst::const_iterator it = array.operands().begin();
180
181 for(mp_integer i=0; i<array_size; i=i+1)
182 {
183 INVARIANT(
184 it != array.operands().end(),
185 "this loop iterates over the array, so `it` shouldn't be increased "
186 "past the array's end");
187
188 // Cache comparisons and equalities
190 equal_exprt(index, from_integer(i, index.type())),
191 equal_exprt(result, *it++))));
192 }
193
194 return bv;
195 }
196
197#endif
198
199
200 // TODO : As with constant index, there is a trade-off
201 // of when it is best to flatten the whole array and
202 // when it is best to use the array theory and then use
203 // one or more of the above encoding strategies.
204
205 // get literals for the whole array
206 const std::size_t width = boolbv_width(expr.type());
207
208 const bvt &array_bv =
210
211 // TODO: maybe a shifter-like construction would be better
212 // Would be a lot more compact but propagate worse
213
214 if(prop.has_set_to())
215 {
216 // free variables
217 bv = prop.new_variables(width);
218
219 // add implications
220
221#ifdef COMPACT_EQUAL_CONST
222 bv_utils.equal_const_register(convert_bv(index)); // Definitely
223#endif
224
226 equal_bv.resize(width);
227
228 for(mp_integer i=0; i<array_size; i=i+1)
229 {
230 mp_integer offset=i*width;
231
232 for(std::size_t j=0; j<width; j++)
233 equal_bv[j] = prop.lequal(
234 bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
235
237 convert(equal_exprt(index, from_integer(i, index.type()))),
238 prop.land(equal_bv)));
239 }
240 }
241 else
242 {
243 bv.resize(width);
244
245#ifdef COMPACT_EQUAL_CONST
246 bv_utils.equal_const_register(convert_bv(index)); // Definitely
247#endif
248
249 typet constant_type=index.type(); // type of index operand
250
252 array_size > 0,
253 "non-positive array sizes are forbidden in goto programs");
254
255 for(mp_integer i=0; i<array_size; i=i+1)
256 {
257 literalt e =
259
260 mp_integer offset=i*width;
261
262 for(std::size_t j=0; j<width; j++)
263 {
265
266 if(i==0) // this initializes bv
267 bv[j]=l;
268 else
269 bv[j]=prop.lselect(e, l, bv[j]);
270 }
271 }
272 }
273 }
274 else
275 return conversion_failed(expr);
276
277 return bv;
278}
279
282 const exprt &array,
283 const mp_integer &index)
284{
285 const array_typet &array_type = to_array_type(array.type());
286
287 std::size_t width = boolbv_width(array_type.element_type());
288
289 // TODO: If the underlying array can use one of the
290 // improvements given above then it may be better to use
291 // the array theory for short chains of updates and then
292 // the improved array handling rather than full flattening.
293 // Note that the calculation is non-trivial as the cost of
294 // full flattening is amortised against all uses of
295 // the array (constant and variable indexes) and updated
296 // versions of it.
297
298 const bvt &tmp=convert_bv(array); // recursive call
299
300 mp_integer offset=index*width;
301
302 if(offset>=0 &&
303 offset+width<=mp_integer(tmp.size()))
304 {
305 // in bounds
306
307 // The assertion below is disabled as we want to be able
308 // to run CBMC without simplifier.
309 // Expression simplification should remove these cases
310 // assert(array.id()!=ID_array_of &&
311 // array.id()!=ID_array);
312 // If not there are large improvements possible as above
313
314 std::size_t offset_int = numeric_cast_v<std::size_t>(offset);
315 return bvt(tmp.begin() + offset_int, tmp.begin() + offset_int + width);
316 }
317 else if(array.id() == ID_member || array.id() == ID_index)
318 {
319 // out of bounds for the component, but not necessarily outside the bounds
320 // of the underlying object
322 o.build(array, ns);
324
325 const auto subtype_bytes_opt =
326 pointer_offset_size(array_type.element_type(), ns);
327 CHECK_RETURN(subtype_bytes_opt.has_value());
328
331 o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),
332 ns);
333
336
337 return convert_bv(be);
338 }
339 else if(
340 array.id() == ID_byte_extract_big_endian ||
342 {
344
345 const auto subtype_bytes_opt =
346 pointer_offset_size(array_type.element_type(), ns);
347 CHECK_RETURN(subtype_bytes_opt.has_value());
348
349 // add offset to index
352 byte_extract_expr.offset(),
354 index * (*subtype_bytes_opt), byte_extract_expr.offset().type())},
355 ns);
356
358 be.offset() = new_offset;
359 be.type() = array_type.element_type();
360
361 return convert_bv(be);
362 }
363 else
364 {
365 // out of bounds
366 return prop.new_variables(width);
367 }
368}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bool has_byte_operator(const exprt &src)
Return true iff src or one of its operands contain a byte extract or byte update expression.
byte_extract_exprt make_byte_extract(const exprt &_op, const exprt &_offset, const typet &_type)
Construct a byte_extract_exprt with endianness and byte width matching the current configuration.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:566
Boolean AND All operands must be boolean, and the result is always boolean.
Definition std_expr.h:2043
Arrays with given size.
Definition std_types.h:806
const namespacet & ns
Definition arrays.h:65
void record_array_index(const index_exprt &expr)
Definition arrays.cpp:45
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:784
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
Definition boolbv_map.cpp:41
virtual std::optional< std::size_t > get_width_opt(const typet &type) const
Definition boolbv_width.h:31
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition boolbv.cpp:40
bool is_unbounded_array(const typet &type) const override
Definition boolbv.cpp:534
boolbv_widtht bv_width
Definition boolbv.h:120
bv_utilst bv_utils
Definition boolbv.h:121
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition boolbv.cpp:95
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:106
boolbv_mapt map
Definition boolbv.h:127
Expression of type type extracted from some object op starting at position offset (given in number of...
Equality.
Definition std_expr.h:1339
Base class for all expressions.
Definition expr.h:57
bool has_operands() const
Return true if there is at least one operand.
Definition expr.h:92
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:213
typet & type()
Return the type of the expression.
Definition expr.h:85
operandst & operands()
Definition expr.h:95
Boolean implication.
Definition std_expr.h:2154
Array index operator.
Definition std_expr.h:1431
exprt & index()
Definition std_expr.h:1471
exprt & array()
Definition std_expr.h:1461
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:388
Split an expression into a base object and a (byte) offset.
Definition pointer_expr.h:181
exprt & offset()
Definition pointer_expr.h:223
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
The plus expression Associativity is not specified.
Definition std_expr.h:1006
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
propt & prop
void l_set_to_true(literalt a)
Definition prop.h:52
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition prop.cpp:30
virtual literalt lequal(literalt a, literalt b)=0
virtual bool has_set_to() const
Definition prop.h:81
Expression to hold a symbol (variable)
Definition std_expr.h:132
The type of an expression, extends irept.
Definition type.h:29
#define CPROVER_PREFIX
static exprt implication(exprt lhs, exprt rhs)
std::vector< literalt > bvt
Definition literal.h:201
API to expression classes for Pointers.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
Pointer Logic.
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#define CHECK_RETURN(CONDITION)
Definition invariant.h:495
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1494
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition std_expr.h:991
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3078
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:887

AltStyle によって変換されたページ (->オリジナル) /