33 const std::string &annotation,
41 std::cout <<
'(' << count <<
") ";
42 if(annotation.empty())
43 std::cout << string_value;
45 std::cout << annotation <<
'(' << string_value <<
')';
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';
60 std::size_t count = 1;
62 std::cout <<
'\n' <<
"Program constraints:" <<
'\n';
64 for(
const auto &step : equation.
SSA_steps)
66 std::cout <<
"// " << step.source.pc->location_number <<
" ";
67 std::cout << step.source.pc->source_location().as_string() <<
"\n";
69 if(step.is_assignment())
71 else if(step.is_assert())
73 else if(step.is_assume())
75 else if(step.is_constraint())
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);
87template <
typename expr_typet>
91 std::is_base_of<exprt, expr_typet>::value,
92 "`expr_typet` is expected to be a type of `exprt`.");
94 std::size_t count = 0;
96 if(can_cast_expr<expr_typet>(e))
115 const exprt &ssa_expr)
118 const std::string ssa_expr_as_string =
from_expr(ns, function_id, ssa_expr);
121 out << ssa_step.
source.
pc->source_location().as_string() <<
"\n"
123 out << ssa_expr_as_string <<
"\n";
129 const exprt &ssa_expr)
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";
136 const std::string ssa_expr_as_string =
from_expr(ns, function_id, ssa_expr);
139 {key_srcloc,
json(ssa_step.
source.
pc->source_location())},
140 {key_ssa_expr_as_string,
json_stringt(ssa_expr_as_string)},
143 return json_ssa_step;
146template <
typename expr_typet>
152 std::size_t equation_byte_op_count = 0;
153 for(
const auto &step : equation.
SSA_steps)
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);
162 if(ssa_expr_byte_op_count == 0)
165 equation_byte_op_count += ssa_expr_byte_op_count;
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: ";
176 out << equation_byte_op_count <<
'\n';
180template <
typename expr_typet>
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";
191template <
typename expr_typet>
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";
202template <
typename expr_typet>
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>();
220 std::size_t equation_byte_op_count = 0;
221 for(
const auto &step : equation.
SSA_steps)
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);
230 if(ssa_expr_byte_op_count == 0)
233 equation_byte_op_count += ssa_expr_byte_op_count;
237 byte_op_stats[key_byte_op_num] =
240 return byte_op_stats;
247template <
typename expr_typet>
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";
260 const std::string &filename = options.
get_option(
"outfile");
261 return (!filename.empty() && filename !=
"-");
278 show_byte_op_plain<byte_extract_exprt>(mout.
status(), ns, equation);
281 show_byte_op_plain<byte_update_exprt>(mout.
status(), ns, equation);
286 show_byte_op_plain<byte_extract_exprt>(msg.
status(), ns, equation);
289 show_byte_op_plain<byte_update_exprt>(msg.
status(), ns, equation);
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)}};
305 json_result[
"byteOpsStats"] = byte_ops_stats;
307 out <<
",\n" << json_result;
314 <<
"XML UI not supported for displaying byte extracts and updates."
326 const std::string &filename = options.
get_option(
"outfile");
333 of.open(filename, std::fstream::out);
336 "failed to open output file: " + filename,
"--outfile");
339 std::ostream &out = outfile_given ? of : std::cout;
341 switch(ui_message_handler.
get_ui())
Expression classes for byte-level operators.
Single SSA step in the equation.
bool is_constraint() const
bool is_shared_write() const
symex_targett::sourcet source
bool is_shared_read() const
bool is_assignment() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
void visit_pre(std::function< void(exprt &)>)
Thrown when users pass incorrect command line arguments, for example passing no files to analysis or ...
jsont & push_back(const jsont &json)
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.
json_arrayt & make_array()
Class that provides messages with a built-in verbosity 'level'.
static const commandt reset
return to default formatting, as defined by the terminal
static const commandt faint
render text with faint font
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const std::string get_option(const std::string &option) const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual uit get_ui() const
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.
#define PRECONDITION(CONDITION)
goto_programt::const_targett pc
Generate Equation using Symbolic Execution.