Merge pull request diffblue#268 from diffblue/owen-jones-diffblue/refactor-external-value-set-types

Owen jones diffblue/refactor external value set types

Author: owen-jones-diffblue

cbmc/src/util/irep_ids.def

@@ -842,7 +842,7 @@ 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(lvsa_evs_type)
 IREP_ID_ONE(is_initializer)
 
 #undef IREP_ID_ONE

src/driver/sec_driver_parse_options.cpp

@@ -186,7 +186,7 @@ int sec_driver_parse_optionst::doit()
       }
       const auto& gf=goto_model.goto_functions.function_map.at(fname);
       local_value_set_analysist value_set_analysis(
-        ns,gf.type,fname,summarydb,LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET);
+        ns, gf.type, fname, summarydb);
       value_set_analysis.set_message_handler(get_message_handler());
       value_set_analysis(gf.body);
       value_set_analysis.output(gf.body, std::cout);
@@ -211,7 +211,10 @@ int sec_driver_parse_optionst::doit()
         if(!gf.body_available())
           continue;
         local_value_set_analysist value_set_analysis(
-          ns,gf.type,id2string(fname),summarydb,LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET);
+          ns,
+          gf.type,
+          id2string(fname),
+          summarydb);
         value_set_analysis.set_message_handler(get_message_handler());
         value_set_analysis(gf.body);
         if(cmdline.isset("show-value-sets"))

src/pointer-analysis/external_value_set_expr.h

@@ -64,10 +64,20 @@ inline const access_path_entry_exprt &to_access_path_entry(const exprt &e)
   return static_cast<const access_path_entry_exprt &>(e);
 }
 
-enum local_value_set_analysis_modet
+enum class external_value_set_typet
 {
-  LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET,
-  LOCAL_VALUE_SET_ANALYSIS_EXTERNAL_SET_PER_ACCESS_PATH
+  /// ROOT_OBJECT EVSs are what static objects and parameters point to at the
+  /// entry point of a function
+  ROOT_OBJECT,
+  /// PER_FIELD EVSs are for accessing a field of an external object. They
+  /// only keep track of the last field of the access path, and the type of
+  /// the object that that is a field of. They are always safe, even if
+  /// two external objects alias each other, but they can be quite imprecise.
+  PER_FIELD,
+  /// PRECISE EVSs are for accessing a field of an external object. They keep
+  /// track of the whole access path. At times it is not safe to use them
+  /// because of aliasing, and we must fall back to PER_FIELD EVSs.
+  PRECISE
 };
 
 // Represents an external unknown points-to set that can't be
@@ -90,21 +100,26 @@ class external_value_set_exprt:public exprt
   external_value_set_exprt(
     const typet &type,
     const constant_exprt &_label,
-    const local_value_set_analysis_modet mode,
+    const external_value_set_typet mode,
     bool is_initializer):
     exprt(ID_external_value_set, type)
   {
     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_lvsa_evs_type, 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
+  external_value_set_typet get_external_value_set_type() const
   {
-    return (local_value_set_analysis_modet)get_int(ID_lvsa_mode);
+    return static_cast<external_value_set_typet>(get_int(ID_lvsa_evs_type));
+  }
+
+  void set_external_value_set_type(external_value_set_typet evs_type)
+  {
+    set(ID_lvsa_evs_type, std::to_string(static_cast<int>(evs_type)));
   }
 
   /// At the beginning of a function, the value set for EVS("A.b") is
@@ -136,13 +151,21 @@ class external_value_set_exprt:public exprt
 
   std::string get_access_path_label() const
   {
-    if(analysis_mode()==LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET)
+    switch(get_external_value_set_type())
+    {
+    case external_value_set_typet::PER_FIELD:
       return "external_objects";
-    std::ostringstream ret;
-    ret << id2string(label().get_value());
-    for(const access_path_entry_exprt &entry : access_path_entries())
-      ret << id2string(entry.label());
-    return ret.str();
+    case external_value_set_typet::PRECISE:
+    {
+      std::ostringstream ret;
+      ret << id2string(label().get_value());
+      for(const access_path_entry_exprt &entry : access_path_entries())
+        ret << id2string(entry.label());
+      return ret.str();
+    }
+    default:
+      UNREACHABLE;
+    }
   }
 
   std::string type_to_basename(const typet &type) const
@@ -158,19 +181,29 @@ class external_value_set_exprt:public exprt
 
   std::string get_access_path_basename(const typet &declared_on_type) const
   {
-    if(analysis_mode()==LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET)
+    switch(get_external_value_set_type())
+    {
+    case external_value_set_typet::PER_FIELD:
       return "external_objects"+type_to_basename(declared_on_type);
-    assert(!access_path_entries().empty());
-    std::ostringstream ret;
-    ret << id2string(label().get_value());
-    for(
-      auto it=access_path_entries().begin();
-      it!=std::prev(access_path_entries().end());
-      ++it)
+    case external_value_set_typet::PRECISE:
     {
-      ret << id2string(it->label());
+      DATA_INVARIANT(
+        !access_path_entries().empty(),
+        "Only root object EVSs can have an empty access path");
+      std::ostringstream ret;
+      ret << id2string(label().get_value());
+      for(
+        auto it=access_path_entries().begin();
+        it!=std::prev(access_path_entries().end());
+        ++it)
+      {
+        ret << id2string(it->label());
+      }
+      return ret.str();
+    }
+    default:
+      UNREACHABLE;
     }
-    return ret.str();
   }
   bool access_path_loops() const
   {
@@ -183,9 +216,14 @@ class external_value_set_exprt:public exprt
     access_path_entries().push_back(access_path_entry_exprt::get_loop_tag());
   }
 
-  void extend_access_path(const access_path_entry_exprt &newentry)
+  void extend_access_path(
+    const access_path_entry_exprt &newentry, external_value_set_typet evs_type)
   {
-    if(analysis_mode()==LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET)
+    PRECONDITION(evs_type!=external_value_set_typet::ROOT_OBJECT);
+    set_external_value_set_type(evs_type);
+    switch(evs_type)
+    {
+    case external_value_set_typet::PER_FIELD:
     {
       // Any attempt to extend a path yields <all-externals>->fieldname
       label()=constant_exprt("external_objects", string_typet());
@@ -197,8 +235,9 @@ class external_value_set_exprt:public exprt
         access_path_entries().push_back(toadd);
       else
         access_path_entries().back()=toadd;
+      break;
     }
-    else
+    case external_value_set_typet::PRECISE:
     {
       if(access_path_loops())
       {
@@ -217,6 +256,11 @@ class external_value_set_exprt:public exprt
         }
         access_path_entries().push_back(newentry);
       }
+      break;
+    }
+    default:
+      UNREACHABLE;
+      break;
     }
   }
 

src/pointer-analysis/local_value_set.cpp

@@ -203,7 +203,8 @@ void local_value_sett::get_value_set_rec(
         std::to_string(location_number),
         declared_on_type);
       external_value_set_exprt new_ext_set=extinit;
-      new_ext_set.extend_access_path(newentry);
+      new_ext_set.extend_access_path(
+        newentry, external_value_set_typet::PER_FIELD);
       new_ext_set.type()=field_type.subtype();
 
       // TODO: figure out how to do this sort of on-demand-insert
@@ -472,7 +473,8 @@ void local_value_sett::assign_rec(
       std::to_string(location_number),
       declared_on_type);
     external_value_set_exprt new_ext_set=evsi;
-    new_ext_set.extend_access_path(newentry);
+    new_ext_set.extend_access_path(
+      newentry, external_value_set_typet::PER_FIELD);
 
     const std::string basename=
       new_ext_set.get_access_path_basename(declared_on_type);

src/pointer-analysis/local_value_set_analysis.cpp

@@ -83,7 +83,7 @@ void local_value_set_analysist::initialize(const goto_programt &fun)
       external_value_set_exprt extsym_var(
         extsym.type().subtype(),
         constant_exprt(extsym_name, string_typet()),
-        mode,
+        external_value_set_typet::ROOT_OBJECT,
         true);
       initial_state.insert(extsym_entry.object_map, extsym_var);
     }
@@ -116,9 +116,14 @@ static void get_all_field_value_sets(
   }
 }
 
-void local_value_set_analysist::transform_function_stub_single_external_set(
+
+void local_value_set_analysist::transform_function_stub(
   const irep_idt &fname, statet &state, locationt l_call, locationt l_return)
 {
+  if(!summarydb.contains(fname))
+    return;
+
+  // Execute a summary description for function fname.
   ++nstubs;
 
   const symbolt &function_symbol=ns.lookup(fname);
@@ -293,25 +298,6 @@ void local_value_set_analysist::transform_function_stub_single_external_set(
   }
 }
 
-void local_value_set_analysist::transform_function_stub(
-  const irep_idt &fname,
-  statet &state,
-  locationt l_call,
-  locationt l_return)
-{
-  // Execute a summary description for function fname.
-  if(!summarydb.contains(fname))
-    return;
-  switch(mode)
-  {
-  case LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET:
-    transform_function_stub_single_external_set(fname, state, l_call, l_return);
-    break;
-  default:
-    throw "summaries not implemented";
-  }
-}
-
 void local_value_set_analysist::save_summary(const goto_programt &goto_program)
 {
   assert(goto_program.instructions.size()!=0);

src/pointer-analysis/local_value_set_analysis.h

@@ -69,41 +69,40 @@ class local_value_set_analysist
       const namespacet& ns,
       const code_typet& ftype,
       const std::string& fname,
-      dbt& summarydb,
-      local_value_set_analysis_modet m)
+      dbt& summarydb)
     : baset(ns),
       nstubs(0),
       nstub_assignments(0),
       function_type(ftype),
       function_name(fname),
-      mode(m),
       summarydb(summarydb)
   { }
 
-  virtual void initialize(const goto_programt &goto_program);
+  virtual void initialize(const goto_programt &goto_program) override;
 
   // Use summaries for all function calls (TODO: recursion and mutual recursion)
-  virtual bool should_enter_function(const irep_idt& f) { return false; }
+  virtual bool should_enter_function(const irep_idt& f) override
+  {
+    return false;
+  }
 
-  void transform_function_stub_single_external_set(
-    const irep_idt& fname, statet& state, locationt l_call, locationt l_return);
   virtual void transform_function_stub(
-    const irep_idt& fname, statet& state, locationt l_call, locationt l_return);
+    const irep_idt& fname, statet& state, locationt l_call, locationt l_return)
+    override;
 
   void save_summary(const goto_programt&);
 
-  bool is_singular(const std::set<exprt> &);
+  virtual bool is_singular(const std::set<exprt> &) override;
 
   size_t nstubs;
   size_t nstub_assignments;
 
  protected:
   const code_typet& function_type;
   const irep_idt function_name;
-  const local_value_set_analysis_modet mode;
   dbt &summarydb;
 
-  virtual bool get_ignore_recursion() { return false; }
+  virtual bool get_ignore_recursion() override { return false; }
 };
 
 #endif

src/taint-analysis/taint_summary.cpp

@@ -124,7 +124,7 @@ static exprt transform_external_objects(const exprt& e)
       "",
       "",
       typet());
-    evs_copy.extend_access_path(new_entry);
+    evs_copy.extend_access_path(new_entry, external_value_set_typet::PER_FIELD);
     evs_copy.label()=constant_exprt("external_objects",string_typet());
     evs_copy.type()=e.type();
     evs_copy.remove("modified");
@@ -136,7 +136,7 @@ static exprt transform_external_objects(const exprt& e)
     // to be an array access, and is rewritten to (any array)
     auto evs_copy=to_external_value_set(e);
     access_path_entry_exprt new_entry("[]","","",typet());
-    evs_copy.extend_access_path(new_entry);
+    evs_copy.extend_access_path(new_entry, external_value_set_typet::PER_FIELD);
     evs_copy.label()=constant_exprt("external_objects",string_typet());
     evs_copy.type()=e.type();
     evs_copy.remove("modified");
@@ -1474,8 +1474,7 @@ void taint_algorithm_computing_summary_of_functiont::
     program->get_namespace(),
     fn_to_summarise.type,
     id2string(function_id),
-    lvsa_db,
-    LOCAL_VALUE_SET_ANALYSIS_SINGLE_EXTERNAL_SET);
+    lvsa_db);
   lvsa.set_message_handler(log->get_message_handler());
   lvsa(fn_to_summarise.body);
   // Retain this summary for use analysing callers.