Merge pull request #2574 from tautschnig/field-sensitivity

Field sensitive goto-symex

Author: tautschnig

jbmc/regression/jbmc-generics/constant_propagation/test.desc

@@ -3,8 +3,10 @@ Test.class
 --function Test.main --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
-^\{-\d+\} symex_dynamic::dynamic_object1#3 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
-^\{-\d+\} symex_dynamic::dynamic_object1#4 = \{ \{ \{ "java::GenericSub" \}, NULL, 5 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object1#2 = \{ \{ \{ "java::GenericSub" \}, NULL, 0 \} \}$
+^\{-\d+\} symex_dynamic::dynamic_object1#2\.\.@Generic\.\[email protected]\.\.@class_identifier = "java::GenericSub"$
+^\{-\d+\} symex_dynamic::dynamic_object1#2\.\.@Generic\.\.key = NULL$
+^\{-\d+\} symex_dynamic::dynamic_object1#3\.\.@Generic\.\.x = 5$
 --
 byte_extract_(big|little)_endian
 --

jbmc/regression/jbmc-strings/ClassName/test.desc

@@ -4,5 +4,3 @@ test.class
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-\[java::test\.main:\(\)V\.assertion\.1\] line 5 assertion at file test\.java line 5 function java::test\.main:\(\)V bytecode-index 8: SUCCESS$
-\[java::test\.main:\(\)V\.assertion\.2\] line 6 assertion at file test\.java line 6 function java::test\.main:\(\)V bytecode-index 19: SUCCESS$

regression/cbmc-concurrency/norace_struct1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG pthread
+CORE pthread
 main.c
 
 ^EXIT=0$

regression/cbmc/Array_Propagation1/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+
+struct S
+{
+  int a;
+};
+
+int main()
+{
+  struct S s;
+  s.a = 1;
+
+  assert(s.a == 1);
+
+  int A[1];
+  A[0] = 1;
+
+  assert(A[0] == 1);
+
+  return 0;
+}

regression/cbmc/Array_Propagation1/test.desc

@@ -0,0 +1,13 @@
+KNOWNBUG
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
+--
+^warning: ignoring
+--
+This requires field-sensitive SSA encoding of arrays to pass entirely via
+constant propagation (changing the above condition to "1 remaining after
+simplification" would also make it pass, but this isn't the point of the test).

regression/cbmc/Struct_Propagation1/main.c

@@ -0,0 +1,34 @@
+struct S
+{
+  int v;
+  struct Inner
+  {
+    int x;
+  } inner;
+};
+
+struct S works;
+
+int main()
+{
+  struct S fails;
+
+  works.v = 2;
+  fails.v = 2;
+
+  while(works.v > 0)
+    --(works.v);
+
+  while(fails.v > 0)
+    --(fails.v);
+
+  __CPROVER_assert(works.inner.x == 0, "");
+
+  _Bool b;
+  if(b)
+  {
+    struct S s = {42, {42}};
+  }
+
+  return 0;
+}

regression/cbmc/Struct_Propagation1/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--unwind 5
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+(Starting CEGAR Loop|VCC\(s\), 0 remaining after simplification$)
+--
+^warning: ignoring

regression/cbmc/variable-access-to-constant-array/test.desc

@@ -6,5 +6,10 @@ main.c
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+--
 This test actually passes when using the SMT2 back-end, but takes 68 seconds to
 do so.
+
+Field-sensitive encoding of array accesses for an array of 2^16 elements is very
+expensive. We might consider some bounds up to which we actually do field
+expansion, or at least need to mark this test as "THOROUGH."

regression/goto-harness/nondet_elements_longer_lists/test.desc

@@ -1,8 +1,6 @@
 CORE
 main.c
 --harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function
-\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 0: SUCCESS
-\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 1: SUCCESS
 \[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$

regression/goto-harness/nondet_elements_longer_lists_global/test.desc

@@ -1,8 +1,6 @@
 CORE
 main.c
 --harness-type call-function --max-nondet-tree-depth 4 --min-null-tree-depth 1 --function test_function --nondet-globals
-\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 0: SUCCESS
-\[test_function.unwind.\d+\] line \d+ unwinding assertion loop 1: SUCCESS
 \[test_function.assertion.\d+\] line \d+ assertion list_walker->datum == \+\+i: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$

src/goto-symex/Makefile

@@ -1,5 +1,6 @@
 SRC = auto_objects.cpp \
       build_goto_trace.cpp \
+      field_sensitivity.cpp \
       goto_state.cpp \
       goto_symex.cpp \
       goto_symex_state.cpp \