CBMC
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 
23 std::string as_string(const ai_verifier_statust &status)
24 {
25  switch(status)
26  {
28  return "SUCCESS";
30  return "FAILURE (if reachable)";
32  return "SUCCESS (unreachable)";
34  return "UNKNOWN";
35  }
37 }
38 
40 {
41  json_arrayt unknown_json;
42  for(const auto &trace_ptr : this->unknown_histories)
43  unknown_json.push_back(trace_ptr->output_json());
44 
45  json_arrayt false_json;
46  for(const auto &trace_ptr : this->false_histories)
47  false_json.push_back(trace_ptr->output_json());
48 
49  return json_objectt{
50  {"status", json_stringt{as_string(this->status)}},
51  {"sourceLocation", json(this->source_location)},
52  {"unknownHistories", unknown_json},
53  {"falseHistories", false_json},
54  };
55 }
56 
58 {
59  xmlt x("result");
60 
61  x.set_attribute("status", as_string(this->status));
62 
63  // DEPRECATED(SINCE(2020, 12, 2, "Remove and use the structured version"));
64  // Unstructured partial output of source location is not great...
65  x.set_attribute("file", id2string(this->source_location.get_file()));
66  x.set_attribute("line", id2string(this->source_location.get_line()));
67 
68  // ... this is better
70 
71  // ( get_comment is not output as part of xml(source_location) )
72  x.set_attribute(
73  "description", id2string(this->source_location.get_comment()));
74 
75  xmlt &unknown_xml = x.new_element("unknown");
76  for(const auto &trace_ptr : this->unknown_histories)
77  unknown_xml.new_element(trace_ptr->output_xml());
78 
79  xmlt &false_xml = x.new_element("false");
80  for(const auto &trace_ptr : this->false_histories)
81  false_xml.new_element(trace_ptr->output_xml());
82 
83  return x;
84 }
85 
87 check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
88 {
89  if(domain.is_bottom())
90  {
92  }
93 
94  domain.ai_simplify(e, ns);
95  if(e.is_true())
96  {
98  }
99  else if(e.is_false())
100  {
102  }
103  else
104  {
106  }
107 
108  UNREACHABLE;
109 }
110 
112  const ai_baset &ai,
113  goto_programt::const_targett assert_location,
114  irep_idt func_id,
115  const namespacet &ns)
116 {
117  PRECONDITION(assert_location->is_assert());
118  exprt e(assert_location->condition());
119 
120  // If there are multiple, distinct histories that reach the same location
121  // we can get better results by checking with each individually rather
122  // than merging all of them and doing one check.
123  const auto trace_set_pointer = ai.abstract_traces_before(
124  assert_location); // Keep a pointer so refcount > 0
125  const auto &trace_set = *trace_set_pointer;
126 
127  if(trace_set.size() == 0) // i.e. unreachable
128  {
130  }
131  else if(trace_set.size() == 1)
132  {
133  auto dp = ai.abstract_state_before(assert_location);
134 
135  status = check_assertion(*dp, e, ns);
137  {
138  false_histories = trace_set;
139  }
141  {
142  unknown_histories = trace_set;
143  }
144  }
145  else
146  {
147  // Multiple traces, verify against each one
148  std::size_t unreachable_traces = 0;
149  std::size_t true_traces = 0;
150  std::size_t false_traces = 0;
151  std::size_t unknown_traces = 0;
152 
153  for(const auto &trace_ptr : trace_set)
154  {
155  auto dp = ai.abstract_state_before(trace_ptr);
156 
157  status = check_assertion(*dp, e, ns);
158  switch(status)
159  {
161  ++unreachable_traces;
162  break;
164  ++true_traces;
165  break;
167  ++false_traces;
168  false_histories.insert(trace_ptr);
169  break;
171  ++unknown_traces;
172  unknown_histories.insert(trace_ptr);
173  break;
174  default:
175  UNREACHABLE;
176  }
177  }
178 
179  // Join the results
180  if(unknown_traces != 0)
181  {
182  // If any trace is unknown, the final result must be unknown
184  }
185  else
186  {
187  if(false_traces == 0)
188  {
189  // Definitely true; the only question is how
190  if(true_traces == 0)
191  {
192  // Definitely not reachable
193  INVARIANT(
194  unreachable_traces == trace_set.size(),
195  "All traces must not reach the assertion");
197  }
198  else
199  {
200  // At least one trace (may) reach it.
201  // All traces that reach it are safe.
203  }
204  }
205  else
206  {
207  // At lease one trace (may) reach it and it is false on that trace
208  if(true_traces == 0)
209  {
210  // All traces that (may) reach it are false
212  }
213  else
214  {
215  // The awkward case, there are traces that (may) reach it and
216  // some are true, some are false. It is not entirely fair to say
217  // "FAILURE (if reachable)" because it's a bit more complex than
218  // that, and so the best we can say is UNKNOWN.
220  }
221  }
222  }
223  }
224 
225  source_location = assert_location->source_location();
226  function_id = func_id;
227 }
228 
230  const abstract_goto_modelt &abstract_goto_model,
231  const ai_baset &ai,
232  propertiest &properties)
233 {
234  const namespacet ns{abstract_goto_model.get_symbol_table()};
235  // this is mutable because we want to change the property status
236  // in this loop
237  for(auto &property : properties)
238  {
239  auto &property_status = property.second.status;
240  const goto_programt::const_targett &property_location = property.second.pc;
241 
242  const static_verifier_resultt result(ai, property_location, "unused", ns);
243 
244  switch(result.status)
245  {
247  // if the condition simplifies to true the assertion always succeeds
248  property_status = property_statust::PASS;
249  break;
251  // if the condition simplifies to false the assertion always fails
252  property_status = property_statust::FAIL;
253  break;
255  // if the domain state is bottom then the assertion is definitely
256  // unreachable
257  property_status = property_statust::NOT_REACHABLE;
258  break;
260  // if the condition isn't definitely true, false or unreachable
261  // we don't know whether or not it may fail
262  property_status = property_statust::UNKNOWN;
263  break;
264  default:
265  UNREACHABLE;
266  }
267  }
268 }
269 
271  const std::vector<static_verifier_resultt> &results,
272  messaget &m,
273  std::ostream &out)
274 {
275  m.status() << "Writing JSON report" << messaget::eom;
276  out << make_range(results)
277  .map([](const static_verifier_resultt &result) {
278  return result.output_json();
279  })
280  .collect<json_arrayt>();
281 }
282 
284  const std::vector<static_verifier_resultt> &results,
285  messaget &m,
286  std::ostream &out)
287 {
288  m.status() << "Writing XML report" << messaget::eom;
289 
290  xmlt xml_result{"cprover"};
291  for(const auto &result : results)
292  xml_result.new_element(result.output_xml());
293 
294  out << xml_result;
295 }
296 
298  const std::vector<static_verifier_resultt> &results,
299  const namespacet &ns,
300  std::ostream &out)
301 {
302  irep_idt last_function_id;
303 
304  for(const auto &result : results)
305  {
306  if(last_function_id != result.function_id)
307  {
308  if(!last_function_id.empty())
309  out << '\n';
310  last_function_id = result.function_id;
311  const auto &symbol = ns.lookup(last_function_id);
312  out << "******** Function " << symbol.display_name() << '\n';
313  }
314 
315  out << '[' << result.source_location.get_property_id() << ']' << ' ';
316 
317  out << result.source_location;
318 
319  if(!result.source_location.get_comment().empty())
320  out << ", " << result.source_location.get_comment();
321 
322  out << ": " << as_string(result.status) << '\n';
323  }
324 }
325 
327  const std::vector<static_verifier_resultt> &results,
328  const namespacet &ns,
329  messaget &m)
330 {
331  irep_idt last_function_id;
332  irep_idt function_file;
333 
334  for(const auto &result : results)
335  {
336  if(last_function_id != result.function_id)
337  {
338  if(!last_function_id.empty())
339  m.status() << '\n';
340  last_function_id = result.function_id;
341  const auto &symbol = ns.lookup(last_function_id);
342  m.status() << messaget::underline << "Function " << symbol.display_name();
343  function_file = symbol.location.get_file();
344  if(!function_file.empty())
345  m.status() << ' ' << function_file;
346  if(!symbol.location.get_line().empty())
347  m.status() << ':' << symbol.location.get_line();
349  }
350 
351  m.result() << messaget::faint << '['
352  << result.source_location.get_property_id() << ']'
353  << messaget::reset;
354 
355  if(
356  !result.source_location.get_file().empty() &&
357  result.source_location.get_file() != function_file)
358  {
359  m.result() << " file " << result.source_location.get_file();
360  }
361 
362  if(!result.source_location.get_line().empty())
363  m.result() << " line " << result.source_location.get_line();
364 
365  if(!result.source_location.get_comment().empty())
366  m.result() << ' ' << result.source_location.get_comment();
367 
368  m.result() << ": ";
369 
370  switch(result.status)
371  {
373  m.result() << m.green << "SUCCESS" << m.reset;
374  break;
375 
377  m.result() << m.red << "FAILURE" << m.reset << " (if reachable)";
378  break;
379 
381  m.result() << m.green << "SUCCESS" << m.reset << " (unreachable)";
382  break;
383 
385  m.result() << m.yellow << "UNKNOWN" << m.reset;
386  break;
387  }
388 
389  m.result() << messaget::eom;
390  }
391 
392  if(!results.empty())
393  m.result() << '\n';
394 }
395 
404  const goto_modelt &goto_model,
405  const ai_baset &ai,
406  const optionst &options,
407  message_handlert &message_handler,
408  std::ostream &out)
409 {
410  std::size_t pass = 0, fail = 0, unknown = 0;
411 
412  namespacet ns(goto_model.symbol_table);
413 
414  messaget m(message_handler);
415  m.status() << "Checking assertions" << messaget::eom;
416 
417  std::vector<static_verifier_resultt> results;
418 
419  for(const auto &f : goto_model.goto_functions.function_map)
420  {
421  const auto &symbol = ns.lookup(f.first);
422 
423  m.progress() << "Checking " << symbol.display_name() << messaget::eom;
424 
425  if(!f.second.body.has_assertion())
426  continue;
427 
428  forall_goto_program_instructions(i_it, f.second.body)
429  {
430  if(!i_it->is_assert())
431  continue;
432 
433  results.push_back(static_verifier_resultt(ai, i_it, f.first, ns));
434 
435  switch(results.back().status)
436  {
438  ++pass;
439  break;
441  ++pass;
442  break;
444  ++fail;
445  break;
447  ++unknown;
448  break;
449  default:
450  UNREACHABLE;
451  }
452  }
453  }
454 
455  if(options.get_bool_option("json"))
456  {
457  static_verifier_json(results, m, out);
458  }
459  else if(options.get_bool_option("xml"))
460  {
461  static_verifier_xml(results, m, out);
462  }
463  else if(options.get_bool_option("text"))
464  {
465  static_verifier_text(results, ns, out);
466  }
467  else
468  {
469  static_verifier_console(results, ns, m);
470  }
471 
472  m.status() << m.bold << "Summary: " << pass << " pass, " << fail
473  << " fail if reachable, " << unknown << " unknown" << m.reset
474  << messaget::eom;
475 
476  return false;
477 }
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:117
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
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
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:54
virtual bool is_bottom() const =0
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition: ai_domain.h:149
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
Base class for all expressions.
Definition: expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:27
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:34
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
instructionst::const_iterator const_targett
Definition: goto_program.h:615
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:94
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:148
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
The result of verifying a single assertion As well as the status of the assertion (see above),...
ai_verifier_statust status
static_verifier_resultt(const ai_baset &ai, goto_programt::const_targett assert_location, irep_idt func_id, const namespacet &ns)
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
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:40
Options.
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:110
@ 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::map< irep_idt, property_infot > propertiest
A map of property IDs to property infos.
Definition: properties.h:76
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:522
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
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)
static ai_verifier_statust check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
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 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)
ai_verifier_statust
An ai_baset contains zero or more histories that reach a location.