Aggressive slicer v2

regression/goto-instrument/aggressive_slicer1/main.c

@@ -0,0 +1,36 @@
+// test should pass. Shortest path main -> C -> D
+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;
+}

regression/goto-instrument/aggressive_slicer1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer2/main.c

@@ -0,0 +1,39 @@
+// test should pass. Shortest path is preserved, main -> C -> D,
+// but is not a possible counterexample because of assumption that
+// nondet != 3
+
+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;
+}

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

regression/goto-instrument/aggressive_slicer3/main.c

@@ -0,0 +1,35 @@
+// test should fail. Shortest path is preserved, main -> C -> D,
+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;
+}

regression/goto-instrument/aggressive_slicer3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer4/main.c

@@ -0,0 +1,39 @@
+// test should fail
+// shortest path only is not sufficient to violate assertion,
+// but we specifically require that function B is kept, which
+// allows path main -> B -> C -> D
+
+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;
+}

regression/goto-instrument/aggressive_slicer4/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --aggressive-slice-preserve-function B
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer5/main.c

@@ -0,0 +1,38 @@
+// Test should fail. Shortest path only is not sufficient
+// due to assumption that nondet !=3, but
+// preserve-all-direct-paths preserves the path main -> B -> C -> D.
+
+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;
+}

regression/goto-instrument/aggressive_slicer5/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --property D.assertion.1 --aggressive-slice-preserve-all-direct-paths
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer6/main.c

@@ -0,0 +1,40 @@
+// Test should fail
+// Assertion in D is reachable when call depth of 1 is preserved,
+// Shortest path = main -> C -> D, which is not possible due to assumption
+// nondet!=3, but call depth 1 preserves the body of function B, which can also reach
+// C.
+
+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;
+}

regression/goto-instrument/aggressive_slicer6/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice --aggressive-slice-call-depth 1
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/goto-instrument/aggressive_slicer7/main.c

@@ -0,0 +1,46 @@
+// Test should fail
+// Assertion in D is reachable by main -> C -> D
+// Assertion in E is reachable by main -> E
+
+void D()
+{
+  __CPROVER_assert(0, "");
+}
+
+void C()
+{
+  int nondet;
+  if(nondet)
+    D();
+}
+
+void B()
+{
+  C();
+};
+
+void E()
+{
+  __CPROVER_assert(0, "");
+}
+
+int main()
+{
+  int nondet;
+
+  switch(nondet)
+  {
+  case 1:
+    B();
+    break;
+  case 2:
+    E();
+    break;
+  case 3:
+    C();
+    break;
+  default:
+    break;
+  }
+  return 0;
+}

regression/goto-instrument/aggressive_slicer7/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--aggressive-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

src/analyses/call_graph_helpers.cpp

@@ -74,7 +74,7 @@ std::set<irep_idt> get_reaching_functions(
 std::set<irep_idt> get_functions_reachable_within_n_steps(
   const call_grapht::directed_grapht &graph,
   const std::set<irep_idt> &start_functions,
-  std::size_t &n)
+  std::size_t n)
 {
   std::vector<std::size_t> start_indices;
   std::set<irep_idt> result;
@@ -91,8 +91,32 @@ std::set<irep_idt> get_functions_reachable_within_n_steps(
 std::set<irep_idt> get_functions_reachable_within_n_steps(
   const call_grapht::directed_grapht &graph,
   const irep_idt &start_function,
-  std::size_t &n)
+  std::size_t n)
 {
-  std::set<irep_idt> start_functions({ start_function });
+  std::set<irep_idt> start_functions({start_function});
   return get_functions_reachable_within_n_steps(graph, start_functions, n);
 }
+
+void disconnect_unreachable_functions(
+  call_grapht::directed_grapht &graph,
+  const irep_idt &function)
+{
+  graph.disconnect_unreachable(*(graph.get_node_index(function)));
+}
+
+std::list<irep_idt> get_shortest_function_path(
+  const call_grapht::directed_grapht &graph,
+  const irep_idt &src,
+  const irep_idt &dest)
+{
+  std::list<irep_idt> result;
+  std::list<std::size_t> path;
+
+  graph.shortest_path(
+    *(graph.get_node_index(src)), *(graph.get_node_index(dest)), path);
+
+  for(const auto &n : path)
+    result.push_back(graph[n].function);
+
+  return result;
+}