cprover
show_program.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Output of the program (SSA) constraints
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "show_program.h"
13 
14 #include <fstream>
15 #include <iostream>
16 
18 
19 #include <langapi/language_util.h>
20 
21 #include <util/byte_operators.h>
22 #include <util/json_irep.h>
23 #include <util/ui_message.h>
24 
30 static void show_step(
31  const namespacet &ns,
32  const SSA_stept &step,
33  const std::string &annotation,
34  std::size_t &count)
35 {
36  const irep_idt &function_id = step.source.function_id;
37 
38  std::string string_value = (step.is_shared_read() || step.is_shared_write())
39  ? from_expr(ns, function_id, step.ssa_lhs)
40  : from_expr(ns, function_id, step.cond_expr);
41  std::cout << '(' << count << ") ";
42  if(annotation.empty())
43  std::cout << string_value;
44  else
45  std::cout << annotation << '(' << string_value << ')';
46  std::cout << '\n';
47 
48  if(!step.guard.is_true())
49  {
50  const std::string guard_string = from_expr(ns, function_id, step.guard);
51  std::cout << std::string(std::to_string(count).size() + 3, ' ');
52  std::cout << "guard: " << guard_string << '\n';
53  }
54 
55  ++count;
56 }
57 
58 void show_program(const namespacet &ns, const symex_target_equationt &equation)
59 {
60  std::size_t count = 1;
61 
62  std::cout << '\n' << "Program constraints:" << '\n';
63 
64  for(const auto &step : equation.SSA_steps)
65  {
66  std::cout << "// " << step.source.pc->location_number << " ";
67  std::cout << step.source.pc->source_location.as_string() << "\n";
68 
69  if(step.is_assignment())
70  show_step(ns, step, "", count);
71  else if(step.is_assert())
72  show_step(ns, step, "ASSERT", count);
73  else if(step.is_assume())
74  show_step(ns, step, "ASSUME", count);
75  else if(step.is_constraint())
76  {
77  PRECONDITION(step.guard.is_true());
78  show_step(ns, step, "CONSTRAINT", count);
79  }
80  else if(step.is_shared_read())
81  show_step(ns, step, "SHARED_READ", count);
82  else if(step.is_shared_write())
83  show_step(ns, step, "SHARED_WRITE", count);
84  }
85 }
86 
87 template <typename expr_typet>
88 std::size_t count_expr_typed(const exprt &expr)
89 {
90  static_assert(
91  std::is_base_of<exprt, expr_typet>::value,
92  "`expr_typet` is expected to be a type of `exprt`.");
93 
94  std::size_t count = 0;
95  expr.visit_pre([&](const exprt &e) {
96  if(can_cast_expr<expr_typet>(e))
97  count++;
98  });
99 
100  return count;
101 }
102 
103 bool duplicated_previous_step(const SSA_stept &ssa_step)
104 {
105  return !(
106  ssa_step.is_assignment() || ssa_step.is_assert() || ssa_step.is_assume() ||
107  ssa_step.is_constraint() || ssa_step.is_shared_read() ||
108  ssa_step.is_shared_write());
109 }
110 
112  messaget::mstreamt &out,
113  const namespacet &ns,
114  const SSA_stept &ssa_step,
115  const exprt &ssa_expr)
116 {
117  const irep_idt &function_id = ssa_step.source.function_id;
118  const std::string ssa_expr_as_string = from_expr(ns, function_id, ssa_expr);
119 
120  out << messaget::faint << "// " << ssa_step.source.pc->location_number << " ";
121  out << ssa_step.source.pc->source_location.as_string() << "\n"
122  << messaget::reset;
123  out << ssa_expr_as_string << "\n";
124 }
125 
127  const namespacet &ns,
128  const SSA_stept &ssa_step,
129  const exprt &ssa_expr)
130 {
131  const std::string key_srcloc = "sourceLocation";
132  const std::string key_ssa_expr = "ssaExpr";
133  const std::string key_ssa_expr_as_string = "ssaExprString";
134 
135  const irep_idt &function_id = ssa_step.source.function_id;
136  const std::string ssa_expr_as_string = from_expr(ns, function_id, ssa_expr);
137 
138  json_objectt json_ssa_step{
139  {key_srcloc, json(ssa_step.source.pc->source_location)},
140  {key_ssa_expr_as_string, json_stringt(ssa_expr_as_string)},
141  {key_ssa_expr, json_irept(false).convert_from_irep(ssa_expr)}};
142 
143  return json_ssa_step;
144 }
145 
146 template <typename expr_typet>
148  messaget::mstreamt &out,
149  const namespacet &ns,
150  const symex_target_equationt &equation)
151 {
152  std::size_t equation_byte_op_count = 0;
153  for(const auto &step : equation.SSA_steps)
154  {
155  if(duplicated_previous_step(step))
156  continue;
157 
158  const exprt &ssa_expr = step.get_ssa_expr();
159  const std::size_t ssa_expr_byte_op_count =
160  count_expr_typed<expr_typet>(ssa_expr);
161 
162  if(ssa_expr_byte_op_count == 0)
163  continue;
164 
165  equation_byte_op_count += ssa_expr_byte_op_count;
166  show_ssa_step_plain(out, ns, step, ssa_expr);
167  }
168 
169  if(std::is_same<expr_typet, byte_extract_exprt>::value)
170  out << '\n' << "Number of byte extracts: ";
171  else if(std::is_same<expr_typet, byte_update_exprt>::value)
172  out << '\n' << "Number of byte updates: ";
173  else
174  UNREACHABLE;
175 
176  out << equation_byte_op_count << '\n';
177  out << messaget::eom;
178 }
179 
180 template <typename expr_typet>
182 {
183  if(std::is_same<expr_typet, byte_extract_exprt>::value)
184  return "byteExtractList";
185  else if(std::is_same<expr_typet, byte_update_exprt>::value)
186  return "byteUpdateList";
187  else
188  UNREACHABLE;
189 }
190 
191 template <typename expr_typet>
193 {
194  if(std::is_same<expr_typet, byte_extract_exprt>::value)
195  return "numOfExtracts";
196  else if(std::is_same<expr_typet, byte_update_exprt>::value)
197  return "numOfUpdates";
198  else
199  UNREACHABLE;
200 }
201 
202 template <typename expr_typet>
205 {
206  // Get key values to be used in the json output based on byte operation type
207  // 1. json_get_key_byte_op_list():
208  // returns relevant json object key string where object records
209  // a list of expressions for given byte operation.
210  // 2. json_get_key_byte_op_num():
211  // returns relevant json object key string where object number
212  // of given byte operation.
213 
214  const std::string key_byte_op_list = json_get_key_byte_op_list<expr_typet>();
215  const std::string key_byte_op_num = json_get_key_byte_op_num<expr_typet>();
216 
217  json_objectt byte_op_stats;
218  json_arrayt &byte_op_list = byte_op_stats[key_byte_op_list].make_array();
219 
220  std::size_t equation_byte_op_count = 0;
221  for(const auto &step : equation.SSA_steps)
222  {
223  if(duplicated_previous_step(step))
224  continue;
225 
226  const exprt &ssa_expr = step.get_ssa_expr();
227  const std::size_t ssa_expr_byte_op_count =
228  count_expr_typed<expr_typet>(ssa_expr);
229 
230  if(ssa_expr_byte_op_count == 0)
231  continue;
232 
233  equation_byte_op_count += ssa_expr_byte_op_count;
234  byte_op_list.push_back(get_ssa_step_json(ns, step, ssa_expr));
235  }
236 
237  byte_op_stats[key_byte_op_num] =
238  json_numbert(std::to_string(equation_byte_op_count));
239 
240  return byte_op_stats;
241 }
242 
243 // Get key values to be used in the json output based on byte operation type
244 // 1. json_get_key_byte_op_stats():
245 // returns relevant json object key string where object records
246 // statistics for given byte operation.
247 template <typename expr_typet>
249 {
250  if(std::is_same<expr_typet, byte_extract_exprt>::value)
251  return "byteExtractStats";
252  else if(std::is_same<expr_typet, byte_update_exprt>::value)
253  return "byteUpdateStats";
254  else
255  UNREACHABLE;
256 }
257 
258 bool is_outfile_specified(const optionst &options)
259 {
260  const std::string &filename = options.get_option("outfile");
261  return (!filename.empty() && filename != "-");
262 }
263 
265  ui_message_handlert &ui_message_handler,
266  std::ostream &out,
267  bool outfile_given,
268  const namespacet &ns,
269  const symex_target_equationt &equation)
270 {
271  messaget msg(ui_message_handler);
272  if(outfile_given)
273  {
274  stream_message_handlert mout_handler(out);
275  messaget mout(mout_handler);
276 
277  msg.status() << "\nByte Extracts written to file" << messaget::eom;
278  show_byte_op_plain<byte_extract_exprt>(mout.status(), ns, equation);
279 
280  msg.status() << "\nByte Updates written to file" << messaget::eom;
281  show_byte_op_plain<byte_update_exprt>(mout.status(), ns, equation);
282  }
283  else
284  {
285  msg.status() << "\nByte Extracts:" << messaget::eom;
286  show_byte_op_plain<byte_extract_exprt>(msg.status(), ns, equation);
287 
288  msg.status() << "\nByte Updates:" << messaget::eom;
289  show_byte_op_plain<byte_update_exprt>(msg.status(), ns, equation);
290  }
291 }
292 
294  std::ostream &out,
295  const namespacet &ns,
296  const symex_target_equationt &equation)
297 {
298  json_objectt byte_ops_stats{
299  {json_get_key_byte_op_stats<byte_extract_exprt>(),
300  get_byte_op_json<byte_extract_exprt>(ns, equation)},
301  {json_get_key_byte_op_stats<byte_update_exprt>(),
302  get_byte_op_json<byte_update_exprt>(ns, equation)}};
303 
304  json_objectt json_result;
305  json_result["byteOpsStats"] = byte_ops_stats;
306 
307  out << ",\n" << json_result;
308 }
309 
310 void show_byte_ops_xml(ui_message_handlert &ui_message_handler)
311 {
312  messaget msg(ui_message_handler);
313  msg.error()
314  << "XML UI not supported for displaying byte extracts and updates."
315  << " Try --json-ui instead" << messaget::eom;
316 
317  return;
318 }
319 
321  const optionst &options,
322  ui_message_handlert &ui_message_handler,
323  const namespacet &ns,
324  const symex_target_equationt &equation)
325 {
326  const std::string &filename = options.get_option("outfile");
327  const bool outfile_given = is_outfile_specified(options);
328 
329  std::ofstream of;
330 
331  if(outfile_given)
332  {
333  of.open(filename, std::fstream::out);
334  if(!of)
336  "failed to open output file: " + filename, "--outfile");
337  }
338 
339  std::ostream &out = outfile_given ? of : std::cout;
340 
341  switch(ui_message_handler.get_ui())
342  {
344  show_byte_ops_xml(ui_message_handler);
345  break;
346 
348  show_byte_ops_json(out, ns, equation);
349  break;
350 
352  show_byte_ops_plain(ui_message_handler, out, outfile_given, ns, equation);
353  break;
354  }
355 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
json_numbert
Definition: json.h:291
show_program
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Print the steps of equation on the standard output.
Definition: show_program.cpp:58
symex_target_equation.h
Generate Equation using Symbolic Execution.
ui_message_handlert
Definition: ui_message.h:22
messaget::reset
static const commandt reset
return to default formatting, as defined by the terminal
Definition: message.h:343
is_outfile_specified
bool is_outfile_specified(const optionst &options)
Definition: show_program.cpp:258
ui_message_handlert::uit::XML_UI
@ XML_UI
optionst
Definition: options.h:23
show_step
static void show_step(const namespacet &ns, const SSA_stept &step, const std::string &annotation, std::size_t &count)
Output a single SSA step.
Definition: show_program.cpp:30
duplicated_previous_step
bool duplicated_previous_step(const SSA_stept &ssa_step)
Definition: show_program.cpp:103
optionst::get_option
const std::string get_option(const std::string &option) const
Definition: options.cpp:67
show_byte_op_plain
void show_byte_op_plain(messaget::mstreamt &out, const namespacet &ns, const symex_target_equationt &equation)
Definition: show_program.cpp:147
SSA_stept
Single SSA step in the equation.
Definition: ssa_step.h:47
symex_targett::sourcet::pc
goto_programt::const_targett pc
Definition: symex_target.h:42
messaget::status
mstreamt & status() const
Definition: message.h:414
SSA_stept::is_assert
bool is_assert() const
Definition: ssa_step.h:52
get_ssa_step_json
json_objectt get_ssa_step_json(const namespacet &ns, const SSA_stept &ssa_step, const exprt &ssa_expr)
Definition: show_program.cpp:126
exprt
Base class for all expressions.
Definition: expr.h:54
json_get_key_byte_op_stats
std::string json_get_key_byte_op_stats()
Definition: show_program.cpp:248
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
messaget::eom
static eomt eom
Definition: message.h:297
SSA_stept::guard
exprt guard
Definition: ssa_step.h:139
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:33
SSA_stept::source
symex_targett::sourcet source
Definition: ssa_step.h:49
json_irep.h
Util.
SSA_stept::is_constraint
bool is_constraint() const
Definition: ssa_step.h:72
json_arrayt
Definition: json.h:165
SSA_stept::is_shared_write
bool is_shared_write() const
Definition: ssa_step.h:107
SSA_stept::is_shared_read
bool is_shared_read() const
Definition: ssa_step.h:102
json_objectt
Definition: json.h:300
ui_message_handlert::get_ui
virtual uit get_ui() const
Definition: ui_message.h:33
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
show_byte_ops_json
void show_byte_ops_json(std::ostream &out, const namespacet &ns, const symex_target_equationt &equation)
Definition: show_program.cpp:293
byte_operators.h
Expression classes for byte-level operators.
messaget::error
mstreamt & error() const
Definition: message.h:399
messaget::faint
static const commandt faint
render text with faint font
Definition: message.h:385
SSA_stept::ssa_lhs
ssa_exprt ssa_lhs
Definition: ssa_step.h:143
ui_message_handlert::uit::JSON_UI
@ JSON_UI
json_get_key_byte_op_list
std::string json_get_key_byte_op_list()
Definition: show_program.cpp:181
language_util.h
SSA_stept::cond_expr
exprt cond_expr
Definition: ssa_step.h:149
show_ssa_step_plain
void show_ssa_step_plain(messaget::mstreamt &out, const namespacet &ns, const SSA_stept &ssa_step, const exprt &ssa_expr)
Definition: show_program.cpp:111
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:116
jsont::make_array
json_arrayt & make_array()
Definition: json.h:420
json_irept::convert_from_irep
json_objectt convert_from_irep(const irept &) const
To convert to JSON from an irep structure by recursively generating JSON for the different sub trees.
Definition: json_irep.cpp:31
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:34
show_byte_ops_plain
void show_byte_ops_plain(ui_message_handlert &ui_message_handler, std::ostream &out, bool outfile_given, const namespacet &ns, const symex_target_equationt &equation)
Definition: show_program.cpp:264
ui_message_handlert::uit::PLAIN
@ PLAIN
symex_target_equationt::SSA_steps
SSA_stepst SSA_steps
Definition: symex_target_equation.h:250
SSA_stept::is_assignment
bool is_assignment() const
Definition: ssa_step.h:62
exprt::visit_pre
void visit_pre(std::function< void(exprt &)>)
Definition: expr.cpp:245
get_byte_op_json
json_objectt get_byte_op_json(const namespacet &ns, const symex_target_equationt &equation)
Definition: show_program.cpp:204
json_get_key_byte_op_num
std::string json_get_key_byte_op_num()
Definition: show_program.cpp:192
messaget::mstreamt
Definition: message.h:224
count_expr_typed
std::size_t count_expr_typed(const exprt &expr)
Definition: show_program.cpp:88
show_program.h
Output of the program (SSA) constraints.
json_irept
Definition: json_irep.h:21
show_byte_ops_xml
void show_byte_ops_xml(ui_message_handlert &ui_message_handler)
Definition: show_program.cpp:310
symex_targett::sourcet::function_id
irep_idt function_id
Definition: symex_target.h:39
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
show_byte_ops
void show_byte_ops(const optionst &options, ui_message_handlert &ui_message_handler, const namespacet &ns, const symex_target_equationt &equation)
Count and display all byte extract and byte update operations from equation on standard output or fil...
Definition: show_program.cpp:320
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition: language_util.cpp:20
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
SSA_stept::is_assume
bool is_assume() const
Definition: ssa_step.h:57
json_stringt
Definition: json.h:270
ui_message.h
stream_message_handlert
Definition: message.h:111