Skip to content

Move call_stack_history to own file #5384

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
Jun 23, 2020
Merged

Move call_stack_history to own file #5384

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
8ae6e36
Move call_stack_historyt to its own file
Jun 18, 2020
2f4108d
Clang-format wants to reorder the header inclusion
Jun 18, 2020
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
1 change: 1 addition & 0 deletions src/analyses/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ SRC = ai.cpp \
ai_history.cpp \
call_graph.cpp \
call_graph_helpers.cpp \
call_stack_history.cpp \
constant_propagator.cpp \
custom_bitvector_analysis.cpp \
dependence_graph.cpp \
Expand Down
202 changes: 0 additions & 202 deletions src/analyses/ai_history.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,205 +27,3 @@ xmlt ai_history_baset::output_xml(void) const
xml.data = out.str();
return xml;
}

ai_history_baset::step_returnt
call_stack_historyt::step(locationt to, const trace_sett &others) const
{
DATA_INVARIANT(current_stack != nullptr, "current_stack must exist");

cse_ptrt next_stack = nullptr;

// First construct what the new history would be.
// This requires special handling if this edge is a function call or return
if(current_stack->current_location->is_function_call())
{
locationt l_return = std::next(current_stack->current_location);

if(l_return->location_number == to->location_number)
{
// Is skipping the function call, only update the location
next_stack = cse_ptrt(
std::make_shared<call_stack_entryt>(l_return, current_stack->caller));
}
else
{
// An interprocedural (call) edge; add to the current stack

// If the recursion limit has been reached
// shorten the stack / merge with the most recent invocation
// before we extend
cse_ptrt shorten = current_stack;

if(has_recursion_limit())
{
unsigned int number_of_recursive_calls = 0;
cse_ptrt first_found = nullptr; // The most recent recursive call

// Iterate back through the call stack
for(cse_ptrt i = current_stack->caller; i != nullptr; i = i->caller)
{
if(
i->current_location->location_number ==
current_stack->current_location->location_number)
{
// Found a recursive instance
if(first_found == nullptr)
{
first_found = i;
}
++number_of_recursive_calls;
if(number_of_recursive_calls == recursion_limit)
{
shorten = first_found;
break;
}
}
}
}

next_stack = cse_ptrt(std::make_shared<call_stack_entryt>(to, shorten));
}
}
else if(current_stack->current_location->is_end_function())
{
if(current_stack->caller == nullptr)
{
// Trying to return but there was no caller?
// Refuse to do the transition outright
return std::make_pair(ai_history_baset::step_statust::BLOCKED, nullptr);
}
else
{
// The expected call return site...
locationt l_caller_return =
std::next(current_stack->caller->current_location);

if(l_caller_return->location_number == to->location_number)
{
// ... which is where we are going
next_stack = cse_ptrt(std::make_shared<call_stack_entryt>(
to, current_stack->caller->caller));
}
else
{
// Not possible to return to somewhere other than the call site
return std::make_pair(ai_history_baset::step_statust::BLOCKED, nullptr);
}
}
}
else
{
// Just update the location
next_stack =
cse_ptrt(std::make_shared<call_stack_entryt>(to, current_stack->caller));
}
INVARIANT(next_stack != nullptr, "All branches should initialise next_stack");

// Create the potential next history
trace_ptrt next(new call_stack_historyt(next_stack, recursion_limit));
// It would be nice to use make_shared here but ... that doesn't work with
// protected constructors

// If there is already an equivalent history, merge with that instead
auto it = others.find(next);

if(it == others.end())
{
return std::make_pair(ai_history_baset::step_statust::NEW, next);
}
else
{
return std::make_pair(ai_history_baset::step_statust::MERGED, *it);
}
}

bool call_stack_historyt::operator<(const ai_history_baset &op) const
{
auto other = dynamic_cast<const call_stack_historyt *>(&op);
PRECONDITION(other != nullptr);

return *(this->current_stack) < *(other->current_stack);
}

bool call_stack_historyt::operator==(const ai_history_baset &op) const
{
auto other = dynamic_cast<const call_stack_historyt *>(&op);
PRECONDITION(other != nullptr);

return *(this->current_stack) == *(other->current_stack);
}

void call_stack_historyt::output(std::ostream &out) const
{
out << "call_stack_history : stack "
<< current_stack->current_location->location_number;
cse_ptrt working = current_stack->caller;
while(working != nullptr)
{
out << " from " << working->current_location->location_number;
working = working->caller;
}
return;
}

bool call_stack_historyt::call_stack_entryt::
operator<(const call_stack_entryt &op) const
{
if(
this->current_location->location_number <
op.current_location->location_number)
{
return true;
}
else if(
this->current_location->location_number >
op.current_location->location_number)
{
return false;
}
else
{
INVARIANT(
this->current_location->location_number ==
op.current_location->location_number,
"Implied by if-then-else");

if(this->caller == op.caller)
{
return false; // Because they are equal
}
else if(this->caller == nullptr)
{
return true; // Shorter stacks are 'lower'
}
else if(op.caller == nullptr)
{
return false;
}
else
{
// Sort by the rest of the stack
return *(this->caller) < *(op.caller);
}
}
UNREACHABLE;
}

bool call_stack_historyt::call_stack_entryt::
operator==(const call_stack_entryt &op) const
{
if(
this->current_location->location_number ==
op.current_location->location_number)
{
if(this->caller == op.caller)
{
return true;
}
else if(this->caller != nullptr && op.caller != nullptr)
{
return *(this->caller) == *(op.caller);
}
}
return false;
}
111 changes: 0 additions & 111 deletions src/analyses/ai_history.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -219,93 +219,6 @@ class ahistoricalt : public ai_history_baset
}
};

/// Records the call stack
/// Care must be taken when using this on recursive code; it will need the
/// domain to be capable of limiting the recursion.
class call_stack_historyt : public ai_history_baset
{
protected:
class call_stack_entryt;
typedef std::shared_ptr<const call_stack_entryt> cse_ptrt;
class call_stack_entryt
{
public:
locationt current_location;
cse_ptrt caller;

call_stack_entryt(locationt l, cse_ptrt p) : current_location(l), caller(p)
{
}

bool operator<(const call_stack_entryt &op) const;
bool operator==(const call_stack_entryt &op) const;
};

cse_ptrt current_stack;
// DATA_INVARIANT(current_stack != nullptr, "current_stack must exist");
// DATA_INVARIANT(current_stack->current.is_dereferenceable(),
// "Must not be _::end()")

// At what point to merge with a previous call stack when handling recursion
// Setting to 0 disables completely
unsigned int recursion_limit;

bool has_recursion_limit(void) const
{
return recursion_limit != 0;
}

call_stack_historyt(cse_ptrt cur_stack, unsigned int rec_lim)
: ai_history_baset(cur_stack->current_location),
current_stack(cur_stack),
recursion_limit(rec_lim)
{
PRECONDITION(
cur_stack != nullptr); // A little late by now but worth documenting
}

public:
explicit call_stack_historyt(locationt l)
: ai_history_baset(l),
current_stack(std::make_shared<call_stack_entryt>(l, nullptr)),
recursion_limit(0)
{
}

call_stack_historyt(locationt l, unsigned int rec_lim)
: ai_history_baset(l),
current_stack(std::make_shared<call_stack_entryt>(l, nullptr)),
recursion_limit(rec_lim)
{
}

call_stack_historyt(const call_stack_historyt &old)
: ai_history_baset(old),
current_stack(old.current_stack),
recursion_limit(old.recursion_limit)
{
}

step_returnt step(locationt to, const trace_sett &others) const override;

bool operator<(const ai_history_baset &op) const override;
bool operator==(const ai_history_baset &op) const override;

const locationt &current_location(void) const override
{
return current_stack->current_location;
}

// Use default widening
// Typically this would be used for loops, which are not tracked
// it would be possible to use this to improve the handling of recursion
bool should_widen(const ai_history_baset &other) const override
{
return ai_history_baset::should_widen(other);
}

void output(std::ostream &out) const override;
};

/// As more detailed histories can get complex (for example, nested loops
/// or deep, mutually recursive call stacks) they often need some user
Expand Down Expand Up @@ -335,28 +248,4 @@ class ai_history_factory_default_constructort : public ai_history_factory_baset
}
};

// Allows passing a recursion limit
class call_stack_history_factoryt : public ai_history_factory_baset
{
protected:
unsigned int recursion_limit;

public:
explicit call_stack_history_factoryt(unsigned int rec_lim)
: recursion_limit(rec_lim)
{
}

ai_history_baset::trace_ptrt epoch(ai_history_baset::locationt l) override
{
ai_history_baset::trace_ptrt p(
std::make_shared<call_stack_historyt>(l, recursion_limit));
return p;
}

virtual ~call_stack_history_factoryt()
{
}
};

#endif // CPROVER_ANALYSES_AI_HISTORY_H
Loading