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  ui_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_message_handler(_message_handler),
87  driver_callback_after_symex(callback_after_symex)
88  {
89  }
90 
91  virtual resultt run(const goto_functionst &goto_functions)
92  {
93  wrapper_goto_modelt model(outer_symbol_table, goto_functions);
94  return run(model);
95  }
97  void setup();
99  virtual ~bmct() { }
100 
101  // the safety_checkert interface
103  const goto_functionst &goto_functions)
104  {
105  return run(goto_functions);
106  }
107 
109  {
111  }
112 
115  {
117  }
118 
119  static int do_language_agnostic_bmc(
120  const path_strategy_choosert &path_strategy_chooser,
121  const optionst &opts,
122  abstract_goto_modelt &goto_model,
124  std::function<void(bmct &, const symbol_tablet &)> driver_configure_bmc =
125  nullptr,
126  std::function<bool(void)> callback_after_symex = nullptr);
127 
128 protected:
137  const optionst &_options,
139  ui_message_handlert &_message_handler,
140  prop_convt &_prop_conv,
141  symex_target_equationt &_equation,
142  path_storaget &_path_storage,
143  std::function<bool(void)> callback_after_symex)
144  : safety_checkert(ns, _message_handler),
145  options(_options),
148  equation(_equation),
149  path_storage(_path_storage),
150  symex(
151  _message_handler,
153  equation,
154  options,
155  path_storage),
156  prop_conv(_prop_conv),
157  ui_message_handler(_message_handler),
158  driver_callback_after_symex(callback_after_symex)
159  {
160  INVARIANT(
161  options.get_bool_option("paths"),
162  "Should only use saved equation & goto_state constructor "
163  "when doing path exploration");
164  }
165 
176  std::unique_ptr<memory_model_baset> memory_model;
177  // use gui format
179 
182 
183  virtual resultt decide(
184  const goto_functionst &,
185  prop_convt &);
186 
187  void do_conversion();
188 
189  virtual void freeze_program_variables();
190 
192  {
193  return trace_optionst(options);
194  }
195 
196  virtual resultt all_properties(
197  const goto_functionst &goto_functions,
198  prop_convt &solver);
200  virtual void report_success();
201  virtual void report_failure();
202 
203  static void report_success(messaget &, ui_message_handlert &);
204  static void report_failure(messaget &, ui_message_handlert &);
205 
206  virtual void error_trace();
208 
209  void get_memory_model();
210  void slice();
211  void show();
212 
213  bool cover(const goto_functionst &goto_functions);
214 
215  friend class bmc_all_propertiest;
216  friend class bmc_covert;
217  template <template <class goalt> class covert>
218  friend class bmc_goal_covert;
219  friend class fault_localizationt;
220 
221 private:
228  virtual void perform_symbolic_execution(
229  goto_symext::get_goto_functiont get_goto_function);
230 
235  std::function<bool(void)> driver_callback_after_symex;
236 };
237 
248 class path_explorert : public bmct
249 {
250 public:
252  const optionst &_options,
254  ui_message_handlert &_message_handler,
255  prop_convt &_prop_conv,
256  symex_target_equationt &saved_equation,
259  std::function<bool(void)> callback_after_symex)
260  : bmct(
261  _options,
263  _message_handler,
264  _prop_conv,
265  saved_equation,
266  path_storage,
267  callback_after_symex),
269  {
270  }
271 
272 protected:
274 
275 private:
282  goto_symext::get_goto_functiont get_goto_function) override;
283 };
284 
285 #define OPT_BMC \
286  "(program-only)" \
287  "(show-loops)" \
288  "(show-vcc)" \
289  "(slice-formula)" \
290  "(unwinding-assertions)" \
291  "(no-unwinding-assertions)" \
292  "(no-pretty-names)" \
293  "(no-self-loops-to-assumptions)" \
294  "(partial-loops)" \
295  "(paths):" \
296  "(show-symex-strategies)" \
297  "(depth):" \
298  "(unwind):" \
299  "(unwindset):" \
300  "(graphml-witness):" \
301  "(unwindset):"
302 
303 #define HELP_BMC \
304  " --paths [strategy] explore paths one at a time\n" \
305  " --show-symex-strategies list strategies for use with --paths\n" \
306  " --program-only only show program expression\n" \
307  " --show-loops show the loops in the program\n" \
308  " --depth nr limit search depth\n" \
309  " --unwind nr unwind nr times\n" \
310  " --unwindset L:B,... unwind loop L with a bound of B\n" \
311  " (use --show-loops to get the loop IDs)\n" \
312  " --show-vcc show the verification conditions\n" \
313  " --slice-formula remove assignments unrelated to property\n" \
314  " --unwinding-assertions generate unwinding assertions (cannot be\n" \
315  " used with --cover or --partial-loops)\n" \
316  " --partial-loops permit paths with partial loops\n" \
317  " --no-self-loops-to-assumptions\n" \
318  " do not simplify while(1){} to assume(0)\n" \
319  " --no-pretty-names do not simplify identifiers\n" \
320  " --graphml-witness filename write the witness in GraphML format to " \
321  "filename\n" // NOLINT(*)
322 
323 #endif // CPROVER_CBMC_BMC_H
void do_conversion()
Definition: bmc.cpp:118
virtual void perform_symbolic_execution(goto_symext::get_goto_functiont get_goto_function)
Class-specific symbolic execution.
Definition: bmc.cpp:639
friend class bmc_goal_covert
Definition: bmc.h:218
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
Definition: bmc_cover.cpp:425
Abstract interface to eager or lazy GOTO models.
ui_message_handlert & ui_message_handler
Definition: bmc.h:178
Generate Equation using Symbolic Execution.
const symbol_tablet & outer_symbol_table
symbol table for the goto-program that we will execute
Definition: bmc.h:168
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
virtual resultt operator()(const goto_functionst &goto_functions)
Definition: bmc.h:102
void show()
Definition: bmc.cpp:443
void slice()
Definition: bmc.cpp:378
path_storaget & path_storage
Definition: bmc.h:173
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void report_failure()
Definition: bmc.cpp:187
Traces of GOTO Programs.
Decision Procedure Interface.
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
Definition: goto_symex.h:109
virtual resultt decide(const goto_functionst &, prop_convt &)
Definition: bmc.cpp:431
namespacet ns
Definition: bmc.h:171
Factory and information for path_storaget.
Definition: path_storage.h:129
symex_bmct symex
Definition: bmc.h:174
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:62
const goto_symex_statet & saved_state
Definition: bmc.h:273
virtual ~bmct()
Definition: bmc.h:99
void add_unwind_recursion_handler(symex_bmct::recursion_unwind_handlert handler)
Definition: bmc.h:113
void add_loop_unwind_handler(symex_bmct::loop_unwind_handlert handler)
Definition: bmc.h:108
virtual void error_trace()
Definition: bmc.cpp:51
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:71
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:655
prop_convt & prop_conv
Definition: bmc.h:175
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
void setup()
Definition: bmc.cpp:236
The symbol table.
Definition: symbol_table.h:19
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
Symbolic execution from a saved branch point.
Definition: bmc.h:248
bmct(const optionst &_options, const symbol_tablet &outer_symbol_table, ui_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
A collection of goto functions.
Class that provides messages with a built-in verbosity &#39;level&#39;.
Definition: message.h:144
std::function< tvt(const goto_symex_statet::call_stackt &, unsigned, unsigned, unsigned &)> loop_unwind_handlert
Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter ...
Definition: symex_bmc.h:47
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Definition: bmc.cpp:130
const optionst & options
Definition: bmc.h:166
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:24
path_explorert(const optionst &_options, const symbol_tablet &outer_symbol_table, ui_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:251
Safety Checker Interface.
static int do_language_agnostic_bmc(const path_strategy_choosert &path_strategy_chooser, const optionst &opts, abstract_goto_modelt &goto_model, ui_message_handlert &ui, 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:502
mstreamt & result() const
Definition: message.h:396
Memory models for partial order concurrency.
void get_memory_model()
Definition: bmc.cpp:219
safety_checkert::resultt execute(abstract_goto_modelt &)
Definition: bmc.cpp:254
virtual resultt run(const goto_functionst &goto_functions)
Definition: bmc.h:91
virtual resultt stop_on_fail(prop_convt &solver)
Definition: bmc.cpp:456
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:108
symbol_tablet symex_symbol_table
symbol table generated during symbolic execution
Definition: bmc.h:170
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
std::unique_ptr< memory_model_baset > memory_model
Definition: bmc.h:176
symex_target_equationt equation
Definition: bmc.h:172
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:235
virtual void report_success()
Definition: bmc.cpp:155
trace_optionst trace_options()
Definition: bmc.h:191
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:46
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:56
Storage of symbolic execution paths to resume.
bmct(const optionst &_options, const symbol_tablet &outer_symbol_table, ui_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:136
void output_graphml(resultt result)
outputs witnesses in graphml format
Definition: bmc.cpp:95