cprover
cbmc_solvers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Solvers for VCs Generated by Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "cbmc_solvers.h"
13 
14 #include <fstream>
15 #include <iostream>
16 #include <memory>
17 
18 #include <util/unicode.h>
19 #include <util/make_unique.h>
20 
21 #include <solvers/sat/satcheck.h>
24 #include <solvers/smt2/smt2_dec.h>
25 #include <solvers/prop/aig_prop.h>
26 #include <solvers/sat/dimacs_cnf.h>
27 
28 #include "bv_cbmc.h"
29 #include "cbmc_dimacs.h"
31 
35 {
36  assert(options.get_bool_option("smt2"));
37 
39 
40  if(options.get_bool_option("boolector"))
42  else if(options.get_bool_option("mathsat"))
44  else if(options.get_bool_option("cvc3"))
46  else if(options.get_bool_option("cvc4"))
48  else if(options.get_bool_option("yices"))
50  else if(options.get_bool_option("z3"))
52  else if(options.get_bool_option("generic"))
54 
55  return s;
56 }
57 
58 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
59 {
60  auto solver=util_make_unique<solvert>();
61 
62  if(options.get_bool_option("beautify") ||
63  !options.get_bool_option("sat-preprocessor")) // no simplifier
64  {
65  // simplifier won't work with beautification
66  solver->set_prop(util_make_unique<satcheck_no_simplifiert>());
67  }
68  else // with simplifier
69  {
70  solver->set_prop(util_make_unique<satcheckt>());
71  }
72 
73  solver->prop().set_message_handler(get_message_handler());
74 
75  auto bv_cbmc=util_make_unique<bv_cbmct>(ns, solver->prop());
76 
77  if(options.get_option("arrays-uf")=="never")
78  bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_NONE;
79  else if(options.get_option("arrays-uf")=="always")
80  bv_cbmc->unbounded_array=bv_cbmct::unbounded_arrayt::U_ALL;
81 
82  solver->set_prop_conv(std::move(bv_cbmc));
83 
84  return solver;
85 }
86 
87 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
88 {
91 
92  auto prop=util_make_unique<dimacs_cnft>();
93  prop->set_message_handler(get_message_handler());
94 
95  std::string filename=options.get_option("outfile");
96 
97  auto cbmc_dimacs=util_make_unique<cbmc_dimacst>(ns, *prop, filename);
98  return util_make_unique<solvert>(std::move(cbmc_dimacs), std::move(prop));
99 }
100 
101 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
102 {
103  std::unique_ptr<propt> prop=[this]() -> std::unique_ptr<propt>
104  {
105  // We offer the option to disable the SAT preprocessor
106  if(options.get_bool_option("sat-preprocessor"))
107  {
109  return util_make_unique<satcheckt>();
110  }
111  return util_make_unique<satcheck_no_simplifiert>();
112  }();
113 
115 
117  info.ns=&ns;
118  info.prop=prop.get();
119  info.ui=ui;
120 
121  // we allow setting some parameters
122  if(options.get_bool_option("max-node-refinement"))
123  info.max_node_refinement=
124  options.get_unsigned_int_option("max-node-refinement");
125 
126  info.refine_arrays=options.get_bool_option("refine-arrays");
127  info.refine_arithmetic=options.get_bool_option("refine-arithmetic");
128 
129  return util_make_unique<solvert>(
130  util_make_unique<bv_refinementt>(info),
131  std::move(prop));
132 }
133 
137 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
138 {
140  info.ns=&ns;
141  auto prop=util_make_unique<satcheck_no_simplifiert>();
142  prop->set_message_handler(get_message_handler());
143  info.prop=prop.get();
145  info.ui=ui;
146  if(options.get_bool_option("string-max-length"))
147  info.max_string_length = options.get_signed_int_option("string-max-length");
148  info.trace=options.get_bool_option("trace");
149  if(options.get_bool_option("max-node-refinement"))
150  info.max_node_refinement=
151  options.get_unsigned_int_option("max-node-refinement");
152  info.refine_arrays=options.get_bool_option("refine-arrays");
153  info.refine_arithmetic=options.get_bool_option("refine-arithmetic");
154 
155  return util_make_unique<solvert>(
156  util_make_unique<string_refinementt>(info), std::move(prop));
157 }
158 
159 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
161 {
163 
164  const std::string &filename=options.get_option("outfile");
165 
166  if(filename=="")
167  {
169  {
170  error() << "please use --outfile" << eom;
171  throw 0;
172  }
173 
174  auto smt2_dec=
175  util_make_unique<smt2_dect>(
176  ns,
177  "cbmc",
178  "Generated by CBMC " CBMC_VERSION,
179  "QF_AUFBV",
180  solver);
181 
182  if(options.get_bool_option("fpa"))
183  smt2_dec->use_FPA_theory=true;
184 
185  return util_make_unique<solvert>(std::move(smt2_dec));
186  }
187  else if(filename=="-")
188  {
189  auto smt2_conv=
190  util_make_unique<smt2_convt>(
191  ns,
192  "cbmc",
193  "Generated by CBMC " CBMC_VERSION,
194  "QF_AUFBV",
195  solver,
196  std::cout);
197 
198  if(options.get_bool_option("fpa"))
199  smt2_conv->use_FPA_theory=true;
200 
201  smt2_conv->set_message_handler(get_message_handler());
202 
203  return util_make_unique<solvert>(std::move(smt2_conv));
204  }
205  else
206  {
207  #ifdef _MSC_VER
208  auto out=util_make_unique<std::ofstream>(widen(filename));
209  #else
210  auto out=util_make_unique<std::ofstream>(filename);
211  #endif
212 
213  if(!*out)
214  {
215  error() << "failed to open " << filename << eom;
216  throw 0;
217  }
218 
219  auto smt2_conv=
220  util_make_unique<smt2_convt>(
221  ns,
222  "cbmc",
223  "Generated by CBMC " CBMC_VERSION,
224  "QF_AUFBV",
225  solver,
226  *out);
227 
228  if(options.get_bool_option("fpa"))
229  smt2_conv->use_FPA_theory=true;
230 
231  smt2_conv->set_message_handler(get_message_handler());
232 
233  return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
234  }
235 }
236 
238 {
239  if(options.get_bool_option("beautify"))
240  {
241  error() << "sorry, this solver does not support beautification" << eom;
242  throw 0;
243  }
244 }
245 
247 {
248  if(options.get_bool_option("all-properties") ||
249  options.get_option("cover")!="" ||
250  options.get_option("incremental-check")!="")
251  {
252  error() << "sorry, this solver does not support incremental solving" << eom;
253  throw 0;
254  }
255 }
bool trace
Concretize strings after solver is finished.
const namespacet * ns
Definition: bv_refinement.h:37
std::unique_ptr< solvert > get_smt2(smt2_dect::solvert solver)
signed int get_signed_int_option(const std::string &option) const
Definition: options.cpp:48
std::wstring widen(const char *s)
Definition: unicode.cpp:56
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:54
Writing DIMACS Files.
#define DEFAULT_MAX_NB_REFINEMENT
string_refinementt constructor arguments
ui_message_handlert::uit ui
Definition: cbmc_solvers.h:131
smt2_dect::solvert get_smt2_solver_type() const
Uses the options to pick an SMT 2.0 solver.
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
bool refine_arrays
Enable array refinement.
Definition: bv_refinement.h:30
int solver(std::istream &in)
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
mstreamt & error() const
Definition: message.h:302
unsigned max_node_refinement
Max number of times we refine a formula node.
Definition: bv_refinement.h:28
std::unique_ptr< solvert > get_string_refinement()
the string refinement adds to the bit vector refinement specifications for functions from the Java st...
void no_incremental_check()
ui_message_handlert::uit ui
Definition: bv_refinement.h:26
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:148
String support via creating string constraints and progressively instantiating the universal constrai...
namespacet ns
Definition: cbmc_solvers.h:128
const optionst & options
Definition: cbmc_solvers.h:126
message_handlert & get_message_handler()
Definition: message.h:153
std::unique_ptr< solvert > get_default()
std::unique_ptr< solvert > get_dimacs()
std::unique_ptr< solvert > get_bv_refinement()
void no_beautification()
bool refine_arithmetic
Enable arithmetic refinement.
Definition: bv_refinement.h:32
Bounded Model Checking for ANSI-C + HDL.
Abstraction Refinement Loop.
Counterexample Beautification.