Merge pull request diffblue#274 from diffblue/owen-jones-diffblue/refactor-lvsa

Minor improvements to LVSA code

Author: smowton

cbmc/src/pointer-analysis/value_set_analysis.h

@@ -24,13 +24,13 @@ Author: Daniel Kroening, [email protected]
 
 class xmlt;
 
-template<class Value_Sett>
+template<class Value_Set_Domaint>
 class value_set_analysis_baset:
   public value_setst,
-  public static_analysist<value_set_domaint<Value_Sett> >
+  public static_analysist<Value_Set_Domaint>
 {
 public:
-  typedef value_set_domaint<Value_Sett> domaint;
+  typedef Value_Set_Domaint domaint;
   typedef static_analysist<domaint> baset;
   typedef typename baset::locationt locationt;
 
@@ -39,11 +39,11 @@ class value_set_analysis_baset:
   }
 
   // overloading
-  void initialize(const goto_programt &goto_program)
+  void initialize(const goto_programt &goto_program) override
   {
     baset::initialize(goto_program);
   }
-  void initialize(const goto_functionst &goto_functions)
+  void initialize(const goto_functionst &goto_functions) override
   {
     baset::initialize(goto_functions);
   }
@@ -105,7 +105,7 @@ class value_set_analysis_baset:
   virtual void get_values(
     locationt l,
     const exprt &expr,
-    value_setst::valuest &dest)
+    value_setst::valuest &dest) override
   {
     ((const value_sett&)(*this)[l].value_set).get_value_set(
       expr,
@@ -134,7 +134,8 @@ class value_set_analysis_baset:
   }
 };
 
-typedef value_set_analysis_baset<value_sett> value_set_analysist;
+typedef value_set_analysis_baset<value_set_domaint<value_sett> >
+  value_set_analysist;
 
 void convert(
   const goto_functionst &goto_functions,

src/pointer-analysis/local_value_set.cpp

@@ -528,3 +528,9 @@ void local_value_sett::apply_code(
     baset::apply_code(code, ns);
   }
 }
+
+void local_value_sett::make_union_bookkeeping_data_structures(
+  const local_value_sett &other)
+{
+  use_precise_evs = use_precise_evs && other.use_precise_evs;
+}

src/pointer-analysis/local_value_set.h

@@ -22,6 +22,7 @@ class local_value_sett:public value_sett
   #endif
 
   declared_on_type_mapt declared_on_types;
+  mutable bool use_precise_evs=true;
 
   void make_union_adjusting_evs_types(
     object_mapt &dest,
@@ -48,6 +49,8 @@ class local_value_sett:public value_sett
     const codet &,
     const namespacet &) override;
 
+  void make_union_bookkeeping_data_structures(const local_value_sett &other);
+
 protected:
   void get_value_set_rec(
     const exprt &expr,

src/pointer-analysis/local_value_set_analysis.cpp

@@ -66,6 +66,8 @@ void local_value_set_analysist::initialize(const goto_programt &fun)
     external_symbols.end());
 
   auto &initial_state=(*this)[fun.instructions.begin()].value_set;
+  const external_value_set_typet
+    default_mode_for_new_evs=external_value_set_typet::ROOT_OBJECT;
 
   // Now insert fresh symbols for each external symbol,
   // indicating an unknown external points-to set.
@@ -83,7 +85,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()),
-        external_value_set_typet::ROOT_OBJECT,
+        default_mode_for_new_evs,
         true);
       initial_state.insert(extsym_entry.object_map, extsym_var);
     }
@@ -129,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())
@@ -179,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;
@@ -222,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());
@@ -234,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);
@@ -285,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);
@@ -409,17 +410,20 @@ void lvsaa_single_external_set_summaryt::from_final_state(
   // by this function, and the values they may be assigned.
 
   std::vector<local_value_sett::valuest::const_iterator> to_export;
+  const std::string per_field_evs_prefix="external_objects";
 
-  for(auto it=final_state.values.begin(), itend=final_state.values.end();
-      it!=itend;
+  for(auto it=final_state.values.begin();
+      it!=final_state.values.end();
       ++it)
   {
     const auto &entry=*it;
-    const std::string prefix="external_objects";
+
     const std::string entryname=id2string(entry.first);
     bool export_this_entry=false;
-    if(has_prefix(entryname, prefix))
+    if(has_prefix(entryname, per_field_evs_prefix))
+    {
       export_this_entry=true;
+    }
     if((!export_this_entry) &&
        has_prefix(entryname, prefix_dynamic_object))
     {
@@ -482,7 +486,7 @@ void lvsaa_single_external_set_summaryt::from_final_state(
         id2string(entry.second.identifier),
         entry.second.suffix,
         entry.second.declared_on_type);
-      field_assignments.push_back(std::make_pair(thisname, *toexport));
+      field_assignments.emplace_back(thisname, *toexport);
     }
   }
 }

src/pointer-analysis/local_value_set_analysis.h

@@ -8,6 +8,7 @@
 
 #include <pointer-analysis/value_set_analysis.h>
 #include "local_value_set.h"
+#include "local_value_set_domain.h"
 #include <pointer-analysis/external_value_set_expr.h>
 #include <summaries/summary.h>
 #include <util/message.h>
@@ -59,10 +60,10 @@ class lvsaa_single_external_set_summaryt:public summaryt
 // to talk about external entities, rather than simply declare them unknown.
 
 class local_value_set_analysist
-  : public value_set_analysis_baset<local_value_sett>, public messaget
+  : public value_set_analysis_baset<local_value_set_domaint>, public messaget
 {
  public:
-  typedef value_set_analysis_baset<local_value_sett> baset;
+  typedef value_set_analysis_baset<local_value_set_domaint> baset;
   typedef cached_mapt<irep_idt, lvsaa_single_external_set_summaryt> dbt;
 
   local_value_set_analysist(

src/pointer-analysis/local_value_set_domain.h

@@ -0,0 +1,23 @@
+// Copyright 2016-2017 Diffblue Limited. All Rights Reserved.
+
+/// \file
+/// Local value-set analysis
+
+#ifndef SECURITY_SCANNER_POINTER_ANALYSIS_LOCAL_VALUE_SET_DOMAIN_H
+#define SECURITY_SCANNER_POINTER_ANALYSIS_LOCAL_VALUE_SET_DOMAIN_H
+
+#include <pointer-analysis/value_set.h>
+#include <pointer-analysis/value_set_domain.h>
+
+class local_value_set_domaint:public value_set_domaint<local_value_sett>
+{
+public:
+
+  bool merge(const local_value_set_domaint &other, locationt to)
+  {
+    value_set.make_union_bookkeeping_data_structures(other.value_set);
+    return value_set.make_union(other.value_set);
+  }
+};
+
+#endif