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 <cassert>
12 
13 #include <util/arith_tools.h>
15 #include <util/simplify_expr.h>
16 #include <util/std_expr.h>
17 
19 {
20  const exprt &array=expr.array();
21  const exprt &index=expr.index();
22 
23  const typet &array_op_type=ns.follow(array.type());
24 
25  bvt bv;
26 
27  if(array_op_type.id()==ID_array)
28  {
29  const array_typet &array_type=
30  to_array_type(array_op_type);
31 
32  std::size_t width=boolbv_width(expr.type());
33 
34  if(width==0)
35  return conversion_failed(expr);
36 
37  // see if the array size is constant
38 
39  if(is_unbounded_array(array_type))
40  {
41  // use array decision procedure
42 
43  // free variables
44 
45  bv.resize(width);
46  for(std::size_t i=0; i<width; i++)
47  bv[i]=prop.new_variable();
48 
49  record_array_index(expr);
50 
51  // record type if array is a symbol
52 
53  if(array.id()==ID_symbol)
55  to_symbol_expr(array).get_identifier(), array_type);
56 
57  // make sure we have the index in the cache
58  convert_bv(index);
59 
60  return bv;
61  }
62 
63  // Must have a finite size
64  mp_integer array_size;
65  if(to_integer(array_type.size(), array_size))
66  throw "failed to convert array size";
67 
68  // see if the index address is constant
69  // many of these are compacted by simplify_expr
70  // but variable location writes will block this
71  mp_integer index_value;
72  if(!to_integer(index, index_value))
73  return convert_index(array, index_value);
74 
75  // Special case : arrays of one thing (useful for constants)
76  // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same
77  // value, bit-patterns with the same value, etc. are treated like
78  // this rather than as a series of individual options.
79  #define UNIFORM_ARRAY_HACK
80  #ifdef UNIFORM_ARRAY_HACK
81  bool is_uniform = false;
82 
83  if(array.id()==ID_array_of)
84  {
85  is_uniform = true;
86  }
87  else if(array.id()==ID_constant || array.id()==ID_array)
88  {
89  bool found_exception = false;
90  forall_expr(it, array.operands())
91  {
92  if(*it != array.op0())
93  {
94  found_exception = true;
95  break;
96  }
97  }
98 
99  if(!found_exception)
100  is_uniform = true;
101  }
102 
103  if(is_uniform && prop.has_set_to())
104  {
105  static int uniform_array_counter; // Temporary hack
106 
107  std::string identifier=
108  "__CPROVER_internal_uniform_array_"+
109  std::to_string(uniform_array_counter++);
110 
111  symbol_exprt result(identifier, expr.type());
112  bv = convert_bv(result);
113 
114  equal_exprt value_equality(result, array.op0());
115 
116  binary_relation_exprt lower_bound(
117  from_integer(0, index.type()), ID_le, index);
118  binary_relation_exprt upper_bound(
119  index, ID_lt, from_integer(array_size, index.type()));
120 
121  if(lower_bound.lhs().is_nil() ||
122  upper_bound.rhs().is_nil())
123  throw "number conversion failed (2)";
124 
125  and_exprt range_condition(lower_bound, upper_bound);
126  implies_exprt implication(range_condition, value_equality);
127 
128  // Simplify may remove the lower bound if the type
129  // is correct.
130  prop.l_set_to_true(convert(simplify_expr(implication, ns)));
131 
132  return bv;
133  }
134  #endif
135 
136  #define ACTUAL_ARRAY_HACK
137  #ifdef ACTUAL_ARRAY_HACK
138  // More useful when updates to concrete locations in
139  // actual arrays are compacted by simplify_expr
140  if((array.id()==ID_constant || array.id()==ID_array) &&
141  prop.has_set_to())
142  {
143  #ifdef CONSTANT_ARRAY_HACK
144  // TODO : Compile the whole array into a single relation
145  #endif
146 
147  // Symbol for output
148  static int actual_array_counter; // Temporary hack
149 
150  std::string identifier=
151  "__CPROVER_internal_actual_array_"+
152  std::to_string(actual_array_counter++);
153 
154  symbol_exprt result(identifier, expr.type());
155  bv = convert_bv(result);
156 
157  // add implications
158 
159  equal_exprt index_equality;
160  index_equality.lhs()=index; // index operand
161 
162  equal_exprt value_equality;
163  value_equality.lhs()=result;
164 
165 #ifdef COMPACT_EQUAL_CONST
166  bv_utils.equal_const_register(convert_bv(index)); // Definitely
167  bv_utils.equal_const_register(convert_bv(result)); // Maybe
168 #endif
169 
170  exprt::operandst::const_iterator it = array.operands().begin();
171 
172  for(mp_integer i=0; i<array_size; i=i+1)
173  {
174  index_equality.rhs()=from_integer(i, index_equality.lhs().type());
175 
176  if(index_equality.rhs().is_nil())
177  throw "number conversion failed (1)";
178 
179  assert(it != array.operands().end());
180 
181  value_equality.rhs()=*it++;
182 
183  // Cache comparisons and equalities
184  prop.l_set_to_true(convert(implies_exprt(index_equality,
185  value_equality)));
186  }
187 
188  return bv;
189  }
190 
191 #endif
192 
193 
194  // TODO : As with constant index, there is a trade-off
195  // of when it is best to flatten the whole array and
196  // when it is best to use the array theory and then use
197  // one or more of the above encoding strategies.
198 
199  // get literals for the whole array
200 
201  const bvt &array_bv=convert_bv(array);
202 
203  if(array_size*width!=array_bv.size())
204  throw "unexpected array size";
205 
206  // TODO: maybe a shifter-like construction would be better
207  // Would be a lot more compact but propagate worse
208 
209  if(prop.has_set_to())
210  {
211  // free variables
212 
213  bv.resize(width);
214  for(std::size_t i=0; i<width; i++)
215  bv[i]=prop.new_variable();
216 
217  // add implications
218 
219  equal_exprt index_equality;
220  index_equality.lhs()=index; // index operand
221 
222 #ifdef COMPACT_EQUAL_CONST
223  bv_utils.equal_const_register(convert_bv(index)); // Definitely
224 #endif
225 
226  bvt equal_bv;
227  equal_bv.resize(width);
228 
229  for(mp_integer i=0; i<array_size; i=i+1)
230  {
231  index_equality.rhs()=from_integer(i, index_equality.lhs().type());
232 
233  if(index_equality.rhs().is_nil())
234  throw "number conversion failed (1)";
235 
236  mp_integer offset=i*width;
237 
238  for(std::size_t j=0; j<width; j++)
239  equal_bv[j]=prop.lequal(bv[j],
240  array_bv[integer2size_t(offset+j)]);
241 
243  prop.limplies(convert(index_equality), prop.land(equal_bv)));
244  }
245  }
246  else
247  {
248  bv.resize(width);
249 
251  equality.lhs()=index; // index operand
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 
259  assert(array_size>0);
260 
261  for(mp_integer i=0; i<array_size; i=i+1)
262  {
263  equality.op1()=from_integer(i, constant_type);
264 
266 
267  mp_integer offset=i*width;
268 
269  for(std::size_t j=0; j<width; j++)
270  {
271  literalt l=array_bv[integer2size_t(offset+j)];
272 
273  if(i==0) // this initializes bv
274  bv[j]=l;
275  else
276  bv[j]=prop.lselect(e, l, bv[j]);
277  }
278  }
279  }
280  }
281  else
282  return conversion_failed(expr);
283 
284  return bv;
285 }
286 
289  const exprt &array,
290  const mp_integer &index)
291 {
292  const array_typet &array_type=
293  to_array_type(ns.follow(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[integer2size_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 mp_integer subtype_bytes =
341  pointer_offset_size(array_type.subtype(), ns);
342  exprt new_offset = simplify_expr(
343  plus_exprt(
344  o.offset(), from_integer(index * subtype_bytes, o.offset().type())),
345  ns);
346 
348  byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
349 
350  return convert_bv(be);
351  }
352  else
353  {
354  // out of bounds
355  for(std::size_t i=0; i<width; i++)
356  bv[i]=prop.new_variable();
357  }
358 
359  return bv;
360 }
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
The type of an expression.
Definition: type.h:22
bv_utilst bv_utils
Definition: boolbv.h:93
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:172
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
exprt & op0()
Definition: expr.h:72
exprt simplify_expr(const exprt &src, const namespacet &ns)
boolbv_widtht boolbv_width
Definition: boolbv.h:90
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
#define forall_expr(it, expr)
Definition: expr.h:28
const exprt & root_object() const
Definition: std_expr.h:1966
typet & type()
Definition: expr.h:56
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:266
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
boolean implication
Definition: std_expr.h:2339
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:49
equality
Definition: std_expr.h:1354
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:259
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void build(const exprt &expr, const namespacet &ns)
Build an object_descriptor_exprt from a given expr.
Definition: std_expr.cpp:121
boolean AND
Definition: std_expr.h:2255
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
irep_idt byte_extract_id()
split an expression into a base object and a (byte) offset
Definition: std_expr.h:1945
const exprt & size() const
Definition: std_types.h:1023
The plus expression.
Definition: std_expr.h:893
const namespacet & ns
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
const typet & follow(const typet &) const
Definition: namespace.cpp:55
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:312
exprt & index()
Definition: std_expr.h:1496
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:32
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
virtual bool has_set_to() const
Definition: prop.h:78
std::string to_string(const string_constraintt &expr)
Used for debug printing.
arrays with given size
Definition: std_types.h:1013
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
boolbv_mapt map
Definition: boolbv.h:99
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
TO_BE_DOCUMENTED.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt & array()
Definition: std_expr.h:1486
std::vector< literalt > bvt
Definition: literal.h:200
array index operator
Definition: std_expr.h:1462