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 <iostream>
15
19
22#include <goto-symex/slice.h>
24
26
28
29#include <util/json_stream.h>
30#include <util/ui_message.h>
31
33#include "symex_bmc.h"
34
36{
37 log.status() << "Building error trace" << messaget::eom;
38}
39
42 const namespacet &ns,
44 const decision_proceduret &decision_procedure,
45 ui_message_handlert &ui_message_handler)
46{
47 messaget log(ui_message_handler);
49
50 build_goto_trace(symex_target_equation, decision_procedure, ns, goto_trace);
51}
52
55{
56 return [property_id](
57 symex_target_equationt::SSA_stepst::const_iterator step,
58 const decision_proceduret &decision_procedure) {
59 return step->is_assert() && step->property_id == property_id &&
60 decision_procedure.get(step->cond_handle).is_false();
61 };
62}
63
66 const namespacet &ns,
68 ui_message_handlert &ui_message_handler)
69{
70 messaget msg(ui_message_handler);
71 switch(ui_message_handler.get_ui())
72 {
74 msg.result() << "Counterexample:" << messaget::eom;
76 msg.result() << messaget::eom;
77 break;
78
80 {
81 const goto_trace_stept &last_step = goto_trace.get_last_step();
84 xmlt xml_result = xml(last_step.property_id, info);
85 convert(ns, goto_trace, xml_result.new_element());
86 msg.result() << xml_result;
87 }
88 break;
89
91 {
93 ui_message_handler.get_json_stream().push_back_stream_object();
94 const goto_trace_stept &step = goto_trace.get_last_step();
95 json_result["property"] = json_stringt(step.property_id);
96 json_result["description"] = json_stringt(step.comment);
97 json_result["status"] = json_stringt("failed");
99 json_result.push_back_stream_array("trace");
101 }
102 break;
103 }
104}
105
108 const goto_tracet &goto_trace,
109 const namespacet &ns,
110 const optionst &options)
111{
112 const std::string graphml = options.get_option("graphml-witness");
113 if(graphml.empty())
114 return;
115
118
119 if(graphml == "-")
120 write_graphml(graphml_witness.graph(), std::cout);
121 else
122 {
123 std::ofstream out(graphml);
124 write_graphml(graphml_witness.graph(), out);
125 }
126}
127
131 const namespacet &ns,
132 const optionst &options)
133{
134 const std::string graphml = options.get_option("graphml-witness");
135 if(graphml.empty())
136 return;
137
140
141 if(graphml == "-")
142 write_graphml(graphml_witness.graph(), std::cout);
143 else
144 {
145 std::ofstream out(graphml);
146 write_graphml(graphml_witness.graph(), out);
147 }
148}
149
151 symex_target_equationt &equation,
152 decision_proceduret &decision_procedure,
153 message_handlert &message_handler)
154{
155 messaget msg(message_handler);
156 msg.status() << "converting SSA" << messaget::eom;
157
158 equation.convert(decision_procedure);
159}
160
161std::unique_ptr<memory_model_baset>
162get_memory_model(const optionst &options, const namespacet &ns)
163{
164 const std::string mm = options.get_option("mm");
165
166 if(mm.empty() || mm == "sc")
167 return std::make_unique<memory_model_sct>(ns);
168 else if(mm == "tso")
169 return std::make_unique<memory_model_tsot>(ns);
170 else if(mm == "pso")
171 return std::make_unique<memory_model_psot>(ns);
172 else
173 {
174 throw "invalid memory model '" + mm + "': use one of sc, tso, pso";
175 }
176}
177
179 symex_bmct &symex,
180 const namespacet &ns,
181 ui_message_handlert &ui_message_handler)
182{
183 messaget msg(ui_message_handler);
184 const symbolt *init_symbol;
186 symex.language_mode = init_symbol->mode;
187
188 msg.status() << "Starting Bounded Model Checking" << messaget::eom;
189
191}
192
193void slice(
194 symex_bmct &symex,
196 const namespacet &ns,
197 const optionst &options,
198 ui_message_handlert &ui_message_handler)
199{
200 messaget msg(ui_message_handler);
201
202 // any properties to check at all?
203 if(symex_target_equation.has_threads())
204 {
205 // we should build a thread-aware SSA slicer
206 msg.statistics() << "no slicing due to threads" << messaget::eom;
207 }
208 else
209 {
210 if(options.get_bool_option("slice-formula"))
211 {
213 msg.statistics() << "slicing removed "
214 << symex_target_equation.count_ignored_SSA_steps()
215 << " assignments" << messaget::eom;
216 }
217 else
218 {
219 if(options.get_bool_option("simple-slice"))
220 {
222 msg.statistics() << "simple slicing removed "
223 << symex_target_equation.count_ignored_SSA_steps()
224 << " assignments" << messaget::eom;
225 }
226 }
227 }
228 msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
229 << symex.get_remaining_vccs()
230 << " remaining after simplification" << messaget::eom;
231}
232
234 propertiest &properties,
235 std::unordered_set<irep_idt> &updated_properties,
236 const symex_target_equationt &equation)
237{
238 for(const auto &step : equation.SSA_steps)
239 {
240 if(!step.is_assert())
241 continue;
242
243 const irep_idt &property_id = step.property_id;
244 CHECK_RETURN(!property_id.empty());
245
246 // Don't update status of properties that are constant 'false';
247 // we wouldn't have traces for them.
248 const auto status = step.cond_expr.is_true() ? property_statust::PASS
250 auto emplace_result = properties.emplace(
251 property_id, property_infot{step.source.pc, step.comment, status});
252
253 if(emplace_result.second)
254 {
255 updated_properties.insert(property_id);
256 }
257 else
258 {
261 property_info.status |= status;
262
263 if(property_info.status != old_status)
264 updated_properties.insert(property_id);
265 }
266 }
267}
268
270 propertiest &properties,
271 std::unordered_set<irep_idt> &updated_properties)
272{
273 for(auto &property_pair : properties)
274 {
276 {
277 // This could be a NOT_CHECKED, NOT_REACHABLE or PASS,
278 // but the equation doesn't give us precise information.
280 updated_properties.insert(property_pair.first);
281 }
282 }
283}
284
286 propertiest &properties,
287 std::unordered_set<irep_idt> &updated_properties)
288{
289 for(auto &property_pair : properties)
290 {
291 if(property_pair.second.status == property_statust::UNKNOWN)
292 {
293 // This could have any status except NOT_CHECKED.
294 // We consider them PASS because we do verification modulo bounds.
296 updated_properties.insert(property_pair.first);
297 }
298 }
299}
300
302 const std::string &cov_out,
303 const abstract_goto_modelt &goto_model,
304 const symex_bmct &symex,
305 ui_message_handlert &ui_message_handler)
306{
307 if(
308 !cov_out.empty() &&
310 {
311 messaget log(ui_message_handler);
312 log.error() << "Failed to write symex coverage report to '" << cov_out
313 << "'" << messaget::eom;
314 }
315}
316
318 symex_bmct &symex,
319 symex_target_equationt &equation,
320 const optionst &options,
321 const namespacet &ns,
322 ui_message_handlert &ui_message_handler)
323{
324 const auto postprocess_equation_start = std::chrono::steady_clock::now();
325 // add a partial ordering, if required
326 if(equation.has_threads())
327 {
328 std::unique_ptr<memory_model_baset> memory_model =
329 get_memory_model(options, ns);
330 (*memory_model)(equation, ui_message_handler);
331 }
332
333 messaget log(ui_message_handler);
334 log.statistics() << "size of program expression: "
335 << equation.SSA_steps.size() << " steps" << messaget::eom;
336
337 slice(symex, equation, ns, options, ui_message_handler);
338
339 if(options.get_bool_option("validate-ssa-equation"))
340 {
342 }
343
344 const auto postprocess_equation_stop = std::chrono::steady_clock::now();
345 std::chrono::duration<double> postprocess_equation_runtime =
346 std::chrono::duration<double>(
348 log.statistics() << "Runtime Postprocess Equation: "
349 << postprocess_equation_runtime.count() << "s"
350 << messaget::eom;
351}
352
353std::chrono::duration<double> prepare_property_decider(
354 propertiest &properties,
355 symex_target_equationt &equation,
356 goto_symex_property_decidert &property_decider,
357 ui_message_handlert &ui_message_handler)
358{
359 auto solver_start = std::chrono::steady_clock::now();
360
361 messaget log(ui_message_handler);
362 log.status()
363 << "Passing problem to "
364 << property_decider.get_decision_procedure().decision_procedure_text()
365 << messaget::eom;
366
368 equation, property_decider.get_decision_procedure(), ui_message_handler);
370 properties);
371 property_decider.convert_goals();
372
373 auto solver_stop = std::chrono::steady_clock::now();
374 return std::chrono::duration<double>(solver_stop - solver_start);
375}
376
379 propertiest &properties,
380 goto_symex_property_decidert &property_decider,
381 ui_message_handlert &ui_message_handler,
382 std::chrono::duration<double> solver_runtime,
383 bool set_pass)
384{
385 auto solver_start = std::chrono::steady_clock::now();
386
387 messaget log(ui_message_handler);
388 log.status()
389 << "Running "
390 << property_decider.get_decision_procedure().decision_procedure_text()
391 << messaget::eom;
392
393 property_decider.add_constraint_from_goals(
394 [&properties](const irep_idt &property_id) {
395 return is_property_to_check(properties.at(property_id).status);
396 });
397
398 auto const sat_solver_start = std::chrono::steady_clock::now();
399
400 decision_proceduret::resultt dec_result = property_decider.solve();
401
402 auto const sat_solver_stop = std::chrono::steady_clock::now();
403 std::chrono::duration<double> sat_solver_runtime =
404 std::chrono::duration<double>(sat_solver_stop - sat_solver_start);
405 log.statistics() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
406 << messaget::eom;
407
409 properties, result.updated_properties, dec_result, set_pass);
410
411 auto solver_stop = std::chrono::steady_clock::now();
412 solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
413 log.statistics() << "Runtime decision procedure: " << solver_runtime.count()
414 << "s" << messaget::eom;
415
417 {
419 }
420}
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:377
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:193
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:301
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:64
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:353
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:285
void message_building_error_trace(messaget &log)
Outputs a message that an error trace is being built.
Definition bmc_util.cpp:35
std::unique_ptr< memory_model_baset > get_memory_model(const optionst &options, const namespacet &ns)
Definition bmc_util.cpp:162
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:233
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:269
void setup_symex(symex_bmct &symex, const namespacet &ns, ui_message_handlert &ui_message_handler)
Definition bmc_util.cpp:178
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:54
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:40
void convert_symex_target_equation(symex_target_equationt &equation, decision_proceduret &decision_procedure, message_handlert &message_handler)
Definition bmc_util.cpp:150
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
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:317
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.
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:242
unsigned get_remaining_vccs() const
Definition goto_symex.h:852
unsigned get_total_vccs() const
Definition goto_symex.h:843
void validate(const validation_modet vm) const
Definition goto_symex.h:861
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
void make_nil()
Definition irep.h:446
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 lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
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
Symbol table entry.
Definition symbol.h:28
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 ...
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.
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.
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
#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.
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.