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 
28  const goto_modelt &goto_model,
29  const ai_baset &ai,
30  const optionst &options,
32  std::ostream &out)
33 {
34  std::size_t pass=0, fail=0, unknown=0;
35 
36  namespacet ns(goto_model.symbol_table);
37 
39  m.status() << "Checking assertions" << messaget::eom;
40 
41  if(options.get_bool_option("json"))
42  {
43  json_arrayt json_result;
44 
45  forall_goto_functions(f_it, goto_model.goto_functions)
46  {
47  m.progress() << "Checking " << f_it->first << messaget::eom;
48 
49  if(!f_it->second.body.has_assertion())
50  continue;
51 
52  forall_goto_program_instructions(i_it, f_it->second.body)
53  {
54  if(!i_it->is_assert())
55  continue;
56 
57  exprt e(i_it->guard);
58  auto dp = ai.abstract_state_before(i_it);
59  const ai_domain_baset &domain(*dp);
60  domain.ai_simplify(e, ns);
61 
62  json_objectt &j=json_result.push_back().make_object();
63 
64  if(e.is_true())
65  {
66  j["status"]=json_stringt("SUCCESS");
67  ++pass;
68  }
69  else if(e.is_false())
70  {
71  j["status"]=json_stringt("FAILURE (if reachable)");
72  ++fail;
73  }
74  else if(domain.is_bottom())
75  {
76  j["status"]=json_stringt("SUCCESS (unreachable)");
77  ++pass;
78  }
79  else
80  {
81  j["status"]=json_stringt("UNKNOWN");
82  ++unknown;
83  }
84 
85  j["sourceLocation"]=json(i_it->source_location);
86  }
87  }
88  m.status() << "Writing JSON report" << messaget::eom;
89  out << json_result;
90  }
91  else if(options.get_bool_option("xml"))
92  {
93  xmlt xml_result;
94 
95  forall_goto_functions(f_it, goto_model.goto_functions)
96  {
97  m.progress() << "Checking " << f_it->first << messaget::eom;
98 
99  if(!f_it->second.body.has_assertion())
100  continue;
101 
102  forall_goto_program_instructions(i_it, f_it->second.body)
103  {
104  if(!i_it->is_assert())
105  continue;
106 
107  exprt e(i_it->guard);
108  auto dp = ai.abstract_state_before(i_it);
109  const ai_domain_baset &domain(*dp);
110  domain.ai_simplify(e, ns);
111 
112  xmlt &x=xml_result.new_element("result");
113 
114  if(e.is_true())
115  {
116  x.set_attribute("status", "SUCCESS");
117  ++pass;
118  }
119  else if(e.is_false())
120  {
121  x.set_attribute("status", "FAILURE (if reachable)");
122  ++fail;
123  }
124  else if(domain.is_bottom())
125  {
126  x.set_attribute("status", "SUCCESS (unreachable)");
127  ++pass;
128  }
129  else
130  {
131  x.set_attribute("status", "UNKNOWN");
132  ++unknown;
133  }
134 
135  x.set_attribute("file", id2string(i_it->source_location.get_file()));
136  x.set_attribute("line", id2string(i_it->source_location.get_line()));
137  x.set_attribute(
138  "description",
139  id2string(i_it->source_location.get_comment()));
140  }
141  }
142 
143  m.status() << "Writing XML report" << messaget::eom;
144  out << xml_result;
145  }
146  else
147  {
148  INVARIANT(options.get_bool_option("text"), "Other output formats handled");
149 
150  forall_goto_functions(f_it, goto_model.goto_functions)
151  {
152  m.progress() << "Checking " << f_it->first << messaget::eom;
153 
154  if(!f_it->second.body.has_assertion())
155  continue;
156 
157  out << "******** Function " << f_it->first << '\n';
158 
159  forall_goto_program_instructions(i_it, f_it->second.body)
160  {
161  if(!i_it->is_assert())
162  continue;
163 
164  exprt e(i_it->guard);
165  auto dp = ai.abstract_state_before(i_it);
166  const ai_domain_baset &domain(*dp);
167  domain.ai_simplify(e, ns);
168 
169  out << '[' << i_it->source_location.get_property_id()
170  << ']' << ' ';
171 
172  out << i_it->source_location;
173 
174  if(!i_it->source_location.get_comment().empty())
175  out << ", " << i_it->source_location.get_comment();
176 
177  out << ": ";
178 
179  if(e.is_true())
180  {
181  out << "Success";
182  pass++;
183  }
184  else if(e.is_false())
185  {
186  out << "Failure (if reachable)";
187  fail++;
188  }
189  else if(domain.is_bottom())
190  {
191  out << "Success (unreachable)";
192  pass++;
193  }
194  else
195  {
196  out << "Unknown";
197  unknown++;
198  }
199 
200  out << '\n';
201  }
202 
203  out << '\n';
204  }
205  }
206 
207  m.status() << "Summary: "
208  << pass << " pass, "
209  << fail << " fail if reachable, "
210  << unknown << " unknown\n";
211 
212  return false;
213 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
mstreamt & progress() const
Definition: message.h:327
bool is_false() const
Definition: expr.cpp:131
bool is_true() const
Definition: expr.cpp:124
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
virtual std::unique_ptr< statet > abstract_state_before(locationt l) const =0
Accessing individual domains at particular locations (without needing to know what kind of domain or ...
virtual bool is_bottom() const =0
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
jsont & push_back(const jsont &json)
Definition: json.h:163
Symbol Table + CFG.
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
also add
Definition: ai_domain.h:103
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:174
TO_BE_DOCUMENTED.
Definition: namespace.h:74
Definition: xml.h:18
xmlt & new_element(const std::string &name)
Definition: xml.h:86
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.
mstreamt & status() const
Definition: message.h:317
Abstract Interpretation.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
Options.
json_objectt & make_object()
Definition: json.h:290
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
#define forall_goto_functions(it, functions)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:83