cprover
boolbv_index.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: 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/cprover_prefix.h>
15 #include <util/pointer_expr.h>
17 #include <util/simplify_expr.h>
18 #include <util/std_expr.h>
19 
21 
23 {
24  const exprt &array=expr.array();
25  const exprt &index=expr.index();
26 
27  const typet &array_op_type = array.type();
28 
29  bvt bv;
30 
31  if(array_op_type.id()==ID_array)
32  {
33  const array_typet &array_type=
34  to_array_type(array_op_type);
35 
36  std::size_t width=boolbv_width(expr.type());
37 
38  if(width==0)
39  return conversion_failed(expr);
40 
41  // see if the array size is constant
42 
43  if(is_unbounded_array(array_type))
44  {
45  // use array decision procedure
46 
47  if(has_byte_operator(expr))
48  {
49  const index_exprt final_expr =
51  CHECK_RETURN(final_expr != expr);
52  bv = convert_bv(final_expr);
53 
54  // record type if array is a symbol
55  const exprt &final_array = final_expr.array();
56  if(
57  final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol)
58  {
59  std::size_t width = boolbv_width(array_type);
60  (void)map.get_literals(
61  final_array.get(ID_identifier), array_type, width);
62  }
63 
64  // make sure we have the index in the cache
65  convert_bv(final_expr.index());
66  }
67  else
68  {
69  // free variables
70  bv.reserve(width);
71  for(std::size_t i = 0; i < width; i++)
72  bv.push_back(prop.new_variable());
73 
74  record_array_index(expr);
75 
76  // record type if array is a symbol
77  if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
78  {
79  std::size_t width = boolbv_width(array_type);
80  (void)map.get_literals(array.get(ID_identifier), array_type, width);
81  }
82 
83  // make sure we have the index in the cache
84  convert_bv(index);
85  }
86 
87  return bv;
88  }
89 
90  // Must have a finite size
91  mp_integer array_size =
92  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
93 
94  {
95  // see if the index address is constant
96  // many of these are compacted by simplify_expr
97  // but variable location writes will block this
98  auto maybe_index_value = numeric_cast<mp_integer>(index);
99  if(maybe_index_value.has_value())
100  {
101  return convert_index(array, maybe_index_value.value());
102  }
103  }
104 
105  // Special case : arrays of one thing (useful for constants)
106  // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same
107  // value, bit-patterns with the same value, etc. are treated like
108  // this rather than as a series of individual options.
109  #define UNIFORM_ARRAY_HACK
110  #ifdef UNIFORM_ARRAY_HACK
111  bool is_uniform = array.id() == ID_array_of;
112 
113  if(array.id() == ID_constant || array.id() == ID_array)
114  {
115  is_uniform = array.operands().size() <= 1 ||
116  std::all_of(
117  ++array.operands().begin(),
118  array.operands().end(),
119  [&array](const exprt &expr) {
120  return expr == to_multi_ary_expr(array).op0();
121  });
122  }
123 
124  if(is_uniform && prop.has_set_to())
125  {
126  static int uniform_array_counter; // Temporary hack
127 
128  const std::string identifier = CPROVER_PREFIX "internal_uniform_array_" +
129  std::to_string(uniform_array_counter++);
130 
131  symbol_exprt result(identifier, expr.type());
132  bv = convert_bv(result);
133 
134  // return an unconstrained value in case of an empty array (the access is
135  // necessarily out-of-bounds)
136  if(!array.has_operands())
137  return bv;
138 
139  equal_exprt value_equality(result, to_multi_ary_expr(array).op0());
140 
141  binary_relation_exprt lower_bound(
142  from_integer(0, index.type()), ID_le, index);
143  binary_relation_exprt upper_bound(
144  index, ID_lt, from_integer(array_size, index.type()));
145 
146  and_exprt range_condition(std::move(lower_bound), std::move(upper_bound));
147  implies_exprt implication(
148  std::move(range_condition), std::move(value_equality));
149 
150  // Simplify may remove the lower bound if the type
151  // is correct.
152  prop.l_set_to_true(convert(simplify_expr(implication, ns)));
153 
154  return bv;
155  }
156  #endif
157 
158  #define ACTUAL_ARRAY_HACK
159  #ifdef ACTUAL_ARRAY_HACK
160  // More useful when updates to concrete locations in
161  // actual arrays are compacted by simplify_expr
162  if((array.id()==ID_constant || array.id()==ID_array) &&
163  prop.has_set_to())
164  {
165  #ifdef CONSTANT_ARRAY_HACK
166  // TODO : Compile the whole array into a single relation
167  #endif
168 
169  // Symbol for output
170  static int actual_array_counter; // Temporary hack
171 
172  const std::string identifier = CPROVER_PREFIX "internal_actual_array_" +
173  std::to_string(actual_array_counter++);
174 
175  symbol_exprt result(identifier, expr.type());
176  bv = convert_bv(result);
177 
178  // add implications
179 
180 #ifdef COMPACT_EQUAL_CONST
181  bv_utils.equal_const_register(convert_bv(index)); // Definitely
182  bv_utils.equal_const_register(convert_bv(result)); // Maybe
183 #endif
184 
185  exprt::operandst::const_iterator it = array.operands().begin();
186 
187  for(mp_integer i=0; i<array_size; i=i+1)
188  {
189  INVARIANT(
190  it != array.operands().end(),
191  "this loop iterates over the array, so `it` shouldn't be increased "
192  "past the array's end");
193 
194  // Cache comparisons and equalities
196  equal_exprt(index, from_integer(i, index.type())),
197  equal_exprt(result, *it++))));
198  }
199 
200  return bv;
201  }
202 
203 #endif
204 
205 
206  // TODO : As with constant index, there is a trade-off
207  // of when it is best to flatten the whole array and
208  // when it is best to use the array theory and then use
209  // one or more of the above encoding strategies.
210 
211  // get literals for the whole array
212 
213  const bvt &array_bv =
214  convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));
215 
216  // TODO: maybe a shifter-like construction would be better
217  // Would be a lot more compact but propagate worse
218 
219  if(prop.has_set_to())
220  {
221  // free variables
222 
223  bv.resize(width);
224  for(std::size_t i=0; i<width; i++)
225  bv[i]=prop.new_variable();
226 
227  // add implications
228 
229 #ifdef COMPACT_EQUAL_CONST
230  bv_utils.equal_const_register(convert_bv(index)); // Definitely
231 #endif
232 
233  bvt equal_bv;
234  equal_bv.resize(width);
235 
236  for(mp_integer i=0; i<array_size; i=i+1)
237  {
238  mp_integer offset=i*width;
239 
240  for(std::size_t j=0; j<width; j++)
241  equal_bv[j] = prop.lequal(
242  bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
243 
245  convert(equal_exprt(index, from_integer(i, index.type()))),
246  prop.land(equal_bv)));
247  }
248  }
249  else
250  {
251  bv.resize(width);
252 
253 #ifdef COMPACT_EQUAL_CONST
254  bv_utils.equal_const_register(convert_bv(index)); // Definitely
255 #endif
256 
257  typet constant_type=index.type(); // type of index operand
258 
260  array_size > 0,
261  "non-positive array sizes are forbidden in goto programs");
262 
263  for(mp_integer i=0; i<array_size; i=i+1)
264  {
265  literalt e =
266  convert(equal_exprt(index, from_integer(i, constant_type)));
267 
268  mp_integer offset=i*width;
269 
270  for(std::size_t j=0; j<width; j++)
271  {
272  literalt l = array_bv[numeric_cast_v<std::size_t>(offset + j)];
273 
274  if(i==0) // this initializes bv
275  bv[j]=l;
276  else
277  bv[j]=prop.lselect(e, l, bv[j]);
278  }
279  }
280  }
281  }
282  else
283  return conversion_failed(expr);
284 
285  return bv;
286 }
287 
290  const exprt &array,
291  const mp_integer &index)
292 {
293  const array_typet &array_type = to_array_type(array.type());
294 
295  std::size_t width=boolbv_width(array_type.subtype());
296 
297  if(width==0)
298  return conversion_failed(array);
299 
300  bvt bv;
301  bv.resize(width);
302 
303  // TODO: If the underlying array can use one of the
304  // improvements given above then it may be better to use
305  // the array theory for short chains of updates and then
306  // the improved array handling rather than full flattening.
307  // Note that the calculation is non-trivial as the cost of
308  // full flattening is amortised against all uses of
309  // the array (constant and variable indexes) and updated
310  // versions of it.
311 
312  const bvt &tmp=convert_bv(array); // recursive call
313 
314  mp_integer offset=index*width;
315 
316  if(offset>=0 &&
317  offset+width<=mp_integer(tmp.size()))
318  {
319  // in bounds
320 
321  // The assertion below is disabled as we want to be able
322  // to run CBMC without simplifier.
323  // Expression simplification should remove these cases
324  // assert(array.id()!=ID_array_of &&
325  // array.id()!=ID_array);
326  // If not there are large improvements possible as above
327 
328  for(std::size_t i=0; i<width; i++)
329  bv[i] = tmp[numeric_cast_v<std::size_t>(offset + i)];
330  }
331  else if(
332  array.id() == ID_member || array.id() == ID_index ||
333  array.id() == ID_byte_extract_big_endian ||
334  array.id() == ID_byte_extract_little_endian)
335  {
337  o.build(array, ns);
338  CHECK_RETURN(o.offset().id() != ID_unknown);
339 
340  const auto subtype_bytes_opt =
341  pointer_offset_size(array_type.subtype(), ns);
342  CHECK_RETURN(subtype_bytes_opt.has_value());
343 
344  exprt new_offset = simplify_expr(
345  plus_exprt(
346  o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),
347  ns);
348 
350  byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
351 
352  return convert_bv(be);
353  }
354  else
355  {
356  // out of bounds
357  for(std::size_t i=0; i<width; i++)
358  bv[i]=prop.new_variable();
359  }
360 
361  return bv;
362 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
Boolean AND.
Definition: std_expr.h:1835
Arrays with given size.
Definition: std_types.h:968
const exprt & size() const
Definition: std_types.h:976
const namespacet & ns
Definition: arrays.h:54
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:675
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
Definition: boolbv_map.cpp:41
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:543
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:38
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:124
bv_utilst bv_utils
Definition: boolbv.h:109
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:96
boolbv_mapt map
Definition: boolbv.h:115
Expression of type type extracted from some object op starting at position offset (given in number of...
Equality.
Definition: std_expr.h:1140
Base class for all expressions.
Definition: expr.h:54
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:96
Boolean implication.
Definition: std_expr.h:1898
Array index operator.
Definition: std_expr.h:1243
exprt & array()
Definition: std_expr.h:1259
exprt & index()
Definition: std_expr.h:1269
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:21
const exprt & root_object() const
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...
The plus expression Associativity is not specified.
Definition: std_expr.h:831
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
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 literalt new_variable()=0
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:81
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
#define CPROVER_PREFIX
std::vector< literalt > bvt
Definition: literal.h:201
BigInt mp_integer
Definition: mp_arith.h:19
API to expression classes for Pointers.
optionalt< 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)
bool has_byte_operator(const exprt &src)
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2701
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:816
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1297
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1018
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
irep_idt byte_extract_id()