Minor improvements to transform_function_stub()

Replaced asserts, used `lhs_expr` and `rhs_expr` as synonyms for
`assignment.first` and `assignment.second`. Added some empty lines and
braces.

Author: Owen Jones

src/pointer-analysis/local_value_set_analysis.cpp

@@ -131,44 +131,41 @@ void local_value_set_analysist::transform_function_stub(
   const symbolt &function_symbol=ns.lookup(fname);
   const code_function_callt &fcall=to_code_function_call(l_call->code);
 
-  std::shared_ptr<lvsaa_single_external_set_summaryt> call_summary =
-    summarydb.at(fname);
+  const auto &assignments=summarydb.at(fname)->field_assignments;
 
   // The summary gives a list of inclusions, in the form symbol1 <- symbol2,
   // indicating that values reachable before the call from symbol2
-  // may now be reachable from symbol1. The assignments are simeltaneous.
+  // may now be reachable from symbol1. The assignments are simultaneous.
   // Thus start by reading all RHS values, before any changes are made:
 
   auto &valuesets=static_cast<domaint&>(state).value_set;
   std::map<exprt, local_value_sett::object_mapt> pre_call_rhs_value_sets;
-  const std::string external_objects_basename_prefix="external_objects";
+  const std::string per_field_evs_prefix="external_objects";
 
   std::set<std::pair<std::string, std::string> > lhs_written;
 
-  for(const auto &assignment : call_summary->field_assignments)
+  for(const auto &assignment : assignments)
   {
     ++nstub_assignments;
+    const auto &lhs_fieldname=assignment.first;
     const auto &rhs_expr=assignment.second;
     if(pre_call_rhs_value_sets.count(rhs_expr))
       continue;
     auto &rhs_map=pre_call_rhs_value_sets[rhs_expr];
-    if(assignment.second.id()==ID_external_value_set)
+    if(rhs_expr.id()==ID_external_value_set)
     {
-      auto &evse=to_external_value_set(assignment.second);
+      const auto &evse=to_external_value_set(rhs_expr);
+      const std::string &evse_label=
+        id2string(to_constant_expr(evse.label()).get_value());
+
       // Differentiate external-set entries that only contain
       // their initialiser from ones that have been written:
       if(!evse.is_initializer())
-      {
-        lhs_written.insert({
-          assignment.first.base_name,
-          assignment.first.field_name});
-      }
-      if(has_prefix(
-           id2string(to_constant_expr(evse.label()).get_value()),
-           "external_objects"))
+        lhs_written.insert({lhs_fieldname.base_name, lhs_fieldname.field_name});
+
+      if(has_prefix(evse_label, per_field_evs_prefix))
       {
         std::vector<local_value_sett::entryt*> rhs_entries;
-        const auto &evse=to_external_value_set(assignment.second);
         PRECONDITION(!evse.access_path_entries().empty());
         const auto &apback=evse.access_path_entries().back();
         if(!evse.is_initializer())
@@ -181,20 +178,21 @@ void local_value_set_analysist::transform_function_stub(
         }
 
         for(const auto &rhs_entry : rhs_entries)
+        {
           valuesets.make_union_adjusting_evs_types(
             rhs_map,
             rhs_entry->object_map,
             evse.type());
+        }
         // Also add the external set itself,
         // representing the possibility that the read
         // comes from outside *this* function as well:
         valuesets.insert(rhs_map, evse);
       }
       else
       {
-        // This should be an external value set assigned
-        // to initialise some global or parameter.
-        assert(evse.access_path_entries().empty());
+        // This should be an external value set of type ROOT_OBJECT.
+        PRECONDITION(evse.access_path_entries().empty());
         const symbolt &inflow_symbol=
           ns.lookup(to_constant_expr(evse.label()).get_value());
         exprt inflow_expr;
@@ -224,7 +222,7 @@ void local_value_set_analysist::transform_function_stub(
                     << to_constant_expr(evse.label()).get_value()
                     << eom;
           }
-          assert(paramidx!=(size_t)-1 && "Unknown parameter symbol?");
+          INVARIANT(paramidx!=(size_t)-1, "Unknown parameter symbol?");
           inflow_expr=fcall.arguments()[paramidx];
         }
         pointer_typet expect_type=pointer_type(evse.type());
@@ -236,49 +234,48 @@ void local_value_set_analysist::transform_function_stub(
     else
     {
       // Ordinary value set member; just add to the RHS map.
-      valuesets.insert(rhs_map, assignment.second);
-      lhs_written.insert({
-          assignment.first.base_name,
-          assignment.first.field_name});
+      valuesets.insert(rhs_map, rhs_expr);
+      lhs_written.insert({lhs_fieldname.base_name, lhs_fieldname.field_name});
     }
   }
 
   // OK, read all the RHS sets, now assign to the LHS symbols:
 
-  for(const auto &assignment : call_summary->field_assignments)
+  for(const auto &assignment : assignments)
   {
+    const auto &lhs_fieldname=assignment.first;
     const auto &rhs_values=pre_call_rhs_value_sets.at(assignment.second);
 
-    if(has_prefix(assignment.first.base_name, external_objects_basename_prefix))
+    if(has_prefix(lhs_fieldname.base_name, per_field_evs_prefix))
     {
       std::vector<local_value_sett::entryt*> lhs_entries;
       const auto find_pair=std::make_pair(
-        assignment.first.base_name,
-        assignment.first.field_name);
+        lhs_fieldname.base_name,
+        lhs_fieldname.field_name);
       if(lhs_written.count(find_pair))
         get_all_field_value_sets(
-          assignment.first.field_name,
-          assignment.first.declared_on_type,
+          lhs_fieldname.field_name,
+          lhs_fieldname.declared_on_type,
           valuesets,
           lhs_entries);
       // Also write to the external value set itself:
       local_value_sett::entryt evse_entry(
-        assignment.first.base_name,
-        assignment.first.field_name,
-        assignment.first.declared_on_type);
-      std::string objkey=assignment.first.base_name+assignment.first.field_name;
+        lhs_fieldname.base_name,
+        lhs_fieldname.field_name,
+        lhs_fieldname.declared_on_type);
+      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);
       for(auto lhs_entry : lhs_entries)
         valuesets.make_union(lhs_entry->object_map, rhs_values);
     }
-    else if(has_prefix(assignment.first.base_name, prefix_dynamic_object))
+    else if(has_prefix(lhs_fieldname.base_name, prefix_dynamic_object))
     {
-      std::string objkey=assignment.first.base_name+assignment.first.field_name;
+      std::string objkey=lhs_fieldname.base_name+lhs_fieldname.field_name;
       local_value_sett::entryt dynobj_entry_name(
-        assignment.first.base_name,
-        assignment.first.field_name,
-        assignment.first.declared_on_type);
+        lhs_fieldname.base_name,
+        lhs_fieldname.field_name,
+        lhs_fieldname.declared_on_type);
       auto insertit=
         valuesets.values.insert(std::make_pair(objkey, dynobj_entry_name));
       valuesets.make_union(insertit.first->second.object_map, rhs_values);
@@ -287,12 +284,14 @@ void local_value_set_analysist::transform_function_stub(
     {
       // The only other kind of symbols mentioned
       // in summary LHS are global variables.
-      assert(assignment.first.field_name=="");
-      const auto &global_sym=ns.lookup(assignment.first.base_name);
+      INVARIANT(
+        lhs_fieldname.field_name=="",
+        "unexpected lhs entry in call summary assignments");
+      const auto &global_sym=ns.lookup(lhs_fieldname.base_name);
       local_value_sett::entryt global_entry_name(
-        assignment.first.base_name,
+        lhs_fieldname.base_name,
         "",
-        assignment.first.declared_on_type);
+        lhs_fieldname.declared_on_type);
       auto &global_entry=
         valuesets.get_entry(global_entry_name, global_sym.type, ns);
       valuesets.make_union(global_entry.object_map, rhs_values);