Skip to content

added --compact-trace option [blocks: #3459] #3458

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
Nov 29, 2018
Merged

added --compact-trace option [blocks: #3459] #3458

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
14 changes: 14 additions & 0 deletions regression/cbmc/compact-trace/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
int x;

int bar(int bar_a)
{
x = 2;
x++;
__CPROVER_assert(0, "assertion");
}

int main()
{
x = 1;
bar(0);
}
10 changes: 10 additions & 0 deletions regression/cbmc/compact-trace/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
main.c
--compact-trace
activate-multi-line-match
^EXIT=10$
^SIGNAL=0$
^↳ main\.c:10 main\(\)\n 12: x=1 .*$
^↳ main.c:13 bar\(0\)\n 13: bar_a=0 .*\n 5: x=2 .*\n 6: x=3 .*$
--
^warning: ignoring
1 change: 1 addition & 0 deletions scripts/delete_failing_smt2_solver_tests
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,7 @@ rm byte_update6/test.desc
rm byte_update7/test.desc
rm byte_update8/test.desc
rm byte_update9/test.desc
rm compact-trace/test.desc
rm dynamic_size1/stack_object.desc
rm equality_through_array1/test.desc
rm equality_through_array2/test.desc
Expand Down
6 changes: 4 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,9 +201,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
options.set_option("stop-on-fail", true);

if(
cmdline.isset("trace") || cmdline.isset("stack-trace") ||
cmdline.isset("stop-on-fail"))
cmdline.isset("trace") || cmdline.isset("compact-trace") ||
cmdline.isset("stack-trace") || cmdline.isset("stop-on-fail"))
Copy link
Collaborator

Choose a reason for hiding this comment

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

Please add braces for readability.

Copy link
Member Author

Choose a reason for hiding this comment

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

ok

{
options.set_option("trace", true);
}

if(cmdline.isset("localize-faults"))
options.set_option("localize-faults", true);
Expand Down
150 changes: 142 additions & 8 deletions src/goto-programs/goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -264,7 +264,7 @@ void trace_value(
if(lhs_object.has_value())
identifier=lhs_object->get_identifier();

out << " " << from_expr(ns, identifier, full_lhs) << '=';
out << from_expr(ns, identifier, full_lhs) << '=';

if(value.is_nil())
out << "(assignment removed)";
Expand Down Expand Up @@ -348,6 +348,136 @@ bool is_index_member_symbol(const exprt &src)
return false;
}

/// \brief show a compact variant of the goto trace on the console
/// \param out the output stream
/// \param ns the namespace
/// \param goto_trace the trace to be shown
/// \param options any options, e.g., numerical representation
void show_compact_goto_trace(
messaget::mstreamt &out,
const namespacet &ns,
const goto_tracet &goto_trace,
const trace_optionst &options)
{
std::size_t function_depth = 0;

for(const auto &step : goto_trace.steps)
{
if(step.is_function_call())
function_depth++;
else if(step.is_function_return())
function_depth--;

// hide the hidden ones
if(step.hidden)
continue;

switch(step.type)
{
case goto_trace_stept::typet::ASSERT:
if(!step.cond_value)
{
out << '\n';
out << messaget::red << "Violated property:" << messaget::reset << '\n';
if(!step.pc->source_location.is_nil())
out << " " << state_location(step, ns) << '\n';

out << " " << messaget::red << step.comment << messaget::reset << '\n';

if(step.pc->is_assert())
out << " " << from_expr(ns, step.function, step.pc->guard) << '\n';

out << '\n';
}
break;

case goto_trace_stept::typet::ASSIGNMENT:
if(
step.assignment_type ==
goto_trace_stept::assignment_typet::ACTUAL_PARAMETER)
{
break;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Braces, please.

Copy link
Member Author

Choose a reason for hiding this comment

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

ok

}

out << " ";

if(!step.pc->source_location.get_line().empty())
{
out << messaget::faint << step.pc->source_location.get_line() << ':'
<< messaget::reset << ' ';
}

trace_value(
out,
ns,
step.get_lhs_object(),
step.full_lhs,
step.full_lhs_value,
options);
break;

case goto_trace_stept::typet::FUNCTION_CALL:
// downwards arrow
out << '\n' << messaget::faint << u8"\u21b3" << messaget::reset << ' ';
if(!step.pc->source_location.get_file().empty())
{
out << messaget::faint << step.pc->source_location.get_file();

if(!step.pc->source_location.get_line().empty())
{
out << messaget::faint << ':' << step.pc->source_location.get_line();
}

out << messaget::reset << ' ';
}

{
// show the display name
const auto &f_symbol = ns.lookup(step.called_function);
out << f_symbol.display_name();
Copy link
Collaborator

Choose a reason for hiding this comment

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

Actually the above comment might just add confusion: symbolt has a pretty_name...

Copy link
Member Author

Choose a reason for hiding this comment

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

fixed

}

out << '(';

{
bool first = true;
Copy link
Member

Choose a reason for hiding this comment

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

💡
The pattern is very simple, but given the number of times we have this in the code base, it could be worth introducing something like this:

join(
  step.function_arguments.begin(), step.function_arguments.end(), 
  [](arg) {out << from_expr(ns, step.function, arg);},
  []() {out << ", ";});

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think you can already do this:

auto arg_strings = make_range(step.function_arguments).map<std::string>(
  [&this](const exprt &arg) { return from_expr(ns, step.function, e); });
join_strings(out, arg_strings.begin(), arg_strings.end(), ", ");

And if the above works we should likely use it in lots of places :-)

Copy link
Member Author

Choose a reason for hiding this comment

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

The range type doesn't have a difference_type, and thus, that doesn't work.

Separate PR.

Copy link
Member Author

Choose a reason for hiding this comment

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

#3477

for(auto &arg : step.function_arguments)
{
if(first)
first = false;
else
out << ", ";

out << from_expr(ns, step.function, arg);
}
}
out << ")\n";
break;

case goto_trace_stept::typet::FUNCTION_RETURN:
// upwards arrow
out << messaget::faint << u8"\u21b5" << messaget::reset << '\n';
break;

case goto_trace_stept::typet::ASSUME:
case goto_trace_stept::typet::LOCATION:
case goto_trace_stept::typet::GOTO:
case goto_trace_stept::typet::DECL:
case goto_trace_stept::typet::OUTPUT:
case goto_trace_stept::typet::INPUT:
case goto_trace_stept::typet::SPAWN:
case goto_trace_stept::typet::MEMORY_BARRIER:
case goto_trace_stept::typet::ATOMIC_BEGIN:
case goto_trace_stept::typet::ATOMIC_END:
case goto_trace_stept::typet::DEAD:
break;

default:
Copy link
Collaborator

Choose a reason for hiding this comment

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

This shouldn't be necessary.

Copy link
Member Author

Choose a reason for hiding this comment

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

fixed

UNREACHABLE;
}
}
}

void show_full_goto_trace(
messaget::mstreamt &out,
const namespacet &ns,
Expand Down Expand Up @@ -419,13 +549,14 @@ void show_full_goto_trace(
show_state_header(out, ns, step, step.step_nr, options);
}

trace_value(
out,
ns,
step.get_lhs_object(),
step.full_lhs,
step.full_lhs_value,
options);
out << " ";
trace_value(
out,
ns,
step.get_lhs_object(),
step.full_lhs,
step.full_lhs_value,
options);
}
break;

Expand All @@ -437,6 +568,7 @@ void show_full_goto_trace(
show_state_header(out, ns, step, step.step_nr, options);
}

out << " ";
trace_value(
out, ns, step.get_lhs_object(), step.full_lhs, step.full_lhs_value, options);
break;
Expand Down Expand Up @@ -623,6 +755,8 @@ void show_goto_trace(
{
if(options.stack_trace)
show_goto_stack_trace(out, ns, goto_trace);
else if(options.compact_trace)
show_compact_goto_trace(out, ns, goto_trace, options);
else
show_full_goto_trace(out, ns, goto_trace, options);
}
Expand Down
7 changes: 7 additions & 0 deletions src/goto-programs/goto_trace.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -200,6 +200,7 @@ struct trace_optionst
bool base_prefix;
bool show_function_calls;
bool show_code;
bool compact_trace;
bool stack_trace;

static const trace_optionst default_options;
Expand All @@ -211,6 +212,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");
compact_trace = options.get_bool_option("compact-trace");
stack_trace = options.get_bool_option("stack-trace");
};

Expand All @@ -222,6 +224,7 @@ struct trace_optionst
base_prefix = false;
show_function_calls = false;
show_code = false;
compact_trace = false;
stack_trace = false;
};
};
Expand Down Expand Up @@ -250,13 +253,15 @@ void trace_value(
"(trace-show-function-calls)" \
"(trace-show-code)" \
"(trace-hex)" \
"(compact-trace)" \
"(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" \
" --compact-trace give a compact trace\n" \
" --stack-trace give a stack trace only\n"

#define PARSE_OPTIONS_GOTO_TRACE(cmdline, options) \
Expand All @@ -268,6 +273,8 @@ void trace_value(
options.set_option("trace-show-code", true); \
if(cmdline.isset("trace-hex")) \
options.set_option("trace-hex", true); \
if(cmdline.isset("compact-trace")) \
options.set_option("compact-trace", true); \
if(cmdline.isset("stack-trace")) \
options.set_option("stack-trace", true);

Expand Down