From 94cacc66d972675427d9de38d6a032f0e0718145 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 3 Jul 2018 11:53:11 +0200 Subject: [PATCH 1/4] represent numerical values in CBMC trace in hex --- regression/cbmc/hex_trace/main.c | 12 ++++ regression/cbmc/hex_trace/test.desc | 14 ++++ src/cbmc/all_properties.cpp | 3 +- src/cbmc/bmc.cpp | 2 +- src/goto-programs/goto_trace.cpp | 102 +++++++++++++++++++++------- src/goto-programs/goto_trace.h | 48 ++++++++----- 6 files changed, 137 insertions(+), 44 deletions(-) create mode 100644 regression/cbmc/hex_trace/main.c create mode 100644 regression/cbmc/hex_trace/test.desc diff --git a/regression/cbmc/hex_trace/main.c b/regression/cbmc/hex_trace/main.c new file mode 100644 index 00000000000..c144bb194b7 --- /dev/null +++ b/regression/cbmc/hex_trace/main.c @@ -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,""); + +} diff --git a/regression/cbmc/hex_trace/test.desc b/regression/cbmc/hex_trace/test.desc new file mode 100644 index 00000000000..0116cd690ee --- /dev/null +++ b/regression/cbmc/hex_trace/test.desc @@ -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 diff --git a/src/cbmc/all_properties.cpp b/src/cbmc/all_properties.cpp index d23889242fd..0fd5ff3c475 100644 --- a/src/cbmc/all_properties.cpp +++ b/src/cbmc/all_properties.cpp @@ -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; diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index 5865f49f154..fc0bea1efa4 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -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; diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index ede8a1efba3..5243dbf0cf7 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -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(); diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 5af74abbe8f..51576939414 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -195,45 +195,61 @@ class goto_tracet } }; -void show_goto_trace( - std::ostream &out, - const namespacet &, - const goto_tracet &); - -void trace_value( - std::ostream &out, - const namespacet &, - const ssa_exprt &lhs_object, - const exprt &full_lhs, - const exprt &value); - - 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; }; }; -#define OPT_GOTO_TRACE "(trace-json-extended)" +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 &, + const ssa_exprt &lhs_object, + const exprt &full_lhs, + const exprt &value); + + +#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 From f532b4bd6fa431d401f63ab2b0478c767ef52fea Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 3 Jul 2018 16:32:09 +0200 Subject: [PATCH 2/4] allow unsigned long instead of unsigned in regression test for hex_trace --- regression/cbmc/hex_trace/test.desc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/regression/cbmc/hex_trace/test.desc b/regression/cbmc/hex_trace/test.desc index 0116cd690ee..028e4a78b8e 100644 --- a/regression/cbmc/hex_trace/test.desc +++ b/regression/cbmc/hex_trace/test.desc @@ -4,10 +4,10 @@ main.c ^EXIT=10$ ^SIGNAL=0$ a=0 \s*\(0x0\) -b=0u \s*\(0x0\) +b=0ul? \s*\(0x0\) a=-100 \s*\(0xFFFFFF9C\) a=2147483647 \s*\(0x7FFFFFFF\) -b=4294967294u \s*\(0xFFFFFFFE\) +b=4294967294ul? \s*\(0xFFFFFFFE\) a=-2147483647 \s*\(0x80000001\) ^VERIFICATION FAILED$ -- From 4fbc10da0f82eef780eb906781362611e3e11400 Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 3 Jul 2018 13:39:00 +0200 Subject: [PATCH 3/4] Add option to show function calls and returns in CBMC trace --- .../cbmc/trace_show_function_calls/main.c | 22 +++++++++++++++++++ .../cbmc/trace_show_function_calls/test.desc | 11 ++++++++++ src/goto-programs/goto_trace.cpp | 11 ++++++++++ src/goto-programs/goto_trace.h | 9 +++++++- 4 files changed, 52 insertions(+), 1 deletion(-) create mode 100644 regression/cbmc/trace_show_function_calls/main.c create mode 100644 regression/cbmc/trace_show_function_calls/test.desc diff --git a/regression/cbmc/trace_show_function_calls/main.c b/regression/cbmc/trace_show_function_calls/main.c new file mode 100644 index 00000000000..bb1ca004bc6 --- /dev/null +++ b/regression/cbmc/trace_show_function_calls/main.c @@ -0,0 +1,22 @@ +int function_to_call(int a) +{ + int local = 1; + return a+local; +} + + +int main() +{ + int a; + unsigned int b; + a = 0; + a = -100; + a = 2147483647; + b = a*2; + a = -2147483647; + a = function_to_call(a); + b = function_to_call(b); + + __CPROVER_assert(0,""); + +} diff --git a/regression/cbmc/trace_show_function_calls/test.desc b/regression/cbmc/trace_show_function_calls/test.desc new file mode 100644 index 00000000000..d4d92b0cfda --- /dev/null +++ b/regression/cbmc/trace_show_function_calls/test.desc @@ -0,0 +1,11 @@ +CORE +main.c +--trace --trace-show-function-calls +^EXIT=10$ +^SIGNAL=0$ +Function call: function_to_call \(depth 2\) +Function return: function_to_call \(depth 1\) +Function call: function_to_call \(depth 2\) +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 5243dbf0cf7..86e4429715a 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -283,6 +283,7 @@ void show_goto_trace( { unsigned prev_step_nr=0; bool first_step=true; + std::size_t function_depth=0; for(const auto &step : goto_trace.steps) { @@ -427,7 +428,17 @@ void show_goto_trace( break; case goto_trace_stept::typet::FUNCTION_CALL: + function_depth++; + if(options.show_function_calls) + out << "\n#### Function call: " << step.identifier << " (depth " + << function_depth << ") ####\n"; + break; case goto_trace_stept::typet::FUNCTION_RETURN: + function_depth--; + if(options.show_function_calls) + out << "\n#### Function return: " << step.identifier << " (depth " + << function_depth << ") ####\n"; + break; case goto_trace_stept::typet::SPAWN: case goto_trace_stept::typet::MEMORY_BARRIER: case goto_trace_stept::typet::ATOMIC_BEGIN: diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 51576939414..295905d2b46 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -200,6 +200,7 @@ struct trace_optionst bool json_full_lhs; bool hex_representation; bool base_prefix; + bool show_function_calls; static const trace_optionst default_options; @@ -208,6 +209,7 @@ struct trace_optionst json_full_lhs = options.get_bool_option("trace-json-extended"); hex_representation = options.get_bool_option("trace-hex"); base_prefix = hex_representation; + show_function_calls = options.get_bool_option("trace-show-function-calls"); }; private: @@ -216,6 +218,7 @@ struct trace_optionst json_full_lhs = false; hex_representation = false; base_prefix = false; + show_function_calls = false; }; }; @@ -239,15 +242,19 @@ void trace_value( #define OPT_GOTO_TRACE "(trace-json-extended)" \ + "(trace-show-function-calls)" \ "(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-show-function-calls show function calls in plain 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); \ + if(cmdline.isset("trace-show-function-calls")) \ + options.set_option("trace-show-function-calls", true); \ if(cmdline.isset("trace-hex")) \ options.set_option("trace-hex", true); From 180e066993407fc2c2e9776f481412e901aab6aa Mon Sep 17 00:00:00 2001 From: Polgreen Date: Tue, 3 Jul 2018 15:19:01 +0200 Subject: [PATCH 4/4] add option to show code in CBMC trace --- regression/cbmc/trace_show_code/main.c | 23 ++++++++++++++++ regression/cbmc/trace_show_code/test.desc | 19 ++++++++++++++ src/goto-programs/goto_trace.cpp | 32 ++++++++++++++++------- src/goto-programs/goto_trace.h | 7 +++++ 4 files changed, 72 insertions(+), 9 deletions(-) create mode 100644 regression/cbmc/trace_show_code/main.c create mode 100644 regression/cbmc/trace_show_code/test.desc diff --git a/regression/cbmc/trace_show_code/main.c b/regression/cbmc/trace_show_code/main.c new file mode 100644 index 00000000000..d725e9d0c22 --- /dev/null +++ b/regression/cbmc/trace_show_code/main.c @@ -0,0 +1,23 @@ +int function_to_call(int a) +{ + int local = 1; + return a+local; +} + + +int main() +{ + int a, c; + unsigned int b; + a = 0; + c = -100; + a = function_to_call(a) + function_to_call(c); + if(a < 0) + b = function_to_call(b); + + if(c < 0) + b = -function_to_call(b); + + __CPROVER_assert(0,""); + +} diff --git a/regression/cbmc/trace_show_code/test.desc b/regression/cbmc/trace_show_code/test.desc new file mode 100644 index 00000000000..962278e6598 --- /dev/null +++ b/regression/cbmc/trace_show_code/test.desc @@ -0,0 +1,19 @@ +CORE +main.c +--trace --trace-show-code +^EXIT=10$ +^SIGNAL=0$ +local = 1 +int a +int c +unsigned int b +a = 0; +c = -100; +function_to_call\(a\) +function_to_call\(c\) +a = return_value_function_to_call \+ return_value_function_to_call +function_to_call\(\(signed int\)b\) +b = \(unsigned int\)return_value_function_to_call +^VERIFICATION FAILED$ +-- +^warning: ignoring diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 86e4429715a..1416b20dc57 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -247,20 +247,30 @@ void trace_value( void show_state_header( std::ostream &out, + const namespacet &ns, const goto_trace_stept &state, const source_locationt &source_location, - unsigned step_nr) + unsigned step_nr, + const trace_optionst &options) { out << "\n"; - if(step_nr==0) + if(step_nr == 0) out << "Initial State"; else out << "State " << step_nr; - out << " " << source_location - << " thread " << state.thread_nr << "\n"; - out << "----------------------------------------------------" << "\n"; + out << " " << source_location << " thread " << state.thread_nr << "\n"; + out << "----------------------------------------------------" + << "\n"; + + if(options.show_code) + { + out << as_string(ns, *state.pc) + << "\n"; + out << "----------------------------------------------------" + << "\n"; + } } bool is_index_member_symbol(const exprt &src) @@ -342,7 +352,8 @@ void show_goto_trace( { first_step=false; prev_step_nr=step.step_nr; - show_state_header(out, step, step.pc->source_location, step.step_nr); + show_state_header( + out, ns, step, step.pc->source_location, step.step_nr, options); } // see if the full lhs is something clean @@ -370,7 +381,8 @@ void show_goto_trace( { first_step=false; prev_step_nr=step.step_nr; - show_state_header(out, step, step.pc->source_location, step.step_nr); + show_state_header( + out, ns, step, step.pc->source_location, step.step_nr, options); } trace_value( @@ -387,7 +399,8 @@ void show_goto_trace( } else { - show_state_header(out, step, step.pc->source_location, step.step_nr); + show_state_header( + out, ns, step, step.pc->source_location, step.step_nr, options); out << " OUTPUT " << step.io_id << ":"; for(std::list::const_iterator @@ -408,7 +421,8 @@ void show_goto_trace( break; case goto_trace_stept::typet::INPUT: - show_state_header(out, step, step.pc->source_location, step.step_nr); + show_state_header( + out, ns, step, step.pc->source_location, step.step_nr, options); out << " INPUT " << step.io_id << ":"; for(std::list::const_iterator diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 295905d2b46..43411264ae6 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -201,6 +201,7 @@ struct trace_optionst bool hex_representation; bool base_prefix; bool show_function_calls; + bool show_code; static const trace_optionst default_options; @@ -210,6 +211,7 @@ struct trace_optionst hex_representation = options.get_bool_option("trace-hex"); base_prefix = hex_representation; show_function_calls = options.get_bool_option("trace-show-function-calls"); + show_code = options.get_bool_option("trace-show-code"); }; private: @@ -219,6 +221,7 @@ struct trace_optionst hex_representation = false; base_prefix = false; show_function_calls = false; + show_code = false; }; }; @@ -243,11 +246,13 @@ void trace_value( #define OPT_GOTO_TRACE "(trace-json-extended)" \ "(trace-show-function-calls)" \ + "(trace-show-code)" \ "(trace-hex)" #define HELP_GOTO_TRACE \ " --trace-json-extended add rawLhs property to trace\n" \ " --trace-show-function-calls show function calls in plain trace\n" \ + " --trace-show-code show original code in plain trace\n" \ " --trace-hex represent plain trace values in hex\n" #define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \ @@ -255,6 +260,8 @@ void trace_value( options.set_option("trace-json-extended", true); \ if(cmdline.isset("trace-show-function-calls")) \ options.set_option("trace-show-function-calls", true); \ + if(cmdline.isset("trace-show-code")) \ + options.set_option("trace-show-code", true); \ if(cmdline.isset("trace-hex")) \ options.set_option("trace-hex", true);