diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 23a1fcf17f4..cf9b65bb66e 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -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 \ diff --git a/src/analyses/ai_history.cpp b/src/analyses/ai_history.cpp index e07b93e9653..06bc366107e 100644 --- a/src/analyses/ai_history.cpp +++ b/src/analyses/ai_history.cpp @@ -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(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(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( - 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(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(&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(&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; -} diff --git a/src/analyses/ai_history.h b/src/analyses/ai_history.h index abc4ff74f8b..358d72a1005 100644 --- a/src/analyses/ai_history.h +++ b/src/analyses/ai_history.h @@ -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 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(l, nullptr)), - recursion_limit(0) - { - } - - call_stack_historyt(locationt l, unsigned int rec_lim) - : ai_history_baset(l), - current_stack(std::make_shared(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 ¤t_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 @@ -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(l, recursion_limit)); - return p; - } - - virtual ~call_stack_history_factoryt() - { - } -}; - #endif // CPROVER_ANALYSES_AI_HISTORY_H diff --git a/src/analyses/call_stack_history.cpp b/src/analyses/call_stack_history.cpp new file mode 100644 index 00000000000..62c2f30dbf4 --- /dev/null +++ b/src/analyses/call_stack_history.cpp @@ -0,0 +1,214 @@ +/*******************************************************************\ + +Module: Abstract Interpretation + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +/// \file +/// History for tracking the call stack and performing interprocedural analysis + +#include "call_stack_history.h" + +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(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(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( + 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(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(&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(&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; +} diff --git a/src/analyses/call_stack_history.h b/src/analyses/call_stack_history.h new file mode 100644 index 00000000000..fc899e796ad --- /dev/null +++ b/src/analyses/call_stack_history.h @@ -0,0 +1,129 @@ +/*******************************************************************\ + +Module: Abstract Interpretation + +Author: Martin Brain, martin.brain@cs.ox.ac.uk + +\*******************************************************************/ + +/// \file +/// History for tracking the call stack and performing interprocedural analysis + +#ifndef CPROVER_ANALYSES_CALL_STACK_HISTORY_H +#define CPROVER_ANALYSES_CALL_STACK_HISTORY_H + +#include "ai_history.h" + +/// 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 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(l, nullptr)), + recursion_limit(0) + { + } + + call_stack_historyt(locationt l, unsigned int rec_lim) + : ai_history_baset(l), + current_stack(std::make_shared(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 ¤t_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; +}; + +// 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(l, recursion_limit)); + return p; + } + + virtual ~call_stack_history_factoryt() + { + } +}; + +#endif // CPROVER_ANALYSES_CALL_STACK_HISTORY_H diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 8dd8d94f09b..972134614e2 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp @@ -42,12 +42,13 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include -#include +#include #include #include +#include #include +#include +#include #include #include