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  const ai_domain_baset &domain(ai.abstract_state_before(i_it));
59  domain.ai_simplify(e, ns);
60 
61  json_objectt &j=json_result.push_back().make_object();
62 
63  if(e.is_true())
64  {
65  j["status"]=json_stringt("SUCCESS");
66  ++pass;
67  }
68  else if(e.is_false())
69  {
70  j["status"]=json_stringt("FAILURE (if reachable)");
71  ++fail;
72  }
73  else if(domain.is_bottom())
74  {
75  j["status"]=json_stringt("SUCCESS (unreachable)");
76  ++pass;
77  }
78  else
79  {
80  j["status"]=json_stringt("UNKNOWN");
81  ++unknown;
82  }
83 
84  j["sourceLocation"]=json(i_it->source_location);
85  }
86  }
87  m.status() << "Writing JSON report" << messaget::eom;
88  out << json_result;
89  }
90  else if(options.get_bool_option("xml"))
91  {
92  xmlt xml_result;
93 
94  forall_goto_functions(f_it, goto_model.goto_functions)
95  {
96  m.progress() << "Checking " << f_it->first << messaget::eom;
97 
98  if(!f_it->second.body.has_assertion())
99  continue;
100 
101  forall_goto_program_instructions(i_it, f_it->second.body)
102  {
103  if(!i_it->is_assert())
104  continue;
105 
106  exprt e(i_it->guard);
107  const ai_domain_baset &domain(ai.abstract_state_before(i_it));
108  domain.ai_simplify(e, ns);
109 
110  xmlt &x=xml_result.new_element("result");
111 
112  if(e.is_true())
113  {
114  x.set_attribute("status", "SUCCESS");
115  ++pass;
116  }
117  else if(e.is_false())
118  {
119  x.set_attribute("status", "FAILURE (if reachable)");
120  ++fail;
121  }
122  else if(domain.is_bottom())
123  {
124  x.set_attribute("status", "SUCCESS (unreachable)");
125  ++pass;
126  }
127  else
128  {
129  x.set_attribute("status", "UNKNOWN");
130  ++unknown;
131  }
132 
133  x.set_attribute("file", id2string(i_it->source_location.get_file()));
134  x.set_attribute("line", id2string(i_it->source_location.get_line()));
135  x.set_attribute(
136  "description",
137  id2string(i_it->source_location.get_comment()));
138  }
139  }
140 
141  m.status() << "Writing XML report" << messaget::eom;
142  out << xml_result;
143  }
144  else
145  {
146  INVARIANT(options.get_bool_option("text"), "Other output formats handled");
147 
148  forall_goto_functions(f_it, goto_model.goto_functions)
149  {
150  m.progress() << "Checking " << f_it->first << messaget::eom;
151 
152  if(!f_it->second.body.has_assertion())
153  continue;
154 
155  out << "******** Function " << f_it->first << '\n';
156 
157  forall_goto_program_instructions(i_it, f_it->second.body)
158  {
159  if(!i_it->is_assert())
160  continue;
161 
162  exprt e(i_it->guard);
163  const ai_domain_baset &domain(ai.abstract_state_before(i_it));
164  domain.ai_simplify(e, ns);
165 
166  out << '[' << i_it->source_location.get_property_id()
167  << ']' << ' ';
168 
169  out << i_it->source_location;
170 
171  if(!i_it->source_location.get_comment().empty())
172  out << ", " << i_it->source_location.get_comment();
173 
174  out << ": ";
175 
176  if(e.is_true())
177  {
178  out << "Success";
179  pass++;
180  }
181  else if(e.is_false())
182  {
183  out << "Failure (if reachable)";
184  fail++;
185  }
186  else if(domain.is_bottom())
187  {
188  out << "Success (unreachable)";
189  pass++;
190  }
191  else
192  {
193  out << "Unknown";
194  unknown++;
195  }
196 
197  out << '\n';
198  }
199 
200  out << '\n';
201  }
202  }
203 
204  m.status() << "Summary: "
205  << pass << " pass, "
206  << fail << " fail if reachable, "
207  << unknown << " unknown\n";
208 
209  return false;
210 }
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
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
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
jsont & push_back(const jsont &json)
Definition: json.h:163
Symbol Table + CFG.
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const
Definition: ai.h:113
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.
Definition: ai.h:128
Base class for all expressions.
Definition: expr.h:42
virtual const ai_domain_baset & abstract_state_before(goto_programt::const_targett t) const =0
Returns the abstract state before the given instruction.
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