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/byte_operators.h>
18 #include <util/expr.h>
19 #include <util/mp_arith.h>
20 #include <util/optional.h>
21 
22 #include "bv_utils.h"
23 #include "boolbv_width.h"
24 #include "boolbv_map.h"
25 #include "arrays.h"
26 #include "functions.h"
27 
28 class extractbit_exprt;
29 class extractbits_exprt;
30 class member_exprt;
31 
32 class boolbvt:public arrayst
33 {
34 public:
36  const namespacet &_ns,
37  propt &_prop):
38  arrayst(_ns, _prop),
40  boolbv_width(_ns),
41  bv_utils(_prop),
42  functions(*this),
43  map(_prop, _ns, boolbv_width)
44  {
45  }
46 
47  virtual const bvt &convert_bv( // check cache
48  const exprt &expr,
49  const optionalt<std::size_t> expected_width = nullopt);
50 
51  virtual bvt convert_bitvector(const exprt &expr); // no cache
52 
53  // overloading
54  exprt get(const exprt &expr) const override;
55  void set_to(const exprt &expr, bool value) override;
56  void print_assignment(std::ostream &out) const override;
57 
58  void clear_cache() override
59  {
61  bv_cache.clear();
62  }
63 
64  void post_process() override
65  {
69  }
70 
71  // get literals for variables/expressions, if available
72  virtual bool literal(
73  const exprt &expr,
74  std::size_t bit,
75  literalt &literal) const;
76 
77  enum class unbounded_arrayt { U_NONE, U_ALL, U_AUTO };
79 
81  {
82  return get_value(bv, 0, bv.size());
83  }
84 
85  mp_integer get_value(const bvt &bv, std::size_t offset, std::size_t width);
86 
87  const boolbv_mapt &get_map() const
88  {
89  return map;
90  }
91 
93 
94 protected:
96 
97  // uninterpreted functions
99 
100  // the mapping from identifiers to literals
102 
103  // overloading
104  literalt convert_rest(const exprt &expr) override;
105  virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
106 
107  // NOLINTNEXTLINE(readability/identifiers)
108  typedef arrayst SUB;
109 
110  void conversion_failed(const exprt &expr, bvt &bv)
111  {
112  bv=conversion_failed(expr);
113  }
114 
115  bvt conversion_failed(const exprt &expr);
116 
117  typedef std::unordered_map<const exprt, bvt, irep_hash> bv_cachet;
119 
120  bool type_conversion(
121  const typet &src_type, const bvt &src,
122  const typet &dest_type, bvt &dest);
123 
124  virtual literalt convert_bv_rel(const exprt &expr);
125  virtual literalt convert_typecast(const typecast_exprt &expr);
126  virtual literalt convert_reduction(const unary_exprt &expr);
127  virtual literalt convert_onehot(const unary_exprt &expr);
128  virtual literalt convert_extractbit(const extractbit_exprt &expr);
129  virtual literalt convert_overflow(const exprt &expr);
130  virtual literalt convert_equality(const equal_exprt &expr);
132  const binary_relation_exprt &expr);
133  virtual literalt convert_ieee_float_rel(const exprt &expr);
134  virtual literalt convert_quantifier(const quantifier_exprt &expr);
135 
136  virtual bvt convert_index(const exprt &array, const mp_integer &index);
137  virtual bvt convert_index(const index_exprt &expr);
138  virtual bvt convert_bswap(const bswap_exprt &expr);
139  virtual bvt convert_byte_extract(const byte_extract_exprt &expr);
140  virtual bvt convert_byte_update(const byte_update_exprt &expr);
141  virtual bvt convert_constraint_select_one(const exprt &expr);
142  virtual bvt convert_if(const if_exprt &expr);
143  virtual bvt convert_struct(const struct_exprt &expr);
144  virtual bvt convert_array(const exprt &expr);
145  virtual bvt convert_vector(const vector_exprt &expr);
146  virtual bvt convert_complex(const complex_exprt &expr);
147  virtual bvt convert_complex_real(const complex_real_exprt &expr);
148  virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
149  virtual bvt convert_lambda(const exprt &expr);
150  virtual bvt convert_let(const let_exprt &);
151  virtual bvt convert_array_of(const array_of_exprt &expr);
152  virtual bvt convert_union(const union_exprt &expr);
153  virtual bvt convert_bv_typecast(const typecast_exprt &expr);
154  virtual bvt convert_add_sub(const exprt &expr);
155  virtual bvt convert_mult(const mult_exprt &expr);
156  virtual bvt convert_div(const div_exprt &expr);
157  virtual bvt convert_mod(const mod_exprt &expr);
158  virtual bvt convert_floatbv_op(const exprt &expr);
160  virtual bvt convert_member(const member_exprt &expr);
161  virtual bvt convert_with(const exprt &expr);
162  virtual bvt convert_update(const exprt &expr);
163  virtual bvt convert_case(const exprt &expr);
164  virtual bvt convert_cond(const cond_exprt &);
165  virtual bvt convert_shift(const binary_exprt &expr);
166  virtual bvt convert_bitwise(const exprt &expr);
167  virtual bvt convert_unary_minus(const unary_minus_exprt &expr);
168  virtual bvt convert_abs(const abs_exprt &expr);
169  virtual bvt convert_concatenation(const concatenation_exprt &expr);
170  virtual bvt convert_replication(const replication_exprt &expr);
171  virtual bvt convert_bv_literals(const exprt &expr);
172  virtual bvt convert_constant(const constant_exprt &expr);
173  virtual bvt convert_extractbits(const extractbits_exprt &expr);
174  virtual bvt convert_symbol(const exprt &expr);
175  virtual bvt convert_bv_reduction(const unary_exprt &expr);
176  virtual bvt convert_not(const not_exprt &expr);
177  virtual bvt convert_power(const binary_exprt &expr);
179  const function_application_exprt &expr);
180 
181  virtual exprt make_bv_expr(const typet &type, const bvt &bv);
182  virtual exprt make_free_bv_expr(const typet &type);
183 
184  void convert_with(
185  const typet &type,
186  const exprt &op1,
187  const exprt &op2,
188  const bvt &prev_bv,
189  bvt &next_bv);
190 
191  void convert_with_bv(
192  const exprt &op1,
193  const exprt &op2,
194  const bvt &prev_bv,
195  bvt &next_bv);
196 
197  void convert_with_array(
198  const array_typet &type,
199  const exprt &op1,
200  const exprt &op2,
201  const bvt &prev_bv,
202  bvt &next_bv);
203 
204  void convert_with_union(
205  const union_typet &type,
206  const exprt &op2,
207  const bvt &prev_bv,
208  bvt &next_bv);
209 
210  void convert_with_struct(
211  const struct_typet &type,
212  const exprt &op1,
213  const exprt &op2,
214  const bvt &prev_bv,
215  bvt &next_bv);
216 
217  void convert_update_rec(
218  const exprt::operandst &designator,
219  std::size_t d,
220  const typet &type,
221  std::size_t offset,
222  const exprt &new_value,
223  bvt &bv);
224 
225  virtual exprt bv_get_unbounded_array(const exprt &) const;
226 
227  virtual exprt bv_get_rec(
228  const bvt &bv,
229  const std::vector<bool> &unknown,
230  std::size_t offset,
231  const typet &type) const;
232 
233  exprt bv_get(const bvt &bv, const typet &type) const;
234  exprt bv_get_cache(const exprt &expr) const;
235 
236  // unbounded arrays
237  bool is_unbounded_array(const typet &type) const override;
238 
239  // quantifier instantiations
241  {
242  public:
245  };
246 
247  typedef std::list<quantifiert> quantifier_listt;
249 
251 
252  typedef std::vector<std::size_t> offset_mapt;
254 
255  // strings
257 };
258 
259 #endif // CPROVER_SOLVERS_FLATTENING_BOOLBV_H
boolbvt(const namespacet &_ns, propt &_prop)
Definition: boolbv.h:35
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
The type of an expression, extends irept.
Definition: type.h:27
void print_assignment(std::ostream &out) const override
Definition: boolbv.cpp:648
std::vector< std::size_t > offset_mapt
Definition: boolbv.h:252
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
virtual bvt convert_with(const exprt &expr)
Definition: boolbv_with.cpp:19
Boolean negation.
Definition: std_expr.h:3308
Semantic type conversion.
Definition: std_expr.h:2277
bv_utilst bv_utils
Definition: boolbv.h:95
virtual literalt convert_ieee_float_rel(const exprt &expr)
BigInt mp_integer
Definition: mp_arith.h:22
virtual bvt convert_array_of(const array_of_exprt &expr)
arrayst SUB
Definition: boolbv.h:108
virtual bvt convert_bv_reduction(const unary_exprt &expr)
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
Application of (mathematical) function.
Definition: std_expr.h:4481
void post_process() override
Definition: arrays.h:33
virtual exprt bv_get_unbounded_array(const exprt &) const
Definition: boolbv_get.cpp:295
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual literalt convert_overflow(const exprt &expr)
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
Definition: boolbv.h:92
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:624
virtual bvt convert_replication(const replication_exprt &expr)
virtual bvt convert_bv_literals(const exprt &expr)
Definition: boolbv.cpp:359
virtual bvt convert_struct(const struct_exprt &expr)
virtual bvt convert_function_application(const function_application_exprt &expr)
Definition: boolbv.cpp:415
void clear_cache() override
Definition: boolbv.h:58
The trinary if-then-else operator.
Definition: std_expr.h:3427
virtual bvt convert_lambda(const exprt &expr)
Definition: boolbv.cpp:310
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
A constant literal expression.
Definition: std_expr.h:4384
Structure type, corresponds to C style structs.
Definition: std_types.h:276
void post_process() override
Definition: boolbv.h:64
virtual bvt convert_constant(const constant_exprt &expr)
Imaginary part of the expression describing a complex number.
Definition: std_expr.h:2087
virtual bvt convert_symbol(const exprt &expr)
Definition: boolbv.cpp:380
Definition: boolbv.h:32
Extract member of struct or union.
Definition: std_expr.h:3890
Concatenation of bit-vector operands.
Definition: std_expr.h:4558
Equality.
Definition: std_expr.h:1484
virtual bvt convert_update(const exprt &expr)
virtual void clear_cache()
Definition: prop_conv.h:115
virtual bvt convert_abs(const abs_exprt &expr)
Definition: boolbv_abs.cpp:17
virtual literalt convert_bv_rel(const exprt &expr)
virtual bvt convert_cond(const cond_exprt &)
Definition: boolbv_cond.cpp:13
Expression classes for byte-level operators.
virtual bvt convert_add_sub(const exprt &expr)
Division.
Definition: std_expr.h:1211
virtual bvt convert_unary_minus(const unary_minus_exprt &expr)
A base class for binary expressions.
Definition: std_expr.h:738
virtual literalt convert_reduction(const unary_exprt &expr)
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Real part of the expression describing a complex number.
Definition: std_expr.h:2040
Theory of Arrays with Extensionality.
virtual bvt convert_complex_real(const complex_real_exprt &expr)
virtual bvt convert_bswap(const bswap_exprt &expr)
virtual bvt convert_complex(const complex_exprt &expr)
functionst functions
Definition: boolbv.h:98
offset_mapt build_offset_map(const struct_typet &src)
Definition: boolbv.cpp:655
nonstd::optional< T > optionalt
Definition: optional.h:35
Union constructor from single element.
Definition: std_expr.h:1840
Extracts a sub-range of a bit-vector operand.
Definition: std_expr.h:3157
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:168
virtual bvt convert_floatbv_op(const exprt &expr)
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
Generic base class for unary expressions.
Definition: std_expr.h:331
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
Definition: boolbv.cpp:562
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
Definition: boolbv.cpp:32
numbering< irep_idt > string_numbering
Definition: boolbv.h:256
virtual bvt convert_union(const union_exprt &expr)
Array constructor from single element.
Definition: std_expr.h:1678
virtual bvt convert_extractbits(const extractbits_exprt &expr)
Vector constructor from list of elements.
Definition: std_expr.h:1800
Definition: arrays.h:28
The unary minus expression.
Definition: std_expr.h:469
quantifier_listt quantifier_list
Definition: boolbv.h:248
literalt convert_rest(const exprt &expr) override
Definition: boolbv.cpp:426
TO_BE_DOCUMENTED.
Definition: prop.h:24
bool type_conversion(const typet &src_type, const bvt &src, const typet &dest_type, bvt &dest)
virtual bvt convert_let(const let_exprt &)
Definition: boolbv_let.cpp:14
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
void post_process_quantifiers()
std::vector< exprt > operandst
Definition: expr.h:57
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
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)
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual bvt convert_concatenation(const concatenation_exprt &expr)
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
mp_integer get_value(const bvt &bv)
Definition: boolbv.h:80
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:614
virtual bvt convert_complex_imag(const complex_imag_exprt &expr)
virtual bvt convert_constraint_select_one(const exprt &expr)
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
unbounded_arrayt unbounded_array
Definition: boolbv.h:78
virtual bvt convert_vector(const vector_exprt &expr)
virtual bvt convert_array(const exprt &expr)
bv_cachet bv_cache
Definition: boolbv.h:118
Uninterpreted Functions.
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2336
Base class for all expressions.
Definition: expr.h:54
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Absolute value.
Definition: std_expr.h:419
The union type.
Definition: std_types.h:425
virtual exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
Definition: boolbv_get.cpp:68
virtual bvt convert_mod(const mod_exprt &expr)
Definition: boolbv_mod.cpp:12
A base class for quantifier expressions.
Definition: std_expr.h:4708
virtual bvt convert_member(const member_exprt &expr)
const boolbv_mapt & get_map() const
Definition: boolbv.h:87
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
Arrays with given size.
Definition: std_types.h:1000
TO_BE_DOCUMENTED.
exprt bv_get(const bvt &bv, const typet &type) const
Definition: boolbv_get.cpp:275
boolbv_mapt map
Definition: boolbv.h:101
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
exprt bv_get_cache(const exprt &expr) const
Definition: boolbv_get.cpp:282
virtual bvt convert_div(const div_exprt &expr)
Definition: boolbv_div.cpp:13
std::list< quantifiert > quantifier_listt
Definition: boolbv.h:247
A let expression.
Definition: std_expr.h:4635
virtual exprt make_bv_expr(const typet &type, const bvt &bv)
Definition: boolbv.cpp:603
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:593
virtual literalt convert_extractbit(const extractbit_exprt &expr)
TO_BE_DOCUMENTED.
Struct constructor from list of elements.
Definition: std_expr.h:1920
virtual literalt convert_quantifier(const quantifier_exprt &expr)
Bit-vector replication.
Definition: std_expr.h:3004
virtual bvt convert_mult(const mult_exprt &expr)
Definition: boolbv_mult.cpp:13
std::unordered_map< const exprt, bvt, irep_hash > bv_cachet
Definition: boolbv.h:117
std::vector< literalt > bvt
Definition: literal.h:200
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
Complex constructor from a pair of numbers.
Definition: std_expr.h:1962
Modulo.
Definition: std_expr.h:1287
virtual bvt convert_bitwise(const exprt &expr)
The byte swap expression.
Definition: std_expr.h:568
virtual void post_process()
Definition: functions.h:34
unbounded_arrayt
Definition: boolbv.h:77
virtual bvt convert_power(const binary_exprt &expr)
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:4868
Extracts a single bit of a bit-vector operand.
Definition: std_expr.h:3080
Array index operator.
Definition: std_expr.h:1595