Merge pull request diffblue#317 from diffblue/owen-jones-diffblue/fix-evs-bugs-and-add-subtype-and-array-tests

SEC-182: Owen jones diffblue/fix evs bugs and add subtype and array tests

Author: owen-jones-diffblue

regression/LVSA/TestEVS/Test$A.class

@@ -30,4 +30,66 @@ public void is_initializer_flag(Node parameter_node) {
     parameter_node.right = new Object();
     static_object = parameter_node.left;
   }
+
+  public class A {
+    Node node;
+  }
+
+  public class B extends A {
+    Object extra_field;
+  }
+
+  public void read_from_field_from_supertype(B b) {
+    static_object = b.node.left;
+  }
+
+  public void write_to_field_from_supertype(B b) {
+    b.node.left = new Object();
+    Node n = b.node;
+    static_object = n.left;
+  }
+
+  public void write_to_field_of_A(A a, Node node_parameter) {
+    a.node = node_parameter;
+  }
+
+  public void write_to_field_of_B_through_A(B b, Node node_parameter) {
+    write_to_field_of_A(b, node_parameter);
+    static_node = b.node;
+  }
+
+  public void read_from_array(Object object_array[]) {
+    static_object = object_array[0];
+  }
+
+  public void write_to_array(Object object_array[]) {
+    object_array[0] = new Object();
+    static_object = object_array[0];
+  }
+
+  public void read_from_field_of_object_in_array(Node node_array[]) {
+    static_object = node_array[0].left;
+  }
+
+  public void write_to_field_of_object_in_array(Node node_array[]) {
+    node_array[0].left = new Object();
+    static_object = node_array[0].left;
+  }
+
+  public class C {
+    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 write_to_array_field(C c) {
+    c.object_array[0] = new Object();
+    static_object = c.object_array[0];
+  }
 }

regression/LVSA/TestEVS/Test$B.class

@@ -60,3 +60,107 @@ def test_is_initializer_flag(tmpdir):
     value_set_expectation_2.check_number_of_values(2)
     value_set_expectation_2.check_contains_dynamic_object(is_most_recent_allocation=True)
     value_set_expectation_2.check_contains_per_field_evs(access_path=['.left'])
+
+
+def test_read_from_field_from_supertype(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('read_from_field_from_supertype')
+    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(2)
+    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'])
+
+
+def test_write_to_field_from_supertype(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('write_to_field_from_supertype')
+    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_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'])
+
+
+def test_write_to_field_of_B_through_A(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('write_to_field_of_B_through_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_root_object_evs(label_suffix='node_parameter')
+    value_set_expectation.check_contains_per_field_evs(access_path=['.node'])
+
+
+def test_read_from_array(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('read_from_array')
+    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(2)
+    value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.data', '[]'])
+
+
+def test_write_to_array(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('write_to_array')
+    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_dynamic_object()
+    value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.data', '[]'])
+
+
+def test_read_from_field_of_object_in_array(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('read_from_field_of_object_in_array')
+    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(2)
+    value_set_expectation.check_contains_per_field_evs(access_path=['.left'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.data', '[]', '.left'])
+
+
+def test_write_to_field_of_object_in_array(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('write_to_field_of_object_in_array')
+    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_dynamic_object()
+    value_set_expectation.check_contains_per_field_evs(access_path=['.left'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.data', '[]', '.left'])
+
+
+def test_read_from_array_field(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('read_from_array_field')
+    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(2)
+    value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.object_array','.data', '[]'])
+
+
+def test_write_to_array_field(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('write_to_array_field')
+    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_dynamic_object()
+    value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.object_array','.data', '[]'])
+

regression/LVSA/TestEVS/Test$C.class

@@ -168,11 +168,11 @@ static const typet &type_from_suffix(
         return static_cast<const typet&>(get_nil_irep());
       // Otherwise this is the base class.
       // Can't use the method below because it might contain periods.
-      const auto &subclass_comp=to_struct_union_type(*ret).components()[0];
-      std::string subclass_name=id2string(subclass_comp.get_name());
-      assert(has_infix(suffix, subclass_name, next_member));
-      ret=&subclass_comp.type();
-      next_member+=(subclass_name.size()+1);
+      const auto &superclass_comp = to_struct_union_type(*ret).components()[0];
+      std::string superclass_name = id2string(superclass_comp.get_name());
+      assert(has_infix(suffix, superclass_name, next_member));
+      ret = &superclass_comp.type();
+      next_member += (superclass_name.size() + 1);
       suffix_without_supertypes=suffix.substr(next_member-1);
     }
     else
@@ -252,37 +252,30 @@ void local_value_sett::get_value_set_rec(
     // if it hasn't been initialised yet, do so now.
 
     typet declared_on_type;
-    std::string suffix_without_subtype;
-    const typet &field_type=
-      type_from_suffix(
-        expr.type(),
-        suffix,
-        ns,
-        declared_on_type,
-        suffix_without_subtype);
+    std::string suffix_without_supertypes;
+    const typet &field_type = type_from_suffix(
+      expr.type(), suffix, ns, declared_on_type, suffix_without_supertypes);
     if(field_type.id()==ID_pointer)
     {
       // Temporary: keep track of whether we read from an EVS, so we can
       // ignore precise access path EVSs when applying function summaries if
       // there are any reads from EVSs.
       ++num_reads_of_field_of_external_object;
 
-      std::string access_path_suffix=
-        suffix_without_subtype == "" ?
-        "[]" :
-        suffix_without_subtype;
       const auto &extinit=to_external_value_set(expr);
 
-      access_path_entry_exprt new_entry(
-        access_path_suffix,
-        function,
-        std::to_string(location_number),
-        declared_on_type);
       // If we're reading from `EVS(A.b)` then initialize an entry for that
       // EVS containing an initializer (e.g.
       // `external_objects.A.b <- { EVS(A.b) }`.
       if(extinit.can_extend_to_imprecise())
       {
+        std::string access_path_suffix =
+          suffix_without_supertypes.empty() ? "[]" : suffix_without_supertypes;
+        access_path_entry_exprt new_entry(
+          access_path_suffix,
+          function,
+          std::to_string(location_number),
+          declared_on_type);
         /// Create external value set for the type and suffix
         external_value_set_exprt new_ext_set=extinit;
         new_ext_set.extend_access_path(
@@ -300,6 +293,12 @@ void local_value_sett::get_value_set_rec(
 
       if(extinit.can_extend_to_precise())
       {
+        std::string access_path_suffix = suffix.empty() ? "[]" : suffix;
+        access_path_entry_exprt new_entry(
+          access_path_suffix,
+          function,
+          std::to_string(location_number),
+          declared_on_type);
         /// Create external value set for the precise access path
         external_value_set_exprt new_ext_set=extinit;
         bool loop_found=new_ext_set.extend_access_path(
@@ -489,13 +488,13 @@ void local_value_sett::assign_rec(
     const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
 
     typet declared_on_type;
-    std::string suffix_without_subtype_ignored;
+    std::string suffix_without_supertypes_ignored;
     type_from_suffix(
       lhs.type(),
       suffix,
       ns,
       declared_on_type,
-      suffix_without_subtype_ignored);
+      suffix_without_supertypes_ignored);
     entryt &e = get_entry(
       entryt(identifier, suffix, declared_on_type, lhs), lhs.type(), ns);
 
@@ -512,13 +511,13 @@ void local_value_sett::assign_rec(
     std::string name=get_dynamic_object_name(dynamic_object);
 
     typet declared_on_type;
-    std::string suffix_without_subtype_ignored;
+    std::string suffix_without_supertypes_ignored;
     type_from_suffix(
       lhs.type(),
       suffix,
       ns,
       declared_on_type,
-      suffix_without_subtype_ignored);
+      suffix_without_supertypes_ignored);
 
     entryt &entry =
       get_entry(entryt(name, suffix, declared_on_type, lhs), lhs.type(), ns);
@@ -544,15 +543,9 @@ void local_value_sett::assign_rec(
     // Write through an opaque external value set.
     const auto &evsi=to_external_value_set(lhs);
     typet declared_on_type;
-    std::string suffix_without_subtype;
-    const typet &field_type=type_from_suffix(
-      lhs.type(),
-      suffix,
-      ns,
-      declared_on_type,
-      suffix_without_subtype);
-    std::string access_path_suffix=
-      suffix_without_subtype.empty() ? "[]" : suffix_without_subtype;
+    std::string suffix_without_supertypes;
+    const typet &field_type = type_from_suffix(
+      lhs.type(), suffix, ns, declared_on_type, suffix_without_supertypes);
 
     if(field_type.id()==ID_pointer)
     {
@@ -564,6 +557,8 @@ void local_value_sett::assign_rec(
 
     if(evsi.can_extend_to_imprecise())
     {
+      std::string access_path_suffix =
+        suffix_without_supertypes.empty() ? "[]" : suffix_without_supertypes;
       access_path_entry_exprt new_entry(
         access_path_suffix,
         function,
@@ -595,8 +590,9 @@ void local_value_sett::assign_rec(
 
     if(evsi.can_extend_to_precise())
     {
+      std::string access_path_suffix = suffix.empty() ? "[]" : suffix;
       access_path_entry_exprt new_entry(
-        suffix,
+        access_path_suffix,
         function,
         std::to_string(location_number),
         declared_on_type);