cprover
static_verifier.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: goto-analyzer
4 
5 Author: Martin Brain, martin.brain@cs.ox.ac.uk
6 
7 \*******************************************************************/
8 
9 #include "static_verifier.h"
10 
11 #include <util/json_irep.h>
12 #include <util/message.h>
13 #include <util/namespace.h>
14 #include <util/options.h>
15 #include <util/range.h>
16 
18 
19 #include <analyses/ai.h>
20 
22 {
23  // clang-format off
25  // clang-format on
28 };
29 
31  const abstract_goto_modelt &abstract_goto_model,
32  const ai_baset &ai,
33  propertiest &properties)
34 {
35  const namespacet ns{abstract_goto_model.get_symbol_table()};
36  // this is mutable because we want to change the property status
37  // in this loop
38  for(auto &property : properties)
39  {
40  auto &property_status = property.second.status;
41  const goto_programt::const_targett &property_location = property.second.pc;
42  exprt condition = property_location->get_condition();
43  const std::shared_ptr<const ai_baset::statet> predecessor_state_copy =
44  ai.abstract_state_before(property_location);
45  // simplify the condition given the domain information we have
46  // about the state right before the assertion is evaluated
47  predecessor_state_copy->ai_simplify(condition, ns);
48  // if the condition simplifies to true the assertion always succeeds
49  if(condition.is_true())
50  {
51  property_status = property_statust::PASS;
52  }
53  // if the condition simplifies to false the assertion always fails
54  else if(condition.is_false())
55  {
56  property_status = property_statust::FAIL;
57  }
58  // if the domain state is bottom then the assertion is definitely
59  // unreachable
60  else if(predecessor_state_copy->is_bottom())
61  {
62  property_status = property_statust::NOT_REACHABLE;
63  }
64  // if the condition isn't definitely true, false or unreachable
65  // we don't know whether or not it may fail
66  else
67  {
68  property_status = property_statust::UNKNOWN;
69  }
70  }
71 }
72 
74 static const char *message(const static_verifier_resultt::statust &status)
75 {
76  switch(status)
77  {
79  return "SUCCESS";
81  return "FAILURE (if reachable)";
83  return "SUCCESS (unreachable)";
85  return "UNKNOWN";
86  }
88 }
89 
91  const std::vector<static_verifier_resultt> &results,
92  messaget &m,
93  std::ostream &out)
94 {
95  m.status() << "Writing JSON report" << messaget::eom;
96  out << make_range(results)
97  .map([](const static_verifier_resultt &result) {
98  return json_objectt{
99  {"status", json_stringt{message(result.status)}},
100  {"sourceLocation", json(result.source_location)}};
101  })
102  .collect<json_arrayt>();
103 }
104 
106  const std::vector<static_verifier_resultt> &results,
107  messaget &m,
108  std::ostream &out)
109 {
110  m.status() << "Writing XML report" << messaget::eom;
111 
112  xmlt xml_result{"cprover"};
113 
114  for(const auto &result : results)
115  {
116  xmlt &x = xml_result.new_element("result");
117 
118  switch(result.status)
119  {
121  x.set_attribute("status", "SUCCESS");
122  break;
123 
125  x.set_attribute("status", "FAILURE (if reachable)");
126  break;
127 
129  x.set_attribute("status", "SUCCESS (unreachable)");
130  break;
131 
133  x.set_attribute("status", "UNKNOWN");
134  }
135 
136  x.set_attribute("file", id2string(result.source_location.get_file()));
137  x.set_attribute("line", id2string(result.source_location.get_line()));
138  x.set_attribute(
139  "description", id2string(result.source_location.get_comment()));
140  }
141 
142  out << xml_result;
143 }
144 
146  const std::vector<static_verifier_resultt> &results,
147  const namespacet &ns,
148  std::ostream &out)
149 {
150  irep_idt last_function_id;
151 
152  for(const auto &result : results)
153  {
154  if(last_function_id != result.function_id)
155  {
156  if(!last_function_id.empty())
157  out << '\n';
158  last_function_id = result.function_id;
159  const auto &symbol = ns.lookup(last_function_id);
160  out << "******** Function " << symbol.display_name() << '\n';
161  }
162 
163  out << '[' << result.source_location.get_property_id() << ']' << ' ';
164 
165  out << result.source_location;
166 
167  if(!result.source_location.get_comment().empty())
168  out << ", " << result.source_location.get_comment();
169 
170  out << ": ";
171 
172  switch(result.status)
173  {
175  out << "Success";
176  break;
177 
179  out << "Failure (if reachable)";
180  break;
181 
183  out << "Success (unreachable)";
184  break;
185 
187  out << "Unknown";
188  break;
189  }
190 
191  out << '\n';
192  }
193 }
194 
196  const std::vector<static_verifier_resultt> &results,
197  const namespacet &ns,
198  messaget &m)
199 {
200  irep_idt last_function_id;
201  irep_idt function_file;
202 
203  for(const auto &result : results)
204  {
205  if(last_function_id != result.function_id)
206  {
207  if(!last_function_id.empty())
208  m.status() << '\n';
209  last_function_id = result.function_id;
210  const auto &symbol = ns.lookup(last_function_id);
211  m.status() << messaget::underline << "Function " << symbol.display_name();
212  function_file = symbol.location.get_file();
213  if(!function_file.empty())
214  m.status() << ' ' << function_file;
215  if(!symbol.location.get_line().empty())
216  m.status() << ':' << symbol.location.get_line();
218  }
219 
220  m.result() << messaget::faint << '['
221  << result.source_location.get_property_id() << ']'
222  << messaget::reset;
223 
224  if(
225  !result.source_location.get_file().empty() &&
226  result.source_location.get_file() != function_file)
227  {
228  m.result() << " file " << result.source_location.get_file();
229  }
230 
231  if(!result.source_location.get_line().empty())
232  m.result() << " line " << result.source_location.get_line();
233 
234  if(!result.source_location.get_comment().empty())
235  m.result() << ' ' << result.source_location.get_comment();
236 
237  m.result() << ": ";
238 
239  switch(result.status)
240  {
242  m.result() << m.green << "SUCCESS" << m.reset;
243  break;
244 
246  m.result() << m.red << "FAILURE" << m.reset << " (if reachable)";
247  break;
248 
250  m.result() << m.green << "SUCCESS" << m.reset << " (unreachable)";
251  break;
252 
254  m.result() << m.yellow << "UNKNOWN" << m.reset;
255  break;
256  }
257 
258  m.result() << messaget::eom;
259  }
260 
261  if(!results.empty())
262  m.result() << '\n';
263 }
264 
266 check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
267 {
268  if(domain.is_bottom())
269  {
271  }
272 
273  domain.ai_simplify(e, ns);
274  if(e.is_true())
275  {
277  }
278  else if(e.is_false())
279  {
281  }
282  else
283  {
285  }
286 
287  UNREACHABLE;
288 }
289 
298  const goto_modelt &goto_model,
299  const ai_baset &ai,
300  const optionst &options,
301  message_handlert &message_handler,
302  std::ostream &out)
303 {
304  std::size_t pass = 0, fail = 0, unknown = 0;
305 
306  namespacet ns(goto_model.symbol_table);
307 
308  messaget m(message_handler);
309  m.status() << "Checking assertions" << messaget::eom;
310 
311  std::vector<static_verifier_resultt> results;
312 
313  for(const auto &f : goto_model.goto_functions.function_map)
314  {
315  const auto &symbol = ns.lookup(f.first);
316 
317  m.progress() << "Checking " << symbol.display_name() << messaget::eom;
318 
319  if(!f.second.body.has_assertion())
320  continue;
321 
322  forall_goto_program_instructions(i_it, f.second.body)
323  {
324  if(!i_it->is_assert())
325  continue;
326 
327  exprt e(i_it->get_condition());
328 
329  results.push_back(static_verifier_resultt());
330  auto &result = results.back();
331 
332  // If there are multiple, distinct histories that reach the same location
333  // we can get better results by checking with each individually rather
334  // than merging all of them and doing one check.
335  const auto trace_set_pointer =
336  ai.abstract_traces_before(i_it); // Keep a pointer so refcount > 0
337  const auto &trace_set = *trace_set_pointer;
338 
339  if(trace_set.size() == 0) // i.e. unreachable
340  {
341  result.status = static_verifier_resultt::BOTTOM;
342  ++pass;
343  }
344  else if(trace_set.size() == 1)
345  {
346  auto dp = ai.abstract_state_before(i_it);
347 
348  result.status = check_assertion(*dp, e, ns);
349  switch(result.status)
350  {
352  ++pass;
353  break;
355  ++pass;
356  break;
358  ++fail;
359  break;
361  ++unknown;
362  break;
363  default:
364  UNREACHABLE;
365  }
366  }
367  else
368  {
369  // Multiple traces, verify against each one
370  std::size_t unreachable_traces = 0;
371  std::size_t true_traces = 0;
372  std::size_t false_traces = 0;
373  std::size_t unknown_traces = 0;
374 
375  for(const auto &trace_ptr : trace_set)
376  {
377  auto dp = ai.abstract_state_before(trace_ptr);
378 
379  result.status = check_assertion(*dp, e, ns);
380  switch(result.status)
381  {
383  ++unreachable_traces;
384  break;
386  ++true_traces;
387  break;
389  ++false_traces;
390  break;
392  ++unknown_traces;
393  break;
394  default:
395  UNREACHABLE;
396  }
397  }
398 
399  // Join the results
400  if(unknown_traces != 0)
401  {
402  // If any trace is unknown, the final result must be unknown
403  result.status = static_verifier_resultt::UNKNOWN;
404  ++unknown;
405  }
406  else
407  {
408  if(false_traces == 0)
409  {
410  // Definitely true; the only question is how
411  ++pass;
412  if(true_traces == 0)
413  {
414  // Definitely not reachable
415  INVARIANT(
416  unreachable_traces == trace_set.size(),
417  "All traces must not reach the assertion");
418  result.status = static_verifier_resultt::BOTTOM;
419  }
420  else
421  {
422  // At least one trace (may) reach it.
423  // All traces that reach it are safe.
424  result.status = static_verifier_resultt::TRUE;
425  }
426  }
427  else
428  {
429  // At lease one trace (may) reach it and it is false on that trace
430  if(true_traces == 0)
431  {
432  // All traces that (may) reach it are false
433  ++fail;
434  result.status = static_verifier_resultt::FALSE;
435  }
436  else
437  {
438  // The awkward case, there are traces that (may) reach it and
439  // some are true, some are false. It is not entirely fair to say
440  // "FAILURE (if reachable)" because it's a bit more complex than
441  // that, "FAILURE (if reachable via a particular trace)" would be
442  // more accurate summary of what we know at this point.
443  // Given that all results of FAILURE from this analysis are
444  // caveated with some reachability questions, the following is not
445  // entirely unreasonable.
446  ++fail;
447  result.status = static_verifier_resultt::FALSE;
448  }
449  }
450  }
451  }
452 
453  result.source_location = i_it->source_location;
454  result.function_id = f.first;
455  }
456  }
457 
458  if(options.get_bool_option("json"))
459  {
460  static_verifier_json(results, m, out);
461  }
462  else if(options.get_bool_option("xml"))
463  {
464  static_verifier_xml(results, m, out);
465  }
466  else if(options.get_bool_option("text"))
467  {
468  static_verifier_text(results, ns, out);
469  }
470  else
471  {
472  static_verifier_console(results, ns, m);
473  }
474 
475  m.status() << m.bold << "Summary: "
476  << pass << " pass, "
477  << fail << " fail if reachable, "
478  << unknown << " unknown"
479  << m.reset << messaget::eom;
480 
481  return false;
482 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
propertiest
std::unordered_map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:75
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:71
property_statust::FAIL
@ FAIL
The property was violated.
abstract_goto_modelt::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
static_verifier_resultt::FALSE
@ FALSE
Definition: static_verifier.cpp:24
check_assertion
static static_verifier_resultt::statust check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
Definition: static_verifier.cpp:266
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
optionst
Definition: options.h:23
static_verifier
void static_verifier(const abstract_goto_modelt &abstract_goto_model, const ai_baset &ai, propertiest &properties)
Use the information from the abstract interpreter to fill out the statuses of the passed properties.
Definition: static_verifier.cpp:30
messaget::status
mstreamt & status() const
Definition: message.h:414
static_verifier.h
static_verifier_json
static void static_verifier_json(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
Definition: static_verifier.cpp:90
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
ai_baset::abstract_state_before
virtual cstate_ptrt abstract_state_before(locationt l) const
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
Definition: ai.h:221
options.h
Options.
messaget::eom
static eomt eom
Definition: message.h:297
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
static_verifier_resultt::source_location
source_locationt source_location
Definition: static_verifier.cpp:26
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
property_statust::NOT_REACHABLE
@ NOT_REACHABLE
The property was proven to be unreachable.
namespace.h
json_irep.h
Util.
static_verifier_resultt::statust
statust
Definition: static_verifier.cpp:24
ai_domain_baset::is_bottom
virtual bool is_bottom() const =0
source_locationt::get_line
const irep_idt & get_line() const
Definition: source_location.h:46
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:101
json_objectt
Definition: json.h:300
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
messaget::green
static const commandt green
render text with green foreground color
Definition: message.h:349
messaget::result
mstreamt & result() const
Definition: message.h:409
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:385
messaget::bold
static const commandt bold
render text with bold font
Definition: message.h:382
messaget::yellow
static const commandt yellow
render text with yellow foreground color
Definition: message.h:352
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
static_verifier_text
static void static_verifier_text(const std::vector< static_verifier_resultt > &results, const namespacet &ns, std::ostream &out)
Definition: static_verifier.cpp:145
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
static_verifier_console
static void static_verifier_console(const std::vector< static_verifier_resultt > &results, const namespacet &ns, messaget &m)
Definition: static_verifier.cpp:195
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
ai_baset::abstract_traces_before
virtual ctrace_set_ptrt abstract_traces_before(locationt l) const
Returns all of the histories that have reached the start of the instruction.
Definition: ai.h:194
message_handlert
Definition: message.h:28
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
dstringt::empty
bool empty() const
Definition: dstring.h:88
ai.h
Abstract Interpretation.
xmlt
Definition: xml.h:21
property_statust::UNKNOWN
@ UNKNOWN
The checker was unable to determine the status of the property.
source_locationt
Definition: source_location.h:20
static_verifier_resultt::UNKNOWN
@ UNKNOWN
Definition: static_verifier.cpp:24
messaget::red
static const commandt red
render text with red foreground color
Definition: message.h:346
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
xmlt::set_attribute
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
static_verifier_resultt::BOTTOM
@ BOTTOM
Definition: static_verifier.cpp:24
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:36
messaget::underline
static const commandt underline
render underlined text
Definition: message.h:391
property_statust::PASS
@ PASS
The property was not violated.
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
static_verifier_resultt::TRUE
@ TRUE
Definition: static_verifier.cpp:24
abstract_goto_modelt
Abstract interface to eager or lazy GOTO models.
Definition: abstract_goto_model.h:21
messaget::progress
mstreamt & progress() const
Definition: message.h:424
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
ai_domain_baset::ai_simplify
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition: ai_domain.h:167
message.h
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
static_verifier_xml
static void static_verifier_xml(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
Definition: static_verifier.cpp:105
static_verifier_resultt::function_id
irep_idt function_id
Definition: static_verifier.cpp:27
static_verifier_resultt::status
enum static_verifier_resultt::statust status
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
json_stringt
Definition: json.h:270
static_verifier_resultt
Definition: static_verifier.cpp:22