Merge pull request diffblue#373 from diffblue/owen-jones-diffblue/precise-evs-function-arguments-alias

SEC-202: Enable strong writes to precise EVSs even when function arguments alias

Author: owen-jones-diffblue

cbmc/src/pointer-analysis/value_set.cpp

@@ -53,18 +53,10 @@ bool value_sett::field_sensitive(
 
 value_sett::entryt &value_sett::get_entry(
   const entryt &e,
-  const typet &type,
   const namespacet &ns)
 {
-  irep_idt index;
-
-  if(field_sensitive(e.identifier, type, ns))
-    index=id2string(e.identifier)+e.suffix;
-  else
-    index=e.identifier;
-
-  std::pair<valuest::iterator, bool> r=
-    values.insert(std::pair<idt, entryt>(index, e));
+  std::pair<valuest::iterator, bool> r =
+    values.insert(std::pair<idt, entryt>(e.get_key(ns), e));
 
   return r.first->second;
 }
@@ -1410,7 +1402,7 @@ void value_sett::assign_rec(
   if(lhs.id()==ID_symbol)
   {
     const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
-    entryt &e = get_entry(entryt(identifier, suffix, lhs), lhs.type(), ns);
+    entryt &e = get_entry(entryt(identifier, suffix, lhs), ns);
 
     if(add_to_sets)
       make_union(e.object_map, values_rhs);
@@ -1423,7 +1415,7 @@ void value_sett::assign_rec(
       to_dynamic_object_expr(lhs);
     std::string name=get_dynamic_object_name(dynamic_object);
 
-    entryt &e = get_entry(entryt(name, suffix, lhs), lhs.type(), ns);
+    entryt &e = get_entry(entryt(name, suffix, lhs), ns);
 
     make_union(e.object_map, values_rhs);
   }

cbmc/src/pointer-analysis/value_set.h

@@ -298,6 +298,14 @@ class value_sett
     {
       return !(*this==other);
     }
+
+    const irep_idt get_key(const namespacet &ns) const
+    {
+      if(field_sensitive(identifier, structured_lhs.type(), ns))
+        return id2string(identifier) + suffix;
+
+      return identifier;
+    }
   };
 
   /// Set of expressions; only used for the `get` API, not for internal
@@ -365,13 +373,8 @@ class value_sett
   ///   `object_map` (RHS value set) will be copied; otherwise it will be
   ///   ignored. Therefore it should probably be left blank and any RHS updates
   ///   conducted against the returned reference.
-  /// \param type: type of `e.identifier`, used to determine whether `e`'s
-  ///   suffix should be used to find a field-sensitive value-set or whether
-  ///   a single entry should be shared by all of symbol `e.identifier`.
   /// \param ns: global namespace
-  entryt &get_entry(
-    const entryt &e, const typet &type,
-    const namespacet &ns);
+  entryt &get_entry(const entryt &e, const namespacet &ns);
 
   /// Pretty-print this value-set
   /// \param ns: global namespace

regression/LVSA/TestEVS/test_evs.py

@@ -94,11 +94,9 @@ def test_write_to_field_of_B_through_A(tmpdir):
 
     value_set_expectation = lvsa_expectation.get_value_set_for_public_static('static_node')
 
-    value_set_expectation.check_number_of_values(3)
+    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'])
-    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):

regression/LVSA/TestPreciseAccessPaths/Test.class

@@ -138,4 +138,25 @@ public void check_using_precise_access_paths() {
     simple_function_should_export_precise_access_paths(dynamic_object_2);
     output = dynamic_object_1.object;
   }
+
+  // Helper function for check_aliasing_function_arguments()
+  public void write_to_fields_of_two_parameters(A param_a_1, A param_a_2) {
+    param_a_1.object = new Object();
+    param_a_2.object = new Object();
+  }
+
+  public void check_strong_writes_for_precise_evs(Object param_object) {
+    A a_1 = new A();
+    a_1.object = param_object;
+    A a_2 = new A();
+    a_2.object = param_object;
+    write_to_fields_of_two_parameters(a_1, a_2);
+    output = a_1.object;
+  }
+
+  public void check_aliasing_function_arguments() {
+    A a = new A();
+    write_to_fields_of_two_parameters(a, a);
+    output = a.object;
+  }
 }

regression/LVSA/TestPreciseAccessPaths/Test.java

@@ -69,10 +69,8 @@ def test_apply_set_field_of_external_object(tmpdir):
     value_set_expectation = lvsa_expectation.get_value_set_for_precise_evs(
         parameter_name='parameter_a', suffix='.object')
 
-    value_set_expectation.check_number_of_values(2)
+    value_set_expectation.check_number_of_values(1)
     value_set_expectation.check_contains_root_object_evs(label_suffix='parameter_object')
-    value_set_expectation.check_contains_precise_evs(label_suffix='parameter_a', access_path=['.object'],
-                                                     is_initializer=True)
 
 
 def test_conditionally_set_field_of_external_object(tmpdir):
@@ -95,15 +93,11 @@ def test_apply_conditionally_set_field_of_external_object(tmpdir):
     value_set_expectation = lvsa_expectation.get_value_set_for_precise_evs(
         parameter_name='parameter_a', suffix='.object')
 
-    value_set_expectation.check_number_of_values(4)
-    # Two values that existed before the function call
+    value_set_expectation.check_number_of_values(3)
     value_set_expectation.check_contains_per_field_evs(access_path=['.object'])
     value_set_expectation.check_contains_precise_evs(label_suffix='parameter_a', access_path=['.object'],
                                                      is_initializer=False)
-    # Two values that came from the function call
     value_set_expectation.check_contains_root_object_evs(label_suffix='parameter_object')
-    value_set_expectation.check_contains_precise_evs(label_suffix='parameter_a', access_path=['.object'],
-                                                     is_initializer=True)
 
 
 def test_read_field_before_writing_to_aliasable_field(tmpdir):
@@ -176,9 +170,8 @@ def test_call_function_to_allocate_new_object(tmpdir):
 
     value_set_expectation = lvsa_expectation.get_value_set_for_output()
 
-    value_set_expectation.check_number_of_values(3)
+    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()
 
 
@@ -266,3 +259,23 @@ def test_apply_array_deref(tmpdir):
     value_set_expectation.check_number_of_values(1)
     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)
+
+
+def test_check_strong_writes_for_precise_evs(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('check_strong_writes_for_precise_evs')
+    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_dynamic_object(1)
+
+
+def test_check_aliasing_function_arguments(tmpdir):
+    lvsa_driver = LvsaDriver(tmpdir, folder_name).with_test_function('check_aliasing_function_arguments')
+    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_dynamic_object(2)

regression/LVSA/TestPreciseAccessPaths/test_precise_access_paths.py

@@ -535,13 +535,12 @@ void local_value_sett::demote_most_recent_dynamic_objects(
         to_dynamic_object_expr(entry.structured_lhs);
       expr_any_allocation.set_recency(false);
 
-      // The second and third arguments to get_entry() are only used for
-      // field_sensitive(), and that will always returns true without using
-      // them because name_any_allocation starts with the prefix for a
-      // dynamic object, so we can use an empty type and namespace.
+      // The second argument to get_entry() is only used for field_sensitive(),
+      // and that will always returns true without using it because
+      // name_any_allocation starts with the prefix for a dynamic object, so
+      // we can use an empty namespace.
       entryt &entry_any_allocation = get_entry(
         entryt(name_any_allocation, entry.suffix, expr_any_allocation),
-        nil_typet(),
         namespacet(symbol_tablet()));
 
       // Add into the any-allocation dynamic-object's object_map
@@ -618,8 +617,8 @@ void local_value_sett::assign_rec(
       ns,
       declared_on_type,
       suffix_without_supertypes_ignored);
-    entryt &e = get_entry(
-      entryt(identifier, suffix, declared_on_type, lhs), lhs.type(), ns);
+    entryt &e =
+      get_entry(entryt(identifier, suffix, declared_on_type, lhs), ns);
 
     if(add_to_sets)
       make_union(e.object_map, values_rhs);
@@ -641,8 +640,7 @@ void local_value_sett::assign_rec(
       declared_on_type,
       suffix_without_supertypes_ignored);
 
-    entryt &entry =
-      get_entry(entryt(name, suffix, declared_on_type, lhs), lhs.type(), ns);
+    entryt &entry = get_entry(entryt(name, suffix, declared_on_type, lhs), ns);
 
     if(
       dynamic_object.get_recency() ==