Skip to content

Commit 2e3fd61

Browse files
kroeningkroening
authored
Merge pull request diffblue#2832 from diffblue/stack-trace
Stack traces
2 parents cbe16b3 + a594f9f commit 2e3fd61

File tree

6 files changed

+135
-15
lines changed

6 files changed

+135
-15
lines changed

‎jbmc/src/jbmc/jbmc_parse_options.cpp‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -135,8 +135,9 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
135135
cmdline.isset("outfile"))
136136
options.set_option("stop-on-fail", true);
137137

138-
if(cmdline.isset("trace") ||
139-
cmdline.isset("stop-on-fail"))
138+
if(
139+
cmdline.isset("trace") || cmdline.isset("stack-trace") ||
140+
cmdline.isset("stop-on-fail"))
140141
options.set_option("trace", true);
141142

142143
if(cmdline.isset("localize-faults"))

‎regression/cbmc/stack-trace/main.c‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int foo(int foo_a)
2+
{
3+
__CPROVER_assert(foo_a != 2, "assertion");
4+
}
5+
6+
int bar(int bar_a)
7+
{
8+
foo(bar_a + 1);
9+
foo(bar_a + 2);
10+
}
11+
12+
int main()
13+
{
14+
bar(0);
15+
}

‎regression/cbmc/stack-trace/test.desc‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
main.c
3+
--stack-trace
4+
activate-multi-line-match
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
^ assertion failure file main.c line 3 .*\n foo\(2\).*\n bar\(0\).*\n main\(\).*
8+
--
9+
^warning: ignoring

‎src/cbmc/cbmc_parse_options.cpp‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -201,8 +201,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
201201
cmdline.isset("outfile"))
202202
options.set_option("stop-on-fail", true);
203203

204-
if(cmdline.isset("trace") ||
205-
cmdline.isset("stop-on-fail"))
204+
if(
205+
cmdline.isset("trace") || cmdline.isset("stack-trace") ||
206+
cmdline.isset("stop-on-fail"))
206207
options.set_option("trace", true);
207208

208209
if(cmdline.isset("localize-faults"))

‎src/goto-programs/goto_trace.cpp‎

Lines changed: 89 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -285,7 +285,7 @@ bool is_index_member_symbol(const exprt &src)
285285
return false;
286286
}
287287

288-
void show_goto_trace(
288+
void show_full_goto_trace(
289289
std::ostream &out,
290290
const namespacet &ns,
291291
const goto_tracet &goto_trace,
@@ -488,6 +488,94 @@ void show_goto_trace(
488488
}
489489
}
490490

491+
void show_goto_stack_trace(
492+
std::ostream &out,
493+
const namespacet &ns,
494+
const goto_tracet &goto_trace,
495+
const trace_optionst &options)
496+
{
497+
// map from thread number to a call stack
498+
std::map<unsigned, std::vector<goto_tracet::stepst::const_iterator>>
499+
call_stacks;
500+
501+
// by default, we show thread 0
502+
unsigned thread_to_show = 0;
503+
504+
for(auto s_it = goto_trace.steps.begin(); s_it != goto_trace.steps.end();
505+
s_it++)
506+
{
507+
const auto &step = *s_it;
508+
auto &stack = call_stacks[step.thread_nr];
509+
510+
if(step.is_assert())
511+
{
512+
if(!step.cond_value)
513+
{
514+
stack.push_back(s_it);
515+
thread_to_show = step.thread_nr;
516+
}
517+
}
518+
else if(step.is_function_call())
519+
{
520+
stack.push_back(s_it);
521+
}
522+
else if(step.is_function_return())
523+
{
524+
stack.pop_back();
525+
}
526+
}
527+
528+
const auto &stack = call_stacks[thread_to_show];
529+
530+
// print in reverse order
531+
for(auto s_it = stack.rbegin(); s_it != stack.rend(); s_it++)
532+
{
533+
const auto &step = **s_it;
534+
if(step.is_assert())
535+
{
536+
out << " assertion failure";
537+
if(!step.pc->source_location.is_nil())
538+
out << ' ' << step.pc->source_location;
539+
out << '\n';
540+
}
541+
else if(step.is_function_call())
542+
{
543+
out << " " << step.function_identifier;
544+
out << '(';
545+
546+
bool first = true;
547+
for(auto &arg : step.function_arguments)
548+
{
549+
if(first)
550+
first = false;
551+
else
552+
out << ", ";
553+
554+
out << from_expr(ns, step.function_identifier, arg);
555+
}
556+
557+
out << ')';
558+
559+
if(!step.pc->source_location.is_nil())
560+
out << ' ' << step.pc->source_location;
561+
562+
out << '\n';
563+
}
564+
}
565+
}
566+
567+
void show_goto_trace(
568+
std::ostream &out,
569+
const namespacet &ns,
570+
const goto_tracet &goto_trace,
571+
const trace_optionst &options)
572+
{
573+
if(options.stack_trace)
574+
show_goto_stack_trace(out, ns, goto_trace, options);
575+
else
576+
show_full_goto_trace(out, ns, goto_trace, options);
577+
}
578+
491579
void show_goto_trace(
492580
std::ostream &out,
493581
const namespacet &ns,

‎src/goto-programs/goto_trace.h‎

Lines changed: 16 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -205,6 +205,7 @@ struct trace_optionst
205205
bool base_prefix;
206206
bool show_function_calls;
207207
bool show_code;
208+
bool stack_trace;
208209

209210
static const trace_optionst default_options;
210211

@@ -215,6 +216,7 @@ struct trace_optionst
215216
base_prefix = hex_representation;
216217
show_function_calls = options.get_bool_option("trace-show-function-calls");
217218
show_code = options.get_bool_option("trace-show-code");
219+
stack_trace = options.get_bool_option("stack-trace");
218220
};
219221

220222
private:
@@ -225,6 +227,7 @@ struct trace_optionst
225227
base_prefix = false;
226228
show_function_calls = false;
227229
show_code = false;
230+
stack_trace = false;
228231
};
229232
};
230233

@@ -246,27 +249,30 @@ void trace_value(
246249
const exprt &full_lhs,
247250
const exprt &value);
248251

249-
250-
#define OPT_GOTO_TRACE "(trace-json-extended)" \
251-
"(trace-show-function-calls)" \
252-
"(trace-show-code)" \
253-
"(trace-hex)"
252+
#define OPT_GOTO_TRACE \
253+
"(trace-json-extended)" \
254+
"(trace-show-function-calls)" \
255+
"(trace-show-code)" \
256+
"(trace-hex)" \
257+
"(stack-trace)"
254258

255259
#define HELP_GOTO_TRACE \
256260
" --trace-json-extended add rawLhs property to trace\n" \
257261
" --trace-show-function-calls show function calls in plain trace\n" \
258262
" --trace-show-code show original code in plain trace\n" \
259-
" --trace-hex represent plain trace values in hex\n"
263+
" --trace-hex represent plain trace values in hex\n" \
264+
" --stack-trace give a stack trace only\n"
260265

261266
#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
262267
if(cmdline.isset("trace-json-extended")) \
263268
options.set_option("trace-json-extended", true); \
264269
if(cmdline.isset("trace-show-function-calls")) \
265270
options.set_option("trace-show-function-calls", true); \
266-
if(cmdline.isset("trace-show-code")) \
267-
options.set_option("trace-show-code", true); \
271+
if(cmdline.isset("trace-show-code")) \
272+
options.set_option("trace-show-code", true); \
268273
if(cmdline.isset("trace-hex")) \
269-
options.set_option("trace-hex", true);
270-
274+
options.set_option("trace-hex", true); \
275+
if(cmdline.isset("stack-trace")) \
276+
options.set_option("stack-trace", true);
271277

272278
#endif // CPROVER_GOTO_PROGRAMS_GOTO_TRACE_H

0 commit comments

Comments
 (0)