cprover
single_path_symex_only_checker.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Single Path Symbolic Execution only
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
13 #define CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
14 
16 
18 
19 #include <chrono>
20 
21 class symex_bmct;
22 
25 {
26 public:
28  const optionst &options,
31 
32  resultt operator()(propertiest &) override;
33 
34  virtual ~single_path_symex_only_checkert() = default;
35 
36 protected:
41  std::unique_ptr<path_storaget> worklist;
42  std::chrono::duration<double> symex_runtime;
43 
44  void equation_output(
45  const symex_bmct &symex,
46  const symex_target_equationt &equation);
47 
48  virtual void setup_symex(symex_bmct &symex);
49 
51  virtual void initialize_worklist();
52 
55  virtual bool resume_path(path_storaget::patht &path);
56 
59  virtual bool
60  is_ready_to_decide(const symex_bmct &symex, const path_storaget::patht &path);
61 
63  virtual bool has_finished_exploration(const propertiest &);
64 
67  virtual void update_properties(
68  propertiest &properties,
69  std::unordered_set<irep_idt> &updated_properties,
70  const symex_target_equationt &equation);
71 
74  virtual void final_update_properties(
75  propertiest &properties,
76  std::unordered_set<irep_idt> &updated_properties);
77 };
78 
79 #endif // CPROVER_GOTO_CHECKER_SINGLE_PATH_SYMEX_ONLY_CHECKER_H
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
single_path_symex_only_checkert::ns
namespacet ns
Definition: single_path_symex_only_checker.h:39
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
single_path_symex_only_checkert::setup_symex
virtual void setup_symex(symex_bmct &symex)
Definition: single_path_symex_only_checker.cpp:149
ui_message_handlert
Definition: ui_message.h:20
incremental_goto_checkert::resultt
Definition: incremental_goto_checker.h:41
optionst
Definition: options.h:23
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:89
single_path_symex_only_checkert::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: single_path_symex_only_checker.h:38
single_path_symex_only_checkert::operator()
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
Definition: single_path_symex_only_checker.cpp:37
single_path_symex_only_checkert::resume_path
virtual bool resume_path(path_storaget::patht &path)
Continues exploring the given path using goto-symex.
Definition: single_path_symex_only_checker.cpp:87
single_path_symex_only_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: single_path_symex_only_checker.h:37
path_storage.h
Storage of symbolic execution paths to resume.
single_path_symex_only_checkert::single_path_symex_only_checkert
single_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: single_path_symex_only_checker.cpp:24
single_path_symex_only_checkert::is_ready_to_decide
virtual bool is_ready_to_decide(const symex_bmct &symex, const path_storaget::patht &path)
Returns whether the given path produced by symex is ready to be checked.
Definition: single_path_symex_only_checker.cpp:116
incremental_goto_checker.h
Incremental Goto Checker Interface.
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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
single_path_symex_only_checkert::~single_path_symex_only_checkert
virtual ~single_path_symex_only_checkert()=default
single_path_symex_only_checkert::final_update_properties
virtual void final_update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Updates the properties after having finished exploration and adds their property IDs to updated_prope...
Definition: single_path_symex_only_checker.cpp:166
single_path_symex_only_checkert::worklist
std::unique_ptr< path_storaget > worklist
Definition: single_path_symex_only_checker.h:41
single_path_symex_only_checkert::guard_manager
guard_managert guard_manager
Definition: single_path_symex_only_checker.h:40
single_path_symex_only_checkert::initialize_worklist
virtual void initialize_worklist()
Adds the initial goto-symex state as a path to the worklist.
Definition: single_path_symex_only_checker.cpp:62
path_storaget::patht
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:42
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
single_path_symex_only_checkert::equation_output
void equation_output(const symex_bmct &symex, const symex_target_equationt &equation)
Definition: single_path_symex_only_checker.cpp:124
incremental_goto_checkert
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
Definition: incremental_goto_checker.h:34
single_path_symex_only_checkert::symex_runtime
std::chrono::duration< double > symex_runtime
Definition: single_path_symex_only_checker.h:42
single_path_symex_only_checkert::has_finished_exploration
virtual bool has_finished_exploration(const propertiest &)
Returns whether we should stop exploring paths.
Definition: single_path_symex_only_checker.cpp:79
single_path_symex_only_checkert
Uses goto-symex to generate a symex_target_equationt for each path.
Definition: single_path_symex_only_checker.h:25
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
symex_bmct
Definition: symex_bmc.h:26
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:90
single_path_symex_only_checkert::update_properties
virtual void update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
Updates the properties from the equation and adds their property IDs to updated_properties.
Definition: single_path_symex_only_checker.cpp:154