CBMC
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/byte_operators.h>
15 #include <util/cprover_prefix.h>
16 #include <util/pointer_expr.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  {
32  const array_typet &array_type=
33  to_array_type(array_op_type);
34 
35  // see if the array size is constant
36 
37  if(is_unbounded_array(array_type))
38  {
39  // use array decision procedure
40 
41  if(has_byte_operator(expr))
42  {
43  const index_exprt final_expr =
45  CHECK_RETURN(final_expr != expr);
46  bv = convert_bv(final_expr);
47 
48  // record type if array is a symbol
49  const exprt &final_array = final_expr.array();
50  if(
51  final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol)
52  {
53  const auto &array_width_opt = bv_width.get_width_opt(array_type);
54  (void)map.get_literals(
55  final_array.get(ID_identifier),
56  array_type,
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 
68  record_array_index(expr);
69 
70  // record type if array is a symbol
71  if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
72  {
73  const auto &array_width_opt = bv_width.get_width_opt(array_type);
74  (void)map.get_literals(
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
86  mp_integer array_size =
87  numeric_cast_v<mp_integer>(to_constant_expr(array_type.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
93  auto maybe_index_value = numeric_cast<mp_integer>(index);
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 =
209  convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));
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 
225  bvt equal_bv;
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 =
258  convert(equal_exprt(index, from_integer(i, constant_type)));
259 
260  mp_integer offset=i*width;
261 
262  for(std::size_t j=0; j<width; j++)
263  {
264  literalt l = array_bv[numeric_cast_v<std::size_t>(offset + j)];
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);
323  CHECK_RETURN(o.offset().id() != ID_unknown);
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 
329  exprt new_offset = simplify_expr(
330  plus_exprt(
331  o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),
332  ns);
333 
334  byte_extract_exprt be =
335  make_byte_extract(o.root_object(), new_offset, array_type.element_type());
336 
337  return convert_bv(be);
338  }
339  else if(
340  array.id() == ID_byte_extract_big_endian ||
341  array.id() == ID_byte_extract_little_endian)
342  {
343  const byte_extract_exprt &byte_extract_expr = to_byte_extract_expr(array);
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
350  exprt new_offset = simplify_expr(
351  plus_exprt{
352  byte_extract_expr.offset(),
353  from_integer(
354  index * (*subtype_bytes_opt), byte_extract_expr.offset().type())},
355  ns);
356 
357  byte_extract_exprt be = byte_extract_expr;
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.
exprt lower_byte_operators(const exprt &src, const namespacet &ns)
Rewrite an expression possibly containing byte-extract or -update expressions to more fundamental ope...
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Boolean AND.
Definition: std_expr.h:2120
Arrays with given size.
Definition: std_types.h:807
const typet & element_type() const
The type of the elements of the array.
Definition: std_types.h:827
const exprt & size() const
Definition: std_types.h:840
const namespacet & ns
Definition: arrays.h:56
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:44
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
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:37
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:518
boolbv_widtht bv_width
Definition: boolbv.h:115
bv_utilst bv_utils
Definition: boolbv.h:116
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:83
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:101
boolbv_mapt map
Definition: boolbv.h:122
Expression of type type extracted from some object op starting at position offset (given in number of...
Equality.
Definition: std_expr.h:1361
Base class for all expressions.
Definition: expr.h:56
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:91
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
Boolean implication.
Definition: std_expr.h:2183
Array index operator.
Definition: std_expr.h:1465
exprt & array()
Definition: std_expr.h:1495
exprt & index()
Definition: std_expr.h:1505
const irep_idt & get(const irep_idt &name) const
Definition: irep.cpp:44
const irep_idt & id() const
Definition: irep.h:384
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:181
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:1002
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 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:131
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
API to expression classes.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3037
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:987
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1533
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:888
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.