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 <chrono>
15 
16 #include <util/xml.h>
17 #include <util/json.h>
18 
19 #include <solvers/sat/satcheck.h>
21 
25 
26 #include "bv_cbmc.h"
27 
29 {
30  for(auto &g : goal_map)
31  {
32  // failed already?
33  if(g.second.status==goalt::statust::FAILURE)
34  continue;
35 
36  // check whether failed
37  for(auto &c : g.second.instances)
38  {
39  literalt cond=c->cond_literal;
40 
41  if(solver.l_get(cond).is_false())
42  {
43  g.second.status=goalt::statust::FAILURE;
44  symex_target_equationt::SSA_stepst::iterator next=c;
45  next++; // include the assertion
47  g.second.goto_trace);
48  break;
49  }
50  }
51  }
52 }
53 
55 {
56  status() << "Passing problem to " << solver.decision_procedure_text() << eom;
57 
59 
60  auto solver_start=std::chrono::steady_clock::now();
61 
63 
64  // Collect _all_ goals in `goal_map'.
65  // This maps property IDs to 'goalt'
67  forall_goto_program_instructions(i_it, f_it->second.body)
68  if(i_it->is_assert())
69  goal_map[i_it->source_location.get_property_id()]=goalt(*i_it);
70 
71  // get the conditions for these goals from formula
72  // collect all 'instances' of the properties
73  for(symex_target_equationt::SSA_stepst::iterator
74  it=bmc.equation.SSA_steps.begin();
75  it!=bmc.equation.SSA_steps.end();
76  it++)
77  {
78  if(it->is_assert())
79  {
80  irep_idt property_id;
81 
82  if(it->source.pc->is_assert())
83  property_id=it->source.pc->source_location.get_property_id();
84  else if(it->source.pc->is_goto())
85  {
86  // this is likely an unwinding assertion
87  property_id=id2string(
88  it->source.pc->source_location.get_function())+".unwind."+
89  std::to_string(it->source.pc->loop_number);
90  goal_map[property_id].description=it->comment;
91  }
92  else
93  continue;
94 
95  goal_map[property_id].instances.push_back(it);
96  }
97  }
98 
100 
101  cover_goalst cover_goals(solver);
102 
104  cover_goals.register_observer(*this);
105 
106  for(const auto &g : goal_map)
107  {
108  // Our goal is to falsify a property, i.e., we will
109  // add the negation of the property as goal.
110  literalt p=!solver.convert(g.second.as_expr());
111  cover_goals.add(p);
112  }
113 
114  status() << "Running " << solver.decision_procedure_text() << eom;
115 
116  bool error=false;
117 
118  decision_proceduret::resultt result=cover_goals();
119 
121  {
122  error=true;
123  for(auto &g : goal_map)
124  if(g.second.status==goalt::statust::UNKNOWN)
125  g.second.status=goalt::statust::ERROR;
126  }
127  else
128  {
129  for(auto &g : goal_map)
130  if(g.second.status==goalt::statust::UNKNOWN)
131  g.second.status=goalt::statust::SUCCESS;
132  }
133 
134  {
135  auto solver_stop = std::chrono::steady_clock::now();
136 
137  status() << "Runtime decision procedure: "
138  << std::chrono::duration<double>(solver_stop-solver_start).count()
139  << "s" << eom;
140  }
141 
142  // report
143  report(cover_goals);
144 
145  if(error)
147 
148  bool safe=(cover_goals.number_covered()==0);
149 
150  if(safe)
151  bmc.report_success(); // legacy, might go away
152  else
153  bmc.report_failure(); // legacy, might go away
154 
156 }
157 
159 {
160  switch(bmc.ui)
161  {
163  {
164  result() << "\n** Results:" << eom;
165 
166  for(const auto &goal_pair : goal_map)
167  result() << "[" << goal_pair.first << "] "
168  << goal_pair.second.description << ": "
169  << goal_pair.second.status_string()
170  << eom;
171 
172  if(bmc.options.get_bool_option("trace"))
173  {
174  for(const auto &g : goal_map)
175  if(g.second.status==goalt::statust::FAILURE)
176  {
177  result() << "\n" << "Trace for " << g.first << ":" << "\n";
178  show_goto_trace(result(), bmc.ns, g.second.goto_trace);
179  }
180  }
181  result() << eom;
182 
183  status() << "\n** " << cover_goals.number_covered()
184  << " of " << cover_goals.size() << " failed ("
185  << cover_goals.iterations() << " iteration"
186  << (cover_goals.iterations()==1?"":"s")
187  << ")" << eom;
188  }
189  break;
190 
192  {
193  for(const auto &g : goal_map)
194  {
195  xmlt xml_result("result");
196  xml_result.set_attribute("property", id2string(g.first));
197  xml_result.set_attribute("status", g.second.status_string());
198 
199  if(g.second.status==goalt::statust::FAILURE)
200  convert(bmc.ns, g.second.goto_trace, xml_result.new_element());
201 
202  result() << xml_result;
203  }
204  break;
205  }
206 
208  {
209  json_stream_objectt &json_result =
211  json_stream_arrayt &result_array =
212  json_result.push_back_stream_array("result");
213 
214  for(const auto &g : goal_map)
215  {
217  result["property"] = json_stringt(g.first);
218  result["description"] = json_stringt(g.second.description);
219  result["status"]=json_stringt(g.second.status_string());
220 
221  if(g.second.status==goalt::statust::FAILURE)
222  {
223  json_stream_arrayt &json_trace =
224  result.push_back_stream_array("trace");
225  convert<json_stream_arrayt>(
226  bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
227  }
228  }
229  }
230  break;
231  }
232 }
233 
235  const goto_functionst &goto_functions,
237 {
238  bmc_all_propertiest bmc_all_properties(goto_functions, solver, *this);
239  bmc_all_properties.set_message_handler(get_message_handler());
240  return bmc_all_properties();
241 }
bool is_false() const
Definition: threeval.h:26
void do_conversion()
Definition: bmc.cpp:112
const goto_functionst & goto_functions
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
virtual resultt all_properties(const goto_functionst &goto_functions, prop_convt &solver)
safety_checkert::resultt operator()()
virtual void do_before_solving()
Provides methods for streaming JSON objects.
Definition: json_stream.h:139
json_stream_objectt & push_back_stream_object()
Add a JSON object child stream.
Definition: json_stream.cpp:82
virtual void report_failure()
Definition: bmc.cpp:176
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:247
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
virtual void goal_covered(const cover_goalst::goalt &)
namespacet ns
Definition: bmc.h:182
Some safety properties were violated.
ui_message_handlert::uit ui
Definition: bmc.h:189
int solver(std::istream &in)
Traces of GOTO Programs.
Safety is unknown due to an error during safety checking.
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
Provides methods for streaming JSON arrays.
Definition: json_stream.h:92
mstreamt & error() const
Definition: message.h:302
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
Symbolic Execution of ANSI-C.
std::size_t number_covered() const
Definition: cover_goals.h:53
No safety properties were violated.
const optionst & options
Definition: bmc.h:177
xmlt & new_element(const std::string &name)
Definition: xml.h:86
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
mstreamt & result() const
Definition: message.h:312
mstreamt & status() const
Definition: message.h:317
virtual void report(const cover_goalst &cover_goals)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
json_stream_arrayt & push_back_stream_array(const std::string &key)
Add a JSON array stream for a specific key.
symex_target_equationt equation
Definition: bmc.h:183
void register_observer(observert &o)
Definition: cover_goals.h:86
virtual void report_success()
Definition: bmc.cpp:149
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
goalst::size_type size() const
Definition: cover_goals.h:63
Traces of GOTO Programs.
virtual std::string decision_procedure_text() const =0