replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

represent numerical values in CBMC trace in hex

This commit is contained in:
Polgreen 2018-07-03 11:53:11 +02:00
parent 6e554d9f0a
commit d5bbdd8af0
6 changed files with 142 additions and 49 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
regression/cbmc/hex_trace/main.c Normal file
View File

@ -0,0 +1,12 @@
int main()
{
int a;
unsigned int b;
a = 0;
a = -100;
a = 2147483647;
b = a*2;
a = -2147483647;
__CPROVER_assert(0,"");
}

14
regression/cbmc/hex_trace/test.desc Normal file
View File

@ -0,0 +1,14 @@
CORE
main.c
--trace-hex --trace
^EXIT=10$
^SIGNAL=0$
a=0 \s*\(0x0\)
b=0u \s*\(0x0\)
a=-100 \s*\(0xFFFFFF9C\)
a=2147483647 \s*\(0x7FFFFFFF\)
b=4294967294u \s*\(0xFFFFFFFE\)
a=-2147483647 \s*\(0x80000001\)
^VERIFICATION FAILED$
--
^warning: ignoring

3
src/cbmc/all_properties.cpp
View File

@ -175,7 +175,8 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
if(g.second.status==goalt::statust::FAILURE)
{
result() << "\n" << "Trace for " << g.first << ":" << "\n";
show_goto_trace(result(), bmc.ns, g.second.goto_trace);
show_goto_trace(
result(), bmc.ns, g.second.goto_trace, bmc.trace_options());
}
}
result() << eom;

2
src/cbmc/bmc.cpp
View File

@ -55,7 +55,7 @@ void bmct::error_trace()
{
case ui_message_handlert::uit::PLAIN:
result() << "Counterexample:" << eom;
show_goto_trace(result(), ns, goto_trace);
show_goto_trace(result(), ns, goto_trace, trace_options());
result() << eom;
break;

102
src/goto-programs/goto_trace.cpp
View File

@ -103,10 +103,50 @@ void goto_trace_stept::output(
out << '\n';
}
/// Returns the numeric representation of an expression, based on
/// options. The default is binary without a base-prefix. Setting
/// options.hex_representation to be true outputs hex format. Setting
/// options.base_prefix to be true appends either 0b or 0x to the number
/// to indicate the base
/// \param expr: expression to get numeric representation from
/// \param options: configuration options
/// \return a string with the numeric representation
static std::string
numeric_representation(const exprt &expr, const trace_optionst &options)
{
std::string result;
std::string prefix;
if(options.hex_representation)
{
mp_integer value_int =
binary2integer(id2string(to_constant_expr(expr).get_value()), false);
result = integer2string(value_int, 16);
prefix = "0x";
}
else
{
prefix = "0b";
result = expr.get_string(ID_value);
}
std::string trace_value_binary(
std::ostringstream oss;
std::string::size_type i = 0;
for(const auto c : result)
{
oss << c;
if(++i % 8 == 0 && result.size() != i)
oss << ' ';
}
if(options.base_prefix)
return prefix + oss.str();
else
return oss.str();
}
std::string trace_numeric_value(
const exprt &expr,
const namespacet &ns)
const namespacet &ns,
const trace_optionst &options)
{
const typet &type=ns.follow(expr.type());
@ -123,18 +163,8 @@ std::string trace_value_binary(
type.id()==ID_c_enum ||
type.id()==ID_c_enum_tag)
{
const std::string & str = expr.get_string(ID_value);
std::ostringstream oss;
std::string::size_type i = 0;
for(const auto c : str)
{
oss << c;
if(++i % 8 == 0 && str.size() != i)
oss << ' ';
}
return oss.str();
const std::string &str = numeric_representation(expr, options);
return str;
}
else if(type.id()==ID_bool)
{
@ -157,7 +187,7 @@ std::string trace_value_binary(
result="{ ";
else
result+=", ";
result+=trace_value_binary(*it, ns);
result+=trace_numeric_value(*it, ns, options);
}
return result+" }";
@ -170,15 +200,15 @@ std::string trace_value_binary(
{
if(it!=expr.operands().begin())
result+=", ";
result+=trace_value_binary(*it, ns);
result+=trace_numeric_value(*it, ns, options);
}
return result+" }";
}
else if(expr.id()==ID_union)
{
assert(expr.operands().size()==1);
return trace_value_binary(expr.op0(), ns);
PRECONDITION(expr.operands().size()==1);
return trace_numeric_value(expr.op0(), ns, options);
}
return "?";
@ -189,7 +219,8 @@ void trace_value(
const namespacet &ns,
const ssa_exprt &lhs_object,
const exprt &full_lhs,
const exprt &value)
const exprt &value,
const trace_optionst &options)
{
irep_idt identifier;
@ -205,7 +236,7 @@ void trace_value(
value_string=from_expr(ns, identifier, value);
// the binary representation
value_string+=" ("+trace_value_binary(value, ns)+")";
value_string += " (" + trace_numeric_value(value, ns, options) + ")";
}
out << " "
@ -247,7 +278,8 @@ bool is_index_member_symbol(const exprt &src)
void show_goto_trace(
std::ostream &out,
const namespacet &ns,
const goto_tracet &goto_trace)
const goto_tracet &goto_trace,
const trace_optionst &options)
{
unsigned prev_step_nr=0;
bool first_step=true;
@ -315,10 +347,20 @@ void show_goto_trace(
// see if the full lhs is something clean
if(is_index_member_symbol(step.full_lhs))
trace_value(
out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
out,
ns,
step.lhs_object,
step.full_lhs,
step.full_lhs_value,
options);
else
trace_value(
out, ns, step.lhs_object, step.lhs_object, step.lhs_object_value);
out,
ns,
step.lhs_object,
step.lhs_object,
step.lhs_object_value,
options);
}
break;
@ -330,7 +372,8 @@ void show_goto_trace(
show_state_header(out, step, step.pc->source_location, step.step_nr);
}
trace_value(out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value);
trace_value(
out, ns, step.lhs_object, step.full_lhs, step.full_lhs_value, options);
break;
case goto_trace_stept::typet::OUTPUT:
@ -356,7 +399,7 @@ void show_goto_trace(
out << " " << from_expr(ns, step.pc->function, *l_it);
// the binary representation
out << " (" << trace_value_binary(*l_it, ns) << ")";
out << " (" << trace_numeric_value(*l_it, ns, options) << ")";
}
out << "\n";
@ -377,7 +420,7 @@ void show_goto_trace(
out << " " << from_expr(ns, step.pc->function, *l_it);
// the binary representation
out << " (" << trace_value_binary(*l_it, ns) << ")";
out << " (" << trace_numeric_value(*l_it, ns, options) << ")";
}
out << "\n";
@ -401,5 +444,12 @@ void show_goto_trace(
}
}
void show_goto_trace(
std::ostream &out,
const namespacet &ns,
const goto_tracet &goto_trace)
{
show_goto_trace(out, ns, goto_trace, trace_optionst::default_options);
}
const trace_optionst trace_optionst::default_options = trace_optionst();

58
src/goto-programs/goto_trace.h
View File

@ -195,11 +195,41 @@ public:
}
};
struct trace_optionst
{
bool json_full_lhs;
bool hex_representation;
bool base_prefix;
static const trace_optionst default_options;
explicit trace_optionst(const optionst &options)
{
json_full_lhs = options.get_bool_option("trace-json-extended");
hex_representation = options.get_bool_option("trace-hex");
base_prefix = hex_representation;
};
private:
trace_optionst()
{
json_full_lhs = false;
hex_representation = false;
base_prefix = false;
};
};
void show_goto_trace(
std::ostream &out,
const namespacet &,
const goto_tracet &);
void show_goto_trace(
std::ostream &out,
const namespacet &,
const goto_tracet &,
const trace_optionst &);
void trace_value(
std::ostream &out,
const namespacet &,
@ -208,32 +238,18 @@ void trace_value(
const exprt &value);
struct trace_optionst
{
bool json_full_lhs;
static const trace_optionst default_options;
explicit trace_optionst(const optionst &options)
{
json_full_lhs = options.get_bool_option("trace-json-extended");
};
private:
trace_optionst()
{
json_full_lhs = false;
};
};
#define OPT_GOTO_TRACE "(trace-json-extended)"
#define OPT_GOTO_TRACE "(trace-json-extended)" \
"(trace-hex)"
#define HELP_GOTO_TRACE \
" --trace-json-extended add rawLhs property to trace\n"
" --trace-json-extended add rawLhs property to trace\n" \
" --trace-hex represent plain trace values in hex\n"
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
if(cmdline.isset("trace-json-extended")) \
options.set_option("trace-json-extended", true);
options.set_option("trace-json-extended", true); \
if(cmdline.isset("trace-hex")) \
options.set_option("trace-hex", true);
#endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H