Merge pull request diffblue#326 from diffblue/owen-jones-diffblue/fix-precise-evs-array-crash

SEC-203: Fix crash with precise array access

Author: owen-jones-diffblue

regression/LVSA/TestPreciseAccessPaths/Test$B.class

@@ -12,7 +12,6 @@ public static class A {
     Object object;
   }
 
-  // Precise access paths should work fine
   public void field_setter(A parameter_a) {
     output = parameter_a.object;
   }
@@ -24,7 +23,6 @@ public void apply_field_setter() {
     output_a = dynamic_object_a;
   }
 
-  // Precise access paths should work fine
   public Object field_getter() {
     return a1.object;
   }
@@ -33,7 +31,6 @@ public Object apply_field_getter() {
     return field_getter();
   }
 
-  // Precise access paths should work fine
   public void set_field_of_external_object(
       A parameter_a, Object parameter_object) {
     parameter_a.object = parameter_object;
@@ -44,7 +41,6 @@ public void apply_set_field_of_external_object(
     set_field_of_external_object(parameter_a, parameter_object);
   }
 
-  // Precise access paths should work fine
   public void conditionally_set_field_of_external_object(
       A parameter_a, Object parameter_object, boolean b) {
     if (b) {
@@ -58,13 +54,11 @@ public void apply_conditionally_set_field_of_external_object(
       parameter_a, parameter_object, b);
   }
 
-  // Precise access paths should work fine
   public void read_field_before_writing_to_aliasable_field() {
     output = a2.object;
     a1.object = new Object();
   }
 
-  // Precise access paths should work fine
   public void apply_read_field_before_writing_to_aliasable_field() {
     read_field_before_writing_to_aliasable_field();
   }
@@ -86,7 +80,6 @@ public void allocate_new_object(A input_A) {
       input_A.object = new Object();
     }
 
-  // Precise access paths should work fine
   public void call_function_to_allocate_new_object(A param_A) {
     allocate_new_object(param_A);
     output = param_A.object;
@@ -119,13 +112,20 @@ public static class B {
     A a;
   }
 
-  // Precise access paths should work fine
-  public void two_derefs(B parameter_b) {
+  public void two_field_derefs(B parameter_b) {
     output = parameter_b.a.object;
   }
 
-  public void apply_two_derefs(B parameter_b) {
-    two_derefs(parameter_b);
+  public void apply_two_field_derefs(B parameter_b) {
+    two_field_derefs(parameter_b);
+  }
+
+  public void array_deref(Object object_array[]) {
+    output = object_array[0];
+  }
+
+  public void apply_array_deref(Object object_array[]) {
+    array_deref(object_array);
   }
 
   public void simple_function_should_export_precise_access_paths(A param_a) {

regression/LVSA/TestPreciseAccessPaths/Test$ListNode.class

@@ -206,8 +206,8 @@ def test_apply_get_list_node(tmpdir):
     value_set_expectation.check_contains_per_field_evs()
 
 
-def test_two_derefs(tmpdir):
-    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('two_derefs')
+def test_two_field_derefs(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('two_field_derefs')
     lvsa_expectation = lvsa_driver.run()
 
     value_set_expectation = lvsa_expectation.get_value_set_for_output()
@@ -217,8 +217,8 @@ def test_two_derefs(tmpdir):
     value_set_expectation.check_contains_per_field_evs(access_path=['.object'])
 
 
-def test_apply_two_derefs(tmpdir):
-    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_two_derefs')
+def test_apply_two_field_derefs(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_two_field_derefs')
     lvsa_expectation = lvsa_driver.run()
 
     value_set_expectation = lvsa_expectation.get_value_set_for_output()
@@ -227,6 +227,27 @@ def test_apply_two_derefs(tmpdir):
     value_set_expectation.check_contains_per_field_evs(access_path=['.object'])
 
 
+def test_array_deref(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('array_deref')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_output()
+
+    value_set_expectation.check_number_of_values(2)
+    value_set_expectation.check_contains_precise_evs(access_path=['.data', '[]'])
+    value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
+
+
+def test_apply_array_deref(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_array_deref')
+    lvsa_expectation = lvsa_driver.run()
+
+    value_set_expectation = lvsa_expectation.get_value_set_for_output()
+
+    value_set_expectation.check_number_of_values(1)
+    value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
+
+
 def test_check_using_precise_access_paths(tmpdir):
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('check_using_precise_access_paths')
     lvsa_expectation = lvsa_driver.run()

regression/LVSA/TestPreciseAccessPaths/Test.class

@@ -17,6 +17,7 @@
 
 #include <pointer-analysis/dynamic_object_name.h>
 #include <util/infix.h>
+#include <java_bytecode/java_types.h>
 
 // Non-static functions are documented in the header file,
 // local_value_set_analysis.h
@@ -202,56 +203,73 @@ static const exprt get_expr_from_root_object(
   }
 
   /// Second, follow access path (if non-empty)
-  for(const auto &access_path_entry : access_path_entries)
+  for(external_value_set_exprt::access_path_entriest::const_iterator it =
+        access_path_entries.begin();
+      it != access_path_entries.end();
+      ++it)
   {
-    std::string access_path_label = id2string(access_path_entry.label());
+    std::string access_path_label = id2string(it->label());
     /// If expr is of type Z and Z <: Y <: X <: ... <: A and we are
     /// accessing a field of A then access_path_label will be
-    /// ".@Y.@X.@W. ... [email protected]_name"
+    /// ".@Y.@X.@W. ... [email protected]_name". For an array dereference, the access
+    /// path will have the label "[]", and the access path entry before
+    /// it will have the label ".data".
     DATA_INVARIANT(
       access_path_label.size() >= 2,
       "Access path label must have length at least 2");
 
-    expr=dereference_exprt(expr);
-    const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
-
-    /// First deal with any superclass identifiers
-    while(access_path_label[1] == '@')
+    if(access_path_label == "[]")
     {
       DATA_INVARIANT(
-        access_path_label[0] == '.',
-        "the label of an access path entry is malformed");
-      access_path_label = access_path_label.substr(1);
-      INVARIANT(
-        !has_prefix(access_path_label, "@lock") &&
+        std::prev(it)->label() == ".data",
+        "Access path entry '[]' must be preceded by access path entry '.data'");
+      expr = dereference_exprt(
+        plus_exprt(
+          expr, side_effect_expr_nondett(java_int_type()), expr.type()));
+    }
+    else
+    {
+      expr=dereference_exprt(expr);
+      const struct_typet &struct_type=to_struct_type(ns.follow(expr.type()));
+
+      /// First deal with any superclass identifiers
+      while(access_path_label[1]=='@')
+      {
+        DATA_INVARIANT(
+          access_path_label[0]=='.',
+          "the label of an access path entry is malformed");
+        access_path_label=access_path_label.substr(1);
+        INVARIANT(
+          !has_prefix(access_path_label, "@lock") &&
           !has_prefix(access_path_label, "@class_identifier"),
-        "Special fields @lock and @class_identifier should not be "
-        "appearing in function summary");
+          "Special fields @lock and @class_identifier should not be "
+            "appearing in function summary");
+
+        const auto expr_components=struct_type.components();
+        DATA_INVARIANT(
+          !expr_components.empty(),
+          "Cannot follow access path if expression has no components");
+        const auto &superclass_component=expr_components[0];
+        const std::string &superclass_name=
+          id2string(superclass_component.get_name());
+        DATA_INVARIANT(
+          has_prefix(access_path_label, superclass_name),
+          "Access path label starting with @ must be followed by superclass "
+            "name");
+        expr=member_exprt(expr, superclass_component);
+        access_path_label=access_path_label.substr(superclass_name.size());
+      }
 
-      const auto expr_components = struct_type.components();
+      /// Now we are just left with a field name
       DATA_INVARIANT(
-        !expr_components.empty(),
-        "Cannot follow access path if expression has no components");
-      const auto &superclass_component = expr_components[0];
-      const std::string &superclass_name =
-        id2string(superclass_component.get_name());
-      DATA_INVARIANT(
-        has_prefix(access_path_label, superclass_name),
-        "Access path label starting with @ must be followed by superclass "
-        "name");
-      expr = member_exprt(expr, superclass_component);
-      access_path_label = access_path_label.substr(superclass_name.size());
+        access_path_label[0]=='.',
+        "the label of an access path entry is malformed");
+      access_path_label=access_path_label.substr(1);
+      auto &component=struct_type.get_component(access_path_label);
+      INVARIANT(
+        component.get_name()!=ID_nil, "Could not find field from access path");
+      expr=member_exprt(expr, component);
     }
-
-    /// Now we are just left with a field name
-    DATA_INVARIANT(
-      access_path_label[0] == '.',
-      "the label of an access path entry is malformed");
-    access_path_label = access_path_label.substr(1);
-    auto &component = struct_type.get_component(access_path_label);
-    INVARIANT(
-      component.get_name() != ID_nil, "Could not find field from access path");
-    expr = member_exprt(expr, component);
   }
 
   return expr;