Merge pull request #5072 from martin-cs/feature/ai-history-use-cases

martin-cs · web-flow · commit 5d6d1aead28a · 2019-11-27T13:08:07.000Z
(Calling) context sensitivity in the abstract interpreter
diff --git a/regression/goto-analyzer/command_line_01/main.c b/regression/goto-analyzer/command_line_01/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int f00(int x)
+{
+  assert(x != 0);
+  return 0;
+}
+
+int main(int argc, char **argv)
+{
+  int v = 0;
+  v = f00(v);
+  assert(v != 0);
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/command_line_01/test.desc b/regression/goto-analyzer/command_line_01/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --recursive-interprocedural --ahistorical --constants --one-domain-per-history
+\[main.assertion.1\] line 13 assertion v != 0: FAILURE \(if reachable\)
+\[f00.assertion.1\] line 5 assertion x != 0: FAILURE \(if reachable\)
+Summary: 0 pass, 2 fail if reachable, 0 unknown
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests the full AI configuration tuple AI/history/domain/storage
diff --git a/regression/goto-analyzer/command_line_02/main.c b/regression/goto-analyzer/command_line_02/main.c
@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int f00(int x)
+{
+  assert(x != 0);
+  return 0;
+}
+
+int main(int argc, char **argv)
+{
+  int v = 0;
+  v = f00(v);
+  assert(v != 0);
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/command_line_02/test.desc b/regression/goto-analyzer/command_line_02/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --recursive-interprocedural --ahistorical --constants --one-domain-per-location
+\[main.assertion.1\] line 13 assertion v != 0: FAILURE \(if reachable\)
+\[f00.assertion.1\] line 5 assertion x != 0: FAILURE \(if reachable\)
+Summary: 0 pass, 2 fail if reachable, 0 unknown
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests the full AI configuration tuple AI/history/domain/storage
diff --git a/regression/goto-analyzer/context_sensitivity_01/main.c b/regression/goto-analyzer/context_sensitivity_01/main.c
@@ -0,0 +1,28 @@
+#include <assert.h>
+
+unsigned fib(unsigned x)
+{
+  switch(x)
+  {
+  case 0:
+    return 0;
+    break;
+  case 1:
+    return 1;
+    break;
+  default:
+    return fib(x - 1) + fib(x - 2);
+    break;
+  }
+}
+
+int main(int argc, char **argv)
+{
+  unsigned v = fib(7);
+  assert(v == 13); // Requires context sensitivity to handle with constants
+
+  unsigned w = fib(9);
+  assert(w == 24); // Requires location, not just function tracking
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/context_sensitivity_01/test.desc b/regression/goto-analyzer/context_sensitivity_01/test.desc
@@ -0,0 +1,12 @@
+FUTURE
+main.c
+--verify --recursive-interprocedural --call-stack 10 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion v == 13: SUCCESS$
+^\[main.assertion.2\] .* assertion w == 24: SUCCESS$
+--
+^warning: ignoring
+--
+This should be possible just tracking constants and calling stacks.
+At the moment the --constants domain can't do it due to the way it proactively merges to handle recursion.
diff --git a/regression/goto-analyzer/context_sensitivity_02/main.c b/regression/goto-analyzer/context_sensitivity_02/main.c
@@ -0,0 +1,17 @@
+#include <assert.h>
+
+int negate(int x)
+{
+  return -x;
+}
+
+int main(int argc, char **argv)
+{
+  int x = 23;
+  int nx = negate(x);
+  int nnx = negate(nx);
+
+  assert(x == nnx);
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/context_sensitivity_02/test.desc b/regression/goto-analyzer/context_sensitivity_02/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--verify --recursive-interprocedural --call-stack 0 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion x == nnx: SUCCESS$
+--
+^warning: ignoring
+--
+A simple test of call stacks and context sensitivity.  Merging calling context with contexts will give a failure.
diff --git a/regression/goto-analyzer/context_sensitivity_03/main.c b/regression/goto-analyzer/context_sensitivity_03/main.c
@@ -0,0 +1,23 @@
+#include <assert.h>
+
+int step(int x)
+{
+  if(x <= 0)
+  {
+    return 0;
+  }
+  else
+  {
+    return x + step(x - 1);
+  }
+}
+
+int main(int argc, char **argv)
+{
+  int x = 5;
+  int res = step(x);
+
+  assert(res == 15);
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/context_sensitivity_03/test.desc b/regression/goto-analyzer/context_sensitivity_03/test.desc
@@ -0,0 +1,11 @@
+FUTURE
+main.c
+--verify --recursive-interprocedural --call-stack 10 --constants --one-domain-per-history
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion res == 15: SUCCESS$
+--
+^warning: ignoring
+--
+This should be possible just tracking constants and calling stacks.
+At the moment the --constants domain can't do it due to the way it proactively merges to handle recursion.
diff --git a/regression/goto-analyzer/context_sensitivity_04/main.c b/regression/goto-analyzer/context_sensitivity_04/main.c
@@ -0,0 +1,24 @@
+#include <assert.h>
+
+int step(int x)
+{
+  if(x == 0)
+  {
+    assert(x == 0);
+    return 0;
+  }
+  else
+  {
+    return step(x - 1);
+  }
+}
+
+int main(int argc, char **argv)
+{
+  int orig = 20;
+  int res = step(orig);
+
+  assert(res == 0);
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/context_sensitivity_04/test.desc b/regression/goto-analyzer/context_sensitivity_04/test.desc
@@ -0,0 +1,12 @@
+CORE
+main.c
+--verify --recursive-interprocedural --call-stack 10 --constants --one-domain-per-history
+^\[main.assertion.1\] .* assertion res == 0: SUCCESS$
+^\[step.assertion.1\] .* assertion x == 0: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests the interaction of call stacks and recursion.
+
diff --git a/regression/goto-analyzer/context_sensitivity_05/main.c b/regression/goto-analyzer/context_sensitivity_05/main.c
@@ -0,0 +1,54 @@
+#include <assert.h>
+
+void f00(int x, int y)
+{
+  if(x < 0)
+  {
+    // Unreachable in all traces if they are considered individually
+    assert(x < 0);
+    assert(1);
+    assert(0);
+  }
+
+  assert(x >= 0); // True in all traces
+  assert(x < 0);  // False in all traces
+  assert(x < 2);  // Split; true in some, false in others
+
+  assert((x <= 0) ? 1 : y);                  // True in some, unknown in others
+  assert((x <= 1) ? 0 : y);                  // False in some, unknown in others
+  assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+
+  if(x < 5)
+  {
+    // Not reachable in all traces
+    assert((x <= 0) ? 1 : y); // True in some, unknown in others
+    assert((x <= 1) ? 0 : y); // False in some, unknown in others
+    assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+  }
+
+  if(x < 3)
+  {
+    // Not reachable in all traces
+    assert((x <= 0) ? 1 : y); // True in some, unknown in others
+    assert((x <= 1) ? 0 : y); // False in some, unknown in others
+    assert((x <= 2) ? ((x <= 3) ? 1 : 0) : y); // A mix of all three
+  }
+}
+
+int nondet_int();
+
+int main(int argc, char **argv)
+{
+  int y = nondet_int();
+
+  // Because the history is context sensitive these should be analysed independently
+  // Just showing the domain will merge them giving top for everything interesting
+  f00(0, y);
+  f00(1, y);
+  f00(2, y);
+  f00(3, y);
+  f00(4, y);
+  f00(5, y);
+
+  return 0;
+}
diff --git a/regression/goto-analyzer/context_sensitivity_05/test.desc b/regression/goto-analyzer/context_sensitivity_05/test.desc
@@ -0,0 +1,25 @@
+CORE
+main.c
+--verify --recursive-interprocedural --call-stack 0 --constants --one-domain-per-history
+^\[f00.assertion.1\] .* assertion x < 0: SUCCESS \(unreachable\)$
+^\[f00.assertion.2\] .* assertion 1: SUCCESS \(unreachable\)$
+^\[f00.assertion.3\] .* assertion 0: SUCCESS \(unreachable\)$
+^\[f00.assertion.4\] .* assertion x >= 0: SUCCESS$
+^\[f00.assertion.5\] .* assertion x < 0: FAILURE \(if reachable\)$
+^\[f00.assertion.6\] .* assertion x < 2: FAILURE \(if reachable\)$
+^\[f00.assertion.7\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
+^\[f00.assertion.8\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
+^\[f00.assertion.9\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: UNKNOWN$
+^\[f00.assertion.10\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
+^\[f00.assertion.11\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
+^\[f00.assertion.12\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: UNKNOWN$
+^\[f00.assertion.13\] .* assertion \(x <= 0\) \? 1 : y: UNKNOWN$
+^\[f00.assertion.14\] .* assertion \(x <= 1\) \? 0 : y: UNKNOWN$
+^\[f00.assertion.15\] .* assertion \(x <= 2\) \? \(\(x <= 3\) \? 1 : 0\) : y: SUCCESS$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Tests the verify tasks handling of multiple traces for each assertion
+
diff --git a/regression/goto-analyzer/intervals_01/test.desc b/regression/goto-analyzer/intervals_01/test.desc
@@ -6,7 +6,7 @@ main.c
 ^\[main.assertion.1\] line 7 assertion i\s*>=\s*10: SUCCESS$
 ^\[main.assertion.2\] line 10 assertion i\s*!=\s*30: SUCCESS$
 ^\[main.assertion.3\] line 13 assertion i\s*!=\s*15: UNKNOWN$
-^\[main.assertion.4\] line 16 assertion 0: SUCCESS$
+^\[main.assertion.4\] line 16 assertion 0: SUCCESS \(unreachable\)$
 ^\[main.assertion.5\] line 19 assertion j\s*>=\s*10: SUCCESS$
 ^\[main.assertion.6\] line 22 assertion i\s*>=\s*j: UNKNOWN$
 ^\[main.assertion.7\] line 25 assertion i\s*>=\s*11: SUCCESS$
diff --git a/regression/goto-analyzer/intervals_13/test.desc b/regression/goto-analyzer/intervals_13/test.desc
@@ -6,7 +6,7 @@ main.c
 ^\[main.assertion.1\] line 7 assertion i\s*>=\s*10: SUCCESS$
 ^\[main.assertion.2\] line 10 assertion i\s*!=\s*30: SUCCESS$
 ^\[main.assertion.3\] line 13 assertion i\s*!=\s*15: UNKNOWN$
-^\[main.assertion.4\] line 16 assertion 0: SUCCESS$
+^\[main.assertion.4\] line 16 assertion 0: SUCCESS \(unreachable\)$
 ^\[main.assertion.5\] line 19 assertion j\s*>=\s*10: SUCCESS$
 ^\[main.assertion.6\] line 22 assertion i\s*>=\s*j: UNKNOWN$
 ^\[main.assertion.7\] line 25 assertion i\s*>=\s*11: SUCCESS$
diff --git a/src/analyses/ai_history.cpp b/src/analyses/ai_history.cpp
diff --git a/src/analyses/ai_history.h b/src/analyses/ai_history.h
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
diff --git a/src/goto-analyzer/static_verifier.cpp b/src/goto-analyzer/static_verifier.cpp
