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.h>
24 #include <util/json_expr.h>
25 #include <util/ui_message.h>
26 
28  messaget::mstreamt &out,
29  const symex_target_equationt &equation)
30 {
31  bool has_threads = equation.has_threads();
32  bool first = true;
33 
34  for(symex_target_equationt::SSA_stepst::const_iterator s_it =
35  equation.SSA_steps.begin();
36  s_it != equation.SSA_steps.end();
37  s_it++)
38  {
39  if(!s_it->is_assert())
40  continue;
41 
42  if(first)
43  first = false;
44  else
45  out << '\n';
46 
47  if(s_it->source.pc->source_location.is_not_nil())
48  out << s_it->source.pc->source_location << '\n';
49 
50  if(s_it->comment != "")
51  out << s_it->comment << '\n';
52 
53  symex_target_equationt::SSA_stepst::const_iterator p_it =
54  equation.SSA_steps.begin();
55 
56  // we show everything in case there are threads
57  symex_target_equationt::SSA_stepst::const_iterator last_it =
58  has_threads ? equation.SSA_steps.end() : s_it;
59 
60  for(std::size_t count = 1; p_it != last_it; p_it++)
61  if(p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint())
62  {
63  if(!p_it->ignore)
64  {
65  out << messaget::faint << "{-" << count << "} " << messaget::reset
66  << format(p_it->cond_expr) << '\n';
67 
68 #ifdef DEBUG
69  out << "GUARD: " << format(p_it->guard) << '\n';
70  out << '\n';
71 #endif
72 
73  count++;
74  }
75  }
76 
77  // Unicode equivalent of "|--------------------------"
78  out << messaget::faint << u8"\u251c";
79  for(unsigned i = 0; i < 26; i++)
80  out << u8"\u2500";
81  out << messaget::reset << '\n';
82 
83  // split property into multiple disjunts, if applicable
84  exprt::operandst disjuncts;
85 
86  if(s_it->cond_expr.id() == ID_or)
87  disjuncts = to_or_expr(s_it->cond_expr).operands();
88  else
89  disjuncts.push_back(s_it->cond_expr);
90 
91  std::size_t count = 1;
92  for(const auto &disjunct : disjuncts)
93  {
94  out << messaget::faint << '{' << count << "} " << messaget::reset
95  << format(disjunct) << '\n';
96  count++;
97  }
98 
99  out << messaget::eom;
100  }
101 }
102 
104  std::ostream &out,
105  const symex_target_equationt &equation)
106 {
107  json_objectt json_result;
108 
109  json_arrayt &json_vccs = json_result["vccs"].make_array();
110 
111  bool has_threads = equation.has_threads();
112 
113  for(symex_target_equationt::SSA_stepst::const_iterator s_it =
114  equation.SSA_steps.begin();
115  s_it != equation.SSA_steps.end();
116  s_it++)
117  {
118  if(!s_it->is_assert())
119  continue;
120 
121  // vcc object
122  json_objectt &object = json_vccs.push_back(jsont()).make_object();
123 
124  const source_locationt &source_location = s_it->source.pc->source_location;
125  if(source_location.is_not_nil())
126  object["sourceLocation"] = json(source_location);
127 
128  const std::string &s = s_it->comment;
129  if(!s.empty())
130  object["comment"] = json_stringt(s);
131 
132  // we show everything in case there are threads
133  symex_target_equationt::SSA_stepst::const_iterator last_it =
134  has_threads ? equation.SSA_steps.end() : s_it;
135 
136  json_arrayt &json_constraints = object["constraints"].make_array();
137 
138  for(symex_target_equationt::SSA_stepst::const_iterator p_it =
139  equation.SSA_steps.begin();
140  p_it != last_it;
141  p_it++)
142  {
143  if(
144  (p_it->is_assume() || p_it->is_assignment() || p_it->is_constraint()) &&
145  !p_it->ignore)
146  {
147  std::ostringstream string_value;
148  string_value << format(p_it->cond_expr);
149  json_constraints.push_back(json_stringt(string_value.str()));
150  }
151  }
152 
153  std::ostringstream string_value;
154  string_value << format(s_it->cond_expr);
155  object["expression"] = json_stringt(string_value.str());
156  }
157 
158  out << ",\n" << json_result;
159 }
160 
161 void show_vcc(
162  const optionst &options,
163  ui_message_handlert &ui_message_handler,
164  const symex_target_equationt &equation)
165 {
166  messaget msg(ui_message_handler);
167 
168  const std::string &filename = options.get_option("outfile");
169  bool have_file = !filename.empty() && filename != "-";
170 
171  std::ofstream of;
172 
173  if(have_file)
174  {
175  of.open(filename);
176  if(!of)
178  "failed to open output file: " + filename, "--outfile");
179  }
180 
181  std::ostream &out = have_file ? of : std::cout;
182 
183  switch(ui_message_handler.get_ui())
184  {
186  msg.error() << "XML UI not supported" << messaget::eom;
187  return;
188 
190  show_vcc_json(out, equation);
191  break;
192 
194  if(have_file)
195  {
196  msg.status() << "Verification conditions written to file"
197  << messaget::eom;
198  stream_message_handlert mout_handler(out);
199  messaget mout(mout_handler);
200  show_vcc_plain(mout.status(), equation);
201  }
202  else
203  {
204  msg.status() << "VERIFICATION CONDITIONS:\n" << messaget::eom;
205  show_vcc_plain(msg.status(), equation);
206  }
207  break;
208  }
209 
210  if(have_file)
211  of.close();
212 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
exception_utils.h
symex_target_equation.h
format
static format_containert< T > format(const T &o)
Definition: format.h:35
json
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87
ui_message_handlert
Definition: ui_message.h:19
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:330
ui_message_handlert::uit::XML_UI
optionst
Definition: options.h:22
show_vcc.h
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:65
u8
uint64_t u8
Definition: bytecode_info.h:58
messaget::status
mstreamt & status() const
Definition: message.h:401
messaget::eom
static eomt eom
Definition: message.h:284
jsont::make_object
json_objectt & make_object()
Definition: json.h:290
jsont
Definition: json.h:23
json_arrayt
Definition: json.h:146
json_objectt
Definition: json.h:244
show_vcc_plain
void show_vcc_plain(messaget::mstreamt &out, const symex_target_equationt &equation)
Definition: show_vcc.cpp:27
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
messaget::error
mstreamt & error() const
Definition: message.h:386
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:372
ui_message_handlert::uit::JSON_UI
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
show_vcc_json
void show_vcc_json(std::ostream &out, const symex_target_equationt &equation)
Definition: show_vcc.cpp:103
json_expr.h
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
jsont::make_array
json_arrayt & make_array()
Definition: json.h:284
symex_target_equationt::has_threads
bool has_threads() const
Definition: symex_target_equation.h:389
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:35
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:2577
ui_message_handlert::get_ui
uit get_ui() const
Definition: ui_message.h:30
format_expr.h
show_vcc
void show_vcc(const optionst &options, ui_message_handlert &ui_message_handler, const symex_target_equationt &equation)
Definition: show_vcc.cpp:161
ui_message_handlert::uit::PLAIN
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:369
json.h
messaget::mstreamt
Definition: message.h:212
exprt::operands
operandst & operands()
Definition: expr.h:78
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:37
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:163
json_stringt
Definition: json.h:214
ui_message.h
stream_message_handlert
Definition: message.h:100