cprover
show_vcc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Output of the verification conditions (VCCs)
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "show_vcc.h"
13 #include "symex_target_equation.h"
14 
15 #include <fstream>
16 #include <iostream>
17 #include <sstream>
18 
20 
21 #include <util/exception_utils.h>
22 #include <util/format_expr.h>
23 #include <util/json_irep.h>
24 #include <util/ui_message.h>
25 
29 static void
31 {
32  bool has_threads = equation.has_threads();
33  bool first = true;
34 
35  for(symex_target_equationt::SSA_stepst::const_iterator s_it =
36  equation.SSA_steps.begin();
37  s_it != equation.SSA_steps.end();
38  s_it++)
39  {
40  if(!s_it->is_assert())
41  continue;
42 
43  if(first)
44  first = false;
45  else
46  out << '\n';
47 
48  if(s_it->source.pc->source_location.is_not_nil())
49  out << s_it->source.pc->source_location << '\n';
50 
51  if(!s_it->comment.empty())
52  out << s_it->comment << '\n';
53 
54  symex_target_equationt::SSA_stepst::const_iterator p_it =
55  equation.SSA_steps.begin();
56 
57  // we show everything in case there are threads
58  symex_target_equationt::SSA_stepst::const_iterator last_it =
59  has_threads ? equation.SSA_steps.end() : s_it;
60 
61  for(std::size_t count = 1; p_it != last_it; p_it++)
62  if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
63  {
64  if(!p_it->ignore)
65  {
66  out << messaget::faint << "{-" << count << "} " << messaget::reset
67  << format(p_it->cond_expr) << '\n';
68 
69 #ifdef DEBUG
70  out << "GUARD: " << format(p_it->guard) << '\n';
71  out << '\n';
72 #endif
73 
74  count++;
75  }
76  }
77 
78  // Unicode equivalent of "|--------------------------"
79  out << messaget::faint << u8"\u251c";
80  for(unsigned i = 0; i < 26; i++)
81  out << u8"\u2500";
82  out << messaget::reset << '\n';
83 
84  // split property into multiple disjunts, if applicable
85  exprt::operandst disjuncts;
86 
87  if(s_it->cond_expr.id() == ID_or)
88  disjuncts = to_or_expr(s_it->cond_expr).operands();
89  else
90  disjuncts.push_back(s_it->cond_expr);
91 
92  std::size_t count = 1;
93  for(const auto &disjunct : disjuncts)
94  {
95  out << messaget::faint << '{' << count << "} " << messaget::reset
96  << format(disjunct) << '\n';
97  count++;
98  }
99 
100  out << messaget::eom;
101  }
102 }
103 
112 static void
113 show_vcc_json(std::ostream &out, const symex_target_equationt &equation)
114 {
115  json_objectt json_result;
116 
117  json_arrayt &json_vccs = json_result["vccs"].make_array();
118 
119  bool has_threads = equation.has_threads();
120 
121  for(symex_target_equationt::SSA_stepst::const_iterator s_it =
122  equation.SSA_steps.begin();
123  s_it != equation.SSA_steps.end();
124  s_it++)
125  {
126  if(!s_it->is_assert())
127  continue;
128 
129  // vcc object
130  json_objectt &object = json_vccs.push_back(jsont()).make_object();
131 
132  const source_locationt &source_location = s_it->source.pc->source_location;
133  if(source_location.is_not_nil())
134  object["sourceLocation"] = json(source_location);
135 
136  const std::string &s = s_it->comment;
137  if(!s.empty())
138  object["comment"] = json_stringt(s);
139 
140  // we show everything in case there are threads
141  symex_target_equationt::SSA_stepst::const_iterator last_it =
142  has_threads ? equation.SSA_steps.end() : s_it;
143 
144  json_arrayt &json_constraints = object["constraints"].make_array();
145 
146  for(symex_target_equationt::SSA_stepst::const_iterator p_it =
147  equation.SSA_steps.begin();
148  p_it != last_it;
149  p_it++)
150  {
151  if(
152  (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) &&
153  !p_it->ignore)
154  {
155  std::ostringstream string_value;
156  string_value << format(p_it->cond_expr);
157  json_constraints.push_back(json_stringt(string_value.str()));
158  }
159  }
160 
161  std::ostringstream string_value;
162  string_value << format(s_it->cond_expr);
163  object["expression"] = json_stringt(string_value.str());
164  }
165 
166  out << ",\n" << json_result;
167 }
168 
169 void show_vcc(
170  const optionst &options,
171  ui_message_handlert &ui_message_handler,
172  const symex_target_equationt &equation)
173 {
174  messaget msg(ui_message_handler);
175 
176  const std::string &filename = options.get_option("outfile");
177  bool have_file = !filename.empty() && filename != "-";
178 
179  std::ofstream of;
180 
181  if(have_file)
182  {
183  of.open(filename);
184  if(!of)
186  "failed to open output file: " + filename, "--outfile");
187  }
188 
189  std::ostream &out = have_file ? of : std::cout;
190 
191  switch(ui_message_handler.get_ui())
192  {
194  msg.error() << "XML UI not supported" << messaget::eom;
195  return;
196 
198  show_vcc_json(out, equation);
199  break;
200 
202  if(have_file)
203  {
204  msg.status() << "Verification conditions written to file"
205  << messaget::eom;
206  stream_message_handlert mout_handler(out);
207  messaget mout(mout_handler);
208  show_vcc_plain(mout.status(), equation);
209  }
210  else
211  {
212  msg.status() << "VERIFICATION CONDITIONS:\n" << messaget::eom;
213  show_vcc_plain(msg.status(), equation);
214  }
215  break;
216  }
217 
218  if(have_file)
219  of.close();
220 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
exception_utils.h
symex_target_equation.h
Generate Equation using Symbolic Execution.
format
static format_containert< T > format(const T &o)
Definition: format.h:35
ui_message_handlert
Definition: ui_message.h:20
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
ui_message_handlert::uit::XML_UI
@ XML_UI
optionst
Definition: options.h:23
show_vcc.h
Output of the verification conditions (VCCs)
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
u8
uint64_t u8
Definition: bytecode_info.h:58
messaget::status
mstreamt & status() const
Definition: message.h:414
show_vcc_json
static void show_vcc_json(std::ostream &out, const symex_target_equationt &equation)
Output equations from equation in the JSON format to the given output stream out.
Definition: show_vcc.cpp:113
messaget::eom
static eomt eom
Definition: message.h:297
jsont::make_object
json_objectt & make_object()
Definition: json.h:438
jsont
Definition: json.h:27
json_irep.h
Util.
json_arrayt
Definition: json.h:165
json_objectt
Definition: json.h:300
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:31
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:402
messaget::error
mstreamt & error() const
Definition: message.h:399
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:385
ui_message_handlert::uit::JSON_UI
@ JSON_UI
ui_message_handlert::out
std::ostream & out
Definition: ui_message.h:51
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:114
show_vcc_plain
static void show_vcc_plain(messaget::mstreamt &out, const symex_target_equationt &equation)
Output equations from equation in plain text format to the given output stream out.
Definition: show_vcc.cpp:30
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
symex_target_equationt::has_threads
bool has_threads() const
Definition: symex_target_equation.h:277
symex_target_equationt
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
Definition: symex_target_equation.h:41
source_locationt
Definition: source_location.h:20
to_or_expr
const or_exprt & to_or_expr(const exprt &expr)
Cast an exprt to a or_exprt.
Definition: std_expr.h:2292
format_expr.h
show_vcc
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Output equations from equation to a file or to the standard output.
Definition: show_vcc.cpp:169
ui_message_handlert::uit::PLAIN
@ PLAIN
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:257
messaget::mstreamt
Definition: message.h:224
exprt::operands
operandst & operands()
Definition: expr.h:95
invalid_command_line_argument_exceptiont
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
Definition: exception_utils.h:38
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
json_stringt
Definition: json.h:270
ui_message.h
stream_message_handlert
Definition: message.h:111