cprover
single_path_symex_only_checker.cpp
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 
13 
14 #include <chrono>
15 
16 #include <util/ui_message.h>
17 
20 #include <goto-symex/show_vcc.h>
21 
22 #include "bmc_util.h"
23 #include "symex_bmc.h"
24 
26  const optionst &options,
27  ui_message_handlert &ui_message_handler,
28  abstract_goto_modelt &goto_model)
29  : incremental_goto_checkert(options, ui_message_handler),
30  goto_model(goto_model),
31  ns(goto_model.get_symbol_table(), symex_symbol_table),
32  worklist(get_path_strategy(options.get_option("exploration-strategy"))),
33  symex_runtime(0)
34 {
35 }
36 
38 operator()(propertiest &properties)
39 {
40  resultt result(resultt::progresst::DONE);
41 
43 
44  while(!has_finished_exploration(properties))
45  {
46  path_storaget::patht &path = worklist->peek();
47 
48  (void)resume_path(path);
49 
50  update_properties(properties, result.updated_properties, path.equation);
51 
52  worklist->pop();
53  }
54 
55  log.status() << "Runtime Symex: " << symex_runtime.count() << "s"
56  << messaget::eom;
57 
58  final_update_properties(properties, result.updated_properties);
59 
60  return result;
61 }
62 
64 {
65  // Put initial state into the work list
67  symex_bmct symex(
70  equation,
71  options,
72  *worklist,
74  setup_symex(symex);
75 
78 }
79 
81  const propertiest &properties)
82 {
83  return worklist->empty() ||
84  (!options.get_bool_option("paths-symex-explore-all") &&
85  !has_properties_to_check(properties));
86 }
87 
89 {
90  const auto symex_start = std::chrono::steady_clock::now();
91 
92  symex_bmct symex(
95  path.equation,
96  options,
97  *worklist,
99  setup_symex(symex);
100 
103  path.state,
104  &path.equation,
106 
107  const auto symex_stop = std::chrono::steady_clock::now();
108  symex_runtime += std::chrono::duration<double>(symex_stop - symex_start);
109 
111 
112  equation_output(symex, path.equation);
113 
114  return is_ready_to_decide(symex, path);
115 }
116 
118  const symex_bmct &,
119  const path_storaget::patht &)
120 {
121  // we don't check anything here
122  return false;
123 }
124 
126  const symex_bmct &symex,
127  const symex_target_equationt &equation)
128 {
130  options.get_option("symex-coverage-report"),
131  goto_model,
132  symex,
134 
135  if(options.get_bool_option("show-vcc"))
136  show_vcc(options, ui_message_handler, equation);
137 
138  if(options.get_bool_option("program-only"))
139  show_program(ns, equation);
140 
141  if(options.get_bool_option("show-byte-ops"))
143 
144  if(options.get_bool_option("validate-ssa-equation"))
145  {
147  }
148 }
149 
151 {
153 }
154 
156  propertiest &properties,
157  std::unordered_set<irep_idt> &updated_properties,
158  const symex_target_equationt &equation)
159 {
160  if(options.get_bool_option("symex-driven-lazy-loading"))
162 
164  properties, updated_properties, equation);
165 }
166 
168  propertiest &properties,
169  std::unordered_set<irep_idt> &updated_properties)
170 {
171  // For now, we assume that NOT_REACHED properties are PASS.
172  update_status_of_not_checked_properties(properties, updated_properties);
173 
174  // For now, we assume that UNKNOWN properties are PASS.
175  update_status_of_unknown_properties(properties, updated_properties);
176 }
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
show_program
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Print the steps of equation on the standard output.
Definition: show_program.cpp:58
update_status_of_unknown_properties
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:290
single_path_symex_only_checkert::ns
namespacet ns
Definition: single_path_symex_only_checker.h:39
postprocess_equation
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
single_path_symex_only_checkert::setup_symex
virtual void setup_symex(symex_bmct &symex)
Definition: single_path_symex_only_checker.cpp:150
abstract_goto_modelt::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
ui_message_handlert
Definition: ui_message.h:22
incremental_goto_checkert::resultt
Definition: incremental_goto_checker.h:43
optionst
Definition: options.h:23
show_vcc.h
Output of the verification conditions (VCCs)
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:91
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
messaget::status
mstreamt & status() const
Definition: message.h:414
single_path_symex_only_checkert::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: single_path_symex_only_checker.h:38
goto_symext::resume_symex_from_saved_state
virtual void resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation, symbol_tablet &new_symbol_table)
Performs symbolic execution using a state and equation that have already been used to symbolically ex...
Definition: symex_main.cpp:382
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:38
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:88
update_status_of_not_checked_properties
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
incremental_goto_checkert::log
messaget log
Definition: incremental_goto_checker.h:93
goto_symext::initialize_path_storage_from_entry_point_of
virtual void initialize_path_storage_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Puts the initial state of the entry point function into the path storage.
Definition: symex_main.cpp:479
messaget::eom
static eomt eom
Definition: message.h:297
single_path_symex_only_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: single_path_symex_only_checker.h:37
update_properties_from_goto_model
void update_properties_from_goto_model(propertiest &properties, const abstract_goto_modelt &goto_model)
Updates properties with the assertions in goto_model.
Definition: properties.cpp:75
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:25
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:117
bmc_util.h
Bounded Model Checking Utilities.
path_storaget::patht::equation
symex_target_equationt equation
Definition: path_storage.h:43
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:167
update_properties_status_from_symex_target_equation
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
has_properties_to_check
bool has_properties_to_check(const propertiest &properties)
Return true if there as a property with NOT_CHECKED or UNKNOWN status.
Definition: properties.cpp:176
single_path_symex_only_checkert::worklist
std::unique_ptr< path_storaget > worklist
Definition: single_path_symex_only_checker.h:41
goto_symext::validate
void validate(const validation_modet vm) const
Definition: goto_symex.h:836
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:63
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:34
show_vcc
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:166
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:125
incremental_goto_checkert
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
Definition: incremental_goto_checker.h:36
path_storaget::patht::state
goto_symex_statet state
Definition: path_storage.h:44
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
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
single_path_symex_only_checkert::symex_runtime
std::chrono::duration< double > symex_runtime
Definition: single_path_symex_only_checker.h:42
output_coverage_report
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
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:80
incremental_goto_checkert::resultt::updated_properties
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
Definition: incremental_goto_checker.h:61
show_program.h
Output of the program (SSA) constraints.
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
symex_bmct
Definition: symex_bmc.h:24
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:92
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
show_byte_ops
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...
Definition: show_program.cpp:320
single_path_symex_only_checker.h
Goto Checker using Single Path Symbolic Execution only.
symex_bmc.h
Bounded Model Checking for ANSI-C.
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:155
get_path_strategy
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 ...
Definition: path_storage.cpp:129
ui_message.h