Generalise get_subexpression_at_offset to extract parts of members

This fixes bugs in the previous implementation and enables re-use in the
simplifier and other places.

Author: tautschnig

src/pointer-analysis/value_set_dereference.cpp

@@ -556,8 +556,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"
@@ -623,58 +625,84 @@ 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 mp_integer target_size = pointer_offset_bits(target_type_raw, ns);
+  if(target_size < 0)
+    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)
+      mp_integer m_size = pointer_offset_bits(component.type(), ns);
+      if(m_size < 0)
+        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);
-    mp_integer elem_size=pointer_offset_size(at.subtype(), ns);
-    if(elem_size==-1)
-      return nil_exprt();
-    mp_integer cellidx=offset/elem_size;
-    if(cellidx < 0 || !cellidx.is_long())
+    const array_typet &array_type = to_array_type(source_type);
+
+    // no arrays of non-byte, zero-, or unknown-sized objects
+    mp_integer sub_size = pointer_offset_bits(array_type.subtype(), ns);
+    if(sub_size <= 0 || sub_size % 8 != 0)
       return nil_exprt();
-    offset=offset%elem_size;
-    result=index_exprt(result, from_integer(cellidx, unsignedbv_typet(64)));
-    return get_subexpression_at_offset(result, offset, target_type, ns);
+
+    if(target_size <= sub_size)
+      return get_subexpression_at_offset(
+        index_exprt(expr, from_integer(offset / (sub_size / 8), index_type())),
+        offset % (sub_size / 8),
+        target_type_raw,
+        byte_extract_op,
+        ns);
+  }
+
+  if(
+    offset == 0 && pointer_offset_bits(source_type, ns) == 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();
@@ -684,11 +712,13 @@ 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();
 
-  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

@@ -83,14 +83,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