Skip to content

Stack traces #2832

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Aug 25, 2018
Merged

Stack traces #2832

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions jbmc/src/jbmc/jbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"))
Expand Down
15 changes: 15 additions & 0 deletions regression/cbmc/stack-trace/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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);
}
9 changes: 9 additions & 0 deletions regression/cbmc/stack-trace/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
5 changes: 3 additions & 2 deletions src/cbmc/cbmc_parse_options.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"))
Expand Down
90 changes: 89 additions & 1 deletion src/goto-programs/goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
Copy link
Contributor

@thk123 thk123 Aug 24, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ Threads indexes are roughly contiguous (?) integers so probably a vector makes more sense than a 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];
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

⛏️ current_step_stack or perhaps just current_stack to distinguish from stack l


if(step.is_assert())
{
if(!step.cond_value)
{
stack.push_back(s_it);
thread_to_show = step.thread_nr;
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 a comment here explaining why we are changing which thread we show.

// switch to the thread that violated the assert

?

}
}
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,
Expand Down
26 changes: 16 additions & 10 deletions src/goto-programs/goto_trace.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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:
Expand All @@ -225,6 +227,7 @@ struct trace_optionst
base_prefix = false;
show_function_calls = false;
show_code = false;
stack_trace = false;
};
};

Expand All @@ -246,27 +249,30 @@ void trace_value(
const exprt &full_lhs,
const exprt &value);


#define OPT_GOTO_TRACE "(trace-json-extended)" \
Copy link
Member

@peterschrammel peterschrammel Aug 24, 2018 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Use // clang-format off to avoid this ugly reformatting. Cf. e.g. https://github.com/diffblue/cbmc/blob/develop/src/goto-programs/show_goto_functions.h#L21

"(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