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  symex_target_equationt::SSA_stepst::const_iterator step,
149  const prop_convt &prop_conv)
150 {
151  return step->is_assume() && prop_conv.l_get(step->cond_literal).is_false();
152 }
153 
155 {
156  tests.push_back(testt());
157  testt &test = tests.back();
158 
159  for(auto &goal_pair : goal_map)
160  {
161  goalt &g=goal_pair.second;
162 
163  // covered already?
164  if(g.satisfied)
165  continue;
166 
167  // check whether satisfied
168  for(const auto &goal_inst : g.instances)
169  {
170  literalt cond=goal_inst.condition;
171 
172  if(solver.l_get(cond).is_true())
173  {
174  status() << "Covered function " << g.source_location.get_function()
175  << " " << g.description << messaget::eom;
176  g.satisfied=true;
177  test.covered_goals.push_back(goal_pair.first);
178  break;
179  }
180  }
181  }
182 
185 }
186 
188 {
189  status() << "Passing problem to " << solver.decision_procedure_text() << eom;
190 
192 
193  auto solver_start=std::chrono::steady_clock::now();
194 
195  // Collect _all_ goals in `goal_map'.
196  // This maps property IDs to 'goalt'
198  {
199  forall_goto_program_instructions(i_it, f_it->second.body)
200  {
201  if(i_it->is_assert())
202  goal_map[id(i_it)]=
203  goalt(
204  id2string(i_it->source_location.get_comment()),
205  i_it->source_location);
206  }
207  }
208 
209  for(auto &step : bmc.equation.SSA_steps)
210  step.cond_literal=literalt(0, 0);
211 
212  // Do conversion to next solver layer
213 
214  bmc.do_conversion();
215 
216  // get the conditions for these goals from formula
217  // collect all 'instances' of the goals
218  for(auto it = bmc.equation.SSA_steps.begin();
219  it!=bmc.equation.SSA_steps.end();
220  it++)
221  {
222  if(it->is_assert())
223  {
224  assert(it->source.pc->is_assert());
225  const and_exprt c(
226  literal_exprt(it->guard_literal), literal_exprt(!it->cond_literal));
227  literalt l_c=solver.convert(c);
228  goal_map[id(it->source.pc)].add_instance(it, l_c);
229  }
230  }
231 
232  status() << "Aiming to cover " << goal_map.size() << " goal(s)" << eom;
233 
234  cover_goalst cover_goals(solver);
235 
236  cover_goals.register_observer(*this);
237 
238  for(const auto &g : goal_map)
239  {
240  literalt l=solver.convert(g.second.as_expr());
241  cover_goals.add(l);
242  }
243 
244  assert(cover_goals.size()==goal_map.size());
245 
246  status() << "Running " << solver.decision_procedure_text() << eom;
247 
248  cover_goals();
249 
250  {
251  auto solver_stop=std::chrono::steady_clock::now();
252  status() << "Runtime decision procedure: "
253  << std::chrono::duration<double>(solver_stop-solver_start).count()
254  << "s" << eom;
255  }
256 
257  // report
258  unsigned goals_covered=0;
259 
260  for(const auto &g : goal_map)
261  if(g.second.satisfied)
262  goals_covered++;
263 
264  switch(bmc.ui)
265  {
267  {
268  result() << "\n** coverage results:" << eom;
269 
270  for(const auto &g : goal_map)
271  {
272  const goalt &goal=g.second;
273 
274  result() << "[" << g.first << "]";
275 
276  if(goal.source_location.is_not_nil())
277  result() << ' ' << goal.source_location;
278 
279  if(!goal.description.empty())
280  result() << ' ' << goal.description;
281 
282  result() << ": " << (goal.satisfied?"SATISFIED":"FAILED")
283  << '\n';
284  }
285 
286  result() << eom;
287  break;
288  }
289 
291  {
292  for(const auto &goal_pair : goal_map)
293  {
294  const goalt &goal=goal_pair.second;
295 
296  xmlt xml_result("goal");
297  xml_result.set_attribute("id", id2string(goal_pair.first));
298  xml_result.set_attribute("description", goal.description);
299  xml_result.set_attribute("status", goal.satisfied?"SATISFIED":"FAILED");
300 
301  if(goal.source_location.is_not_nil())
302  xml_result.new_element()=xml(goal.source_location);
303 
304  result() << xml_result;
305  }
306 
307  for(const auto &test : tests)
308  {
309  xmlt xml_result("test");
310  if(bmc.options.get_bool_option("trace"))
311  {
312  convert(bmc.ns, test.goto_trace, xml_result.new_element());
313  }
314  else
315  {
316  xmlt &xml_test=xml_result.new_element("inputs");
317 
318  for(const auto &step : test.goto_trace.steps)
319  {
320  if(step.is_input())
321  {
322  xmlt &xml_input=xml_test.new_element("input");
323  xml_input.set_attribute("id", id2string(step.io_id));
324  if(step.io_args.size()==1)
325  xml_input.new_element("value")=
326  xml(step.io_args.front(), bmc.ns);
327  }
328  }
329  }
330 
331  for(const auto &goal_id : test.covered_goals)
332  {
333  xmlt &xml_goal=xml_result.new_element("goal");
334  xml_goal.set_attribute("id", id2string(goal_id));
335  }
336 
337  result() << xml_result;
338  }
339  break;
340  }
341 
343  {
344  json_stream_objectt &json_result =
346  for(const auto &goal_pair : goal_map)
347  {
348  const goalt &goal=goal_pair.second;
349 
350  json_result["status"] =
351  json_stringt(goal.satisfied ? "satisfied" : "failed");
352  json_result["goal"] = json_stringt(goal_pair.first);
353  json_result["description"] = json_stringt(goal.description);
354 
355  if(goal.source_location.is_not_nil())
356  json_result["sourceLocation"] = json(goal.source_location);
357  }
358  json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size()));
359  json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered));
360 
361  json_arrayt &tests_array=json_result["tests"].make_array();
362  for(const auto &test : tests)
363  {
364  json_objectt &result=tests_array.push_back().make_object();
365  if(bmc.options.get_bool_option("trace"))
366  {
367  json_arrayt &json_trace = json_result["trace"].make_array();
368  convert(bmc.ns, test.goto_trace, json_trace, bmc.trace_options());
369  }
370  else
371  {
372  json_arrayt &json_test = json_result["inputs"].make_array();
373 
374  for(const auto &step : test.goto_trace.steps)
375  {
376  if(step.is_input())
377  {
378  json_objectt json_input;
379  json_input["id"] = json_stringt(step.io_id);
380  if(step.io_args.size()==1)
381  json_input["value"]=
382  json(step.io_args.front(), bmc.ns, ID_unknown);
383  json_test.push_back(json_input);
384  }
385  }
386  }
387  json_arrayt &goal_refs=result["coveredGoals"].make_array();
388  for(const auto &goal_id : test.covered_goals)
389  {
390  goal_refs.push_back(json_stringt(goal_id));
391  }
392  }
393 
394  break;
395  }
396  }
397 
398  status() << "** " << goals_covered
399  << " of " << goal_map.size() << " covered ("
400  << std::fixed << std::setw(1) << std::setprecision(1)
401  << (goal_map.empty()?100.0:100.0*goals_covered/goal_map.size())
402  << "%)" << eom;
403 
404  statistics() << "** Used "
405  << cover_goals.iterations() << " iteration"
406  << (cover_goals.iterations()==1?"":"s")
407  << eom;
408 
410  {
411  result() << "Test suite:" << '\n';
412 
413  for(const auto &test : tests)
414  result() << get_test(test.goto_trace) << '\n';
415 
416  result() << eom;
417  }
418 
419  return false;
420 }
421 
423 bool bmct::cover(const goto_functionst &goto_functions)
424 {
425  bmc_covert bmc_cover(goto_functions, *this);
427  return bmc_cover();
428 }
#define loc()
bool is_false() const
Definition: threeval.h:26
void do_conversion()
Definition: bmc.cpp:112
void build_goto_trace(const symex_target_equationt &target, ssa_step_predicatet is_last_step_to_keep, const prop_convt &prop_conv, const namespacet &ns, goto_tracet &goto_trace)
source_locationt source_location
Definition: bmc_cover.cpp:73
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
Definition: bmc_cover.cpp:423
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
bool is_not_nil() const
Definition: irep.h:173
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
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
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:187
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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 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:154
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
static bool is_failed_assumption_step(symex_target_equationt::SSA_stepst::const_iterator step, const prop_convt &prop_conv)
Definition: bmc_cover.cpp:147
Traces of GOTO Programs.
virtual std::string decision_procedure_text() const =0