cprover
single_loop_incremental_symex_checker.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Goto Checker using Multi-Path Symbolic Execution
4  with Incremental Unwinding of a specified Loop
5 
6 Author: Daniel Kroening, Peter Schrammel
7 
8 \*******************************************************************/
9 
13 
15 
16 #include <chrono>
17 
18 #include <util/structured_data.h>
19 
20 #include <goto-symex/slice.h>
21 
22 #include "bmc_util.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  equation(ui_message_handler),
33  symex(
34  ui_message_handler,
35  goto_model.get_symbol_table(),
36  equation,
37  options,
38  path_storage,
39  guard_manager,
40  ui_message_handler.get_ui()),
41  property_decider(options, ui_message_handler, equation, ns)
42 {
44 
45  // Freeze all symbols if we are using a prop_conv_solvert
46  prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(
48  if(prop_conv_solver != nullptr)
49  prop_conv_solver->set_all_frozen();
50 }
51 
53  const propertiest &properties,
54  messaget &message_hander)
55 {
56  const auto any_failures = std::any_of(
57  properties.begin(),
58  properties.end(),
59  [](const std::pair<irep_idt, property_infot> &property) {
60  return property.second.status == property_statust::FAIL;
61  });
62  std::string status = any_failures ? "FAILURE" : "INCONCLUSIVE";
63  structured_datat incremental_status{
64  {{labelt({"incremental", "status"}),
66  message_hander.statistics() << incremental_status;
67 }
68 
70 operator()(propertiest &properties)
71 {
72  resultt result(resultt::progresst::DONE);
73 
74  std::chrono::duration<double> solver_runtime(0);
75 
76  // we haven't got an equation yet
78  {
81 
82  // This might add new properties such as unwinding assertions, for instance.
84  properties, result.updated_properties, equation);
85 
87  }
88 
89  while(has_properties_to_check(properties))
90  {
91  // There are NOT_CHECKED or UNKNOWN properties.
92 
93  if(count_properties(properties, property_statust::UNKNOWN) > 0)
94  {
95  // We have UNKNOWN properties, i.e. properties that we can check
96  // on the current equation.
97 
98  log.status()
99  << "Passing problem to "
101  << messaget::eom;
102 
103  const auto solver_start = std::chrono::steady_clock::now();
104 
106  {
108 
109  log.status() << "converting SSA" << messaget::eom;
112 
114  properties);
115 
116  // We convert the assertions in a new context.
121 
123  }
124 
126  [&properties](const irep_idt &property_id) {
127  return is_property_to_check(properties.at(property_id).status);
128  });
129 
130  log.status()
131  << "Running "
133  << messaget::eom;
134 
136 
138  properties, result.updated_properties, dec_result, false);
139 
140  const auto solver_stop = std::chrono::steady_clock::now();
141  solver_runtime +=
142  std::chrono::duration<double>(solver_stop - solver_start);
143  log.status() << "Runtime decision procedure: " << solver_runtime.count()
144  << "s" << messaget::eom;
145 
146  result.progress =
148  ? resultt::progresst::FOUND_FAIL
149  : resultt::progresst::DONE;
150 
151  // We've got a trace to report.
152  if(result.progress == resultt::progresst::FOUND_FAIL)
153  break;
154 
155  // Nothing else to do with the current set of assertions.
156  // Let's pop them.
158  }
159 
160  // Now we are finally done.
162  {
163  // For now, we assume that UNKNOWN properties are PASS.
165  properties, result.updated_properties);
166 
167  // For now, we assume that NOT_REACHED properties are PASS.
169  properties, result.updated_properties);
170 
171  break;
172  }
173 
174  output_incremental_status(properties, log);
175 
176  // We continue symbolic execution
180 
181  // This might add new properties such as unwinding assertions, for instance.
183  properties, result.updated_properties, equation);
184 
186  }
187 
188  return result;
189 }
190 
192 {
193  goto_tracet goto_trace;
195  equation,
196  equation.SSA_steps.end(),
198  ns,
199  goto_trace);
200 
201  return goto_trace;
202 }
203 
205 {
206  if(options.get_bool_option("beautify"))
207  {
208  // NOLINTNEXTLINE(whitespace/braces)
211  equation);
212  }
213 
214  goto_tracet goto_trace;
217 
218  return goto_trace;
219 }
220 
222  const irep_idt &property_id) const
223 {
224  goto_tracet goto_trace;
226  equation,
229  ns,
230  goto_trace);
231 
232  return goto_trace;
233 }
234 
236 {
237  return ns;
238 }
239 
241 {
243 }
244 
246  const goto_tracet &error_trace)
247 {
248  output_graphml(error_trace, ns, options);
249 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
single_loop_incremental_symex_checkert::operator()
resultt operator()(propertiest &) override
Check whether the given properties with status NOT_CHECKED, UNKNOWN or properties newly discovered by...
Definition: single_loop_incremental_symex_checker.cpp:70
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
single_loop_incremental_symex_checkert::symex_symbol_table
symbol_tablet symex_symbol_table
Definition: single_loop_incremental_symex_checker.h:55
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
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
structured_data_entryt::data_node
static structured_data_entryt data_node(const jsont &data)
Definition: structured_data.cpp:64
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
stack_decision_proceduret::push
virtual void push(const std::vector< exprt > &assumptions)=0
Pushes a new context on the stack that consists of the given (possibly empty vector of) assumptions.
messaget::status
mstreamt & status() const
Definition: message.h:414
single_loop_incremental_symex_checkert::output_error_witness
void output_error_witness(const goto_tracet &) override
Definition: single_loop_incremental_symex_checker.cpp:245
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
counterexample_beautificationt
Definition: counterexample_beautification.h:20
incremental_goto_checkert::log
messaget log
Definition: incremental_goto_checker.h:93
single_loop_incremental_symex_checkert::current_equation_converted
bool current_equation_converted
Definition: single_loop_incremental_symex_checker.h:63
messaget::eom
static eomt eom
Definition: message.h:297
goto_symex_property_decidert::solve
decision_proceduret::resultt solve()
Calls solve() on the solver instance.
Definition: goto_symex_property_decider.cpp:101
output_incremental_status
void output_incremental_status(const propertiest &properties, messaget &message_hander)
Definition: single_loop_incremental_symex_checker.cpp:52
single_loop_incremental_symex_checkert::build_full_trace
goto_tracet build_full_trace() const override
Builds and returns the complete trace.
Definition: single_loop_incremental_symex_checker.cpp:191
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:33
decision_proceduret::resultt::D_SATISFIABLE
@ D_SATISFIABLE
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
single_loop_incremental_symex_checkert::ns
namespacet ns
Definition: single_loop_incremental_symex_checker.h:56
bmc_util.h
Bounded Model Checking Utilities.
single_loop_incremental_symex_checkert::initial_equation_generated
bool initial_equation_generated
Definition: single_loop_incremental_symex_checker.h:61
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
single_loop_incremental_symex_checkert::output_proof
void output_proof() override
Definition: single_loop_incremental_symex_checker.cpp:240
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
goto_symex_property_decidert::convert_goals
void convert_goals()
Convert the instances of a property into a goal variable.
Definition: goto_symex_property_decider.cpp:71
single_loop_incremental_symex_checkert::equation
symex_target_equationt equation
Definition: single_loop_incremental_symex_checker.h:57
single_loop_incremental_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_loop_incremental_symex_checker.cpp:221
labelt
Definition: structured_data.h:17
single_loop_incremental_symex_checkert::symex
symex_bmc_incremental_one_loopt symex
Definition: single_loop_incremental_symex_checker.h:60
is_property_to_check
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:170
single_loop_incremental_symex_checkert::full_equation_generated
bool full_equation_generated
Definition: single_loop_incremental_symex_checker.h:62
revert_slice
void revert_slice(symex_target_equationt &equation)
Undo whatever has been done by slice
Definition: slice.cpp:261
goto_symex_property_decidert::get_decision_procedure
decision_proceduret & get_decision_procedure() const
Returns the solver instance.
Definition: goto_symex_property_decider.cpp:107
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:113
single_loop_incremental_symex_checkert::get_namespace
const namespacet & get_namespace() const override
Returns the namespace associated with the traces.
Definition: single_loop_incremental_symex_checker.cpp:235
prop_conv_solvert::set_all_frozen
void set_all_frozen()
Definition: prop_conv_solver.cpp:35
count_properties
std::size_t count_properties(const propertiest &properties, property_statust status)
Return the number of properties with given status.
Definition: properties.cpp:159
goto_symex_property_decidert::add_constraint_from_goals
void add_constraint_from_goals(std::function< bool(const irep_idt &property_id)> select_property)
Add disjunction of negated selected properties to the equation.
Definition: goto_symex_property_decider.cpp:82
decision_proceduret::resultt
resultt
Result of running the decision procedure.
Definition: decision_procedure.h:44
structured_datat
A way of representing nested key/value data.
Definition: structured_data.h:74
property_statust::UNKNOWN
@ UNKNOWN
The checker was unable to determine the status of the property.
goto_symex_property_decidert::update_properties_goals_from_symex_target_equation
void update_properties_goals_from_symex_target_equation(propertiest &properties)
Get the conditions for the properties from the equation and collect all 'instances' of the properties...
Definition: goto_symex_property_decider.cpp:43
symex_target_equationt::convert_assertions
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
Definition: symex_target_equation.cpp:503
decision_proceduret::decision_procedure_text
virtual std::string decision_procedure_text() const =0
Return a textual description of the decision procedure.
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
incremental_goto_checkert
An implementation of incremental_goto_checkert provides functionality for checking a set of propertie...
Definition: incremental_goto_checker.h:36
setup_symex
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:179
goto_symex_property_decidert::update_properties_status_from_goals
void update_properties_status_from_goals(propertiest &properties, std::unordered_set< irep_idt > &updated_properties, decision_proceduret::resultt dec_result, bool set_pass=true) const
Update the property status from the truth value of the goal variable.
Definition: goto_symex_property_decider.cpp:123
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:250
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
single_loop_incremental_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_loop_incremental_symex_checker.cpp:204
single_loop_incremental_symex_checkert::goto_model
abstract_goto_modelt & goto_model
Definition: single_loop_incremental_symex_checker.h:54
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
symex_target_equationt::convert_without_assertions
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
Definition: symex_target_equation.cpp:330
symex_bmc_incremental_one_loopt::resume
bool resume(const get_goto_functiont &get_goto_function)
Return true if symex can be resumed.
Definition: symex_bmc_incremental_one_loop.cpp:132
goto_tracet
Trace of a GOTO program.
Definition: goto_trace.h:175
boolbvt
Definition: boolbv.h:42
counterexample_beautification.h
Counterexample Beautification.
incremental_goto_checkert::resultt::progress
progresst progress
Definition: incremental_goto_checker.h:54
stack_decision_proceduret::pop
virtual void pop()=0
Pop whatever is on top of the stack.
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
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
structured_data.h
single_loop_incremental_symex_checker.h
Goto Checker using multi-path symbolic execution with incremental unwinding of a specified loop.
incremental_goto_checkert::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: incremental_goto_checker.h:92
symex_bmc_incremental_one_loopt::from_entry_point_of
bool from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_tablet &new_symbol_table)
Return true if symex can be resumed.
Definition: symex_bmc_incremental_one_loop.cpp:121
slice.h
Slicer for symex traces.
single_loop_incremental_symex_checkert::property_decider
goto_symex_property_decidert property_decider
Definition: single_loop_incremental_symex_checker.h:64
prop_conv_solvert
Definition: prop_conv_solver.h:29
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
json_stringt
Definition: json.h:270
single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert
single_loop_incremental_symex_checkert(const optionst &options, ui_message_handlert &ui_message_handler, abstract_goto_modelt &goto_model)
Definition: single_loop_incremental_symex_checker.cpp:25