cprover
boolbv.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #ifndef CPROVER_SOLVERS_FLATTENING_BOOLBV_H
11 #define CPROVER_SOLVERS_FLATTENING_BOOLBV_H
12 
13 //
14 // convert expression to boolean formula
15 //
16 
17 #include <util/endianness_map.h>
18 #include <util/expr.h>
19 #include <util/mp_arith.h>
20 #include <util/optional.h>
21 
23 
24 #include "bv_utils.h"
25 #include "boolbv_width.h"
26 #include "boolbv_map.h"
27 #include "arrays.h"
28 
30 class bswap_exprt;
31 class byte_extract_exprt;
32 class byte_update_exprt;
34 class extractbit_exprt;
35 class extractbits_exprt;
38 class member_exprt;
39 class replication_exprt;
40 
41 class boolbvt:public arrayst
42 {
43 public:
45  const namespacet &_ns,
46  propt &_prop,
48  bool get_array_constraints = false)
51  bv_width(_ns),
52  bv_utils(_prop),
53  functions(*this),
54  map(_prop)
55  {
56  }
57 
58  virtual const bvt &convert_bv( // check cache
59  const exprt &expr,
60  const optionalt<std::size_t> expected_width = nullopt);
61 
62  virtual bvt convert_bitvector(const exprt &expr); // no cache
63 
64  // overloading
65  exprt get(const exprt &expr) const override;
66  void set_to(const exprt &expr, bool value) override;
67  void print_assignment(std::ostream &out) const override;
68 
69  void clear_cache() override
70  {
72  bv_cache.clear();
73  }
74 
75  void post_process() override
76  {
80  }
81 
82  enum class unbounded_arrayt { U_NONE, U_ALL, U_AUTO };
84 
86  {
87  return get_value(bv, 0, bv.size());
88  }
89 
90  mp_integer get_value(const bvt &bv, std::size_t offset, std::size_t width);
91 
92  const boolbv_mapt &get_map() const
93  {
94  return map;
95  }
96 
97  virtual std::size_t boolbv_width(const typet &type) const
98  {
99  return bv_width(type);
100  }
101 
102  virtual endianness_mapt
103  endianness_map(const typet &type, bool little_endian) const
104  {
105  return endianness_mapt{type, little_endian, ns};
106  }
107 
108  virtual endianness_mapt endianness_map(const typet &type) const;
109 
110 protected:
113 
114  // uninterpreted functions
116 
117  // the mapping from identifiers to literals
119 
120  // overloading
121  literalt convert_rest(const exprt &expr) override;
122  virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
123 
124  // NOLINTNEXTLINE(readability/identifiers)
125  typedef arrayst SUB;
126 
127  bvt conversion_failed(const exprt &expr);
128 
129  typedef std::unordered_map<const exprt, bvt, irep_hash> bv_cachet;
131 
132  bool type_conversion(
133  const typet &src_type, const bvt &src,
134  const typet &dest_type, bvt &dest);
135 
137  virtual literalt convert_typecast(const typecast_exprt &expr);
138  virtual literalt convert_reduction(const unary_exprt &expr);
139  virtual literalt convert_onehot(const unary_exprt &expr);
140  virtual literalt convert_extractbit(const extractbit_exprt &expr);
141  virtual literalt convert_overflow(const exprt &expr);
142  virtual literalt convert_equality(const equal_exprt &expr);
144  const binary_relation_exprt &expr);
146  virtual literalt convert_quantifier(const quantifier_exprt &expr);
147 
148  virtual bvt convert_index(const exprt &array, const mp_integer &index);
149  virtual bvt convert_index(const index_exprt &expr);
150  virtual bvt convert_bswap(const bswap_exprt &expr);
151  virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
152  virtual bvt convert_byte_update(const byte_update_exprt &expr);
153  virtual bvt convert_constraint_select_one(const exprt &expr);
154  virtual bvt convert_if(const if_exprt &expr);
155  virtual bvt convert_struct(const struct_exprt &expr);
156  virtual bvt convert_array(const exprt &expr);
157  virtual bvt convert_vector(const vector_exprt &expr);
158  virtual bvt convert_complex(const complex_exprt &expr);
159  virtual bvt convert_complex_real(const complex_real_exprt &expr);
160  virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
162  virtual bvt convert_let(const let_exprt &);
163  virtual bvt convert_array_of(const array_of_exprt &expr);
164  virtual bvt convert_union(const union_exprt &expr);
165  virtual bvt convert_bv_typecast(const typecast_exprt &expr);
166  virtual bvt convert_add_sub(const exprt &expr);
167  virtual bvt convert_mult(const mult_exprt &expr);
168  virtual bvt convert_div(const div_exprt &expr);
169  virtual bvt convert_mod(const mod_exprt &expr);
170  virtual bvt convert_floatbv_op(const ieee_float_op_exprt &);
171  virtual bvt convert_floatbv_mod_rem(const binary_exprt &);
173  virtual bvt convert_member(const member_exprt &expr);
174  virtual bvt convert_with(const with_exprt &expr);
175  virtual bvt convert_update(const update_exprt &);
176  virtual bvt convert_case(const exprt &expr);
177  virtual bvt convert_cond(const cond_exprt &);
178  virtual bvt convert_shift(const binary_exprt &expr);
179  virtual bvt convert_bitwise(const exprt &expr);
180  virtual bvt convert_unary_minus(const unary_minus_exprt &expr);
181  virtual bvt convert_abs(const abs_exprt &expr);
182  virtual bvt convert_concatenation(const concatenation_exprt &expr);
183  virtual bvt convert_replication(const replication_exprt &expr);
184  virtual bvt convert_bv_literals(const exprt &expr);
185  virtual bvt convert_constant(const constant_exprt &expr);
186  virtual bvt convert_extractbits(const extractbits_exprt &expr);
187  virtual bvt convert_symbol(const exprt &expr);
188  virtual bvt convert_bv_reduction(const unary_exprt &expr);
189  virtual bvt convert_not(const not_exprt &expr);
190  virtual bvt convert_power(const binary_exprt &expr);
192  const function_application_exprt &expr);
193 
194  virtual exprt make_bv_expr(const typet &type, const bvt &bv);
195  virtual exprt make_free_bv_expr(const typet &type);
196 
197  void convert_with(
198  const typet &type,
199  const exprt &op1,
200  const exprt &op2,
201  const bvt &prev_bv,
202  bvt &next_bv);
203 
204  void convert_with_bv(
205  const exprt &op1,
206  const exprt &op2,
207  const bvt &prev_bv,
208  bvt &next_bv);
209 
210  void convert_with_array(
211  const array_typet &type,
212  const exprt &op1,
213  const exprt &op2,
214  const bvt &prev_bv,
215  bvt &next_bv);
216 
217  void convert_with_union(
218  const union_typet &type,
219  const exprt &op2,
220  const bvt &prev_bv,
221  bvt &next_bv);
222 
223  void convert_with_struct(
224  const struct_typet &type,
225  const exprt &op1,
226  const exprt &op2,
227  const bvt &prev_bv,
228  bvt &next_bv);
229 
230  void convert_update_rec(
231  const exprt::operandst &designator,
232  std::size_t d,
233  const typet &type,
234  std::size_t offset,
235  const exprt &new_value,
236  bvt &bv);
237 
238  virtual exprt bv_get_unbounded_array(const exprt &) const;
239 
240  virtual exprt bv_get_rec(
241  const exprt &expr,
242  const bvt &bv,
243  std::size_t offset,
244  const typet &type) const;
245 
246  exprt bv_get(const bvt &bv, const typet &type) const;
247  exprt bv_get_cache(const exprt &expr) const;
248 
249  // unbounded arrays
250  bool is_unbounded_array(const typet &type) const override;
251 
252  // quantifier instantiations
254  {
255  public:
257  : expr(std::move(_expr)), l(std::move(_l))
258  {
259  }
260 
263  };
264 
265  typedef std::list<quantifiert> quantifier_listt;
267 
269 
270  typedef std::vector<std::size_t> offset_mapt;
272 
273  // strings
275 
276  // scopes
277  std::size_t scope_counter = 0;
278 
281 };
282 
283 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H
Theory of Arrays with Extensionality.
Absolute value.
Definition: std_expr.h:346
Expression to define a mapping from an argument (index) to elements.
Definition: std_expr.h:3128
Array constructor from single element.
Definition: std_expr.h:1402
Arrays with given size.
Definition: std_types.h:763
Definition: arrays.h:31
void post_process() override
Definition: arrays.h:39
const namespacet & ns
Definition: arrays.h:54
message_handlert & message_handler
Definition: arrays.h:56
bool get_array_constraints
Definition: arrays.h:111
A base class for binary expressions.
Definition: std_expr.h:550
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
A base class for variable bindings (quantifiers, let, lambda)
Definition: std_expr.h:2846
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2848
quantifiert(exprt _expr, literalt _l)
Definition: boolbv.h:256
Definition: boolbv.h:42
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:274
virtual bvt convert_with(const with_exprt &expr)
Definition: boolbv_with.cpp:15
virtual bvt convert_array(const exprt &expr)
Flatten array.
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual literalt convert_bv_rel(const binary_relation_exprt &)
Flatten <, >, <= and >= expressions.
bv_cachet bv_cache
Definition: boolbv.h:130
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
std::size_t scope_counter
Definition: boolbv.h:277
virtual bvt convert_constraint_select_one(const exprt &expr)
void convert_update_rec(const exprt::operandst &designator, std::size_t d, const typet &type, std::size_t offset, const exprt &new_value, bvt &bv)
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:535
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)
virtual literalt convert_reduction(const unary_exprt &expr)
virtual literalt convert_ieee_float_rel(const binary_relation_exprt &)
std::unordered_map< const exprt, bvt, irep_hash > bv_cachet
Definition: boolbv.h:129
virtual bvt convert_complex_real(const complex_real_exprt &expr)
virtual bvt convert_complex(const complex_exprt &expr)
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:15
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:591
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition: boolbv.cpp:98
const boolbv_mapt & get_map() const
Definition: boolbv.h:92
unbounded_arrayt
Definition: boolbv.h:82
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Definition: boolbv.cpp:562
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
virtual bvt convert_bswap(const bswap_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:543
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
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:262
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
virtual bvt convert_add_sub(const exprt &expr)
virtual bvt convert_constant(const constant_exprt &expr)
numberingt< irep_idt > string_numbering
Definition: boolbv.h:274
virtual literalt convert_quantifier(const quantifier_exprt &expr)
void post_process() override
Definition: boolbv.h:75
boolbvt(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition: boolbv.h:44
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:483
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:279
void clear_cache() override
Definition: boolbv.h:69
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
virtual bvt convert_member(const member_exprt &expr)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:319
virtual bvt convert_cond(const cond_exprt &)
Definition: boolbv_cond.cpp:13
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
virtual bvt convert_union(const union_exprt &expr)
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Definition: boolbv.cpp:514
virtual bvt convert_byte_update(const byte_update_exprt &expr)
boolbv_widtht bv_width
Definition: boolbv.h:111
virtual literalt convert_extractbit(const extractbit_exprt &expr)
std::list< quantifiert > quantifier_listt
Definition: boolbv.h:265
unbounded_arrayt unbounded_array
Definition: boolbv.h:83
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:19
virtual bvt convert_floatbv_op(const ieee_float_op_exprt &)
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: boolbv.cpp:585
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:13
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:267
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual bvt convert_update(const update_exprt &)
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
virtual bvt convert_array_of(const array_of_exprt &expr)
Flatten arrays constructed from a single element.
bv_utilst bv_utils
Definition: boolbv.h:112
virtual bvt convert_floatbv_mod_rem(const binary_exprt &)
virtual bvt convert_bitwise(const exprt &expr)
virtual bvt convert_array_comprehension(const array_comprehension_exprt &)
Definition: boolbv.cpp:232
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_bv_reduction(const unary_exprt &expr)
virtual literalt convert_equality(const equal_exprt &expr)
functionst functions
Definition: boolbv.h:115
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
virtual bvt convert_vector(const vector_exprt &expr)
quantifier_listt quantifier_list
Definition: boolbv.h:266
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:103
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:97
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
Definition: boolbv.cpp:524
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:295
virtual literalt convert_overflow(const exprt &expr)
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:83
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
arrayst SUB
Definition: boolbv.h:125
virtual bvt convert_power(const binary_exprt &expr)
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:44
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:85
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
virtual bvt convert_concatenation(const concatenation_exprt &expr)
virtual bvt convert_struct(const struct_exprt &expr)
void post_process_quantifiers()
virtual bvt convert_replication(const replication_exprt &expr)
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:330
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:270
virtual bvt convert_abs(const abs_exprt &expr)
Definition: boolbv_abs.cpp:17
boolbv_mapt map
Definition: boolbv.h:118
The byte swap expression.
Expression of type type extracted from some object op starting at position offset (given in number of...
Expression corresponding to op() where the bytes starting at position offset (given in number of byte...
Complex constructor from a pair of numbers.
Definition: std_expr.h:1707
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1820
Real part of the expression describing a complex number.
Definition: std_expr.h:1775
Concatenation of bit-vector operands.
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:3065
A constant literal expression.
Definition: std_expr.h:2753
Division.
Definition: std_expr.h:1064
Maps a big-endian offset to a little-endian offset.
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
Extracts a single bit of a bit-vector operand.
Extracts a sub-range of a bit-vector operand.
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
Application of (mathematical) function.
virtual void post_process()
Definition: functions.h:36
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
The trinary if-then-else operator.
Definition: std_expr.h:2172
Array index operator.
Definition: std_expr.h:1328
A let expression.
Definition: std_expr.h:2919
Extract member of struct or union.
Definition: std_expr.h:2613
Modulo defined as lhs-(rhs * truncate(lhs/rhs)).
Definition: std_expr.h:1135
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1019
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
Boolean negation.
Definition: std_expr.h:2127
virtual void clear_cache()
TO_BE_DOCUMENTED.
Definition: prop.h:23
A base class for quantifier expressions.
Bit-vector replication.
Struct constructor from list of elements.
Definition: std_expr.h:1668
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
Generic base class for unary expressions.
Definition: std_expr.h:281
The unary minus expression.
Definition: std_expr.h:390
Union constructor from single element.
Definition: std_expr.h:1602
The union type.
Definition: c_types.h:112
Operator to update elements in structs and arrays.
Definition: std_expr.h:2442
Vector constructor from list of elements.
Definition: std_expr.h:1566
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
Uninterpreted Functions.
std::vector< literalt > bvt
Definition: literal.h:201
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:12