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