cprover
bmc_util.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Bounded Model Checking Utilities
4
5Author: Daniel Kroening, Peter Schrammel
6
7\*******************************************************************/
8
11
12#include "bmc_util.h"
13
14#include <iostream>
15
19
22#include <goto-symex/slice.h>
24
26
28
29#include <util/json_stream.h>
30#include <util/make_unique.h>
31#include <util/ui_message.h>
32
34#include "symex_bmc.h"
35
37{
38 log.status() << "Building error trace" << messaget::eom;
39}
40
42 goto_tracet &goto_trace,
43 const namespacet &ns,
44 const symex_target_equationt &symex_target_equation,
45 const decision_proceduret &decision_procedure,
46 ui_message_handlert &ui_message_handler)
47{
48 messaget log(ui_message_handler);
50
51 build_goto_trace(symex_target_equation, decision_procedure, ns, goto_trace);
52}
53
56{
57 return [property_id](
58 symex_target_equationt::SSA_stepst::const_iterator step,
59 const decision_proceduret &decision_procedure) {
60 return step->is_assert() && step->get_property_id() == property_id &&
61 decision_procedure.get(step->cond_handle).is_false();
62 };
63}
64
66 const goto_tracet &goto_trace,
67 const namespacet &ns,
68 const trace_optionst &trace_options,
69 ui_message_handlert &ui_message_handler)
70{
71 messaget msg(ui_message_handler);
72 switch(ui_message_handler.get_ui())
73 {
75 msg.result() << "Counterexample:" << messaget::eom;
76 show_goto_trace(msg.result(), ns, goto_trace, trace_options);
77 msg.result() << messaget::eom;
78 break;
79
81 {
82 const goto_trace_stept &last_step = goto_trace.get_last_step();
83 property_infot info{
84 last_step.pc, last_step.comment, property_statust::FAIL};
85 xmlt xml_result = xml(last_step.property_id, info);
86 convert(ns, goto_trace, xml_result.new_element());
87 msg.result() << xml_result;
88 }
89 break;
90
92 {
93 json_stream_objectt &json_result =
94 ui_message_handler.get_json_stream().push_back_stream_object();
95 const goto_trace_stept &step = goto_trace.get_last_step();
96 json_result["property"] = json_stringt(step.property_id);
97 json_result["description"] = json_stringt(step.comment);
98 json_result["status"] = json_stringt("failed");
99 json_stream_arrayt &json_trace =
100 json_result.push_back_stream_array("trace");
101 convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
102 }
103 break;
104 }
105}
106
109 const goto_tracet &goto_trace,
110 const namespacet &ns,
111 const optionst &options)
112{
113 const std::string graphml = options.get_option("graphml-witness");
114 if(graphml.empty())
115 return;
116
117 graphml_witnesst graphml_witness(ns);
118 graphml_witness(goto_trace);
119
120 if(graphml == "-")
121 write_graphml(graphml_witness.graph(), std::cout);
122 else
123 {
124 std::ofstream out(graphml);
125 write_graphml(graphml_witness.graph(), out);
126 }
127}
128
131 const symex_target_equationt &symex_target_equation,
132 const namespacet &ns,
133 const optionst &options)
134{
135 const std::string graphml = options.get_option("graphml-witness");
136 if(graphml.empty())
137 return;
138
139 graphml_witnesst graphml_witness(ns);
140 graphml_witness(symex_target_equation);
141
142 if(graphml == "-")
143 write_graphml(graphml_witness.graph(), std::cout);
144 else
145 {
146 std::ofstream out(graphml);
147 write_graphml(graphml_witness.graph(), out);
148 }
149}
150
152 symex_target_equationt &equation,
153 decision_proceduret &decision_procedure,
154 message_handlert &message_handler)
155{
156 messaget msg(message_handler);
157 msg.status() << "converting SSA" << messaget::eom;
158
159 equation.convert(decision_procedure);
160}
161
162std::unique_ptr<memory_model_baset>
163get_memory_model(const optionst &options, const namespacet &ns)
164{
165 const std::string mm = options.get_option("mm");
166
167 if(mm.empty() || mm == "sc")
168 return util_make_unique<memory_model_sct>(ns);
169 else if(mm == "tso")
170 return util_make_unique<memory_model_tsot>(ns);
171 else if(mm == "pso")
172 return util_make_unique<memory_model_psot>(ns);
173 else
174 {
175 throw "invalid memory model '" + mm + "': use one of sc, tso, pso";
176 }
177}
178
180 symex_bmct &symex,
181 const namespacet &ns,
182 const optionst &options,
183 ui_message_handlert &ui_message_handler)
184{
185 messaget msg(ui_message_handler);
186 const symbolt *init_symbol;
188 symex.language_mode = init_symbol->mode;
189
190 msg.status() << "Starting Bounded Model Checking" << messaget::eom;
191
193
194 symex.unwindset.parse_unwind(options.get_option("unwind"));
196 options.get_list_option("unwindset"), ui_message_handler);
197}
198
199void slice(
200 symex_bmct &symex,
201 symex_target_equationt &symex_target_equation,
202 const namespacet &ns,
203 const optionst &options,
204 ui_message_handlert &ui_message_handler)
205{
206 messaget msg(ui_message_handler);
207
208 // any properties to check at all?
209 if(symex_target_equation.has_threads())
210 {
211 // we should build a thread-aware SSA slicer
212 msg.statistics() << "no slicing due to threads" << messaget::eom;
213 }
214 else
215 {
216 if(options.get_bool_option("slice-formula"))
217 {
218 ::slice(symex_target_equation);
219 msg.statistics() << "slicing removed "
220 << symex_target_equation.count_ignored_SSA_steps()
221 << " assignments" << messaget::eom;
222 }
223 else
224 {
225 if(options.get_bool_option("simple-slice"))
226 {
227 simple_slice(symex_target_equation);
228 msg.statistics() << "simple slicing removed "
229 << symex_target_equation.count_ignored_SSA_steps()
230 << " assignments" << messaget::eom;
231 }
232 }
233 }
234 msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
235 << symex.get_remaining_vccs()
236 << " remaining after simplification" << messaget::eom;
237}
238
240 propertiest &properties,
241 std::unordered_set<irep_idt> &updated_properties,
242 const symex_target_equationt &equation)
243{
244 for(const auto &step : equation.SSA_steps)
245 {
246 if(!step.is_assert())
247 continue;
248
249 irep_idt property_id = step.get_property_id();
250 CHECK_RETURN(!property_id.empty());
251
252 // Don't update status of properties that are constant 'false';
253 // we wouldn't have traces for them.
254 const auto status = step.cond_expr.is_true() ? property_statust::PASS
256 auto emplace_result = properties.emplace(
257 property_id, property_infot{step.source.pc, step.comment, status});
258
259 if(emplace_result.second)
260 {
261 updated_properties.insert(property_id);
262 }
263 else
264 {
265 property_infot &property_info = emplace_result.first->second;
266 property_statust old_status = property_info.status;
267 property_info.status |= status;
268
269 if(property_info.status != old_status)
270 updated_properties.insert(property_id);
271 }
272 }
273}
274
276 propertiest &properties,
277 std::unordered_set<irep_idt> &updated_properties)
278{
279 for(auto &property_pair : properties)
280 {
281 if(property_pair.second.status == property_statust::NOT_CHECKED)
282 {
283 // This could be a NOT_CHECKED, NOT_REACHABLE or PASS,
284 // but the equation doesn't give us precise information.
285 property_pair.second.status = property_statust::PASS;
286 updated_properties.insert(property_pair.first);
287 }
288 }
289}
290
292 propertiest &properties,
293 std::unordered_set<irep_idt> &updated_properties)
294{
295 for(auto &property_pair : properties)
296 {
297 if(property_pair.second.status == property_statust::UNKNOWN)
298 {
299 // This could have any status except NOT_CHECKED.
300 // We consider them PASS because we do verification modulo bounds.
301 property_pair.second.status = property_statust::PASS;
302 updated_properties.insert(property_pair.first);
303 }
304 }
305}
306
308 const std::string &cov_out,
309 const abstract_goto_modelt &goto_model,
310 const symex_bmct &symex,
311 ui_message_handlert &ui_message_handler)
312{
313 if(
314 !cov_out.empty() &&
315 symex.output_coverage_report(goto_model.get_goto_functions(), cov_out))
316 {
317 messaget log(ui_message_handler);
318 log.error() << "Failed to write symex coverage report to '" << cov_out
319 << "'" << messaget::eom;
320 }
321}
322
324 symex_bmct &symex,
325 symex_target_equationt &equation,
326 const optionst &options,
327 const namespacet &ns,
328 ui_message_handlert &ui_message_handler)
329{
330 const auto postprocess_equation_start = std::chrono::steady_clock::now();
331 // add a partial ordering, if required
332 if(equation.has_threads())
333 {
334 std::unique_ptr<memory_model_baset> memory_model =
335 get_memory_model(options, ns);
336 (*memory_model)(equation, ui_message_handler);
337 }
338
339 messaget log(ui_message_handler);
340 log.statistics() << "size of program expression: "
341 << equation.SSA_steps.size() << " steps" << messaget::eom;
342
343 slice(symex, equation, ns, options, ui_message_handler);
344
345 if(options.get_bool_option("validate-ssa-equation"))
346 {
348 }
349
350 const auto postprocess_equation_stop = std::chrono::steady_clock::now();
351 std::chrono::duration<double> postprocess_equation_runtime =
352 std::chrono::duration<double>(
353 postprocess_equation_stop - postprocess_equation_start);
354 log.status() << "Runtime Postprocess Equation: "
355 << postprocess_equation_runtime.count() << "s" << messaget::eom;
356}
357
358std::chrono::duration<double> prepare_property_decider(
359 propertiest &properties,
360 symex_target_equationt &equation,
361 goto_symex_property_decidert &property_decider,
362 ui_message_handlert &ui_message_handler)
363{
364 auto solver_start = std::chrono::steady_clock::now();
365
366 messaget log(ui_message_handler);
367 log.status()
368 << "Passing problem to "
369 << property_decider.get_decision_procedure().decision_procedure_text()
370 << messaget::eom;
371
373 equation, property_decider.get_decision_procedure(), ui_message_handler);
375 properties);
376 property_decider.convert_goals();
377
378 auto solver_stop = std::chrono::steady_clock::now();
379 return std::chrono::duration<double>(solver_stop - solver_start);
380}
381
384 propertiest &properties,
385 goto_symex_property_decidert &property_decider,
386 ui_message_handlert &ui_message_handler,
387 std::chrono::duration<double> solver_runtime,
388 bool set_pass)
389{
390 auto solver_start = std::chrono::steady_clock::now();
391
392 messaget log(ui_message_handler);
393 log.status()
394 << "Running "
395 << property_decider.get_decision_procedure().decision_procedure_text()
396 << messaget::eom;
397
398 property_decider.add_constraint_from_goals(
399 [&properties](const irep_idt &property_id) {
400 return is_property_to_check(properties.at(property_id).status);
401 });
402
403 auto const sat_solver_start = std::chrono::steady_clock::now();
404
405 decision_proceduret::resultt dec_result = property_decider.solve();
406
407 auto const sat_solver_stop = std::chrono::steady_clock::now();
408 std::chrono::duration<double> sat_solver_runtime =
409 std::chrono::duration<double>(sat_solver_stop - sat_solver_start);
410 log.status() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
411 << messaget::eom;
412
414 properties, result.updated_properties, dec_result, set_pass);
415
416 auto solver_stop = std::chrono::steady_clock::now();
417 solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
418 log.status() << "Runtime decision procedure: " << solver_runtime.count()
419 << "s" << messaget::eom;
420
422 {
424 }
425}
void run_property_decider(incremental_goto_checkert::resultt &result, propertiest &properties, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler, std::chrono::duration< double > solver_runtime, bool set_pass)
Runs the property decider to solve the equation.
Definition: bmc_util.cpp:382
void slice(symex_bmct &symex, symex_target_equationt &symex_target_equation, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:199
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:307
void output_error_trace(const goto_tracet &goto_trace, const namespacet &ns, const trace_optionst &trace_options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:65
std::chrono::duration< double > prepare_property_decider(propertiest &properties, symex_target_equationt &equation, goto_symex_property_decidert &property_decider, ui_message_handlert &ui_message_handler)
Converts the equation and sets up the property decider, but does not call solve.
Definition: bmc_util.cpp:358
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:291
void message_building_error_trace(messaget &log)
Outputs a message that an error trace is being built.
Definition: bmc_util.cpp:36
std::unique_ptr< memory_model_baset > get_memory_model(const optionst &options, const namespacet &ns)
Definition: bmc_util.cpp:163
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:239
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:275
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
void build_error_trace(goto_tracet &goto_trace, const namespacet &ns, const symex_target_equationt &symex_target_equation, const decision_proceduret &decision_procedure, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:41
void convert_symex_target_equation(symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
Definition: bmc_util.cpp:151
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
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:323
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:179
Bounded Model Checking Utilities.
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...
Traces of GOTO Programs.
std::function< bool(symex_target_equationt::SSA_stepst::const_iterator, const decision_proceduret &)> ssa_step_predicatet
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
Abstract interface to eager or lazy GOTO models.
virtual const goto_functionst & get_goto_functions() const =0
Accessor to get a raw goto_functionst.
resultt
Result of running the decision procedure.
virtual std::string decision_procedure_text() const =0
Return a textual description of the decision procedure.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool empty() const
Definition: dstring.h:88
Provides management of goal variables that encode properties.
decision_proceduret & get_decision_procedure() const
Returns the solver instance.
decision_proceduret::resultt solve()
Calls solve() on the solver instance.
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...
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.
void add_constraint_from_goals(std::function< bool(const irep_idt &property_id)> select_property)
Add disjunction of negated selected properties to the equation.
void convert_goals()
Convert the instances of a property into a goal variable.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
Definition: goto_symex.h:226
unsigned get_remaining_vccs() const
Definition: goto_symex.h:826
unsigned get_total_vccs() const
Definition: goto_symex.h:817
void validate(const validation_modet vm) const
Definition: goto_symex.h:835
Step of the trace of a GOTO program.
Definition: goto_trace.h:50
std::string comment
Definition: goto_trace.h:123
goto_programt::const_targett pc
Definition: goto_trace.h:112
irep_idt property_id
Definition: goto_trace.h:122
Trace of a GOTO program.
Definition: goto_trace.h:175
goto_trace_stept & get_last_step()
Retrieves the final step in the trace for manipulation (used to fill a trace from code,...
Definition: goto_trace.h:203
const graphmlt & graph()
void make_nil()
Definition: irep.h:454
Provides methods for streaming JSON arrays.
Definition: json_stream.h:93
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
Provides methods for streaming JSON objects.
Definition: json_stream.h:140
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & error() const
Definition: message.h:399
mstreamt & statistics() const
Definition: message.h:419
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
mstreamt & status() const
Definition: message.h:414
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:80
Symbol table entry.
Definition: symbol.h:28
unwindsett & unwindset
Definition: symex_bmc.h:85
source_locationt last_source_location
Definition: symex_bmc.h:36
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:75
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::size_t count_ignored_SSA_steps() const
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual uit get_ui() const
Definition: ui_message.h:33
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:40
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:22
void parse_unwindset(const std::list< std::string > &unwindset, message_handlert &message_handler)
Definition: unwindset.cpp:168
Definition: xml.h:21
xmlt & new_element(const std::string &key)
Definition: xml.h:95
Decision Procedure Interface.
Property Decider for Goto-Symex.
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Output the trace on the given stream out.
Definition: goto_trace.cpp:785
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:205
Witnesses for Traces and Proofs.
static std::unordered_set< irep_idt > init_symbol(const symbolt &sym, code_blockt &code_block, symbol_table_baset &symbol_table, const source_locationt &source_location, bool assume_init_pointers_not_null, const java_object_factory_parameterst &object_factory_parameters, const select_pointer_typet &pointer_type_selector, bool string_refinement_enabled, message_handlert &message_handler)
Traces of GOTO Programs.
Memory models for partial order concurrency.
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
Definition: properties.cpp:171
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:108
property_statust
The status of a property.
Definition: properties.h:26
@ UNKNOWN
The checker was unable to determine the status of the property.
@ PASS
The property was not violated.
@ FAIL
The property was violated.
@ NOT_CHECKED
The property was not checked (also used for initialization)
std::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:234
Slicer for symex traces.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define INITIALIZE_FUNCTION
std::unordered_set< irep_idt > updated_properties
Changed properties since the last call to incremental_goto_checkert::operator()
@ FOUND_FAIL
The goto checker may be able to find another FAILed property if operator() is called again.
property_statust status
The status of the property.
Definition: properties.h:72
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition: properties.h:66
Options for printing the trace using show_goto_trace.
Definition: goto_trace.h:219
Bounded Model Checking for ANSI-C.
Generate Equation using Symbolic Execution.
Traces of GOTO Programs.