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  build_goto_trace(bmc.equation, c, solver, bmc.ns, g.second.goto_trace);
45  break;
46  }
47  }
48  }
49 }
50 
52 {
53  status() << "Passing problem to " << solver.decision_procedure_text() << eom;
54 
56 
57  auto solver_start=std::chrono::steady_clock::now();
58 
60 
61  // Collect _all_ goals in `goal_map'.
62  // This maps property IDs to 'goalt'
64  forall_goto_program_instructions(i_it, f_it->second.body)
65  if(i_it->is_assert())
66  goal_map[i_it->source_location.get_property_id()]=goalt(*i_it);
67 
68  // get the conditions for these goals from formula
69  // collect all 'instances' of the properties
70  for(symex_target_equationt::SSA_stepst::iterator
71  it=bmc.equation.SSA_steps.begin();
72  it!=bmc.equation.SSA_steps.end();
73  it++)
74  {
75  if(it->is_assert())
76  {
77  irep_idt property_id;
78 
79  if(it->source.pc->is_assert())
80  property_id=it->source.pc->source_location.get_property_id();
81  else if(it->source.pc->is_goto())
82  {
83  // this is likely an unwinding assertion
84  property_id=id2string(
85  it->source.pc->source_location.get_function())+".unwind."+
86  std::to_string(it->source.pc->loop_number);
87  goal_map[property_id].description=it->comment;
88  }
89  else
90  continue;
91 
92  goal_map[property_id].instances.push_back(it);
93  }
94  }
95 
97 
98  cover_goalst cover_goals(solver);
99 
101  cover_goals.register_observer(*this);
102 
103  for(const auto &g : goal_map)
104  {
105  // Our goal is to falsify a property, i.e., we will
106  // add the negation of the property as goal.
107  literalt p=!solver.convert(g.second.as_expr());
108  cover_goals.add(p);
109  }
110 
111  status() << "Running " << solver.decision_procedure_text() << eom;
112 
113  bool error=false;
114 
115  decision_proceduret::resultt result=cover_goals();
116 
118  {
119  error=true;
120  for(auto &g : goal_map)
121  if(g.second.status==goalt::statust::UNKNOWN)
122  g.second.status=goalt::statust::ERROR;
123  }
124  else
125  {
126  for(auto &g : goal_map)
127  if(g.second.status==goalt::statust::UNKNOWN)
128  g.second.status=goalt::statust::SUCCESS;
129  }
130 
131  {
132  auto solver_stop = std::chrono::steady_clock::now();
133 
134  status() << "Runtime decision procedure: "
135  << std::chrono::duration<double>(solver_stop-solver_start).count()
136  << "s" << eom;
137  }
138 
139  // report
140  report(cover_goals);
141 
142  if(error)
144 
145  bool safe=(cover_goals.number_covered()==0);
146 
147  if(safe)
148  bmc.report_success(); // legacy, might go away
149  else
150  bmc.report_failure(); // legacy, might go away
151 
153 }
154 
156 {
157  switch(bmc.ui)
158  {
160  {
161  result() << "\n** Results:" << eom;
162 
163  for(const auto &goal_pair : goal_map)
164  result() << "[" << goal_pair.first << "] "
165  << goal_pair.second.description << ": "
166  << goal_pair.second.status_string()
167  << eom;
168 
169  if(bmc.options.get_bool_option("trace"))
170  {
171  for(const auto &g : goal_map)
172  if(g.second.status==goalt::statust::FAILURE)
173  {
174  result() << "\n" << "Trace for " << g.first << ":" << "\n";
176  result(), bmc.ns, g.second.goto_trace, bmc.trace_options());
177  result() << eom;
178  }
179  }
180 
181  status() << "\n** " << cover_goals.number_covered()
182  << " of " << cover_goals.size() << " failed ("
183  << cover_goals.iterations() << " iteration"
184  << (cover_goals.iterations()==1?"":"s")
185  << ")" << eom;
186  }
187  break;
188 
190  {
191  for(const auto &g : goal_map)
192  {
193  xmlt xml_result("result");
194  xml_result.set_attribute("property", id2string(g.first));
195  xml_result.set_attribute("status", g.second.status_string());
196 
197  if(g.second.status==goalt::statust::FAILURE)
198  convert(bmc.ns, g.second.goto_trace, xml_result.new_element());
199 
200  result() << xml_result;
201  }
202  break;
203  }
204 
206  {
207  json_stream_objectt &json_result =
209  json_stream_arrayt &result_array =
210  json_result.push_back_stream_array("result");
211 
212  for(const auto &g : goal_map)
213  {
215  result["property"] = json_stringt(g.first);
216  result["description"] = json_stringt(g.second.description);
217  result["status"]=json_stringt(g.second.status_string());
218 
219  if(g.second.status==goalt::statust::FAILURE)
220  {
221  json_stream_arrayt &json_trace =
222  result.push_back_stream_array("trace");
223  convert<json_stream_arrayt>(
224  bmc.ns, g.second.goto_trace, json_trace, bmc.trace_options());
225  }
226  }
227  }
228  break;
229  }
230 }
231 
233  const goto_functionst &goto_functions,
235 {
236  bmc_all_propertiest bmc_all_properties(goto_functions, solver, *this);
237  bmc_all_properties.set_message_handler(get_message_handler());
238  return bmc_all_properties();
239 }
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)
const goto_functionst & goto_functions
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
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
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
No safety properties were violated.
const optionst & options
Definition: bmc.h:177
xmlt & new_element(const std::string &name)
Definition: xml.h:86
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.
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, const trace_optionst &options)
Definition: goto_trace.cpp:288
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