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 class bmc_covert:
34  public messaget
35 {
36 public:
38  const goto_functionst &_goto_functions,
39  bmct &_bmc):
40  goto_functions(_goto_functions), solver(_bmc.prop_conv), bmc(_bmc)
41  {
42  }
43 
44  bool operator()();
45 
46  // gets called by prop_covert
47  virtual void satisfying_assignment();
48 
49  struct goalt
50  {
51  // a criterion is satisfied if _any_ instance is true
52  struct instancet
53  {
54  symex_target_equationt::SSA_stepst::iterator step;
56  };
57 
58  typedef std::vector<instancet> instancest;
60 
62  symex_target_equationt::SSA_stepst::iterator step,
63  literalt condition)
64  {
65  instances.push_back(instancet());
66  instances.back().step=step;
67  instances.back().condition=condition;
68  }
69 
70  std::string description;
72 
73  // if satisfied, we compute a goto_trace
74  bool satisfied;
75 
77  const std::string &_description,
78  const source_locationt &_source_location):
79  description(_description),
80  source_location(_source_location),
81  satisfied(false)
82  {
83  }
84 
86  satisfied(false)
87  {
88  }
89 
90  exprt as_expr() const
91  {
92  std::vector<exprt> tmp;
93 
94  for(const auto &goal_inst : instances)
95  tmp.push_back(literal_exprt(goal_inst.condition));
96 
97  return disjunction(tmp);
98  }
99  };
100 
101  struct testt
102  {
104  std::vector<irep_idt> covered_goals;
105  };
106 
108  {
109  return loc->source_location.get_property_id();
110  }
111 
112  typedef std::map<irep_idt, goalt> goal_mapt;
114  typedef std::vector<testt> testst;
116 
117  std::string get_test(const goto_tracet &goto_trace) const
118  {
119  bool first=true;
120  std::string test;
121  for(const auto &step : goto_trace.steps)
122  {
123  if(step.is_input())
124  {
125  if(first)
126  first=false;
127  else
128  test+=", ";
129 
130  test+=id2string(step.io_id)+"=";
131 
132  if(step.io_args.size()==1)
133  test+=from_expr(bmc.ns, "", step.io_args.front());
134  }
135  }
136  return test;
137  }
138 
139 protected:
143 };
144 
146  symex_target_equationt::SSA_stepst::const_iterator step,
147  const prop_convt &prop_conv)
148 {
149  return step->is_assume() && prop_conv.l_get(step->cond_literal).is_false();
150 }
151 
153 {
154  tests.push_back(testt());
155  testt &test = tests.back();
156 
157  for(auto &goal_pair : goal_map)
158  {
159  goalt &g=goal_pair.second;
160 
161  // covered already?
162  if(g.satisfied)
163  continue;
164 
165  // check whether satisfied
166  for(const auto &goal_inst : g.instances)
167  {
168  literalt cond=goal_inst.condition;
169 
170  if(solver.l_get(cond).is_true())
171  {
172  status() << "Covered function " << g.source_location.get_function()
173  << " " << g.description << messaget::eom;
174  g.satisfied=true;
175  test.covered_goals.push_back(goal_pair.first);
176  break;
177  }
178  }
179  }
180 
183 }
184 
186 {
187  status() << "Passing problem to " << solver.decision_procedure_text() << eom;
188 
190 
191  auto solver_start=std::chrono::steady_clock::now();
192 
193  // Collect _all_ goals in `goal_map'.
194  // This maps property IDs to 'goalt'
196  {
197  forall_goto_program_instructions(i_it, f_it->second.body)
198  {
199  if(i_it->is_assert())
200  goal_map[id(i_it)]=
201  goalt(
202  id2string(i_it->source_location.get_comment()),
203  i_it->source_location);
204  }
205  }
206 
207  for(auto &step : bmc.equation.SSA_steps)
208  step.cond_literal=literalt(0, 0);
209 
210  // Do conversion to next solver layer
211 
212  bmc.do_conversion();
213 
214  // get the conditions for these goals from formula
215  // collect all 'instances' of the goals
216  for(auto it = bmc.equation.SSA_steps.begin();
217  it!=bmc.equation.SSA_steps.end();
218  it++)
219  {
220  if(it->is_assert())
221  {
222  PRECONDITION(it->source.pc->is_assert());
223  const and_exprt c(
224  literal_exprt(it->guard_literal), literal_exprt(!it->cond_literal));
225  literalt l_c=solver.convert(c);
226  goal_map[id(it->source.pc)].add_instance(it, l_c);
227  }
228  }
229 
230  status() << "Aiming to cover " << goal_map.size() << " goal(s)" << eom;
231 
232  cover_goalst cover_goals(solver);
233 
234  cover_goals.register_observer(*this);
235 
236  for(const auto &g : goal_map)
237  {
238  literalt l=solver.convert(g.second.as_expr());
239  cover_goals.add(l);
240  }
241 
242  INVARIANT(cover_goals.size() == goal_map.size(),
243  "we add coverage for each goal");
244 
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_message_handler.get_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  if(status().tellp() > 0)
345  status() << eom; // force end of previous message
346  json_stream_objectt &json_result =
348  for(const auto &goal_pair : goal_map)
349  {
350  const goalt &goal=goal_pair.second;
351 
352  json_result["status"] =
353  json_stringt(goal.satisfied ? "satisfied" : "failed");
354  json_result["goal"] = json_stringt(goal_pair.first);
355  json_result["description"] = json_stringt(goal.description);
356 
357  if(goal.source_location.is_not_nil())
358  json_result["sourceLocation"] = json(goal.source_location);
359  }
360  json_result["totalGoals"]=json_numbert(std::to_string(goal_map.size()));
361  json_result["goalsCovered"]=json_numbert(std::to_string(goals_covered));
362 
363  json_arrayt &tests_array=json_result["tests"].make_array();
364  for(const auto &test : tests)
365  {
366  json_objectt &result=tests_array.push_back().make_object();
367  if(bmc.options.get_bool_option("trace"))
368  {
369  json_arrayt &json_trace = json_result["trace"].make_array();
370  convert(bmc.ns, test.goto_trace, json_trace, bmc.trace_options());
371  }
372  else
373  {
374  json_arrayt &json_test = json_result["inputs"].make_array();
375 
376  for(const auto &step : test.goto_trace.steps)
377  {
378  if(step.is_input())
379  {
380  json_objectt json_input;
381  json_input["id"] = json_stringt(step.io_id);
382  if(step.io_args.size()==1)
383  json_input["value"]=
384  json(step.io_args.front(), bmc.ns, ID_unknown);
385  json_test.push_back(json_input);
386  }
387  }
388  }
389  json_arrayt &goal_refs=result["coveredGoals"].make_array();
390  for(const auto &goal_id : test.covered_goals)
391  {
392  goal_refs.push_back(json_stringt(goal_id));
393  }
394  }
395 
396  break;
397  }
398  }
399 
400  status() << "** " << goals_covered
401  << " of " << goal_map.size() << " covered ("
402  << std::fixed << std::setw(1) << std::setprecision(1)
403  << (goal_map.empty()?100.0:100.0*goals_covered/goal_map.size())
404  << "%)" << eom;
405 
406  statistics() << "** Used "
407  << cover_goals.iterations() << " iteration"
408  << (cover_goals.iterations()==1?"":"s")
409  << eom;
410 
412  {
413  result() << "Test suite:" << '\n';
414 
415  for(const auto &test : tests)
416  result() << get_test(test.goto_trace) << '\n';
417 
418  result() << eom;
419  }
420 
421  return false;
422 }
423 
425 bool bmct::cover(const goto_functionst &goto_functions)
426 {
427  bmc_covert bmc_cover(goto_functions, *this);
429  return bmc_cover();
430 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
bmc_covert::goalt
Definition: bmc_cover.cpp:49
json_numbert
Definition: json.h:235
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:57
is_failed_assumption_step
static bool is_failed_assumption_step(symex_target_equationt::SSA_stepst::const_iterator step, const prop_convt &prop_conv)
Definition: bmc_cover.cpp:145
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
bmct::trace_options
trace_optionst trace_options()
Definition: bmc.h:191
json
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
bmc_covert::id
irep_idt id(goto_programt::const_targett loc)
Definition: bmc_cover.cpp:107
bmct
Bounded model checking or path exploration for goto-programs.
Definition: bmc.h:41
bmc_covert::testt::goto_trace
goto_tracet goto_trace
Definition: bmc_cover.cpp:103
bmct::cover
bool cover(const goto_functionst &goto_functions)
Try to cover all goals.
Definition: bmc_cover.cpp:425
build_goto_trace
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)
Definition: build_goto_trace.cpp:166
ui_message_handlert::uit::XML_UI
@ XML_UI
prop_convt
Definition: prop_conv.h:27
messaget::status
mstreamt & status() const
Definition: message.h:401
bmc_covert::goto_functions
const goto_functionst & goto_functions
Definition: bmc_cover.cpp:140
bmc_covert::satisfying_assignment
virtual void satisfying_assignment()
Definition: bmc_cover.cpp:152
json_stream.h
xml
xmlt xml(const source_locationt &location)
Definition: xml_expr.cpp:26
bmc_covert::goal_map
goal_mapt goal_map
Definition: bmc_cover.cpp:113
cover_goalst::observert
Definition: cover_goals.h:79
and_exprt
Boolean AND.
Definition: std_expr.h:2409
bmc_covert::goalt::satisfied
bool satisfied
Definition: bmc_cover.cpp:74
goto_tracet::steps
stepst steps
Definition: goto_trace.h:154
bmc_covert::solver
prop_convt & solver
Definition: bmc_cover.cpp:141
bmc_covert::testt
Definition: bmc_cover.cpp:101
exprt
Base class for all expressions.
Definition: expr.h:54
bmc_covert::goalt::instancet
Definition: bmc_cover.cpp:52
bmc_covert::tests
testst tests
Definition: bmc_cover.cpp:115
bmc_covert::goalt::goalt
goalt(const std::string &_description, const source_locationt &_source_location)
Definition: bmc_cover.cpp:76
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
messaget::eom
static eomt eom
Definition: message.h:284
bmc_covert::goalt::description
std::string description
Definition: bmc_cover.cpp:70
jsont::make_object
json_objectt & make_object()
Definition: json.h:290
cover_goalst
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
xml.h
bmc_covert::goal_mapt
std::map< irep_idt, goalt > goal_mapt
Definition: bmc_cover.cpp:112
bmc_covert::goalt::instancet::step
symex_target_equationt::SSA_stepst::iterator step
Definition: bmc_cover.cpp:54
json_arrayt
Definition: json.h:146
json_objectt
Definition: json.h:244
cover_goalst::iterations
unsigned iterations() const
Definition: cover_goals.h:58
bmct::ui_message_handler
ui_message_handlert & ui_message_handler
Definition: bmc.h:178
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
convert
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
Definition: builtin_factory.cpp:41
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:26
bmc_covert::testt::covered_goals
std::vector< irep_idt > covered_goals
Definition: bmc_cover.cpp:104
messaget::result
mstreamt & result() const
Definition: message.h:396
bmct::ns
namespacet ns
Definition: bmc.h:171
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
ui_message_handlert::uit::JSON_UI
@ JSON_UI
ui_message_handlert::get_json_stream
json_stream_arrayt & get_json_stream()
Definition: ui_message.h:37
prop_convt::convert
virtual literalt convert(const exprt &expr)=0
language_util.h
bmct::options
const optionst & options
Definition: bmc.h:166
literal_exprt
Definition: literal_expr.h:17
xml_goto_trace.h
cover_goalst::register_observer
void register_observer(observert &o)
Definition: cover_goals.h:86
messaget::set_message_handler
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:169
json_expr.h
bmc_covert::goalt::goalt
goalt()
Definition: bmc_cover.cpp:85
cover_goalst::size
goalst::size_type size() const
Definition: cover_goals.h:63
json_goto_trace.h
tvt::is_false
bool is_false() const
Definition: threeval.h:26
bmc.h
xmlt
Definition: xml.h:18
prop_convt::l_get
virtual tvt l_get(literalt a) const =0
bmc_covert::bmc
bmct & bmc
Definition: bmc_cover.cpp:142
bmc_covert::testst
std::vector< testt > testst
Definition: bmc_cover.cpp:114
bmc_covert::goalt::instancet::condition
literalt condition
Definition: bmc_cover.cpp:55
source_locationt
Definition: source_location.h:20
json_stream_arrayt::push_back_stream_object
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
cover_goalst::add
void add(const literalt condition)
Definition: cover_goals.h:70
decision_proceduret::decision_procedure_text
virtual std::string decision_procedure_text() const =0
json_stream_objectt
Provides methods for streaming JSON objects.
Definition: json_stream.h:139
ui_message_handlert::get_ui
uit get_ui() const
Definition: ui_message.h:30
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
bmc_covert::goalt::add_instance
void add_instance(symex_target_equationt::SSA_stepst::iterator step, literalt condition)
Definition: bmc_cover.cpp:61
bmc_covert::goalt::instances
instancest instances
Definition: bmc_cover.cpp:59
bmc_covert::bmc_covert
bmc_covert(const goto_functionst &_goto_functions, bmct &_bmc)
Definition: bmc_cover.cpp:37
ui_message_handlert::uit::PLAIN
@ PLAIN
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
bmct::equation
symex_target_equationt equation
Definition: bmc.h:172
build_goto_trace.h
literalt
Definition: literal.h:24
bmc_covert::operator()
bool operator()()
Definition: bmc_cover.cpp:185
json.h
bmc_covert
Definition: bmc_cover.cpp:32
bmc_covert::goalt::source_location
source_locationt source_location
Definition: bmc_cover.cpp:71
bmc_covert::goalt::instancest
std::vector< instancet > instancest
Definition: bmc_cover.cpp:58
goto_tracet
TO_BE_DOCUMENTED.
Definition: goto_trace.h:150
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
bmc_covert::goalt::as_expr
exprt as_expr() const
Definition: bmc_cover.cpp:90
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
loc
#define loc()
Definition: ansi_c_lex.yy.cpp:4256
bmc_covert::get_test
std::string get_test(const goto_tracet &goto_trace) const
Definition: bmc_cover.cpp:117
cover_goals.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
bmct::do_conversion
void do_conversion()
Definition: bmc.cpp:118
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:163
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
xml_expr.h
literal_expr.h
validation_modet::INVARIANT
@ INVARIANT
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:86
tvt::is_true
bool is_true() const
Definition: threeval.h:25
messaget::statistics
mstreamt & statistics() const
Definition: message.h:406
json_stringt
Definition: json.h:214