cprover
bmc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution of ANSI-C
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "bmc.h"
13 
14 #include <fstream>
15 #include <iostream>
16 #include <memory>
17 
18 #include <util/string2int.h>
19 #include <util/source_location.h>
20 #include <util/string_utils.h>
21 #include <util/time_stopping.h>
22 #include <util/message.h>
23 #include <util/json.h>
24 #include <util/cprover_prefix.h>
25 
26 #include <langapi/mode.h>
27 #include <langapi/languages.h>
28 #include <langapi/language_util.h>
29 
30 #include <ansi-c/ansi_c_language.h>
31 
35 
37 #include <goto-symex/slice.h>
42 
44 #include "fault_localization.h"
45 
47 {
48  // this is a hook for hw-cbmc
49 }
50 
52 {
53  status() << "Building error trace" << eom;
54 
56  build_goto_trace(equation, prop_conv, ns, goto_trace);
57 
58  switch(ui)
59  {
61  std::cout << "\n" << "Counterexample:" << "\n";
62  show_goto_trace(std::cout, ns, goto_trace);
63  break;
64 
66  {
67  xmlt xml;
68  convert(ns, goto_trace, xml);
69  std::cout << xml << "\n";
70  }
71  break;
72 
74  {
75  json_objectt json_result;
76  json_arrayt &result_array=json_result["results"].make_array();
77  json_objectt &result=result_array.push_back().make_object();
78  const goto_trace_stept &step=goto_trace.steps.back();
79  result["property"]=
80  json_stringt(id2string(step.pc->source_location.get_property_id()));
81  result["description"]=
82  json_stringt(id2string(step.pc->source_location.get_comment()));
83  result["status"]=json_stringt("failed");
84  jsont &json_trace=result["trace"];
85  convert(ns, goto_trace, json_trace);
86  std::cout << ",\n" << json_result;
87  }
88  break;
89  }
90 }
91 
94  resultt result,
95  const goto_functionst &goto_functions)
96 {
97  const std::string graphml=options.get_option("graphml-witness");
98  if(graphml.empty())
99  return;
100 
101  graphml_witnesst graphml_witness(ns);
103  graphml_witness(safety_checkert::error_trace);
104  else if(result==resultt::SAFE)
105  graphml_witness(equation);
106  else
107  return;
108 
109  if(graphml=="-")
110  write_graphml(graphml_witness.graph(), std::cout);
111  else
112  {
113  std::ofstream out(graphml);
114  write_graphml(graphml_witness.graph(), out);
115  }
116 }
117 
119 {
120  // convert HDL (hook for hw-cbmc)
122 
123  status() << "converting SSA" << eom;
124 
125  // convert SSA
127 
128  // the 'extra constraints'
129  if(!bmc_constraints.empty())
130  {
131  status() << "converting constraints" << eom;
132 
134  prop_conv.set_to_true(*it);
135  }
136 }
137 
140 {
141  status() << "Passing problem to "
143 
145 
146  // stop the time
147  absolute_timet sat_start=current_time();
148 
149  do_conversion();
150 
151  status() << "Running " << prop_conv.decision_procedure_text() << eom;
152 
154  // output runtime
155 
156  {
157  absolute_timet sat_stop=current_time();
158  status() << "Runtime decision procedure: "
159  << (sat_stop-sat_start) << "s" << eom;
160  }
161 
162  return dec_result;
163 }
164 
166 {
167  result() << "VERIFICATION SUCCESSFUL" << eom;
168 
169  switch(ui)
170  {
172  break;
173 
175  {
176  xmlt xml("cprover-status");
177  xml.data="SUCCESS";
178  std::cout << xml;
179  std::cout << "\n";
180  }
181  break;
182 
184  {
185  json_objectt json_result;
186  json_result["cProverStatus"]=json_stringt("success");
187  std::cout << ",\n" << json_result;
188  }
189  break;
190  }
191 }
192 
194 {
195  result() << "VERIFICATION FAILED" << eom;
196 
197  switch(ui)
198  {
200  break;
201 
203  {
204  xmlt xml("cprover-status");
205  xml.data="FAILURE";
206  std::cout << xml;
207  std::cout << "\n";
208  }
209  break;
210 
212  {
213  json_objectt json_result;
214  json_result["cProverStatus"]=json_stringt("failure");
215  std::cout << ",\n" << json_result;
216  }
217  break;
218  }
219 }
220 
222 {
223  unsigned count=1;
224 
226 
227  std::cout << "\n" << "Program constraints:" << "\n";
228 
229  for(const auto &step : equation.SSA_steps)
230  {
231  std::cout << "// " << step.source.pc->location_number << " ";
232  std::cout << step.source.pc->source_location.as_string() << "\n";
233 
234  if(step.is_assignment())
235  {
236  std::string string_value;
237  languages.from_expr(step.cond_expr, string_value);
238  std::cout << "(" << count << ") " << string_value << "\n";
239 
240  if(!step.guard.is_true())
241  {
242  languages.from_expr(step.guard, string_value);
243  std::cout << std::string(std::to_string(count).size()+3, ' ');
244  std::cout << "guard: " << string_value << "\n";
245  }
246 
247  count++;
248  }
249  else if(step.is_assert())
250  {
251  std::string string_value;
252  languages.from_expr(step.cond_expr, string_value);
253  std::cout << "(" << count << ") ASSERT("
254  << string_value <<") " << "\n";
255 
256  if(!step.guard.is_true())
257  {
258  languages.from_expr(step.guard, string_value);
259  std::cout << std::string(std::to_string(count).size()+3, ' ');
260  std::cout << "guard: " << string_value << "\n";
261  }
262 
263  count++;
264  }
265  else if(step.is_assume())
266  {
267  std::string string_value;
268  languages.from_expr(step.cond_expr, string_value);
269  std::cout << "(" << count << ") ASSUME("
270  << string_value <<") " << "\n";
271 
272  if(!step.guard.is_true())
273  {
274  languages.from_expr(step.guard, string_value);
275  std::cout << std::string(std::to_string(count).size()+3, ' ');
276  std::cout << "guard: " << string_value << "\n";
277  }
278 
279  count++;
280  }
281  else if(step.is_constraint())
282  {
283  std::string string_value;
284  languages.from_expr(step.cond_expr, string_value);
285  std::cout << "(" << count << ") CONSTRAINT("
286  << string_value <<") " << "\n";
287 
288  count++;
289  }
290  else if(step.is_shared_read() || step.is_shared_write())
291  {
292  std::string string_value;
293  languages.from_expr(step.ssa_lhs, string_value);
294  std::cout << "(" << count << ") SHARED_"
295  << (step.is_shared_write()?"WRITE":"READ")
296  << "(" << string_value <<")\n";
297 
298  if(!step.guard.is_true())
299  {
300  languages.from_expr(step.guard, string_value);
301  std::cout << std::string(std::to_string(count).size()+3, ' ');
302  std::cout << "guard: " << string_value << "\n";
303  }
304 
305  count++;
306  }
307  }
308 }
309 
311  const goto_functionst &goto_functions)
312 {
313  const std::string mm=options.get_option("mm");
314  std::unique_ptr<memory_model_baset> memory_model;
315 
316  if(mm.empty() || mm=="sc")
317  memory_model=std::unique_ptr<memory_model_baset>(new memory_model_sct(ns));
318  else if(mm=="tso")
319  memory_model=std::unique_ptr<memory_model_baset>(new memory_model_tsot(ns));
320  else if(mm=="pso")
321  memory_model=std::unique_ptr<memory_model_baset>(new memory_model_psot(ns));
322  else
323  {
324  error() << "Invalid memory model " << mm
325  << " -- use one of sc, tso, pso" << eom;
327  }
328 
331 
332  {
333  const symbolt *init_symbol;
334  if(!ns.lookup(CPROVER_PREFIX "initialize", init_symbol))
335  symex.language_mode=init_symbol->mode;
336  }
337 
338  status() << "Starting Bounded Model Checking" << eom;
339 
341 
342  try
343  {
344  // get unwinding info
345  setup_unwind();
346 
347  // perform symbolic execution
348  symex(goto_functions);
349 
350  // add a partial ordering, if required
351  if(equation.has_threads())
352  {
353  memory_model->set_message_handler(get_message_handler());
354  (*memory_model)(equation);
355  }
356  }
357 
358  catch(const std::string &error_str)
359  {
360  messaget message(get_message_handler());
362  message.error() << error_str << messaget::eom;
363 
365  }
366 
367  catch(const char *error_str)
368  {
369  messaget message(get_message_handler());
371  message.error() << error_str << messaget::eom;
372 
374  }
375 
376  catch(std::bad_alloc)
377  {
378  error() << "Out of memory" << eom;
380  }
381 
382  statistics() << "size of program expression: "
383  << equation.SSA_steps.size()
384  << " steps" << eom;
385 
386  try
387  {
388  if(options.get_option("slice-by-trace")!="")
389  {
390  symex_slice_by_tracet symex_slice_by_trace(ns);
391 
392  symex_slice_by_trace.slice_by_trace
393  (options.get_option("slice-by-trace"), equation);
394  }
395 
396  if(equation.has_threads())
397  {
398  // we should build a thread-aware SSA slicer
399  statistics() << "no slicing due to threads" << eom;
400  }
401  else
402  {
403  if(options.get_bool_option("slice-formula"))
404  {
405  slice(equation);
406  statistics() << "slicing removed "
408  << " assignments" << eom;
409  }
410  else
411  {
412  if(options.get_list_option("cover").empty())
413  {
415  statistics() << "simple slicing removed "
417  << " assignments" << eom;
418  }
419  }
420  }
421 
422  {
423  statistics() << "Generated " << symex.total_vccs
424  << " VCC(s), " << symex.remaining_vccs
425  << " remaining after simplification" << eom;
426  }
427 
428  // coverage report
429  std::string cov_out=options.get_option("symex-coverage-report");
430  if(!cov_out.empty() &&
431  symex.output_coverage_report(goto_functions, cov_out))
432  {
433  error() << "Failed to write symex coverage report" << eom;
435  }
436 
437  if(options.get_bool_option("show-vcc"))
438  {
439  show_vcc();
440  return safety_checkert::resultt::SAFE; // to indicate non-error
441  }
442 
443  if(!options.get_list_option("cover").empty())
444  {
445  const optionst::value_listt criteria=
446  options.get_list_option("cover");
447  return cover(goto_functions, criteria)?
449  }
450 
451  if(options.get_option("localize-faults")!="")
452  {
453  fault_localizationt fault_localization(
454  goto_functions, *this, options);
455  return fault_localization();
456  }
457 
458  // any properties to check at all?
459  if(!options.get_bool_option("program-only") &&
461  {
462  report_success();
463  output_graphml(resultt::SAFE, goto_functions);
465  }
466 
467  if(options.get_bool_option("program-only"))
468  {
469  show_program();
471  }
472 
473  return decide(goto_functions, prop_conv);
474  }
475 
476  catch(std::string &error_str)
477  {
478  error() << error_str << eom;
480  }
481 
482  catch(const char *error_str)
483  {
484  error() << error_str << eom;
486  }
487 
488  catch(std::bad_alloc)
489  {
490  error() << "Out of memory" << eom;
492  }
493 }
494 
496  const goto_functionst &goto_functions,
497  prop_convt &prop_conv)
498 {
500 
501  if(options.get_bool_option("stop-on-fail"))
502  return stop_on_fail(goto_functions, prop_conv);
503  else
504  return all_properties(goto_functions, prop_conv);
505 }
506 
508  const goto_functionst &goto_functions,
509  prop_convt &prop_conv)
510 {
512  {
514  report_success();
515  output_graphml(resultt::SAFE, goto_functions);
516  return resultt::SAFE;
517 
519  if(options.get_bool_option("trace"))
520  {
521  if(options.get_bool_option("beautify"))
523  dynamic_cast<bv_cbmct &>(prop_conv), equation, ns);
524 
525  error_trace();
526  output_graphml(resultt::UNSAFE, goto_functions);
527  }
528 
529  report_failure();
530  return resultt::UNSAFE;
531 
532  default:
533  if(options.get_bool_option("dimacs") ||
534  options.get_option("outfile")!="")
535  return resultt::SAFE;
536 
537  error() << "decision procedure failed" << eom;
538 
539  return resultt::ERROR;
540  }
541 }
542 
544 {
545  const std::string &set=options.get_option("unwindset");
546  std::vector<std::string> unwindset_loops;
547  split_string(set, ',', unwindset_loops, true, true);
548 
549  for(auto &val : unwindset_loops)
550  {
551  unsigned thread_nr=0;
552  bool thread_nr_set=false;
553 
554  if(!val.empty() &&
555  isdigit(val[0]) &&
556  val.find(":")!=std::string::npos)
557  {
558  std::string nr=val.substr(0, val.find(":"));
559  thread_nr=unsafe_string2unsigned(nr);
560  thread_nr_set=true;
561  val.erase(0, nr.size()+1);
562  }
563 
564  if(val.rfind(":")!=std::string::npos)
565  {
566  std::string id=val.substr(0, val.rfind(":"));
567  long uw=unsafe_string2int(val.substr(val.rfind(":")+1));
568 
569  if(thread_nr_set)
570  symex.set_unwind_thread_loop_limit(thread_nr, id, uw);
571  else
573  }
574  }
575 
576  if(options.get_option("unwind")!="")
578 }
void output_graphml(resultt result, const goto_functionst &goto_functions)
outputs witnesses in graphml format
Definition: bmc.cpp:93
mstreamt & result()
Definition: message.h:233
Fault Localization.
void do_conversion()
Definition: bmc.cpp:118
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
Definition: namespace.cpp:139
void slice(symex_target_equationt &equation)
Definition: slice.cpp:209
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void convert(prop_convt &prop_conv)
void simple_slice(symex_target_equationt &equation)
Definition: slice.cpp:239
#define CPROVER_PREFIX
unsigned int get_unsigned_int_option(const std::string &option) const
Definition: options.cpp:54
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
irep_idt mode
Language mode.
Definition: symbol.h:55
mstreamt & status()
Definition: message.h:238
void set_unwind_loop_limit(const irep_idt &id, unsigned limit)
Definition: symex_bmc.h:50
unsigned unsafe_string2unsigned(const std::string &str, int base)
Definition: string2int.cpp:66
const graphmlt & graph()
bool from_expr(const exprt &expr, std::string &code)
Definition: languages.h:20
Definition: json.h:21
virtual void show_vcc()
Definition: show_vcc.cpp:142
languaget * new_ansi_c_language()
Slicer for matching with trace files.
virtual void report_failure()
Definition: bmc.cpp:193
optionst options
Definition: goto_symex.h:96
const value_listt & get_list_option(const std::string &option) const
Definition: options.cpp:73
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
Definition: bmc_cover.cpp:435
Memory models for partial order concurrency.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
void set_unwind_limit(unsigned limit)
Definition: symex_bmc.h:36
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:239
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
TO_BE_DOCUMENTED.
Definition: goto_trace.h:34
stepst steps
Definition: goto_trace.h:150
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
goto_programt::const_targett pc
Definition: goto_trace.h:90
virtual void setup_unwind()
Definition: bmc.cpp:543
json_arrayt & make_array()
Definition: json.h:228
virtual resultt decide(const goto_functionst &, prop_convt &)
Definition: bmc.cpp:495
goto_tracet error_trace
namespacet ns
Definition: bmc.h:71
symex_bmct symex
Definition: bmc.h:73
expr_listt bmc_constraints
Definition: bmc.h:57
jsont & push_back(const jsont &json)
Definition: json.h:157
unsigned count_ignored_SSA_steps() const
virtual void error_trace()
Definition: bmc.cpp:51
virtual void do_unwind_module()
Definition: bmc.cpp:46
virtual resultt dec_solve()=0
bool output_coverage_report(const goto_functionst &goto_functions, const std::string &path) const
Definition: symex_bmc.h:57
Traces of GOTO Programs.
source_locationt source_location
Definition: message.h:175
prop_convt & prop_conv
Definition: bmc.h:74
const std::string get_option(const std::string &option) const
Definition: options.cpp:60
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
std::list< std::string > value_listt
Definition: options.h:22
Definition: xml.h:18
unsigned remaining_vccs
Definition: goto_symex.h:92
Traces of GOTO Programs.
Time Stopping.
virtual resultt run(const goto_functionst &goto_functions)
Definition: bmc.cpp:310
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
std::string data
Definition: xml.h:30
virtual decision_proceduret::resultt run_decision_procedure(prop_convt &prop_conv)
Definition: bmc.cpp:139
#define forall_expr_list(it, expr)
Definition: expr.h:36
const optionst & options
Definition: bmc.h:69
mstreamt & statistics()
Definition: message.h:243
language_uit::uit ui
Definition: bmc.h:77
virtual resultt stop_on_fail(const goto_functionst &goto_functions, prop_convt &solver)
Definition: bmc.cpp:507
message_handlert & get_message_handler()
Definition: message.h:127
Bounded Model Checking for ANSI-C + HDL.
absolute_timet current_time()
void split_string(const std::string &s, char delim, std::vector< std::string > &result, bool strip, bool remove_empty)
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:101
void slice_by_trace(std::string trace_files, symex_target_equationt &equation)
Slicer for symex traces.
bool write_graphml(const graphmlt &src, std::ostream &os)
Definition: graphml.cpp:212
virtual void show_program()
Definition: bmc.cpp:221
void set_to_true(const exprt &expr)
Traces of GOTO Programs.
Memory models for partial order concurrency.
void make_nil()
Definition: irep.h:243
mstreamt & error()
Definition: message.h:223
Memory models for partial order concurrency.
symex_target_equationt equation
Definition: bmc.h:72
json_objectt & make_object()
Definition: json.h:234
virtual void report_success()
Definition: bmc.cpp:165
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
source_locationt last_source_location
Definition: symex_bmc.h:32
unsigned total_vccs
Definition: goto_symex.h:92
int unsafe_string2int(const std::string &str, int base)
Definition: string2int.cpp:61
void set_unwind_thread_loop_limit(unsigned thread_nr, const irep_idt &id, unsigned limit)
Definition: symex_bmc.h:42
languagest languages
Definition: mode.cpp:29
Witnesses for Traces and Proofs.
void build_goto_trace(const symex_target_equationt &target, symex_target_equationt::SSA_stepst::const_iterator end_step, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
Counterexample Beautification.
virtual std::string decision_procedure_text() const =0