diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index abcfc87057b..7e3d09a4ed5 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/jbmc/src/jbmc/jbmc_parse_options.cpp @@ -135,8 +135,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options) cmdline.isset("outfile")) options.set_option("stop-on-fail", true); - if(cmdline.isset("trace") || - cmdline.isset("stop-on-fail")) + if( + cmdline.isset("trace") || cmdline.isset("stack-trace") || + cmdline.isset("stop-on-fail")) options.set_option("trace", true); if(cmdline.isset("localize-faults")) diff --git a/regression/cbmc/stack-trace/main.c b/regression/cbmc/stack-trace/main.c new file mode 100644 index 00000000000..7e4bbdd61dd --- /dev/null +++ b/regression/cbmc/stack-trace/main.c @@ -0,0 +1,15 @@ +int foo(int foo_a) +{ + __CPROVER_assert(foo_a != 2, "assertion"); +} + +int bar(int bar_a) +{ + foo(bar_a + 1); + foo(bar_a + 2); +} + +int main() +{ + bar(0); +} diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc new file mode 100644 index 00000000000..eceab4a2d07 --- /dev/null +++ b/regression/cbmc/stack-trace/test.desc @@ -0,0 +1,9 @@ +CORE +main.c +--stack-trace +activate-multi-line-match +^EXIT=10$ +^SIGNAL=0$ +^ assertion failure file main.c line 3 .*\n foo\(2\).*\n bar\(0\).*\n main\(\).* +-- +^warning: ignoring diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 8f6e92cb262..6e11e67eac8 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -201,8 +201,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options) cmdline.isset("outfile")) options.set_option("stop-on-fail", true); - if(cmdline.isset("trace") || - cmdline.isset("stop-on-fail")) + if( + cmdline.isset("trace") || cmdline.isset("stack-trace") || + cmdline.isset("stop-on-fail")) options.set_option("trace", true); if(cmdline.isset("localize-faults")) diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp index 2eb97a9112e..1de01cc2bfe 100644 --- a/src/goto-programs/goto_trace.cpp +++ b/src/goto-programs/goto_trace.cpp @@ -285,7 +285,7 @@ bool is_index_member_symbol(const exprt &src) return false; } -void show_goto_trace( +void show_full_goto_trace( std::ostream &out, const namespacet &ns, const goto_tracet &goto_trace, @@ -488,6 +488,94 @@ void show_goto_trace( } } +void show_goto_stack_trace( + std::ostream &out, + const namespacet &ns, + const goto_tracet &goto_trace, + const trace_optionst &options) +{ + // map from thread number to a call stack + std::map> + call_stacks; + + // by default, we show thread 0 + unsigned thread_to_show = 0; + + for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end(); + s_it++) + { + const auto &step = *s_it; + auto &stack = call_stacks[step.thread_nr]; + + if(step.is_assert()) + { + if(!step.cond_value) + { + stack.push_back(s_it); + thread_to_show = step.thread_nr; + } + } + else if(step.is_function_call()) + { + stack.push_back(s_it); + } + else if(step.is_function_return()) + { + stack.pop_back(); + } + } + + const auto &stack = call_stacks[thread_to_show]; + + // print in reverse order + for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++) + { + const auto &step = **s_it; + if(step.is_assert()) + { + out << " assertion failure"; + if(!step.pc->source_location.is_nil()) + out << ' ' << step.pc->source_location; + out << '\n'; + } + else if(step.is_function_call()) + { + out << " " << step.function_identifier; + out << '('; + + bool first = true; + for(auto &arg : step.function_arguments) + { + if(first) + first = false; + else + out << ", "; + + out << from_expr(ns, step.function_identifier, arg); + } + + out << ')'; + + if(!step.pc->source_location.is_nil()) + out << ' ' << step.pc->source_location; + + out << '\n'; + } + } +} + +void show_goto_trace( + std::ostream &out, + const namespacet &ns, + const goto_tracet &goto_trace, + const trace_optionst &options) +{ + if(options.stack_trace) + show_goto_stack_trace(out, ns, goto_trace, options); + else + show_full_goto_trace(out, ns, goto_trace, options); +} + void show_goto_trace( std::ostream &out, const namespacet &ns, diff --git a/src/goto-programs/goto_trace.h b/src/goto-programs/goto_trace.h index 2d3a0ed94d5..e550e3e1535 100644 --- a/src/goto-programs/goto_trace.h +++ b/src/goto-programs/goto_trace.h @@ -205,6 +205,7 @@ struct trace_optionst bool base_prefix; bool show_function_calls; bool show_code; + bool stack_trace; static const trace_optionst default_options; @@ -215,6 +216,7 @@ struct trace_optionst base_prefix = hex_representation; show_function_calls = options.get_bool_option("trace-show-function-calls"); show_code = options.get_bool_option("trace-show-code"); + stack_trace = options.get_bool_option("stack-trace"); }; private: @@ -225,6 +227,7 @@ struct trace_optionst base_prefix = false; show_function_calls = false; show_code = false; + stack_trace = false; }; }; @@ -246,27 +249,30 @@ void trace_value( const exprt &full_lhs, const exprt &value); - -#define OPT_GOTO_TRACE "(trace-json-extended)" \ - "(trace-show-function-calls)" \ - "(trace-show-code)" \ - "(trace-hex)" +#define OPT_GOTO_TRACE \ + "(trace-json-extended)" \ + "(trace-show-function-calls)" \ + "(trace-show-code)" \ + "(trace-hex)" \ + "(stack-trace)" #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" + " --trace-hex represent plain trace values in hex\n" \ + " --stack-trace give a stack trace only\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-show-code")) \ - options.set_option("trace-show-code", 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); - + options.set_option("trace-hex", true); \ + if(cmdline.isset("stack-trace")) \ + options.set_option("stack-trace", true); #endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H