CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
show_program.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Output of the program (SSA) constraints
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "show_program.h"
13
14#include <util/byte_operators.h> // IWYU pragma: keep
15#include <util/json_irep.h>
16#include <util/ui_message.h>
17
20
21#include <fstream> // IWYU pragma: keep
22#include <iostream>
23
29static void show_step(
30 const namespacet &ns,
31 const SSA_stept &step,
32 const std::string &annotation,
33 std::size_t &count)
34{
35 const irep_idt &function_id = step.source.function_id;
36
37 std::string string_value = (step.is_shared_read() || step.is_shared_write())
38 ? from_expr(ns, function_id, step.ssa_lhs)
39 : from_expr(ns, function_id, step.cond_expr);
40 if(step.ignore)
41 std::cout << "(sliced) ";
42 else
43 std::cout << '(' << count << ") ";
44 if(annotation.empty())
45 std::cout << string_value;
46 else
47 std::cout << annotation << '(' << string_value << ')';
48 std::cout << '\n';
49
50 if(!step.guard.is_true())
51 {
52 const std::string guard_string = from_expr(ns, function_id, step.guard);
53 std::cout << std::string(std::to_string(count).size() + 3, ' ');
54 std::cout << "guard: " << guard_string << '\n';
55 }
56
57 ++count;
58}
59
60void show_program(const namespacet &ns, const symex_target_equationt &equation)
61{
62 std::size_t count = 1;
63
64 std::cout << '\n' << "Program constraints:" << '\n';
65
66 for(const auto &step : equation.SSA_steps)
67 {
68 std::cout << "// " << step.source.pc->location_number << " ";
69 std::cout << step.source.pc->source_location().as_string() << "\n";
70
71 if(step.is_assignment())
72 show_step(ns, step, "", count);
73 else if(step.is_assert())
74 show_step(ns, step, "ASSERT", count);
75 else if(step.is_assume())
76 show_step(ns, step, "ASSUME", count);
77 else if(step.is_constraint())
78 {
79 PRECONDITION(step.guard.is_true());
80 show_step(ns, step, "CONSTRAINT", count);
81 }
82 else if(step.is_shared_read())
83 show_step(ns, step, "SHARED_READ", count);
84 else if(step.is_shared_write())
85 show_step(ns, step, "SHARED_WRITE", count);
86 }
87}
88
89template <typename expr_typet>
90std::size_t count_expr_typed(const exprt &expr)
91{
92 static_assert(
93 std::is_base_of<exprt, expr_typet>::value,
94 "`expr_typet` is expected to be a type of `exprt`.");
95
96 std::size_t count = 0;
97 expr.visit_pre([&](const exprt &e) {
99 count++;
100 });
101
102 return count;
103}
104
106{
107 return !(
108 ssa_step.is_assignment() || ssa_step.is_assert() || ssa_step.is_assume() ||
109 ssa_step.is_constraint() || ssa_step.is_shared_read() ||
110 ssa_step.is_shared_write());
111}
112
115 const namespacet &ns,
116 const SSA_stept &ssa_step,
117 const exprt &ssa_expr)
118{
119 const irep_idt &function_id = ssa_step.source.function_id;
120 const std::string ssa_expr_as_string = from_expr(ns, function_id, ssa_expr);
121
122 out << messaget::faint << "// " << ssa_step.source.pc->location_number << " ";
123 out << ssa_step.source.pc->source_location().as_string() << "\n"
125 out << ssa_expr_as_string << "\n";
126}
127
129 const namespacet &ns,
130 const SSA_stept &ssa_step,
131 const exprt &ssa_expr)
132{
133 const std::string key_srcloc = "sourceLocation";
134 const std::string key_ssa_expr = "ssaExpr";
135 const std::string key_ssa_expr_as_string = "ssaExprString";
136
137 const irep_idt &function_id = ssa_step.source.function_id;
138 const std::string ssa_expr_as_string = from_expr(ns, function_id, ssa_expr);
139
141 {key_srcloc, json(ssa_step.source.pc->source_location())},
144
145 return json_ssa_step;
146}
147
148template <typename expr_typet>
151 const namespacet &ns,
152 const symex_target_equationt &equation)
153{
154 std::size_t equation_byte_op_count = 0;
155 for(const auto &step : equation.SSA_steps)
156 {
158 continue;
159
160 const exprt &ssa_expr = step.get_ssa_expr();
161 const std::size_t ssa_expr_byte_op_count =
163
165 continue;
166
168 show_ssa_step_plain(out, ns, step, ssa_expr);
169 }
170
171 if(std::is_same<expr_typet, byte_extract_exprt>::value)
172 out << '\n' << "Number of byte extracts: ";
173 else if(std::is_same<expr_typet, byte_update_exprt>::value)
174 out << '\n' << "Number of byte updates: ";
175 else
177
178 out << equation_byte_op_count << '\n';
179 out << messaget::eom;
180}
181
182template <typename expr_typet>
184{
185 if(std::is_same<expr_typet, byte_extract_exprt>::value)
186 return "byteExtractList";
187 else if(std::is_same<expr_typet, byte_update_exprt>::value)
188 return "byteUpdateList";
189 else
191}
192
193template <typename expr_typet>
195{
196 if(std::is_same<expr_typet, byte_extract_exprt>::value)
197 return "numOfExtracts";
198 else if(std::is_same<expr_typet, byte_update_exprt>::value)
199 return "numOfUpdates";
200 else
202}
203
204template <typename expr_typet>
207{
208 // Get key values to be used in the json output based on byte operation type
209 // 1. json_get_key_byte_op_list():
210 // returns relevant json object key string where object records
211 // a list of expressions for given byte operation.
212 // 2. json_get_key_byte_op_num():
213 // returns relevant json object key string where object number
214 // of given byte operation.
215
218
221
222 std::size_t equation_byte_op_count = 0;
223 for(const auto &step : equation.SSA_steps)
224 {
226 continue;
227
228 const exprt &ssa_expr = step.get_ssa_expr();
229 const std::size_t ssa_expr_byte_op_count =
231
233 continue;
234
236 byte_op_list.push_back(get_ssa_step_json(ns, step, ssa_expr));
237 }
238
240 json_numbert(std::to_string(equation_byte_op_count));
241
242 return byte_op_stats;
243}
244
245// Get key values to be used in the json output based on byte operation type
246// 1. json_get_key_byte_op_stats():
247// returns relevant json object key string where object records
248// statistics for given byte operation.
249template <typename expr_typet>
251{
252 if(std::is_same<expr_typet, byte_extract_exprt>::value)
253 return "byteExtractStats";
254 else if(std::is_same<expr_typet, byte_update_exprt>::value)
255 return "byteUpdateStats";
256 else
258}
259
260bool is_outfile_specified(const optionst &options)
261{
262 const std::string &filename = options.get_option("outfile");
263 return (!filename.empty() && filename != "-");
264}
265
267 ui_message_handlert &ui_message_handler,
268 std::ostream &out,
269 bool outfile_given,
270 const namespacet &ns,
271 const symex_target_equationt &equation)
272{
273 messaget msg(ui_message_handler);
274 if(outfile_given)
275 {
278
279 msg.status() << "\nByte Extracts written to file" << messaget::eom;
280 show_byte_op_plain<byte_extract_exprt>(mout.status(), ns, equation);
281
282 msg.status() << "\nByte Updates written to file" << messaget::eom;
283 show_byte_op_plain<byte_update_exprt>(mout.status(), ns, equation);
284 }
285 else
286 {
287 msg.status() << "\nByte Extracts:" << messaget::eom;
288 show_byte_op_plain<byte_extract_exprt>(msg.status(), ns, equation);
289
290 msg.status() << "\nByte Updates:" << messaget::eom;
291 show_byte_op_plain<byte_update_exprt>(msg.status(), ns, equation);
292 }
293}
294
296 std::ostream &out,
297 const namespacet &ns,
298 const symex_target_equationt &equation)
299{
305
307 json_result["byteOpsStats"] = byte_ops_stats;
308
309 out << ",\n" << json_result;
310}
311
312void show_byte_ops_xml(ui_message_handlert &ui_message_handler)
313{
314 messaget msg(ui_message_handler);
315 msg.error()
316 << "XML UI not supported for displaying byte extracts and updates."
317 << " Try --json-ui instead" << messaget::eom;
318
319 return;
320}
321
323 const optionst &options,
324 ui_message_handlert &ui_message_handler,
325 const namespacet &ns,
326 const symex_target_equationt &equation)
327{
328 const std::string &filename = options.get_option("outfile");
329 const bool outfile_given = is_outfile_specified(options);
330
331 std::ofstream of;
332
333 if(outfile_given)
334 {
335 of.open(filename, std::fstream::out);
336 if(!of)
338 "failed to open output file: " + filename, "--outfile");
339 }
340
341 std::ostream &out = outfile_given ? of : std::cout;
342
343 switch(ui_message_handler.get_ui())
344 {
346 show_byte_ops_xml(ui_message_handler);
347 break;
348
350 show_byte_ops_json(out, ns, equation);
351 break;
352
354 show_byte_ops_plain(ui_message_handler, out, outfile_given, ns, equation);
355 break;
356 }
357}
Expression classes for byte-level operators.
Single SSA step in the equation.
Definition ssa_step.h:47
bool ignore
Definition ssa_step.h:172
exprt cond_expr
Definition ssa_step.h:145
exprt guard
Definition ssa_step.h:135
bool is_shared_write() const
Definition ssa_step.h:107
symex_targett::sourcet source
Definition ssa_step.h:49
bool is_shared_read() const
Definition ssa_step.h:102
ssa_exprt ssa_lhs
Definition ssa_step.h:139
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:227
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
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
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
static const commandt reset
return to default formatting, as defined by the terminal
Definition message.h:335
static const commandt faint
render text with faint font
Definition message.h:377
static eomt eom
Definition message.h:289
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
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
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
std::string json_get_key_byte_op_list()
void show_ssa_step_plain(messaget::mstreamt &out, const namespacet &ns, const SSA_stept &ssa_step, const exprt &ssa_expr)
std::string json_get_key_byte_op_stats()
std::string json_get_key_byte_op_num()
static void show_step(const namespacet &ns, const SSA_stept &step, const std::string &annotation, std::size_t &count)
Output a single SSA step.
json_objectt get_ssa_step_json(const namespacet &ns, const SSA_stept &ssa_step, const exprt &ssa_expr)
std::size_t count_expr_typed(const exprt &expr)
void show_byte_op_plain(messaget::mstreamt &out, const namespacet &ns, const symex_target_equationt &equation)
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Print the steps of equation on the standard output.
bool duplicated_previous_step(const SSA_stept &ssa_step)
bool is_outfile_specified(const optionst &options)
void show_byte_ops_json(std::ostream &out, const namespacet &ns, const symex_target_equationt &equation)
void show_byte_ops_xml(ui_message_handlert &ui_message_handler)
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)
json_objectt get_byte_op_json(const namespacet &ns, const symex_target_equationt &equation)
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...
Output of the program (SSA) constraints.
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Generate Equation using Symbolic Execution.