CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
multi_path_symex_only_checker.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Checker using Multi-Path Symbolic Execution Only
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
13
14#include <util/ui_message.h>
15
18#include <goto-symex/show_vcc.h>
19
20#include "bmc_util.h"
21
23 const optionst &options,
24 ui_message_handlert &ui_message_handler,
25 abstract_goto_modelt &goto_model)
26 : incremental_goto_checkert(options, ui_message_handler),
27 goto_model(goto_model),
28 ns(goto_model.get_symbol_table(), symex_symbol_table),
29 equation(ui_message_handler),
30 unwindset(goto_model),
31 symex(
32 ui_message_handler,
33 goto_model.get_symbol_table(),
34 equation,
35 options,
36 path_storage,
37 guard_manager,
38 unwindset)
39{
41}
42
44operator()(propertiest &properties)
45{
47
49 options.get_option("symex-coverage-report"),
51 symex,
53
54 if(options.get_bool_option("show-vcc"))
55 {
57 }
58
59 if(options.get_bool_option("program-only"))
60 {
62 }
63
64 if(options.get_bool_option("show-byte-ops"))
65 {
67 }
68
69 resultt result(resultt::progresst::DONE);
70 update_properties(properties, result.updated_properties);
71 return result;
72}
73
75{
76 // Gather fields for shadow memory instrumentation
77 const auto fields =
79
80 const auto symex_start = std::chrono::steady_clock::now();
81
84
85 const auto symex_stop = std::chrono::steady_clock::now();
86 std::chrono::duration<double> symex_runtime =
87 std::chrono::duration<double>(symex_stop - symex_start);
88 log.statistics() << "Runtime Symex: " << symex_runtime.count() << "s"
90
92}
93
95 propertiest &properties,
96 std::unordered_set<irep_idt> &updated_properties)
97{
98 if(options.get_bool_option("symex-driven-lazy-loading"))
100
102 properties, updated_properties, equation);
103 // Since we will not symex any further we can decide the status
104 // of all properties that do not occur in the equation now.
105 // The current behavior is PASS.
106 update_status_of_not_checked_properties(properties, updated_properties);
107}
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:306
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:238
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:274
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:322
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition bmc_util.cpp:178
Bounded Model Checking Utilities.
Abstract interface to eager or lazy GOTO models.
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 symex_from_entry_point_of(const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)
Symbolically execute the entire program starting from entry point.
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
multi_path_symex_only_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
virtual void update_properties(propertiest &properties, std::unordered_set< irep_idt > &updated_properties)
Updates the properties from the equation and adds their property IDs to updated_properties.
virtual void generate_equation()
Generates the equation by running goto-symex.
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...
Goto Checker using Multi-Path Symbolic Execution only (no SAT solving)
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)
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()