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 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:72
json
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
optionst
Definition: options.h:22
messaget::status
mstreamt & status() const
Definition: message.h:401
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:29
static_verifier
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.
Definition: static_verifier.cpp:234
goto_model.h
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:24
options.h
messaget::eom
static eomt eom
Definition: message.h:284
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
static_verifier_resultt::source_location
source_locationt source_location
Definition: static_verifier.cpp:25
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
jsont::make_object
json_objectt & make_object()
Definition: json.h:290
namespace.h
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:47
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
json_arrayt
Definition: json.h:146
json_objectt
Definition: json.h:244
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
static_verifier_resultt::TRUE
@ TRUE
Definition: static_verifier.cpp:23
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
messaget::green
static const commandt green
render text with green foreground color
Definition: message.h:336
messaget::result
mstreamt & result() const
Definition: message.h:396
static_verifier_resultt::BOTTOM
@ BOTTOM
Definition: static_verifier.cpp:23
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:372
messaget::bold
static const commandt bold
render text with bold font
Definition: message.h:369
messaget::yellow
static const commandt yellow
render text with yellow foreground color
Definition: message.h:339
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:107
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
static_verifier_console
static void static_verifier_console(const std::vector< static_verifier_resultt > &results, const namespacet &ns, messaget &m)
Definition: static_verifier.cpp:157
static_verifier_resultt::status
enum static_verifier_resultt::@0 status
ai_baset::abstract_state_before
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...
json_expr.h
message_handlert
Definition: message.h:24
dstringt::empty
bool empty() const
Definition: dstring.h:75
ai.h
xmlt
Definition: xml.h:18
source_locationt
Definition: source_location.h:20
static_verifier_resultt::FALSE
@ FALSE
Definition: static_verifier.cpp:23
messaget::red
static const commandt red
render text with red foreground color
Definition: message.h:333
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
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:42
ai_baset
The basic interface of an abstract interpreter.
Definition: ai.h:32
source_locationt::get_file
const irep_idt & get_file() const
Definition: source_location.h:37
messaget::underline
static const commandt underline
render underlined text
Definition: message.h:378
static_verifier_resultt::UNKNOWN
@ UNKNOWN
Definition: static_verifier.cpp:23
messaget::progress
mstreamt & progress() const
Definition: message.h:411
ai_domain_baset::ai_simplify
virtual bool ai_simplify(exprt &condition, const namespacet &) const
also add
Definition: ai_domain.h:105
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:27
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static_verifier_xml
static void static_verifier_xml(const std::vector< static_verifier_resultt > &results, messaget &m, std::ostream &out)
Definition: static_verifier.cpp:67
static_verifier_resultt::function_id
irep_idt function_id
Definition: static_verifier.cpp:26
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:163
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:804
xmlt::new_element
xmlt & new_element(const std::string &key)
Definition: xml.h:86
json_stringt
Definition: json.h:214
static_verifier_resultt
Definition: static_verifier.cpp:20