Export precise EVSs unless there is a loop

Note that several tests are marked xfail. This will be fixed in
SEC-226.

# Conflicts:
#	src/pointer-analysis/local_value_set.cpp

Author: Owen Jones

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 =
@@ -692,19 +679,9 @@ void local_value_sett::apply_code_rec(const codet &code, const namespacet &ns)
 bool local_value_sett::make_union_bookkeeping_data_structures(
   const local_value_sett &other)
 {
-  bool original_curtailed = precise_evs_curtailed_because_of_loop;
-  bool original_reads = num_reads_of_field_of_external_object;
-  bool original_writes = num_writes_to_field_of_external_object;
-
+  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;
-  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;
-
-  return (precise_evs_curtailed_because_of_loop != original_curtailed) ||
-         (num_reads_of_field_of_external_object != original_reads) ||
-         (num_writes_to_field_of_external_object != original_writes);
+  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
   }
 

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");