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!