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/make_unique.h>
19 #include <util/unicode.h>
20 #include <util/version.h>
21 
22 #include <solvers/sat/satcheck.h>
25 #include <solvers/smt2/smt2_dec.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 =
148  options.get_unsigned_int_option("string-max-length");
149  info.trace=options.get_bool_option("trace");
150  if(options.get_bool_option("max-node-refinement"))
151  info.max_node_refinement=
152  options.get_unsigned_int_option("max-node-refinement");
153  info.refine_arrays=options.get_bool_option("refine-arrays");
154  info.refine_arithmetic=options.get_bool_option("refine-arithmetic");
155 
156  return util_make_unique<solvert>(
157  util_make_unique<string_refinementt>(info), std::move(prop));
158 }
159 
160 std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_smt2(
162 {
164 
165  const std::string &filename=options.get_option("outfile");
166 
167  if(filename=="")
168  {
170  {
171  error() << "please use --outfile" << eom;
172  throw 0;
173  }
174 
175  auto smt2_dec = util_make_unique<smt2_dect>(
176  ns,
177  "cbmc",
178  std::string("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 = util_make_unique<smt2_convt>(
190  ns,
191  "cbmc",
192  std::string("Generated by CBMC ") + CBMC_VERSION,
193  "QF_AUFBV",
194  solver,
195  std::cout);
196 
197  if(options.get_bool_option("fpa"))
198  smt2_conv->use_FPA_theory=true;
199 
200  smt2_conv->set_message_handler(get_message_handler());
201 
202  return util_make_unique<solvert>(std::move(smt2_conv));
203  }
204  else
205  {
206  #ifdef _MSC_VER
207  auto out=util_make_unique<std::ofstream>(widen(filename));
208  #else
209  auto out=util_make_unique<std::ofstream>(filename);
210  #endif
211 
212  if(!*out)
213  {
214  error() << "failed to open " << filename << eom;
215  throw 0;
216  }
217 
218  auto smt2_conv = util_make_unique<smt2_convt>(
219  ns,
220  "cbmc",
221  std::string("Generated by CBMC ") + CBMC_VERSION,
222  "QF_AUFBV",
223  solver,
224  *out);
225 
226  if(options.get_bool_option("fpa"))
227  smt2_conv->use_FPA_theory=true;
228 
229  smt2_conv->set_message_handler(get_message_handler());
230 
231  return util_make_unique<solvert>(std::move(smt2_conv), std::move(out));
232  }
233 }
234 
236 {
237  if(options.get_bool_option("beautify"))
238  {
239  error() << "sorry, this solver does not support beautification" << eom;
240  throw 0;
241  }
242 }
243 
245 {
246  if(options.get_bool_option("all-properties") ||
247  options.get_option("cover")!="" ||
248  options.get_option("incremental-check")!="")
249  {
250  error() << "sorry, this solver does not support incremental solving" << eom;
251  throw 0;
252  }
253 }
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)
std::wstring widen(const char *s)
Definition: unicode.cpp:46
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:130
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:127
const optionst & options
Definition: cbmc_solvers.h:125
message_handlert & get_message_handler()
Definition: message.h:153
const char * CBMC_VERSION
Definition: version.cpp:1
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.