cprover
bmc_cover.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Test-Suite Generation with BMC
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "bmc.h"
13 
14 #include <iostream>
15 
16 #include <util/time_stopping.h>
17 #include <util/xml.h>
18 #include <util/xml_expr.h>
19 #include <util/json.h>
20 #include <util/json_expr.h>
21 
24 
28 
29 #include "bv_cbmc.h"
30 
31 class bmc_covert:
33  public messaget
34 {
35 public:
37  const goto_functionst &_goto_functions,
38  bmct &_bmc):
39  goto_functions(_goto_functions), solver(_bmc.prop_conv), bmc(_bmc)
40  {
41  }
42 
43  bool operator()();
44 
45  // gets called by prop_covert
46  virtual void satisfying_assignment();
47 
48  struct goalt
49  {
50  // a criterion is satisfied if _any_ instance is true
51  struct instancet
52  {
53  symex_target_equationt::SSA_stepst::iterator step;
55  };
56 
57  typedef std::vector<instancet> instancest;
58  instancest instances;
59 
61  symex_target_equationt::SSA_stepst::iterator step,
63  {
64  instances.push_back(instancet());
65  instances.back().step=step;
66  instances.back().condition=condition;
67  }
68 
69  std::string description;
71 
72  // if satisfied, we compute a goto_trace
73  bool satisfied;
74 
76  const std::string &_description,
77  const source_locationt &_source_location):
78  description(_description),
79  source_location(_source_location),
80  satisfied(false)
81  {
82  }
83 
84  goalt():source_location(source_locationt::nil()),
85  satisfied(false)
86  {
87  }
88 
89  exprt as_expr() const
90  {
91  std::vector<exprt> tmp;
92 
93  for(const auto &goal_inst : instances)
94  tmp.push_back(literal_exprt(goal_inst.condition));
95 
96  return disjunction(tmp);
97  }
98  };
99 
100  struct testt
101  {
103  std::vector<irep_idt> covered_goals;
104  };
105 
107  {
108  return loc->source_location.get_property_id();
109  }
110 
111  typedef std::map<irep_idt, goalt> goal_mapt;
112  goal_mapt goal_map;
113  typedef std::vector<testt> testst;
114  testst tests;
115 
116  std::string get_test(const goto_tracet &goto_trace) const
117  {
118  bool first=true;
119  std::string test;
120  for(const auto &step : goto_trace.steps)
121  {
122  if(step.is_input())
123  {
124  if(first)
125  first=false;
126  else
127  test+=", ";
128 
129  test+=id2string(step.io_id)+"=";
130 
131  if(step.io_args.size()==1)
132  test+=from_expr(bmc.ns, "", step.io_args.front());
133  }
134  }
135  return test;
136  }
137 
138 protected:
142 };
143 
145 {
146  tests.push_back(testt());
147  testt &test = tests.back();
148 
149  for(auto &goal_pair : goal_map)
150  {
151  goalt &g=goal_pair.second;
152 
153  // covered already?
154  if(g.satisfied)
155  continue;
156 
157  // check whether satisfied
158  for(const auto &goal_inst : g.instances)
159  {
160  literalt cond=goal_inst.condition;
161 
162  if(solver.l_get(cond).is_true())
163  {
164  status() << "Covered " << g.description << messaget::eom;
165  g.satisfied=true;
166  test.covered_goals.push_back(goal_pair.first);
167  break;
168  }
169  }
170  }
171 
173  solver, bmc.ns, test.goto_trace);
174 
175  goto_tracet &goto_trace=test.goto_trace;
176 
177  // Now delete anything after first failed assumption
178  for(goto_tracet::stepst::iterator
179  s_it1=goto_trace.steps.begin();
180  s_it1!=goto_trace.steps.end();
181  s_it1++)
182  if(s_it1->is_assume() && !s_it1->cond_value)
183  {
184  goto_trace.steps.erase(++s_it1, goto_trace.steps.end());
185  break;
186  }
187 
188  #if 0
189  show_goto_trace(std::cout, bmc.ns, test.goto_trace);
190  #endif
191 }
192 
194 {
195  status() << "Passing problem to " << solver.decision_procedure_text() << eom;
196 
198 
199  // stop the time
200  absolute_timet sat_start=current_time();
201 
202  // Collect _all_ goals in `goal_map'.
203  // This maps property IDs to 'goalt'
205  {
206  // Functions are already inlined.
207  if(f_it->second.is_inlined()) continue;
208  forall_goto_program_instructions(i_it, f_it->second.body)
209  {
210  if(i_it->is_assert())
211  goal_map[id(i_it)]=
212  goalt(
213  id2string(i_it->source_location.get_comment()),
214  i_it->source_location);
215  }
216  }
217 
218  for(auto &step : bmc.equation.SSA_steps)
219  step.cond_literal=literalt(0, 0);
220 
221  // Do conversion to next solver layer
222 
223  bmc.do_conversion();
224 
225  // bmc.equation.output(std::cout);
226 
227  // get the conditions for these goals from formula
228  // collect all 'instances' of the goals
229  for(auto it = bmc.equation.SSA_steps.begin();
230  it!=bmc.equation.SSA_steps.end();
231  it++)
232  {
233  if(it->is_assert())
234  {
235  assert(it->source.pc->is_assert());
236  exprt c=
237  conjunction({ // NOLINT(whitespace/braces)
238  literal_exprt(it->guard_literal),
239  literal_exprt(!it->cond_literal) });
240  literalt l_c=solver.convert(c);
241  goal_map[id(it->source.pc)].add_instance(it, l_c);
242  }
243  }
244 
245  status() << "Aiming to cover " << goal_map.size() << " goal(s)" << eom;
246 
247  cover_goalst cover_goals(solver);
248 
249  cover_goals.register_observer(*this);
250 
251  for(const auto &g : goal_map)
252  {
253  literalt l=solver.convert(g.second.as_expr());
254  cover_goals.add(l);
255  }
256 
257  assert(cover_goals.size()==goal_map.size());
258 
259  status() << "Running " << solver.decision_procedure_text() << eom;
260 
261  cover_goals();
262 
263  // output runtime
264 
265  {
266  absolute_timet sat_stop=current_time();
267  status() << "Runtime decision procedure: "
268  << (sat_stop-sat_start) << "s" << eom;
269  }
270 
271  // report
272  unsigned goals_covered=0;
273 
274  for(const auto &g : goal_map)
275  if(g.second.satisfied)
276  goals_covered++;
277 
278  switch(bmc.ui)
279  {
281  {
282  status() << "\n** coverage results:" << eom;
283 
284  for(const auto &g : goal_map)
285  {
286  const goalt &goal=g.second;
287 
288  status() << "[" << g.first << "]";
289 
290  if(goal.source_location.is_not_nil())
291  status() << ' ' << goal.source_location;
292 
293  if(!goal.description.empty())
294  status() << ' ' << goal.description;
295 
296  status() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
297  << eom;
298  }
299 
300  status() << '\n';
301 
302  break;
303  }
304 
306  {
307  for(const auto &goal_pair : goal_map)
308  {
309  const goalt &goal=goal_pair.second;
310 
311  xmlt xml_result("goal");
312  xml_result.set_attribute("id", id2string(goal_pair.first));
313  xml_result.set_attribute("description", goal.description);
314  xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED");
315 
316  if(goal.source_location.is_not_nil())
317  xml_result.new_element()=xml(goal.source_location);
318 
319  std::cout << xml_result << "\n";
320  }
321 
322  for(const auto &test : tests)
323  {
324  xmlt xml_result("test");
325  if(bmc.options.get_bool_option("trace"))
326  {
327  convert(bmc.ns, test.goto_trace, xml_result.new_element());
328  }
329  else
330  {
331  xmlt &xml_test=xml_result.new_element("inputs");
332 
333  for(const auto &step : test.goto_trace.steps)
334  {
335  if(step.is_input())
336  {
337  xmlt &xml_input=xml_test.new_element("input");
338  xml_input.set_attribute("id", id2string(step.io_id));
339  if(step.io_args.size()==1)
340  xml_input.new_element("value")=
341  xml(step.io_args.front(), bmc.ns);
342  }
343  }
344  }
345 
346  for(const auto &goal_id : test.covered_goals)
347  {
348  xmlt &xml_goal=xml_result.new_element("goal");
349  xml_goal.set_attribute("id", id2string(goal_id));
350  }
351 
352  std::cout << xml_result << "\n";
353  }
354  break;
355  }
356 
358  {
359  json_objectt json_result;
360  json_arrayt &goals_array=json_result["goals"].make_array();
361  for(const auto &goal_pair : goal_map)
362  {
363  const goalt &goal=goal_pair.second;
364 
365  json_objectt &result=goals_array.push_back().make_object();
366  result["status"]=json_stringt(goal.satisfied?"satisfied":"failed");
367  result["goal"]=json_stringt(id2string(goal_pair.first));
368  result["description"]=json_stringt(goal.description);
369 
370  if(goal.source_location.is_not_nil())
371  result["sourceLocation"]=json(goal.source_location);
372  }
373  json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size()));
374  json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered));
375 
376  json_arrayt &tests_array=json_result["tests"].make_array();
377  for(const auto &test : tests)
378  {
379  json_objectt &result=tests_array.push_back().make_object();
380  if(bmc.options.get_bool_option("trace"))
381  {
382  jsont &json_trace=result["trace"];
383  convert(bmc.ns, test.goto_trace, json_trace);
384  }
385  else
386  {
387  json_arrayt &json_test=result["inputs"].make_array();
388 
389  for(const auto &step : test.goto_trace.steps)
390  {
391  if(step.is_input())
392  {
393  json_objectt json_input;
394  json_input["id"]=json_stringt(id2string(step.io_id));
395  if(step.io_args.size()==1)
396  json_input["value"]=json(step.io_args.front(), bmc.ns);
397  json_test.push_back(json_input);
398  }
399  }
400  }
401  json_arrayt &goal_refs=result["coveredGoals"].make_array();
402  for(const auto &goal_id : test.covered_goals)
403  {
404  goal_refs.push_back(json_stringt(id2string(goal_id)));
405  }
406  }
407  std::cout << ",\n" << json_result;
408  break;
409  }
410  }
411 
412  status() << "** " << goals_covered
413  << " of " << goal_map.size() << " covered ("
414  << std::fixed << std::setw(1) << std::setprecision(1)
415  << (goal_map.empty()?100.0:100.0*goals_covered/goal_map.size())
416  << "%)" << eom;
417 
418  statistics() << "** Used "
419  << cover_goals.iterations() << " iteration"
420  << (cover_goals.iterations()==1?"":"s")
421  << eom;
422 
424  {
425  std::cout << "Test suite:" << '\n';
426 
427  for(const auto &test : tests)
428  std::cout << get_test(test.goto_trace) << '\n';
429  }
430 
431  return false;
432 }
433 
437  const optionst::value_listt &criteria)
438 {
439  bmc_covert bmc_cover(goto_functions, *this);
441  return bmc_cover();
442 }
#define loc()
mstreamt & result()
Definition: message.h:233
void do_conversion()
Definition: bmc.cpp:118
source_locationt source_location
Definition: bmc_cover.cpp:70
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:104
instancest instances
Definition: bmc_cover.cpp:58
goto_tracet goto_trace
Definition: bmc_cover.cpp:102
prop_convt & solver
Definition: bmc_cover.cpp:140
mstreamt & status()
Definition: message.h:238
bmct & bmc
Definition: bmc_cover.cpp:141
const goto_functionst & goto_functions
Definition: bmc_cover.cpp:139
Definition: json.h:21
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool cover(const goto_functionst &goto_functions, const optionst::value_listt &criteria)
Try to cover all goals.
Definition: bmc_cover.cpp:435
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
std::map< irep_idt, goalt > goal_mapt
Definition: bmc_cover.cpp:111
stepst steps
Definition: goto_trace.h:150
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:25
json_arrayt & make_array()
Definition: json.h:228
irep_idt id(goto_programt::const_targett loc)
Definition: bmc_cover.cpp:106
namespacet ns
Definition: bmc.h:71
jsont & push_back(const jsont &json)
Definition: json.h:157
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:50
goal_mapt goal_map
Definition: bmc_cover.cpp:112
instructionst::const_iterator const_targett
exprt as_expr() const
Definition: bmc_cover.cpp:89
Traces of GOTO Programs.
symex_target_equationt::SSA_stepst::iterator step
Definition: bmc_cover.cpp:53
std::vector< instancet > instancest
Definition: bmc_cover.cpp:57
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
Expressions in JSON.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
goalt(const std::string &_description, const source_locationt &_source_location)
Definition: bmc_cover.cpp:75
std::list< std::string > value_listt
Definition: options.h:22
Definition: xml.h:18
Traces of GOTO Programs.
virtual literalt convert(const exprt &expr)=0
Time Stopping.
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
bool operator()()
Definition: bmc_cover.cpp:193
const optionst & options
Definition: bmc.h:69
mstreamt & statistics()
Definition: message.h:243
exprt disjunction(const exprt::operandst &op)
Definition: std_expr.cpp:26
xmlt & new_element(const std::string &name)
Definition: xml.h:86
language_uit::uit ui
Definition: bmc.h:77
bool is_true() const
Definition: threeval.h:25
std::string description
Definition: bmc_cover.cpp:69
void add(const literalt condition)
Definition: cover_goals.h:68
unsigned iterations() const
Definition: cover_goals.h:56
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
Definition: message.h:127
Bounded Model Checking for ANSI-C + HDL.
absolute_timet current_time()
Base class for all expressions.
Definition: expr.h:46
std::vector< testt > testst
Definition: bmc_cover.cpp:113
std::string get_test(const goto_tracet &goto_trace) const
Definition: bmc_cover.cpp:116
Cover a set of goals incrementally.
Traces of GOTO Programs.
Definition: bmc.h:32
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
std::vector< irep_idt > covered_goals
Definition: bmc_cover.cpp:103
symex_target_equationt equation
Definition: bmc.h:72
void add_instance(symex_target_equationt::SSA_stepst::iterator step, literalt condition)
Definition: bmc_cover.cpp:60
json_objectt & make_object()
Definition: json.h:234
void register_observer(observert &o)
Definition: cover_goals.h:84
TO_BE_DOCUMENTED.
Definition: goto_trace.h:146
virtual void satisfying_assignment()
Definition: bmc_cover.cpp:144
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
testst tests
Definition: bmc_cover.cpp:114
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23
goalst::size_type size() const
Definition: cover_goals.h:61
bmc_covert(const goto_functionst &_goto_functions, bmct &_bmc)
Definition: bmc_cover.cpp:36
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)
virtual std::string decision_procedure_text() const =0