Merge pull request diffblue#355 from diffblue/owen-jones-diffblue/fix-lvsa-crash

SEC-238: LVSA: Fix precise access path crashes

Author: owen-jones-diffblue

cbmc/src/pointer-analysis/value_set.cpp

@@ -498,9 +498,7 @@ void value_sett::get_value_set_rec(
     get_reference_set(expr, reference_set, ns);
     const object_map_dt &object_map=reference_set.read();
 
-    if(object_map.begin()==object_map.end())
-      insert(dest, exprt(ID_unknown, original_type));
-    else
+    if(object_map.begin() != object_map.end())
     {
       for(object_map_dt::const_iterator
           it1=object_map.begin();

regression/LVSA/TestEVS/Test$A.class

@@ -4,7 +4,7 @@ public class Test {
   public static Node static_node;
   public static Object static_object;
 
-  public class Node {
+  public static class Node {
     Object left;
     Object right;
   }
@@ -31,12 +31,24 @@ public void is_initializer_flag(Node parameter_node) {
     static_object = parameter_node.left;
   }
 
-  public class A {
+  public static class A {
     Node node;
+
+    public Node get_special_node() {
+      return node;
+    }
   }
 
-  public class B extends A {
-    Object extra_field;
+  public static class B extends A {
+    Node extra_node;
+
+    public Node get_special_node() {
+      return extra_node;
+    }
+  }
+
+  public static class C extends B {
+    Object extra_object;
   }
 
   public void read_from_field_from_supertype(B b) {
@@ -58,6 +70,73 @@ public void write_to_field_of_B_through_A(B b, Node node_parameter) {
     static_node = b.node;
   }
 
+  // Do not test this function directly as it gives quite different results when
+  // using CSVSA-driven lazy loading
+  public void call_overridden_method_on_A(A a) {
+    a.node = new Node();
+    static_node = a.get_special_node();
+  }
+
+  public void apply_call_overridden_method_on_A_with_A() {
+    Node n = static_node; // workaround for SEC-209
+    A a = new A();
+    call_overridden_method_on_A(a);
+  }
+
+  public void apply_call_overridden_method_on_A_with_B() {
+    Node n = static_node; // workaround for SEC-209
+    B b = new B();
+    call_overridden_method_on_A(b);
+  }
+
+  public void apply_call_overridden_method_on_A_with_C() {
+    Node n = static_node; // workaround for SEC-209
+    C c = new C();
+    call_overridden_method_on_A(c);
+  }
+
+  public void call_overridden_method_on_B(B b) {
+    b.extra_node = new Node();
+    static_node = b.get_special_node();
+  }
+
+  public void call_overridden_method_on_C(C c) {
+    c.extra_node = new Node();
+    static_node = c.get_special_node();
+  }
+
+  public void call_overridden_method_on_C_upcast_to_A(C c) {
+    c.extra_node = new Node();
+    A a = c;
+    static_node = a.get_special_node();
+  }
+
+
+  public static void function_with_B_parameter(B b) {
+    if (b instanceof C) {
+      static_object = ((C)b).extra_object;
+    }
+  }
+
+  public void call_function_with_B_parameter_with_C_argument(C c) {
+    Object o = static_object; // workaround for SEC-209
+    Test.function_with_B_parameter(c);
+  }
+
+  public void call_function_with_B_parameter_with_A_argument_cast_to_C(A a) {
+    Object o = static_object; // workaround for SEC-209
+    if (a instanceof C) {
+      Test.function_with_B_parameter((C)a);
+    }
+  }
+
+  public void
+  apply_call_function_with_B_parameter_with_A_argument_cast_to_C_with_C(C c) {
+    Object o = static_object; // workaround for SEC-209
+    c.extra_object = new Object();
+    call_function_with_B_parameter_with_A_argument_cast_to_C(c);
+  }
+
   public void read_from_array(Object object_array[]) {
     static_object = object_array[0];
   }
@@ -76,21 +155,17 @@ public void write_to_field_of_object_in_array(Node node_array[]) {
     static_object = node_array[0].left;
   }
 
-  public class C {
+  public class P {
     Object object_array[];
   }
 
-  public class D {
-    A a_array[];
-  }
-
-  public void read_from_array_field(C c) {
-    static_object = c.object_array[0];
+  public void read_from_array_field(P p) {
+    static_object = p.object_array[0];
   }
 
-  public void write_to_array_field(C c) {
-    c.object_array[0] = new Object();
-    static_object = c.object_array[0];
+  public void write_to_array_field(P p) {
+    p.object_array[0] = new Object();
+    static_object = p.object_array[0];
   }
 
   public void function_which_sets_static_variable() {

regression/LVSA/TestEVS/Test$B.class

@@ -1,3 +1,5 @@
+import pytest
+
 from regression.LVSA.lvsa_driver import LvsaDriver, EvsType
 
 folder_name = 'TestEVS'
@@ -70,8 +72,7 @@ def test_read_from_field_from_supertype(tmpdir):
 
     value_set_expectation.check_number_of_values(2)
     value_set_expectation.check_contains_per_field_evs(access_path=['.left'])
-    value_set_expectation.check_contains_precise_evs(label_suffix='b', access_path=['[email protected]$A.node',
-                                                                                '.left'])
+    value_set_expectation.check_contains_precise_evs(label_suffix='b', access_path=['.node', '.left'])
 
 
 def test_write_to_field_from_supertype(tmpdir):
@@ -83,7 +84,8 @@ def test_write_to_field_from_supertype(tmpdir):
     value_set_expectation.check_number_of_values(3)
     value_set_expectation.check_contains_dynamic_object()
     value_set_expectation.check_contains_per_field_evs(access_path=['.left'])
-    value_set_expectation.check_contains_precise_evs(access_path=['[email protected]$A.node', '.left'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.node', '.left'],
+                                                     decl_on_types=['LVSA.TestEVS.Test$A', 'LVSA.TestEVS.Test$Node'])
 
 
 def test_write_to_field_of_B_through_A(tmpdir):
@@ -95,7 +97,114 @@ def test_write_to_field_of_B_through_A(tmpdir):
     value_set_expectation.check_number_of_values(3)
     value_set_expectation.check_contains_root_object_evs(label_suffix='node_parameter')
     value_set_expectation.check_contains_per_field_evs(access_path=['.node'])
-    value_set_expectation.check_contains_precise_evs(label_suffix='b', access_path=['[email protected]$A.node'])
+    value_set_expectation.check_contains_precise_evs(label_suffix='b', access_path=['.node'],
+                                                     decl_on_types=['LVSA.TestEVS.Test$A'])
+
+
+def test_apply_call_overridden_method_on_A_with_A(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_call_overridden_method_on_A_with_A')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_node')
+
+    value_set_expectation.check_number_of_values(2)
+    value_set_expectation.check_contains_dynamic_object()
+    value_set_expectation.check_contains_root_object_evs(label_suffix='static_node')
+
+
+def test_apply_call_overridden_method_on_A_with_B(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_call_overridden_method_on_A_with_B')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_node')
+
+    # Only test for what's important as CSVSA-driven-lazy-loading changes the results
+    value_set_expectation.check_contains_null_object()
+    value_set_expectation.check_contains_root_object_evs(label_suffix='static_node')
+
+
+def test_apply_call_overridden_method_on_A_with_C(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_call_overridden_method_on_A_with_C')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_node')
+
+    # Only test for what's important as CSVSA-driven-lazy-loading changes the results
+    value_set_expectation.check_contains_null_object()
+    value_set_expectation.check_contains_root_object_evs(label_suffix='static_node')
+
+
+def test_call_overridden_method_on_B(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('call_overridden_method_on_B')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_node')
+
+    value_set_expectation.check_number_of_values(2)
+    value_set_expectation.check_contains_dynamic_object()
+    value_set_expectation.check_contains_per_field_evs(access_path=['.extra_node'])
+
+
+def test_call_overridden_method_on_C(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('call_overridden_method_on_C')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_node')
+
+    value_set_expectation.check_number_of_values(2)
+    value_set_expectation.check_contains_dynamic_object()
+    value_set_expectation.check_contains_per_field_evs(access_path=['.extra_node'])
+
+
+def test_call_overridden_method_on_C_upcast_to_A(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('call_overridden_method_on_C_upcast_to_A')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_node')
+
+    # Only test for what's important as CSVSA-driven-lazy-loading changes the results
+    value_set_expectation.check_contains_dynamic_object()
+    value_set_expectation.check_contains_per_field_evs(access_path=['.extra_node'])
+
+
+def test_call_function_with_B_parameter_with_C_argument(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('call_function_with_B_parameter_with_C_argument')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_object')
+
+    value_set_expectation.check_number_of_values(3)
+    value_set_expectation.check_contains_root_object_evs(label_suffix='static_object')
+    value_set_expectation.check_contains_precise_evs(label_suffix='c', access_path=['.extra_object'])
+    value_set_expectation.check_contains_per_field_evs(access_path=['.extra_object'], is_initializer=True)
+
+
+def test_call_function_with_B_parameter_with_A_argument_cast_to_C(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function(
+        'call_function_with_B_parameter_with_A_argument_cast_to_C')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_object')
+
+    value_set_expectation.check_number_of_values(3)
+    value_set_expectation.check_contains_root_object_evs(label_suffix='static_object')
+    value_set_expectation.check_contains_per_field_evs(access_path=['.extra_object'],
+                                                       decl_on_types=['LVSA.TestEVS.Test$C'], is_initializer=True)
+    value_set_expectation.check_contains_precise_evs(access_path=['.extra_object'],
+                                                     decl_on_types=['LVSA.TestEVS.Test$C'])
+
+
+def test_apply_call_function_with_B_parameter_with_A_argument_cast_to_C_with_C(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function(
+        'apply_call_function_with_B_parameter_with_A_argument_cast_to_C_with_C')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_object')
+
+    value_set_expectation.check_number_of_values(3)
+    value_set_expectation.check_contains_root_object_evs(label_suffix='static_object')
+    value_set_expectation.check_contains_dynamic_object()
+    value_set_expectation.check_contains_per_field_evs(access_path=['.extra_object'], is_initializer=True)
 
 
 def test_read_from_array(tmpdir):
@@ -152,7 +261,7 @@ def test_read_from_array_field(tmpdir):
 
     value_set_expectation.check_number_of_values(2)
     value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
-    value_set_expectation.check_contains_precise_evs(access_path=['.object_array','.data', '[]'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.object_array', '.data', '[]'])
 
 
 def test_write_to_array_field(tmpdir):
@@ -164,7 +273,7 @@ def test_write_to_array_field(tmpdir):
     value_set_expectation.check_number_of_values(3)
     value_set_expectation.check_contains_dynamic_object()
     value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
-    value_set_expectation.check_contains_precise_evs(access_path=['.object_array','.data', '[]'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.object_array', '.data', '[]'])
 
 
 def test_apply_function_which_sets_static_variable(tmpdir):

regression/LVSA/TestEVS/Test$C.class

@@ -119,6 +119,7 @@ def test_read_field_before_writing_to_aliasable_field(tmpdir):
 
 @pytest.mark.xfail(strict=True)
 def test_apply_read_field_before_writing_to_aliasable_field(tmpdir):
+    # SEC-266: Erroneous initialiser per field EVSs
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function(
         'apply_read_field_before_writing_to_aliasable_field')
     lvsa_expectation = lvsa_driver.run()
@@ -150,6 +151,7 @@ def test_read_field_after_writing_to_aliasable_field(tmpdir):
 
 @pytest.mark.xfail(strict=True)
 def test_apply_read_field_after_writing_to_aliasable_field(tmpdir):
+    # SEC-266: Erroneous initialiser per field EVSs
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function(
         'apply_read_field_after_writing_to_aliasable_field')
     lvsa_expectation = lvsa_driver.run()
@@ -176,6 +178,7 @@ def test_call_function_to_allocate_new_object(tmpdir):
 
 @pytest.mark.xfail(strict=True)
 def test_apply_call_function_to_allocate_new_object(tmpdir):
+    # SEC-266: Erroneous initialiser per field EVSs
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_call_function_to_allocate_new_object')
     lvsa_expectation = lvsa_driver.run()
 
@@ -222,6 +225,7 @@ def test_two_field_derefs(tmpdir):
 
 @pytest.mark.xfail(strict=True)
 def test_apply_two_field_derefs(tmpdir):
+    # SEC-266: Erroneous initialiser per field EVSs
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_two_field_derefs')
     lvsa_expectation = lvsa_driver.run()
 
@@ -245,6 +249,7 @@ def test_array_deref(tmpdir):
 
 @pytest.mark.xfail(strict=True)
 def test_apply_array_deref(tmpdir):
+    # SEC-266: Erroneous initialiser per field EVSs
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_array_deref')
     lvsa_expectation = lvsa_driver.run()