Generalise get_subexpression_at_offset to extract parts of members

This enables re-use in the simplifier and other places. Adding a unit test of
get_subexpression_at_offset.

Author: tautschnig

src/pointer-analysis/value_set_dereference.cpp

@@ -468,8 +468,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     }
     else
     {
+      // try to build a member/index expression - do not use byte_extract
       exprt subexpr = get_subexpression_at_offset(
-        root_object_subexpression, o.offset(), dereference_type, ns);
+        root_object_subexpression, o.offset(), dereference_type, "", ns);
       if(subexpr.is_not_nil())
       {
         // Successfully found a member, array index, or combination thereof

src/util/pointer_offset_size.cpp

@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
 #include "pointer_offset_size.h"
 
 #include "arith_tools.h"
+#include "base_type.h"
+#include "byte_operators.h"
 #include "c_types.h"
 #include "invariant.h"
 #include "namespace.h"
@@ -672,64 +674,87 @@ exprt build_sizeof_expr(
 
 exprt get_subexpression_at_offset(
   const exprt &expr,
-  mp_integer offset,
+  const mp_integer &offset,
   const typet &target_type_raw,
+  const irep_idt &byte_extract_op,
   const namespacet &ns)
 {
-  exprt result = expr;
-  const typet &source_type=ns.follow(result.type());
-  const typet &target_type=ns.follow(target_type_raw);
+  if(offset == 0 && base_type_eq(expr.type(), target_type_raw, ns))
+  {
+    exprt result = expr;
+
+    if(expr.type() != target_type_raw)
+      result.type() = target_type_raw;
 
-  if(offset==0 && source_type==target_type)
     return result;
+  }
+
+  const typet &source_type = ns.follow(expr.type());
+  const auto target_size = pointer_offset_bits(target_type_raw, ns);
+  if(!target_size.has_value())
+    return nil_exprt();
 
   if(source_type.id()==ID_struct)
   {
-    const auto &st=to_struct_type(source_type);
-    const struct_typet::componentst &components=st.components();
-    member_offset_iterator offsets(st, ns);
-    while(offsets->first<components.size() &&
-          offsets->second!=-1 &&
-          offsets->second<=offset)
+    const struct_typet &struct_type = to_struct_type(source_type);
+
+    mp_integer m_offset_bits = 0;
+    for(const auto &component : struct_type.components())
     {
-      auto nextit=offsets;
-      ++nextit;
-      if((offsets->first+1)==components.size() || offset<nextit->second)
+      const auto m_size = pointer_offset_bits(component.type(), ns);
+      if(!m_size.has_value())
+        return nil_exprt();
+
+      if(
+        offset * 8 >= m_offset_bits && m_offset_bits % 8 == 0 &&
+        offset * 8 + *target_size <= m_offset_bits + *m_size)
       {
-        // This field might be, or might contain, the answer.
-        result=
-          member_exprt(
-            result,
-            components[offsets->first].get_name(),
-            components[offsets->first].type());
-        return
-          get_subexpression_at_offset(
-            result, offset-offsets->second, target_type, ns);
+        const member_exprt member(expr, component.get_name(), component.type());
+        return get_subexpression_at_offset(
+          member,
+          offset - m_offset_bits / 8,
+          target_type_raw,
+          byte_extract_op,
+          ns);
       }
-      ++offsets;
+
+      m_offset_bits += *m_size;
     }
-    return nil_exprt();
   }
   else if(source_type.id()==ID_array)
   {
-    // A cell of the array might be, or contain, the subexpression
-    // we're looking for.
-    const auto &at=to_array_type(source_type);
-
-    auto elem_size = pointer_offset_size(at.subtype(), ns);
-
-    if(!elem_size.has_value())
-      return nil_exprt();
+    const array_typet &array_type = to_array_type(source_type);
 
-    mp_integer cellidx = offset / (*elem_size);
+    const auto elem_size = pointer_offset_bits(array_type.subtype(), ns);
 
-    if(cellidx < 0 || !cellidx.is_long())
+    // no arrays of non-byte, zero-, or unknown-sized objects
+    if(!elem_size.has_value() || *elem_size == 0 || *elem_size % 8 != 0)
       return nil_exprt();
 
-    offset = offset % (*elem_size);
+    if(*target_size <= *elem_size)
+      return get_subexpression_at_offset(
+        index_exprt(
+          expr, from_integer(offset / (*elem_size / 8), index_type())),
+        offset % (*elem_size / 8),
+        target_type_raw,
+        byte_extract_op,
+        ns);
+  }
 
-    result=index_exprt(result, from_integer(cellidx, unsignedbv_typet(64)));
-    return get_subexpression_at_offset(result, offset, target_type, ns);
+  const auto source_size = pointer_offset_bits(source_type, ns);
+  if(
+    offset == 0 && source_size.has_value() && *source_size == *target_size &&
+    source_type.id() == ID_pointer && target_type_raw.id() == ID_pointer)
+  {
+    return typecast_exprt(expr, target_type_raw);
+  }
+  else if(!byte_extract_op.empty())
+  {
+    return byte_extract_exprt(
+      byte_extract_op,
+      expr,
+      from_integer(offset, index_type()),
+      target_type_raw);
   }
   else
     return nil_exprt();
@@ -739,12 +764,14 @@ exprt get_subexpression_at_offset(
   const exprt &expr,
   const exprt &offset,
   const typet &target_type,
+  const irep_idt &byte_extract_op,
   const namespacet &ns)
 {
   mp_integer offset_const;
 
   if(to_integer(offset, offset_const))
     return nil_exprt();
   else
-    return get_subexpression_at_offset(expr, offset_const, target_type, ns);
+    return get_subexpression_at_offset(
+      expr, offset_const, target_type, byte_extract_op, ns);
 }

src/util/pointer_offset_size.h

@@ -81,14 +81,16 @@ exprt build_sizeof_expr(
 
 exprt get_subexpression_at_offset(
   const exprt &expr,
-  mp_integer offset,
+  const mp_integer &offset,
   const typet &target_type,
+  const irep_idt &byte_extract_op,
   const namespacet &ns);
 
 exprt get_subexpression_at_offset(
   const exprt &expr,
   const exprt &offset,
   const typet &target_type,
+  const irep_idt &byte_extract_op,
   const namespacet &ns);
 
 #endif // CPROVER_UTIL_POINTER_OFFSET_SIZE_H

unit/Makefile

@@ -40,6 +40,7 @@ SRC += analyses/ai/ai.cpp \
        util/irep_sharing.cpp \
        util/message.cpp \
        util/optional.cpp \
+       util/pointer_offset_size.cpp \
        util/replace_symbol.cpp \
        util/sharing_map.cpp \
        util/sharing_node.cpp \

unit/util/pointer_offset_size.cpp

@@ -0,0 +1,122 @@
+/*******************************************************************\
+
+ Module: Unit tests of expression size/offset computation
+
+ Author: Michael Tautschnig
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+#include <util/arith_tools.h>
+#include <util/byte_operators.h>
+#include <util/c_types.h>
+#include <util/cmdline.h>
+#include <util/config.h>
+#include <util/namespace.h>
+#include <util/pointer_offset_size.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+TEST_CASE("Build subexpression to access element at offset into array")
+{
+  // this test does require a proper architecture to be set so that byte extract
+  // uses adequate endianness
+  cmdlinet cmdline;
+  config.set(cmdline);
+
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  const signedbv_typet t(32);
+
+  array_typet array_type(t, from_integer(2, size_type()));
+  symbol_exprt a("array", array_type);
+
+  {
+    const exprt result = get_subexpression_at_offset(a, 0, t, "", ns);
+    REQUIRE(result == index_exprt(a, from_integer(0, index_type())));
+  }
+
+  {
+    const exprt result = get_subexpression_at_offset(a, 32 / 8, t, "", ns);
+    REQUIRE(result == index_exprt(a, from_integer(1, index_type())));
+  }
+
+  {
+    const exprt result =
+      get_subexpression_at_offset(a, from_integer(0, size_type()), t, "", ns);
+    REQUIRE(result == index_exprt(a, from_integer(0, index_type())));
+  }
+
+  {
+    const exprt result =
+      get_subexpression_at_offset(a, size_of_expr(t, ns), t, "", ns);
+    REQUIRE(result == index_exprt(a, from_integer(1, index_type())));
+  }
+
+  {
+    const signedbv_typet small_t(8);
+    const exprt result =
+      get_subexpression_at_offset(a, 1, small_t, byte_extract_id(), ns);
+    REQUIRE(
+      result == byte_extract_exprt(
+                  byte_extract_id(),
+                  index_exprt(a, from_integer(0, index_type())),
+                  from_integer(1, index_type()),
+                  small_t));
+  }
+}
+
+TEST_CASE("Build subexpression to access element at offset into struct")
+{
+  // this test does require a proper architecture to be set so that byte extract
+  // uses adequate endianness
+  cmdlinet cmdline;
+  config.set(cmdline);
+
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  const signedbv_typet t(32);
+
+  struct_typet st;
+  st.components().emplace_back("foo", t);
+  st.components().emplace_back("bar", t);
+
+  symbol_exprt s("struct", st);
+
+  {
+    const exprt result = get_subexpression_at_offset(s, 0, t, "", ns);
+    REQUIRE(result == member_exprt(s, "foo", t));
+  }
+
+  {
+    const exprt result = get_subexpression_at_offset(s, 32 / 8, t, "", ns);
+    REQUIRE(result == member_exprt(s, "bar", t));
+  }
+
+  {
+    const exprt result =
+      get_subexpression_at_offset(s, from_integer(0, size_type()), t, "", ns);
+    REQUIRE(result == member_exprt(s, "foo", t));
+  }
+
+  {
+    const exprt result =
+      get_subexpression_at_offset(s, size_of_expr(t, ns), t, "", ns);
+    REQUIRE(result == member_exprt(s, "bar", t));
+  }
+
+  {
+    const signedbv_typet small_t(8);
+    const exprt result =
+      get_subexpression_at_offset(s, 1, small_t, byte_extract_id(), ns);
+    REQUIRE(
+      result == byte_extract_exprt(
+                  byte_extract_id(),
+                  member_exprt(s, "foo", t),
+                  from_integer(1, index_type()),
+                  small_t));
+  }
+}