cprover
multi_path_symex_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Bounded Model Checking
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <chrono>
15 
16 #include "bmc_util.h"
19 
21  const optionst &options,
22  ui_message_handlert &ui_message_handler,
23  abstract_goto_modelt &goto_model)
24  : multi_path_symex_only_checkert(options, ui_message_handler, goto_model),
25  equation_generated(false),
26  property_decider(options, ui_message_handler, equation, ns)
27 {
28 }
29 
31 operator()(propertiest &properties)
32 {
33  resultt result(resultt::progresst::DONE);
34 
35  // When the equation has been generated, we know all the properties.
36  // Have we got anything to check? Otherwise we return DONE.
38  return result;
39 
40  std::chrono::duration<double> solver_runtime(0);
41 
42  // we haven't got an equation yet
44  {
46 
48  options.get_option("symex-coverage-report"),
49  goto_model,
50  symex,
52 
53  update_properties(properties, result.updated_properties);
54 
55  // Have we got anything to check? Otherwise we return DONE.
56  if(!has_properties_to_check(properties))
57  return result;
58 
59  solver_runtime += prepare_property_decider(properties);
60 
61  equation_generated = true;
62  }
63 
64  run_property_decider(result, properties, solver_runtime);
65 
66  return result;
67 }
68 
69 std::chrono::duration<double>
71 {
72  std::chrono::duration<double> solver_runtime = ::prepare_property_decider(
74 
75  return solver_runtime;
76 }
77 
80  propertiest &properties,
81  std::chrono::duration<double> solver_runtime)
82 {
84  result, properties, property_decider, ui_message_handler, solver_runtime);
85 }
86 
88 {
89  goto_tracet goto_trace;
91  equation,
92  equation.SSA_steps.end(),
94  ns,
95  goto_trace);
96 
97  return goto_trace;
98 }
99 
101 {
102  if(options.get_bool_option("beautify"))
103  {
104  // NOLINTNEXTLINE(whitespace/braces)
107  equation);
108  }
109 
110  goto_tracet goto_trace;
113 
114  return goto_trace;
115 }
116 
119 {
120  goto_tracet goto_trace;
122  equation,
125  ns,
126  goto_trace);
127 
128  return goto_trace;
129 }
130 
132 {
133  return ns;
134 }
135 
137 {
139 }
140 
142  const goto_tracet &error_trace)
143 {
144  output_graphml(error_trace, ns, options);
145 }
146 
149 {
150  goto_symex_fault_localizert fault_localizer(
151  options,
153  equation,
155 
156  return fault_localizer(property_id);
157 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
multi_path_symex_checkert::property_decider
goto_symex_property_decidert property_decider
Definition: multi_path_symex_checker.h:59
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
multi_path_symex_checkert::output_proof
void output_proof() override
Definition: multi_path_symex_checker.cpp:136
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:107
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:83
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
multi_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: multi_path_symex_checker.cpp:100
multi_path_symex_checkert::operator()
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
Definition: multi_path_symex_checker.cpp:31
counterexample_beautificationt
Definition: counterexample_beautification.h:22
fault_location_infot
Definition: fault_localization_provider.h:23
multi_path_symex_only_checkert::equation
symex_target_equationt equation
Definition: multi_path_symex_only_checker.h:33
multi_path_symex_checkert::localize_fault
fault_location_infot localize_fault(const irep_idt &property_id) const override
Returns the most likely fault locations for the given FAILed property_id.
Definition: multi_path_symex_checker.cpp:148
goto_symex_fault_localizert
Definition: goto_symex_fault_localizer.h:26
multi_path_symex_checkert::equation_generated
bool equation_generated
Definition: multi_path_symex_checker.h:58
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
multi_path_symex_only_checkert::symex
symex_bmct symex
Definition: multi_path_symex_only_checker.h:36
multi_path_symex_only_checkert::ns
namespacet ns
Definition: multi_path_symex_only_checker.h:32
bmc_util.h
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:174
multi_path_symex_checkert::output_error_witness
void output_error_witness(const goto_tracet &) override
Definition: multi_path_symex_checker.cpp:141
multi_path_symex_only_checkert
Definition: multi_path_symex_only_checker.h:20
multi_path_symex_checker.h
goto_symex_property_decidert::get_decision_procedure
decision_proceduret & get_decision_procedure() const
Returns the solver instance.
Definition: goto_symex_property_decider.cpp:108
goto_symex_property_decidert::get_stack_decision_procedure
stack_decision_proceduret & get_stack_decision_procedure() const
Returns the solver instance.
Definition: goto_symex_property_decider.cpp:114
multi_path_symex_checkert::prepare_property_decider
virtual std::chrono::duration< double > prepare_property_decider(propertiest &properties)
Prepare the property decider for solving.
Definition: multi_path_symex_checker.cpp:70
multi_path_symex_checkert::get_namespace
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
Definition: multi_path_symex_checker.cpp:131
multi_path_symex_only_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: multi_path_symex_only_checker.h:30
multi_path_symex_only_checkert::update_properties
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.
Definition: multi_path_symex_only_checker.cpp:74
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
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:255
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
multi_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: multi_path_symex_checker.cpp:118
multi_path_symex_checkert::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: multi_path_symex_checker.cpp:87
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
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:171
boolbvt
Definition: boolbv.h:35
counterexample_beautification.h
goto_symex_fault_localizer.h
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:59
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:84
multi_path_symex_checkert::run_property_decider
virtual void run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, std::chrono::duration< double > solver_runtime)
Run the property decider, which calls the SAT solver, and set the status of checked properties accord...
Definition: multi_path_symex_checker.cpp:78
multi_path_symex_checkert::multi_path_symex_checkert
multi_path_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: multi_path_symex_checker.cpp:20
multi_path_symex_only_checkert::generate_equation
virtual void generate_equation()
Generates the equation by running goto-symex.
Definition: multi_path_symex_only_checker.cpp:67