get_l1_object: only set L0 and L1 if they are non-empty

This is important because an expression "L0: '', L1: ''" is semantically equivalent to
one with either index not specified at all, but they do not compare equal (irept::compare
distinguishes an empty-string from an absent key), leading to confusing behaviour when
ssa_exprts are used as keys in a map, for example.

Author: smowton

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;

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(

unit/util/ssa_expr.cpp

@@ -172,6 +172,7 @@ TEST_CASE("ssa_exprt::get_l1_object", "[unit][util][ssa_expr]")
 
     WHEN("get_l1_object is called on the SSA expression")
     {
+
       const ssa_exprt l1_object = ssa.get_l1_object();
       THEN("level 0 and level 1 are the same, l2 is removed")
       {
@@ -211,4 +212,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});
+      }
+    }
+  }
 }