Merge pull request diffblue#332 from diffblue/owen-jones-diffblue/export-precise-evs-in-most-cases

Export precise access path EVSs in most cases

Author: owen-jones-diffblue

regression/LVSA/TestPreciseAccessPaths/Test.class

@@ -138,16 +138,4 @@ public void check_using_precise_access_paths() {
     simple_function_should_export_precise_access_paths(dynamic_object_2);
     output = dynamic_object_1.object;
   }
-
-  public void simple_function_should_export_imprecise_access_paths(A param_a) {
-    param_a.object = new Object();
-    static_list_node.data = null;
-  }
-
-  public void check_using_imprecise_access_paths() {
-    A dynamic_object_1 = new A();
-    A dynamic_object_2 = new A();
-    simple_function_should_export_imprecise_access_paths(dynamic_object_2);
-    output = dynamic_object_1.object;
-  }
 }

regression/LVSA/TestPreciseAccessPaths/Test.java

@@ -44,8 +44,9 @@ def test_apply_field_getter(tmpdir):
 
     value_set_expectation = lvsa_expectation.get_value_set_for_return_value()
 
-    value_set_expectation.check_number_of_values(1)
+    value_set_expectation.check_number_of_values(2)
     value_set_expectation.check_contains_per_field_evs(access_path=['.object'])
+    value_set_expectation.check_contains_precise_evs(access_path=['.a1', '.object'])
 
 
 def test_set_field_of_external_object(tmpdir):
@@ -113,21 +114,17 @@ def test_read_field_before_writing_to_aliasable_field(tmpdir):
     value_set_expectation_2.check_contains_per_field_evs(access_path=['.object'])
 
 
+@pytest.mark.xfail(strict=True)
 def test_apply_read_field_before_writing_to_aliasable_field(tmpdir):
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function(
         'apply_read_field_before_writing_to_aliasable_field')
     lvsa_expectation = lvsa_driver.run()
 
-    value_set_expectation_1 = lvsa_expectation.get_value_set_for_per_field_evs(inner_class_name='A', suffix='.object')
-
-    value_set_expectation_1.check_number_of_values(2)
-    value_set_expectation_1.check_contains_per_field_evs(access_path=['.object'], is_initializer=True)
-    value_set_expectation_1.check_contains_dynamic_object()
-
-    value_set_expectation_2 = lvsa_expectation.get_value_set_for_output()
+    value_set_expectation = lvsa_expectation.get_value_set_for_output()
 
-    value_set_expectation_2.check_number_of_values(1)
-    value_set_expectation_2.check_contains_per_field_evs(access_path=['.object'])
+    value_set_expectation.check_number_of_values(1)
+    value_set_expectation.check_contains_precise_evs(label_suffix='this', access_path=['.a2','.object'])
+    # value_set_expectation.check_contains_per_field_evs(access_path=['.object'], is_initializer=True)
 
 
 def test_read_field_after_writing_to_aliasable_field(tmpdir):
@@ -148,22 +145,18 @@ def test_read_field_after_writing_to_aliasable_field(tmpdir):
     value_set_expectation_2.check_contains_dynamic_object()
 
 
+@pytest.mark.xfail(strict=True)
 def test_apply_read_field_after_writing_to_aliasable_field(tmpdir):
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function(
         'apply_read_field_after_writing_to_aliasable_field')
     lvsa_expectation = lvsa_driver.run()
 
-    value_set_expectation_1 = lvsa_expectation.get_value_set_for_per_field_evs(inner_class_name='A', suffix='.object')
-
-    value_set_expectation_1.check_number_of_values(2)
-    value_set_expectation_1.check_contains_per_field_evs(access_path=['.object'], is_initializer=True)
-    value_set_expectation_1.check_contains_dynamic_object()
-
-    value_set_expectation_2 = lvsa_expectation.get_value_set_for_output()
+    value_set_expectation = lvsa_expectation.get_value_set_for_output()
 
-    value_set_expectation_2.check_number_of_values(2)
-    value_set_expectation_2.check_contains_per_field_evs(access_path=['.object'])
-    value_set_expectation_2.check_contains_dynamic_object()
+    value_set_expectation.check_number_of_values(2)
+    value_set_expectation.check_contains_precise_evs(label_suffix='this', access_path=['.a2', '.object'])
+    value_set_expectation.check_contains_dynamic_object()
+    # value_set_expectation.check_contains_per_field_evs(access_path=['.object'], is_initializer=True)
 
 
 def test_call_function_to_allocate_new_object(tmpdir):
@@ -178,15 +171,17 @@ def test_call_function_to_allocate_new_object(tmpdir):
     value_set_expectation.check_contains_dynamic_object()
 
 
+@pytest.mark.xfail(strict=True)
 def test_apply_call_function_to_allocate_new_object(tmpdir):
     lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('apply_call_function_to_allocate_new_object')
     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_per_field_evs(access_path=['.object'])
+    value_set_expectation.check_contains_precise_evs(label_suffix='param_A', access_path=['.object'])
     value_set_expectation.check_contains_dynamic_object()
+    # value_set_expectation.check_contains_per_field_evs(access_path=['.object'], is_initializer=True)
 
 
 def test_get_list_node(tmpdir):
@@ -208,7 +203,7 @@ def test_apply_get_list_node(tmpdir):
     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()
+    value_set_expectation.check_contains_per_field_evs(access_path=['.data'])
 
 
 def test_two_field_derefs(tmpdir):
@@ -222,14 +217,16 @@ def test_two_field_derefs(tmpdir):
     value_set_expectation.check_contains_per_field_evs(access_path=['.object'])
 
 
+@pytest.mark.xfail(strict=True)
 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()
 
     value_set_expectation.check_number_of_values(1)
-    value_set_expectation.check_contains_per_field_evs(access_path=['.object'])
+    value_set_expectation.check_contains_precise_evs(label_suffix='parameter_b', access_path=['.a', '.object'])
+    # value_set_expectation.check_contains_per_field_evs(access_path=['.object'], is_initializer=True)
 
 
 def test_array_deref(tmpdir):
@@ -243,32 +240,13 @@ def test_array_deref(tmpdir):
     value_set_expectation.check_contains_per_field_evs(access_path=['[]'])
 
 
+@pytest.mark.xfail(strict=True)
 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()
-
-    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('output')
-
-    value_set_expectation.check_number_of_values(1)
-    value_set_expectation.check_contains_null_object()
-
-
-def test_check_using_imprecise_access_paths(tmpdir):
-    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('check_using_imprecise_access_paths')
-    lvsa_expectation = lvsa_driver.run()
-
-    value_set_expectation = lvsa_expectation.get_value_set_for_public_static('output')
-
-    value_set_expectation.check_number_of_values(2)
-    value_set_expectation.check_contains_null_object()
-    value_set_expectation.check_contains_dynamic_object()
+    value_set_expectation.check_contains_precise_evs(label_suffix='object_array', access_path=['.data', '[]'])
+    # value_set_expectation.check_contains_per_field_evs(access_path=['.object'], is_initializer=True)

regression/LVSA/TestPreciseAccessPaths/test_precise_access_paths.py

@@ -248,11 +248,6 @@ void local_value_sett::get_value_set_rec(
       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;
-
       const auto &extinit = to_external_value_set(expr);
 
       // If we're reading from `EVS(A.b)` then initialize an entry for that
@@ -563,14 +558,6 @@ void local_value_sett::assign_rec(
     const typet &field_type = type_from_suffix(
       lhs.type(), suffix, ns, declared_on_type, suffix_without_supertypes);
 
-    if(field_type.id() == ID_pointer)
-    {
-      // Temporary: keep track of how many times we write to a field of an EVS,
-      // so we can ignore precise access path EVSs when applying function
-      // summaries if  there is more than one write to a field of an EVS.
-      ++num_writes_to_field_of_external_object;
-    }
-
     if(evsi.can_extend_to_imprecise())
     {
       std::string access_path_suffix =
@@ -622,11 +609,12 @@ void local_value_sett::assign_rec(
       {
         const std::string basename =
           new_ext_set.get_access_path_basename(declared_on_type);
-        std::string entryname = basename + access_path_suffix;
+        const std::string fieldname = new_ext_set.get_access_path_suffix();
+        const std::string entryname = basename + fieldname;
 
         entryt entry(
           basename,
-          access_path_suffix,
+          fieldname,
           external_value_set_exprt::get_precise_evs_irep_id(),
           new_ext_set);
 
@@ -688,13 +676,12 @@ void local_value_sett::apply_code_rec(const codet &code, const namespacet &ns)
   }
 }
 
-void local_value_sett::make_union_bookkeeping_data_structures(
+bool local_value_sett::make_union_bookkeeping_data_structures(
   const local_value_sett &other)
 {
-  num_reads_of_field_of_external_object +=
-    other.num_reads_of_field_of_external_object;
-  num_writes_to_field_of_external_object +=
-    other.num_writes_to_field_of_external_object;
-  precise_evs_curtailed_because_of_loop &=
+  bool original_value = precise_evs_curtailed_because_of_loop;
+  precise_evs_curtailed_because_of_loop =
+    precise_evs_curtailed_because_of_loop ||
     other.precise_evs_curtailed_because_of_loop;
+  return precise_evs_curtailed_because_of_loop != original_value;
 }

regression/LVSA/TestTest/.gitignore

@@ -18,8 +18,6 @@ class local_value_sett : public value_sett
 public:
   typedef value_sett baset;
 
-  mutable unsigned int num_reads_of_field_of_external_object = 0;
-  mutable unsigned int num_writes_to_field_of_external_object = 0;
   mutable bool precise_evs_curtailed_because_of_loop = false;
 
   /// Determines whether we should export precise or per_field external value
@@ -30,10 +28,7 @@ class local_value_sett : public value_sett
 #ifdef DO_NOT_USE_PRECISE_EXTERNAL_VALUE_SETS
     return false;
 #else
-    return !precise_evs_curtailed_because_of_loop &&
-           (num_reads_of_field_of_external_object +
-              num_writes_to_field_of_external_object <=
-            1);
+    return !precise_evs_curtailed_because_of_loop;
 #endif
   }
 
@@ -82,7 +77,9 @@ class local_value_sett : public value_sett
 
   /// Union data structures in this value-set besides the actual `values`
   /// with those in `other`.
-  void make_union_bookkeeping_data_structures(const local_value_sett &other);
+  /// \param other: the local_value_sett we are unioning with *this
+  /// \return true if anything changed
+  bool make_union_bookkeeping_data_structures(const local_value_sett &other);
 
 protected:
   /// Overrides `value_sett::get_value_set_rec` to (a) handle reads from

src/pointer-analysis/local_value_set.cpp

@@ -216,7 +216,7 @@ static const exprt get_expr_from_root_object(
     /// accessing a field of A then access_path_label will be
     /// ".@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".
+    /// it will have a label ending in ".data".
     DATA_INVARIANT(
       access_path_label.size() >= 2,
       "Access path label must have length at least 2");
@@ -226,14 +226,18 @@ static const exprt get_expr_from_root_object(
       DATA_INVARIANT(
         std::prev(it)->label() == ".data",
         "Access path entry '[]' must be preceded by access path entry '.data'");
+
+      const typet &array_type = to_member_expr(expr).compound().type();
+      const typet target_type = java_reference_type(
+        java_array_element_type(to_symbol_type(array_type)));
+
       expr = dereference_exprt(
         plus_exprt(
-          expr, side_effect_expr_nondett(java_int_type()), expr.type()));
+          expr, side_effect_expr_nondett(java_int_type()), target_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] == '@')
@@ -248,6 +252,8 @@ static const exprt get_expr_from_root_object(
           "Special fields @lock and @class_identifier should not be "
           "appearing in function summary");
 
+        const struct_typet &struct_type =
+          to_struct_type(ns.follow(expr.type()));
         const auto expr_components = struct_type.components();
         DATA_INVARIANT(
           !expr_components.empty(),
@@ -268,10 +274,10 @@ static const exprt get_expr_from_root_object(
         access_path_label[0] == '.',
         "the label of an access path entry is malformed");
       access_path_label = access_path_label.substr(1);
+      const struct_typet &struct_type = to_struct_type(ns.follow(expr.type()));
       auto &component = struct_type.get_component(access_path_label);
       INVARIANT(
-        component.get_name() != ID_nil,
-        "Could not find field from access path");
+        component.is_not_nil(), "Could not find field from access path");
       expr = member_exprt(expr, component);
     }
   }
@@ -464,8 +470,9 @@ void local_value_set_analysist::transform_function_stub(
 
       /// Weak write - can we do strong writes?
       bool add_to_sets = true;
-      auto demoted_rhs_values=pre_call_rhs_value_sets.at(assignment.second);
-      valuesets.demote_initializers(demoted_rhs_values);
+      const auto &rhs_expr = assignment.second;
+      auto demoted_rhs_values = pre_call_rhs_value_sets.at(assignment.second);
+      valuesets.adjust_assign_rhs_values(rhs_expr, ns, demoted_rhs_values);
       valuesets.assign_valueset(
         precise_access_path_expr, demoted_rhs_values, ns, add_to_sets);
     }

src/pointer-analysis/local_value_set.h

@@ -15,8 +15,10 @@ class local_value_set_domaint
 public:
   bool merge(const local_value_set_domaint &other, locationt to)
   {
-    value_set.make_union_bookkeeping_data_structures(other.value_set);
-    return value_set.make_union(other.value_set);
+    bool bookkeeping_data_structures_changed =
+      value_set.make_union_bookkeeping_data_structures(other.value_set);
+    bool value_set_changed = value_set.make_union(other.value_set);
+    return bookkeeping_data_structures_changed || value_set_changed;
   }
 };