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>
14 #include <util/std_expr.h>
15 #include <util/simplify_expr.h>
16 
18 {
19  if(expr.id()!=ID_index)
20  throw "expected index expression";
21 
22  if(expr.operands().size()!=2)
23  throw "index takes two operands";
24 
25  const exprt &array=expr.array();
26  const exprt &index=expr.index();
27 
28  const typet &array_op_type=ns.follow(array.type());
29 
30  bvt bv;
31 
32  if(array_op_type.id()==ID_array)
33  {
34  const array_typet &array_type=
35  to_array_type(array_op_type);
36 
37  std::size_t width=boolbv_width(expr.type());
38 
39  if(width==0)
40  return conversion_failed(expr);
41 
42  // see if the array size is constant
43 
44  if(is_unbounded_array(array_type))
45  {
46  // use array decision procedure
47 
48  // free variables
49 
50  bv.resize(width);
51  for(std::size_t i=0; i<width; i++)
52  bv[i]=prop.new_variable();
53 
54  record_array_index(expr);
55 
56  // record type if array is a symbol
57 
58  if(array.id()==ID_symbol)
60  to_symbol_expr(array).get_identifier(), array_type);
61 
62  // make sure we have the index in the cache
63  convert_bv(index);
64 
65  return bv;
66  }
67 
68  // Must have a finite size
69  mp_integer array_size;
70  if(to_integer(array_type.size(), array_size))
71  throw "failed to convert array size";
72 
73  // see if the index address is constant
74  // many of these are compacted by simplify_expr
75  // but variable location writes will block this
76  mp_integer index_value;
77  if(!to_integer(index, index_value))
78  return convert_index(array, index_value);
79 
80  // Special case : arrays of one thing (useful for constants)
81  // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same
82  // value, bit-patterns with the same value, etc. are treated like
83  // this rather than as a series of individual options.
84  #define UNIFORM_ARRAY_HACK
85  #ifdef UNIFORM_ARRAY_HACK
86  bool is_uniform = false;
87 
88  if(array.id()==ID_array_of)
89  {
90  is_uniform = true;
91  }
92  else if(array.id()==ID_constant || array.id()==ID_array)
93  {
94  bool found_exception = false;
95  forall_expr(it, array.operands())
96  {
97  if(*it != array.op0())
98  {
99  found_exception = true;
100  break;
101  }
102  }
103 
104  if(!found_exception)
105  is_uniform = true;
106  }
107 
108  if(is_uniform && prop.has_set_to())
109  {
110  static int uniform_array_counter; // Temporary hack
111 
112  std::string identifier=
113  "__CPROVER_internal_uniform_array_"+
114  std::to_string(uniform_array_counter++);
115 
116  symbol_exprt result(identifier, expr.type());
117  bv = convert_bv(result);
118 
119  equal_exprt value_equality(result, array.op0());
120 
121  binary_relation_exprt lower_bound(
122  from_integer(0, index.type()), ID_le, index);
123  binary_relation_exprt upper_bound(
124  index, ID_lt, from_integer(array_size, index.type()));
125 
126  if(lower_bound.lhs().is_nil() ||
127  upper_bound.rhs().is_nil())
128  throw "number conversion failed (2)";
129 
130  and_exprt range_condition(lower_bound, upper_bound);
131  implies_exprt implication(range_condition, value_equality);
132 
133  // Simplify may remove the lower bound if the type
134  // is correct.
135  prop.l_set_to_true(convert(simplify_expr(implication, ns)));
136 
137  return bv;
138  }
139  #endif
140 
141  #define ACTUAL_ARRAY_HACK
142  #ifdef ACTUAL_ARRAY_HACK
143  // More useful when updates to concrete locations in
144  // actual arrays are compacted by simplify_expr
145  if((array.id()==ID_constant || array.id()==ID_array) &&
146  prop.has_set_to())
147  {
148  #ifdef CONSTANT_ARRAY_HACK
149  // TODO : Compile the whole array into a single relation
150  #endif
151 
152  // Symbol for output
153  static int actual_array_counter; // Temporary hack
154 
155  std::string identifier=
156  "__CPROVER_internal_actual_array_"+
157  std::to_string(actual_array_counter++);
158 
159  symbol_exprt result(identifier, expr.type());
160  bv = convert_bv(result);
161 
162  // add implications
163 
164  equal_exprt index_equality;
165  index_equality.lhs()=index; // index operand
166 
167  equal_exprt value_equality;
168  value_equality.lhs()=result;
169 
170 #ifdef COMPACT_EQUAL_CONST
171  bv_utils.equal_const_register(convert_bv(index)); // Definitely
172  bv_utils.equal_const_register(convert_bv(result)); // Maybe
173 #endif
174 
175  exprt::operandst::const_iterator it = array.operands().begin();
176 
177  for(mp_integer i=0; i<array_size; i=i+1)
178  {
179  index_equality.rhs()=from_integer(i, index_equality.lhs().type());
180 
181  if(index_equality.rhs().is_nil())
182  throw "number conversion failed (1)";
183 
184  assert(it != array.operands().end());
185 
186  value_equality.rhs()=*it++;
187 
188  // Cache comparisons and equalities
189  prop.l_set_to_true(convert(implies_exprt(index_equality,
190  value_equality)));
191  }
192 
193  return bv;
194  }
195 
196 #endif
197 
198 
199  // TODO : As with constant index, there is a trade-off
200  // of when it is best to flatten the whole array and
201  // when it is best to use the array theory and then use
202  // one or more of the above encoding strategies.
203 
204  // get literals for the whole array
205 
206  const bvt &array_bv=convert_bv(array);
207 
208  if(array_size*width!=array_bv.size())
209  throw "unexpected array size";
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 
218  bv.resize(width);
219  for(std::size_t i=0; i<width; i++)
220  bv[i]=prop.new_variable();
221 
222  // add implications
223 
224  equal_exprt index_equality;
225  index_equality.lhs()=index; // index operand
226 
227 #ifdef COMPACT_EQUAL_CONST
228  bv_utils.equal_const_register(convert_bv(index)); // Definitely
229 #endif
230 
231  bvt equal_bv;
232  equal_bv.resize(width);
233 
234  for(mp_integer i=0; i<array_size; i=i+1)
235  {
236  index_equality.rhs()=from_integer(i, index_equality.lhs().type());
237 
238  if(index_equality.rhs().is_nil())
239  throw "number conversion failed (1)";
240 
241  mp_integer offset=i*width;
242 
243  for(std::size_t j=0; j<width; j++)
244  equal_bv[j]=prop.lequal(bv[j],
245  array_bv[integer2size_t(offset+j)]);
246 
248  prop.limplies(convert(index_equality), prop.land(equal_bv)));
249  }
250  }
251  else
252  {
253  bv.resize(width);
254 
256  equality.lhs()=index; // index operand
257 
258 #ifdef COMPACT_EQUAL_CONST
259  bv_utils.equal_const_register(convert_bv(index)); // Definitely
260 #endif
261 
262  typet constant_type=index.type(); // type of index operand
263 
264  assert(array_size>0);
265 
266  for(mp_integer i=0; i<array_size; i=i+1)
267  {
268  equality.op1()=from_integer(i, constant_type);
269 
270  literalt e=convert(equality);
271 
272  mp_integer offset=i*width;
273 
274  for(std::size_t j=0; j<width; j++)
275  {
276  literalt l=array_bv[integer2size_t(offset+j)];
277 
278  if(i==0) // this initializes bv
279  bv[j]=l;
280  else
281  bv[j]=prop.lselect(e, l, bv[j]);
282  }
283  }
284  }
285  }
286  else
287  return conversion_failed(expr);
288 
289  return bv;
290 }
291 
294  const exprt &array,
295  const mp_integer &index)
296 {
297  const array_typet &array_type=
298  to_array_type(ns.follow(array.type()));
299 
300  std::size_t width=boolbv_width(array_type.subtype());
301 
302  if(width==0)
303  return conversion_failed(array);
304 
305  bvt bv;
306  bv.resize(width);
307 
308  // TODO: If the underlying array can use one of the
309  // improvements given above then it may be better to use
310  // the array theory for short chains of updates and then
311  // the improved array handling rather than full flattening.
312  // Note that the calculation is non-trivial as the cost of
313  // full flattening is amortised against all uses of
314  // the array (constant and variable indexes) and updated
315  // versions of it.
316 
317  const bvt &tmp=convert_bv(array); // recursive call
318 
319  mp_integer offset=index*width;
320 
321  if(offset>=0 &&
322  offset+width<=mp_integer(tmp.size()))
323  {
324  // in bounds
325 
326  // The assertion below is disabled as we want to be able
327  // to run CBMC without simplifier.
328  // Expression simplification should remove these cases
329  // assert(array.id()!=ID_array_of &&
330  // array.id()!=ID_array);
331  // If not there are large improvements possible as above
332 
333  for(std::size_t i=0; i<width; i++)
334  bv[i]=tmp[integer2size_t(offset+i)];
335  }
336  else
337  {
338  // out of bounds
339  for(std::size_t i=0; i<width; i++)
340  bv[i]=prop.new_variable();
341  }
342 
343  return bv;
344 }
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:20
mstreamt & result()
Definition: message.h:233
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
bv_utilst bv_utils
Definition: boolbv.h:93
BigInt mp_integer
Definition: mp_arith.h:19
bool is_nil() const
Definition: irep.h:103
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
exprt & op0()
Definition: expr.h:84
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:673
#define forall_expr(it, expr)
Definition: expr.h:28
typet & type()
Definition: expr.h:60
boolean implication
Definition: std_expr.h:1926
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:47
equality
Definition: std_expr.h:1082
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
virtual literalt new_variable()=0
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
boolean AND
Definition: std_expr.h:1852
API to expression classes.
exprt & op1()
Definition: expr.h:87
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const exprt & size() const
Definition: std_types.h:915
const namespacet & ns
virtual literalt lequal(literalt a, literalt b)=0
virtual literalt equality(const exprt &e1, const exprt &e2)
Definition: equality.cpp:17
exprt & index()
Definition: std_expr.h:1208
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:32
Base class for all expressions.
Definition: expr.h:46
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
virtual bool has_set_to() const
Definition: prop.h:76
arrays with given size
Definition: std_types.h:901
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
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:31
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt & array()
Definition: std_expr.h:1198
std::vector< literalt > bvt
Definition: literal.h:197
array index operator
Definition: std_expr.h:1170