Skip to content

goto_trace now contains the arguments of function calls #2819

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 2 commits into from
Aug 23, 2018
Merged

goto_trace now contains the arguments of function calls #2819

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
08cbe58
add arguments of function calls to goto_trace
Aug 22, 2018
bf717d3
show function arguments in trace
Aug 22, 2018
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
4 changes: 2 additions & 2 deletions regression/cbmc/trace_show_function_calls/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ main.c
--trace --trace-show-function-calls
^EXIT=10$
^SIGNAL=0$
Function call: function_to_call \(depth 2\)
Function call: function_to_call\(-2147483647\) \(depth 2\)
Copy link
Contributor

Choose a reason for hiding this comment

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

Are these random nondet choices? If so they're probably not good to constrain in the test

Copy link
Collaborator

Choose a reason for hiding this comment

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

No, they seem to be hard-coded in the test. (I'm just wondering whether the values are portable across all architectures.)

Function return: function_to_call \(depth 1\)
Function call: function_to_call \(depth 2\)
Function call: function_to_call\(-2\) \(depth 2\)
^VERIFICATION FAILED$
--
^warning: ignoring
23 changes: 21 additions & 2 deletions src/goto-programs/goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -444,15 +444,34 @@ void show_goto_trace(
case goto_trace_stept::typet::FUNCTION_CALL:
function_depth++;
if(options.show_function_calls)
out << "\n#### Function call: " << step.function_identifier
<< " (depth " << function_depth << ") ####\n";
{
out << "\n#### Function call: " << 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 << ") (depth " << function_depth << ") ####\n";
}
break;

case goto_trace_stept::typet::FUNCTION_RETURN:
function_depth--;
if(options.show_function_calls)
{
out << "\n#### Function return: " << step.function_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:
Expand Down
3 changes: 3 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 @@ -122,6 +122,9 @@ class goto_trace_stept
// for function call/return
irep_idt function_identifier;

// for function call
std::vector<exprt> function_arguments;

/*! \brief outputs the trace step in ASCII to a given stream
*/
void output(
Expand Down
5 changes: 5 additions & 0 deletions src/goto-symex/build_goto_trace.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -304,12 +304,17 @@ void build_goto_trace(
{
goto_trace_step.lhs_object.make_nil();
}

goto_trace_step.type = SSA_step.type;
goto_trace_step.hidden = SSA_step.hidden;
goto_trace_step.format_string = SSA_step.format_string;
goto_trace_step.io_id = SSA_step.io_id;
goto_trace_step.formatted = SSA_step.formatted;
goto_trace_step.function_identifier = SSA_step.function_identifier;
goto_trace_step.function_arguments = SSA_step.converted_function_arguments;

for(auto &arg : goto_trace_step.function_arguments)
arg = prop_conv.get(arg);

// update internal field for specific variables in the counterexample
update_internal_field(SSA_step, goto_trace_step, ns);
Expand Down
13 changes: 7 additions & 6 deletions src/goto-symex/symex_function_call.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -254,8 +254,14 @@ void goto_symext::symex_function_call_code(
return;
}

// read the arguments -- before the locality renaming
exprt::operandst arguments = call.arguments();
for(auto &a : arguments)
state.rename(a, ns);

// record the call
target.function_call(state.guard.as_expr(), identifier, state.source);
target.function_call(
state.guard.as_expr(), identifier, arguments, state.source);

if(!goto_function.body_available())
{
Expand All @@ -276,11 +282,6 @@ void goto_symext::symex_function_call_code(
return;
}

// read the arguments -- before the locality renaming
exprt::operandst arguments=call.arguments();
for(auto &a : arguments)
state.rename(a, ns);

// produce a new frame
PRECONDITION(!state.call_stack().empty());
goto_symex_statet::framet &frame=state.new_frame();
Expand Down
3 changes: 2 additions & 1 deletion src/goto-symex/symex_target.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,7 +105,8 @@ class symex_targett
virtual void function_call(
const exprt &guard,
const irep_idt &function_identifier,
const sourcet &source)=0;
const std::vector<exprt> &ssa_function_arguments,
const sourcet &source) = 0;

// record return from a function
virtual void function_return(
Expand Down
40 changes: 39 additions & 1 deletion src/goto-symex/symex_target_equation.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -210,6 +210,7 @@ void symex_target_equationt::location(
void symex_target_equationt::function_call(
const exprt &guard,
const irep_idt &function_identifier,
const std::vector<exprt> &ssa_function_arguments,
const sourcet &source)
{
SSA_steps.push_back(SSA_stept());
Expand All @@ -219,6 +220,7 @@ void symex_target_equationt::function_call(
SSA_step.type = goto_trace_stept::typet::FUNCTION_CALL;
SSA_step.source = source;
SSA_step.function_identifier = function_identifier;
SSA_step.ssa_function_arguments = ssa_function_arguments;

merge_ireps(SSA_step);
}
Expand Down Expand Up @@ -383,6 +385,7 @@ void symex_target_equationt::convert(
convert_assumptions(prop_conv);
convert_assertions(prop_conv);
convert_goto_instructions(prop_conv);
convert_function_calls(prop_conv);
convert_io(prop_conv);
convert_constraints(prop_conv);
}
Expand Down Expand Up @@ -658,6 +661,39 @@ void symex_target_equationt::convert_assertions(
prop_conv.set_to_true(disjunction(disjuncts));
}

/// converts function calls
/// \par parameters: decision procedure
/// \return -
void symex_target_equationt::convert_function_calls(
decision_proceduret &dec_proc)
{
std::size_t argument_count=0;

for(auto &step : SSA_steps)
if(!step.ignore)
{
step.converted_function_arguments.reserve(step.ssa_function_arguments.size());

for(const auto &arg : step.ssa_function_arguments)
{
if(arg.is_constant() ||
arg.id()==ID_string_constant)
step.converted_function_arguments.push_back(arg);
else
{
const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
symbol_exprt symbol(identifier, arg.type());

equal_exprt eq(arg, symbol);
merge_irep(eq);

dec_proc.set_to(eq, true);
step.converted_function_arguments.push_back(symbol);
}
}
}
}

/// converts I/O
/// \par parameters: decision procedure
/// \return -
Expand Down Expand Up @@ -690,7 +726,6 @@ void symex_target_equationt::convert_io(
}
}


void symex_target_equationt::merge_ireps(SSA_stept &SSA_step)
{
merge_irep(SSA_step.guard);
Expand All @@ -705,6 +740,9 @@ void symex_target_equationt::merge_ireps(SSA_stept &SSA_step)
for(auto &step : SSA_step.io_args)
merge_irep(step);

for(auto &arg : SSA_step.ssa_function_arguments)
merge_irep(arg);

// converted_io_args is merged in convert_io
}

Expand Down
6 changes: 6 additions & 0 deletions src/goto-symex/symex_target_equation.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ class symex_target_equationt:public symex_targett
virtual void function_call(
const exprt &guard,
const irep_idt &function_identifier,
const std::vector<exprt> &ssa_function_arguments,
const sourcet &source);

// record return from a function
Expand Down Expand Up @@ -163,6 +164,7 @@ class symex_target_equationt:public symex_targett
void convert_constraints(decision_proceduret &decision_procedure) const;
void convert_goto_instructions(prop_convt &prop_conv);
void convert_guards(prop_convt &prop_conv);
void convert_function_calls(decision_proceduret &decision_procedure);
void convert_io(decision_proceduret &decision_procedure);

exprt make_expression() const;
Expand Down Expand Up @@ -232,6 +234,10 @@ class symex_target_equationt:public symex_targett
// for function call/return
irep_idt function_identifier;

// for function calls
std::vector<exprt> ssa_function_arguments,
converted_function_arguments;

// for SHARED_READ/SHARED_WRITE and ATOMIC_BEGIN/ATOMIC_END
unsigned atomic_section_id=0;

Expand Down