CBMC
Loading...
Searching...
No Matches
single_path_symex_only_checker.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Single Path Symbolic Execution only
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
13
14#include <util/ui_message.h>
15
19#include <goto-symex/show_vcc.h>
20
21#include "bmc_util.h"
22#include "symex_bmc.h"
23
25 const optionst &options,
26 ui_message_handlert &ui_message_handler,
27 abstract_goto_modelt &goto_model)
28 : incremental_goto_checkert(options, ui_message_handler),
29 goto_model(goto_model),
30 ns(goto_model.get_symbol_table(), symex_symbol_table),
31 worklist(get_path_strategy(options.get_option("exploration-strategy"))),
32 symex_runtime(0)
33{
34 unwindset.parse_unwind(options.get_option("unwind"));
36 options.get_list_option("unwindset"), goto_model, ui_message_handler);
37}
38
40operator()(propertiest &properties)
41{
42 resultt result(resultt::progresst::DONE);
43
45
46 while(!has_finished_exploration(properties))
47 {
48 path_storaget::patht &path = worklist->peek();
49
50 (void)resume_path(path);
51
52 update_properties(properties, result.updated_properties, path.equation);
53
54 worklist->pop();
55 }
56
57 log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s"
59
61
62 return result;
63}
64
66{
67 // Put initial state into the work list
69 symex_bmct symex(
72 equation,
73 options,
74 *worklist,
76 unwindset);
77 setup_symex(symex);
78
79 // Gather fields for shadow memory instrumentation
80 const auto fields =
82
85}
86
88 const propertiest &properties)
89{
90 return worklist->empty() ||
91 (!options.get_bool_option("paths-symex-explore-all") &&
92 !has_properties_to_check(properties));
93}
94
96{
97 const auto symex_start = std::chrono::steady_clock::now();
98
99 symex_bmct symex(
102 path.equation,
103 options,
104 *worklist,
106 unwindset);
107 setup_symex(symex);
108
111
112 const auto symex_stop = std::chrono::steady_clock::now();
113 symex_runtime += std::chrono::duration<double>(symex_stop - symex_start);
114
116
117 equation_output(symex, path.equation);
118
119 return is_ready_to_decide(symex, path);
120}
121
123 const symex_bmct &,
124 const path_storaget::patht &)
125{
126 // we don't check anything here
127 return false;
128}
129
131 const symex_bmct &symex,
132 const symex_target_equationt &equation)
133{
135 options.get_option("symex-coverage-report"),
137 symex,
139
140 if(options.get_bool_option("show-vcc"))
142
143 if(options.get_bool_option("program-only"))
144 show_program(ns, equation);
145
146 if(options.get_bool_option("show-byte-ops"))
148
149 if(options.get_bool_option("validate-ssa-equation"))
150 {
152 }
153}
154
159
161 propertiest &properties,
162 std::unordered_set<irep_idt> &updated_properties,
163 const symex_target_equationt &equation)
164{
165 if(options.get_bool_option("symex-driven-lazy-loading"))
167
169 properties, updated_properties, equation);
170}
171
173 propertiest &properties,
174 std::unordered_set<irep_idt> &updated_properties)
175{
176 // For now, we assume that NOT_REACHED properties are PASS.
177 update_status_of_not_checked_properties(properties, updated_properties);
178
179 // For now, we assume that UNKNOWN properties are PASS.
180 update_status_of_unknown_properties(properties, updated_properties);
181}
void output_coverage_report(const std::string &cov_out, const abstract_goto_modelt &goto_model, const symex_bmct &symex, ui_message_handlert &ui_message_handler)
Output a coverage report as generated by symex_coveraget if cov_out is non-empty.
Definition bmc_util.cpp:301
void update_status_of_unknown_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of UNKNOWN properties to PASS.
Definition bmc_util.cpp:285
void update_properties_status_from_symex_target_equation(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, const symex_target_equationt &equation)
Sets property status to PASS for properties whose conditions are constant true in the equation.
Definition bmc_util.cpp:233
void update_status_of_not_checked_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Sets the property status of NOT_CHECKED properties to PASS.
Definition bmc_util.cpp:269
void postprocess_equation(symex_bmct &symex, symex_target_equationt &equation, const optionst &options, const namespacet &ns, ui_message_handlert &ui_message_handler)
Post process the equation.
Definition bmc_util.cpp:317
Bounded Model Checking Utilities.
Abstract interface to eager or lazy GOTO models.
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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 ...
virtual symbol_tablet resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation)
Performs symbolic execution using a state and equation that have already been used to symbolically ex...
void validate(const validation_modet vm) const
Definition goto_symex.h:861
virtual void initialize_path_storage_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_table_baset &new_symbol_table, const shadow_memory_field_definitionst &fields)
Puts the initial state of the entry point function into the path storage.
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
ui_message_handlert & ui_message_handler
mstreamt & statistics() const
Definition message.h:411
static eomt eom
Definition message.h:289
static shadow_memory_field_definitionst gather_field_declarations(const abstract_goto_modelt &goto_model, message_handlert &message_handler)
Gathers the available shadow memory field definitions (__CPROVER_field_decl calls) from the goto mode...
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.
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...
virtual void initialize_worklist()
Adds the initial goto-symex state as a path to the worklist.
std::chrono::duration< double > symex_runtime
std::unique_ptr< path_storaget > worklist
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.
single_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
virtual bool resume_path(path_storaget::patht &path)
Continues exploring the given path using goto-symex.
virtual bool has_finished_exploration(const propertiest &)
Returns whether we should stop exploring paths.
void equation_output(const symex_bmct &symex, const symex_target_equationt &equation)
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
void parse_unwind(const std::string &unwind)
Definition unwindset.cpp:23
void parse_unwindset(const std::list< std::string > &unwindset, abstract_goto_modelt &goto_model, message_handlert &message_handler)
std::unique_ptr< path_storaget > get_path_strategy(const std::string strategy)
Ensure that is_valid_strategy() returns true for a particular string before calling this function on ...
Storage of symbolic execution paths to resume.
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
void update_properties_from_goto_model(propertiest &properties, const abstract_goto_modelt &goto_model)
Updates properties with the assertions in goto_model.
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition properties.h:76
Symex Shadow Memory Instrumentation.
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Print the steps of equation on the standard output.
void show_byte_ops(const optionst &options, ui_message_handlert &ui_message_handler, const namespacet &ns, const symex_target_equationt &equation)
Count and display all byte extract and byte update operations from equation on standard output or fil...
Output of the program (SSA) constraints.
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Output equations from equation to a file or to the standard output.
Definition show_vcc.cpp:168
Output of the verification conditions (VCCs)
Goto Checker using Single Path Symbolic Execution only.
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
Information saved at a conditional goto to resume execution.
symex_target_equationt equation
goto_symex_statet state
Bounded Model Checking for ANSI-C.