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/std_expr.h>
17 #include <util/byte_operators.h>
18 
19 #ifndef HASH_CODE
21 #endif
22 
23 #include <solvers/prop/prop_conv.h>
26 
27 class typecast_exprt;
28 class constant_exprt;
29 class index_exprt;
30 class member_exprt;
31 
32 class smt2_convt:public prop_convt
33 {
34 public:
35  enum class solvert
36  {
37  GENERIC,
38  BOOLECTOR,
40  CVC3,
41  CVC4,
42  MATHSAT,
43  YICES,
44  Z3
45  };
46 
48  const namespacet &_ns,
49  const std::string &_benchmark,
50  const std::string &_notes,
51  const std::string &_logic,
52  solvert _solver,
53  std::ostream &_out):
54  prop_convt(_ns),
55  use_FPA_theory(false),
56  use_datatypes(false),
57  use_array_of_bool(false),
58  emit_set_logic(true),
59  out(_out),
60  benchmark(_benchmark),
61  notes(_notes),
62  logic(_logic),
63  solver(_solver),
64  boolbv_width(_ns),
65  let_id_count(0),
66  pointer_logic(_ns),
68  {
69  // We set some defaults differently
70  // for some solvers.
71 
72  switch(solver)
73  {
74  case solvert::GENERIC:
75  break;
76 
77  case solvert::BOOLECTOR:
78  break;
79 
81  use_array_of_bool = true;
82  emit_set_logic = false;
83  break;
84 
85  case solvert::CVC3:
86  break;
87 
88  case solvert::CVC4:
89  break;
90 
91  case solvert::MATHSAT:
92  break;
93 
94  case solvert::YICES:
95  break;
96 
97  case solvert::Z3:
98  use_array_of_bool=true;
99  emit_set_logic=false;
100  use_datatypes=true;
101  break;
102  }
103 
104  write_header();
105  }
106 
107  virtual ~smt2_convt() { }
108  virtual resultt dec_solve();
109 
114 
115  // overloading interfaces
116  virtual literalt convert(const exprt &expr);
117  virtual void set_frozen(literalt) { /* not needed */ }
118  virtual void set_to(const exprt &expr, bool value);
119  virtual exprt get(const exprt &expr) const;
120  virtual std::string decision_procedure_text() const { return "SMT2"; }
121  virtual void print_assignment(std::ostream &out) const;
122  virtual tvt l_get(literalt l) const;
123  virtual void set_assumptions(const bvt &bv) { assumptions=bv; }
124 
125  // new stuff
126  void convert_expr(const exprt &);
127  void convert_type(const typet &);
128  void convert_literal(const literalt);
129 
130 protected:
131  std::ostream &out;
132  std::string benchmark, notes, logic;
134 
137 
138  void write_header();
139  void write_footer(std::ostream &);
140 
141  // tweaks for arrays
142  bool use_array_theory(const exprt &);
143  void flatten_array(const exprt &);
144  void unflatten_array(const exprt &);
145 
146  // specific expressions go here
147  void convert_byte_update(const byte_update_exprt &expr);
148  void convert_byte_extract(const byte_extract_exprt &expr);
149  void convert_typecast(const typecast_exprt &expr);
151  void convert_struct(const struct_exprt &expr);
152  void convert_union(const union_exprt &expr);
153  void convert_constant(const constant_exprt &expr);
154  void convert_relation(const exprt &expr);
155  void convert_is_dynamic_object(const exprt &expr);
156  void convert_plus(const plus_exprt &expr);
157  void convert_minus(const minus_exprt &expr);
158  void convert_div(const div_exprt &expr);
159  void convert_mult(const mult_exprt &expr);
160  void convert_rounding_mode_FPA(const exprt &expr);
161  void convert_floatbv_plus(const ieee_float_op_exprt &expr);
162  void convert_floatbv_minus(const ieee_float_op_exprt &expr);
163  void convert_floatbv_div(const ieee_float_op_exprt &expr);
164  void convert_floatbv_mult(const ieee_float_op_exprt &expr);
165  void convert_mod(const mod_exprt &expr);
166  void convert_index(const index_exprt &expr);
167  void convert_member(const member_exprt &expr);
168  void convert_overflow(const exprt &expr);
169  void convert_with(const with_exprt &expr);
170  void convert_update(const exprt &expr);
171 
172  std::string convert_identifier(const irep_idt &identifier);
173 
174  // introduces a let-expression for operands
175  exprt convert_operands(const exprt &);
176 
177  // auxiliary methods
178  void find_symbols(const exprt &expr);
179  void find_symbols(const typet &type);
180  void find_symbols_rec(const typet &type, std::set<irep_idt> &recstack);
181 
182  // letification
184  {
185  let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
186  : count(_count), let_symbol(_let_symbol)
187  {
188  }
189 
190  std::size_t count;
192  };
193 
194 #ifdef HASH_CODE
195  typedef std::unordered_map<exprt, let_count_idt, irep_hash> seen_expressionst;
196 #else
198 #endif
199 
200  std::size_t let_id_count;
201  static const std::size_t LET_COUNT = 2;
202 
204  {
206 
207  public:
208  explicit let_visitort(const seen_expressionst &map):let_map(map) { }
209 
210  void operator()(exprt &expr)
211  {
213  if(it != let_map.end() && it->second.count >= LET_COUNT)
214  {
215  const symbol_exprt &symb = it->second.let_symbol;
216  expr=symb;
217  }
218  }
219  };
220 
221  exprt letify(exprt &expr);
223  exprt &expr,
224  std::vector<exprt> &let_order,
225  const seen_expressionst &map,
226  std::size_t i);
227 
228  void collect_bindings(
229  exprt &expr,
230  seen_expressionst &map,
231  std::vector<exprt> &let_order);
232 
234  exprt &expr,
235  const seen_expressionst &map);
236 
237  // Parsing solver responses
238  constant_exprt parse_literal(const irept &, const typet &type);
239  exprt parse_struct(const irept &s, const struct_typet &type);
240  exprt parse_union(const irept &s, const union_typet &type);
241  exprt parse_array(const irept &s, const array_typet &type);
242  exprt parse_rec(const irept &s, const typet &type);
243 
244  // we use this to build a bit-vector encoding of the FPA theory
245  void convert_floatbv(const exprt &expr);
246  std::string type2id(const typet &) const;
247  std::string floatbv_suffix(const exprt &) const;
248  std::set<irep_idt> bvfp_set; // already converted
249 
251  {
252  public:
253  smt2_symbolt(const irep_idt &_identifier, const typet &_type)
254  : nullary_exprt(ID_smt2_symbol, _type)
255  { set(ID_identifier, _identifier); }
256 
257  const irep_idt &get_identifier() const
258  {
259  return get(ID_identifier);
260  }
261  };
262 
263  const smt2_symbolt &to_smt2_symbol(const exprt &expr)
264  {
265  assert(expr.id()==ID_smt2_symbol && !expr.has_operands());
266  return static_cast<const smt2_symbolt&>(expr);
267  }
268 
269  // flattens any non-bitvector type into a bitvector,
270  // e.g., booleans, vectors, structs, arrays but also
271  // floats when using the FPA theory.
272  // unflatten() does the opposite.
273  enum class wheret { BEGIN, END };
274  void flatten2bv(const exprt &);
275  void unflatten(wheret, const typet &, unsigned nesting=0);
276 
277  // pointers
280  const exprt &expr, const pointer_typet &result_type);
281 
282  void define_object_size(const irep_idt &id, const exprt &expr);
283 
284  // keeps track of all non-Boolean symbols and their value
285  struct identifiert
286  {
289 
291  {
292  type.make_nil();
293  value.make_nil();
294  }
295  };
296 
297  typedef std::unordered_map<irep_idt, identifiert> identifier_mapt;
298 
300 
301  // for modeling structs as Z3 datatype, enabled when
302  // use_datatype is set
303  typedef std::map<typet, std::string> datatype_mapt;
305 
306  // for replacing various defined expressions:
307  //
308  // ID_array_of
309  // ID_array
310  // ID_string_constant
311 
312  typedef std::map<exprt, irep_idt> defined_expressionst;
314 
316 
317  typedef std::set<std::string> smt2_identifierst;
319 
320  // Boolean part
321  std::size_t no_boolean_variables;
322  std::vector<bool> boolean_assignment;
323 };
324 
325 #endif // CPROVER_SOLVERS_SMT2_SMT2_CONV_H
void unflatten(wheret, const typet &, unsigned nesting=0)
Definition: smt2_conv.cpp:3973
The type of an expression, extends irept.
Definition: type.h:27
smt2_symbolt(const irep_idt &_identifier, const typet &_type)
Definition: smt2_conv.h:253
exprt parse_union(const irept &s, const union_typet &type)
Definition: smt2_conv.cpp:370
exprt convert_operands(const exprt &)
IREP Hash Container.
datatype_mapt datatype_map
Definition: smt2_conv.h:304
virtual tvt l_get(literalt l) const
Definition: smt2_conv.cpp:53
Semantic type conversion.
Definition: std_expr.h:2277
void flatten2bv(const exprt &)
Definition: smt2_conv.cpp:3884
An expression without operands.
Definition: std_expr.h:23
void convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
Definition: smt2_conv.cpp:2425
exprt parse_array(const irept &s, const array_typet &type)
Definition: smt2_conv.cpp:340
exprt letify(exprt &expr)
Definition: smt2_conv.cpp:4735
let_count_idt(std::size_t _count, const symbol_exprt &_let_symbol)
Definition: smt2_conv.h:185
virtual resultt dec_solve()
Definition: smt2_conv.cpp:171
void convert_literal(const literalt)
Definition: smt2_conv.cpp:737
void convert_typecast(const typecast_exprt &expr)
Definition: smt2_conv.cpp:1915
void convert_floatbv_plus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3156
void convert_expr(const exprt &)
Definition: smt2_conv.cpp:862
void convert_constant(const constant_exprt &expr)
Definition: smt2_conv.cpp:2700
bool use_datatypes
Definition: smt2_conv.h:111
void convert_update(const exprt &expr)
Definition: smt2_conv.cpp:3718
const_iterator find(const Key &key) const
const smt2_symbolt & to_smt2_symbol(const exprt &expr)
Definition: smt2_conv.h:263
void convert_floatbv(const exprt &expr)
Definition: smt2_conv.cpp:828
std::unordered_map< irep_idt, identifiert > identifier_mapt
Definition: smt2_conv.h:297
void convert_plus(const plus_exprt &expr)
Definition: smt2_conv.cpp:2977
std::string type2id(const typet &) const
Definition: smt2_conv.cpp:788
A constant literal expression.
Definition: std_expr.h:4384
std::string notes
Definition: smt2_conv.h:132
Structure type, corresponds to C style structs.
Definition: std_types.h:276
void flatten_array(const exprt &)
produce a flat bit-vector for a given array of fixed size
Definition: smt2_conv.cpp:2635
virtual void set_assumptions(const bvt &bv)
Definition: smt2_conv.h:123
identifier_mapt identifier_map
Definition: smt2_conv.h:299
void convert_type(const typet &)
Definition: smt2_conv.cpp:4389
std::size_t let_id_count
Definition: smt2_conv.h:200
bool use_array_theory(const exprt &)
Definition: smt2_conv.cpp:4367
Extract member of struct or union.
Definition: std_expr.h:3890
void convert_floatbv_mult(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3451
exprt substitute_let(exprt &expr, const seen_expressionst &map)
Definition: smt2_conv.cpp:4799
virtual literalt convert(const exprt &expr)
Definition: smt2_conv.cpp:705
void convert_mult(const mult_exprt &expr)
Definition: smt2_conv.cpp:3376
void convert_relation(const exprt &expr)
Definition: smt2_conv.cpp:2892
const irep_idt & id() const
Definition: irep.h:259
void define_object_size(const irep_idt &id, const exprt &expr)
Definition: smt2_conv.cpp:133
Expression classes for byte-level operators.
virtual void print_assignment(std::ostream &out) const
Definition: smt2_conv.cpp:43
defined_expressionst object_sizes
Definition: smt2_conv.h:315
Division.
Definition: std_expr.h:1211
void convert_mod(const mod_exprt &expr)
Definition: smt2_conv.cpp:2832
virtual std::string decision_procedure_text() const
Definition: smt2_conv.h:120
void operator()(exprt &expr)
Definition: smt2_conv.h:210
void convert_floatbv_div(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3356
void convert_struct(const struct_exprt &expr)
Definition: smt2_conv.cpp:2571
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
Definition: std_types.h:1507
symbol_exprt let_symbol
Definition: smt2_conv.h:191
void convert_rounding_mode_FPA(const exprt &expr)
Converting a constant or symbolic rounding mode to SMT-LIB.
Definition: smt2_conv.cpp:3099
void convert_div(const div_exprt &expr)
Definition: smt2_conv.cpp:3312
Union constructor from single element.
Definition: std_expr.h:1840
API to expression classes.
void convert_index(const index_exprt &expr)
Definition: smt2_conv.cpp:3725
Definition: threeval.h:19
boolbv_widtht boolbv_width
Definition: smt2_conv.h:136
exprt letify_rec(exprt &expr, std::vector< exprt > &let_order, const seen_expressionst &map, std::size_t i)
Definition: smt2_conv.cpp:4745
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
virtual void set_frozen(literalt)
Definition: smt2_conv.h:117
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void find_symbols_rec(const typet &type, std::set< irep_idt > &recstack)
Definition: smt2_conv.cpp:4538
Base class for tree-like data structures with sharing.
Definition: irep.h:156
std::string convert_identifier(const irep_idt &identifier)
Definition: smt2_conv.cpp:757
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
constant_exprt parse_literal(const irept &, const typet &type)
Definition: smt2_conv.cpp:210
void write_header()
Definition: smt2_conv.cpp:66
void convert_minus(const minus_exprt &expr)
Definition: smt2_conv.cpp:3195
const_iterator end() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
std::string floatbv_suffix(const exprt &) const
Definition: smt2_conv.cpp:822
const irep_idt & get_identifier() const
Definition: smt2_conv.h:257
bool has_operands() const
Return true if there is at least one operand.
Definition: expr.h:75
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.h:47
virtual ~smt2_convt()
Definition: smt2_conv.h:107
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
std::map< typet, std::string > datatype_mapt
Definition: smt2_conv.h:303
bool use_array_of_bool
Definition: smt2_conv.h:112
typename mapt::const_iterator const_iterator
virtual exprt get(const exprt &expr) const
Definition: smt2_conv.cpp:178
void convert_byte_update(const byte_update_exprt &expr)
Definition: smt2_conv.cpp:605
std::ostream & out
Definition: smt2_conv.h:131
std::string benchmark
Definition: smt2_conv.h:132
void convert_is_dynamic_object(const exprt &expr)
Definition: smt2_conv.cpp:2851
void unflatten_array(const exprt &)
Semantic type conversion from/to floating-point formats.
Definition: std_expr.h:2336
const seen_expressionst & let_map
Definition: smt2_conv.h:205
Base class for all expressions.
Definition: expr.h:54
std::set< irep_idt > bvfp_set
Definition: smt2_conv.h:248
The union type.
Definition: std_types.h:425
let_visitort(const seen_expressionst &map)
Definition: smt2_conv.h:208
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
void convert_overflow(const exprt &expr)
Definition: smt2_conv.cpp:4080
void find_symbols(const exprt &expr)
Definition: smt2_conv.cpp:4171
std::size_t no_boolean_variables
Definition: smt2_conv.h:321
void convert_member(const member_exprt &expr)
Definition: smt2_conv.cpp:3823
exprt parse_rec(const irept &s, const typet &type)
Definition: smt2_conv.cpp:449
void make_nil()
Definition: irep.h:315
Arrays with given size.
Definition: std_types.h:1000
void convert_union(const union_exprt &expr)
Definition: smt2_conv.cpp:2665
virtual void set_to(const exprt &expr, bool value)
Definition: smt2_conv.cpp:4085
static const std::size_t LET_COUNT
Definition: smt2_conv.h:201
Binary minus.
Definition: std_expr.h:1106
TO_BE_DOCUMENTED.
void convert_with(const with_exprt &expr)
Definition: smt2_conv.cpp:3471
Expression to hold a symbol (variable)
Definition: std_expr.h:143
std::vector< bool > boolean_assignment
Definition: smt2_conv.h:322
solvert solver
Definition: smt2_conv.h:133
std::string logic
Definition: smt2_conv.h:132
void convert_address_of_rec(const exprt &expr, const pointer_typet &result_type)
Definition: smt2_conv.cpp:501
void convert_byte_extract(const byte_extract_exprt &expr)
Definition: smt2_conv.cpp:596
std::map< exprt, irep_idt > defined_expressionst
Definition: smt2_conv.h:312
Pointer Logic.
exprt parse_struct(const irept &s, const struct_typet &type)
Definition: smt2_conv.cpp:385
bool use_FPA_theory
Definition: smt2_conv.h:110
void write_footer(std::ostream &)
Definition: smt2_conv.cpp:96
TO_BE_DOCUMENTED.
Struct constructor from list of elements.
Definition: std_expr.h:1920
std::set< std::string > smt2_identifierst
Definition: smt2_conv.h:317
bool emit_set_logic
Definition: smt2_conv.h:113
bvt assumptions
Definition: smt2_conv.h:135
IEEE floating-point operations These have two data operands (op0 and op1) and one rounding mode (op2)...
Definition: std_expr.h:4282
smt2_identifierst smt2_identifiers
Definition: smt2_conv.h:318
std::vector< literalt > bvt
Definition: literal.h:200
defined_expressionst defined_expressions
Definition: smt2_conv.h:313
Modulo.
Definition: std_expr.h:1287
void set(const irep_namet &name, const irep_idt &value)
Definition: irep.h:286
pointer_logict pointer_logic
Definition: smt2_conv.h:278
void convert_floatbv_minus(const ieee_float_op_exprt &expr)
Definition: smt2_conv.cpp:3292
void collect_bindings(exprt &expr, seen_expressionst &map, std::vector< exprt > &let_order)
Definition: smt2_conv.cpp:4767
irep_hash_mapt< exprt, let_count_idt > seen_expressionst
Definition: smt2_conv.h:197
Array index operator.
Definition: std_expr.h:1595