Introducing function 'get_may_alias_values'.

Author: marek-trtik

src/pointer-analysis/value_set.cpp

@@ -10,6 +10,7 @@
 
 #include <cassert>
 #include <ostream>
+#include <algorithm>
 
 #include <util/symbol_table.h>
 #include <util/simplify_expr.h>
@@ -368,6 +369,61 @@ void value_sett::get_value_set(
   #endif
 }
 
+static exprt get_uniform_expr(const exprt &expr)
+{
+  if(expr.id()==ID_object_descriptor)
+  {
+    object_descriptor_exprt ob;
+    ob.object() = get_uniform_expr(to_object_descriptor_expr(expr).object());
+    ob.offset() = to_object_descriptor_expr(expr).offset();
+    return ob;
+  }
+  if(expr.id()==ID_external_value_set)
+  {
+    exprt copy = expr;
+    copy.set(ID_is_initializer, ID_0);
+    return copy;
+  }
+  return expr;
+}
+
+static typet get_alias_type(const exprt &expr)
+{
+  if(expr.id()==ID_object_descriptor)
+  {
+    object_descriptor_exprt ob_expr=to_object_descriptor_expr(expr);
+    if(ob_expr.offset().id()==ID_invalid || ob_expr.offset().id()==ID_unknown)
+      return pointer_type(ob_expr.object().type());
+  }
+  return pointer_type(expr.type());
+}
+
+void value_sett::get_may_alias_set(
+  const exprt &expr,
+  value_setst::valuest &dest,
+  const namespacet &ns) const
+{
+  object_mapt pointed_objects;
+  get_value_set(expr, pointed_objects, ns, false);
+  std::vector<exprt> uniform_pointed_objects;
+  for(const auto &num_obj : pointed_objects.read())
+    uniform_pointed_objects.push_back(get_uniform_expr(to_expr(num_obj)));
+
+  for(const auto &name_entry : values)
+    for(const auto &enum_eobj : name_entry.second.object_map.read())
+    {
+      if(std::find(uniform_pointed_objects.cbegin(),
+                   uniform_pointed_objects.cend(),
+                   get_uniform_expr(to_expr(enum_eobj)))!=
+         uniform_pointed_objects.cend())
+      {
+        dest.push_back(symbol_exprt(
+          name_entry.second.identifier,
+          get_alias_type(to_expr(enum_eobj))));
+      }
+    }
+}
+
 void value_sett::get_value_set(
   const exprt &expr,
   object_mapt &dest,

src/pointer-analysis/value_set.h

@@ -221,6 +221,11 @@ class value_sett
     value_setst::valuest &dest,
     const namespacet &ns) const;
 
+  void get_may_alias_set(
+    const exprt &expr,
+    value_setst::valuest &dest,
+    const namespacet &ns) const;
+
   expr_sett &get(
     const idt &identifier,
     const std::string &suffix);

src/pointer-analysis/value_set_analysis.h

@@ -113,6 +113,17 @@ class value_set_analysis_baset:
       baset::ns);
   }
 
+  virtual void get_may_alias_values(
+    locationt l,
+    const exprt &expr,
+    value_setst::valuest &dest)
+  {
+    ((const value_sett&)(*this)[l].value_set).get_may_alias_set(
+      expr,
+      dest,
+      baset::ns);
+  }
+
   /*******************************************************************\
 
   Function: value_set_analysis_baset::is_singular