reachability_slicer.cpp

Go to the documentation of this file.

/*******************************************************************\
 
Module: Slicer
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#include "full_slicer_class.h"
#include "reachability_slicer_class.h"
 
#include <util/exception_utils.h>
 
#include <goto-programs/cfg.h>
#include <goto-programs/remove_calls_no_body.h>
#include <goto-programs/remove_skip.h>
#include <goto-programs/remove_unreachable.h>
 
#include <analyses/is_threaded.h>
 
#include "reachability_slicer.h"
 
void reachability_slicert::operator()(
  goto_functionst &goto_functions,
  const slicing_criteriont &criterion,
  bool include_forward_reachability,
  message_handlert &message_handler)
{
  // Replace function calls without body by non-deterministic return values to
  // ensure the CFG does not consider instructions after such a call to be
  // unreachable.
  remove_calls_no_bodyt remove_calls_no_body;
  remove_calls_no_body(goto_functions, message_handler);
  goto_functions.update();
 
  cfg(goto_functions);
  for(const auto &gf_entry : goto_functions.function_map)
  {
    forall_goto_program_instructions(i_it, gf_entry.second.body)
      cfg[cfg.entry_map[i_it]].function_id = gf_entry.first;
  }
 
  is_threadedt is_threaded(goto_functions);
  fixedpoint_to_assertions(is_threaded, criterion);
  if(include_forward_reachability)
    fixedpoint_from_assertions(is_threaded, criterion);
  slice(goto_functions);
}
 
std::vector<reachability_slicert::cfgt::node_indext>
reachability_slicert::get_sources(
  const is_threadedt &is_threaded,
  const slicing_criteriont &criterion)
{
  std::vector<cfgt::node_indext> sources;
  for(const auto &e_it : cfg.entries())
  {
    if(
      criterion(cfg[e_it.second].function_id, e_it.first) ||
      is_threaded(e_it.first))
      sources.push_back(e_it.second);
  }
 
  if(sources.empty())
  {
    throw invalid_command_line_argument_exceptiont{
      "no slicing criterion found",
      "--property",
      "provide at least one property using --property <property>"};
  }
 
  return sources;
}
 
bool reachability_slicert::is_same_target(
  goto_programt::const_targett it1,
  goto_programt::const_targett it2) const
{
  // Avoid comparing iterators belonging to different functions, and therefore
  // different std::lists.
  const auto &node1 = cfg.get_node(it1);
  const auto &node2 = cfg.get_node(it2);
  return node1.function_id == node2.function_id && it1 == it2;
}
 
std::vector<reachability_slicert::cfgt::node_indext>
reachability_slicert::backward_outwards_walk_from(
  std::vector<cfgt::node_indext> stack)
{
  std::vector<cfgt::node_indext> return_sites;
 
  while(!stack.empty())
  {
    auto &node = cfg[stack.back()];
    stack.pop_back();
 
    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.
        // Record the return site for later investigation and step over it:
        return_sites.push_back(edge.first);
 
        INVARIANT(
          std::prev(node.PC)->is_function_call(),
          "all function return edges should point to the successor of a "
          "FUNCTION_CALL instruction");
 
        stack.push_back(cfg.get_node_index(std::prev(node.PC)));
      }
      else
      {
        stack.push_back(edge.first);
      }
    }
  }
 
  return return_sites;
}
 
void reachability_slicert::backward_inwards_walk_from(
  std::vector<cfgt::node_indext> stack)
{
  while(!stack.empty())
  {
    auto &node = cfg[stack.back()];
    stack.pop_back();
 
    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.
        // Walk into the called function, and then walk from the callsite
        // backward:
        stack.push_back(edge.first);
 
        INVARIANT(
          std::prev(node.PC)->is_function_call(),
          "all function return edges should point to the successor of a "
          "FUNCTION_CALL instruction");
 
        stack.push_back(cfg.get_node_index(std::prev(node.PC)));
      }
      else if(pred_node.PC->is_function_call())
      {
        // Skip -- the callsite relevant to this function was already queued
        // when we processed the return site.
      }
      else
      {
        stack.push_back(edge.first);
      }
    }
  }
}
 
void reachability_slicert::fixedpoint_to_assertions(
  const is_threadedt &is_threaded,
  const slicing_criteriont &criterion)
{
  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
 
  // First walk outwards towards __CPROVER_start, visiting all possible callers
  // and stepping over but recording callees as we go:
  std::vector<cfgt::node_indext> return_sites =
    backward_outwards_walk_from(sources);
 
  // Now walk into those callees, restricting our walk to the known callsites:
  backward_inwards_walk_from(return_sites);
}
 
void reachability_slicert::forward_walk_call_instruction(
  const cfgt::nodet &call_node,
  std::vector<cfgt::node_indext> &callsite_successor_stack,
  std::vector<cfgt::node_indext> &callee_head_stack)
{
  // Get the instruction's natural successor (function head, or next
  // instruction if the function is bodyless)
  INVARIANT(call_node.out.size() == 1, "Call sites should have one successor");
  const auto successor_index = call_node.out.begin()->first;
 
  auto callsite_successor_pc = std::next(call_node.PC);
 
  auto successor_pc = cfg[successor_index].PC;
  if(!is_same_target(successor_pc, callsite_successor_pc))
  {
    // Real call -- store the callee head node:
    callee_head_stack.push_back(successor_index);
 
    // Check if it can return, and if so store the callsite's successor:
    while(!successor_pc->is_end_function())
      ++successor_pc;
 
    if(!cfg.get_node(successor_pc).out.empty())
      callsite_successor_stack.push_back(
        cfg.get_node_index(callsite_successor_pc));
  }
  else
  {
    // Bodyless function -- mark the successor instruction only.
    callsite_successor_stack.push_back(successor_index);
  }
}
 
std::vector<reachability_slicert::cfgt::node_indext>
reachability_slicert::forward_outwards_walk_from(
  std::vector<cfgt::node_indext> stack)
{
  std::vector<cfgt::node_indext> called_function_heads;
 
  while(!stack.empty())
  {
    auto &node = cfg[stack.back()];
    stack.pop_back();
 
    if(node.reachable_from_assertion)
      continue;
    node.reachable_from_assertion = true;
 
    if(node.PC->is_function_call())
    {
      // Store the called function head for the later inwards walk;
      // visit the call instruction's local successor now.
      forward_walk_call_instruction(node, stack, called_function_heads);
    }
    else
    {
      // General case, including end of function: queue all successors.
      for(const auto &edge : node.out)
        stack.push_back(edge.first);
    }
  }
 
  return called_function_heads;
}
 
void reachability_slicert::forward_inwards_walk_from(
  std::vector<cfgt::node_indext> stack)
{
  while(!stack.empty())
  {
    auto &node = cfg[stack.back()];
    stack.pop_back();
 
    if(node.reachable_from_assertion)
      continue;
    node.reachable_from_assertion = true;
 
    if(node.PC->is_function_call())
    {
      // Visit both the called function head and the callsite successor:
      forward_walk_call_instruction(node, stack, stack);
    }
    else if(node.PC->is_end_function())
    {
      // 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: queue all successors.
      for(const auto &edge : node.out)
        stack.push_back(edge.first);
    }
  }
}
 
void reachability_slicert::fixedpoint_from_assertions(
  const is_threadedt &is_threaded,
  const slicing_criteriont &criterion)
{
  std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
 
  // First walk outwards towards __CPROVER_start, visiting all possible callers
  // and stepping over but recording callees as we go:
  std::vector<cfgt::node_indext> return_sites =
    forward_outwards_walk_from(sources);
 
  // Now walk into those callees, restricting our walk to the known callsites:
  forward_inwards_walk_from(return_sites);
}
 
void reachability_slicert::slice(goto_functionst &goto_functions)
{
  // now replace those instructions that do not reach any assertions
  // by assume(false)
 
  for(auto &gf_entry : goto_functions.function_map)
  {
    if(gf_entry.second.body_available())
    {
      Forall_goto_program_instructions(i_it, gf_entry.second.body)
      {
        cfgt::nodet &e = cfg.get_node(i_it);
        if(
          !e.reaches_assertion && !e.reachable_from_assertion &&
          !i_it->is_end_function())
        {
          *i_it = goto_programt::make_assumption(
            false_exprt(), i_it->source_location());
        }
      }
 
      // replace unreachable code by skip
      remove_unreachable(gf_entry.second.body);
    }
  }
 
  // remove the skips
  remove_skip(goto_functions);
}
 
void reachability_slicer(
  goto_modelt &goto_model,
  const bool include_forward_reachability,
  message_handlert &message_handler)
{
  reachability_slicert s;
  assert_criteriont a;
  s(goto_model.goto_functions,
    a,
    include_forward_reachability,
    message_handler);
}
 
void reachability_slicer(
  goto_modelt &goto_model,
  const std::list<std::string> &properties,
  const bool include_forward_reachability,
  message_handlert &message_handler)
{
  reachability_slicert s;
  properties_criteriont p(properties);
  s(goto_model.goto_functions,
    p,
    include_forward_reachability,
    message_handler);
}
 
void function_path_reachability_slicer(
  goto_modelt &goto_model,
  const std::list<std::string> &functions_list,
  message_handlert &message_handler)
{
  for(const auto &function : functions_list)
  {
    in_function_criteriont matching_criterion(function);
    reachability_slicert slicer;
    slicer(
      goto_model.goto_functions, matching_criterion, true, message_handler);
  }
 
  remove_calls_no_bodyt remove_calls_no_body;
  remove_calls_no_body(goto_model.goto_functions, message_handler);
 
  goto_model.goto_functions.update();
  goto_model.goto_functions.compute_loop_numbers();
}
 
void reachability_slicer(
  goto_modelt &goto_model,
  message_handlert &message_handler)
{
  reachability_slicer(goto_model, false, message_handler);
}
 
void reachability_slicer(
  goto_modelt &goto_model,
  const std::list<std::string> &properties,
  message_handlert &message_handler)
{
  reachability_slicer(goto_model, properties, false, message_handler);
}