cprover
all_properties.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 "all_properties_class.h"
13 
14 #include <algorithm>
15 #include <chrono>
16 
17 #include <util/xml.h>
18 #include <util/json.h>
19 
20 #include <solvers/sat/satcheck.h>
22 
26 
28 {
29  for(auto &g : goal_map)
30  {
31  // failed already?
32  if(g.second.status==goalt::statust::FAILURE)
33  continue;
34 
35  // check whether failed
36  for(auto &c : g.second.instances)
37  {
38  literalt cond=c->cond_literal;
39 
40  if(solver.l_get(cond).is_false())
41  {
42  g.second.status=goalt::statust::FAILURE;
43  build_goto_trace(bmc.equation, c, solver, bmc.ns, g.second.goto_trace);
44  break;
45  }
46  }
47  }
48 }
49 
51 {
52  status() << "Passing problem to " << solver.decision_procedure_text() << eom;
53 
55 
56  auto solver_start=std::chrono::steady_clock::now();
57 
59 
60  // Collect _all_ goals in `goal_map'.
61  // This maps property IDs to 'goalt'
63  forall_goto_program_instructions(i_it, f_it->second.body)
64  if(i_it->is_assert())
65  goal_map[i_it->source_location.get_property_id()]=goalt(*i_it);
66 
67  // get the conditions for these goals from formula
68  // collect all 'instances' of the properties
69  for(symex_target_equationt::SSA_stepst::iterator
70  it=bmc.equation.SSA_steps.begin();
71  it!=bmc.equation.SSA_steps.end();
72  it++)
73  {
74  if(it->is_assert())
75  {
76  irep_idt property_id;
77 
78  if(it->source.pc->is_assert())
79  property_id=it->source.pc->source_location.get_property_id();
80  else if(it->source.pc->is_goto())
81  {
82  // this is likely an unwinding assertion
83  property_id=id2string(
84  it->source.pc->source_location.get_function())+".unwind."+
85  std::to_string(it->source.pc->loop_number);
86  goal_map[property_id].description=it->comment;
87  }
88  else
89  continue;
90 
91  goal_map[property_id].instances.push_back(it);
92  }
93  }
94 
96 
97  cover_goalst cover_goals(solver);
98 
100  cover_goals.register_observer(*this);
101 
102  for(const auto &g : goal_map)
103  {
104  // Our goal is to falsify a property, i.e., we will
105  // add the negation of the property as goal.
106  literalt p=!solver.convert(g.second.as_expr());
107  cover_goals.add(p);
108  }
109 
110  status() << "Running " << solver.decision_procedure_text() << eom;
111 
112  bool error=false;
113 
114  decision_proceduret::resultt result=cover_goals();
115 
117  {
118  error=true;
119  for(auto &g : goal_map)
120  if(g.second.status==goalt::statust::UNKNOWN)
121  g.second.status=goalt::statust::ERROR;
122  }
123  else
124  {
125  for(auto &g : goal_map)
126  if(g.second.status==goalt::statust::UNKNOWN)
127  g.second.status=goalt::statust::SUCCESS;
128  }
129 
130  {
131  auto solver_stop = std::chrono::steady_clock::now();
132 
133  status() << "Runtime decision procedure: "
134  << std::chrono::duration<double>(solver_stop-solver_start).count()
135  << "s" << eom;
136  }
137 
138  // report
139  report(cover_goals);
140 
141  if(error)
143 
144  bool safe=(cover_goals.number_covered()==0);
145 
146  if(safe)
147  bmc.report_success(); // legacy, might go away
148  else
149  bmc.report_failure(); // legacy, might go away
150 
152 }
153 
155 {
156  switch(bmc.ui_message_handler.get_ui())
157  {
159  {
160  result() << "\n** Results:" << eom;
161 
162  // collect goals in a vector
163  std::vector<goal_mapt::const_iterator> goals;
164 
165  for(auto g_it = goal_map.begin(); g_it != goal_map.end(); g_it++)
166  goals.push_back(g_it);
167 
168  // now determine an ordering for those goals:
169  // 1. alphabetical ordering of file name
170  // 2. numerical ordering of line number
171  // 3. alphabetical ordering of goal ID
172  std::sort(
173  goals.begin(),
174  goals.end(),
175  [](goal_mapt::const_iterator git1, goal_mapt::const_iterator git2) {
176  const auto &g1 = git1->second.source_location;
177  const auto &g2 = git2->second.source_location;
178  if(g1.get_file() != g2.get_file())
179  return id2string(g1.get_file()) < id2string(g2.get_file());
180  else if(!g1.get_line().empty() && !g2.get_line().empty())
181  return std::stoul(id2string(g1.get_line())) <
182  std::stoul(id2string(g2.get_line()));
183  else
184  return id2string(git1->first) < id2string(git2->first);
185  });
186 
187  // now show in the order we have determined
188 
189  irep_idt previous_function;
190  irep_idt current_file;
191  for(const auto &g : goals)
192  {
193  const auto &l = g->second.source_location;
194 
195  if(l.get_function() != previous_function)
196  {
197  if(!previous_function.empty())
198  result() << '\n';
199  previous_function = l.get_function();
200  if(!previous_function.empty())
201  {
202  current_file = l.get_file();
203  if(!current_file.empty())
204  result() << current_file << ' ';
205  if(!l.get_function().empty())
206  result() << "function " << l.get_function();
207  result() << eom;
208  }
209  }
210 
211  result() << faint << '[' << g->first << "] " << reset;
212 
213  if(l.get_file() != current_file)
214  result() << "file " << l.get_file() << ' ';
215 
216  if(!l.get_line().empty())
217  result() << "line " << l.get_line() << ' ';
218 
219  result() << g->second.description << ": ";
220 
221  if(g->second.status == goalt::statust::SUCCESS)
222  result() << green;
223  else
224  result() << red;
225 
226  result() << g->second.status_string() << reset << eom;
227  }
228 
229  if(bmc.options.get_bool_option("trace"))
230  {
231  for(const auto &g : goal_map)
232  if(g.second.status==goalt::statust::FAILURE)
233  {
234  result() << "\n" << "Trace for " << g.first << ":" << "\n";
236  result(), bmc.ns, g.second.goto_trace, bmc.trace_options());
237  result() << eom;
238  }
239  }
240 
241  status() << "\n** " << cover_goals.number_covered()
242  << " of " << cover_goals.size() << " failed ("
243  << cover_goals.iterations() << " iteration"
244  << (cover_goals.iterations()==1?"":"s")
245  << ")" << eom;
246  }
247  break;
248 
250  {
251  for(const auto &g : goal_map)
252  {
253  xmlt xml_result("result");
254  xml_result.set_attribute("property", id2string(g.first));
255  xml_result.set_attribute("status", g.second.status_string());
256 
257  if(g.second.status==goalt::statust::FAILURE)
258  convert(bmc.ns, g.second.goto_trace, xml_result.new_element());
259 
260  result() << xml_result;
261  }
262  break;
263  }
264 
266  {
267  if(result().tellp() > 0)
268  result() << eom; // force end of previous message
269  json_stream_objectt &json_result =
271  json_stream_arrayt &result_array =
272  json_result.push_back_stream_array("result");
273 
274  for(const auto &g : goal_map)
275  {
277  result["property"] = json_stringt(g.first);
278  result["description"] = json_stringt(g.second.description);
279  result["status"]=json_stringt(g.second.status_string());
280 
281  if(g.second.status==goalt::statust::FAILURE)
282  {
283  json_stream_arrayt &json_trace =
284  result.push_back_stream_array("trace");
285  convert<json_stream_arrayt>(
286  bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
287  }
288  }
289  }
290  break;
291  }
292 }
293 
295  const goto_functionst &goto_functions,
297 {
298  bmc_all_propertiest bmc_all_properties(goto_functions, solver, *this);
299  bmc_all_properties.set_message_handler(get_message_handler());
300  return bmc_all_properties();
301 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
bmct::trace_options
trace_optionst trace_options()
Definition: bmc.h:191
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
bmct::report_success
virtual void report_success()
Definition: bmc.cpp:155
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
prop_convt
Definition: prop_conv.h:27
bmc_all_propertiest::goal_map
goal_mapt goal_map
Definition: all_properties_class.h:87
messaget::status
mstreamt & status() const
Definition: message.h:401
safety_checkert::resultt::SAFE
No safety properties were violated.
bmc_all_propertiest::report
virtual void report(const cover_goalst &cover_goals)
Definition: all_properties.cpp:154
bmc_all_propertiest::goalt
Definition: all_properties_class.h:36
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_all_propertiest::do_before_solving
virtual void do_before_solving()
Definition: all_properties_class.h:95
cover_goalst
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
xml.h
cover_goalst::number_covered
std::size_t number_covered() const
Definition: cover_goals.h:53
json_stream_objectt::push_back_stream_array
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
Definition: json_stream.cpp:120
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
messaget::green
static const commandt green
render text with green foreground color
Definition: message.h:336
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
messaget::result
mstreamt & result() const
Definition: message.h:396
messaget::error
mstreamt & error() const
Definition: message.h:386
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:372
bmct::ns
namespacet ns
Definition: bmc.h:171
bmc_all_propertiest::operator()
safety_checkert::resultt operator()()
Definition: all_properties.cpp:50
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
ui_message_handlert::uit::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
bmct::options
const optionst & options
Definition: bmc.h:166
xml_goto_trace.h
json_stream_arrayt
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
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
cover_goalst::size
goalst::size_type size() const
Definition: cover_goals.h:63
decision_proceduret::resultt::D_ERROR
dstringt::empty
bool empty() const
Definition: dstring.h:75
json_goto_trace.h
tvt::is_false
bool is_false() const
Definition: threeval.h:26
safety_checkert::resultt::ERROR
Safety is unknown due to an error during safety checking.
xmlt
Definition: xml.h:18
prop_convt::l_get
virtual tvt l_get(literalt a) const =0
safety_checkert::resultt::UNSAFE
Some safety properties were violated.
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
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
satcheck.h
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
safety_checkert::resultt
resultt
Definition: safety_checker.h:33
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
show_goto_trace
void show_goto_trace(messaget::mstreamt &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:748
bmc_all_propertiest::solver
prop_convt & solver
Definition: all_properties_class.h:91
messaget::red
static const commandt red
render text with red foreground color
Definition: message.h:333
ui_message_handlert::uit::PLAIN
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
bmc_all_propertiest::goto_functions
const goto_functionst & goto_functions
Definition: all_properties_class.h:90
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:360
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
bmct::all_properties
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
Definition: all_properties.cpp:294
bmct::equation
symex_target_equationt equation
Definition: bmc.h:172
build_goto_trace.h
literalt
Definition: literal.h:24
json.h
bmc_all_propertiest::goal_covered
virtual void goal_covered(const cover_goalst::goalt &)
Definition: all_properties.cpp:27
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
bmct::report_failure
virtual void report_failure()
Definition: bmc.cpp:187
cover_goalst::goalt
Definition: cover_goals.h:38
bmc_all_propertiest
Definition: all_properties_class.h:19
all_properties_class.h
bmct::do_conversion
void do_conversion()
Definition: bmc.cpp:118
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
literal_expr.h
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:86
bmc_all_propertiest::bmc
bmct & bmc
Definition: all_properties_class.h:92
json_stringt
Definition: json.h:214