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 <iostream>
15 
16 #include <util/time_stopping.h>
17 #include <util/xml.h>
18 #include <util/json.h>
19 
20 #include <solvers/sat/satcheck.h>
22 
26 
27 #include "bv_cbmc.h"
28 
30 {
31  for(auto &g : goal_map)
32  {
33  // failed already?
34  if(g.second.status==goalt::statust::FAILURE)
35  continue;
36 
37  // check whether failed
38  for(auto &c : g.second.instances)
39  {
40  literalt cond=c->cond_literal;
41 
42  if(solver.l_get(cond).is_false())
43  {
44  g.second.status=goalt::statust::FAILURE;
45  symex_target_equationt::SSA_stepst::iterator next=c;
46  next++; // include the assertion
48  g.second.goto_trace);
49  break;
50  }
51  }
52  }
53 }
54 
56 {
57  status() << "Passing problem to " << solver.decision_procedure_text() << eom;
58 
60 
61  // stop the time
62  absolute_timet sat_start=current_time();
63 
65 
66  // Collect _all_ goals in `goal_map'.
67  // This maps property IDs to 'goalt'
69  forall_goto_program_instructions(i_it, f_it->second.body)
70  if(i_it->is_assert())
71  goal_map[i_it->source_location.get_property_id()]=goalt(*i_it);
72 
73  // get the conditions for these goals from formula
74  // collect all 'instances' of the properties
75  for(symex_target_equationt::SSA_stepst::iterator
76  it=bmc.equation.SSA_steps.begin();
77  it!=bmc.equation.SSA_steps.end();
78  it++)
79  {
80  if(it->is_assert())
81  {
82  irep_idt property_id;
83 
84  if(it->source.pc->is_assert())
85  property_id=it->source.pc->source_location.get_property_id();
86  else if(it->source.pc->is_goto())
87  {
88  // this is likely an unwinding assertion
89  property_id=id2string(
90  it->source.pc->source_location.get_function())+".unwind."+
91  std::to_string(it->source.pc->loop_number);
92  goal_map[property_id].description=it->comment;
93  }
94  else
95  continue;
96 
97  goal_map[property_id].instances.push_back(it);
98  }
99  }
100 
102 
103  cover_goalst cover_goals(solver);
104 
106  cover_goals.register_observer(*this);
107 
108  for(const auto &g : goal_map)
109  {
110  // Our goal is to falsify a property, i.e., we will
111  // add the negation of the property as goal.
112  literalt p=!solver.convert(g.second.as_expr());
113  cover_goals.add(p);
114  }
115 
116  status() << "Running " << solver.decision_procedure_text() << eom;
117 
118  bool error=false;
119 
120  decision_proceduret::resultt result=cover_goals();
121 
123  {
124  error=true;
125  for(auto &g : goal_map)
126  if(g.second.status==goalt::statust::UNKNOWN)
127  g.second.status=goalt::statust::ERROR;
128  }
129  else
130  {
131  for(auto &g : goal_map)
132  if(g.second.status==goalt::statust::UNKNOWN)
133  g.second.status=goalt::statust::SUCCESS;
134  }
135 
136  // output runtime
137 
138  {
139  absolute_timet sat_stop=current_time();
140  status() << "Runtime decision procedure: "
141  << (sat_stop-sat_start) << "s" << eom;
142  }
143 
144  // report
145  report(cover_goals);
146 
147  if(error)
149 
150  bool safe=(cover_goals.number_covered()==0);
151 
152  if(safe)
153  bmc.report_success(); // legacy, might go away
154  else
155  bmc.report_failure(); // legacy, might go away
156 
158 }
159 
161 {
162  switch(bmc.ui)
163  {
165  {
166  status() << "\n** Results:" << eom;
167 
168  for(const auto &goal_pair : goal_map)
169  status() << "[" << goal_pair.first << "] "
170  << goal_pair.second.description << ": "
171  << goal_pair.second.status_string()
172  << eom;
173 
174  if(bmc.options.get_bool_option("trace"))
175  {
176  for(const auto &g : goal_map)
177  if(g.second.status==goalt::statust::FAILURE)
178  {
179  std::cout << "\n" << "Trace for " << g.first << ":" << "\n";
180  show_goto_trace(std::cout, bmc.ns, g.second.goto_trace);
181  }
182  }
183 
184  status() << "\n** " << cover_goals.number_covered()
185  << " of " << cover_goals.size() << " failed ("
186  << cover_goals.iterations() << " iteration"
187  << (cover_goals.iterations()==1?"":"s")
188  << ")" << eom;
189  }
190  break;
191 
193  {
194  for(const auto &g : goal_map)
195  {
196  xmlt xml_result("result");
197  xml_result.set_attribute("property", id2string(g.first));
198  xml_result.set_attribute("status", g.second.status_string());
199 
200  if(g.second.status==goalt::statust::FAILURE)
201  convert(bmc.ns, g.second.goto_trace, xml_result.new_element());
202 
203  std::cout << xml_result << "\n";
204  }
205  break;
206  }
207 
209  {
210  json_objectt json_result;
211  json_arrayt &result_array=json_result["result"].make_array();
212 
213  for(const auto &g : goal_map)
214  {
215  json_objectt &result=result_array.push_back().make_object();
216  result["property"]=json_stringt(id2string(g.first));
217  result["description"]=json_stringt(id2string(g.second.description));
218  result["status"]=json_stringt(g.second.status_string());
219 
220  if(g.second.status==goalt::statust::FAILURE)
221  {
222  jsont &json_trace=result["trace"];
223  convert(bmc.ns, g.second.goto_trace, json_trace);
224  }
225  }
226 
227  std::cout << ",\n" << json_result;
228  }
229  break;
230  }
231 }
232 
236 {
237  bmc_all_propertiest bmc_all_properties(goto_functions, solver, *this);
238  bmc_all_properties.set_message_handler(get_message_handler());
239  return bmc_all_properties();
240 }
bool is_false() const
Definition: threeval.h:26
mstreamt & result()
Definition: message.h:233
void do_conversion()
Definition: bmc.cpp:118
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()
mstreamt & status()
Definition: message.h:238
Definition: json.h:21
virtual void report_failure()
Definition: bmc.cpp:193
void show_goto_trace(std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace)
Definition: goto_trace.cpp:239
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual void goal_covered(const cover_goalst::goalt &)
json_arrayt & make_array()
Definition: json.h:228
namespacet ns
Definition: bmc.h:71
jsont & push_back(const jsont &json)
Definition: json.h:157
Traces of GOTO Programs.
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
Definition: xml.h:18
Traces of GOTO Programs.
virtual literalt convert(const exprt &expr)=0
Time Stopping.
virtual void set_message_handler(message_handlert &_message_handler)
Definition: message.h:122
void convert(const goto_functionst::goto_functiont &function, xmlt &xml)
takes a goto_function and creates an according xml structure
Symbolic Execution of ANSI-C.
std::size_t number_covered() const
Definition: cover_goals.h:51
const optionst & options
Definition: bmc.h:69
xmlt & new_element(const std::string &name)
Definition: xml.h:86
language_uit::uit ui
Definition: bmc.h:77
void add(const literalt condition)
Definition: cover_goals.h:68
unsigned iterations() const
Definition: cover_goals.h:56
virtual tvt l_get(literalt a) const =0
message_handlert & get_message_handler()
Definition: message.h:127
absolute_timet current_time()
virtual void report(const cover_goalst &cover_goals)
Traces of GOTO Programs.
Try to cover some given set of goals incrementally.
Definition: cover_goals.h:21
mstreamt & error()
Definition: message.h:223
symex_target_equationt equation
Definition: bmc.h:72
json_objectt & make_object()
Definition: json.h:234
void register_observer(observert &o)
Definition: cover_goals.h:84
virtual void report_success()
Definition: bmc.cpp:165
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
goalst::size_type size() const
Definition: cover_goals.h:61
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)
virtual std::string decision_procedure_text() const =0