cprover
bmc_util.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Bounded Model Checking Utilities
4 
5 Author: Daniel Kroening, Peter Schrammel
6 
7 \*******************************************************************/
8 
11 
12 #include "bmc_util.h"
13 
14 #include <fstream>
15 #include <iostream>
16 
20 
23 #include <goto-symex/slice.h>
25 
27 
29 
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  xmlt xml;
83  convert(ns, goto_trace, xml);
84  msg.status() << xml;
85  }
86  break;
87 
89  {
90  json_stream_objectt &json_result =
91  ui_message_handler.get_json_stream().push_back_stream_object();
92  const goto_trace_stept &step = goto_trace.steps.back();
93  json_result["property"] =
94  json_stringt(step.pc->source_location.get_property_id());
95  json_result["description"] =
96  json_stringt(step.pc->source_location.get_comment());
97  json_result["status"] = json_stringt("failed");
98  json_stream_arrayt &json_trace =
99  json_result.push_back_stream_array("trace");
100  convert<json_stream_arrayt>(ns, goto_trace, json_trace, trace_options);
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 
116  graphml_witnesst graphml_witness(ns);
117  graphml_witness(goto_trace);
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 
130  const symex_target_equationt &symex_target_equation,
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 
138  graphml_witnesst graphml_witness(ns);
139  graphml_witness(symex_target_equation);
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 
161 std::unique_ptr<memory_model_baset>
162 get_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 util_make_unique<memory_model_sct>(ns);
168  else if(mm == "tso")
169  return util_make_unique<memory_model_tsot>(ns);
170  else if(mm == "pso")
171  return util_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  const optionst &options,
182  ui_message_handlert &ui_message_handler)
183 {
184  messaget msg(ui_message_handler);
185  const symbolt *init_symbol;
186  if(!ns.lookup(INITIALIZE_FUNCTION, init_symbol))
187  symex.language_mode = init_symbol->mode;
188 
189  msg.status() << "Starting Bounded Model Checking" << messaget::eom;
190 
192 
193  symex.unwindset.parse_unwind(options.get_option("unwind"));
194  symex.unwindset.parse_unwindset(options.get_list_option("unwindset"));
195 }
196 
197 void slice(
198  symex_bmct &symex,
199  symex_target_equationt &symex_target_equation,
200  const namespacet &ns,
201  const optionst &options,
202  ui_message_handlert &ui_message_handler)
203 {
204  messaget msg(ui_message_handler);
205 
206  // any properties to check at all?
207  if(symex_target_equation.has_threads())
208  {
209  // we should build a thread-aware SSA slicer
210  msg.statistics() << "no slicing due to threads" << messaget::eom;
211  }
212  else
213  {
214  if(options.get_bool_option("slice-formula"))
215  {
216  ::slice(symex_target_equation);
217  msg.statistics() << "slicing removed "
218  << symex_target_equation.count_ignored_SSA_steps()
219  << " assignments" << messaget::eom;
220  }
221  else
222  {
223  if(options.get_bool_option("simple-slice"))
224  {
225  simple_slice(symex_target_equation);
226  msg.statistics() << "simple slicing removed "
227  << symex_target_equation.count_ignored_SSA_steps()
228  << " assignments" << messaget::eom;
229  }
230  }
231  }
232  msg.statistics() << "Generated " << symex.get_total_vccs() << " VCC(s), "
233  << symex.get_remaining_vccs()
234  << " remaining after simplification" << messaget::eom;
235 }
236 
238  propertiest &properties,
239  std::unordered_set<irep_idt> &updated_properties,
240  const symex_target_equationt &equation)
241 {
242  for(const auto &step : equation.SSA_steps)
243  {
244  if(!step.is_assert())
245  continue;
246 
247  irep_idt property_id = step.get_property_id();
248  CHECK_RETURN(!property_id.empty());
249 
250  // Don't update status of properties that are constant 'false';
251  // we wouldn't have traces for them.
252  const auto status = step.cond_expr.is_true() ? property_statust::PASS
254  auto emplace_result = properties.emplace(
255  property_id, property_infot{step.source.pc, step.comment, status});
256 
257  if(emplace_result.second)
258  {
259  updated_properties.insert(property_id);
260  }
261  else
262  {
263  property_infot &property_info = emplace_result.first->second;
264  property_statust old_status = property_info.status;
265  property_info.status |= status;
266 
267  if(property_info.status != old_status)
268  updated_properties.insert(property_id);
269  }
270  }
271 }
272 
274  propertiest &properties,
275  std::unordered_set<irep_idt> &updated_properties)
276 {
277  for(auto &property_pair : properties)
278  {
279  if(property_pair.second.status == property_statust::NOT_CHECKED)
280  {
281  // This could be a NOT_CHECKED, NOT_REACHABLE or PASS,
282  // but the equation doesn't give us precise information.
283  property_pair.second.status = property_statust::PASS;
284  updated_properties.insert(property_pair.first);
285  }
286  }
287 }
288 
290  propertiest &properties,
291  std::unordered_set<irep_idt> &updated_properties)
292 {
293  for(auto &property_pair : properties)
294  {
295  if(property_pair.second.status == property_statust::UNKNOWN)
296  {
297  // This could have any status except NOT_CHECKED.
298  // We consider them PASS because we do verification modulo bounds.
299  property_pair.second.status = property_statust::PASS;
300  updated_properties.insert(property_pair.first);
301  }
302  }
303 }
304 
306  const std::string &cov_out,
307  const abstract_goto_modelt &goto_model,
308  const symex_bmct &symex,
309  ui_message_handlert &ui_message_handler)
310 {
311  if(
312  !cov_out.empty() &&
313  symex.output_coverage_report(goto_model.get_goto_functions(), cov_out))
314  {
315  messaget log(ui_message_handler);
316  log.error() << "Failed to write symex coverage report to '" << cov_out
317  << "'" << messaget::eom;
318  }
319 }
320 
322  symex_bmct &symex,
323  symex_target_equationt &equation,
324  const optionst &options,
325  const namespacet &ns,
326  ui_message_handlert &ui_message_handler)
327 {
328  const auto postprocess_equation_start = std::chrono::steady_clock::now();
329  // add a partial ordering, if required
330  if(equation.has_threads())
331  {
332  std::unique_ptr<memory_model_baset> memory_model =
333  get_memory_model(options, ns);
334  (*memory_model)(equation, ui_message_handler);
335  }
336 
337  messaget log(ui_message_handler);
338  log.statistics() << "size of program expression: "
339  << equation.SSA_steps.size() << " steps" << messaget::eom;
340 
341  slice(symex, equation, ns, options, ui_message_handler);
342 
343  if(options.get_bool_option("validate-ssa-equation"))
344  {
346  }
347 
348  const auto postprocess_equation_stop = std::chrono::steady_clock::now();
349  std::chrono::duration<double> postprocess_equation_runtime =
350  std::chrono::duration<double>(
351  postprocess_equation_stop - postprocess_equation_start);
352  log.status() << "Runtime Postprocess Equation: "
353  << postprocess_equation_runtime.count() << "s" << messaget::eom;
354 }
355 
356 std::chrono::duration<double> prepare_property_decider(
357  propertiest &properties,
358  symex_target_equationt &equation,
359  goto_symex_property_decidert &property_decider,
360  ui_message_handlert &ui_message_handler)
361 {
362  auto solver_start = std::chrono::steady_clock::now();
363 
364  messaget log(ui_message_handler);
365  log.status()
366  << "Passing problem to "
367  << property_decider.get_decision_procedure().decision_procedure_text()
368  << messaget::eom;
369 
371  equation, property_decider.get_decision_procedure(), ui_message_handler);
373  properties);
374  property_decider.convert_goals();
375 
376  auto solver_stop = std::chrono::steady_clock::now();
377  return std::chrono::duration<double>(solver_stop - solver_start);
378 }
379 
382  propertiest &properties,
383  goto_symex_property_decidert &property_decider,
384  ui_message_handlert &ui_message_handler,
385  std::chrono::duration<double> solver_runtime,
386  bool set_pass)
387 {
388  auto solver_start = std::chrono::steady_clock::now();
389 
390  messaget log(ui_message_handler);
391  log.status()
392  << "Running "
393  << property_decider.get_decision_procedure().decision_procedure_text()
394  << messaget::eom;
395 
396  property_decider.add_constraint_from_goals(
397  [&properties](const irep_idt &property_id) {
398  return is_property_to_check(properties.at(property_id).status);
399  });
400 
401  auto const sat_solver_start = std::chrono::steady_clock::now();
402 
403  decision_proceduret::resultt dec_result = property_decider.solve();
404 
405  auto const sat_solver_stop = std::chrono::steady_clock::now();
406  std::chrono::duration<double> sat_solver_runtime =
407  std::chrono::duration<double>(sat_solver_stop - sat_solver_start);
408  log.status() << "Runtime Solver: " << sat_solver_runtime.count() << "s"
409  << messaget::eom;
410 
411  property_decider.update_properties_status_from_goals(
412  properties, result.updated_properties, dec_result, set_pass);
413 
414  auto solver_stop = std::chrono::steady_clock::now();
415  solver_runtime += std::chrono::duration<double>(solver_stop - solver_start);
416  log.status() << "Runtime decision procedure: " << solver_runtime.count()
417  << "s" << messaget::eom;
418 
420  {
422  }
423 }
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:380
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:356
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:197
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:305
std::unique_ptr< memory_model_baset > get_memory_model(const optionst &options, const namespacet &ns)
Definition: bmc_util.cpp:162
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
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:289
void message_building_error_trace(messaget &log)
Outputs a message that an error trace is being built.
Definition: bmc_util.cpp:36
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:237
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:273
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: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:321
void setup_symex(symex_bmct &symex, const namespacet &ns, const optionst &options, ui_message_handlert &ui_message_handler)
Definition: bmc_util.cpp:178
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:239
unsigned get_remaining_vccs() const
Definition: goto_symex.h:835
unsigned get_total_vccs() const
Definition: goto_symex.h:826
void validate(const validation_modet vm) const
Definition: goto_symex.h:844
Step of the trace of a GOTO program.
Definition: goto_trace.h:52
goto_programt::const_targett pc
Definition: goto_trace.h:114
Trace of a GOTO program.
Definition: goto_trace.h:177
stepst steps
Definition: goto_trace.h:180
const graphmlt & graph()
void make_nil()
Definition: irep.h:464
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 & status() const
Definition: message.h:414
mstreamt & result() const
Definition: message.h:409
static eomt eom
Definition: message.h:297
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
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
irep_idt mode
Language mode.
Definition: symbol.h:49
unwindsett unwindset
Definition: symex_bmc.h:86
source_locationt last_source_location
Definition: symex_bmc.h:37
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:76
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:31
virtual json_stream_arrayt & get_json_stream()
Definition: ui_message.h:38
void parse_unwind(const std::string &unwind)
Definition: unwindset.cpp:18
void parse_unwindset(const std::list< std::string > &unwindset)
Definition: unwindset.cpp:57
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.
Definition: goto_trace.cpp:782
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:208
Witnesses for Traces and Proofs.
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:168
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
property_statust
The status of a property.
Definition: properties.h:25
@ UNKNOWN
The checker was unable to determine the status of the property.
@ PASS
The property was not violated.
@ NOT_CHECKED
The property was not checked (also used for initialization)
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:237
Slicer for symex traces.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
#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:71
goto_programt::const_targett pc
A pointer to the corresponding goto instruction.
Definition: properties.h:65
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.