cprover
smt2_conv.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_SMT2_SMT2_CONV_H
11 #define CPROVER_SOLVERS_SMT2_SMT2_CONV_H
12 
13 #include <sstream>
14 #include <set>
15 
16 #include <util/byte_operators.h>
17 #include <util/c_types.h>
18 #include <util/floatbv_expr.h>
19 #include <util/std_expr.h>
20 
21 #if !HASH_CODE
23 #endif
24 
25 #include <solvers/prop/prop_conv.h>
28 
29 #include "letify.h"
30 
31 class typecast_exprt;
32 class constant_exprt;
33 class index_exprt;
34 class member_exprt;
35 
37 {
38 public:
39  enum class solvert
40  {
41  GENERIC,
42  BOOLECTOR,
44  CVC3,
45  CVC4,
46  MATHSAT,
47  YICES,
48  Z3
49  };
50 
51  smt2_convt(
52  const namespacet &_ns,
53  const std::string &_benchmark,
54  const std::string &_notes,
55  const std::string &_logic,
56  solvert _solver,
57  std::ostream &_out);
58 
59  ~smt2_convt() override = default;
60 
68 
69  exprt handle(const exprt &expr) override;
70  void set_to(const exprt &expr, bool value) override;
71  exprt get(const exprt &expr) const override;
72  std::string decision_procedure_text() const override;
73  void print_assignment(std::ostream &out) const override;
74 
76  void push() override;
77 
79  void push(const std::vector<exprt> &_assumptions) override;
80 
82  void pop() override;
83 
84  std::size_t get_number_of_solver_calls() const override;
85 
86 protected:
87  const namespacet &ns;
88  std::ostream &out;
89  std::string benchmark, notes, logic;
91 
92  std::vector<exprt> assumptions;
94 
95  std::size_t number_of_solver_calls = 0;
96 
97  resultt dec_solve() override;
98 
99  void write_header();
100  void write_footer(std::ostream &);
101 
102  // tweaks for arrays
103  bool use_array_theory(const exprt &);
104  void flatten_array(const exprt &);
105 
106  // specific expressions go here
107  void convert_typecast(const typecast_exprt &expr);
109  void convert_struct(const struct_exprt &expr);
110  void convert_union(const union_exprt &expr);
111  void convert_constant(const constant_exprt &expr);
114  void convert_plus(const plus_exprt &expr);
115  void convert_minus(const minus_exprt &expr);
116  void convert_div(const div_exprt &expr);
117  void convert_mult(const mult_exprt &expr);
118  void convert_rounding_mode_FPA(const exprt &expr);
119  void convert_floatbv_plus(const ieee_float_op_exprt &expr);
120  void convert_floatbv_minus(const ieee_float_op_exprt &expr);
121  void convert_floatbv_div(const ieee_float_op_exprt &expr);
122  void convert_floatbv_mult(const ieee_float_op_exprt &expr);
123  void convert_mod(const mod_exprt &expr);
124  void convert_index(const index_exprt &expr);
125  void convert_member(const member_exprt &expr);
126 
127  void convert_with(const with_exprt &expr);
128  void convert_update(const exprt &expr);
129 
130  std::string convert_identifier(const irep_idt &identifier);
131 
132  void convert_expr(const exprt &);
133  void convert_type(const typet &);
134  void convert_literal(const literalt);
135 
136  literalt convert(const exprt &expr);
137  tvt l_get(literalt l) const;
138 
139  // auxiliary methods
140  exprt prepare_for_convert_expr(const exprt &expr);
141  exprt lower_byte_operators(const exprt &expr);
142  void find_symbols(const exprt &expr);
143  void find_symbols(const typet &type);
144  void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
145 
146  // letification
148 
149  // Parsing solver responses
150  constant_exprt parse_literal(const irept &, const typet &type);
151  struct_exprt parse_struct(const irept &s, const struct_typet &type);
152  exprt parse_union(const irept &s, const union_typet &type);
153  exprt parse_array(const irept &s, const array_typet &type);
154  exprt parse_rec(const irept &s, const typet &type);
155 
156  // we use this to build a bit-vector encoding of the FPA theory
157  void convert_floatbv(const exprt &expr);
158  std::string type2id(const typet &) const;
159  std::string floatbv_suffix(const exprt &) const;
160  std::set<irep_idt> bvfp_set; // already converted
161 
163  {
164  public:
165  smt2_symbolt(const irep_idt &_identifier, const typet &_type)
166  : nullary_exprt(ID_smt2_symbol, _type)
167  { set(ID_identifier, _identifier); }
168 
169  const irep_idt &get_identifier() const
170  {
171  return get(ID_identifier);
172  }
173  };
174 
175  const smt2_symbolt &to_smt2_symbol(const exprt &expr)
176  {
177  assert(expr.id()==ID_smt2_symbol && !expr.has_operands());
178  return static_cast<const smt2_symbolt&>(expr);
179  }
180 
181  // flattens any non-bitvector type into a bitvector,
182  // e.g., booleans, vectors, structs, arrays but also
183  // floats when using the FPA theory.
184  // unflatten() does the opposite.
185  enum class wheret { BEGIN, END };
186  void flatten2bv(const exprt &);
187  void unflatten(wheret, const typet &, unsigned nesting=0);
188 
189  // pointers
192  const exprt &expr, const pointer_typet &result_type);
193 
194  void define_object_size(const irep_idt &id, const exprt &expr);
195 
196  // keeps track of all non-Boolean symbols and their value
197  struct identifiert
198  {
199  bool is_bound;
202 
204  {
205  type.make_nil();
206  value.make_nil();
207  }
208  };
209 
210  typedef std::unordered_map<irep_idt, identifiert> identifier_mapt;
211 
213 
214  // for modeling structs as SMT datatype when use_datatype is set
215  //
216  // it maintains a map of `struct_typet` or `struct_tag_typet`
217  // to datatype names declared in SMT
218  typedef std::map<typet, std::string> datatype_mapt;
220 
221  // for replacing various defined expressions:
222  //
223  // ID_array_of
224  // ID_array
225  // ID_string_constant
226 
227  typedef std::map<exprt, irep_idt> defined_expressionst;
229 
231 
232  typedef std::set<std::string> smt2_identifierst;
234 
235  // Boolean part
236  std::size_t no_boolean_variables;
237  std::vector<bool> boolean_assignment;
238 };
239 
240 #endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:2172
smt2_convt::set_to
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: smt2_conv.cpp:4232
smt2_convt::convert_typecast
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:2045
smt2_convt::solvert::CVC4
@ CVC4
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
smt2_convt::solver
solvert solver
Definition: smt2_conv.h:90
smt2_convt::solvert::CPROVER_SMT2
@ CPROVER_SMT2
smt2_convt::print_assignment
void print_assignment(std::ostream &out) const override
Print satisfying assignment to out.
Definition: smt2_conv.cpp:122
letifyt
Introduce LET for common subexpressions.
Definition: letify.h:17
smt2_convt::wheret
wheret
Definition: smt2_conv.h:185
smt2_convt::get_number_of_solver_calls
std::size_t get_number_of_solver_calls() const override
Return the number of incremental solver calls.
Definition: smt2_conv.cpp:5024
smt2_convt::wheret::END
@ END
smt2_convt::letify
letifyt letify
Definition: smt2_conv.h:147
smt2_convt::convert_type
void convert_type(const typet &)
Definition: smt2_conv.cpp:4677
irept::make_nil
void make_nil()
Definition: irep.h:465
typet
The type of an expression, extends irept.
Definition: type.h:28
smt2_convt::pop
void pop() override
Currently, only implements a single stack element (no nested contexts)
Definition: smt2_conv.cpp:793
smt2_convt::datatype_map
datatype_mapt datatype_map
Definition: smt2_conv.h:219
smt2_convt::parse_array
exprt parse_array(const irept &s, const array_typet &type)
Definition: smt2_conv.cpp:459
smt2_convt::use_array_theory
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4656
smt2_convt::convert_floatbv
void convert_floatbv(const exprt &expr)
Definition: smt2_conv.cpp:873
smt2_convt::use_datatypes
bool use_datatypes
Definition: smt2_conv.h:65
smt2_convt::convert
literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:720
smt2_convt::smt2_symbolt::smt2_symbolt
smt2_symbolt(const irep_idt &_identifier, const typet &_type)
Definition: smt2_conv.h:165
smt2_convt::solvert::MATHSAT
@ MATHSAT
smt2_convt::convert_update
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:3873
union_exprt
Union constructor from single element.
Definition: std_expr.h:1516
smt2_convt::convert_plus
void convert_plus(const plus_exprt &expr)
Definition: smt2_conv.cpp:3122
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
smt2_convt::convert_floatbv_plus
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3311
exprt
Base class for all expressions.
Definition: expr.h:54
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:281
smt2_convt::convert_expr
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:907
smt2_convt::identifier_mapt
std::unordered_map< irep_idt, identifiert > identifier_mapt
Definition: smt2_conv.h:210
smt2_convt::convert_constant
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2852
smt2_convt::convert_literal
void convert_literal(const literalt)
Definition: smt2_conv.cpp:761
smt2_convt::handle
exprt handle(const exprt &expr) override
Generate a handle, which is an expression that has the same value as the argument in any model that i...
Definition: smt2_conv.cpp:752
pointer_logict
Definition: pointer_logic.h:23
stack_decision_proceduret
Definition: stack_decision_procedure.h:58
div_exprt
Division.
Definition: std_expr.h:980
smt2_convt::~smt2_convt
~smt2_convt() override=default
smt2_convt::solvert::CVC3
@ CVC3
smt2_convt::type2id
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:829
smt2_convt::flatten_array
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
Definition: smt2_conv.cpp:2788
irep_hash_container.h
IREP Hash Container.
smt2_convt::solvert::BOOLECTOR
@ BOOLECTOR
smt2_convt::convert_is_dynamic_object
void convert_is_dynamic_object(const unary_exprt &)
Definition: smt2_conv.cpp:3002
smt2_convt::convert_index
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:3880
smt2_convt::convert_rounding_mode_FPA
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:3254
struct_exprt
Struct constructor from list of elements.
Definition: std_expr.h:1582
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
smt2_convt::notes
std::string notes
Definition: smt2_conv.h:89
nullary_exprt
An expression without operands.
Definition: std_expr.h:22
smt2_convt::to_smt2_symbol
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition: smt2_conv.h:175
smt2_convt::number_of_solver_calls
std::size_t number_of_solver_calls
Definition: smt2_conv.h:95
pointer_logic.h
Pointer Logic.
smt2_convt::convert_mult
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3531
byte_operators.h
Expression classes for byte-level operators.
smt2_convt::convert_identifier
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:798
smt2_convt::convert_floatbv_div
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3511
smt2_convt::prepare_for_convert_expr
exprt prepare_for_convert_expr(const exprt &expr)
Perform steps necessary before an expression is passed to convert_expr.
Definition: smt2_conv.cpp:4361
smt2_convt::push
void push() override
Unimplemented.
Definition: smt2_conv.cpp:781
smt2_convt::parse_literal
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:321
prop_conv.h
smt2_convt::solvert::YICES
@ YICES
exprt::has_operands
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:93
smt2_convt::convert_relation
void convert_relation(const binary_relation_exprt &)
Definition: smt2_conv.cpp:3039
floatbv_typecast_exprt
Semantic type conversion from/to floating-point formats.
Definition: floatbv_expr.h:19
smt2_convt::identifier_map
identifier_mapt identifier_map
Definition: smt2_conv.h:212
smt2_convt::convert_mod
void convert_mod(const mod_exprt &expr)
Definition: smt2_conv.cpp:2983
smt2_convt::smt2_symbolt::get_identifier
const irep_idt & get_identifier() const
Definition: smt2_conv.h:169
smt2_convt::convert_floatbv_mult
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3606
smt2_convt::use_check_sat_assuming
bool use_check_sat_assuming
Definition: smt2_conv.h:64
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:935
smt2_convt::convert_struct
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2724
smt2_convt::use_lambda_for_array
bool use_lambda_for_array
Definition: smt2_conv.h:66
smt2_convt::out
std::ostream & out
Definition: smt2_conv.h:88
irept::id
const irep_idt & id() const
Definition: irep.h:407
smt2_convt::define_object_size
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:226
smt2_convt::object_sizes
defined_expressionst object_sizes
Definition: smt2_conv.h:230
smt2_convt::bvfp_set
std::set< irep_idt > bvfp_set
Definition: smt2_conv.h:160
floatbv_expr.h
API to expression classes for floating-point arithmetic.
union_typet
The union type.
Definition: c_types.h:112
smt2_convt::convert_div
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3467
smt2_convt::use_array_of_bool
bool use_array_of_bool
Definition: smt2_conv.h:62
smt2_convt::datatype_mapt
std::map< typet, std::string > datatype_mapt
Definition: smt2_conv.h:218
smt2_convt::convert_minus
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3350
tvt
Definition: threeval.h:20
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
minus_exprt
Binary minus.
Definition: std_expr.h:889
smt2_convt::boolbv_width
boolbv_widtht boolbv_width
Definition: smt2_conv.h:93
smt2_convt
Definition: smt2_conv.h:37
smt2_convt::find_symbols_rec
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:4818
smt2_convt::convert_with
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3626
member_exprt
Extract member of struct or union.
Definition: std_expr.h:2527
boolbv_widtht
Definition: boolbv_width.h:18
smt2_convt::use_FPA_theory
bool use_FPA_theory
Definition: smt2_conv.h:61
smt2_convt::write_header
void write_header()
Definition: smt2_conv.cpp:145
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:225
smt2_convt::logic
std::string logic
Definition: smt2_conv.h:89
array_typet
Arrays with given size.
Definition: std_types.h:757
smt2_convt::smt2_symbolt
Definition: smt2_conv.h:163
boolbv_width.h
smt2_convt::defined_expressionst
std::map< exprt, irep_idt > defined_expressionst
Definition: smt2_conv.h:227
smt2_convt::write_footer
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:175
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
smt2_convt::parse_rec
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:564
smt2_convt::dec_solve
resultt dec_solve() override
Run the decision procedure to solve the problem.
Definition: smt2_conv.cpp:264
smt2_convt::floatbv_suffix
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:866
smt2_convt::identifiert::identifiert
identifiert()
Definition: smt2_conv.h:203
irept::set
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:431
smt2_convt::smt2_convt
smt2_convt(const namespacet &_ns, const std::string &_benchmark, const std::string &_notes, const std::string &_logic, solvert _solver, std::ostream &_out)
Definition: smt2_conv.cpp:49
smt2_convt::assumptions
std::vector< exprt > assumptions
Definition: smt2_conv.h:92
smt2_convt::lower_byte_operators
exprt lower_byte_operators(const exprt &expr)
Lower byte_update and byte_extract operations within expr.
Definition: smt2_conv.cpp:4329
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:674
smt2_convt::benchmark
std::string benchmark
Definition: smt2_conv.h:89
smt2_convt::parse_struct
struct_exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:505
smt2_convt::no_boolean_variables
std::size_t no_boolean_variables
Definition: smt2_conv.h:236
literalt
Definition: literal.h:26
smt2_convt::convert_union
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2819
smt2_convt::ns
const namespacet & ns
Definition: smt2_conv.h:87
smt2_convt::solvert::GENERIC
@ GENERIC
smt2_convt::emit_set_logic
bool emit_set_logic
Definition: smt2_conv.h:67
smt2_convt::pointer_logic
pointer_logict pointer_logic
Definition: smt2_conv.h:190
smt2_convt::convert_address_of_rec
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt2_conv.cpp:628
smt2_convt::get
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
Definition: smt2_conv.cpp:271
ieee_float_op_exprt
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: floatbv_expr.h:364
smt2_convt::solvert::Z3
@ Z3
irept
There are a large number of kinds of tree structured or tree-like data in CPROVER.
Definition: irep.h:383
smt2_convt::l_get
tvt l_get(literalt l) const
Definition: smt2_conv.cpp:132
smt2_convt::smt2_identifierst
std::set< std::string > smt2_identifierst
Definition: smt2_conv.h:232
smt2_convt::identifiert
Definition: smt2_conv.h:198
smt2_convt::find_symbols
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4376
letify.h
smt2_convt::solvert
solvert
Definition: smt2_conv.h:40
index_exprt
Array index operator.
Definition: std_expr.h:1242
smt2_convt::boolean_assignment
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:237
smt2_convt::use_as_const
bool use_as_const
Definition: smt2_conv.h:63
smt2_convt::identifiert::type
typet type
Definition: smt2_conv.h:200
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
pointer_typet
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: pointer_expr.h:24
constant_exprt
A constant literal expression.
Definition: std_expr.h:2667
std_expr.h
API to expression classes.
smt2_convt::unflatten
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:4128
smt2_convt::parse_union
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:489
smt2_convt::convert_floatbv_minus
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3447
c_types.h
smt2_convt::flatten2bv
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:4039
smt2_convt::smt2_identifiers
smt2_identifierst smt2_identifiers
Definition: smt2_conv.h:233
smt2_convt::convert_floatbv_typecast
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2578
smt2_convt::identifiert::value
exprt value
Definition: smt2_conv.h:201
smt2_convt::identifiert::is_bound
bool is_bound
Definition: smt2_conv.h:199
mod_exprt
Modulo.
Definition: std_expr.h:1049
smt2_convt::wheret::BEGIN
@ BEGIN
smt2_convt::decision_procedure_text
std::string decision_procedure_text() const override
Return a textual description of the decision procedure.
Definition: smt2_conv.cpp:117
smt2_convt::convert_member
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:3978
smt2_convt::defined_expressions
defined_expressionst defined_expressions
Definition: smt2_conv.h:228