CBMC
Loading...
Searching...
No Matches
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 <util/json_stream.h>
15#include <util/ui_message.h>
16
20
23#include <goto-symex/slice.h>
26
28#include "symex_bmc.h"
29
30#include <iostream>
31
33{
34 log.status() << "Building error trace" << messaget::eom;
35}
36
39 const namespacet &ns,
41 const decision_proceduret &decision_procedure,
42 ui_message_handlert &ui_message_handler)
43{
44 messaget log(ui_message_handler);
46
47 build_goto_trace(symex_target_equation, decision_procedure, ns, goto_trace);
48}
49
52{
53 return [property_id](
54 symex_target_equationt::SSA_stepst::const_iterator step,
55 const decision_proceduret &decision_procedure) {
56 return step->is_assert() && step->property_id == property_id &&
57 decision_procedure.get(step->cond_handle).is_false();
58 };
59}
60
63 const namespacet &ns,
65 ui_message_handlert &ui_message_handler)
66{
67 messaget msg(ui_message_handler);
68 switch(ui_message_handler.get_ui())
69 {
71 msg.result() << "Counterexample:" << messaget::eom;
73 msg.result() << messaget::eom;
74 break;
75
77 {
78 const goto_trace_stept &last_step = goto_trace.get_last_step();
81 xmlt xml_result = xml(last_step.property_id, info);
82 convert(ns, goto_trace, xml_result.new_element());
83 msg.result() << xml_result;
84 }
85 break;
86
88 {
90 ui_message_handler.get_json_stream().push_back_stream_object();
91 const goto_trace_stept &step = goto_trace.get_last_step();
92 json_result["property"] = json_stringt(step.property_id);
93 json_result["description"] = json_stringt(step.comment);
94 json_result["status"] = json_stringt("failed");
96 json_result.push_back_stream_array("trace");
98 }
99 break;
100 }
101}
102
105 const goto_tracet &goto_trace,
106 const namespacet &ns,
107 const optionst &options)
108{
109 const std::string graphml = options.get_option("graphml-witness");
110 if(graphml.empty())
111 return;
112
115
116 if(graphml == "-")
117 write_graphml(graphml_witness.graph(), std::cout);
118 else
119 {
120 std::ofstream out(graphml);
121 write_graphml(graphml_witness.graph(), out);
122 }
123}
124
128 const namespacet &ns,
129 const optionst &options)
130{
131 const std::string graphml = options.get_option("graphml-witness");
132 if(graphml.empty())
133 return;
134
137
138 if(graphml == "-")
139 write_graphml(graphml_witness.graph(), std::cout);
140 else
141 {
142 std::ofstream out(graphml);
143 write_graphml(graphml_witness.graph(), out);
144 }
145}
146
148 symex_target_equationt &equation,
149 decision_proceduret &decision_procedure,
150 message_handlert &message_handler)
151{
152 messaget msg(message_handler);
153 msg.status() << "converting SSA" << messaget::eom;
154
155 equation.convert(decision_procedure);
156}
157
158std::unique_ptr<memory_model_baset>
159get_memory_model(const optionst &options, const namespacet &ns)
160{
161 const std::string mm = options.get_option("mm");
162
163 if(mm.empty() || mm == "sc")
164 return std::make_unique<memory_model_sct>(ns);
165 else if(mm == "tso")
166 return std::make_unique<memory_model_tsot>(ns);
167 else if(mm == "pso")
168 return std::make_unique<memory_model_psot>(ns);
169 else
170 {
171 throw "invalid memory model '" + mm + "': use one of sc, tso, pso";
172 }
173}
174
175void slice(
176 symex_bmct &symex,
178 const namespacet &ns,
179 const optionst &options,
180 ui_message_handlert &ui_message_handler)
181{
182 messaget msg(ui_message_handler);
183
184 // any properties to check at all?
185 if(symex_target_equation.has_threads())
186 {
187 // we should build a thread-aware SSA slicer
188 msg.statistics() << "no slicing due to threads" << messaget::eom;
189 }
190 else
191 {
192 if(options.get_bool_option("slice-formula"))
193 {
195 msg.statistics() << "slicing removed "
196 << symex_target_equation.count_ignored_SSA_steps()
197 << " assignments" << messaget::eom;
198 }
199 else
200 {
201 if(options.get_bool_option("simple-slice"))
202 {
204 msg.statistics() << "simple slicing removed "
205 << symex_target_equation.count_ignored_SSA_steps()
206 << " assignments" << messaget::eom;
207 }
208 }
209 }
210 msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
211 << symex.get_remaining_vccs()
212 << " remaining after simplification" << messaget::eom;
213}
214
216 propertiest &properties,
217 std::unordered_set<irep_idt> &updated_properties,
218 const symex_target_equationt &equation)
219{
220 for(const auto &step : equation.SSA_steps)
221 {
222 if(!step.is_assert())
223 continue;
224
225 const irep_idt &property_id = step.property_id;
226 CHECK_RETURN(!property_id.empty());
227
228 // Don't update status of properties that are constant 'false';
229 // we wouldn't have traces for them.
230 const auto status = step.cond_expr.is_true() ? property_statust::PASS
232 auto emplace_result = properties.emplace(
233 property_id, property_infot{step.source.pc, step.comment, status});
234
235 if(emplace_result.second)
236 {
237 updated_properties.insert(property_id);
238 }
239 else
240 {
243 property_info.status |= status;
244
245 if(property_info.status != old_status)
246 updated_properties.insert(property_id);
247 }
248 }
249}
250
252 propertiest &properties,
253 std::unordered_set<irep_idt> &updated_properties)
254{
255 for(auto &property_pair : properties)
256 {
258 {
259 // This could be a NOT_CHECKED, NOT_REACHABLE or PASS,
260 // but the equation doesn't give us precise information.
262 updated_properties.insert(property_pair.first);
263 }
264 }
265}
266
268 propertiest &properties,
269 std::unordered_set<irep_idt> &updated_properties)
270{
271 for(auto &property_pair : properties)
272 {
273 if(property_pair.second.status == property_statust::UNKNOWN)
274 {
275 // This could have any status except NOT_CHECKED.
276 // We consider them PASS because we do verification modulo bounds.
278 updated_properties.insert(property_pair.first);
279 }
280 }
281}
282
284 const std::string &cov_out,
285 const abstract_goto_modelt &goto_model,
286 const symex_bmct &symex,
287 ui_message_handlert &ui_message_handler)
288{
289 if(
290 !cov_out.empty() &&
292 {
293 messaget log(ui_message_handler);
294 log.error() << "Failed to write symex coverage report to '" << cov_out
295 << "'" << messaget::eom;
296 }
297}
298
300 symex_bmct &symex,
301 symex_target_equationt &equation,
302 const optionst &options,
303 const namespacet &ns,
304 ui_message_handlert &ui_message_handler)
305{
306 const auto postprocess_equation_start = std::chrono::steady_clock::now();
307 // add a partial ordering, if required
308 if(equation.has_threads())
309 {
310 std::unique_ptr<memory_model_baset> memory_model =
311 get_memory_model(options, ns);
312 (*memory_model)(equation, ui_message_handler);
313 }
314
315 messaget log(ui_message_handler);
316 log.statistics() << "size of program expression: "
317 << equation.SSA_steps.size() << " steps" << messaget::eom;
318
319 slice(symex, equation, ns, options, ui_message_handler);
320
321 if(options.get_bool_option("validate-ssa-equation"))
322 {
324 }
325
326 const auto postprocess_equation_stop = std::chrono::steady_clock::now();
327 std::chrono::duration<double> postprocess_equation_runtime =
328 std::chrono::duration<double>(
330 log.statistics() << "Runtime Postprocess Equation: "
331 << postprocess_equation_runtime.count() << "s"
332 << messaget::eom;
333}
334
335std::chrono::duration<double> prepare_property_decider(
336 propertiest &properties,
337 symex_target_equationt &equation,
338 goto_symex_property_decidert &property_decider,
339 ui_message_handlert &ui_message_handler)
340{
341 auto solver_start = std::chrono::steady_clock::now();
342
343 messaget log(ui_message_handler);
344 log.status()
345 << "Passing problem to "
346 << property_decider.get_decision_procedure().decision_procedure_text()
347 << messaget::eom;
348
350 equation, property_decider.get_decision_procedure(), ui_message_handler);
352 properties);
353 property_decider.convert_goals();
354
355 auto solver_stop = std::chrono::steady_clock::now();
356 return std::chrono::duration<double>(solver_stop - solver_start);
357}
358
361 propertiest &properties,
362 goto_symex_property_decidert &property_decider,
363 ui_message_handlert &ui_message_handler,
364 std::chrono::duration<double> solver_runtime,
365 bool set_pass)
366{
367 auto solver_start = std::chrono::steady_clock::now();
368
369 messaget log(ui_message_handler);
370 log.status()
371 << "Running "
372 << property_decider.get_decision_procedure().decision_procedure_text()
373 << messaget::eom;
374
375 property_decider.add_constraint_from_goals(
376 [&properties](const irep_idt &property_id) {
377 return is_property_to_check(properties.at(property_id).status);
378 });
379
380 auto const sat_solver_start = std::chrono::steady_clock::now();
381
382 decision_proceduret::resultt dec_result = property_decider.solve();
383
384 auto const sat_solver_stop = std::chrono::steady_clock::now();
385 std::chrono::duration<double> sat_solver_runtime =
386 std::chrono::duration<double>(sat_solver_stop - sat_solver_start);
387 log.statistics() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
388 << messaget::eom;
389
391 properties, result.updated_properties, dec_result, set_pass);
392
393 auto solver_stop = std::chrono::steady_clock::now();
394 solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
395 log.statistics() << "Runtime decision procedure: " << solver_runtime.count()
396 << "s" << messaget::eom;
397
399 {
401 }
402}
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:359
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:175
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:283
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:61
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:335
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:267
void message_building_error_trace(messaget &log)
Outputs a message that an error trace is being built.
Definition bmc_util.cpp:32
std::unique_ptr< memory_model_baset > get_memory_model(const optionst &options, const namespacet &ns)
Definition bmc_util.cpp:159
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:215
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:251
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:51
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:37
void convert_symex_target_equation(symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
Definition bmc_util.cpp:147
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:104
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:299
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_table_baset &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.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
An interface for a decision procedure for satisfiability problems.
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:38
bool empty() const
Definition dstring.h:89
Provides management of goal variables that encode properties.
stack_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.
unsigned get_remaining_vccs() const
Definition goto_symex.h:849
unsigned get_total_vccs() const
Definition goto_symex.h:840
void validate(const validation_modet vm) const
Definition goto_symex.h:858
Step of the trace of a GOTO program.
Definition goto_trace.h:50
std::string comment
Definition goto_trace.h:124
irep_idt property_id
Definition goto_trace.h:123
Trace of a GOTO program.
Definition goto_trace.h:177
Provides methods for streaming JSON arrays.
Definition json_stream.h:93
Provides methods for streaming JSON objects.
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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
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 ...
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
Definition xml.h:21
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.
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition graphml.cpp:203
Witnesses for Traces and Proofs.
Traces of GOTO Programs.
double log(double x)
Definition math.c:2449
Memory models for partial order concurrency.
bool is_property_to_check(property_statust status)
Return true if the status is NOT_CHECKED or UNKNOWN.
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
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
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.
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:221
Bounded Model Checking for ANSI-C.
Generate Equation using Symbolic Execution.
Traces of GOTO Programs.