Merge pull request diffblue#260 from diffblue/owen/evs-changes

SEC-105 Cleanup LVSA code (nothing functional)

cbmc/src/util/irep_ids.def

@@ -842,6 +842,8 @@ IREP_ID_TWO(generic_types, #generic_types)
 IREP_ID_TWO(type_variables, #type_variables)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
+IREP_ID_ONE(lvsa_mode)
+IREP_ID_ONE(is_initializer)
 
 #undef IREP_ID_ONE
 #undef IREP_ID_TWO

src/pointer-analysis/evs_pretty_printer.cpp

@@ -21,7 +21,7 @@ std::string evs_pretty_printert::convert(const exprt &src)
       result << top_pretty_printer->convert(*it);
     }
     result << ")";
-    if(src.get_bool("is_initializer"))
+    if(src.get_bool(ID_is_initializer))
       result << "<is-initializer>";
     result << " ["
            << top_pretty_printer->convert(src.type())

src/pointer-analysis/external_value_set_expr.h

@@ -81,8 +81,10 @@ class external_value_set_exprt:public exprt
     // The default-initalised version of EVS doesn't represent anything sane;
     // the caller should set label() before using an instance constructed
     // this way.
-    operands().resize(1);
-    operands()[0]=constant_exprt();
+    operands().resize(2);
+    op0()=constant_exprt();
+    /// No need to initialise op1(). op1().operands() will hold the vector of
+    /// access path entries.
   }
 
   external_value_set_exprt(
@@ -92,15 +94,17 @@ class external_value_set_exprt:public exprt
     bool is_initializer):
     exprt(ID_external_value_set, type)
   {
-    operands().resize(1);
-    operands()[0]=_label;
-    set("#lva_mode", std::to_string(static_cast<int>(mode)));
-    set("is_initializer", std::to_string(is_initializer ? 1 : 0));
+    operands().resize(2);
+    op0()=_label;
+    /// No need to initialise op1(). op1().operands() will hold the vector of
+    /// access path entries.
+    set(ID_lvsa_mode, std::to_string(static_cast<int>(mode)));
+    set(ID_is_initializer, std::to_string(is_initializer ? 1 : 0));
   }
 
   local_value_set_analysis_modet analysis_mode() const
   {
-    return (local_value_set_analysis_modet)get_int("#lva_mode");
+    return (local_value_set_analysis_modet)get_int(ID_lvsa_mode);
   }
 
   /// At the beginning of a function, the value set for EVS("A.b") is
@@ -112,38 +116,32 @@ class external_value_set_exprt:public exprt
   /// from a different A.b.
   bool is_initializer() const
   {
-    return get_bool("is_initializer");
+    return get_bool(ID_is_initializer);
   }
 
   constant_exprt &label() { return to_constant_expr(op0()); }
   const constant_exprt &label() const { return to_constant_expr(op0()); }
 
-  size_t access_path_size() const { return operands().size()-1; }
-  access_path_entry_exprt &access_path_entry(size_t index)
-  {
-    return to_access_path_entry(operands()[index+1]);
-  }
-  const access_path_entry_exprt &access_path_entry(size_t index) const
-  {
-    return to_access_path_entry(operands()[index+1]);
-  }
-  const access_path_entry_exprt &access_path_back() const
+  typedef std::vector<access_path_entry_exprt> access_path_entriest;
+
+  access_path_entriest &access_path_entries()
   {
-    assert(access_path_size()!=0);
-    return to_access_path_entry(operands().back());
+    return reinterpret_cast<access_path_entriest &>(op1().operands());
   }
-  void access_path_push_back(const access_path_entry_exprt &newentry)
+
+  const access_path_entriest &access_path_entries() const
   {
-    copy_to_operands(newentry);
+    return reinterpret_cast<const access_path_entriest &>(op1().operands());
   }
+
   std::string get_access_path_label() const
   {
     if(analysis_mode()==LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET)
       return "external_objects";
     std::ostringstream ret;
     ret << id2string(label().get_value());
-    for(size_t i=0; i!=access_path_size(); ++i)
-      ret << id2string(access_path_entry(i).label());
+    for(const access_path_entry_exprt &entry : access_path_entries())
+      ret << id2string(entry.label());
     return ret.str();
   }
 
@@ -162,26 +160,27 @@ class external_value_set_exprt:public exprt
   {
     if(analysis_mode()==LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET)
       return "external_objects"+type_to_basename(declared_on_type);
-    assert(access_path_size()!=0);
+    assert(!access_path_entries().empty());
     std::ostringstream ret;
     ret << id2string(label().get_value());
-    for(size_t i=0; i!=access_path_size()-1; ++i)
-      ret << id2string(access_path_entry(i).label());
+    for(
+      auto it=access_path_entries().begin();
+      it!=std::prev(access_path_entries().end());
+      ++it)
+    {
+      ret << id2string(it->label());
+    }
     return ret.str();
   }
   bool access_path_loops() const
   {
-    if(access_path_size()<2)
+    if(access_path_entries().size()<2)
       return false;
-    return access_path_entry(access_path_size()-2).is_loop();
+    return access_path_entries()[access_path_entries().size()-2].is_loop();
   }
   void create_access_path_loop()
   {
-    copy_to_operands(access_path_entry_exprt::get_loop_tag());
-  }
-  void replace_access_path_back(const access_path_entry_exprt &newtail)
-  {
-    operands()[operands().size()-1]=newtail;
+    access_path_entries().push_back(access_path_entry_exprt::get_loop_tag());
   }
 
   void extend_access_path(const access_path_entry_exprt &newentry)
@@ -194,29 +193,29 @@ class external_value_set_exprt:public exprt
       // In this case entries created at different
       // locations are not distinguished:
       toadd.drop_loc();
-      if(access_path_size()==0)
-        access_path_push_back(toadd);
+      if(access_path_entries().empty())
+        access_path_entries().push_back(toadd);
       else
-        replace_access_path_back(toadd);
+        access_path_entries().back()=toadd;
     }
     else
     {
       if(access_path_loops())
       {
         // Replace the existing tail field with this one.
-        replace_access_path_back(newentry);
+        access_path_entries().back()=newentry;
       }
       else
       {
-        for(size_t i=0; i!=access_path_size(); ++i)
+        for(const auto &entry : access_path_entries())
         {
-          if(access_path_entry(i).label()==newentry.label())
+          if(entry.label()==newentry.label())
           {
             create_access_path_loop();
             break;
           }
         }
-        access_path_push_back(newentry);
+        access_path_entries().push_back(newentry);
       }
     }
   }
@@ -228,7 +227,7 @@ class external_value_set_exprt:public exprt
     else
     {
       external_value_set_exprt copy=*this;
-      copy.set("is_initializer", ID_0);
+      copy.set(ID_is_initializer, ID_0);
       return copy;
     }
   }

src/pointer-analysis/local_value_set.cpp

@@ -39,7 +39,8 @@ void local_value_sett::make_union_adjusting_evs_types(
 std::pair<value_sett::valuest::iterator, bool>
 local_value_sett::init_external_value_set(const external_value_set_exprt &evse)
 {
-  const auto &apback=evse.access_path_back();
+  PRECONDITION(!evse.access_path_entries().empty());
+  const auto &apback=evse.access_path_entries().back();
   std::string basename=evse.get_access_path_basename(apback.declared_on_type());
   std::string access_path_suffix=id2string(apback.label());
   std::string entryname=basename+access_path_suffix;
@@ -134,9 +135,7 @@ static const typet &type_from_suffix(
   return *ret;
 }
 
-// Override value_sett to provide behaviour for external value sets:
-// Note all overridden cases must *return* if they don't want to fall through
-// to value_sett's behaviour afterwards.
+// Override value_sett to provide behaviour for external value sets
 void local_value_sett::get_value_set_rec(
   const exprt &expr,
   object_mapt &dest,
@@ -157,7 +156,6 @@ void local_value_sett::get_value_set_rec(
       get_value_set_rec(expr.op0(), tmp, suffix, original_type, ns);
       // ...except to fix up the types of external objects as they pass through:
       make_union_adjusting_evs_types(dest, tmp, expr.type().subtype());
-      return;
     }
   }
   else if(expr.id()==ID_side_effect)
@@ -170,9 +168,12 @@ void local_value_sett::get_value_set_rec(
       assert(expr.type().id()==ID_pointer && "non-pointer-typed malloc?");
       malloc_copy.set(ID_C_cxx_alloc_type, expr.type().subtype());
       baset::get_value_set_rec(malloc_copy, dest, suffix, original_type, ns);
-      return;
     }
-    // Other kinds of side-effect fall through to base class handler.
+    else
+    {
+      // For other kinds of side-effect, pass on to the base class handler.
+      baset::get_value_set_rec(expr, dest, suffix, original_type, ns);
+    }
   }
   else if(expr.id()==ID_external_value_set)
   {
@@ -218,11 +219,12 @@ void local_value_sett::get_value_set_rec(
       // Deref-of-external yields a scalar type.
       insert(dest, exprt(ID_unknown, original_type));
     }
-    return;
   }
-
-  // For everything else, use base behaviour:
-  baset::get_value_set_rec(expr, dest, suffix, original_type, ns);
+  else
+  {
+    // For everything else, pass on to the base class handler
+    baset::get_value_set_rec(expr, dest, suffix, original_type, ns);
+  }
 }
 
 /// Applying side effects needed in Recency Analysis.
@@ -511,15 +513,16 @@ void local_value_sett::apply_code(
       throw "dead expected to have symbol on lhs";
 
     assign(lhs, exprt(ID_invalid), ns, true, false);
-    return;
   }
   else if(statement=="set_may" ||
           statement=="get_may" ||
           statement=="clear_may")
   {
-    return;
+    // Do nothing
+  }
+  else
+  {
+    // Otherwise fall back to base:
+    baset::apply_code(code, ns);
   }
-
-  // Otherwise fall back to base:
-  baset::apply_code(code, ns);
 }

src/pointer-analysis/local_value_set_analysis.cpp

@@ -162,7 +162,8 @@ void local_value_set_analysist::transform_function_stub_single_external_set(
       {
         std::vector<local_value_sett::entryt*> rhs_entries;
         const auto &evse=to_external_value_set(assignment.second);
-        const auto &apback=evse.access_path_back();
+        PRECONDITION(!evse.access_path_entries().empty());
+        const auto &apback=evse.access_path_entries().back();
         if(!evse.is_initializer())
         {
           get_all_field_value_sets(
@@ -186,7 +187,7 @@ void local_value_set_analysist::transform_function_stub_single_external_set(
       {
         // This should be an external value set assigned
         // to initialise some global or parameter.
-        assert(evse.access_path_size()==0);
+        assert(evse.access_path_entries().empty());
         const symbolt &inflow_symbol=
           ns.lookup(to_constant_expr(evse.label()).get_value());
         exprt inflow_expr;

src/taint-analysis/taint_summary.cpp

@@ -92,8 +92,8 @@ void expand_external_objects(
       const auto& label=to_constant_expr(evse.label()).get_value();
       if(label=="external_objects")
       {
-        assert(evse.access_path_size()==1);
-        const auto fieldname=evse.access_path_back().label();
+        assert(evse.access_path_entries().size()==1);
+        const auto fieldname=evse.access_path_entries().back().label();
         auto findit=by_fieldname.find(fieldname);
         if(findit!=by_fieldname.end())
           new_keys.insert(
@@ -720,10 +720,10 @@ void taint_algorithm_computing_summary_of_functiont::initialise_domain(
         {
           const auto& evse=to_external_value_set(
             numbering->at(input.first));
-          if(evse.access_path_size()==1)
+          if(evse.access_path_entries().size()==1)
             numbering_map
               ->get_object_numbers_by_field()[as_string(function_id)]
-              .insert({ evse.access_path_back().label(), {} });
+              .insert({ evse.access_path_entries().back().label(), {} });
         }
       }
       for(const std::pair<taint_lvalue_numbert, taint_sett> &lvalue_taint: