diff --git a/regression/cbmc/reachability-slice-interproc/test.c b/regression/cbmc/reachability-slice-interproc/test.c new file mode 100644 index 00000000000..f149e6f0976 --- /dev/null +++ b/regression/cbmc/reachability-slice-interproc/test.c @@ -0,0 +1,76 @@ +#include + +// After a reachability slice based on the assertion in `target`, we should +// retain both its possible callers (...may_call_target_1, ...may_call_target_2) +// and their callees, but should be more precise concerning before_target and +// after_target, which even though they are also called by +// `unreachable_calls_before_target` and `unreachable_calls_after_target`, those +// functions are not reachable. + +void before_target() +{ + const char *local = "before_target_kept"; +} + +void after_target() +{ + const char *local = "after_target_kept"; +} + +void target() +{ + const char *local = "target_kept"; + + before_target(); + assert(0); + after_target(); +} + +void unreachable_calls_before_target() +{ + const char *local = "unreachable_calls_before_target_kept"; + before_target(); +} + +void unreachable_calls_after_target() +{ + const char *local = "unreachable_calls_after_target_kept"; + after_target(); +} + +void reachable_before_target_caller_1() +{ + const char *local = "reachable_before_target_caller_1_kept"; +} + +void reachable_after_target_caller_1() +{ + const char *local = "reachable_after_target_caller_1_kept"; +} + +void reachable_may_call_target_1() +{ + const char *local = "reachable_may_call_target_1_kept"; + reachable_before_target_caller_1(); + target(); + reachable_after_target_caller_1(); +} + +void reachable_before_target_caller_2() +{ + const char *local = "reachable_before_target_caller_2_kept"; +} + +void reachable_after_target_caller_2() +{ + const char *local = "reachable_after_target_caller_2_kept"; +} + +void reachable_may_call_target_2() +{ + const char *local = "reachable_may_call_target_2_kept"; + reachable_before_target_caller_2(); + target(); + reachable_after_target_caller_2(); +} + diff --git a/regression/cbmc/reachability-slice-interproc/test.desc b/regression/cbmc/reachability-slice-interproc/test.desc new file mode 100644 index 00000000000..d4d422fa6ba --- /dev/null +++ b/regression/cbmc/reachability-slice-interproc/test.desc @@ -0,0 +1,13 @@ +CORE +test.c +--reachability-slice-fb --show-goto-functions +target_kept +reachable_before_target_caller_1_kept +reachable_after_target_caller_1_kept +reachable_may_call_target_1_kept +reachable_before_target_caller_2_kept +reachable_after_target_caller_2_kept +reachable_may_call_target_2_kept +-- +unreachable_calls_before_target_kept +unreachable_calls_after_target_kept diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 9658c218a83..2f65d0b4893 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -44,6 +44,15 @@ reachability_slicert::get_sources( return sources; } +static bool is_same_target( + goto_programt::const_targett it1, + goto_programt::const_targett it2) +{ + // Avoid comparing iterators belonging to different functions, and therefore + // different std::lists. + return it1->function == it2->function && it1 == it2; +} + /// Perform backwards depth-first search of the control-flow graph of the /// goto program, starting from the nodes corresponding to the criterion and /// the instructions that might be executed concurrently. Set reaches_assertion @@ -54,11 +63,50 @@ void reachability_slicert::fixedpoint_to_assertions( const is_threadedt &is_threaded, slicing_criteriont &criterion) { - std::vector src = get_sources(is_threaded, criterion); + std::vector stack; + std::vector sources = get_sources(is_threaded, criterion); + for(const auto source : sources) + stack.emplace_back(source, false); + + while(!stack.empty()) + { + auto &node = cfg[stack.back().node_index]; + const auto caller_is_known = stack.back().caller_is_known; + stack.pop_back(); - std::vector reachable = cfg.get_reachable(src, false); - for(const auto index : reachable) - cfg[index].reaches_assertion = true; + if(node.reaches_assertion) + continue; + node.reaches_assertion = true; + + for(const auto &edge : node.in) + { + const auto &pred_node = cfg[edge.first]; + + if(pred_node.PC->is_end_function()) + { + // This is an end-of-function -> successor-of-callsite edge. + // Queue both the caller and the end of the callee. + INVARIANT( + std::prev(node.PC)->is_function_call(), + "all function return edges should point to the successor of a " + "FUNCTION_CALL instruction"); + stack.emplace_back(edge.first, true); + stack.emplace_back( + cfg.entry_map[std::prev(node.PC)], caller_is_known); + } + else if(pred_node.PC->is_function_call()) + { + // Skip this predecessor, unless this is a bodyless function, or we + // don't know who our callee was: + if(!caller_is_known || is_same_target(std::next(pred_node.PC), node.PC)) + stack.emplace_back(edge.first, caller_is_known); + } + else + { + stack.emplace_back(edge.first, caller_is_known); + } + } + } } /// Perform forwards depth-first search of the control-flow graph of the @@ -71,11 +119,66 @@ void reachability_slicert::fixedpoint_from_assertions( const is_threadedt &is_threaded, slicing_criteriont &criterion) { - std::vector src = get_sources(is_threaded, criterion); + std::vector stack; + std::vector sources = get_sources(is_threaded, criterion); + for(const auto source : sources) + stack.emplace_back(source, false); - const std::vector reachable = cfg.get_reachable(src, true); - for(const auto index : reachable) - cfg[index].reachable_from_assertion = true; + while(!stack.empty()) + { + auto &node = cfg[stack.back().node_index]; + const auto caller_is_known = stack.back().caller_is_known; + stack.pop_back(); + + if(node.reachable_from_assertion) + continue; + node.reachable_from_assertion = true; + + if(node.PC->is_function_call()) + { + // Queue the instruction's natural successor (function head, or next + // instruction if the function is bodyless) + INVARIANT(node.out.size() == 1, "Call sites should have one successor"); + const auto successor_index = node.out.begin()->first; + + // If the function has a body, mark the function head, but note that we + // have already taken care of the return site. + const auto &callee_head_node = cfg[successor_index]; + auto callee_it = callee_head_node.PC; + if(!is_same_target(callee_it, std::next(node.PC))) + { + stack.emplace_back(successor_index, true); + + // Check if it can return, and if so mark the callsite's successor: + while(!callee_it->is_end_function()) + ++callee_it; + + if(!cfg[cfg.entry_map[callee_it]].out.empty()) + { + stack.emplace_back( + cfg.entry_map[std::next(node.PC)], caller_is_known); + } + } + else + { + // Bodyless function -- mark the successor instruction only. + stack.emplace_back(successor_index, caller_is_known); + } + } + else if(node.PC->is_end_function() && caller_is_known) + { + // Special case -- the callsite successor was already queued when entering + // this function, more precisely than we can see from the function return + // edges (which lead to all possible callers), so nothing to do here. + } + else + { + // General case, including end-of-function where we don't know our caller. + // Queue all successors. + for(const auto &edge : node.out) + stack.emplace_back(edge.first, caller_is_known); + } + } } /// This function removes all instructions that have the flag diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h index 5f52a6d1795..2bb241e785d 100644 --- a/src/goto-instrument/reachability_slicer_class.h +++ b/src/goto-instrument/reachability_slicer_class.h @@ -51,6 +51,29 @@ class reachability_slicert typedef std::stack queuet; + /// A search stack entry, used in tracking nodes to mark reachable when + /// walking over the CFG in `fixedpoint_to_assertions` and + /// `fixedpoint_from_assertions`. + struct search_stack_entryt + { + /// CFG node to mark reachable + cfgt::node_indext node_index; + + /// If true, this function's caller is known and has already been queued to + /// mark reachable, so there is no need to queue anything when walking out + /// of the function, whether forwards (via END_FUNCTION) or backwards (via a + /// callsite). + /// If false, this function's caller is not known, so when walking forwards + /// from the end or backwards from the beginning we should queue all + /// possible callers. + bool caller_is_known; + + search_stack_entryt(cfgt::node_indext node_index, bool caller_is_known) : + node_index(node_index), caller_is_known(caller_is_known) + { + } + }; + void fixedpoint_to_assertions( const is_threadedt &is_threaded, slicing_criteriont &criterion);