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