34 const std::string &annotation,
42 std::cout <<
'(' << count <<
") ";
43 if(annotation.empty())
44 std::cout << string_value;
46 std::cout << annotation <<
'(' << string_value <<
')';
51 const std::string guard_string =
from_expr(ns, function_id, step.
guard);
53 std::cout <<
"guard: " << guard_string <<
'\n';
61 std::size_t count = 1;
63 std::cout <<
'\n' <<
"Program constraints:" <<
'\n';
65 for(
const auto &step : equation.
SSA_steps)
67 std::cout <<
"// " << step.source.pc->location_number <<
" ";
68 std::cout << step.source.pc->source_location.as_string() <<
"\n";
70 if(step.is_assignment())
72 else if(step.is_assert())
74 else if(step.is_assume())
76 else if(step.is_constraint())
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);
88 template <
typename expr_typet>
92 std::is_base_of<exprt, expr_typet>::value,
93 "`expr_typet` is expected to be a type of `exprt`.");
95 std::size_t count = 0;
97 if(can_cast_expr<expr_typet>(e))
116 const exprt &ssa_expr)
119 const std::string ssa_expr_as_string =
from_expr(ns, function_id, ssa_expr);
122 out << ssa_step.
source.
pc->source_location.as_string() <<
"\n"
124 out << ssa_expr_as_string <<
"\n";
130 const exprt &ssa_expr)
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";
137 const std::string ssa_expr_as_string =
from_expr(ns, function_id, ssa_expr);
140 {key_srcloc,
json(ssa_step.
source.
pc->source_location)},
141 {key_ssa_expr_as_string,
json_stringt(ssa_expr_as_string)},
144 return json_ssa_step;
147 template <
typename expr_typet>
153 std::size_t equation_byte_op_count = 0;
154 for(
const auto &step : equation.
SSA_steps)
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);
163 if(ssa_expr_byte_op_count == 0)
166 equation_byte_op_count += ssa_expr_byte_op_count;
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: ";
177 out << equation_byte_op_count <<
'\n';
181 template <
typename expr_typet>
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";
192 template <
typename expr_typet>
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";
203 template <
typename expr_typet>
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>();
221 std::size_t equation_byte_op_count = 0;
222 for(
const auto &step : equation.
SSA_steps)
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);
231 if(ssa_expr_byte_op_count == 0)
234 equation_byte_op_count += ssa_expr_byte_op_count;
238 byte_op_stats[key_byte_op_num] =
241 return byte_op_stats;
248 template <
typename expr_typet>
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";
261 const std::string &filename = options.
get_option(
"outfile");
262 return (!filename.empty() && filename !=
"-");
279 show_byte_op_plain<byte_extract_exprt>(mout.
status(), ns, equation);
282 show_byte_op_plain<byte_update_exprt>(mout.
status(), ns, equation);
287 show_byte_op_plain<byte_extract_exprt>(msg.
status(), ns, equation);
290 show_byte_op_plain<byte_update_exprt>(msg.
status(), ns, equation);
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)}};
306 json_result[
"byteOpsStats"] = byte_ops_stats;
308 out <<
",\n" << json_result;
315 <<
"XML UI not supported for displaying byte extracts and updates."
327 const std::string &filename = options.
get_option(
"outfile");
334 of.open(filename, std::fstream::out);
337 "failed to open output file: " + filename,
"--outfile");
340 std::ostream &out = outfile_given ? of : std::cout;
342 switch(ui_message_handler.
get_ui())