Verify member expressions

This checks that the component they refer to really exists, and the expression and component's types match (are base_type_eq).

Author: smowton

src/util/std_expr.cpp

@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include "c_types.h"
 #include "expr_util.h"
 #include "mathematical_types.h"
+#include "namespace.h"
 #include "pointer_offset_size.h"
 #include "simplify_expr.h"
 
@@ -226,3 +227,43 @@ const exprt &object_descriptor_exprt::root_object() const
 
   return *p;
 }
+
+/// Check that the member expression has the right number of operands, refers
+/// to a component that exists on its underlying compound type, and uses the
+/// same type as is declared on that compound type. Throws or raises an
+/// invariant if not, according to validation mode.
+/// \param expr: expression to validate
+/// \param ns: global namespace
+/// \param vm: validation mode (see \ref exprt::validate)
+void member_exprt::validate(
+  const exprt &expr,
+  const namespacet &ns,
+  const validation_modet vm)
+{
+  check(expr, vm);
+
+  const auto &member_expr = to_member_expr(expr);
+
+  const typet &compound_type = ns.follow(member_expr.compound().type());
+  const auto *struct_union_type =
+    type_try_dynamic_cast<struct_union_typet>(compound_type);
+  DATA_CHECK(
+    vm,
+    struct_union_type != nullptr,
+    "member must address a struct, union or compatible type");
+
+  const auto &component =
+    struct_union_type->get_component(member_expr.get_component_name());
+
+  DATA_CHECK(
+    vm,
+    component.is_not_nil(),
+    "member component '" + id2string(member_expr.get_component_name()) +
+      "' must exist on addressed type");
+
+  DATA_CHECK(
+    vm,
+    component.type() == member_expr.type(),
+    "member expression's type must match the addressed struct or union "
+    "component");
+}

src/util/std_expr.h

@@ -3795,6 +3795,21 @@ class member_exprt:public unary_exprt
   {
     return op0();
   }
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm,
+      expr.operands().size() == 1,
+      "member expression must have one operand");
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT);
 };
 
 template <>

src/util/validate_expressions.cpp

@@ -37,6 +37,10 @@ void call_on_expr(const exprt &expr, Args &&... args)
   {
     CALL_ON_EXPR(ssa_exprt);
   }
+  else if(expr.id() == ID_member)
+  {
+    CALL_ON_EXPR(member_exprt);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS