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/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 
24 {
25  const exprt &array=expr.array();
26  const exprt &index=expr.index();
27 
28  const typet &array_op_type = 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  if(has_byte_operator(expr))
49  {
50  const index_exprt final_expr =
52  CHECK_RETURN(final_expr != expr);
53  bv = convert_bv(final_expr);
54 
55  // record type if array is a symbol
56  const exprt &final_array = final_expr.array();
57  if(
58  final_array.id() == ID_symbol || final_array.id() == ID_nondet_symbol)
59  {
60  std::size_t width = boolbv_width(array_type);
61  (void)map.get_literals(
62  final_array.get(ID_identifier), array_type, width);
63  }
64 
65  // make sure we have the index in the cache
66  convert_bv(final_expr.index());
67  }
68  else
69  {
70  // free variables
71  bv = prop.new_variables(width);
72 
73  record_array_index(expr);
74 
75  // record type if array is a symbol
76  if(array.id() == ID_symbol || array.id() == ID_nondet_symbol)
77  {
78  std::size_t width = boolbv_width(array_type);
79  (void)map.get_literals(array.get(ID_identifier), array_type, width);
80  }
81 
82  // make sure we have the index in the cache
83  convert_bv(index);
84  }
85 
86  return bv;
87  }
88 
89  // Must have a finite size
90  mp_integer array_size =
91  numeric_cast_v<mp_integer>(to_constant_expr(array_type.size()));
92 
93  {
94  // see if the index address is constant
95  // many of these are compacted by simplify_expr
96  // but variable location writes will block this
97  auto maybe_index_value = numeric_cast<mp_integer>(index);
98  if(maybe_index_value.has_value())
99  {
100  return convert_index(array, maybe_index_value.value());
101  }
102  }
103 
104  // Special case : arrays of one thing (useful for constants)
105  // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same
106  // value, bit-patterns with the same value, etc. are treated like
107  // this rather than as a series of individual options.
108  #define UNIFORM_ARRAY_HACK
109  #ifdef UNIFORM_ARRAY_HACK
110  bool is_uniform = array.id() == ID_array_of;
111 
112  if(array.id() == ID_constant || array.id() == ID_array)
113  {
114  is_uniform = array.operands().size() <= 1 ||
115  std::all_of(
116  ++array.operands().begin(),
117  array.operands().end(),
118  [&array](const exprt &expr) {
119  return expr == to_multi_ary_expr(array).op0();
120  });
121  }
122 
123  if(is_uniform && prop.has_set_to())
124  {
125  static int uniform_array_counter; // Temporary hack
126 
127  const std::string identifier = CPROVER_PREFIX "internal_uniform_array_" +
128  std::to_string(uniform_array_counter++);
129 
130  symbol_exprt result(identifier, expr.type());
131  bv = convert_bv(result);
132 
133  // return an unconstrained value in case of an empty array (the access is
134  // necessarily out-of-bounds)
135  if(!array.has_operands())
136  return bv;
137 
138  equal_exprt value_equality(result, to_multi_ary_expr(array).op0());
139 
140  binary_relation_exprt lower_bound(
141  from_integer(0, index.type()), ID_le, index);
142  binary_relation_exprt upper_bound(
143  index, ID_lt, from_integer(array_size, index.type()));
144 
145  and_exprt range_condition(std::move(lower_bound), std::move(upper_bound));
146  implies_exprt implication(
147  std::move(range_condition), std::move(value_equality));
148 
149  // Simplify may remove the lower bound if the type
150  // is correct.
151  prop.l_set_to_true(convert(simplify_expr(implication, ns)));
152 
153  return bv;
154  }
155  #endif
156 
157  #define ACTUAL_ARRAY_HACK
158  #ifdef ACTUAL_ARRAY_HACK
159  // More useful when updates to concrete locations in
160  // actual arrays are compacted by simplify_expr
161  if((array.id()==ID_constant || array.id()==ID_array) &&
162  prop.has_set_to())
163  {
164  #ifdef CONSTANT_ARRAY_HACK
165  // TODO : Compile the whole array into a single relation
166  #endif
167 
168  // Symbol for output
169  static int actual_array_counter; // Temporary hack
170 
171  const std::string identifier = CPROVER_PREFIX "internal_actual_array_" +
172  std::to_string(actual_array_counter++);
173 
174  symbol_exprt result(identifier, expr.type());
175  bv = convert_bv(result);
176 
177  // add implications
178 
179 #ifdef COMPACT_EQUAL_CONST
180  bv_utils.equal_const_register(convert_bv(index)); // Definitely
181  bv_utils.equal_const_register(convert_bv(result)); // Maybe
182 #endif
183 
184  exprt::operandst::const_iterator it = array.operands().begin();
185 
186  for(mp_integer i=0; i<array_size; i=i+1)
187  {
188  INVARIANT(
189  it != array.operands().end(),
190  "this loop iterates over the array, so `it` shouldn't be increased "
191  "past the array's end");
192 
193  // Cache comparisons and equalities
195  equal_exprt(index, from_integer(i, index.type())),
196  equal_exprt(result, *it++))));
197  }
198 
199  return bv;
200  }
201 
202 #endif
203 
204 
205  // TODO : As with constant index, there is a trade-off
206  // of when it is best to flatten the whole array and
207  // when it is best to use the array theory and then use
208  // one or more of the above encoding strategies.
209 
210  // get literals for the whole array
211 
212  const bvt &array_bv =
213  convert_bv(array, numeric_cast_v<std::size_t>(array_size * width));
214 
215  // TODO: maybe a shifter-like construction would be better
216  // Would be a lot more compact but propagate worse
217 
218  if(prop.has_set_to())
219  {
220  // free variables
221  bv = prop.new_variables(width);
222 
223  // add implications
224 
225 #ifdef COMPACT_EQUAL_CONST
226  bv_utils.equal_const_register(convert_bv(index)); // Definitely
227 #endif
228 
229  bvt equal_bv;
230  equal_bv.resize(width);
231 
232  for(mp_integer i=0; i<array_size; i=i+1)
233  {
234  mp_integer offset=i*width;
235 
236  for(std::size_t j=0; j<width; j++)
237  equal_bv[j] = prop.lequal(
238  bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
239 
241  convert(equal_exprt(index, from_integer(i, index.type()))),
242  prop.land(equal_bv)));
243  }
244  }
245  else
246  {
247  bv.resize(width);
248 
249 #ifdef COMPACT_EQUAL_CONST
250  bv_utils.equal_const_register(convert_bv(index)); // Definitely
251 #endif
252 
253  typet constant_type=index.type(); // type of index operand
254 
256  array_size > 0,
257  "non-positive array sizes are forbidden in goto programs");
258 
259  for(mp_integer i=0; i<array_size; i=i+1)
260  {
261  literalt e =
262  convert(equal_exprt(index, from_integer(i, constant_type)));
263 
264  mp_integer offset=i*width;
265 
266  for(std::size_t j=0; j<width; j++)
267  {
268  literalt l = array_bv[numeric_cast_v<std::size_t>(offset + j)];
269 
270  if(i==0) // this initializes bv
271  bv[j]=l;
272  else
273  bv[j]=prop.lselect(e, l, bv[j]);
274  }
275  }
276  }
277  }
278  else
279  return conversion_failed(expr);
280 
281  return bv;
282 }
283 
286  const exprt &array,
287  const mp_integer &index)
288 {
289  const array_typet &array_type = to_array_type(array.type());
290 
291  std::size_t width=boolbv_width(array_type.subtype());
292 
293  if(width==0)
294  return conversion_failed(array);
295 
296  // TODO: If the underlying array can use one of the
297  // improvements given above then it may be better to use
298  // the array theory for short chains of updates and then
299  // the improved array handling rather than full flattening.
300  // Note that the calculation is non-trivial as the cost of
301  // full flattening is amortised against all uses of
302  // the array (constant and variable indexes) and updated
303  // versions of it.
304 
305  const bvt &tmp=convert_bv(array); // recursive call
306 
307  mp_integer offset=index*width;
308 
309  if(offset>=0 &&
310  offset+width<=mp_integer(tmp.size()))
311  {
312  // in bounds
313 
314  // The assertion below is disabled as we want to be able
315  // to run CBMC without simplifier.
316  // Expression simplification should remove these cases
317  // assert(array.id()!=ID_array_of &&
318  // array.id()!=ID_array);
319  // If not there are large improvements possible as above
320 
321  std::size_t offset_int = numeric_cast_v<std::size_t>(offset);
322  return bvt(tmp.begin() + offset_int, tmp.begin() + offset_int + width);
323  }
324  else if(array.id() == ID_member || array.id() == ID_index)
325  {
326  // out of bounds for the component, but not necessarily outside the bounds
327  // of the underlying object
329  o.build(array, ns);
330  CHECK_RETURN(o.offset().id() != ID_unknown);
331 
332  const auto subtype_bytes_opt =
333  pointer_offset_size(array_type.subtype(), ns);
334  CHECK_RETURN(subtype_bytes_opt.has_value());
335 
336  exprt new_offset = simplify_expr(
337  plus_exprt(
338  o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),
339  ns);
340 
341  byte_extract_exprt be =
342  make_byte_extract(o.root_object(), new_offset, array_type.subtype());
343 
344  return convert_bv(be);
345  }
346  else if(
347  array.id() == ID_byte_extract_big_endian ||
348  array.id() == ID_byte_extract_little_endian)
349  {
350  const byte_extract_exprt &byte_extract_expr = to_byte_extract_expr(array);
351 
352  const auto subtype_bytes_opt =
353  pointer_offset_size(array_type.subtype(), ns);
354  CHECK_RETURN(subtype_bytes_opt.has_value());
355 
356  // add offset to index
357  exprt new_offset = simplify_expr(
358  plus_exprt{
359  byte_extract_expr.offset(),
360  from_integer(
361  index * (*subtype_bytes_opt), byte_extract_expr.offset().type())},
362  ns);
363 
364  byte_extract_exprt be = byte_extract_expr;
365  be.offset() = new_offset;
366  be.type() = array_type.subtype();
367 
368  return convert_bv(be);
369  }
370  else
371  {
372  // out of bounds
373  return prop.new_variables(width);
374  }
375 }
pointer_offset_size.h
Pointer Logic.
make_byte_extract
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.
Definition: byte_operators.cpp:48
boolbvt::map
boolbv_mapt map
Definition: boolbv.h:118
typet::subtype
const typet & subtype() const
Definition: type.h:47
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
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: pointer_expr.cpp:107
propt::new_variables
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:543
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
typet
The type of an expression, extends irept.
Definition: type.h:28
bvt
std::vector< literalt > bvt
Definition: literal.h:201
to_byte_extract_expr
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Definition: byte_operators.h:57
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1382
has_byte_operator
bool has_byte_operator(const exprt &src)
Definition: byte_operators.cpp:2302
boolbv_mapt::get_literals
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
Definition: boolbv_map.cpp:41
object_descriptor_exprt
Split an expression into a base object and a (byte) offset.
Definition: pointer_expr.h:147
and_exprt
Boolean AND.
Definition: std_expr.h:1920
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:914
boolbvt::convert_index
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Definition: boolbv_index.cpp:285
exprt
Base class for all expressions.
Definition: expr.h:54
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:50
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:80
propt::land
virtual literalt land(literalt a, literalt b)=0
equal_exprt
Equality.
Definition: std_expr.h:1225
object_descriptor_exprt::root_object
static const exprt & root_object(const exprt &expr)
Definition: pointer_expr.cpp:161
expr_lowering.h
array_typet::size
const exprt & size() const
Definition: std_types.h:771
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
byte_operators.h
Expression classes for byte-level operators.
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:510
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:89
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:97
arrayst::ns
const namespacet & ns
Definition: arrays.h:54
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
pointer_expr.h
API to expression classes for Pointers.
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2659
index_exprt::index
exprt & index()
Definition: std_expr.h:1354
index_exprt::array
exprt & array()
Definition: std_expr.h:1344
irept::id
const irep_idt & id() const
Definition: irep.h:407
arrayst::record_array_index
void record_array_index(const index_exprt &expr)
Definition: arrays.cpp:42
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:40
cprover_prefix.h
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:156
simplify_expr.h
byte_extract_exprt::offset
exprt & offset()
Definition: byte_operators.h:44
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:90
array_typet
Arrays with given size.
Definition: std_types.h:763
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:112
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:674
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:813
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:79
boolbvt::conversion_failed
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:84
implies_exprt
Boolean implication.
Definition: std_expr.h:1983
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:92
index_exprt
Array index operator.
Definition: std_expr.h:1328
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
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:899
std_expr.h
API to expression classes.
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:126
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
object_descriptor_exprt::offset
exprt & offset()
Definition: pointer_expr.h:189