cprover
Loading...
Searching...
No Matches
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 <fstream>
15#include <iostream>
16
18
20
21#include <util/byte_operators.h>
22#include <util/json_irep.h>
23#include <util/ui_message.h>
24
30static 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
58void 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
87template <typename expr_typet>
88std::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) {
97 count++;
98 });
99
100 return count;
101}
102
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
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"
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
139 {key_srcloc, json(ssa_step.source.pc->source_location())},
142
143 return json_ssa_step;
144}
145
146template <typename expr_typet>
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 {
156 continue;
157
158 const exprt &ssa_expr = step.get_ssa_expr();
159 const std::size_t ssa_expr_byte_op_count =
161
163 continue;
164
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
175
176 out << equation_byte_op_count << '\n';
177 out << messaget::eom;
178}
179
180template <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
189}
190
191template <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
200}
201
202template <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
216
219
220 std::size_t equation_byte_op_count = 0;
221 for(const auto &step : equation.SSA_steps)
222 {
224 continue;
225
226 const exprt &ssa_expr = step.get_ssa_expr();
227 const std::size_t ssa_expr_byte_op_count =
229
231 continue;
232
234 byte_op_list.push_back(get_ssa_step_json(ns, step, ssa_expr));
235 }
236
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.
247template <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
256}
257
258bool 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 {
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;
287
288 msg.status() << "\nByte Updates:" << messaget::eom;
290 }
291}
292
294 std::ostream &out,
295 const namespacet &ns,
296 const symex_target_equationt &equation)
297{
303
305 json_result["byteOpsStats"] = byte_ops_stats;
306
307 out << ",\n" << json_result;
308}
309
310void 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}
Expression classes for byte-level operators.
Single SSA step in the equation.
Definition ssa_step.h:47
exprt cond_expr
Definition ssa_step.h:149
exprt guard
Definition ssa_step.h:139
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:143
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
void visit_pre(std::function< void(exprt &)>)
Definition expr.cpp:245
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: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
static const commandt faint
render text with faint font
Definition message.h:385
static eomt eom
Definition message.h:297
mstreamt & status() const
Definition message.h:414
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:503
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Generate Equation using Symbolic Execution.