From eea9fa056ec704872b148701db106211372e071e Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Wed, 11 Oct 2017 10:16:50 +0200
Subject: [PATCH 01/14] grapht::output_dot needs digraph declaration

Without the "digraph call_graph{" this is not parsable dot. This change makes the output dot consistent with the previous output_dot function in call_grapht
---
 src/util/graph.h | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/util/graph.h b/src/util/graph.h
index b0b5713b5ee..9fe82642f1c 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -655,8 +655,12 @@ std::list<typename grapht<N>::node_indext> grapht<N>::topsort() const
 template<class N>
 void grapht<N>::output_dot(std::ostream &out) const
 {
+  out << "digraph call_graph {\n";
+
   for(node_indext n=0; n<nodes.size(); n++)
     output_dot_node(out, n);
+
+  out << "}\n";
 }
 
 template<class N>
@@ -668,7 +672,12 @@ void grapht<N>::output_dot_node(std::ostream &out, node_indext n) const
       it=node.out.begin();
       it!=node.out.end();
       it++)
-    out << n << " -> " << it->first << '\n';
+  {
+    out << "  \"" << n << "\" -> "
+        << "\"" << it->first << "\" "
+        << " [arrowhead=\"vee\"];"
+        << "\n";
+  }
 }
 
 #endif // CPROVER_UTIL_GRAPH_H

From 46a6804c09b6ad67eac3b58b8f9323ce90f7601c Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Tue, 17 Oct 2017 13:38:34 +0200
Subject: [PATCH 02/14] Introduce reachable call graph class, and rewrite call
 graph to inherit from grapht<T>

I have rewritten call_grapht to inherit from grapht, because I think there should be fewer graph classes in CBMC.

Instead of constructing the entire call graph, the reachable call graph class constructs only the reachable call graph.

There is some duplication between the call_graph class and the show_call_sequences function, however the show_call_sequences function outputs the graph on the fly, instead of constructing it, which doesn't allow for further use of the graph
---
 src/analyses/Makefile                         |   1 +
 src/analyses/call_graph.cpp                   | 104 +++++++++++------
 src/analyses/call_graph.h                     |  61 ++++++++--
 src/analyses/reachable_call_graph.cpp         | 105 ++++++++++++++++++
 src/analyses/reachable_call_graph.h           |  36 ++++++
 .../goto_instrument_parse_options.cpp         |  20 +++-
 .../goto_instrument_parse_options.h           |   1 +
 src/goto-programs/slice_global_inits.cpp      |  27 +----
 src/util/graph.h                              |   2 +-
 unit/analyses/call_graph.cpp                  |  36 +++---
 10 files changed, 304 insertions(+), 89 deletions(-)
 create mode 100644 src/analyses/reachable_call_graph.cpp
 create mode 100644 src/analyses/reachable_call_graph.h

diff --git a/src/analyses/Makefile b/src/analyses/Makefile
index a63a4d4e1c6..8094a345251 100644
--- a/src/analyses/Makefile
+++ b/src/analyses/Makefile
@@ -22,6 +22,7 @@ SRC = ai.cpp \
       locals.cpp \
       natural_loops.cpp \
       reaching_definitions.cpp \
+      reachable_call_graph.cpp \
       static_analysis.cpp \
       uncaught_exceptions_analysis.cpp \
       uninitialized_domain.cpp \
diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp
index 93850f64d1d..683ed7905dc 100644
--- a/src/analyses/call_graph.cpp
+++ b/src/analyses/call_graph.cpp
@@ -7,7 +7,7 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 /// \file
-/// Function Call Graphs
+/// Function Call Graph
 
 #include "call_graph.h"
 
@@ -18,14 +18,9 @@ call_grapht::call_grapht()
 {
 }
 
-call_grapht::call_grapht(const goto_modelt &goto_model):
-  call_grapht(goto_model.goto_functions)
+call_grapht::call_grapht(const goto_modelt &goto_model)
 {
-}
-
-call_grapht::call_grapht(const goto_functionst &goto_functions)
-{
-  forall_goto_functions(f_it, goto_functions)
+  forall_goto_functions(f_it, goto_model.goto_functions)
   {
     const goto_programt &body=f_it->second.body;
     add(f_it->first, body);
@@ -51,50 +46,91 @@ void call_grapht::add(
   const irep_idt &caller,
   const irep_idt &callee)
 {
-  graph.insert(std::pair<irep_idt, irep_idt>(caller, callee));
+  std::size_t caller_idx = node_numbering.number(caller);
+  if(caller_idx >= nodes.size())
+  {
+    node_indext node_index = add_node();
+    nodes[node_index].function_name = caller;
+  }
+
+  std::size_t callee_idx = node_numbering.number(callee);
+  if(callee_idx >= nodes.size())
+  {
+    node_indext node_index = add_node();
+    nodes[node_index].function_name = callee;
+  }
+
+  add_edge(caller_idx, callee_idx);
 }
 
-/// Returns an inverted copy of this call graph
-/// \return Inverted (callee -> caller) call graph
-call_grapht call_grapht::get_inverted() const
+
+void call_grapht::output_dot_node(std::ostream &out, node_indext n) const
 {
-  call_grapht result;
-  for(const auto &caller_callee : graph)
-    result.add(caller_callee.second, caller_callee.first);
-  return result;
+  const nodet &node = nodes.at(n);
+
+  for(const auto &edge : node.out)
+  {
+    out << "  \"" << node.function_name << "\" -> " << "\""
+        << nodes[edge.first].function_name << "\" " << " [arrowhead=\"vee\"];"
+        << "\n";
+  }
 }
 
-void call_grapht::output_dot(std::ostream &out) const
+void call_grapht::output_xml_node(std::ostream &out, node_indext n) const
 {
-  out << "digraph call_graph {\n";
+  const nodet &node = nodes.at(n);
 
-  for(const auto &edge : graph)
+  for(const auto &edge : node.out)
   {
-    out << "  \"" << edge.first << "\" -> "
-        << "\"" << edge.second << "\" "
-        << " [arrowhead=\"vee\"];"
-        << "\n";
+    out << "<call_graph_edge caller=\"";
+    xmlt::escape_attribute(id2string(node.function_name), out);
+    out << "\" callee=\"";
+    xmlt::escape_attribute(id2string(nodes[edge.first].function_name), out);
+    out << "\">\n";
   }
+}
 
-  out << "}\n";
+void call_grapht::output_xml(std::ostream &out) const
+{
+  for(node_indext n = 0; n < nodes.size(); n++)
+    output_xml_node(out, n);
 }
 
-void call_grapht::output(std::ostream &out) const
+call_grapht call_grapht::get_inverted() const
 {
-  for(const auto &edge : graph)
+  call_grapht result;
+  for(const auto &n : nodes)
   {
-    out << edge.first << " -> " << edge.second << "\n";
+    for(const auto &i : n.in)
+      result.add(n.function_name, nodes[i.first].function_name);
   }
+  return result;
 }
 
-void call_grapht::output_xml(std::ostream &out) const
+std::unordered_set<irep_idt, irep_id_hash>
+call_grapht::reachable_functions(irep_idt start_function)
 {
-  for(const auto &edge : graph)
+  std::unordered_set<irep_idt, irep_id_hash> result;
+  std::list<node_indext> worklist;
+  node_indext start_index;
+
+  if(get_node_index(start_function, start_index))
+    worklist.push_back(start_index);
+  else
+    throw "no start function found in call graph";
+
+  while(!worklist.empty())
   {
-    out << "<call_graph_edge caller=\"";
-    xmlt::escape_attribute(id2string(edge.first), out);
-    out << "\" callee=\"";
-    xmlt::escape_attribute(id2string(edge.second), out);
-    out << "\">\n";
+    const node_indext id = worklist.front();
+    worklist.pop_front();
+
+    result.insert(nodes[id].function_name);
+    for(const auto &o : nodes[id].out)
+    {
+      if(result.find(nodes[o.first].function_name) == result.end())
+        worklist.push_back(o.first);
+    }
   }
+
+  return result;
 }
diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h
index 684f74c3a3a..b8a4d61d58b 100644
--- a/src/analyses/call_graph.h
+++ b/src/analyses/call_graph.h
@@ -7,34 +7,77 @@ Author: Daniel Kroening, kroening@kroening.com
 \*******************************************************************/
 
 /// \file
-/// Function Call Graphs
+/// Function Call Graph
 
 #ifndef CPROVER_ANALYSES_CALL_GRAPH_H
 #define CPROVER_ANALYSES_CALL_GRAPH_H
 
 #include <iosfwd>
 #include <map>
+#include <unordered_set>
 
 #include <goto-programs/goto_model.h>
 
-class call_grapht
+#include <util/irep.h>
+#include <util/graph.h>
+#include <util/numbering.h>
+
+
+/// Function call graph inherits from grapht to allow forward and
+/// backward traversal of the function call graph
+
+struct call_graph_nodet: public graph_nodet<empty_edget>
+{
+  typedef graph_nodet<empty_edget>::edget edget;
+  typedef graph_nodet<empty_edget>::edgest edgest;
+
+  irep_idt function_name;
+  bool visited = false;
+};
+
+class call_grapht: public grapht<call_graph_nodet>
 {
 public:
   call_grapht();
   explicit call_grapht(const goto_modelt &);
-  explicit call_grapht(const goto_functionst &);
 
-  void output_dot(std::ostream &out) const;
-  void output(std::ostream &out) const;
+  void add(const irep_idt &caller, const irep_idt &callee);
   void output_xml(std::ostream &out) const;
+  call_grapht get_inverted() const;
+  std::unordered_set<irep_idt, irep_id_hash>
+      reachable_functions(irep_idt start);
 
-  typedef std::multimap<irep_idt, irep_idt> grapht;
-  grapht graph;
+  bool get_node_index(const irep_idt& function_name, node_indext &n) const
+  {
+    for(node_indext idx = 0; idx < nodes.size(); idx++)
+    {
+      if(nodes[idx].function_name == function_name)
+      {
+        n = idx;
+        return true;
+      }
+    }
+    return false;
+  }
+
+  std::unordered_set<irep_idt, irep_id_hash> get_successors(
+      const irep_idt& function_name) const
+  {
+    std::unordered_set<irep_idt, irep_id_hash> result;
+    node_indext function_idx;
+    if(!get_node_index(function_name, function_idx))
+      return result;
+
+    for(const auto &o : nodes[function_idx].out)
+      result.insert(nodes[o.first].function_name);
+    return result;
+  }
 
-  void add(const irep_idt &caller, const irep_idt &callee);
-  call_grapht get_inverted() const;
 
 protected:
+  void output_dot_node(std::ostream &out, node_indext n) const override;
+  void output_xml_node(std::ostream &out, node_indext n) const;
+  numbering<irep_idt> node_numbering;
   void add(const irep_idt &function,
            const goto_programt &body);
 };
diff --git a/src/analyses/reachable_call_graph.cpp b/src/analyses/reachable_call_graph.cpp
new file mode 100644
index 00000000000..50674fde86c
--- /dev/null
+++ b/src/analyses/reachable_call_graph.cpp
@@ -0,0 +1,105 @@
+/*******************************************************************\
+
+Module: Reachable Call Graphs
+
+Author:
+
+\*******************************************************************/
+
+/// \file
+/// Reachable Call Graph
+/// Constructs a call graph only from the functions reachable from a given
+/// entry point, or the goto_functions.entry_point if none is given.
+
+#include "reachable_call_graph.h"
+#include <util/message.h>
+
+
+reachable_call_grapht::reachable_call_grapht
+(const goto_modelt & _goto_model)
+{
+  build(_goto_model.goto_functions);
+}
+
+void reachable_call_grapht::build(const goto_functionst & goto_functions)
+{
+  irep_idt start_function_name = goto_functions.entry_point();
+  build(goto_functions, start_function_name);
+}
+
+
+void reachable_call_grapht::build(
+    const goto_functionst & goto_functions,
+    irep_idt start_function_name)
+{
+  std::set<irep_idt> working_queue;
+  std::set<irep_idt> done;
+
+  // start from entry point
+  working_queue.insert(start_function_name);
+
+  while(!working_queue.empty())
+  {
+    irep_idt caller=*working_queue.begin();
+    working_queue.erase(working_queue.begin());
+
+    if(!done.insert(caller).second)
+      continue;
+
+    const goto_functionst::function_mapt::const_iterator f_it=
+      goto_functions.function_map.find(caller);
+
+    if(f_it==goto_functions.function_map.end())
+      continue;
+
+    const goto_programt &program=
+      f_it->second.body;
+
+    forall_goto_program_instructions(i_it, program)
+    {
+      if(i_it->is_function_call())
+      {
+        const exprt &function_expr=to_code_function_call(i_it->code).function();
+        if(function_expr.id()==ID_symbol)
+        {
+          irep_idt callee = to_symbol_expr(function_expr).get_identifier();
+          add(caller, callee);
+          working_queue.insert(callee);
+        }
+      }
+    }
+  }
+}
+
+
+std::unordered_set<irep_idt, irep_id_hash>
+reachable_call_grapht::backward_slice(irep_idt destination_function)
+{
+  std::unordered_set<irep_idt, irep_id_hash> result;
+  std::list<node_indext> worklist;
+  for(node_indext idx=0; idx<nodes.size(); idx++)
+  {
+    if(nodes[idx].function_name==destination_function)
+    {
+      worklist.push_back(idx);
+      break;
+    }
+  }
+  INVARIANT(!worklist.empty(), "destination function not found");
+
+  while(!worklist.empty())
+  {
+    const node_indext id = worklist.front();
+    worklist.pop_front();
+
+    result.insert(nodes[id].function_name);
+    for(const auto o : nodes[id].in)
+    {
+      if(result.find(nodes[o.first].function_name)==result.end())
+          worklist.push_back(o.first);
+    }
+  }
+
+return result;
+}
+
diff --git a/src/analyses/reachable_call_graph.h b/src/analyses/reachable_call_graph.h
new file mode 100644
index 00000000000..2de7b84eb0d
--- /dev/null
+++ b/src/analyses/reachable_call_graph.h
@@ -0,0 +1,36 @@
+/*******************************************************************\
+
+Module: Reachable Call Graphs
+
+Author:
+
+\*******************************************************************/
+
+/// \file
+/// Reachable Call Graphs
+
+#ifndef CPROVER_ANALYSES_REACHABLE_CALL_GRAPH_H
+#define CPROVER_ANALYSES_REACHABLE_CALL_GRAPH_H
+
+#include "call_graph.h"
+
+class reachable_call_grapht: public call_grapht
+{
+public:
+  explicit reachable_call_grapht(const goto_modelt &);
+
+  /// \brief Generates list of functions reachable from initial state and
+  /// that may reach a given destination function
+  ///
+  /// This is done by inverting the reachable call graph and performing bfs on
+  /// the inverted call graph.
+  /// \param destination function
+  /// \return unorderded set of function names as irep_idts
+  std::unordered_set<irep_idt, irep_id_hash>
+  backward_slice(irep_idt destination_function);
+protected:
+  void build(const goto_functionst &);
+  void build(const goto_functionst &, irep_idt start_function);
+};
+
+#endif /* SRC_ANALYSES_REACHABLE_CALL_GRAPH_H_ */
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 2218fd68235..d868369c516 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -61,6 +61,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <analyses/dependence_graph.h>
 #include <analyses/constant_propagator.h>
 #include <analyses/is_threaded.h>
+#include <analyses/reachable_call_graph.h>
+
 
 #include <cbmc/version.h>
 
@@ -648,17 +650,25 @@ int goto_instrument_parse_optionst::doit()
     {
       do_indirect_call_and_rtti_removal();
       call_grapht call_graph(goto_model);
-
       if(cmdline.isset("xml"))
         call_graph.output_xml(std::cout);
-      else if(cmdline.isset("dot"))
-        call_graph.output_dot(std::cout);
       else
-        call_graph.output(std::cout);
+        call_graph.output_dot(std::cout);
 
       return CPROVER_EXIT_SUCCESS;
     }
 
+    if(cmdline.isset("reachable-call-graph"))
+    {
+      do_indirect_call_and_rtti_removal();
+      reachable_call_grapht reach_graph(goto_model);
+      if(cmdline.isset("xml"))
+        reach_graph.output_xml(std::cout);
+      else
+        reach_graph.output_dot(std::cout);
+    return 0;
+    }
+
     if(cmdline.isset("dot"))
     {
       namespacet ns(goto_model.symbol_table);
@@ -1454,6 +1464,8 @@ void goto_instrument_parse_optionst::help()
     " --list-calls-args            list all function calls with their arguments\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --print-path-lengths         print statistics about control-flow graph paths\n"
+    " --call-graph                 show graph of function calls\n"
+    " --reachable-call-graph       show graph of function calls potentially reachable from main function\n" // NOLINT(*)
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 04b3a8f7b2b..d6f85090923 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -44,6 +44,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(max-var):(max-po-trans):(ignore-arrays)" \
   "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
   "(call-graph)" \
+  "(reachable-call-graph)" \
   "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
   "(nondet-volatile)(isr):" \
   "(stack-depth):(nondet-static)" \
diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp
index cc4f7349eb7..a08b3331449 100644
--- a/src/goto-programs/slice_global_inits.cpp
+++ b/src/goto-programs/slice_global_inits.cpp
@@ -30,11 +30,8 @@ void slice_global_inits(goto_modelt &goto_model)
   // gather all functions reachable from the entry point
 
   call_grapht call_graph(goto_model);
-  const call_grapht::grapht &graph=call_graph.graph;
-  goto_functionst &goto_functions=goto_model.goto_functions;
 
-  std::list<irep_idt> worklist;
-  std::unordered_set<irep_idt, irep_id_hash> functions_reached;
+  goto_functionst &goto_functions=goto_model.goto_functions;
 
   const irep_idt entry_point=goto_functionst::entry_point();
 
@@ -44,26 +41,8 @@ void slice_global_inits(goto_modelt &goto_model)
   if(e_it==goto_functions.function_map.end())
     throw "entry point not found";
 
-  worklist.push_back(entry_point);
-
-  do
-  {
-    const irep_idt id=worklist.front();
-    worklist.pop_front();
-
-    functions_reached.insert(id);
-
-    const auto &p=graph.equal_range(id);
-
-    for(auto it=p.first; it!=p.second; it++)
-    {
-      const irep_idt callee=it->second;
-
-      if(functions_reached.find(callee)==functions_reached.end())
-        worklist.push_back(callee);
-    }
-  }
-  while(!worklist.empty());
+  std::unordered_set<irep_idt, irep_id_hash> functions_reached=
+      call_graph.reachable_functions(entry_point);
 
   const irep_idt initialize=CPROVER_PREFIX "initialize";
   functions_reached.erase(initialize);
diff --git a/src/util/graph.h b/src/util/graph.h
index 9fe82642f1c..e4cd7097978 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -263,7 +263,7 @@ class grapht
   std::list<node_indext> topsort() const;
 
   void output_dot(std::ostream &out) const;
-  void output_dot_node(std::ostream &out, node_indext n) const;
+  virtual void output_dot_node(std::ostream &out, node_indext n) const;
 
 protected:
   class tarjant
diff --git a/unit/analyses/call_graph.cpp b/unit/analyses/call_graph.cpp
index 985c804c91c..77c328cecac 100644
--- a/unit/analyses/call_graph.cpp
+++ b/unit/analyses/call_graph.cpp
@@ -30,15 +30,13 @@ static symbolt create_void_function_symbol(
   return function;
 }
 
-static bool multimap_key_matches(
-  const std::multimap<irep_idt, irep_idt> &map,
+static bool graph_key_matches(
+  const call_grapht graph,
   const irep_idt &key,
-  const std::set<irep_idt> &values)
+  const std::unordered_set<irep_idt, irep_id_hash> &values)
 {
-  auto matching_values=map.equal_range(key);
-  std::set<irep_idt> matching_set;
-  for(auto it=matching_values.first; it!=matching_values.second; ++it)
-    matching_set.insert(it->second);
+  std::unordered_set<irep_idt, irep_id_hash> matching_set =
+      graph.get_successors(key);
   return matching_set==values;
 }
 
@@ -106,10 +104,11 @@ SCENARIO("call_graph",
     {
       THEN("We expect A -> { A, B }, B -> { C, D }")
       {
-        const auto &check_graph=call_graph_from_goto_functions.graph;
-        REQUIRE(check_graph.size()==4);
-        REQUIRE(multimap_key_matches(check_graph, "A", {"A", "B"}));
-        REQUIRE(multimap_key_matches(check_graph, "B", {"C", "D"}));
+        REQUIRE(call_graph_from_goto_functions.size()==4);
+        REQUIRE(graph_key_matches
+            (call_graph_from_goto_functions, "A", {"A", "B"}));
+        REQUIRE(graph_key_matches
+            (call_graph_from_goto_functions, "B", {"C", "D"}));
       }
     }
 
@@ -119,12 +118,15 @@ SCENARIO("call_graph",
         call_graph_from_goto_functions.get_inverted();
       THEN("We expect A -> { A }, B -> { A }, C -> { B }, D -> { B }")
       {
-        const auto &check_graph=inverse_call_graph_from_goto_functions.graph;
-        REQUIRE(check_graph.size()==4);
-        REQUIRE(multimap_key_matches(check_graph, "A", {"A"}));
-        REQUIRE(multimap_key_matches(check_graph, "B", {"A"}));
-        REQUIRE(multimap_key_matches(check_graph, "C", {"B"}));
-        REQUIRE(multimap_key_matches(check_graph, "D", {"B"}));
+        REQUIRE(inverse_call_graph_from_goto_functions.size()==4);
+        REQUIRE(graph_key_matches
+            (inverse_call_graph_from_goto_functions, "A", {"A"}));
+        REQUIRE(graph_key_matches
+            (inverse_call_graph_from_goto_functions, "B", {"A"}));
+        REQUIRE(graph_key_matches
+            (inverse_call_graph_from_goto_functions, "C", {"B"}));
+        REQUIRE(graph_key_matches
+            (inverse_call_graph_from_goto_functions, "D", {"B"}));
       }
     }
 

From 5682636a1646ebca117dae8939fe6b8ee38a2482 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Tue, 17 Oct 2017 09:48:32 +0200
Subject: [PATCH 03/14] CR fixes for grapht

Michael's comments on CR-766007 highlighted things that should be changed in grapht.
---
 src/util/graph.h | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/util/graph.h b/src/util/graph.h
index e4cd7097978..f7eec376a9f 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -666,15 +666,12 @@ void grapht<N>::output_dot(std::ostream &out) const
 template<class N>
 void grapht<N>::output_dot_node(std::ostream &out, node_indext n) const
 {
-  const nodet &node=nodes[n];
+  const nodet &node=nodes.at(n);
 
-  for(typename edgest::const_iterator
-      it=node.out.begin();
-      it!=node.out.end();
-      it++)
+  for(const auto &edge : node.out)
   {
     out << "  \"" << n << "\" -> "
-        << "\"" << it->first << "\" "
+        << "\"" << edge.first << "\" "
         << " [arrowhead=\"vee\"];"
         << "\n";
   }

From ab074ea2fcf8b793a6f48e36b885b15a332efc12 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Wed, 11 Oct 2017 13:23:49 +0200
Subject: [PATCH 04/14] return shortest path from function call graph

Returns the list of functions on the shortest path from a src function to a destination function on the function call graph.
---
 src/analyses/call_graph.cpp | 20 ++++++++++++++++++++
 src/analyses/call_graph.h   |  1 +
 2 files changed, 21 insertions(+)

diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp
index 683ed7905dc..5d581bdeb57 100644
--- a/src/analyses/call_graph.cpp
+++ b/src/analyses/call_graph.cpp
@@ -107,6 +107,26 @@ call_grapht call_grapht::get_inverted() const
   return result;
 }
 
+std::list<irep_idt>call_grapht::shortest_function_path
+(irep_idt src, irep_idt dest)
+{
+  std::list<irep_idt> result;
+  node_indext src_idx, dest_idx;
+  if(!get_node_index(src, src_idx))
+    throw "unable to find src function in call graph";
+  if(!get_node_index(dest, dest_idx))
+    throw "unable to find destination function in call graph";
+
+  patht path;
+  shortest_path(src_idx, dest_idx, path);
+  for(const auto &n : path)
+  {
+    result.push_back(nodes[n].function_name);
+  }
+  return result;
+}
+
+
 std::unordered_set<irep_idt, irep_id_hash>
 call_grapht::reachable_functions(irep_idt start_function)
 {
diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h
index b8a4d61d58b..d31091a7c8b 100644
--- a/src/analyses/call_graph.h
+++ b/src/analyses/call_graph.h
@@ -46,6 +46,7 @@ class call_grapht: public grapht<call_graph_nodet>
   call_grapht get_inverted() const;
   std::unordered_set<irep_idt, irep_id_hash>
       reachable_functions(irep_idt start);
+  std::list<irep_idt>shortest_function_path(irep_idt src, irep_idt dest);
 
   bool get_node_index(const irep_idt& function_name, node_indext &n) const
   {

From d3515063ad333444e103cc6155ebfec6e544024e Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Mon, 23 Oct 2017 19:54:30 +0200
Subject: [PATCH 05/14] Documentation of call graph and reachable call graph

---
 src/analyses/call_graph.h             | 26 ++++++++++++++++++++++++--
 src/analyses/reachable_call_graph.cpp |  5 -----
 src/analyses/reachable_call_graph.h   | 14 +++++++-------
 3 files changed, 31 insertions(+), 14 deletions(-)

diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h
index d31091a7c8b..28fcd147173 100644
--- a/src/analyses/call_graph.h
+++ b/src/analyses/call_graph.h
@@ -23,9 +23,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/numbering.h>
 
 
-/// Function call graph inherits from grapht to allow forward and
+/// \brief Function call graph: each node represents a function
+/// in the GOTO model, a directed edge from A to B indicates
+/// that function A calls function B.
+/// Inherits from grapht to allow forward and
 /// backward traversal of the function call graph
-
 struct call_graph_nodet: public graph_nodet<empty_edget>
 {
   typedef graph_nodet<empty_edget>::edget edget;
@@ -43,11 +45,28 @@ class call_grapht: public grapht<call_graph_nodet>
 
   void add(const irep_idt &caller, const irep_idt &callee);
   void output_xml(std::ostream &out) const;
+
+  /// \return the inverted call graph
   call_grapht get_inverted() const;
+
+  /// \brief get the names of all functions reachable from a start function
+  /// \param start  name of initial function
+  /// \return set of all names of the reachable functions
   std::unordered_set<irep_idt, irep_id_hash>
       reachable_functions(irep_idt start);
+
+  /// \brief Function returns the shortest path on the function call graph
+  /// between a source and a destination function
+  /// \param src  name of the starting function
+  /// \param dest name of the destination function
+  /// \return list of function names on the shortest path between src and dest
   std::list<irep_idt>shortest_function_path(irep_idt src, irep_idt dest);
 
+  /// get the index of the node that corresponds to a function name
+  /// \param[in] function_name function_name passed by reference
+  /// \param[out] n variable for the node index to be written to
+  /// \return true if a node with the given function name exists,
+  /// false if it does not exist
   bool get_node_index(const irep_idt& function_name, node_indext &n) const
   {
     for(node_indext idx = 0; idx < nodes.size(); idx++)
@@ -61,6 +80,9 @@ class call_grapht: public grapht<call_graph_nodet>
     return false;
   }
 
+  /// \brief get a list of functions called by a function
+  /// \param function_name   the irep_idt of the function
+  /// \return an unordered set of all functions called by function_name
   std::unordered_set<irep_idt, irep_id_hash> get_successors(
       const irep_idt& function_name) const
   {
diff --git a/src/analyses/reachable_call_graph.cpp b/src/analyses/reachable_call_graph.cpp
index 50674fde86c..2ed17371dd9 100644
--- a/src/analyses/reachable_call_graph.cpp
+++ b/src/analyses/reachable_call_graph.cpp
@@ -8,13 +8,9 @@ Module: Reachable Call Graphs
 
 /// \file
 /// Reachable Call Graph
-/// Constructs a call graph only from the functions reachable from a given
-/// entry point, or the goto_functions.entry_point if none is given.
-
 #include "reachable_call_graph.h"
 #include <util/message.h>
 
-
 reachable_call_grapht::reachable_call_grapht
 (const goto_modelt & _goto_model)
 {
@@ -71,7 +67,6 @@ void reachable_call_grapht::build(
   }
 }
 
-
 std::unordered_set<irep_idt, irep_id_hash>
 reachable_call_grapht::backward_slice(irep_idt destination_function)
 {
diff --git a/src/analyses/reachable_call_graph.h b/src/analyses/reachable_call_graph.h
index 2de7b84eb0d..4dcfd5cfd0c 100644
--- a/src/analyses/reachable_call_graph.h
+++ b/src/analyses/reachable_call_graph.h
@@ -8,6 +8,8 @@ Module: Reachable Call Graphs
 
 /// \file
 /// Reachable Call Graphs
+/// Constructs a call graph only from the functions reachable from a given
+/// entry point, or the goto_functions.entry_point if none is given.
 
 #ifndef CPROVER_ANALYSES_REACHABLE_CALL_GRAPH_H
 #define CPROVER_ANALYSES_REACHABLE_CALL_GRAPH_H
@@ -19,13 +21,11 @@ class reachable_call_grapht: public call_grapht
 public:
   explicit reachable_call_grapht(const goto_modelt &);
 
-  /// \brief Generates list of functions reachable from initial state and
-  /// that may reach a given destination function
-  ///
-  /// This is done by inverting the reachable call graph and performing bfs on
-  /// the inverted call graph.
-  /// \param destination function
-  /// \return unorderded set of function names as irep_idts
+  /// \brief performs a backwards slice on a reachable call graph
+  /// and returns an unordered set of all functions between the initial
+  /// function and the destination function, i.e., a cone of influence
+  /// \param destination_function   name of destination function
+  /// \return unordered set of function names
   std::unordered_set<irep_idt, irep_id_hash>
   backward_slice(irep_idt destination_function);
 protected:

From 13ad1b0677ff3a45853ca911c616ed30cae0aecf Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Tue, 24 Oct 2017 13:22:44 +0200
Subject: [PATCH 06/14] white space call graph

---
 src/analyses/call_graph.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp
index 5d581bdeb57..dec7f9205c8 100644
--- a/src/analyses/call_graph.cpp
+++ b/src/analyses/call_graph.cpp
@@ -107,8 +107,8 @@ call_grapht call_grapht::get_inverted() const
   return result;
 }
 
-std::list<irep_idt>call_grapht::shortest_function_path
-(irep_idt src, irep_idt dest)
+std::list<irep_idt> call_grapht::shortest_function_path(
+    irep_idt src, irep_idt dest)
 {
   std::list<irep_idt> result;
   node_indext src_idx, dest_idx;

From 8fb979341226500ea5aadb575fd2abb77b6e2462 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Tue, 17 Oct 2017 11:19:05 +0200
Subject: [PATCH 07/14] Aggressive slicer: automatically stub functions not on
 shortest path

Automatically removes the function bodies of any function not on the shortest path in the function call graph or reachable within N function calls of the shortest path
---
 .../goto_instrument_parse_options.cpp         | 33 ++++++++
 .../goto_instrument_parse_options.h           |  6 +-
 src/goto-instrument/remove_function.cpp       | 78 +++++++++++++++++++
 src/goto-instrument/remove_function.h         | 61 +++++++++++++++
 4 files changed, 177 insertions(+), 1 deletion(-)

diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index d868369c516..82929997a5d 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1420,6 +1420,32 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       throw 0;
   }
 
+  // aggressive slicer
+  if(cmdline.isset("aggressive-slice"))
+  {
+    do_indirect_call_and_rtti_removal();
+
+    status() << "Performing an aggressive slice" << eom;
+    aggressive_slicert aggressive_slicer(goto_model, get_message_handler());
+
+    if(cmdline.isset("call-depth"))
+      aggressive_slicer.call_depth = safe_string2unsigned(
+          cmdline.get_value("call-depth"));
+
+    if(cmdline.isset("preserve-function"))
+      aggressive_slicer.preserve_functions(
+          cmdline.get_values("preserve-function"));
+
+    if(cmdline.isset("property"))
+      aggressive_slicer.properties = cmdline.get_values("property");
+
+    if(cmdline.isset("preserve-functions-containing"))
+      aggressive_slicer.name_snippets = cmdline.get_values(
+          "preserve-functions-containing");
+
+    aggressive_slicer.doit();
+  }
+
   // recalculate numbers, etc.
   goto_model.goto_functions.update();
 }
@@ -1519,6 +1545,13 @@ void goto_instrument_parse_optionst::help()
     " --full-slice                 slice away instructions that don't affect assertions\n" // NOLINT(*)
     " --property id                slice with respect to specific property only\n" // NOLINT(*)
     " --slice-global-inits         slice away initializations of unused global variables\n" // NOLINT(*)
+    " --aggressive-slice           remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
+    "                              the start function and the function containing the property(s)\n" // NOLINT(*)
+    " --call-depth <n>             used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
+    "                              of the functions on the shortest path\n"
+    " --preserve-function <f>      force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
+    " --preserve-function containing <f>\n"
+    "                              force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
     "\n"
     "Further transformations:\n"
     " --constant-propagator        propagate constants and simplify expressions\n" // NOLINT(*)
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index d6f85090923..4bdc05c3039 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -80,7 +80,11 @@ Author: Daniel Kroening, kroening@kroening.com
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
   "(splice-call):" \
-
+  "(aggressive-slice)" \
+  "(call-depth):" \
+  "(harness-generator):" \
+  "(preserve-function):" \
+  "(preserve-functions-containing):" \
 
 class goto_instrument_parse_optionst:
   public parse_options_baset,
diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp
index 6376b4a5512..3f3a7415964 100644
--- a/src/goto-instrument/remove_function.cpp
+++ b/src/goto-instrument/remove_function.cpp
@@ -12,10 +12,88 @@ Date: April 2017
 /// Remove function definition
 
 #include "remove_function.h"
+#include "function_modifies.h"
 
 #include <util/message.h>
 
 #include <goto-programs/goto_model.h>
+#include <goto-programs/show_properties.h>
+
+#include <string>
+
+
+void aggressive_slicert::get_property_list()
+{
+  for(const auto &fct : goto_model.goto_functions.function_map)
+  {
+    if(!fct.second.is_inlined())
+    {
+      for(const auto &ins : fct.second.body.instructions)
+        if(ins.is_assert())
+        {
+          for(const auto &func : call_graph.shortest_function_path(
+              start_function, ins.function))
+          {
+            functions_to_keep.insert(func);
+          }
+        }
+    }
+  }
+}
+
+
+void aggressive_slicert::find_functions_that_contain_name_snippet()
+{
+  for(const auto &name_snippet : name_snippets)
+  {
+    forall_goto_functions(f_it, goto_model.goto_functions)
+    {
+      if(id2string(f_it->first).find(name_snippet)!=std::string::npos)
+        functions_to_keep.insert(f_it->first);
+    }
+  }
+}
+
+
+void aggressive_slicert::doit()
+{
+  messaget message(message_handler);
+
+  functions_to_keep.insert(CPROVER_PREFIX "initialize");
+  functions_to_keep.insert(start_function);
+
+  // if no properties are specified, get list of all properties
+  if(properties.empty())
+    get_property_list();
+
+  // if a name snippet is given, get list of all functions containing
+  // name snippet
+  if(!name_snippets.empty())
+    find_functions_that_contain_name_snippet();
+
+  for(const auto &p : properties)
+  {
+    source_locationt property_loc = find_property(p, goto_model.goto_functions);
+    irep_idt dest = property_loc.get_function();
+    for(const auto &func : call_graph.shortest_function_path(
+        start_function, dest))
+      functions_to_keep.insert(func);
+  }
+
+  // Add functions within distance of shortest path functions
+  // to the list
+  if(call_depth != 0)
+    call_graph.reachable_within_n_steps(call_depth, functions_to_keep);
+
+  for(const auto &func : functions_to_keep)
+    message.status() << "Keeping: " << func << messaget::eom;
+
+  forall_goto_functions(f_it, goto_model.goto_functions)
+  {
+    if(functions_to_keep.find(f_it->first)==functions_to_keep.end())
+      remove_function(goto_model, f_it->first, message_handler);
+  }
+}
 
 /// Remove the body of function "identifier" such that an analysis will treat it
 /// as a side-effect free function with non-deterministic return value.
diff --git a/src/goto-instrument/remove_function.h b/src/goto-instrument/remove_function.h
index 3c88b8ce803..47cd2fcf299 100644
--- a/src/goto-instrument/remove_function.h
+++ b/src/goto-instrument/remove_function.h
@@ -16,9 +16,12 @@ Date: April 2017
 
 #include <list>
 #include <string>
+#include <unordered_set>
 
 #include <util/irep.h>
 
+#include <analyses/call_graph.h>
+
 class goto_modelt;
 class message_handlert;
 
@@ -32,4 +35,62 @@ void remove_functions(
   const std::list<std::string> &names,
   message_handlert &);
 
+/// \brief The aggressive slicer removes the body of all the functions except
+/// those on the shortest path, those within the call-depth of the
+/// shortest path, those given by name as command line argument,
+/// and those that contain a given irep_idt snippet
+/// If no properties are set by the user, we preserve all functions on
+/// the shortest paths to each property.
+class aggressive_slicert
+{
+public:
+  aggressive_slicert(
+      goto_modelt & _goto_model,
+      message_handlert &_msg) :
+      goto_model(_goto_model),
+      message_handler(_msg),
+      call_graph(_goto_model)
+  {
+    start_function = goto_model.goto_functions.entry_point();
+    call_depth=0;
+  }
+
+  ///  \brief Removes the body of all functions except those on the
+  /// shortest path or functions
+  /// that are reachable from functions on the shortest path within
+  /// N calls, where N is given by the parameter "distance"
+  void doit();
+
+  /// \brief Adds a list of functions to the set of functions for the aggressive
+  /// slicer to preserve
+  /// \param  function list a list of functions in form std::list<std::string>, as returned
+  /// by get_cmdline_option.
+  void preserve_functions(const std::list<std::string>& function_list)
+  {
+    for(const auto &f : function_list)
+      functions_to_keep.insert(f);
+  };
+
+  std::list<std::string> properties;
+  std::size_t call_depth;
+  std::list<std::string> name_snippets;
+
+private:
+  irep_idt start_function;
+  goto_modelt & goto_model;
+  message_handlert & message_handler;
+  std::unordered_set<irep_idt, irep_id_hash> functions_to_keep;
+  call_grapht call_graph;
+
+  /// \brief Finds all functions whose name contains a name snippet
+  /// and adds them to the std::unordered_set of irep_idts of functions
+  /// for the aggressive slicer to preserve
+  void find_functions_that_contain_name_snippet();
+
+  /// \brief Finds all properties in the goto_model and writes their
+  /// names to a list. This function is only called if no properties
+  /// are given by the user
+  void get_property_list();
+};
+
 #endif // CPROVER_GOTO_INSTRUMENT_REMOVE_FUNCTION_H

From 50aed7458c7249ce68027801dc18d23bca4a8467 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Mon, 23 Oct 2017 10:27:56 +0200
Subject: [PATCH 08/14] Aggressive slice should also do a reachability slice
 and a slice of gobal inits

---
 .../goto_instrument_parse_options.cpp         | 24 +++++++++++++++++--
 1 file changed, 22 insertions(+), 2 deletions(-)

diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 82929997a5d..30ba633e914 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -662,8 +662,18 @@ int goto_instrument_parse_optionst::doit()
     {
       do_indirect_call_and_rtti_removal();
       reachable_call_grapht reach_graph(goto_model);
-      if(cmdline.isset("xml"))
-        reach_graph.output_xml(std::cout);
+      if(cmdline.isset("property"))
+      {
+        std::list<std::string> function_names = cmdline.get_values("property");
+        if(function_names.size() > 1)
+          status() << "Only one destination allowed, "
+              "using only first function name given\n";
+        cmdline.get_value("property");
+        std::cout << "list of reachable functions: \n";
+        for(const auto f :
+            reach_graph.backward_slice(function_names.front()))
+          std::cout << f << "\n";
+      }
       else
         reach_graph.output_dot(std::cout);
     return 0;
@@ -1425,6 +1435,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     do_indirect_call_and_rtti_removal();
 
+    status() << "Slicing away initializations of unused global variables"
+             << eom;
+    slice_global_inits(goto_model);
+
     status() << "Performing an aggressive slice" << eom;
     aggressive_slicert aggressive_slicer(goto_model, get_message_handler());
 
@@ -1444,6 +1458,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
           "preserve-functions-containing");
 
     aggressive_slicer.doit();
+
+    status() << "Performing a reachability slice" << eom;
+    if(cmdline.isset("property"))
+      reachability_slicer(goto_model, cmdline.get_values("property"));
+    else
+      reachability_slicer(goto_model);
   }
 
   // recalculate numbers, etc.

From 17441135fc91e895c9a631855f064d096b405c30 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Tue, 17 Oct 2017 10:51:17 +0200
Subject: [PATCH 09/14] Return functions reachable within N function calls

Adds call_grapht::reachable_within_n_steps. Function is passed an unordered set of function names and a number of steps, N,, and adds any function reachable within N function calls from the original set of functions, to the set of function names
---
 src/analyses/call_graph.cpp | 47 +++++++++++++++++++++++++++++++++++++
 src/analyses/call_graph.h   |  9 +++++++
 2 files changed, 56 insertions(+)

diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp
index dec7f9205c8..fece7b93975 100644
--- a/src/analyses/call_graph.cpp
+++ b/src/analyses/call_graph.cpp
@@ -126,6 +126,53 @@ std::list<irep_idt> call_grapht::shortest_function_path(
   return result;
 }
 
+void call_grapht::reachable_within_n_steps(
+    std::size_t steps,
+    std::unordered_set<irep_idt,
+    irep_id_hash> & function_list)
+{
+  std::list<node_indext> worklist;
+
+  for(const auto &f : function_list)
+  {
+    node_indext start_index;
+    if(get_node_index(f, start_index))
+      worklist.push_back(start_index);
+    else
+      throw "function not found in call graph";
+  }
+
+  // mark end of level 0
+  worklist.push_back(std::numeric_limits<std::size_t>::max());
+  std::size_t depth=0;
+
+  while(!worklist.empty())
+  {
+    const node_indext id = worklist.front();
+    worklist.pop_front();
+
+    // check if we have hit end of level
+    if(id == std::numeric_limits<std::size_t>::max())
+    {
+      depth++;
+      // mark end of next level
+      if(!worklist.empty())
+        worklist.push_back(id);
+      continue;
+    }
+    function_list.insert(nodes[id].function_name);
+
+    if(depth < steps)
+    {
+      for(const auto &o : nodes[id].out)
+      {
+        if(function_list.find(nodes[o.first].function_name)
+            == function_list.end())
+          worklist.push_back(o.first);
+      }
+    }
+  }
+}
 
 std::unordered_set<irep_idt, irep_id_hash>
 call_grapht::reachable_functions(irep_idt start_function)
diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h
index 28fcd147173..53e59547c7e 100644
--- a/src/analyses/call_graph.h
+++ b/src/analyses/call_graph.h
@@ -62,6 +62,15 @@ class call_grapht: public grapht<call_graph_nodet>
   /// \return list of function names on the shortest path between src and dest
   std::list<irep_idt>shortest_function_path(irep_idt src, irep_idt dest);
 
+  /// \brief get the names of all functions reachable from a list of functions
+  /// within N function call steps.
+  /// \param function_list  list of functions to start from. Functions reachable within
+  /// N function call steps are appended to this list
+  /// \param steps  number of function call steps
+  void reachable_within_n_steps(std::size_t steps,
+      std::unordered_set<irep_idt, irep_id_hash> &function_list);
+
+
   /// get the index of the node that corresponds to a function name
   /// \param[in] function_name function_name passed by reference
   /// \param[out] n variable for the node index to be written to

From 1eeacb0d4e35d26415d0e0c2f81b9cc5650cebd9 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Wed, 11 Oct 2017 15:09:50 +0200
Subject: [PATCH 10/14] Find source location from a property irep_idt

returns the source_locationt for a property irep_idt
---
 src/goto-programs/show_properties.cpp | 24 ++++++++++++++++++++++++
 src/goto-programs/show_properties.h   |  7 +++++++
 2 files changed, 31 insertions(+)

diff --git a/src/goto-programs/show_properties.cpp b/src/goto-programs/show_properties.cpp
index 7f0be70cc64..663f1d03393 100644
--- a/src/goto-programs/show_properties.cpp
+++ b/src/goto-programs/show_properties.cpp
@@ -23,6 +23,30 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "goto_functions.h"
 #include "goto_model.h"
 
+
+source_locationt find_property(
+    const irep_idt &property,
+    const goto_functionst & goto_functions)
+{
+  for(const auto &fct : goto_functions.function_map)
+  {
+    const goto_programt &goto_program = fct.second.body;
+
+    for(const auto &ins : goto_program.instructions)
+    {
+      if(ins.is_assert())
+      {
+        if(ins.source_location.get_property_id() == property)
+        {
+          return ins.source_location;
+        }
+      }
+    }
+  }
+  throw "property not found";
+}
+
+
 void show_properties(
   const namespacet &ns,
   const irep_idt &identifier,
diff --git a/src/goto-programs/show_properties.h b/src/goto-programs/show_properties.h
index 0cb0d1c641f..19109bd1d5f 100644
--- a/src/goto-programs/show_properties.h
+++ b/src/goto-programs/show_properties.h
@@ -28,4 +28,11 @@ void show_properties(
   ui_message_handlert::uit ui,
   const goto_functionst &goto_functions);
 
+/// \brief Returns a source_locationt that corresponds
+/// to the property given by an irep_idt.
+/// \param property irep_idt and goto_functions
+source_locationt find_property(
+    const irep_idt &property,
+    const goto_functionst &);
+
 #endif // CPROVER_GOTO_PROGRAMS_SHOW_PROPERTIES_H

From a80f9a4265f9eacc5af8c1c8002d73b109e6acd0 Mon Sep 17 00:00:00 2001
From: polgreen <polgreen@amazon.com>
Date: Mon, 23 Oct 2017 17:06:23 +0200
Subject: [PATCH 11/14] Sound aggressive slicer

Extends the aggressive slicer with an option --preserve-all-direct-paths

This preserves all functions on direct, loop free, paths from the start function to the function containing the property, and removes the function bodies of all other functions.

This significantly reduces the size of the binary whilst ensuring that no counter-examples (possible with the given unwinding limit) are missed (although the counterexamples produced may still be spurious)
---
 src/analyses/reachable_call_graph.cpp         |  5 +++++
 src/analyses/reachable_call_graph.h           |  5 +++++
 .../goto_instrument_parse_options.cpp         | 14 ++++++++++++++
 .../goto_instrument_parse_options.h           |  1 +
 src/goto-instrument/remove_function.cpp       | 18 +++++++++++++++---
 src/goto-instrument/remove_function.h         | 19 ++++++++++++++-----
 6 files changed, 54 insertions(+), 8 deletions(-)

diff --git a/src/analyses/reachable_call_graph.cpp b/src/analyses/reachable_call_graph.cpp
index 2ed17371dd9..4c65c60bef4 100644
--- a/src/analyses/reachable_call_graph.cpp
+++ b/src/analyses/reachable_call_graph.cpp
@@ -17,6 +17,11 @@ reachable_call_grapht::reachable_call_grapht
   build(_goto_model.goto_functions);
 }
 
+void reachable_call_grapht::initialize(const goto_modelt & _goto_model)
+{
+  build(_goto_model.goto_functions);
+}
+
 void reachable_call_grapht::build(const goto_functionst & goto_functions)
 {
   irep_idt start_function_name = goto_functions.entry_point();
diff --git a/src/analyses/reachable_call_graph.h b/src/analyses/reachable_call_graph.h
index 4dcfd5cfd0c..2f42ab4ad1a 100644
--- a/src/analyses/reachable_call_graph.h
+++ b/src/analyses/reachable_call_graph.h
@@ -20,6 +20,7 @@ class reachable_call_grapht: public call_grapht
 {
 public:
   explicit reachable_call_grapht(const goto_modelt &);
+  reachable_call_grapht() = default;
 
   /// \brief performs a backwards slice on a reachable call graph
   /// and returns an unordered set of all functions between the initial
@@ -28,6 +29,10 @@ class reachable_call_grapht: public call_grapht
   /// \return unordered set of function names
   std::unordered_set<irep_idt, irep_id_hash>
   backward_slice(irep_idt destination_function);
+  /// \brief used to initialise reachable_call_graph if we have used the
+  /// empty constructor. Necessary for aggressive slicer, to avoid constructing
+  /// reachable call graph unless we need it.
+  void initialize(const goto_modelt &);
 protected:
   void build(const goto_functionst &);
   void build(const goto_functionst &, irep_idt start_function);
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index 30ba633e914..7ef82bf4cb6 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1442,6 +1442,18 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     status() << "Performing an aggressive slice" << eom;
     aggressive_slicert aggressive_slicer(goto_model, get_message_handler());
 
+    if(cmdline.isset("preserve-all-direct-paths"))
+    {
+      if(!cmdline.isset("property"))
+      {
+        error() << "Property must be specified"
+                << " with the sound aggressive slicer"
+                << eom;
+        throw 0;
+      }
+      aggressive_slicer.preserve_all_direct_paths=true;
+    }
+
     if(cmdline.isset("call-depth"))
       aggressive_slicer.call_depth = safe_string2unsigned(
           cmdline.get_value("call-depth"));
@@ -1572,6 +1584,8 @@ void goto_instrument_parse_optionst::help()
     " --preserve-function <f>      force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
     " --preserve-function containing <f>\n"
     "                              force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
+    " --preserve-all-direct-paths  force the aggressive slicer to preserve all functions on direct paths to the property\n" // NOLINT(*)
+    "                              Must be used with a specified property\n"
     "\n"
     "Further transformations:\n"
     " --constant-propagator        propagate constants and simplify expressions\n" // NOLINT(*)
diff --git a/src/goto-instrument/goto_instrument_parse_options.h b/src/goto-instrument/goto_instrument_parse_options.h
index 4bdc05c3039..55db20837d9 100644
--- a/src/goto-instrument/goto_instrument_parse_options.h
+++ b/src/goto-instrument/goto_instrument_parse_options.h
@@ -85,6 +85,7 @@ Author: Daniel Kroening, kroening@kroening.com
   "(harness-generator):" \
   "(preserve-function):" \
   "(preserve-functions-containing):" \
+  "(preserve-all-direct-paths)" \
 
 class goto_instrument_parse_optionst:
   public parse_options_baset,
diff --git a/src/goto-instrument/remove_function.cpp b/src/goto-instrument/remove_function.cpp
index 3f3a7415964..ffaf3f1bfe3 100644
--- a/src/goto-instrument/remove_function.cpp
+++ b/src/goto-instrument/remove_function.cpp
@@ -71,13 +71,25 @@ void aggressive_slicert::doit()
   if(!name_snippets.empty())
     find_functions_that_contain_name_snippet();
 
+  if(preserve_all_direct_paths)
+    reach_graph.initialize(goto_model);
+
   for(const auto &p : properties)
   {
     source_locationt property_loc = find_property(p, goto_model.goto_functions);
     irep_idt dest = property_loc.get_function();
-    for(const auto &func : call_graph.shortest_function_path(
-        start_function, dest))
-      functions_to_keep.insert(func);
+
+    if(preserve_all_direct_paths)
+    {
+      for(const auto & func : reach_graph.backward_slice(dest))
+        functions_to_keep.insert(func);
+    }
+    else
+    {
+      for(const auto &func : call_graph.shortest_function_path(start_function,
+          dest))
+        functions_to_keep.insert(func);
+    }
   }
 
   // Add functions within distance of shortest path functions
diff --git a/src/goto-instrument/remove_function.h b/src/goto-instrument/remove_function.h
index 47cd2fcf299..f6e004ac2fc 100644
--- a/src/goto-instrument/remove_function.h
+++ b/src/goto-instrument/remove_function.h
@@ -21,6 +21,7 @@ Date: April 2017
 #include <util/irep.h>
 
 #include <analyses/call_graph.h>
+#include <analyses/reachable_call_graph.h>
 
 class goto_modelt;
 class message_handlert;
@@ -47,13 +48,15 @@ class aggressive_slicert
   aggressive_slicert(
       goto_modelt & _goto_model,
       message_handlert &_msg) :
+      preserve_all_direct_paths(false),
+      call_depth(0),
+      start_function(_goto_model.goto_functions.entry_point()),
       goto_model(_goto_model),
       message_handler(_msg),
-      call_graph(_goto_model)
-  {
-    start_function = goto_model.goto_functions.entry_point();
-    call_depth=0;
-  }
+      call_graph(_goto_model),
+      reach_graph()
+      {
+      }
 
   ///  \brief Removes the body of all functions except those on the
   /// shortest path or functions
@@ -71,6 +74,11 @@ class aggressive_slicert
       functions_to_keep.insert(f);
   };
 
+  /// \brief When set to true we preserve all functions on direct paths between
+  /// the start function
+  /// and any given properties. We do not allow this option to be used without
+  /// specifying a property, as that would effectively be doing a full-slice
+  bool preserve_all_direct_paths;
   std::list<std::string> properties;
   std::size_t call_depth;
   std::list<std::string> name_snippets;
@@ -81,6 +89,7 @@ class aggressive_slicert
   message_handlert & message_handler;
   std::unordered_set<irep_idt, irep_id_hash> functions_to_keep;
   call_grapht call_graph;
+  reachable_call_grapht reach_graph;
 
   /// \brief Finds all functions whose name contains a name snippet
   /// and adds them to the std::unordered_set of irep_idts of functions

From 6ce0cd85b3c942033ee0065d52ab8ae46e2a7423 Mon Sep 17 00:00:00 2001
From: polgreen <elizabeth.polgreen@cs.ox.ac.uk>
Date: Tue, 21 Nov 2017 11:45:32 +0000
Subject: [PATCH 12/14] linter fix: line length

---
 src/analyses/call_graph.h             | 3 ++-
 src/goto-instrument/remove_function.h | 4 ++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h
index 53e59547c7e..c8be6914f25 100644
--- a/src/analyses/call_graph.h
+++ b/src/analyses/call_graph.h
@@ -64,7 +64,8 @@ class call_grapht: public grapht<call_graph_nodet>
 
   /// \brief get the names of all functions reachable from a list of functions
   /// within N function call steps.
-  /// \param function_list  list of functions to start from. Functions reachable within
+  /// \param function_list  list of functions to start from.
+  /// Functions reachable within
   /// N function call steps are appended to this list
   /// \param steps  number of function call steps
   void reachable_within_n_steps(std::size_t steps,
diff --git a/src/goto-instrument/remove_function.h b/src/goto-instrument/remove_function.h
index f6e004ac2fc..b161a4c391e 100644
--- a/src/goto-instrument/remove_function.h
+++ b/src/goto-instrument/remove_function.h
@@ -66,8 +66,8 @@ class aggressive_slicert
 
   /// \brief Adds a list of functions to the set of functions for the aggressive
   /// slicer to preserve
-  /// \param  function list a list of functions in form std::list<std::string>, as returned
-  /// by get_cmdline_option.
+  /// \param  function_list    a list of functions in form
+  /// std::list<std::string>, as returned by get_cmdline_option.
   void preserve_functions(const std::list<std::string>& function_list)
   {
     for(const auto &f : function_list)

From fbc04789ffaac2a809001491b31b58fb46aa5c87 Mon Sep 17 00:00:00 2001
From: polgreen <elizabeth.polgreen@cs.ox.ac.uk>
Date: Tue, 21 Nov 2017 13:14:37 +0000
Subject: [PATCH 13/14] Aggressive slicer regression tests

---
 .../goto-instrument/aggressive_slicer1/main.c | 30 +++++++++++++++++++
 .../aggressive_slicer1/test.desc              |  8 +++++
 .../goto-instrument/aggressive_slicer2/main.c | 30 +++++++++++++++++++
 .../aggressive_slicer2/test.desc              |  8 +++++
 .../goto-instrument/aggressive_slicer3/main.c | 29 ++++++++++++++++++
 .../aggressive_slicer3/test.desc              |  8 +++++
 .../goto-instrument/aggressive_slicer4/main.c | 29 ++++++++++++++++++
 .../aggressive_slicer4/test.desc              |  8 +++++
 .../goto-instrument/aggressive_slicer5/main.c | 29 ++++++++++++++++++
 .../aggressive_slicer5/test.desc              |  8 +++++
 .../goto-instrument/aggressive_slicer6/main.c | 29 ++++++++++++++++++
 .../aggressive_slicer6/test.desc              |  8 +++++
 12 files changed, 224 insertions(+)
 create mode 100644 regression/goto-instrument/aggressive_slicer1/main.c
 create mode 100644 regression/goto-instrument/aggressive_slicer1/test.desc
 create mode 100644 regression/goto-instrument/aggressive_slicer2/main.c
 create mode 100644 regression/goto-instrument/aggressive_slicer2/test.desc
 create mode 100644 regression/goto-instrument/aggressive_slicer3/main.c
 create mode 100644 regression/goto-instrument/aggressive_slicer3/test.desc
 create mode 100644 regression/goto-instrument/aggressive_slicer4/main.c
 create mode 100644 regression/goto-instrument/aggressive_slicer4/test.desc
 create mode 100644 regression/goto-instrument/aggressive_slicer5/main.c
 create mode 100644 regression/goto-instrument/aggressive_slicer5/test.desc
 create mode 100644 regression/goto-instrument/aggressive_slicer6/main.c
 create mode 100644 regression/goto-instrument/aggressive_slicer6/test.desc

diff --git a/regression/goto-instrument/aggressive_slicer1/main.c b/regression/goto-instrument/aggressive_slicer1/main.c
new file mode 100644
index 00000000000..ded2b118a5c
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer1/main.c
@@ -0,0 +1,30 @@
+void D()
+{
+  __CPROVER_assert(0,"");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+  	D();
+}
+
+void B() 
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+
+  __CPROVER_assume(nondet!=3);
+  switch(nondet)
+  {
+    case 1: B(); break;
+    case 3: C(); break;
+    default: break;
+  }
+return 0;
+}
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer1/test.desc b/regression/goto-instrument/aggressive_slicer1/test.desc
new file mode 100644
index 00000000000..c10f611316f
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer2/main.c b/regression/goto-instrument/aggressive_slicer2/main.c
new file mode 100644
index 00000000000..ded2b118a5c
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer2/main.c
@@ -0,0 +1,30 @@
+void D()
+{
+  __CPROVER_assert(0,"");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+  	D();
+}
+
+void B() 
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+
+  __CPROVER_assume(nondet!=3);
+  switch(nondet)
+  {
+    case 1: B(); break;
+    case 3: C(); break;
+    default: break;
+  }
+return 0;
+}
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer2/test.desc b/regression/goto-instrument/aggressive_slicer2/test.desc
new file mode 100644
index 00000000000..4e4584eb814
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --property D.assertion.1
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer3/main.c b/regression/goto-instrument/aggressive_slicer3/main.c
new file mode 100644
index 00000000000..db3ed7e203b
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer3/main.c
@@ -0,0 +1,29 @@
+void D()
+{
+  __CPROVER_assert(0,"");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+  	D();
+}
+
+void B() 
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+
+  switch(nondet)
+  {
+    case 1: B(); break;
+    case 3: C(); break;
+    default: break;
+  }
+return 0;
+}
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer3/test.desc b/regression/goto-instrument/aggressive_slicer3/test.desc
new file mode 100644
index 00000000000..a37279572b5
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer3/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer4/main.c b/regression/goto-instrument/aggressive_slicer4/main.c
new file mode 100644
index 00000000000..85d56f13603
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer4/main.c
@@ -0,0 +1,29 @@
+void D()
+{
+  __CPROVER_assert(0,"");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+  	D();
+}
+
+void B() 
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+  __CPROVER_assume(nondet!=3);
+  switch(nondet)
+  {
+    case 1: B(); break;
+    case 3: C(); break;
+    default: break;
+  }
+return 0;
+}
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer4/test.desc b/regression/goto-instrument/aggressive_slicer4/test.desc
new file mode 100644
index 00000000000..75d03f51c09
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer4/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --preserve-function B
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer5/main.c b/regression/goto-instrument/aggressive_slicer5/main.c
new file mode 100644
index 00000000000..f3bc92a8e9a
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer5/main.c
@@ -0,0 +1,29 @@
+void D()
+{
+  __CPROVER_assert(0,"");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+  	D();
+}
+
+void B() 
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+__CPROVER_assume(nondet!=3);
+  switch(nondet)
+  {
+    case 1: B(); break;
+    case 3: C(); break;
+    default: break;
+  }
+return 0;
+}
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer5/test.desc b/regression/goto-instrument/aggressive_slicer5/test.desc
new file mode 100644
index 00000000000..08c29c68d99
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer5/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --property D.assertion.1 --preserve-all-direct-paths
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer6/main.c b/regression/goto-instrument/aggressive_slicer6/main.c
new file mode 100644
index 00000000000..85d56f13603
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer6/main.c
@@ -0,0 +1,29 @@
+void D()
+{
+  __CPROVER_assert(0,"");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+  	D();
+}
+
+void B() 
+{
+  C();
+};
+
+int main()
+{
+  int nondet;
+  __CPROVER_assume(nondet!=3);
+  switch(nondet)
+  {
+    case 1: B(); break;
+    case 3: C(); break;
+    default: break;
+  }
+return 0;
+}
\ No newline at end of file
diff --git a/regression/goto-instrument/aggressive_slicer6/test.desc b/regression/goto-instrument/aggressive_slicer6/test.desc
new file mode 100644
index 00000000000..b40f55b4185
--- /dev/null
+++ b/regression/goto-instrument/aggressive_slicer6/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --call-depth 1
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
\ No newline at end of file

From 35ee9e43e42ef710b7c0c26ba35041ac3a1235d2 Mon Sep 17 00:00:00 2001
From: polgreen <elizabeth.polgreen@cs.ox.ac.uk>
Date: Tue, 21 Nov 2017 13:25:58 +0000
Subject: [PATCH 14/14] re-introduce constructor

---
 src/analyses/call_graph.cpp | 9 +++++++--
 src/analyses/call_graph.h   | 1 +
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/analyses/call_graph.cpp b/src/analyses/call_graph.cpp
index fece7b93975..7b24e163ce1 100644
--- a/src/analyses/call_graph.cpp
+++ b/src/analyses/call_graph.cpp
@@ -18,9 +18,14 @@ call_grapht::call_grapht()
 {
 }
 
-call_grapht::call_grapht(const goto_modelt &goto_model)
+call_grapht::call_grapht(const goto_modelt &goto_model):
+  call_grapht(goto_model.goto_functions)
 {
-  forall_goto_functions(f_it, goto_model.goto_functions)
+}
+
+call_grapht::call_grapht(const goto_functionst &goto_functions)
+{
+  forall_goto_functions(f_it, goto_functions)
   {
     const goto_programt &body=f_it->second.body;
     add(f_it->first, body);
diff --git a/src/analyses/call_graph.h b/src/analyses/call_graph.h
index c8be6914f25..9b50ee4f984 100644
--- a/src/analyses/call_graph.h
+++ b/src/analyses/call_graph.h
@@ -42,6 +42,7 @@ class call_grapht: public grapht<call_graph_nodet>
 public:
   call_grapht();
   explicit call_grapht(const goto_modelt &);
+  explicit call_grapht(const goto_functionst &);
 
   void add(const irep_idt &caller, const irep_idt &callee);
   void output_xml(std::ostream &out) const;