cprover
bmc.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking for ANSI-C + HDL
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_CBMC_BMC_H
13 #define CPROVER_CBMC_BMC_H
14 
15 #include <list>
16 #include <map>
17 
18 #include <util/invariant.h>
19 #include <util/options.h>
20 #include <util/ui_message.h>
22 
24 
27 
31 
32 #include "symex_bmc.h"
33 
34 class cbmc_solverst;
35 
41 class bmct:public safety_checkert
42 {
43 public:
67  const optionst &_options,
69  message_handlert &_message_handler,
70  prop_convt &_prop_conv,
71  path_storaget &_path_storage,
72  std::function<bool(void)> callback_after_symex)
73  : safety_checkert(ns, _message_handler),
74  options(_options),
77  equation(),
78  path_storage(_path_storage),
79  symex(
80  _message_handler,
82  equation,
83  options,
84  path_storage),
85  prop_conv(_prop_conv),
86  ui(ui_message_handlert::uit::PLAIN),
87  driver_callback_after_symex(callback_after_symex)
88  {
91  !options.get_option("symex-coverage-report").empty();
93  options.get_bool_option("self-loops-to-assumptions");
94  }
95 
96  virtual resultt run(const goto_functionst &goto_functions)
97  {
98  wrapper_goto_modelt model(outer_symbol_table, goto_functions);
99  return run(model);
100  }
102  void setup();
104  virtual ~bmct() { }
105 
106  void set_ui(ui_message_handlert::uit _ui) { ui=_ui; }
107 
108  // the safety_checkert interface
110  const goto_functionst &goto_functions)
111  {
112  return run(goto_functions);
113  }
114 
116  {
118  }
119 
122  {
124  }
125 
126  static int do_language_agnostic_bmc(
127  const path_strategy_choosert &path_strategy_chooser,
128  const optionst &opts,
129  abstract_goto_modelt &goto_model,
131  messaget &message,
132  std::function<void(bmct &, const symbol_tablet &)>
133  driver_configure_bmc = nullptr,
134  std::function<bool(void)> callback_after_symex = nullptr);
135 
136 protected:
145  const optionst &_options,
147  message_handlert &_message_handler,
148  prop_convt &_prop_conv,
149  symex_target_equationt &_equation,
150  path_storaget &_path_storage,
151  std::function<bool(void)> callback_after_symex)
152  : safety_checkert(ns, _message_handler),
153  options(_options),
156  equation(_equation),
157  path_storage(_path_storage),
158  symex(
159  _message_handler,
161  equation,
162  options,
163  path_storage),
164  prop_conv(_prop_conv),
165  ui(ui_message_handlert::uit::PLAIN),
166  driver_callback_after_symex(callback_after_symex)
167  {
170  !options.get_option("symex-coverage-report").empty();
171  INVARIANT(
172  options.get_bool_option("paths"),
173  "Should only use saved equation & goto_state constructor "
174  "when doing path exploration");
175  }
176 
187  std::unique_ptr<memory_model_baset> memory_model;
188  // use gui format
190 
193 
194  virtual resultt decide(
195  const goto_functionst &,
196  prop_convt &);
197 
198  void do_conversion();
199 
200  virtual void freeze_program_variables();
201 
202  virtual void show_vcc();
203  virtual void show_vcc_plain(std::ostream &out);
204  virtual void show_vcc_json(std::ostream &out);
205 
207  {
208  return trace_optionst(options);
209  }
210 
211  virtual resultt all_properties(
212  const goto_functionst &goto_functions,
213  prop_convt &solver);
215  virtual void show_program();
216  virtual void report_success();
217  virtual void report_failure();
218 
219  virtual void error_trace();
221 
222  void get_memory_model();
223  void slice();
224  void show();
225 
226  bool cover(
227  const goto_functionst &goto_functions,
228  const optionst::value_listt &criteria);
229 
230  friend class bmc_all_propertiest;
231  friend class bmc_covert;
232  template <template <class goalt> class covert>
233  friend class bmc_goal_covert;
234  friend class fault_localizationt;
235 
236 private:
243  virtual void perform_symbolic_execution(
244  goto_symext::get_goto_functiont get_goto_function);
245 
250  std::function<bool(void)> driver_callback_after_symex;
251 };
252 
263 class path_explorert : public bmct
264 {
265 public:
267  const optionst &_options,
269  message_handlert &_message_handler,
270  prop_convt &_prop_conv,
271  symex_target_equationt &saved_equation,
274  std::function<bool(void)> callback_after_symex)
275  : bmct(
276  _options,
278  _message_handler,
279  _prop_conv,
280  saved_equation,
281  path_storage,
282  callback_after_symex),
284  {
285  }
286 
287 protected:
289 
290 private:
297  goto_symext::get_goto_functiont get_goto_function) override;
298 
299 #define OPT_BMC \
300  "(program-only)" \
301  "(show-loops)" \
302  "(show-vcc)" \
303  "(slice-formula)" \
304  "(unwinding-assertions)" \
305  "(no-unwinding-assertions)" \
306  "(no-pretty-names)" \
307  "(no-self-loops-to-assumptions)" \
308  "(partial-loops)" \
309  "(paths):" \
310  "(show-symex-strategies)" \
311  "(depth):" \
312  "(unwind):" \
313  "(unwindset):" \
314  "(graphml-witness):" \
315  "(unwindset):"
316 
317 #define HELP_BMC \
318  " --paths [strategy] explore paths one at a time\n" \
319  " --show-symex-strategies list strategies for use with --paths\n" \
320  " --program-only only show program expression\n" \
321  " --show-loops show the loops in the program\n" \
322  " --depth nr limit search depth\n" \
323  " --unwind nr unwind nr times\n" \
324  " --unwindset L:B,... unwind loop L with a bound of B\n" \
325  " (use --show-loops to get the loop IDs)\n" \
326  " --show-vcc show the verification conditions\n" \
327  " --slice-formula remove assignments unrelated to property\n" \
328  " --unwinding-assertions generate unwinding assertions (cannot be\n" \
329  " used with --cover or --partial-loops)\n" \
330  " --partial-loops permit paths with partial loops\n" \
331  " --no-self-loops-to-assumptions\n" \
332  " do not simplify while(1){} to assume(0)\n" \
333  " --no-pretty-names do not simplify identifiers\n" \
334  " --graphml-witness filename write the witness in GraphML format to " \
335  "filename\n" // NOLINT(*)
336 };
337 
338 #endif // CPROVER_CBMC_BMC_H
void do_conversion()
Definition: bmc.cpp:112
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
Definition: bmc.cpp:679
friend class bmc_goal_covert
Definition: bmc.h:233
void set_ui(ui_message_handlert::uit _ui)
Definition: bmc.h:106
Abstract interface to eager or lazy GOTO models.
Generate Equation using Symbolic Execution.
const symbol_tablet & outer_symbol_table
symbol table for the goto-program that we will execute
Definition: bmc.h:179
bmct(const optionst &_options, const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &_equation, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex)
Constructor for path exploration from saved state.
Definition: bmc.h:144
virtual void show_vcc_plain(std::ostream &out)
Definition: show_vcc.cpp:23
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
virtual resultt operator()(const goto_functionst &goto_functions)
Definition: bmc.h:109
bool record_coverage
Definition: symex_bmc.h:82
void show()
Definition: bmc.cpp:503
void slice()
Definition: bmc.cpp:441
virtual void show_vcc()
Definition: show_vcc.cpp:135
path_storaget & path_storage
Definition: bmc.h:184
bool constant_propagation
Definition: goto_symex.h:215
virtual void report_failure()
Definition: bmc.cpp:176
Traces of GOTO Programs.
Decision Procedure Interface.
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
Definition: bmc_cover.cpp:429
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:84
virtual resultt decide(const goto_functionst &, prop_convt &)
Definition: bmc.cpp:491
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, const ui_message_handlert::uit &ui, messaget &message, std::function< void(bmct &, const symbol_tablet &)> driver_configure_bmc=nullptr, std::function< bool(void)> callback_after_symex=nullptr)
Perform core BMC, using an abstract model to supply GOTO function bodies (perhaps created on demand)...
Definition: bmc.cpp:561
namespacet ns
Definition: bmc.h:182
Factory and information for path_storaget.
Definition: path_storage.h:119
symex_bmct symex
Definition: bmc.h:185
void add_loop_unwind_handler(loop_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind loops. ...
Definition: symex_bmc.h:61
const goto_symex_statet & saved_state
Definition: bmc.h:288
virtual ~bmct()
Definition: bmc.h:104
void add_unwind_recursion_handler(symex_bmct::recursion_unwind_handlert handler)
Definition: bmc.h:120
bool self_loops_to_assumptions
Definition: goto_symex.h:216
void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
Definition: bmc.h:115
virtual void error_trace()
Definition: bmc.cpp:47
Symbol Table + CFG.
void add_recursion_unwind_handler(recursion_unwind_handlert handler)
Add a callback function that will be called to determine whether to unwind recursion.
Definition: symex_bmc.h:70
ui_message_handlert::uit ui
Definition: bmc.h:189
int solver(std::istream &in)
void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function) override
Resume symbolic execution from saved branch point.
Definition: bmc.cpp:689
prop_convt & prop_conv
Definition: bmc.h:186
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
void setup()
Definition: bmc.cpp:305
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
std::list< std::string > value_listt
Definition: options.h:22
Symbolic execution from a saved branch point.
Definition: bmc.h:263
virtual void show_vcc_json(std::ostream &out)
Definition: show_vcc.cpp:79
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Definition: bmc.cpp:124
const optionst & options
Definition: bmc.h:177
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
Safety Checker Interface.
mstreamt & result() const
Definition: message.h:312
Memory models for partial order concurrency.
void get_memory_model()
Definition: bmc.cpp:287
safety_checkert::resultt execute(abstract_goto_modelt &)
Definition: bmc.cpp:323
virtual resultt run(const goto_functionst &goto_functions)
Definition: bmc.h:96
std::function< tvt(const irep_idt &, unsigned, unsigned, unsigned &)> loop_unwind_handlert
Loop unwind handlers take the function ID and loop number, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.
Definition: symex_bmc.h:46
virtual void show_program()
Definition: bmc.cpp:203
virtual resultt stop_on_fail(prop_convt &solver)
Definition: bmc.cpp:516
Bounded Model Checking for ANSI-C.
Class providing the abstract GOTO model interface onto an unrelated symbol table and goto_functionst...
Definition: goto_model.h:102
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
Definition: bmc.h:181
bmct(const optionst &_options, const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, path_storaget &_path_storage, std::function< bool(void)> callback_after_symex)
Constructor for path exploration with freshly-initialized state.
Definition: bmc.h:66
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
std::unique_ptr< memory_model_baset > memory_model
Definition: bmc.h:187
symex_target_equationt equation
Definition: bmc.h:183
Options.
std::function< bool(void)> driver_callback_after_symex
Optional callback, to be run after symex but before handing the resulting equation to the solver...
Definition: bmc.h:250
virtual void report_success()
Definition: bmc.cpp:149
trace_optionst trace_options()
Definition: bmc.h:206
virtual void freeze_program_variables()
Hook used by CEGIS to selectively freeze variables in the SAT solver after the SSA formula is added t...
Definition: bmc.cpp:42
std::function< tvt(const irep_idt &, unsigned, unsigned &)> recursion_unwind_handlert
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specify...
Definition: symex_bmc.h:55
Storage of symbolic execution paths to resume.
void output_graphml(resultt result)
outputs witnesses in graphml format
Definition: bmc.cpp:89
path_explorert(const optionst &_options, const symbol_tablet &outer_symbol_table, message_handlert &_message_handler, prop_convt &_prop_conv, symex_target_equationt &saved_equation, const goto_symex_statet &saved_state, path_storaget &path_storage, std::function< bool(void)> callback_after_symex)
Definition: bmc.h:266