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