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