cprover
single_path_symex_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Single Path Symbolic Execution
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/ui_message.h>
15 
16 #include "bmc_util.h"
18 #include "symex_bmc.h"
19 
21  const optionst &options,
22  ui_message_handlert &ui_message_handler,
23  abstract_goto_modelt &goto_model)
24  : single_path_symex_only_checkert(options, ui_message_handler, goto_model)
25 {
26 }
27 
29 operator()(propertiest &properties)
30 {
31  resultt result(resultt::progresst::DONE);
32 
33  // There might be more solutions from the previous equation.
35  {
37  result, properties, *property_decider, std::chrono::duration<double>(0));
38 
39  if(result.progress == resultt::progresst::FOUND_FAIL)
40  return result;
41  }
42 
43  if(!worklist->empty())
44  {
45  // We pop the item processed in the previous iteration.
46  worklist->pop();
47  }
48 
50  {
51  symex_initialized = true;
52 
54  }
55 
56  while(!has_finished_exploration(properties))
57  {
58  path_storaget::patht &path = worklist->peek();
59  const bool ready_to_decide = resume_path(path);
60 
61  if(ready_to_decide)
62  {
63  update_properties(properties, result.updated_properties, path.equation);
64 
65  property_decider = util_make_unique<goto_symex_property_decidert>(
67 
68  const auto solver_runtime =
70 
72  result, properties, *property_decider, solver_runtime);
73 
74  if(result.progress == resultt::progresst::FOUND_FAIL)
75  return result;
76  }
77 
78  worklist->pop();
79  }
80 
81  log.status() << "Runtime Symex: " << symex_runtime.count() << "s"
82  << messaget::eom;
83 
84  final_update_properties(properties, result.updated_properties);
85 
86  // Worklist is empty: we are done.
87  return result;
88 }
89 
91  const symex_bmct &symex,
92  const path_storaget::patht &)
93 {
94  return symex.get_remaining_vccs() > 0;
95 }
96 
97 std::chrono::duration<double>
99  propertiest &properties,
100  symex_target_equationt &equation,
101  goto_symex_property_decidert &property_decider)
102 {
103  std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
104  properties, equation, property_decider, ui_message_handler);
105 
106  return solver_runtime;
107 }
108 
111  propertiest &properties,
112  goto_symex_property_decidert &property_decider,
113  std::chrono::duration<double> solver_runtime)
114 {
116  result,
117  properties,
120  solver_runtime,
121  false);
122 }
123 
125 {
126  goto_tracet goto_trace;
128  property_decider->get_equation(),
129  property_decider->get_equation().SSA_steps.end(),
130  property_decider->get_decision_procedure(),
131  ns,
132  goto_trace);
133 
134  return goto_trace;
135 }
136 
138 {
139  if(options.get_bool_option("beautify"))
140  {
141  // NOLINTNEXTLINE(whitespace/braces)
143  dynamic_cast<boolbvt &>(property_decider->get_stack_decision_procedure()),
144  property_decider->get_equation());
145  }
146 
147  goto_tracet goto_trace;
149  property_decider->get_equation(),
150  property_decider->get_decision_procedure(),
151  ns,
152  goto_trace);
153 
154  return goto_trace;
155 }
156 
159 {
160  goto_tracet goto_trace;
162  property_decider->get_equation(),
164  property_decider->get_decision_procedure(),
165  ns,
166  goto_trace);
167 
168  return goto_trace;
169 }
170 
172 {
173  return ns;
174 }
175 
177  const goto_tracet &goto_trace)
178 {
179  output_graphml(goto_trace, ns, options);
180 }
181 
183 {
184  // This is incorrect, but the best we can do at the moment.
185  const path_storaget::patht &resume = worklist->peek();
186  output_graphml(resume.equation, ns, options);
187 }
single_path_symex_checkert::build_trace
goto_tracet build_trace(const irep_idt &) const override
Builds and returns the trace for the FAILed property with the given property_id.
Definition: single_path_symex_checker.cpp:158
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
single_path_symex_only_checkert::ns
namespacet ns
Definition: single_path_symex_only_checker.h:39
build_goto_trace
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const decision_proceduret &decision_procedure, const namespacet &ns, goto_tracet &goto_trace)
Build a trace by going through the steps of target and stopping after the step matching a given condi...
Definition: build_goto_trace.cpp:204
output_graphml
void output_graphml(const goto_tracet &goto_trace, const namespacet &ns, const optionst &options)
outputs an error witness in graphml format
Definition: bmc_util.cpp:108
ui_message_handlert
Definition: ui_message.h:22
incremental_goto_checkert::resultt
Definition: incremental_goto_checker.h:43
optionst
Definition: options.h:23
incremental_goto_checkert::options
const optionst & options
Definition: incremental_goto_checker.h:91
messaget::status
mstreamt & status() const
Definition: message.h:414
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
single_path_symex_checkert::symex_initialized
bool symex_initialized
Definition: single_path_symex_checker.h:47
counterexample_beautificationt
Definition: counterexample_beautification.h:20
incremental_goto_checkert::log
messaget log
Definition: incremental_goto_checker.h:93
single_path_symex_checkert::prepare_property_decider
virtual std::chrono::duration< double > prepare_property_decider(propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider)
Prepare the property_decider for solving.
Definition: single_path_symex_checker.cpp:98
messaget::eom
static eomt eom
Definition: message.h:297
single_path_symex_checkert::is_ready_to_decide
bool is_ready_to_decide(const symex_bmct &, const path_storaget::patht &) override
Returns whether the given path produced by symex is ready to be checked.
Definition: single_path_symex_checker.cpp:90
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bmc_util.h
Bounded Model Checking Utilities.
path_storaget::patht::equation
symex_target_equationt equation
Definition: path_storage.h:43
single_path_symex_checkert::build_shortest_trace
goto_tracet build_shortest_trace() const override
Builds and returns the trace up to the first failed property.
Definition: single_path_symex_checker.cpp:137
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
single_path_symex_checkert::run_property_decider
virtual void run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, std::chrono::duration< double > solver_runtime)
Run the property_decider, which calls the SAT solver, and set the status of checked properties accord...
Definition: single_path_symex_checker.cpp:109
single_path_symex_checkert::single_path_symex_checkert
single_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: single_path_symex_checker.cpp:20
single_path_symex_only_checkert::worklist
std::unique_ptr< path_storaget > worklist
Definition: single_path_symex_only_checker.h:41
single_path_symex_checker.h
Goto Checker using Single Path Symbolic Execution.
single_path_symex_checkert::output_error_witness
void output_error_witness(const goto_tracet &) override
Definition: single_path_symex_checker.cpp:176
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
single_path_symex_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_checker.cpp:29
path_storaget::patht
Information saved at a conditional goto to resume execution.
Definition: path_storage.h:42
single_path_symex_checkert::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: single_path_symex_checker.cpp:124
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
ssa_step_matches_failing_property
ssa_step_predicatet ssa_step_matches_failing_property(const irep_idt &property_id)
Returns a function that checks whether an SSA step is an assertion with property_id.
Definition: bmc_util.cpp:55
single_path_symex_checkert::output_proof
void output_proof() override
Definition: single_path_symex_checker.cpp:182
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
single_path_symex_only_checkert::symex_runtime
std::chrono::duration< double > symex_runtime
Definition: single_path_symex_only_checker.h:42
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:175
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
single_path_symex_checkert::get_namespace
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
Definition: single_path_symex_checker.cpp:171
boolbvt
Definition: boolbv.h:42
goto_symex_property_decidert
Provides management of goal variables that encode properties.
Definition: goto_symex_property_decider.h:24
counterexample_beautification.h
Counterexample Beautification.
incremental_goto_checkert::resultt::progress
progresst progress
Definition: incremental_goto_checker.h:54
single_path_symex_checkert::property_decider
std::unique_ptr< goto_symex_property_decidert > property_decider
Definition: single_path_symex_checker.h:48
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
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:24
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:92
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
goto_symext::get_remaining_vccs
unsigned get_remaining_vccs() const
Definition: goto_symex.h:827
ui_message.h