Tests for the new functionality in goto-analyzer

Author: martin

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