Use strong writes for precise EVSs when applying function summaries

Owen Jones · Owen Jones · commit a390ae04feb1 · 2018-06-19T11:13:58.000+01:00
diff --git a/regression/LVSA/TestEVS/test_evs.py b/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):
diff --git a/regression/LVSA/TestPreciseAccessPaths/test_precise_access_paths.py b/regression/LVSA/TestPreciseAccessPaths/test_precise_access_paths.py
@@ -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()
 
 
@@ -268,7 +261,6 @@ def test_apply_array_deref(tmpdir):
     # value_set_expectation.check_contains_per_field_evs(access_path=['.object'], is_initializer=True)
 
 
-@pytest.mark.xfail(strict=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()
@@ -279,7 +271,6 @@ def test_check_strong_writes_for_precise_evs(tmpdir):
     value_set_expectation.check_contains_dynamic_object(1)
 
 
-@pytest.mark.xfail(strict=True)
 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()
diff --git a/src/pointer-analysis/local_value_set_analysis.cpp b/src/pointer-analysis/local_value_set_analysis.cpp
@@ -140,13 +140,14 @@ void local_value_set_analysist::initialize(const goto_programt &fun)
 /// \param declared_on_type: if not nil, filter by LHS object type
 /// \param state: value set to search. Non-const as we will derive non-const
 ///   pointers into its internal data structures.
-/// \param [out] entrylist: extended with pointers into `state.values` for each
-///   matching entry. Note the pointers are non-const.
+/// \param [out] key_list: extended with keys in state.values for each matching
+///   entry
 static void get_all_field_value_sets(
   const std::string &fieldname,
   const typet &declared_on_type,
   local_value_sett &state,
-  std::vector<local_value_sett::entryt *> &entrylist)
+  const namespacet &ns,
+  std::vector<irep_idt> &key_list)
 {
   // Find all value sets we're currently aware of that may be affected by
   // a write to the given field:
@@ -163,7 +164,7 @@ static void get_all_field_value_sets(
       else if(entry.second.declared_on_type == declared_on_type)
         include_this = true;
       if(include_this)
-        entrylist.push_back(&entry.second);
+        key_list.push_back(entry.second.get_key(ns));
     }
   }
 }
@@ -407,12 +408,18 @@ void local_value_set_analysist::transform_function_stub(
 
   std::map<exprt, local_value_sett::object_mapt> pre_call_rhs_value_sets;
 
+  local_value_sett::valuest weak_updates;
+  std::vector<std::pair<exprt, value_sett::object_mapt>> strong_updates;
+
   for(const auto &assignment : assignments)
   {
     ++nstub_assignments;
+
+    // First evaluate the right hand side of this assignment, with caching to
+    // avoid unnecessary recalculations
     const auto &rhs_expr = assignment.second;
-    if(pre_call_rhs_value_sets.count(rhs_expr))
-      continue;
+    if(!pre_call_rhs_value_sets.count(rhs_expr))
+      {
     value_sett::object_mapt &rhs_values = pre_call_rhs_value_sets[rhs_expr];
     if(rhs_expr.id() == ID_external_value_set)
     {
@@ -422,29 +429,31 @@ void local_value_set_analysist::transform_function_stub(
       const std::string &evse_label =
         id2string(to_constant_expr(evse.label()).get_value());
 
-      if(has_prefix(evse_label, PER_FIELD_EVS_PREFIX))
-      {
-        PRECONDITION(evse.access_path_entries().size() == 1);
-
-        // This external value set denotes either all pointers stored in a
-        // particular field (e.g. TypeA.fieldb), or all arrays (in which case
-        // declared_on_type() is nil the the field name is "[]")
-        std::vector<local_value_sett::entryt *> rhs_entries;
-        const auto &apback = evse.access_path_entries().back();
-        if(!evse.is_initializer())
+        if(has_prefix(evse_label, PER_FIELD_EVS_PREFIX))
         {
-          get_all_field_value_sets(
-            id2string(apback.label()),
-            apback.declared_on_type(),
-            valuesets,
-            rhs_entries);
-        }
-
-        // Accumulate all possibly-read pointers into `rhs_values`:
-        for(const auto &rhs_entry : rhs_entries)
-        {
-          valuesets.make_union_adjusting_types(
-            rhs_values, rhs_entry->object_map, evse.type(), ns);
+          PRECONDITION(evse.access_path_entries().size() == 1);
+
+          // This external value set denotes either all pointers stored in a
+          // particular field (e.g. TypeA.fieldb), or all arrays (in which case
+          // declared_on_type() is nil the the field name is "[]")
+          std::vector<irep_idt> key_list;
+          const auto &apback = evse.access_path_entries().back();
+          if(!evse.is_initializer())
+          {
+            get_all_field_value_sets(
+              id2string(apback.label()),
+              apback.declared_on_type(),
+              valuesets,
+              ns,
+              key_list);
+          }
+
+          // Accumulate all possibly-read pointers into `rhs_values`:
+          for(const auto &key : key_list)
+          {
+            local_value_sett::entryt &entry = valuesets.values.at(key);
+            valuesets.make_union_adjusting_types(
+              rhs_values, entry.object_map, evse.type(), ns);
         }
         // Also add the external set itself,
         // representing the possibility that the read
@@ -472,37 +481,37 @@ void local_value_set_analysist::transform_function_stub(
 
         valuesets.get_value_set(root_object_expr, rhs_values, ns, false);
       }
-    }
-    else
-    {
-      // Ordinary value set member (not an external value set);
-
-      const auto rhs_num = valuesets.object_numbering.get_number(rhs_expr);
-      if(can_cast_expr<dynamic_object_exprt>(rhs_expr) && rhs_num)
-      {
-        unsigned loc_number =
-          expr_try_dynamic_cast<dynamic_object_exprt>(rhs_expr)->get_instance();
-        valuesets.demote_most_recent_dynamic_objects(loc_number);
       }
+      else
+      {
+        // Ordinary value set member (not an external value set);
+
+        const auto rhs_num = valuesets.object_numbering.get_number(rhs_expr);
+        if(can_cast_expr<dynamic_object_exprt>(rhs_expr) && rhs_num)
+        {
+          unsigned loc_number =
+            expr_try_dynamic_cast<dynamic_object_exprt>(rhs_expr)
+              ->get_instance();
+          valuesets.demote_most_recent_dynamic_objects(loc_number);
+        }
 
-      valuesets.insert(rhs_values, rhs_expr);
+        valuesets.insert(rhs_values, rhs_expr);
+      }
     }
-  }
 
-  // OK, all RHS sets have been read, now assign to the LHS symbols:
+    // Now calculate the left hand side of the assignment and store the update
+    // from the lhs to the rhs
 
-  for(const auto &assignment : assignments)
-  {
     const auto &lhs_fieldname = assignment.first;
-    const auto &rhs_expr = assignment.second;
-    const auto &rhs_values = pre_call_rhs_value_sets.at(rhs_expr);
+    const value_sett::object_mapt &rhs_values =
+      pre_call_rhs_value_sets.at(rhs_expr);
 
     if(has_prefix(lhs_fieldname.base_name, PER_FIELD_EVS_PREFIX))
     {
       // This writes to an external value set that denotes all fields with
       // a particular name and declaring type.
       // Apply the write to all matching local objects too:
-      std::vector<local_value_sett::entryt *> lhs_entries;
+      std::vector<irep_idt> key_list;
 
       const bool rhs_is_initializer_per_field_evs =
         rhs_expr.id() == ID_external_value_set &&
@@ -515,7 +524,8 @@ void local_value_set_analysist::transform_function_stub(
           lhs_fieldname.field_name,
           lhs_fieldname.declared_on_type,
           valuesets,
-          lhs_entries);
+          ns,
+          key_list);
       }
       // Also write to the external value set itself, representing writes
       // whose effects are external to this context too:
@@ -524,14 +534,17 @@ void local_value_set_analysist::transform_function_stub(
         lhs_fieldname.field_name,
         lhs_fieldname.declared_on_type,
         lhs_fieldname.structured_lhs);
-      std::string objkey = lhs_fieldname.base_name + lhs_fieldname.field_name;
-      auto insertit =
-        valuesets.values.insert(std::make_pair(objkey, evse_entry));
-      lhs_entries.push_back(&insertit.first->second);
+      irep_idt objkey = evse_entry.get_key(ns);
+      valuesets.values.insert(std::make_pair(objkey, evse_entry));
+      key_list.emplace_back(objkey);
 
-      // Apply the write to `state`:
-      for(auto lhs_entry : lhs_entries)
-        valuesets.make_union(lhs_entry->object_map, rhs_values);
+      // Store the write to `weak_updates`:
+      for(const irep_idt &key : key_list)
+      {
+        auto insert_it =
+          weak_updates.insert(std::make_pair(key, valuesets.values.at(key)));
+        valuesets.make_union(insert_it.first->second.object_map, rhs_values);
+      }
     }
     else if(has_prefix(lhs_fieldname.base_name, PRECISE_EVS_PREFIX))
     {
@@ -544,11 +557,9 @@ void local_value_set_analysist::transform_function_stub(
       exprt lhs_expr = get_expr_from_precise_evs(
         precise_evs, function_symbol, fcall, ns, *this);
 
-      // Weak write - can we do strong writes?
-      bool add_to_sets = true;
-      auto demoted_rhs_values = pre_call_rhs_value_sets.at(rhs_expr);
-      valuesets.adjust_assign_rhs_values(rhs_expr, ns, demoted_rhs_values);
-      valuesets.assign_valueset(lhs_expr, demoted_rhs_values, ns, add_to_sets);
+      strong_updates.emplace_back(lhs_expr, rhs_values);
+      valuesets.adjust_assign_rhs_values(
+        rhs_expr, ns, strong_updates.back().second);
     }
     else if(has_prefix(lhs_fieldname.base_name, prefix_dynamic_object))
     {
@@ -560,7 +571,7 @@ void local_value_set_analysist::transform_function_stub(
         lhs_fieldname.declared_on_type,
         lhs_fieldname.structured_lhs);
       auto insertit =
-        valuesets.values.insert(std::make_pair(objkey, dynobj_entry_name));
+        weak_updates.insert(std::make_pair(objkey, dynobj_entry_name));
       valuesets.make_union(insertit.first->second.object_map, rhs_values);
     }
     else
@@ -569,15 +580,40 @@ void local_value_set_analysist::transform_function_stub(
       // variables. Global variables defined in the java source cannot be
       // structs and thus will have an empty string as the field name, but
       // this is not true for synthetic global variables, such as class models.
-      local_value_sett::entryt global_entry_name(
+      local_value_sett::entryt global_entry(
         lhs_fieldname.base_name,
         lhs_fieldname.field_name,
         lhs_fieldname.declared_on_type,
         lhs_fieldname.structured_lhs);
-      auto &global_entry = valuesets.get_entry(global_entry_name, ns);
-      valuesets.make_union(global_entry.object_map, rhs_values);
+      auto insert_it = weak_updates.insert(
+        std::make_pair(global_entry.get_key(ns), global_entry));
+
+      valuesets.make_union(insert_it.first->second.object_map, rhs_values);
     }
   }
+
+  // Now apply the updates. We have to be careful that parameters might alias,
+  // so we have to deal with strong updates in a slightly roundabout way. We
+  // first write an empty object map to expr which got a strong update. If the
+  // expr is singular then this will erase the object map. Then we write the
+  // intended object map with `add_to_sets` false, so the write is weak. Then we
+  // apply the weak updates.
+  value_sett::object_mapt empty_object_map;
+  for(auto &strong_update : strong_updates)
+  {
+    const bool add_to_sets = false;
+    valuesets.assign_valueset(
+      strong_update.first, empty_object_map, ns, add_to_sets);
+  }
+
+  for(auto &strong_update : strong_updates)
+  {
+    const bool add_to_sets = true;
+    valuesets.assign_valueset(
+      strong_update.first, strong_update.second, ns, add_to_sets);
+  }
+
+  valuesets.make_union(weak_updates);
 }
 
 void local_value_set_analysist::save_summary(const goto_programt &goto_program)
