Merge pull request #7877 from esteffin/esteffin/fix-shadow-memory-array-L2

Fix problem on array size L2 renaming

Author: Enrico Steffinlongo

regression/cbmc-shadow-memory/getenv1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$

src/goto-symex/goto_symex_state.cpp

@@ -263,15 +263,40 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       *it = rename<level>(std::move(*it), ns).get();
 
     const exprt &c_expr = as_const(expr);
+
+    // It may happen that the `old` subexpression of a `with_exprt` expression
+    // is propagated with a value that has an array type with a size that is a
+    // symbol with an L2 index that is different. In this case the type of the
+    // `with_exprt` will not match with the type of the `old` subexpression
+    // anymore.
+    // To address this issue we re-canonicalize the `with_exprt` by propagating
+    // the type of the `old` subexpression to the type of the `with_exprt`.
+    const auto *c_with_expr = expr_try_dynamic_cast<with_exprt>(c_expr);
+    if(
+      c_with_expr && can_cast_type<array_typet>(c_with_expr->type()) &&
+      can_cast_type<array_typet>(c_with_expr->old().type()) &&
+      c_with_expr->type() != c_with_expr->old().type())
+    {
+      expr.type() = to_with_expr(expr).old().type();
+    }
+    INVARIANT_WITH_DIAGNOSTICS(
+      expr.id() != ID_with ||
+        c_expr.type() == to_with_expr(c_expr).old().type(),
+      "Type of renamed expr should be the same as operands for with_exprt",
+      c_expr.type().pretty(),
+      to_with_expr(c_expr).old().type().pretty());
+    INVARIANT_WITH_DIAGNOSTICS(
+      expr.id() != ID_if ||
+        c_expr.type() == to_if_expr(c_expr).true_case().type(),
+      "Type of renamed expr should be the same as operands for if_exprt",
+      c_expr.type().pretty(),
+      to_if_expr(c_expr).true_case().type().pretty());
     INVARIANT_WITH_DIAGNOSTICS(
-      (expr.id() != ID_with ||
-       c_expr.type() == to_with_expr(c_expr).old().type()) &&
-        (expr.id() != ID_if ||
-         (c_expr.type() == to_if_expr(c_expr).true_case().type() &&
-          c_expr.type() == to_if_expr(c_expr).false_case().type())),
-      "Type of renamed expr should be the same as operands for with_exprt and "
-      "if_exprt",
-      irep_pretty_diagnosticst{expr});
+      expr.id() != ID_if ||
+        c_expr.type() == to_if_expr(c_expr).false_case().type(),
+      "Type of renamed expr should be the same as operands for if_exprt",
+      c_expr.type().pretty(),
+      to_if_expr(c_expr).false_case().type().pretty());
 
     if(level == L2)
       expr = field_sensitivity.apply(ns, *this, std::move(expr), false);