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 
23 std::string as_string(const ai_verifier_statust &status)
24 {
25  switch(status)
26  {
28  return "SUCCESS";
29  case ai_verifier_statust::FALSE_IF_REACHABLE:
30  return "FAILURE (if reachable)";
31  case ai_verifier_statust::NOT_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  {
91  return ai_verifier_statust::NOT_REACHABLE;
92  }
93 
94  domain.ai_simplify(e, ns);
95  if(e.is_true())
96  {
98  }
99  else if(e.is_false())
100  {
101  return ai_verifier_statust::FALSE_IF_REACHABLE;
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->get_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  {
129  status = ai_verifier_statust::NOT_REACHABLE;
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);
136  if(status == ai_verifier_statust::FALSE_IF_REACHABLE)
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  {
160  case ai_verifier_statust::NOT_REACHABLE:
161  ++unreachable_traces;
162  break;
164  ++true_traces;
165  break;
166  case ai_verifier_statust::FALSE_IF_REACHABLE:
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");
196  status = ai_verifier_statust::NOT_REACHABLE;
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
211  status = ai_verifier_statust::FALSE_IF_REACHABLE;
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, "FAILURE (if reachable via a particular trace)" would be
219  // more accurate summary of what we know at this point.
220  // Given that all results of FAILURE from this analysis are
221  // caveated with some reachability questions, the following is not
222  // entirely unreasonable.
223  status = ai_verifier_statust::FALSE_IF_REACHABLE;
224  }
225  }
226  }
227  }
228 
229  source_location = assert_location->source_location;
230  function_id = func_id;
231 }
232 
234  const abstract_goto_modelt &abstract_goto_model,
235  const ai_baset &ai,
236  propertiest &properties)
237 {
238  const namespacet ns{abstract_goto_model.get_symbol_table()};
239  // this is mutable because we want to change the property status
240  // in this loop
241  for(auto &property : properties)
242  {
243  auto &property_status = property.second.status;
244  const goto_programt::const_targett &property_location = property.second.pc;
245 
246  const static_verifier_resultt result(ai, property_location, "unused", ns);
247 
248  switch(result.status)
249  {
251  // if the condition simplifies to true the assertion always succeeds
252  property_status = property_statust::PASS;
253  break;
254  case ai_verifier_statust::FALSE_IF_REACHABLE:
255  // if the condition simplifies to false the assertion always fails
256  property_status = property_statust::FAIL;
257  break;
258  case ai_verifier_statust::NOT_REACHABLE:
259  // if the domain state is bottom then the assertion is definitely
260  // unreachable
261  property_status = property_statust::NOT_REACHABLE;
262  break;
264  // if the condition isn't definitely true, false or unreachable
265  // we don't know whether or not it may fail
266  property_status = property_statust::UNKNOWN;
267  break;
268  default:
269  UNREACHABLE;
270  }
271  }
272 }
273 
275  const std::vector<static_verifier_resultt> &results,
276  messaget &m,
277  std::ostream &out)
278 {
279  m.status() << "Writing JSON report" << messaget::eom;
280  out << make_range(results)
281  .map([](const static_verifier_resultt &result) {
282  return result.output_json();
283  })
284  .collect<json_arrayt>();
285 }
286 
288  const std::vector<static_verifier_resultt> &results,
289  messaget &m,
290  std::ostream &out)
291 {
292  m.status() << "Writing XML report" << messaget::eom;
293 
294  xmlt xml_result{"cprover"};
295  for(const auto &result : results)
296  xml_result.new_element(result.output_xml());
297 
298  out << xml_result;
299 }
300 
302  const std::vector<static_verifier_resultt> &results,
303  const namespacet &ns,
304  std::ostream &out)
305 {
306  irep_idt last_function_id;
307 
308  for(const auto &result : results)
309  {
310  if(last_function_id != result.function_id)
311  {
312  if(!last_function_id.empty())
313  out << '\n';
314  last_function_id = result.function_id;
315  const auto &symbol = ns.lookup(last_function_id);
316  out << "******** Function " << symbol.display_name() << '\n';
317  }
318 
319  out << '[' << result.source_location.get_property_id() << ']' << ' ';
320 
321  out << result.source_location;
322 
323  if(!result.source_location.get_comment().empty())
324  out << ", " << result.source_location.get_comment();
325 
326  out << ": " << as_string(result.status) << '\n';
327  }
328 }
329 
331  const std::vector<static_verifier_resultt> &results,
332  const namespacet &ns,
333  messaget &m)
334 {
335  irep_idt last_function_id;
336  irep_idt function_file;
337 
338  for(const auto &result : results)
339  {
340  if(last_function_id != result.function_id)
341  {
342  if(!last_function_id.empty())
343  m.status() << '\n';
344  last_function_id = result.function_id;
345  const auto &symbol = ns.lookup(last_function_id);
346  m.status() << messaget::underline << "Function " << symbol.display_name();
347  function_file = symbol.location.get_file();
348  if(!function_file.empty())
349  m.status() << ' ' << function_file;
350  if(!symbol.location.get_line().empty())
351  m.status() << ':' << symbol.location.get_line();
353  }
354 
355  m.result() << messaget::faint << '['
356  << result.source_location.get_property_id() << ']'
357  << messaget::reset;
358 
359  if(
360  !result.source_location.get_file().empty() &&
361  result.source_location.get_file() != function_file)
362  {
363  m.result() << " file " << result.source_location.get_file();
364  }
365 
366  if(!result.source_location.get_line().empty())
367  m.result() << " line " << result.source_location.get_line();
368 
369  if(!result.source_location.get_comment().empty())
370  m.result() << ' ' << result.source_location.get_comment();
371 
372  m.result() << ": ";
373 
374  switch(result.status)
375  {
377  m.result() << m.green << "SUCCESS" << m.reset;
378  break;
379 
380  case ai_verifier_statust::FALSE_IF_REACHABLE:
381  m.result() << m.red << "FAILURE" << m.reset << " (if reachable)";
382  break;
383 
384  case ai_verifier_statust::NOT_REACHABLE:
385  m.result() << m.green << "SUCCESS" << m.reset << " (unreachable)";
386  break;
387 
389  m.result() << m.yellow << "UNKNOWN" << m.reset;
390  break;
391  }
392 
393  m.result() << messaget::eom;
394  }
395 
396  if(!results.empty())
397  m.result() << '\n';
398 }
399 
408  const goto_modelt &goto_model,
409  const ai_baset &ai,
410  const optionst &options,
411  message_handlert &message_handler,
412  std::ostream &out)
413 {
414  std::size_t pass = 0, fail = 0, unknown = 0;
415 
416  namespacet ns(goto_model.symbol_table);
417 
418  messaget m(message_handler);
419  m.status() << "Checking assertions" << messaget::eom;
420 
421  std::vector<static_verifier_resultt> results;
422 
423  for(const auto &f : goto_model.goto_functions.function_map)
424  {
425  const auto &symbol = ns.lookup(f.first);
426 
427  m.progress() << "Checking " << symbol.display_name() << messaget::eom;
428 
429  if(!f.second.body.has_assertion())
430  continue;
431 
432  forall_goto_program_instructions(i_it, f.second.body)
433  {
434  if(!i_it->is_assert())
435  continue;
436 
437  results.push_back(static_verifier_resultt(ai, i_it, f.first, ns));
438 
439  switch(results.back().status)
440  {
441  case ai_verifier_statust::NOT_REACHABLE:
442  ++pass;
443  break;
445  ++pass;
446  break;
447  case ai_verifier_statust::FALSE_IF_REACHABLE:
448  ++fail;
449  break;
451  ++unknown;
452  break;
453  default:
454  UNREACHABLE;
455  }
456  }
457  }
458 
459  if(options.get_bool_option("json"))
460  {
461  static_verifier_json(results, m, out);
462  }
463  else if(options.get_bool_option("xml"))
464  {
465  static_verifier_xml(results, m, out);
466  }
467  else if(options.get_bool_option("text"))
468  {
469  static_verifier_text(results, ns, out);
470  }
471  else
472  {
473  static_verifier_console(results, ns, m);
474  }
475 
476  m.status() << m.bold << "Summary: "
477  << pass << " pass, "
478  << fail << " fail if reachable, "
479  << unknown << " unknown"
480  << m.reset << messaget::eom;
481 
482  return false;
483 }
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
ai_verifier_statust::UNKNOWN
@ UNKNOWN
abstract_goto_modelt::get_symbol_table
virtual const symbol_tablet & get_symbol_table() const =0
Accessor to get the symbol table.
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:233
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:274
goto_model.h
Symbol Table + CFG.
exprt
Base class for all expressions.
Definition: expr.h:54
xml_irep.h
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:222
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:60
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
namespace.h
jsont
Definition: json.h:27
json_irep.h
Util.
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:69
json_arrayt
Definition: json.h:165
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
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:141
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:49
xml
xmlt xml(const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:105
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:301
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:330
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
static_verifier_resultt::unknown_histories
ai_history_baset::trace_sett unknown_histories
Definition: static_verifier.h:71
static_verifier_resultt
The result of verifying a single assertion As well as the status of the assertion (see above),...
Definition: static_verifier.h:66
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
ai_verifier_statust::TRUE
@ TRUE
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:195
check_assertion
static ai_verifier_statust check_assertion(const ai_domain_baset &domain, exprt e, const namespacet &ns)
Definition: static_verifier.cpp:87
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
static_verifier_resultt::source_location
source_locationt source_location
Definition: static_verifier.h:69
ai.h
Abstract Interpretation.
xmlt
Definition: xml.h:21
property_statust::UNKNOWN
@ UNKNOWN
The checker was unable to determine the status of the property.
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:198
static_verifier_resultt::function_id
irep_idt function_id
Definition: static_verifier.h:70
optionst::get_bool_option
bool get_bool_option(const std::string &option) const
Definition: options.cpp:44
ai_verifier_statust
ai_verifier_statust
An ai_baset contains zero or more histories that reach a location.
Definition: static_verifier.h:51
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:120
static_verifier_resultt::false_histories
ai_history_baset::trace_sett false_histories
Definition: static_verifier.h:72
as_string
std::string as_string(const ai_verifier_statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:23
static_verifier_resultt::output_json
jsont output_json(void) const
Definition: static_verifier.cpp:39
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
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:564
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
static_verifier_resultt::status
ai_verifier_statust status
Definition: static_verifier.h:68
ai_domain_baset::ai_simplify
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition: ai_domain.h:150
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:59
static_verifier_resultt::static_verifier_resultt
static_verifier_resultt(const ai_baset &ai, goto_programt::const_targett assert_location, irep_idt func_id, const namespacet &ns)
Definition: static_verifier.cpp:111
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:287
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1180
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:95
json_stringt
Definition: json.h:270
static_verifier_resultt::output_xml
xmlt output_xml(void) const
Definition: static_verifier.cpp:57