cprover
symex_bmc.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking for ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_SYMEX_BMC_H
13 #define CPROVER_GOTO_CHECKER_SYMEX_BMC_H
14 
15 #include <util/message.h>
16 #include <util/threeval.h>
17 
18 #include <goto-symex/goto_symex.h>
20 
22 
23 #include "symex_coverage.h"
24 
25 class symex_bmct : public goto_symext
26 {
27 public:
28  symex_bmct(
29  message_handlert &mh,
31  symex_target_equationt &_target,
32  const optionst &options,
35 
36  // To show progress
38 
45  typedef std::function<
46  tvt(const call_stackt &, unsigned, unsigned, unsigned &)>
48 
55  typedef std::function<tvt(const irep_idt &, unsigned, unsigned &)>
57 
63  {
64  loop_unwind_handlers.push_back(handler);
65  }
66 
72  {
73  recursion_unwind_handlers.push_back(handler);
74  }
75 
77  const goto_functionst &goto_functions,
78  const std::string &path) const
79  {
80  return symex_coverage.generate_report(goto_functions, path);
81  }
82 
83  const bool record_coverage;
85 
87 
88 protected:
90  std::vector<loop_unwind_handlert> loop_unwind_handlers;
91 
94  std::vector<recursion_unwind_handlert> recursion_unwind_handlers;
95 
97  override;
98 
99  void merge_goto(
100  const symex_targett::sourcet &source,
101  goto_statet &&goto_state,
102  statet &state) override;
103 
104  bool should_stop_unwind(
105  const symex_targett::sourcet &source,
106  const call_stackt &context,
107  unsigned unwind) override;
108 
110  const irep_idt &identifier,
111  unsigned thread_nr,
112  unsigned unwind) override;
113 
114  void no_body(const irep_idt &identifier) override;
115 
116  std::unordered_set<irep_idt> body_warnings;
117 
119 };
120 
121 #endif // CPROVER_GOTO_CHECKER_SYMEX_BMC_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_coveraget
Definition: symex_coverage.h:29
symex_bmct::loop_unwind_handlert
std::function< tvt(const 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
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
symex_bmct::loop_unwind_handlers
std::vector< loop_unwind_handlert > loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Definition: symex_bmc.h:90
symex_bmct::recursion_unwind_handlert
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
symex_bmct::unwindset
unwindsett unwindset
Definition: symex_bmc.h:86
optionst
Definition: options.h:23
threeval.h
path_storaget
Storage for symbolic execution paths to be resumed later.
Definition: path_storage.h:38
goto_symext::path_storage
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Definition: goto_symex.h:796
goto_symex_statet
Central data structure: state.
Definition: goto_symex_state.h:46
goto_symext::guard_manager
guard_managert & guard_manager
Used to create guards.
Definition: goto_symex.h:261
symex_bmct::record_coverage
const bool record_coverage
Definition: symex_bmc.h:83
symex_bmct::body_warnings
std::unordered_set< irep_idt > body_warnings
Definition: symex_bmc.h:116
symex_bmct::add_loop_unwind_handler
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
call_stackt
Definition: call_stack.h:15
path_storage.h
Storage of symbolic execution paths to resume.
symex_bmct::recursion_unwind_handlers
std::vector< recursion_unwind_handlert > recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
Definition: symex_bmc.h:94
symex_bmct::output_coverage_report
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:76
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
goto_symext::outer_symbol_table
const symbol_tablet & outer_symbol_table
The symbol table associated with the goto-program being executed.
Definition: goto_symex.h:247
symex_bmct::symex_bmct
symex_bmct(message_handlert &mh, const symbol_tablet &outer_symbol_table, symex_target_equationt &_target, const optionst &options, path_storaget &path_storage, guard_managert &guard_manager)
Definition: symex_bmc.cpp:21
unwindsett
Definition: unwindset.h:24
symex_bmct::add_recursion_unwind_handler
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
symex_coverage.h
Record and print code coverage of symbolic execution.
goto_symex.h
Symbolic Execution.
goto_symext
The main class for the forward symbolic simulator.
Definition: goto_symex.h:48
symex_coveraget::generate_report
bool generate_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_coverage.cpp:423
message_handlert
Definition: message.h:28
symex_bmct::symex_coverage
symex_coveraget symex_coverage
Definition: symex_bmc.h:118
symex_bmct::should_stop_unwind
bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind) override
Determine whether to unwind a loop.
Definition: symex_bmc.cpp:118
goto_statet
Container for data that varies per program point, e.g.
Definition: goto_state.h:28
tvt
Definition: threeval.h:20
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
symex_bmct::havoc_bodyless_functions
const bool havoc_bodyless_functions
Definition: symex_bmc.h:84
source_locationt
Definition: source_location.h:20
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
symex_bmct::symex_step
void symex_step(const get_goto_functiont &get_goto_function, statet &state) override
show progress
Definition: symex_bmc.cpp:43
goto_symext::get_goto_function
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
Definition: symex_main.cpp:493
symex_bmct::get_unwind_recursion
bool get_unwind_recursion(const irep_idt &identifier, unsigned thread_nr, unsigned unwind) override
Definition: symex_bmc.cpp:164
goto_symext::get_goto_functiont
std::function< const goto_functionst::goto_functiont &(const irep_idt &)> get_goto_functiont
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
Definition: goto_symex.h:95
symex_bmct::merge_goto
void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state) override
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
Definition: symex_bmc.cpp:98
symex_bmct
Definition: symex_bmc.h:26
symex_targett::sourcet
Identifies source in the context of symbolic execution.
Definition: symex_target.h:38
unwindset.h
Loop unwinding.
message.h
symex_bmct::no_body
void no_body(const irep_idt &identifier) override
Log a warning that a function has no body.
Definition: symex_bmc.cpp:211
symex_bmct::last_source_location
source_locationt last_source_location
Definition: symex_bmc.h:37