Add class for object size expression

So that these kinds of expressions can be handled in a more type safe
fashion.

Author: thomasspriggs

src/util/pointer_expr.h

@@ -989,4 +989,39 @@ inline pointer_object_exprt &to_pointer_object_expr(exprt &expr)
   return ret;
 }
 
+/// Expression for finding the size (in bytes) of the object a pointer points
+/// to.
+class object_size_exprt : public unary_exprt
+{
+public:
+  explicit object_size_exprt(exprt pointer, typet type)
+    : unary_exprt(ID_object_size, std::move(pointer), std::move(type))
+  {
+  }
+
+  exprt &pointer()
+  {
+    return op();
+  }
+
+  const exprt &pointer() const
+  {
+    return op();
+  }
+};
+
+template <>
+inline bool can_cast_expr<object_size_exprt>(const exprt &base)
+{
+  return base.id() == ID_object_size;
+}
+
+inline void validate_expr(const object_size_exprt &value)
+{
+  validate_operands(value, 1, "Object size expression must have one operand.");
+  DATA_INVARIANT(
+    can_cast_type<pointer_typet>(value.pointer().type()),
+    "Object size expression must have pointer typed operand.");
+}
+
 #endif // CPROVER_UTIL_POINTER_EXPR_H

unit/util/pointer_expr.cpp

@@ -122,3 +122,63 @@ TEST_CASE("pointer_object_exprt", "[core][util]")
     }
   }
 }
+
+TEST_CASE("object_size_exprt", "[core][util]")
+{
+  const exprt pointer = symbol_exprt{"foo", pointer_type(void_type())};
+  const object_size_exprt object_size{pointer, size_type()};
+  SECTION("Is equivalent to free function.")
+  {
+    CHECK(::object_size(pointer) == object_size);
+  }
+  SECTION("Result type")
+  {
+    CHECK(object_size.type() == size_type());
+  }
+  SECTION("Pointer operand accessor")
+  {
+    CHECK(object_size.pointer() == pointer);
+  }
+  SECTION("Downcasting")
+  {
+    const exprt &upcast = object_size;
+    CHECK(expr_try_dynamic_cast<object_size_exprt>(upcast));
+    CHECK_FALSE(expr_try_dynamic_cast<pointer_object_exprt>(upcast));
+    SECTION("Validation")
+    {
+      SECTION("Invalid operand")
+      {
+        unary_exprt invalid_type = object_size;
+        invalid_type.op().type() = bool_typet{};
+        const cbmc_invariants_should_throwt invariants_throw;
+        REQUIRE_THROWS_MATCHES(
+          expr_try_dynamic_cast<object_size_exprt>(invalid_type),
+          invariant_failedt,
+          invariant_failure_containing(
+            "Object size expression must have pointer typed operand."));
+      }
+      SECTION("Missing operand")
+      {
+        exprt missing_operand = object_size;
+        missing_operand.operands().clear();
+        const cbmc_invariants_should_throwt invariants_throw;
+        REQUIRE_THROWS_MATCHES(
+          expr_try_dynamic_cast<object_size_exprt>(missing_operand),
+          invariant_failedt,
+          invariant_failure_containing(
+            "Object size expression must have one operand"));
+      }
+      SECTION("Too many operands")
+      {
+        exprt two_operands = object_size;
+        two_operands.operands().push_back(pointer);
+        const cbmc_invariants_should_throwt invariants_throw;
+        REQUIRE_THROWS_MATCHES(
+          expr_try_dynamic_cast<object_size_exprt>(two_operands),
+          invariant_failedt,
+          invariant_failure_containing(
+            "Object size expression must have one operand"));
+      }
+    }
+  }
+}