Address review comments

Author: Owen Jones

src/pointer-analysis/local_value_set_analysis.cpp

@@ -419,23 +419,23 @@ void local_value_set_analysist::transform_function_stub(
     // avoid unnecessary recalculations
     const auto &rhs_expr = assignment.second;
     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)
     {
-      // The RHS expression is an external value set. Expand this to read from
-      // local objects that match it too.
-      const auto &evse = to_external_value_set(rhs_expr);
-      const std::string &evse_label =
-        id2string(to_constant_expr(evse.label()).get_value());
+      value_sett::object_mapt &rhs_values = pre_call_rhs_value_sets[rhs_expr];
+      if(rhs_expr.id() == ID_external_value_set)
+      {
+        // The RHS expression is an external value set. Expand this to read from
+        // local objects that match it too.
+        const auto &evse = to_external_value_set(rhs_expr);
+        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 "[]")
+          // declared_on_type() is nil and the field name is "[]")
           std::vector<irep_idt> key_list;
           const auto &apback = evse.access_path_entries().back();
           if(!evse.is_initializer())
@@ -454,33 +454,33 @@ void local_value_set_analysist::transform_function_stub(
             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
+          // comes from outside *this* function as well:
+          valuesets.insert(rhs_values, evse);
         }
-        // Also add the external set itself,
-        // representing the possibility that the read
-        // comes from outside *this* function as well:
-        valuesets.insert(rhs_values, evse);
-      }
-      else if(has_prefix(evse_label, PRECISE_EVS_PREFIX))
-      {
-        // Precise EVS
-        PRECONDITION(!evse.access_path_entries().empty());
-        exprt precise_access_path_expr =
-          get_expr_from_precise_evs(evse, function_symbol, fcall, ns, *this);
+        else if(has_prefix(evse_label, PRECISE_EVS_PREFIX))
+        {
+          // Precise EVS
+          PRECONDITION(!evse.access_path_entries().empty());
+          exprt precise_access_path_expr =
+            get_expr_from_precise_evs(evse, function_symbol, fcall, ns, *this);
 
-        valuesets.get_value_set(
-          precise_access_path_expr, rhs_values, ns, false);
-      }
-      else
-      {
-        // This should be an external value set of type ROOT_OBJECT. It denotes
-        // the pointers that may be stored in a particular argument or global
-        // pre-call.
-        PRECONDITION(evse.access_path_entries().empty());
-        exprt root_object_expr = get_expr_from_root_object_evs(
-          evse, function_symbol, fcall, ns, *this);
-
-        valuesets.get_value_set(root_object_expr, rhs_values, ns, false);
-      }
+          valuesets.get_value_set(
+            precise_access_path_expr, rhs_values, ns, false);
+        }
+        else
+        {
+          // This should be an external value set of type ROOT_OBJECT. It denotes
+          // the pointers that may be stored in a particular argument or global
+          // pre-call.
+          PRECONDITION(evse.access_path_entries().empty());
+          exprt root_object_expr = get_expr_from_root_object_evs(
+            evse, function_symbol, fcall, ns, *this);
+
+          valuesets.get_value_set(root_object_expr, rhs_values, ns, false);
+        }
       }
       else
       {
@@ -535,15 +535,14 @@ void local_value_set_analysist::transform_function_stub(
         lhs_fieldname.declared_on_type,
         lhs_fieldname.structured_lhs);
       irep_idt objkey = evse_entry.get_key(ns);
-      valuesets.values.insert(std::make_pair(objkey, evse_entry));
-      key_list.emplace_back(objkey);
+      valuesets.values.emplace(objkey, evse_entry);
+      key_list.push_back(std::move(objkey));
 
       // 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);
+        auto result = weak_updates.emplace(key, valuesets.values.at(key));
+        valuesets.make_union(result.first->second.object_map, rhs_values);
       }
     }
     else if(has_prefix(lhs_fieldname.base_name, PRECISE_EVS_PREFIX))
@@ -570,8 +569,7 @@ void local_value_set_analysist::transform_function_stub(
         lhs_fieldname.field_name,
         lhs_fieldname.declared_on_type,
         lhs_fieldname.structured_lhs);
-      auto insertit =
-        weak_updates.insert(std::make_pair(objkey, dynobj_entry_name));
+      auto insertit = weak_updates.emplace(objkey, dynobj_entry_name);
       valuesets.make_union(insertit.first->second.object_map, rhs_values);
     }
     else
@@ -585,19 +583,22 @@ void local_value_set_analysist::transform_function_stub(
         lhs_fieldname.field_name,
         lhs_fieldname.declared_on_type,
         lhs_fieldname.structured_lhs);
-      auto insert_it = weak_updates.insert(
-        std::make_pair(global_entry.get_key(ns), global_entry));
+      auto result =
+        weak_updates.emplace(global_entry.get_key(ns), global_entry);
 
-      valuesets.make_union(insert_it.first->second.object_map, rhs_values);
+      valuesets.make_union(result.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.
+  // Now apply the updates. We can't implement strong updates in the naive way
+  // because if two parameters alias and both get strong updates then the first
+  // one will get overwritten by the second one, whereas we want to end up with
+  // the union of the two (but pre-existing entries in the value set should be
+  // cleared).
+
+  // First go through all expressions that get strong updates and try to do a
+  // strong write of an empty object map. If a strong write is possible then
+  // this will clear the value set. Otherwise it will do nothing.
   value_sett::object_mapt empty_object_map;
   for(auto &strong_update : strong_updates)
   {
@@ -606,13 +607,16 @@ void local_value_set_analysist::transform_function_stub(
       strong_update.first, empty_object_map, ns, add_to_sets);
   }
 
+  // Now go through all strong updates doing a weak write of the desired object
+  // map
   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);
   }
 
+  // Finally do all weak updates
   valuesets.make_union(weak_updates);
 }