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