member_exprt now checks type of compound operand

kroening · kroening · commit 5009854218e4 · 2022-06-20T10:45:17.000+01:00
This commit adds a precondition to the constructors of member_exprt that
enforces that the compound operand has one of the compound types.

A legacy constructor is offered to ease the transition.
diff --git a/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp b/jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp
@@ -25,9 +25,9 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
   const symbol_exprt valid_symbol_expr = symbol_exprt("id", java_int_type());
   const symbol_exprt invalid_symbol_expr = symbol_exprt(java_int_type());
   const member_exprt valid_member =
-    member_exprt(valid_symbol_expr, "member", java_int_type());
+    member_exprt::unchecked(valid_symbol_expr, "member", java_int_type());
   const member_exprt invalid_member =
-    member_exprt(plain_expr, "member", java_int_type());
+    member_exprt::unchecked(plain_expr, "member", java_int_type());
   const constant_exprt invalid_constant = constant_exprt("", java_int_type());
   const constant_exprt valid_constant = constant_exprt("0", java_int_type());
   const index_exprt valid_index = index_exprt(
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
@@ -817,7 +817,8 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)
   if(object.id()==ID_member)
   {
     const member_exprt &o_mem=to_member_expr(object);
-    dest=member_exprt(exprt(), o_mem.get_component_name(), abstract_type);
+    dest = member_exprt::unchecked(
+      exprt(), o_mem.get_component_name(), abstract_type);
     return build_wrap(
       o_mem.struct_op(), to_member_expr(dest).compound(), write);
   }
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
@@ -1192,7 +1192,10 @@ void value_sett::get_reference_set_rec(
 
       if(object.id()==ID_unknown)
         insert(dest, exprt(ID_unknown, expr.type()));
-      else
+      else if(
+        object.type().id() == ID_struct ||
+        object.type().id() == ID_struct_tag || object.type().id() == ID_union ||
+        object.type().id() == ID_union_tag)
       {
         offsett o = it->second;
 
@@ -1218,6 +1221,8 @@ void value_sett::get_reference_set_rec(
         else
           insert(dest, exprt(ID_unknown, expr.type()));
       }
+      else
+        insert(dest, exprt(ID_unknown, expr.type()));
     }
 
     return;
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
@@ -2780,15 +2780,44 @@ class member_exprt:public unary_exprt
   member_exprt(exprt op, const irep_idt &component_name, typet _type)
     : unary_exprt(ID_member, std::move(op), std::move(_type))
   {
+    const auto &compound_type_id = compound().type().id();
+    PRECONDITION(
+      compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
+      compound_type_id == ID_struct || compound_type_id == ID_union);
     set_component_name(component_name);
   }
 
+  // legacy constructor without type checking,
+  // will be removed eventually
+  member_exprt(exprt op, const irep_idt &component_name, typet _type, int)
+    : unary_exprt(ID_member, std::move(op), std::move(_type))
+  {
+    set_component_name(component_name);
+  }
+
+  static member_exprt unchecked(exprt op, irep_idt component_name, typet type)
+  {
+    return member_exprt(
+      std::move(op), std::move(component_name), std::move(type), 0);
+  }
+
   member_exprt(exprt op, const struct_typet::componentt &c)
     : unary_exprt(ID_member, std::move(op), c.type())
   {
+    const auto &compound_type_id = compound().type().id();
+    PRECONDITION(
+      compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
+      compound_type_id == ID_struct || compound_type_id == ID_union);
     set_component_name(c.get_name());
   }
 
+  // legacy constructor without type checking,
+  // will be removed eventually
+  static member_exprt unchecked(exprt op, struct_typet::componentt c)
+  {
+    return member_exprt(std::move(op), c.get_name(), c.type(), 0);
+  }
+
   irep_idt get_component_name() const
   {
     return get(ID_component_name);
diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp
@@ -34,9 +34,9 @@ SCENARIO(
     auto val2 = std::map<std::string, int>{{"a", 1}, {"b", 4}, {"c", 5}};
 
     // index_exprt for reading from an array
-    const member_exprt a(nil_exprt(), "a", integer_typet());
-    const member_exprt b(nil_exprt(), "b", integer_typet());
-    const member_exprt c(nil_exprt(), "c", integer_typet());
+    const auto a = member_exprt::unchecked(nil_exprt(), "a", integer_typet());
+    const auto b = member_exprt::unchecked(nil_exprt(), "b", integer_typet());
+    const auto c = member_exprt::unchecked(nil_exprt(), "c", integer_typet());
 
     auto object_factory = variable_sensitivity_object_factoryt::configured_with(
       vsd_configt::constant_domain());
diff --git a/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp b/unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp
@@ -26,7 +26,8 @@ full_struct_abstract_objectt::constant_struct_pointert build_struct(
       environment,
       ns,
       std::stack<exprt>(),
-      member_exprt(nil_exprt(), component.get_name(), component.type()),
+      member_exprt::unchecked(
+        nil_exprt(), component.get_name(), component.type()),
       environment.eval(op, ns),
       false);
 
diff --git a/unit/goto-symex/expr_skeleton.cpp b/unit/goto-symex/expr_skeleton.cpp
@@ -24,8 +24,9 @@ SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]")
       expr_skeletont::remove_op0(index_exprt{
         array_exprt{{}, array_typet{int_type, from_integer(2, size_type())}},
         from_integer(1, size_type())});
-    const expr_skeletont member_skeleton = expr_skeletont::remove_op0(
-      member_exprt{symbol_exprt{"struct1", typet{}}, "field1", int_type});
+    const expr_skeletont member_skeleton =
+      expr_skeletont::remove_op0(member_exprt::unchecked(
+        symbol_exprt{"struct1", typet{}}, "field1", int_type));
     THEN(
       "Applying the skeletons to `foo` gives `foo`, `foo[index]` and "
       "`foo.field1` respectively")
@@ -35,7 +36,8 @@ SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]")
         index_skeleton.apply(foo) ==
         index_exprt{foo, from_integer(1, size_type()), int_type});
       REQUIRE(
-        member_skeleton.apply(foo) == member_exprt{foo, "field1", int_type});
+        member_skeleton.apply(foo) ==
+        member_exprt::unchecked(foo, "field1", int_type));
     }
     THEN(
       "The composition of `☐[index]` with `☐.field1` applied to `foo` gives "
@@ -45,9 +47,10 @@ SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]")
         index_skeleton.compose(member_skeleton);
       REQUIRE(
         composition.apply(foo) ==
-        index_exprt{member_exprt{foo, "field1", int_type},
-                    from_integer(1, size_type()),
-                    int_type});
+        index_exprt{
+          member_exprt::unchecked(foo, "field1", int_type),
+          from_integer(1, size_type()),
+          int_type});
     }
     THEN(
       "The composition of `☐[index]` with `☐` applied to `foo` gives "
diff --git a/unit/pointer-analysis/value_set.cpp b/unit/pointer-analysis/value_set.cpp
@@ -135,7 +135,9 @@ SCENARIO(
     WHEN("We query what (a1 WITH x = NULL).x points to")
     {
       with_exprt a1_with(
-        a1_symbol.symbol_expr(), member_exprt(nil_exprt(), A_x), null_A_ptr);
+        a1_symbol.symbol_expr(),
+        member_exprt::unchecked(nil_exprt(), A_x),
+        null_A_ptr);
 
       member_exprt member_of_with(a1_with, A_x);
 
@@ -153,7 +155,9 @@ SCENARIO(
     WHEN("We query what (a1 WITH x = NULL).y points to")
     {
       with_exprt a1_with(
-        a1_symbol.symbol_expr(), member_exprt(nil_exprt(), A_x), null_A_ptr);
+        a1_symbol.symbol_expr(),
+        member_exprt::unchecked(nil_exprt(), A_x),
+        null_A_ptr);
 
       member_exprt member_of_with(a1_with, A_y);
 
@@ -171,7 +175,9 @@ SCENARIO(
     WHEN("We query what (a1 WITH x = NULL) points to")
     {
       with_exprt a1_with(
-        a1_symbol.symbol_expr(), member_exprt(nil_exprt(), A_x), null_A_ptr);
+        a1_symbol.symbol_expr(),
+        member_exprt::unchecked(nil_exprt(), A_x),
+        null_A_ptr);
 
       const std::vector<exprt> maybe_matching_with_result =
         value_set.get_value_set(a1_with, ns);
diff --git a/unit/solvers/smt2_incremental/object_tracking.cpp b/unit/solvers/smt2_incremental/object_tracking.cpp
@@ -26,16 +26,18 @@ TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
     rowt{"Address of index", {index_exprt{object_base, index}, pointer_type}},
     rowt{
       "Address of struct member",
-      {member_exprt{object_base, "baz", unsignedbv_typet{8}}, pointer_type}},
+      {member_exprt::unchecked(object_base, "baz", unsignedbv_typet{8}),
+       pointer_type}},
     rowt{
       "Address of index of struct member",
       {index_exprt{
-         member_exprt{object_base, "baz", unsignedbv_typet{8}}, index},
+         member_exprt::unchecked(object_base, "baz", unsignedbv_typet{8}),
+         index},
        pointer_type}},
     rowt{
       "Address of struct member at index",
-      {member_exprt{
-         index_exprt{object_base, index}, "baz", unsignedbv_typet{8}},
+      {member_exprt::unchecked(
+         index_exprt{object_base, index}, "baz", unsignedbv_typet{8}),
        pointer_type}});
   SECTION(description)
   {
@@ -56,7 +58,7 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]")
       address_of_exprt{index_exprt{foo, index}, pointer_type}, bar_address},
     notequal_exprt{
       address_of_exprt{
-        member_exprt{foo, "baz", unsignedbv_typet{8}}, pointer_type},
+        member_exprt::unchecked(foo, "baz", unsignedbv_typet{8}), pointer_type},
       bar_address}};
   SECTION("Find base expressions")
   {

Original file line number	Diff line number	Diff line change
`@@ -817,7 +817,8 @@ bool string_abstractiont::build(const exprt &object, exprt &dest, bool write)`
`817`	`817`	`if(object.id()==ID_member)`
`818`	`818`	`{`
`819`	`819`	`const member_exprt &o_mem=to_member_expr(object);`
`820`		`- dest=member_exprt(exprt(), o_mem.get_component_name(), abstract_type);`
	`820`	`+ dest = member_exprt::unchecked(`
	`821`	`+ exprt(), o_mem.get_component_name(), abstract_type);`
`821`	`822`	`return build_wrap(`
`822`	`823`	`o_mem.struct_op(), to_member_expr(dest).compound(), write);`
`823`	`824`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1192,7 +1192,10 @@ void value_sett::get_reference_set_rec(`
`1192`	`1192`
`1193`	`1193`	`if(object.id()==ID_unknown)`
`1194`	`1194`	`insert(dest, exprt(ID_unknown, expr.type()));`
`1195`		`- else`
	`1195`	`+ else if(`
	`1196`	`+ object.type().id() == ID_struct \|\|`
	`1197`	`+ object.type().id() == ID_struct_tag \|\| object.type().id() == ID_union \|\|`
	`1198`	`+ object.type().id() == ID_union_tag)`
`1196`	`1199`	`{`
`1197`	`1200`	`offsett o = it->second;`
`1198`	`1201`
`@@ -1218,6 +1221,8 @@ void value_sett::get_reference_set_rec(`
`1218`	`1221`	`else`
`1219`	`1222`	`insert(dest, exprt(ID_unknown, expr.type()));`
`1220`	`1223`	`}`
	`1224`	`+ else`
	`1225`	`+ insert(dest, exprt(ID_unknown, expr.type()));`
`1221`	`1226`	`}`
`1222`	`1227`
`1223`	`1228`	`return;`