member_exprt now checks type of compound operand

This commit adds a precondition to the constructors of member_exprt that
enforces that the compound operand has one of the compound types.

Author: kroening

jbmc/unit/java_bytecode/java_trace_validation/java_trace_validation.cpp

@@ -22,12 +22,13 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
 {
   const exprt plain_expr = exprt();
   const exprt expr_with_data = exprt("id", java_int_type());
-  const symbol_exprt valid_symbol_expr = symbol_exprt("id", java_int_type());
+  const symbol_exprt valid_symbol_expr =
+    symbol_exprt("id", struct_typet{{{"member", 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());
-  const member_exprt invalid_member =
-    member_exprt(plain_expr, "member", java_int_type());
+  exprt invalid_member = unary_exprt{ID_member, plain_expr, java_int_type()};
+  invalid_member.set(ID_component_name, "member");
   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(
@@ -88,7 +89,8 @@ TEST_CASE("java trace validation", "[core][java_trace_validation]")
     INFO("valid member structure")
     REQUIRE(check_member_structure(valid_member));
     INFO("invalid member structure, no symbol operand")
-    REQUIRE_FALSE(check_member_structure(invalid_member));
+    REQUIRE_FALSE(check_member_structure(
+      static_cast<const member_exprt &>(invalid_member)));
   }
 
   SECTION("can_evaluate_to_constant")

src/goto-programs/string_abstraction.cpp

@@ -817,24 +817,32 @@ 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);
-    return build_wrap(
-      o_mem.struct_op(), to_member_expr(dest).compound(), write);
+    exprt compound;
+    if(build_wrap(o_mem.struct_op(), compound, write))
+      return true;
+    dest = member_exprt{
+      std::move(compound), o_mem.get_component_name(), abstract_type};
+    return false;
   }
 
   if(object.id()==ID_dereference)
   {
     const dereference_exprt &o_deref=to_dereference_expr(object);
-    dest=dereference_exprt(exprt(), abstract_type);
-    return build_wrap(
-      o_deref.pointer(), to_dereference_expr(dest).pointer(), write);
+    exprt pointer;
+    if(build_wrap(o_deref.pointer(), pointer, write))
+      return true;
+    dest = dereference_exprt{std::move(pointer)};
+    return false;
   }
 
   if(object.id()==ID_index)
   {
     const index_exprt &o_index=to_index_expr(object);
-    dest=index_exprt(exprt(), o_index.index(), abstract_type);
-    return build_wrap(o_index.array(), to_index_expr(dest).array(), write);
+    exprt array;
+    if(build_wrap(o_index.array(), array, write))
+      return true;
+    dest = index_exprt{std::move(array), o_index.index()};
+    return false;
   }
 
   // handle pointer stuff

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;

src/pointer-analysis/value_set_fi.cpp

@@ -916,11 +916,10 @@ void value_set_fit::get_reference_set_sharing_rec(
       if(object.id()==ID_unknown)
         insert(dest, exprt(ID_unknown, expr.type()));
       else if(
-        object.id() == ID_dynamic_object && obj_type.id() != ID_struct &&
-        obj_type.id() != ID_union && obj_type.id() != ID_struct_tag &&
-        obj_type.id() != ID_union_tag)
+        obj_type.id() != ID_struct && obj_type.id() != ID_union &&
+        obj_type.id() != ID_struct_tag && obj_type.id() != ID_union_tag)
       {
-        // we catch dynamic objects of the wrong type,
+        // we catch objects of the wrong type,
         // to avoid non-integral typecasts.
         insert(dest, exprt(ID_unknown, expr.type()));
       }

src/util/std_expr.h

@@ -2789,12 +2789,20 @@ 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);
   }
 
   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());
   }
 

unit/analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp

@@ -33,10 +33,13 @@ SCENARIO(
     // struct val2 = {.a = 1, .b = 4, .c = 5}
     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());
+    // member_exprt for reading from a struct
+    exprt dummy = nil_exprt{};
+    dummy.type() = struct_typet{
+      {{"a", integer_typet{}}, {"b", integer_typet{}}, {"c", integer_typet{}}}};
+    const auto a = member_exprt(dummy, "a", integer_typet());
+    const auto b = member_exprt(dummy, "b", integer_typet());
+    const auto c = member_exprt(dummy, "c", integer_typet());
 
     auto object_factory = variable_sensitivity_object_factoryt::configured_with(
       vsd_configt::constant_domain());

unit/analyses/variable-sensitivity/full_struct_abstract_object/struct_builder.cpp

@@ -19,14 +19,18 @@ full_struct_abstract_objectt::constant_struct_pointert build_struct(
 
   auto struct_type = to_struct_type(starting_value.type());
   size_t comp_index = 0;
+
+  auto nil_with_type = nil_exprt();
+  nil_with_type.type() = struct_type;
+
   for(const exprt &op : starting_value.operands())
   {
     const auto &component = struct_type.components()[comp_index];
     auto new_result = result->write(
       environment,
       ns,
       std::stack<exprt>(),
-      member_exprt(nil_exprt(), component.get_name(), component.type()),
+      member_exprt(nil_with_type, component.get_name(), component.type()),
       environment.eval(op, ns),
       false);
 

unit/goto-symex/expr_skeleton.cpp

@@ -15,27 +15,32 @@ Author: Romain Brenguier, [email protected]
 
 SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]")
 {
-  const symbol_exprt foo{"foo", typet{}};
+  const signedbv_typet int_type{32};
+  const array_typet array_type{int_type, from_integer(2, size_type())};
+  const symbol_exprt foo_a{"foo", array_type};
+  const symbol_exprt foo_s{"foo", struct_typet{{{"field1", array_type}}}};
+
   GIVEN("Skeletons `☐`, `☐[index]` and `☐.field1`")
   {
     const expr_skeletont empty_skeleton;
-    const signedbv_typet int_type{32};
-    const expr_skeletont index_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 index_skeleton = expr_skeletont::remove_op0(
+      index_exprt{array_exprt{{}, array_type}, from_integer(1, size_type())});
+    const expr_skeletont member_skeleton =
+      expr_skeletont::remove_op0(member_exprt{
+        symbol_exprt{"struct1", struct_typet{{{"field1", array_type}}}},
+        "field1",
+        array_type});
     THEN(
       "Applying the skeletons to `foo` gives `foo`, `foo[index]` and "
       "`foo.field1` respectively")
     {
-      REQUIRE(empty_skeleton.apply(foo) == foo);
+      REQUIRE(empty_skeleton.apply(foo_a) == foo_a);
       REQUIRE(
-        index_skeleton.apply(foo) ==
-        index_exprt{foo, from_integer(1, size_type()), int_type});
+        index_skeleton.apply(foo_a) ==
+        index_exprt{foo_a, from_integer(1, size_type()), int_type});
       REQUIRE(
-        member_skeleton.apply(foo) == member_exprt{foo, "field1", int_type});
+        member_skeleton.apply(foo_s) ==
+        member_exprt(foo_s, "field1", array_type));
     }
     THEN(
       "The composition of `☐[index]` with `☐.field1` applied to `foo` gives "
@@ -44,19 +49,19 @@ SCENARIO("expr skeleton", "[core][goto-symex][symex-assign][expr-skeleton]")
       const expr_skeletont composition =
         index_skeleton.compose(member_skeleton);
       REQUIRE(
-        composition.apply(foo) ==
-        index_exprt{member_exprt{foo, "field1", int_type},
-                    from_integer(1, size_type()),
-                    int_type});
+        composition.apply(foo_s) == index_exprt{
+                                      member_exprt(foo_s, "field1", array_type),
+                                      from_integer(1, size_type()),
+                                      int_type});
     }
     THEN(
       "The composition of `☐[index]` with `☐` applied to `foo` gives "
       "`foo[index]`")
     {
       const expr_skeletont composition = index_skeleton.compose(empty_skeleton);
       REQUIRE(
-        composition.apply(foo) ==
-        index_exprt{foo, from_integer(1, size_type()), int_type});
+        composition.apply(foo_a) ==
+        index_exprt{foo_a, from_integer(1, size_type()), int_type});
     }
   }
 }

unit/pointer-analysis/value_set.cpp

@@ -135,7 +135,8 @@ 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(), exprt{ID_member_name}, null_A_ptr);
+      a1_with.where().set(ID_component_name, A_x.get_name());
 
       member_exprt member_of_with(a1_with, A_x);
 
@@ -153,7 +154,8 @@ 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(), exprt{ID_member_name}, null_A_ptr);
+      a1_with.where().set(ID_component_name, A_x.get_name());
 
       member_exprt member_of_with(a1_with, A_y);
 
@@ -171,7 +173,8 @@ 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(), exprt{ID_member_name}, null_A_ptr);
+      a1_with.where().set(ID_component_name, A_x.get_name());
 
       const std::vector<exprt> maybe_matching_with_result =
         value_set.get_value_set(a1_with, ns);

unit/solvers/smt2_incremental/object_tracking.cpp

@@ -12,41 +12,12 @@
 #include <string>
 #include <utility>
 
-TEST_CASE("find_object_base_expression", "[core][smt2_incremental]")
-{
-  const typet base_type = pointer_typet{unsignedbv_typet{8}, 18};
-  const symbol_exprt object_base{"base", base_type};
-  const symbol_exprt index{"index", base_type};
-  const pointer_typet pointer_type{base_type, 12};
-  std::string description;
-  optionalt<address_of_exprt> address_of;
-  using rowt = std::pair<std::string, address_of_exprt>;
-  std::tie(description, address_of) = GENERATE_REF(
-    rowt{"Address of symbol", {object_base, pointer_type}},
-    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}},
-    rowt{
-      "Address of index of struct member",
-      {index_exprt{member_exprt{object_base, "baz", base_type}, index},
-       pointer_type}},
-    rowt{
-      "Address of struct member at index",
-      {member_exprt{
-         index_exprt{object_base, index}, "baz", unsignedbv_typet{8}},
-       pointer_type}});
-  SECTION(description)
-  {
-    CHECK(find_object_base_expression(*address_of) == object_base);
-  }
-}
-
 TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]")
 {
   const typet base_type = pointer_typet{signedbv_typet{16}, 18};
   const symbol_exprt foo{"foo", base_type};
   const symbol_exprt bar{"bar", base_type};
+  const symbol_exprt qux{"qux", struct_typet{}};
   const symbol_exprt index{"index", base_type};
   const pointer_typet pointer_type{base_type, 32};
   const exprt bar_address = address_of_exprt{bar, pointer_type};
@@ -55,15 +26,15 @@ 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(qux, "baz", unsignedbv_typet{8}), pointer_type},
       bar_address}};
   SECTION("Find base expressions")
   {
     std::vector<exprt> expressions;
     find_object_base_expressions(compound_expression, [&](const exprt &expr) {
       expressions.push_back(expr);
     });
-    CHECK(expressions == std::vector<exprt>{bar, foo, bar, foo});
+    CHECK(expressions == std::vector<exprt>{bar, qux, bar, foo});
   }
   smt_object_mapt object_map = initial_smt_object_map();
   SECTION("Check initial object map has null pointer")
@@ -83,11 +54,11 @@ TEST_CASE("Tracking object base expressions", "[core][smt2_incremental]")
   track_expression_objects(compound_expression, ns, object_map);
   SECTION("Tracking expression objects")
   {
-    CHECK(object_map.size() == 3);
+    CHECK(object_map.size() == 4);
     const auto foo_object = object_map.find(foo);
     REQUIRE(foo_object != object_map.end());
     CHECK(foo_object->second.base_expression == foo);
-    CHECK(foo_object->second.unique_id == 2);
+    CHECK(foo_object->second.unique_id == 3);
     const auto bar_object = object_map.find(bar);
     REQUIRE(bar_object != object_map.end());
     CHECK(bar_object->second.base_expression == bar);