cprover
boolbv.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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
31class bswap_exprt;
39class member_exprt;
41class union_typet;
42
43class boolbvt:public arrayst
44{
45public:
47 const namespacet &_ns,
48 propt &_prop,
50 bool get_array_constraints = false)
53 bv_width(_ns),
54 bv_utils(_prop),
55 functions(*this),
56 map(_prop)
57 {
58 }
59
60 virtual const bvt &convert_bv( // check cache
61 const exprt &expr,
62 const optionalt<std::size_t> expected_width = nullopt);
63
64 virtual bvt convert_bitvector(const exprt &expr); // no cache
65
66 // overloading
67 exprt get(const exprt &expr) const override;
68 void set_to(const exprt &expr, bool value) override;
69 void print_assignment(std::ostream &out) const override;
70
71 void clear_cache() override
72 {
74 bv_cache.clear();
75 }
76
78 {
82 }
83
84 enum class unbounded_arrayt { U_NONE, U_ALL, U_AUTO };
86
88 {
89 return get_value(bv, 0, bv.size());
90 }
91
92 mp_integer get_value(const bvt &bv, std::size_t offset, std::size_t width);
93
94 const boolbv_mapt &get_map() const
95 {
96 return map;
97 }
98
99 virtual std::size_t boolbv_width(const typet &type) const
100 {
101 return bv_width(type);
102 }
103
104 virtual endianness_mapt
105 endianness_map(const typet &type, bool little_endian) const
106 {
107 return endianness_mapt{type, little_endian, ns};
108 }
109
110 virtual endianness_mapt endianness_map(const typet &type) const;
111
112protected:
115
116 // uninterpreted functions
118
119 // the mapping from identifiers to literals
121
122 // overloading
123 literalt convert_rest(const exprt &expr) override;
124 virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
125
126 // NOLINTNEXTLINE(readability/identifiers)
127 typedef arrayst SUB;
128
129 bvt conversion_failed(const exprt &expr);
130
131 typedef std::unordered_map<const exprt, bvt, irep_hash> bv_cachet;
133
134 bool type_conversion(
135 const typet &src_type, const bvt &src,
136 const typet &dest_type, bvt &dest);
137
139 virtual literalt convert_typecast(const typecast_exprt &expr);
140 virtual literalt convert_reduction(const unary_exprt &expr);
141 virtual literalt convert_onehot(const unary_exprt &expr);
142 virtual literalt convert_extractbit(const extractbit_exprt &expr);
143 virtual literalt convert_overflow(const exprt &expr);
144 virtual literalt convert_equality(const equal_exprt &expr);
146 const binary_relation_exprt &expr);
148 virtual literalt convert_quantifier(const quantifier_exprt &expr);
149
150 virtual bvt convert_index(const exprt &array, const mp_integer &index);
151 virtual bvt convert_index(const index_exprt &expr);
152 virtual bvt convert_bswap(const bswap_exprt &expr);
153 virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
154 virtual bvt convert_byte_update(const byte_update_exprt &expr);
155 virtual bvt convert_constraint_select_one(const exprt &expr);
156 virtual bvt convert_if(const if_exprt &expr);
157 virtual bvt convert_struct(const struct_exprt &expr);
158 virtual bvt convert_array(const exprt &expr);
159 virtual bvt convert_vector(const vector_exprt &expr);
160 virtual bvt convert_complex(const complex_exprt &expr);
161 virtual bvt convert_complex_real(const complex_real_exprt &expr);
162 virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
164 virtual bvt convert_let(const let_exprt &);
165 virtual bvt convert_array_of(const array_of_exprt &expr);
166 virtual bvt convert_union(const union_exprt &expr);
167 virtual bvt convert_empty_union(const empty_union_exprt &expr);
168 virtual bvt convert_bv_typecast(const typecast_exprt &expr);
169 virtual bvt convert_add_sub(const exprt &expr);
170 virtual bvt convert_mult(const mult_exprt &expr);
171 virtual bvt convert_div(const div_exprt &expr);
172 virtual bvt convert_mod(const mod_exprt &expr);
176 virtual bvt convert_member(const member_exprt &expr);
177 virtual bvt convert_with(const with_exprt &expr);
178 virtual bvt convert_update(const update_exprt &);
179 virtual bvt convert_case(const exprt &expr);
180 virtual bvt convert_cond(const cond_exprt &);
181 virtual bvt convert_shift(const binary_exprt &expr);
182 virtual bvt convert_bitwise(const exprt &expr);
183 virtual bvt convert_unary_minus(const unary_minus_exprt &expr);
184 virtual bvt convert_abs(const abs_exprt &expr);
185 virtual bvt convert_concatenation(const concatenation_exprt &expr);
186 virtual bvt convert_replication(const replication_exprt &expr);
187 virtual bvt convert_bv_literals(const exprt &expr);
188 virtual bvt convert_constant(const constant_exprt &expr);
189 virtual bvt convert_extractbits(const extractbits_exprt &expr);
190 virtual bvt convert_symbol(const exprt &expr);
191 virtual bvt convert_bv_reduction(const unary_exprt &expr);
192 virtual bvt convert_not(const not_exprt &expr);
193 virtual bvt convert_power(const binary_exprt &expr);
195 const function_application_exprt &expr);
196 virtual bvt convert_bitreverse(const bitreverse_exprt &expr);
197
198 virtual exprt make_bv_expr(const typet &type, const bvt &bv);
199 virtual exprt make_free_bv_expr(const typet &type);
200
201 void convert_with(
202 const typet &type,
203 const exprt &op1,
204 const exprt &op2,
205 const bvt &prev_bv,
206 bvt &next_bv);
207
208 void convert_with_bv(
209 const exprt &op1,
210 const exprt &op2,
211 const bvt &prev_bv,
212 bvt &next_bv);
213
215 const array_typet &type,
216 const exprt &op1,
217 const exprt &op2,
218 const bvt &prev_bv,
219 bvt &next_bv);
220
222 const union_typet &type,
223 const exprt &op2,
224 const bvt &prev_bv,
225 bvt &next_bv);
226
228 const struct_typet &type,
229 const exprt &op1,
230 const exprt &op2,
231 const bvt &prev_bv,
232 bvt &next_bv);
233
235 const exprt::operandst &designator,
236 std::size_t d,
237 const typet &type,
238 std::size_t offset,
239 const exprt &new_value,
240 bvt &bv);
241
242 virtual exprt bv_get_unbounded_array(const exprt &) const;
243
244 virtual exprt bv_get_rec(
245 const exprt &expr,
246 const bvt &bv,
247 std::size_t offset,
248 const typet &type) const;
249
250 exprt bv_get(const bvt &bv, const typet &type) const;
251 exprt bv_get_cache(const exprt &expr) const;
252
253 // unbounded arrays
254 bool is_unbounded_array(const typet &type) const override;
255
256 // quantifier instantiations
258 {
259 public:
261 : expr(std::move(_expr)), l(std::move(_l))
262 {
263 }
264
267 };
268
269 typedef std::list<quantifiert> quantifier_listt;
271
273
274 typedef std::vector<std::size_t> offset_mapt;
276
277 // strings
279
280 // scopes
281 std::size_t scope_counter = 0;
282
285};
286
287#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:3182
Array constructor from single element.
Definition: std_expr.h:1411
Arrays with given size.
Definition: std_types.h:763
Definition: arrays.h:33
const namespacet & ns
Definition: arrays.h:56
message_handlert & message_handler
Definition: arrays.h:58
void finish_eager_conversion() override
Definition: arrays.h:41
bool get_array_constraints
Definition: arrays.h:113
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:2900
std::vector< symbol_exprt > variablest
Definition: std_expr.h:2902
Reverse the order of bits in a bit-vector.
quantifiert(exprt _expr, literalt _l)
Definition: boolbv.h:260
Definition: boolbv.h:44
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:278
virtual bvt convert_with(const with_exprt &expr)
Definition: boolbv_with.cpp:16
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:132
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:281
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:539
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:131
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:595
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
unbounded_arrayt
Definition: boolbv.h:84
binding_exprt::variablest fresh_binding(const binding_exprt &)
create new, unique variables for the given binding
Definition: boolbv.cpp:566
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:547
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
void finish_eager_conversion_quantifiers()
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:269
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:278
virtual literalt convert_quantifier(const quantifier_exprt &expr)
boolbvt(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
Definition: boolbv.h:46
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:487
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:286
void clear_cache() override
Definition: boolbv.h:71
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:323
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_empty_union(const empty_union_exprt &expr)
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:518
virtual bvt convert_byte_update(const byte_update_exprt &expr)
boolbv_widtht bv_width
Definition: boolbv.h:113
virtual literalt convert_extractbit(const extractbit_exprt &expr)
const boolbv_mapt & get_map() const
Definition: boolbv.h:94
std::list< quantifiert > quantifier_listt
Definition: boolbv.h:269
unbounded_arrayt unbounded_array
Definition: boolbv.h:85
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: boolbv_get.cpp:20
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:589
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:274
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual bvt convert_update(const update_exprt &)
void finish_eager_conversion() override
Definition: boolbv.h:77
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:114
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:236
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:117
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:270
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:105
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
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:528
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:299
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:88
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
arrayst SUB
Definition: boolbv.h:127
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:45
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:87
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)
virtual bvt convert_bitreverse(const bitreverse_exprt &expr)
virtual bvt convert_replication(const replication_exprt &expr)
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:334
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:274
virtual bvt convert_abs(const abs_exprt &expr)
Definition: boolbv_abs.cpp:17
boolbv_mapt map
Definition: boolbv.h:120
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:1761
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:1874
Real part of the expression describing a complex number.
Definition: std_expr.h:1829
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:3119
A constant literal expression.
Definition: std_expr.h:2807
Division.
Definition: std_expr.h:1064
Union constructor to support unions without any member (a GCC/Clang feature).
Definition: std_expr.h:1677
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 finish_eager_conversion()
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:2226
Array index operator.
Definition: std_expr.h:1328
A let expression.
Definition: std_expr.h:2973
Extract member of struct or union.
Definition: std_expr.h:2667
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:2181
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:1722
Structure type, corresponds to C style structs.
Definition: std_types.h:231
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
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:1611
The union type.
Definition: c_types.h:125
Operator to update elements in structs and arrays.
Definition: std_expr.h:2496
Vector constructor from list of elements.
Definition: std_expr.h:1575
Operator to update elements in structs and arrays.
Definition: std_expr.h:2312
Uninterpreted Functions.
std::vector< literalt > bvt
Definition: literal.h:201
STL namespace.
nonstd::optional< T > optionalt
Definition: optional.h:35
BigInt mp_integer
Definition: smt_terms.h:12