diff --git a/src/util/ssa_expr.cpp b/src/util/ssa_expr.cpp index 53acec47310..18b75b338d9 100644 --- a/src/util/ssa_expr.cpp +++ b/src/util/ssa_expr.cpp @@ -160,8 +160,10 @@ const ssa_exprt ssa_exprt::get_l1_object() const object_descriptor_exprt ode(get_original_expr()); ssa_exprt root(ode.root_object()); - root.set(ID_L0, get(ID_L0)); - root.set(ID_L1, get(ID_L1)); + if(!get_level_0().empty()) + root.set(ID_L0, get(ID_L0)); + if(!get_level_1().empty()) + root.set(ID_L1, get(ID_L1)); ::update_identifier(root); return root; diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h index a7902db8ab9..79bd38ff95a 100644 --- a/src/util/ssa_expr.h +++ b/src/util/ssa_expr.h @@ -91,6 +91,27 @@ class ssa_exprt:public symbol_exprt DATA_CHECK( vm, expr.id() == ID_symbol, "SSA expression symbols are symbols"); DATA_CHECK(vm, expr.get_bool(ID_C_SSA_symbol), "wrong SSA expression ID"); + // Check that each of the L0, L1 and L2 indices are either absent or are + // set to a non-empty value -- otherwise we could have two ssa_exprts that + // represent the same value (since get(ID_L0/1/2) will yield an empty string + // in both cases), but which do not compare equal (since irept::compare + // does not regard a missing key and an empty value as equivalent) + const auto &expr_sub = expr.get_named_sub(); + const auto expr_l0 = expr_sub.find(ID_L0); + const auto expr_l1 = expr_sub.find(ID_L1); + const auto expr_l2 = expr_sub.find(ID_L2); + DATA_CHECK( + vm, + expr_l0 == expr_sub.end() || !expr_l0->second.id().empty(), + "L0 must not be an empty string"); + DATA_CHECK( + vm, + expr_l1 == expr_sub.end() || !expr_l1->second.id().empty(), + "L1 must not be an empty string"); + DATA_CHECK( + vm, + expr_l2 == expr_sub.end() || !expr_l2->second.id().empty(), + "L2 must not be an empty string"); } static void validate( diff --git a/unit/util/ssa_expr.cpp b/unit/util/ssa_expr.cpp index 09362f9cb54..ec35114452a 100644 --- a/unit/util/ssa_expr.cpp +++ b/unit/util/ssa_expr.cpp @@ -211,4 +211,20 @@ TEST_CASE("ssa_exprt::get_l1_object", "[unit][util][ssa_expr]") } } } + + GIVEN("An ssa_exprt with its L2 index set") + { + const symbol_exprt symbol{"sym", int_type}; + ssa_exprt ssa{symbol}; + ssa.set_level_2(7); + + WHEN("Its L1 object is taken") + { + const ssa_exprt l1_object = ssa.get_l1_object(); + THEN("It should compare equal to the base symbol") + { + REQUIRE(l1_object == ssa_exprt{symbol}); + } + } + } }