Merge pull request #6715 from diffblue/address_expressions

Fixes for address expressions

Author: kroening

src/solvers/flattening/bv_pointers.cpp

@@ -539,6 +539,51 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   {
     return SUB::convert_byte_update(to_byte_update_expr(expr));
   }
+  else if(expr.id() == ID_field_address)
+  {
+    const auto &field_address_expr = to_field_address_expr(expr);
+    const typet &compound_type = ns.follow(field_address_expr.compound_type());
+
+    // recursive call
+    auto bv = convert_bitvector(field_address_expr.base());
+
+    if(compound_type.id() == ID_struct)
+    {
+      auto offset = member_offset(
+        to_struct_type(compound_type), field_address_expr.component_name(), ns);
+      CHECK_RETURN(offset.has_value());
+
+      // add offset
+      bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
+    }
+    else if(compound_type.id() == ID_union)
+    {
+      // nothing to do, all fields have offset 0
+    }
+    else
+    {
+      INVARIANT(false, "field address expressions operate on struct or union");
+    }
+
+    return bv;
+  }
+  else if(expr.id() == ID_element_address)
+  {
+    const auto &element_address_expr = to_element_address_expr(expr);
+
+    // recursive call
+    auto bv = convert_bitvector(element_address_expr.base());
+
+    // get element size
+    auto size = pointer_offset_size(element_address_expr.element_type(), ns);
+    CHECK_RETURN(size.has_value() && *size >= 0);
+
+    // add offset
+    bv = offset_arithmetic(
+      element_address_expr.type(), bv, *size, element_address_expr.index());
+
+    return bv;
+  }
 
   return conversion_failed(expr);
 }
@@ -702,51 +747,6 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     const auto &object_address_expr = to_object_address_expr(expr);
     return add_addr(object_address_expr.object_expr());
   }
-  else if(expr.id() == ID_field_address)
-  {
-    const auto &field_address_expr = to_field_address_expr(expr);
-    const typet &compound_type = ns.follow(field_address_expr.compound_type());
-
-    // recursive call
-    auto bv = convert_bitvector(field_address_expr.base());
-
-    if(compound_type.id() == ID_struct)
-    {
-      auto offset = member_offset(
-        to_struct_type(compound_type), field_address_expr.component_name(), ns);
-      CHECK_RETURN(offset.has_value());
-
-      // add offset
-      bv = offset_arithmetic(field_address_expr.type(), bv, *offset);
-    }
-    else if(compound_type.id() == ID_union)
-    {
-      // nothing to do, all fields have offset 0
-    }
-    else
-    {
-      INVARIANT(false, "field address expressions operate on struct or union");
-    }
-
-    return bv;
-  }
-  else if(expr.id() == ID_element_address)
-  {
-    const auto &element_address_expr = to_element_address_expr(expr);
-
-    // recursive call
-    auto bv = convert_bitvector(element_address_expr.base());
-
-    // get element size
-    auto size = pointer_offset_size(element_address_expr.element_type(), ns);
-    CHECK_RETURN(size.has_value() && *size >= 0);
-
-    // add offset
-    bv = offset_arithmetic(
-      element_address_expr.type(), bv, *size, element_address_expr.index());
-
-    return bv;
-  }
 
   return SUB::convert_bitvector(expr);
 }

src/util/pointer_expr.cpp

@@ -138,22 +138,22 @@ field_address_exprt::field_address_exprt(
   pointer_typet _type)
   : unary_exprt(ID_field_address, std::move(compound_ptr), std::move(_type))
 {
-  const auto &compound_ptr_type = compound_ptr.type();
-  PRECONDITION(compound_ptr_type.id() == ID_pointer);
-  const auto &compound_type = to_pointer_type(compound_ptr_type).base_type();
+  const auto &base_type = field_address_exprt::base().type();
+  PRECONDITION(base_type.id() == ID_pointer);
+  const auto &compound_type = to_pointer_type(base_type).base_type();
   PRECONDITION(
     compound_type.id() == ID_struct || compound_type.id() == ID_struct_tag ||
     compound_type.id() == ID_union || compound_type.id() == ID_union_tag);
   set(ID_component_name, component_name);
 }
 
-element_address_exprt::element_address_exprt(exprt base, exprt index)
+element_address_exprt::element_address_exprt(const exprt &base, exprt index)
   : binary_exprt(
-      std::move(base),
+      base,
       ID_element_address,
       std::move(index),
       pointer_typet(
-        to_array_type(base.type()).element_type(),
+        to_pointer_type(base.type()).base_type(),
         to_pointer_type(base.type()).get_width()))
 {
 }

src/util/pointer_expr.h

@@ -450,7 +450,7 @@ inline bool can_cast_expr<object_address_exprt>(const exprt &base)
 
 inline void validate_expr(const object_address_exprt &value)
 {
-  validate_operands(value, 1, "object_address must have one operand");
+  validate_operands(value, 0, "object_address must have zero operands");
 }
 
 /// \brief Cast an exprt to an \ref object_address_exprt
@@ -569,7 +569,7 @@ class element_address_exprt : public binary_exprt
   /// constructor for element addresses.
   /// The base address must be a pointer to an element.
   /// The index is expected to have an integer type.
-  element_address_exprt(exprt base, exprt index);
+  element_address_exprt(const exprt &base, exprt index);
 
   const pointer_typet &type() const
   {