SSS: value-set-analysis adaptation

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

@@ -1064,6 +1064,53 @@ void value_sett::get_reference_set(
 
 /*******************************************************************\
 
+Function: strip_casts
+
+  Inputs: `e`: expression to strip
+          `ns`: global namespace
+          `target_type_raw`: if in the course of stripping casts we
+            end up at an expression with this type, stop stripping.
+
+ Outputs: Side-effect on `e`: remove typecasts and address-of-first-
+          struct-member expressions until either we find an underlying
+          expression of type `target_type_raw`, or we run out of
+          strippable expressions.
+
+ Purpose: Cleanly cast `e` to a given type if possible, avoiding the
+          possibility of ever-expanding towers of typecasts (either
+          explict or via taking address of first member).
+
+\*******************************************************************/
+
+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
 
   Inputs:
@@ -1208,7 +1255,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 +1545,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,16 @@ 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 +177,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 +208,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: