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 
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  std::size_t width=boolbv_width(expr.type());
36 
37  if(width==0)
38  return conversion_failed(expr);
39 
40  // see if the array size is constant
41 
42  if(is_unbounded_array(array_type))
43  {
44  // use array decision procedure
45 
46  if(has_byte_operator(expr))
47  {
48  const index_exprt final_expr =
50  CHECK_RETURN(final_expr != expr);
51  bv = convert_bv(final_expr);
52 
53  // record type if array is a symbol
54  const exprt &final_array = final_expr.array();
55  if(
56  final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol)
57  {
58  map.get_map_entry(final_array.get(ID_identifier), array_type);
59  }
60 
61  // make sure we have the index in the cache
62  convert_bv(final_expr.index());
63  }
64  else
65  {
66  // free variables
67  bv.reserve(width);
68  for(std::size_t i = 0; i < width; i++)
69  bv.push_back(prop.new_variable());
70 
71  record_array_index(expr);
72 
73  // record type if array is a symbol
74  if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
75  map.get_map_entry(array.get(ID_identifier), array_type);
76 
77  // make sure we have the index in the cache
78  convert_bv(index);
79  }
80 
81  return bv;
82  }
83 
84  // Must have a finite size
85  mp_integer array_size =
86  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
87 
88  {
89  // see if the index address is constant
90  // many of these are compacted by simplify_expr
91  // but variable location writes will block this
92  auto maybe_index_value = numeric_cast<mp_integer>(index);
93  if(maybe_index_value.has_value())
94  {
95  return convert_index(array, maybe_index_value.value());
96  }
97  }
98 
99  // Special case : arrays of one thing (useful for constants)
100  // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same
101  // value, bit-patterns with the same value, etc. are treated like
102  // this rather than as a series of individual options.
103  #define UNIFORM_ARRAY_HACK
104  #ifdef UNIFORM_ARRAY_HACK
105  bool is_uniform = array.id() == ID_array_of;
106 
107  if(array.id() == ID_constant || array.id() == ID_array)
108  {
109  is_uniform = array.operands().size() <= 1 ||
110  std::all_of(
111  ++array.operands().begin(),
112  array.operands().end(),
113  [&array](const exprt &expr) {
114  return expr == to_multi_ary_expr(array).op0();
115  });
116  }
117 
118  if(is_uniform && prop.has_set_to())
119  {
120  static int uniform_array_counter; // Temporary hack
121 
122  const std::string identifier = CPROVER_PREFIX "internal_uniform_array_" +
123  std::to_string(uniform_array_counter++);
124 
125  symbol_exprt result(identifier, expr.type());
126  bv = convert_bv(result);
127 
128  // return an unconstrained value in case of an empty array (the access is
129  // necessarily out-of-bounds)
130  if(!array.has_operands())
131  return bv;
132 
133  equal_exprt value_equality(result, to_multi_ary_expr(array).op0());
134 
135  binary_relation_exprt lower_bound(
136  from_integer(0, index.type()), ID_le, index);
137  binary_relation_exprt upper_bound(
138  index, ID_lt, from_integer(array_size, index.type()));
139 
140  and_exprt range_condition(std::move(lower_bound), std::move(upper_bound));
141  implies_exprt implication(
142  std::move(range_condition), std::move(value_equality));
143 
144  // Simplify may remove the lower bound if the type
145  // is correct.
146  prop.l_set_to_true(convert(simplify_expr(implication, ns)));
147 
148  return bv;
149  }
150  #endif
151 
152  #define ACTUAL_ARRAY_HACK
153  #ifdef ACTUAL_ARRAY_HACK
154  // More useful when updates to concrete locations in
155  // actual arrays are compacted by simplify_expr
156  if((array.id()==ID_constant || array.id()==ID_array) &&
157  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 
207  const bvt &array_bv =
208  convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));
209 
210  // TODO: maybe a shifter-like construction would be better
211  // Would be a lot more compact but propagate worse
212 
213  if(prop.has_set_to())
214  {
215  // free variables
216 
217  bv.resize(width);
218  for(std::size_t i=0; i<width; i++)
219  bv[i]=prop.new_variable();
220 
221  // add implications
222 
223 #ifdef COMPACT_EQUAL_CONST
224  bv_utils.equal_const_register(convert_bv(index)); // Definitely
225 #endif
226 
227  bvt equal_bv;
228  equal_bv.resize(width);
229 
230  for(mp_integer i=0; i<array_size; i=i+1)
231  {
232  mp_integer offset=i*width;
233 
234  for(std::size_t j=0; j<width; j++)
235  equal_bv[j] = prop.lequal(
236  bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
237 
239  convert(equal_exprt(index, from_integer(i, index.type()))),
240  prop.land(equal_bv)));
241  }
242  }
243  else
244  {
245  bv.resize(width);
246 
247 #ifdef COMPACT_EQUAL_CONST
248  bv_utils.equal_const_register(convert_bv(index)); // Definitely
249 #endif
250 
251  typet constant_type=index.type(); // type of index operand
252 
254  array_size > 0,
255  "non-positive array sizes are forbidden in goto programs");
256 
257  for(mp_integer i=0; i<array_size; i=i+1)
258  {
259  literalt e =
260  convert(equal_exprt(index, from_integer(i, constant_type)));
261 
262  mp_integer offset=i*width;
263 
264  for(std::size_t j=0; j<width; j++)
265  {
266  literalt l = array_bv[numeric_cast_v<std::size_t>(offset + j)];
267 
268  if(i==0) // this initializes bv
269  bv[j]=l;
270  else
271  bv[j]=prop.lselect(e, l, bv[j]);
272  }
273  }
274  }
275  }
276  else
277  return conversion_failed(expr);
278 
279  return bv;
280 }
281 
284  const exprt &array,
285  const mp_integer &index)
286 {
287  const array_typet &array_type = to_array_type(array.type());
288 
289  std::size_t width=boolbv_width(array_type.subtype());
290 
291  if(width==0)
292  return conversion_failed(array);
293 
294  bvt bv;
295  bv.resize(width);
296 
297  // TODO: If the underlying array can use one of the
298  // improvements given above then it may be better to use
299  // the array theory for short chains of updates and then
300  // the improved array handling rather than full flattening.
301  // Note that the calculation is non-trivial as the cost of
302  // full flattening is amortised against all uses of
303  // the array (constant and variable indexes) and updated
304  // versions of it.
305 
306  const bvt &tmp=convert_bv(array); // recursive call
307 
308  mp_integer offset=index*width;
309 
310  if(offset>=0 &&
311  offset+width<=mp_integer(tmp.size()))
312  {
313  // in bounds
314 
315  // The assertion below is disabled as we want to be able
316  // to run CBMC without simplifier.
317  // Expression simplification should remove these cases
318  // assert(array.id()!=ID_array_of &&
319  // array.id()!=ID_array);
320  // If not there are large improvements possible as above
321 
322  for(std::size_t i=0; i<width; i++)
323  bv[i] = tmp[numeric_cast_v<std::size_t>(offset + i)];
324  }
325  else if(
326  array.id() == ID_member || array.id() == ID_index ||
327  array.id() == ID_byte_extract_big_endian ||
328  array.id() == ID_byte_extract_little_endian)
329  {
331  o.build(array, ns);
332  CHECK_RETURN(o.offset().id() != ID_unknown);
333 
334  const auto subtype_bytes_opt =
335  pointer_offset_size(array_type.subtype(), ns);
336  CHECK_RETURN(subtype_bytes_opt.has_value());
337 
338  exprt new_offset = simplify_expr(
339  plus_exprt(
340  o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),
341  ns);
342 
344  byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
345 
346  return convert_bv(be);
347  }
348  else
349  {
350  // out of bounds
351  for(std::size_t i=0; i<width; i++)
352  bv[i]=prop.new_variable();
353  }
354 
355  return bv;
356 }
pointer_offset_size.h
Pointer Logic.
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:104
typet::subtype
const typet & subtype() const
Definition: type.h:47
boolbv_mapt::get_map_entry
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
Definition: boolbv_map.cpp:49
arith_tools.h
object_descriptor_exprt::build
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...
Definition: std_expr.cpp:141
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
has_byte_operator
bool has_byte_operator(const exprt &src)
Definition: byte_operators.cpp:2302
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: std_expr.h:1832
and_exprt
Boolean AND.
Definition: std_expr.h:2137
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
propt::new_variable
virtual literalt new_variable()=0
boolbvt::convert_index
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Definition: boolbv_index.cpp:283
exprt
Base class for all expressions.
Definition: expr.h:53
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
propt::land
virtual literalt land(literalt a, literalt b)=0
equal_exprt
Equality.
Definition: std_expr.h:1190
expr_lowering.h
array_typet::size
const exprt & size() const
Definition: std_types.h:973
byte_extract_id
irep_idt byte_extract_id()
Definition: byte_operators.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:92
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
lower_byte_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...
Definition: byte_operators.cpp:2317
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
irept::id
const irep_idt & id() const
Definition: irep.h:418
arrayst::record_array_index
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:36
boolbvt::convert_bv
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:119
cprover_prefix.h
object_descriptor_exprt::root_object
const exprt & root_object() const
Definition: std_expr.cpp:218
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
simplify_expr.h
propt::lequal
virtual literalt lequal(literalt a, literalt b)=0
pointer_offset_size
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.
Definition: pointer_offset_size.cpp:89
array_typet
Arrays with given size.
Definition: std_types.h:965
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
literalt
Definition: literal.h:26
CPROVER_PREFIX
#define CPROVER_PREFIX
Definition: cprover_prefix.h:14
byte_extract_exprt
Expression of type type extracted from some object op starting at position offset (given in number of...
Definition: byte_operators.h:29
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:81
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:95
index_exprt
Array index operator.
Definition: std_expr.h:1293
to_multi_ary_expr
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:866
std_expr.h
API to expression classes.
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
object_descriptor_exprt::offset
exprt & offset()
Definition: std_expr.h:1870