Merge pull request #5404 from martin-cs/feature/ai-local-history

Add an abstract interpreter 'history' that gives (local) per-path analysis and / or loop unwinding

Author: martin-cs

regression/goto-analyzer/local_control_flow_history_01/main.c

@@ -0,0 +1,55 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int branch;
+  int x = 0;
+
+  if(branch)
+  {
+    x = 1;
+  }
+  else
+  {
+    x = -1;
+  }
+
+  // Merging a constant domain here will make this unprovable
+  assert(x != 0);
+
+  // Some subtle points here...
+  // The history tracks paths, it is up to the domain to track the
+  // path conditon / consequences of that path.
+  //
+  // We have two paths:
+  //  branch == ?, x ==  1
+  //  branch == 0, x == -1
+  //
+  // As the domain in the first case can't express branch != 0
+  // we will wind up with three paths here, including a spurious
+  // one with branch == 0, x == 1.
+  if(branch)
+  {
+    assert(x == 1);
+  }
+  else
+  {
+    assert(x == -1);
+  }
+
+  // Working around the domain issues...
+  // (This doesn't increase the number of paths)
+  if(x == 1)
+  {
+    x--;
+  }
+  else
+  {
+    x++;
+  }
+
+  // Should be true in all 3 paths
+  assert(x == 0);
+
+  return 0;
+}

regression/goto-analyzer/local_control_flow_history_01/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--verify --recursive-interprocedural --branching 0 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion x != 0: SUCCESS$
+^\[main.assertion.2\] .* assertion x == 1: SUCCESS$
+^\[main.assertion.3\] .* assertion x == -1: FAILURE \(if reachable\)$
+^\[main.assertion.4\] .* assertion x == 0: SUCCESS$
+--
+^warning: ignoring
+--
+This demonstrates the "lazy merging" that comes from tracking the history of branching

regression/goto-analyzer/local_control_flow_history_02/main.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int branching_array[5];
+  int x = 1;
+
+  if(branching_array[0])
+  {
+    ++x;
+  }
+  // Two paths...
+  assert(x > 0);
+
+  if(branching_array[1])
+  {
+    ++x;
+  }
+  // Four paths...
+  assert(x > 0);
+
+  if(branching_array[2])
+  {
+    ++x;
+  }
+  // Eight paths...
+  assert(x > 0);
+
+  if(branching_array[3])
+  {
+    ++x;
+  }
+  // Paths merge so there will be some paths that will set x to \top
+  // and so this will be flagged as unknown
+  assert(x > 0);
+  // In principle it would be possible to merge paths in such a way
+  // that the those with similar domains are merged and this would be
+  // able to be proved.  The local_control_flow_history code doesn't
+  // do this though.
+
+  return 0;
+}

regression/goto-analyzer/local_control_flow_history_02/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--verify --recursive-interprocedural --branching 12 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion x > 0: SUCCESS$
+^\[main.assertion.2\] .* assertion x > 0: SUCCESS$
+^\[main.assertion.3\] .* assertion x > 0: SUCCESS$
+^\[main.assertion.4\] .* assertion x > 0: UNKNOWN$
+--
+^warning: ignoring
+--
+This demonstrates hitting the path limit and the merging of paths

regression/goto-analyzer/local_control_flow_history_03/main.c

@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int total = 0;
+  int n = 50;
+  int i;
+
+  for(i = 0; i < n; ++i)
+  {
+    total += i;
+  }
+
+  assert(total == (n * (n - 1) / 2));
+
+  return 0;
+}

regression/goto-analyzer/local_control_flow_history_03/test.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--verify --recursive-interprocedural --loop-unwind 0 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion total == \(n \* \(n - 1\) / 2\): SUCCESS$
+--
+^warning: ignoring
+--
+A basic test of loop unwinding.

regression/goto-analyzer/local_control_flow_history_04/main.c

@@ -0,0 +1,42 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int total;
+  int n;
+  int i;
+
+  total = 0;
+  n = 8;
+  for(i = 0; i < n; ++i)
+  {
+    total += i;
+  }
+
+  // Unknown due to the limit on unwindings
+  assert(total == (n * (n - 1) / 2));
+
+  // Condense down to one path...
+
+  total = 0;
+  n = 16;
+  for(i = 0; i < n; ++i)
+  {
+    total += i;
+  }
+
+  // Creates a merge path but only one user of it
+  assert(total == (n * (n - 1) / 2));
+
+  total = 0;
+  n = 32;
+  for(i = 0; i < n; ++i)
+  {
+    total += i;
+  }
+
+  // Provable
+  assert(total == (n * (n - 1) / 2));
+
+  return 0;
+}

regression/goto-analyzer/local_control_flow_history_04/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--verify --recursive-interprocedural --loop-unwind 17 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion total == \(n \* \(n - 1\) / 2\): SUCCESS$
+^\[main.assertion.2\] .* assertion total == \(n \* \(n - 1\) / 2\): SUCCESS$
+^\[main.assertion.3\] .* assertion total == \(n \* \(n - 1\) / 2\): UNKNOWN$
+--
+^warning: ignoring
+--
+A basic test of the loop unwinding limit.
+You might think this has an off-by-one error but to process a loop 16 times
+you have to visit the loop guard 17 times.  Setting the loop limit to 16 will
+cause the last two visits to merge loosing the precision needed to prove the
+conjecture.

regression/goto-analyzer/local_control_flow_history_05/main.c

@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  int total;
+  int n;
+  int i;
+  int branching[4];
+
+  total = 0;
+  n = 4;
+  for(i = 0; i < n; ++i)
+  {
+    if(branching[i])
+    {
+      total += i;
+    }
+  }
+
+  assert(total <= (n * (n - 1) / 2));
+
+  return 0;
+}

regression/goto-analyzer/local_control_flow_history_05/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--verify --recursive-interprocedural --loop-unwind-and-branching 32 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion total <= \(n \* \(n - 1\) / 2\): SUCCESS$
+--
+^warning: ignoring
+--
+Test tracking all local control-flow history.
+Note the exponential rise in the number of paths!

regression/goto-analyzer/local_control_flow_history_06/main.c

@@ -0,0 +1,37 @@
+#include <assert.h>
+
+#define CODE_BLOCK                                                             \
+  int i;                                                                       \
+  float flotal = 0;                                                            \
+  for(i = 0; i < n; ++i)                                                       \
+  {                                                                            \
+    flotal += i;                                                               \
+  }                                                                            \
+  assert(flotal == (n * (n - 1) / 2))
+
+void do_the_loop(int n)
+{
+  CODE_BLOCK;
+}
+
+int main(int argc, char **argv)
+{
+  int j;
+
+  // Will give unknown unless the bound is over 25
+  for(j = 0; j < 5; j++)
+  {
+    int n = 5;
+    CODE_BLOCK;
+  }
+
+  // Paths in the loop will merge but that is OK
+  // because the value of n is the important bit
+  for(j = 0; j < 1000; j++)
+  {
+    int n = 10;
+    do_the_loop(n);
+  }
+
+  return 0;
+}

regression/goto-analyzer/local_control_flow_history_06/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--verify --recursive-interprocedural --loop-unwind-and-branching 12 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion flotal == \(n \* \(n - 1\) / 2\): UNKNOWN$
+^\[do_the_loop.assertion.1\] .* assertion flotal == \(n \* \(n - 1\) / 2\): SUCCESS$
+--
+^warning: ignoring
+--
+Demonstrate the function local behaviour of this history

src/analyses/Makefile

@@ -24,6 +24,7 @@ SRC = ai.cpp \
       is_threaded.cpp \
       local_bitvector_analysis.cpp \
       local_cfg.cpp \
+      local_control_flow_history.cpp \
       local_may_alias.cpp \
       local_safe_pointers.cpp \
       locals.cpp \

src/analyses/ai.cpp

@@ -303,8 +303,14 @@ bool ai_baset::visit(
       if(to_l == goto_program.instructions.end())
         continue;
 
-      new_data |=
-        visit_edge(function_id, p, function_id, to_l, ns, working_set);
+      new_data |= visit_edge(
+        function_id,
+        p,
+        function_id,
+        to_l,
+        ai_history_baset::no_caller_history,
+        ns,
+        working_set); // Local steps so no caller history needed
     }
   }
 
@@ -316,11 +322,13 @@ bool ai_baset::visit_edge(
   trace_ptrt p,
   const irep_idt &to_function_id,
   locationt to_l,
+  trace_ptrt caller_history,
   const namespacet &ns,
   working_sett &working_set)
 {
   // Has history taught us not to step here...
-  auto next = p->step(to_l, *(storage->abstract_traces_before(to_l)));
+  auto next =
+    p->step(to_l, *(storage->abstract_traces_before(to_l)), caller_history);
   if(next.first == ai_history_baset::step_statust::BLOCKED)
     return false;
   trace_ptrt to_p = next.second;
@@ -366,6 +374,8 @@ bool ai_baset::visit_edge_function_call(
     p_call,
     calling_function_id,
     l_return,
+    ai_history_baset::
+      no_caller_history, // Not needed as we are skipping the function call
     ns,
     working_set);
 }
@@ -439,6 +449,7 @@ bool ai_baset::visit_function_call(
     p_call,
     calling_function_id,
     l_return,
+    ai_history_baset::no_caller_history, // Would be the same as p_call...
     ns,
     working_set);
 }
@@ -480,6 +491,8 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
       p_call,
       callee_function_id,
       l_begin,
+      ai_history_baset::
+        no_caller_history, // Not needed as p_call already has the info
       ns,
       catch_working_set);
 
@@ -525,6 +538,7 @@ bool ai_recursive_interproceduralt::visit_edge_function_call(
           p_end,
           calling_function_id,
           l_return,
+          p_call, // To allow function-local history
           ns,
           working_set);
       }

src/analyses/ai.h

@@ -252,7 +252,11 @@ class ai_baset
 
     locationt n = std::next(l);
 
-    auto step_return = p->step(n, *(storage->abstract_traces_before(n)));
+    auto step_return = p->step(
+      n,
+      *(storage->abstract_traces_before(n)),
+      ai_history_baset::no_caller_history);
+    // Caller history not needed as this is a local step
 
     return storage->abstract_state_before(step_return.second, *domain_factory);
   }
@@ -469,6 +473,7 @@ class ai_baset
     trace_ptrt p,
     const irep_idt &to_function_id,
     locationt to_l,
+    trace_ptrt caller_history,
     const namespacet &ns,
     working_sett &working_set);