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_expr.h>
12 #include <util/message.h>
13 #include <util/namespace.h>
14 #include <util/options.h>
15 
17 
18 #include <analyses/ai.h>
19 
21 {
22  // clang-format off
24  // clang-format on
27 };
28 
30  const std::vector<static_verifier_resultt> &results,
31  messaget &m,
32  std::ostream &out)
33 {
34  m.status() << "Writing JSON report" << messaget::eom;
35 
36  json_arrayt json_result;
37 
38  for(const auto &result : results)
39  {
40  json_objectt &j = json_result.push_back().make_object();
41 
42  switch(result.status)
43  {
45  j["status"] = json_stringt("SUCCESS");
46  break;
47 
49  j["status"] = json_stringt("FAILURE (if reachable)");
50  break;
51 
53  j["status"] = json_stringt("SUCCESS (unreachable)");
54  break;
55 
57  j["status"] = json_stringt("UNKNOWN");
58  break;
59  }
60 
61  j["sourceLocation"] = json(result.source_location);
62  }
63 
64  out << json_result;
65 }
66 
67 static void static_verifier_xml(
68  const std::vector<static_verifier_resultt> &results,
69  messaget &m,
70  std::ostream &out)
71 {
72  m.status() << "Writing XML report" << messaget::eom;
73 
74  xmlt xml_result;
75 
76  for(const auto &result : results)
77  {
78  xmlt &x = xml_result.new_element("result");
79 
80  switch(result.status)
81  {
83  x.set_attribute("status", "SUCCESS");
84  break;
85 
87  x.set_attribute("status", "FAILURE (if reachable)");
88  break;
89 
91  x.set_attribute("status", "SUCCESS (unreachable)");
92  break;
93 
95  x.set_attribute("status", "UNKNOWN");
96  }
97 
98  x.set_attribute("file", id2string(result.source_location.get_file()));
99  x.set_attribute("line", id2string(result.source_location.get_line()));
100  x.set_attribute(
101  "description", id2string(result.source_location.get_comment()));
102  }
103 
104  out << xml_result;
105 }
106 
108  const std::vector<static_verifier_resultt> &results,
109  const namespacet &ns,
110  std::ostream &out)
111 {
112  irep_idt last_function_id;
113 
114  for(const auto &result : results)
115  {
116  if(last_function_id != result.function_id)
117  {
118  if(!last_function_id.empty())
119  out << '\n';
120  last_function_id = result.function_id;
121  const auto &symbol = ns.lookup(last_function_id);
122  out << "******** Function " << symbol.display_name() << '\n';
123  }
124 
125  out << '[' << result.source_location.get_property_id() << ']' << ' ';
126 
127  out << result.source_location;
128 
129  if(!result.source_location.get_comment().empty())
130  out << ", " << result.source_location.get_comment();
131 
132  out << ": ";
133 
134  switch(result.status)
135  {
137  out << "Success";
138  break;
139 
141  out << "Failure (if reachable)";
142  break;
143 
145  out << "Success (unreachable)";
146  break;
147 
149  out << "Unknown";
150  break;
151  }
152 
153  out << '\n';
154  }
155 }
156 
158  const std::vector<static_verifier_resultt> &results,
159  const namespacet &ns,
160  messaget &m)
161 {
162  irep_idt last_function_id;
163  irep_idt function_file;
164 
165  for(const auto &result : results)
166  {
167  if(last_function_id != result.function_id)
168  {
169  if(!last_function_id.empty())
170  m.status() << '\n';
171  last_function_id = result.function_id;
172  const auto &symbol = ns.lookup(last_function_id);
173  m.status() << messaget::underline << "Function " << symbol.display_name();
174  function_file = symbol.location.get_file();
175  if(!function_file.empty())
176  m.status() << ' ' << function_file;
177  if(!symbol.location.get_line().empty())
178  m.status() << ':' << symbol.location.get_line();
180  }
181 
182  m.result() << messaget::faint << '['
183  << result.source_location.get_property_id() << ']'
184  << messaget::reset;
185 
186  if(
187  !result.source_location.get_file().empty() &&
188  result.source_location.get_file() != function_file)
189  {
190  m.result() << " file " << result.source_location.get_file();
191  }
192 
193  if(!result.source_location.get_line().empty())
194  m.result() << " line " << result.source_location.get_line();
195 
196  if(!result.source_location.get_comment().empty())
197  m.result() << ' ' << result.source_location.get_comment();
198 
199  m.result() << ": ";
200 
201  switch(result.status)
202  {
204  m.result() << m.green << "SUCCESS" << m.reset;
205  break;
206 
208  m.result() << m.red << "FAILURE" << m.reset << " (if reachable)";
209  break;
210 
212  m.result() << m.green << "SUCCESS" << m.reset << " (unreachable)";
213  break;
214 
216  m.result() << m.yellow << "UNKNOWN" << m.reset;
217  break;
218  }
219 
220  m.result() << messaget::eom;
221  }
222 
223  if(!results.empty())
224  m.result() << '\n';
225 }
226 
235  const goto_modelt &goto_model,
236  const ai_baset &ai,
237  const optionst &options,
238  message_handlert &message_handler,
239  std::ostream &out)
240 {
241  std::size_t pass = 0, fail = 0, unknown = 0;
242 
243  namespacet ns(goto_model.symbol_table);
244 
245  messaget m(message_handler);
246  m.status() << "Checking assertions" << messaget::eom;
247 
248  std::vector<static_verifier_resultt> results;
249 
250  for(const auto &f : goto_model.goto_functions.function_map)
251  {
252  const auto &symbol = ns.lookup(f.first);
253 
254  m.progress() << "Checking " << symbol.display_name() << messaget::eom;
255 
256  if(!f.second.body.has_assertion())
257  continue;
258 
259  forall_goto_program_instructions(i_it, f.second.body)
260  {
261  if(!i_it->is_assert())
262  continue;
263 
264  exprt e(i_it->guard);
265  auto dp = ai.abstract_state_before(i_it);
266  const ai_domain_baset &domain(*dp);
267  domain.ai_simplify(e, ns);
268 
269  results.push_back(static_verifier_resultt());
270  auto &result = results.back();
271 
272  if(e.is_true())
273  {
274  result.status = static_verifier_resultt::TRUE;
275  ++pass;
276  }
277  else if(e.is_false())
278  {
279  result.status = static_verifier_resultt::FALSE;
280  ++fail;
281  }
282  else if(domain.is_bottom())
283  {
284  result.status = static_verifier_resultt::BOTTOM;
285  ++pass;
286  }
287  else
288  {
289  result.status = static_verifier_resultt::UNKNOWN;
290  ++unknown;
291  }
292 
293  result.source_location = i_it->source_location;
294  result.function_id = f.first;
295  }
296  }
297 
298  if(options.get_bool_option("json"))
299  {
300  static_verifier_json(results, m, out);
301  }
302  else if(options.get_bool_option("xml"))
303  {
304  static_verifier_xml(results, m, out);
305  }
306  else if(options.get_bool_option("text"))
307  {
308  static_verifier_text(results, ns, out);
309  }
310  else
311  {
312  static_verifier_console(results, ns, m);
313  }
314 
315  m.status() << m.bold << "Summary: "
316  << pass << " pass, "
317  << fail << " fail if reachable, "
318  << unknown << " unknown"
319  << m.reset << messaget::eom;
320 
321  return false;
322 }
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition: ai_domain.h:105
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
static const commandt bold
render text with bold font
Definition: message.h:369
mstreamt & progress() const
Definition: message.h:411
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
static void static_verifier_xml(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
function_mapt function_map
enum static_verifier_resultt::@0 status
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Get a copy of the abstract state before the given instruction, without needing to know what kind of d...
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
virtual bool is_bottom() const =0
jsont & push_back(const jsont &json)
Definition: json.h:163
static const commandt underline
render underlined text
Definition: message.h:378
Symbol Table + CFG.
const irep_idt & get_line() const
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
source_locationt source_location
Definition: message.h:236
bool get_bool_option(const std::string &option) const
Definition: options.cpp:42
Expressions in JSON.
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:175
static const commandt red
render text with red foreground color
Definition: message.h:333
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
static void static_verifier_json(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
Definition: xml.h:18
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
static void static_verifier_text(const std::vector< static_verifier_resultt > &results, const namespacet &ns, std::ostream &out)
static const commandt faint
render text with faint font
Definition: message.h:372
static eomt eom
Definition: message.h:284
bool static_verifier(const goto_modelt &goto_model, const ai_baset &ai, const optionst &options, message_handlert &message_handler, std::ostream &out)
Runs the analyzer and then prints out the domain.
const irep_idt & get_file() const
mstreamt & result() const
Definition: message.h:396
xmlt & new_element(const std::string &key)
Definition: xml.h:86
mstreamt & status() const
Definition: message.h:401
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:54
source_locationt source_location
Options.
json_objectt & make_object()
Definition: json.h:290
const irep_idt & get_comment() const
static const commandt green
render text with green foreground color
Definition: message.h:336
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
bool empty() const
Definition: dstring.h:75
static const commandt yellow
render text with yellow foreground color
Definition: message.h:339
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
static void static_verifier_console(const std::vector< static_verifier_resultt > &results, const namespacet &ns, messaget &m)