cprover
static_analyzer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "static_analyzer.h"
10 
11 #include <fstream>
12 
13 #include <util/threeval.h>
14 #include <util/json.h>
15 #include <util/xml.h>
16 
18 
20 {
21 public:
23  const goto_modelt &_goto_model,
24  const optionst &_options,
25  message_handlert &_message_handler):
26  messaget(_message_handler),
27  goto_functions(_goto_model.goto_functions),
28  ns(_goto_model.symbol_table),
29  options(_options)
30  {
31  }
32 
33  bool operator()();
34 
35 protected:
37  const namespacet ns;
38  const optionst &options;
39 
40  // analyses
42 
43  void plain_text_report();
44  void json_report(const std::string &);
45  void xml_report(const std::string &);
46 
48 };
49 
51 {
52  status() << "performing interval analysis" << eom;
54 
55  if(!options.get_option("json").empty())
57  else if(!options.get_option("xml").empty())
59  else
61 
62  return false;
63 }
64 
66 {
67  exprt guard=t->guard;
69  d.assume(not_exprt(guard), ns);
70  if(d.is_bottom())
71  return tvt(true);
72  return tvt::unknown();
73 }
74 
76 {
77  unsigned pass=0, fail=0, unknown=0;
78 
80  {
81  if(!f_it->second.body.has_assertion())
82  continue;
83 
84  if(f_it->first=="__actual_thread_spawn")
85  continue;
86 
87  status() << "******** Function " << f_it->first << eom;
88 
89  forall_goto_program_instructions(i_it, f_it->second.body)
90  {
91  if(!i_it->is_assert())
92  continue;
93 
94  tvt r=eval(i_it);
95 
96  result() << '[' << i_it->source_location.get_property_id()
97  << ']' << ' ';
98 
99  result() << i_it->source_location;
100  if(!i_it->source_location.get_comment().empty())
101  result() << ", " << i_it->source_location.get_comment();
102  result() << ": ";
103  if(r.is_true())
104  result() << "SUCCESS";
105  else if(r.is_false())
106  result() << "FAILURE";
107  else
108  result() << "UNKNOWN";
109  result() << eom;
110 
111  if(r.is_true())
112  pass++;
113  else if(r.is_false())
114  fail++;
115  else
116  unknown++;
117  }
118 
119  status() << '\n';
120  }
121 
122  status() << "SUMMARY: " << pass << " pass, " << fail << " fail, "
123  << unknown << " unknown\n";
124 }
125 
126 void static_analyzert::json_report(const std::string &file_name)
127 {
128  json_arrayt json_result;
129 
131  {
132  if(!f_it->second.body.has_assertion())
133  continue;
134 
135  if(f_it->first=="__actual_thread_spawn")
136  continue;
137 
138  forall_goto_program_instructions(i_it, f_it->second.body)
139  {
140  if(!i_it->is_assert())
141  continue;
142 
143  tvt r=eval(i_it);
144 
145  json_objectt &j=json_result.push_back().make_object();
146 
147  if(r.is_true())
148  j["status"]=json_stringt("SUCCESS");
149  else if(r.is_false())
150  j["status"]=json_stringt("FAILURE");
151  else
152  j["status"]=json_stringt("UNKNOWN");
153 
154  j["file"]=json_stringt(id2string(i_it->source_location.get_file()));
155  j["line"]=json_numbert(id2string(i_it->source_location.get_line()));
156  j["description"]=json_stringt(id2string(
157  i_it->source_location.get_comment()));
158  }
159  }
160 
161  std::ofstream out(file_name);
162  if(!out)
163  {
164  error() << "failed to open JSON output file `"
165  << file_name << "'" << eom;
166  return;
167  }
168 
169  status() << "Writing report to `" << file_name << "'" << eom;
170  out << json_result;
171 }
172 
173 void static_analyzert::xml_report(const std::string &file_name)
174 {
175  xmlt xml_result;
176 
178  {
179  if(!f_it->second.body.has_assertion())
180  continue;
181 
182  if(f_it->first=="__actual_thread_spawn")
183  continue;
184 
185  forall_goto_program_instructions(i_it, f_it->second.body)
186  {
187  if(!i_it->is_assert())
188  continue;
189 
190  tvt r=eval(i_it);
191 
192  xmlt &x=xml_result.new_element("result");
193 
194  if(r.is_true())
195  x.set_attribute("status", "SUCCESS");
196  else if(r.is_false())
197  x.set_attribute("status", "FAILURE");
198  else
199  x.set_attribute("status", "UNKNOWN");
200 
201  x.set_attribute("file", id2string(i_it->source_location.get_file()));
202  x.set_attribute("line", id2string(i_it->source_location.get_line()));
203  x.set_attribute(
204  "description", id2string(i_it->source_location.get_comment()));
205  }
206  }
207 
208  std::ofstream out(file_name);
209  if(!out)
210  {
211  error() << "failed to open XML output file `"
212  << file_name << "'" << eom;
213  return;
214  }
215 
216  status() << "Writing report to `" << file_name << "'" << eom;
217  out << xml_result;
218 }
219 
221  const goto_modelt &goto_model,
222  const optionst &options,
223  message_handlert &message_handler)
224 {
225  return static_analyzert(
226  goto_model, options, message_handler)();
227 }
228 
230  const goto_modelt &goto_model,
231  std::ostream &out)
232 {
234  interval_analysis(goto_model);
235  interval_analysis.output(goto_model, out);
236 }
mstreamt & result()
Definition: message.h:233
Boolean negation.
Definition: std_expr.h:2648
static int8_t r
Definition: irep_hash.h:59
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
mstreamt & status()
Definition: message.h:238
void assume(const exprt &, const namespacet &)
static tvt unknown()
Definition: threeval.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
bool is_bottom() const
void json_report(const std::string &)
jsont & push_back(const jsont &json)
Definition: json.h:157
instructionst::const_iterator const_targett
void show_intervals(const goto_modelt &goto_model, std::ostream &out)
source_locationt source_location
Definition: message.h:175
const std::string get_option(const std::string &option) const
Definition: options.cpp:60
Definition: threeval.h:19
void set_attribute(const std::string &attribute, unsigned value)
Definition: xml.cpp:174
TO_BE_DOCUMENTED.
Definition: namespace.h:62
Definition: xml.h:18
tvt eval(goto_programt::const_targett)
ait< interval_domaint > interval_analysis
const optionst & options
xmlt & new_element(const std::string &name)
Definition: xml.h:86
Interval Domain.
void xml_report(const std::string &)
Base class for all expressions.
Definition: expr.h:46
bool static_analyzer(const goto_modelt &goto_model, const optionst &options, message_handlert &message_handler)
mstreamt & error()
Definition: message.h:223
json_objectt & make_object()
Definition: json.h:234
const irep_idt & get_comment() const
#define forall_goto_functions(it, functions)
const irep_idt & get_property_id() const
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:68
const goto_functionst & goto_functions
void interval_analysis(const namespacet &ns, goto_functionst &goto_functions)
const namespacet ns
static_analyzert(const goto_modelt &_goto_model, const optionst &_options, message_handlert &_message_handler)