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

@@ -13,8 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "arith_tools.h"
 #include "byte_operators.h"
 #include "c_types.h"
-#include "expr_util.h"
-#include "mathematical_types.h"
+#include "namespace.h"
 #include "pointer_offset_size.h"
 
 bool constant_exprt::value_is_zero_string() const
@@ -223,3 +222,35 @@ const exprt &object_descriptor_exprt::root_object() const
 
   return *p;
 }
+
+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());
+  DATA_CHECK(
+    vm,
+    can_cast_type<struct_union_typet>(compound_type),
+    "member must address a struct, union or compatible type");
+
+  const auto &component =
+    to_struct_union_type(compound_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,
+    base_type_eq(component.type(), member_expr.type(), ns),
+    "member expression's type must match the addressed struct or union "
+    "component");
+}

src/util/std_expr.h

@@ -3897,6 +3897,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);
 };
 
 /// \brief Cast an exprt to a \ref member_exprt
@@ -3933,7 +3948,6 @@ inline void validate_expr(const member_exprt &value)
   validate_operands(value, 1, "Extract member must have one operand");
 }
 
-
 /// \brief Evaluates to true if the operand is NaN
 class isnan_exprt:public unary_predicate_exprt
 {

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