Merge remote-tracking branch 'smowton-nontg/sss_templatize_vsa' into sss_temporary_merge

Author: smowton

src/pointer-analysis/Makefile

@@ -1,6 +1,6 @@
 SRC = value_set.cpp goto_program_dereference.cpp value_set_analysis.cpp \
       dereference.cpp pointer_offset_sum.cpp add_failed_symbols.cpp \
-      show_value_sets.cpp value_set_domain.cpp rewrite_index.cpp \
+      show_value_sets.cpp rewrite_index.cpp \
       value_set_analysis_fi.cpp value_set_fi.cpp value_set_domain_fi.cpp \
       value_set_analysis_fivr.cpp value_set_fivr.cpp value_set_domain_fivr.cpp \
       value_set_analysis_fivrns.cpp value_set_fivrns.cpp \

src/pointer-analysis/show_value_sets.h

@@ -10,10 +10,10 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_POINTER_ANALYSIS_SHOW_VALUE_SETS_H
 
 #include <util/ui_message.h>
+#include "value_set_analysis.h"
 
 class goto_functionst;
 class goto_programt;
-class value_set_analysist;
 
 void show_value_sets(
   ui_message_handlert::uit ui,

src/pointer-analysis/value_set.cpp

@@ -1062,6 +1062,29 @@ void value_sett::get_reference_set(
     dest.push_back(to_expr(it));
 }
 
+static void strip_casts(exprt& e, const namespacet& ns, const typet& target_type_raw)
+{
+  const auto& target_type=ns.follow(target_type_raw);
+  while(true)
+  {
+    if(e.id()==ID_typecast)
+      e=e.op0();
+    else if(e.id()==ID_member)
+    {
+      auto& mem=to_member_expr(e);
+      const auto& struct_type=to_struct_type(ns.follow(e.op0().type()));
+      if(mem.get_component_name()==struct_type.components()[0].get_name())
+        e=e.op0();
+      else
+        return;
+    }
+    else
+      return;
+    if(ns.follow(e.type())==target_type)
+      return;
+  }
+}
+
 /*******************************************************************\
 
 Function: value_sett::get_reference_set_rec
@@ -1208,7 +1231,13 @@ void value_sett::get_reference_set_rec(
         {
           // adjust type?
           if(ns.follow(struct_op.type())!=final_object_type)
+          {
+            // Avoid an infinite loop of casting by stripping typecasts
+            // and address-of-first-members first.
+            strip_casts(member_expr.op0(),ns,struct_op.type());
+            if(ns.follow(member_expr.op0().type())!=ns.follow(struct_op.type()))
             member_expr.op0().make_typecast(struct_op.type());
+          }
 
           insert(dest, member_expr, o);
         }
@@ -1492,7 +1521,6 @@ void value_sett::assign_rec(
   if(lhs.id()==ID_symbol)
   {
     const irep_idt &identifier=to_symbol_expr(lhs).get_identifier();
-
     entryt &e=get_entry(entryt(identifier, suffix), lhs.type(), ns);
 
     if(add_to_sets)

src/pointer-analysis/value_set.h

@@ -32,6 +32,7 @@ class value_sett
     const namespacet &);
 
   unsigned location_number;
+  irep_idt function;
   static object_numberingt object_numbering;
 
   typedef irep_idt idt;
@@ -101,7 +102,7 @@ class value_sett
     object_mapt object_map;
     idt identifier;
     std::string suffix;
-
+    typet declared_on_type;
     entryt()
     {
     }
@@ -111,6 +112,13 @@ class value_sett
       suffix(_suffix)
     {
     }
+
+    entryt(const idt &_identifier, const std::string &_suffix, const typet &_declared_on_type):
+      identifier(_identifier),
+      suffix(_suffix),
+      declared_on_type(_declared_on_type)
+    {
+    }
   };
 
   typedef std::set<exprt> expr_sett;
@@ -166,11 +174,11 @@ class value_sett
     const exprt &expr,
     const namespacet &ns);
 
-  void apply_code(
+  virtual void apply_code(
     const codet &code,
     const namespacet &ns);
 
-  void assign(
+  virtual void assign(
     const exprt &lhs,
     const exprt &rhs,
     const namespacet &ns,
@@ -197,37 +205,37 @@ class value_sett
     const namespacet &ns) const;
 
 protected:
-  void get_value_set_rec(
+  virtual void get_value_set_rec(
     const exprt &expr,
     object_mapt &dest,
     const std::string &suffix,
     const typet &original_type,
     const namespacet &ns) const;
 
-  void get_value_set(
+  virtual void get_value_set(
     const exprt &expr,
     object_mapt &dest,
     const namespacet &ns,
     bool is_simplified) const;
 
-  void get_reference_set(
+  virtual void get_reference_set(
     const exprt &expr,
     object_mapt &dest,
     const namespacet &ns) const
   {
     get_reference_set_rec(expr, dest, ns);
   }
 
-  void get_reference_set_rec(
+  virtual void get_reference_set_rec(
     const exprt &expr,
     object_mapt &dest,
     const namespacet &ns) const;
 
-  void dereference_rec(
+  virtual void dereference_rec(
     const exprt &src,
     exprt &dest) const;
 
-  void assign_rec(
+  virtual void assign_rec(
     const exprt &lhs,
     const object_mapt &values_rhs,
     const std::string &suffix,

src/pointer-analysis/value_set_analysis.cpp

@@ -8,114 +8,13 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/prefix.h>
 #include <util/cprover_prefix.h>
-#include <util/xml_expr.h>
-#include <util/xml.h>
 
 #include <langapi/language_util.h>
 
 #include "value_set_analysis.h"
 
 /*******************************************************************\
 
-Function: value_set_analysist::initialize
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void value_set_analysist::initialize(
-  const goto_programt &goto_program)
-{
-  baset::initialize(goto_program);
-}
-
-/*******************************************************************\
-
-Function: value_set_analysist::initialize
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void value_set_analysist::initialize(
-  const goto_functionst &goto_functions)
-{
-  baset::initialize(goto_functions);
-}
-
-/*******************************************************************\
-
-Function: value_set_analysist::convert
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void value_set_analysist::convert(
-  const goto_programt &goto_program,
-  const irep_idt &identifier,
-  xmlt &dest) const
-{
-  source_locationt previous_location;
-
-  forall_goto_program_instructions(i_it, goto_program)
-  {
-    const source_locationt &location=i_it->source_location;
-
-    if(location==previous_location)
-      continue;
-
-    if(location.is_nil() || location.get_file()==irep_idt())
-      continue;
-
-    // find value set
-    const value_sett &value_set=(*this)[i_it].value_set;
-
-    xmlt &i=dest.new_element("instruction");
-    i.new_element()=::xml(location);
-
-    for(value_sett::valuest::const_iterator
-        v_it=value_set.values.begin();
-        v_it!=value_set.values.end();
-        v_it++)
-    {
-      xmlt &var=i.new_element("variable");
-      var.new_element("identifier").data=
-        id2string(v_it->first);
-
-      #if 0
-      const value_sett::expr_sett &expr_set=
-        v_it->second.expr_set();
-
-      for(value_sett::expr_sett::const_iterator
-          e_it=expr_set.begin();
-          e_it!=expr_set.end();
-          e_it++)
-      {
-        std::string value_str=
-          from_expr(ns, identifier, *e_it);
-
-        var.new_element("value").data=
-          xmlt::escape(value_str);
-      }
-      #endif
-    }
-  }
-}
-/*******************************************************************\
-
 Function: convert
 
   Inputs:

src/pointer-analysis/value_set_analysis.h

@@ -11,32 +11,90 @@ Author: Daniel Kroening, [email protected]
 
 #define USE_DEPRECATED_STATIC_ANALYSIS_H
 #include <analyses/static_analysis.h>
+#include <util/xml_expr.h>
+#include <util/xml.h>
 
 #include "value_set_domain.h"
 #include "value_sets.h"
+#include "value_set.h"
 
 class xmlt;
 
-class value_set_analysist:
+template<class Value_Sett>
+class value_set_analysis_baset:
   public value_setst,
-  public static_analysist<value_set_domaint>
+  public static_analysist<value_set_domaint<Value_Sett> >
 {
 public:
-  explicit value_set_analysist(const namespacet &_ns):
-    static_analysist<value_set_domaint>(_ns)
+  typedef value_set_domaint<Value_Sett> domaint;
+  typedef static_analysist<domaint> baset;
+  typedef typename baset::locationt locationt;
+
+  explicit value_set_analysis_baset(const namespacet &_ns):baset(_ns)
   {
   }
 
-  typedef static_analysist<value_set_domaint> baset;
-
   // overloading
-  virtual void initialize(const goto_programt &goto_program);
-  virtual void initialize(const goto_functionst &goto_functions);
+  void initialize(const goto_programt &goto_program)
+  {
+    baset::initialize(goto_program);
+  }
+  void initialize(const goto_functionst &goto_functions)
+  {
+    baset::initialize(goto_functions);
+  }
 
   void convert(
     const goto_programt &goto_program,
     const irep_idt &identifier,
-    xmlt &dest) const;
+    xmlt &dest) const
+  {
+    source_locationt previous_location;
+
+    forall_goto_program_instructions(i_it, goto_program)
+    {
+      const source_locationt &location=i_it->source_location;
+
+      if(location==previous_location)
+        continue;
+
+      if(location.is_nil() || location.get_file()==irep_idt())
+        continue;
+
+      // find value set
+      const value_sett &value_set=(*this)[i_it].value_set;
+
+      xmlt &i=dest.new_element("instruction");
+      i.new_element()=::xml(location);
+
+      for(value_sett::valuest::const_iterator
+            v_it=value_set.values.begin();
+          v_it!=value_set.values.end();
+          v_it++)
+      {
+        xmlt &var=i.new_element("variable");
+        var.new_element("identifier").data=
+          id2string(v_it->first);
+
+#if 0
+        const value_sett::expr_sett &expr_set=
+          v_it->second.expr_set();
+
+        for(value_sett::expr_sett::const_iterator
+              e_it=expr_set.begin();
+            e_it!=expr_set.end();
+            e_it++)
+        {
+          std::string value_str=
+            from_expr(ns, identifier, *e_it);
+
+          var.new_element("value").data=
+            xmlt::escape(value_str);
+        }
+#endif
+      }
+    }
+  }
 
 public:
   // interface value_sets
@@ -45,10 +103,12 @@ class value_set_analysist:
     const exprt &expr,
     value_setst::valuest &dest)
   {
-    (*this)[l].value_set.get_value_set(expr, dest, ns);
+    (*this)[l].value_set.get_value_set(expr, dest, baset::ns);
   }
 };
 
+typedef value_set_analysis_baset<value_sett> value_set_analysist;
+
 void convert(
   const goto_functionst &goto_functions,
   const value_set_analysist &value_set_analysis,