Merge pull request #7340 from tautschnig/feature/be-simplify-lowering

Simplify byte extract: use lowering when expression is a constant

Author: tautschnig

regression/cbmc-library/memcpy-01/constant-propagation.desc

@@ -1,7 +1,7 @@
 CORE
 main.c
---show-vcc
-main::1::m!0@1#2 = .*byte_extract_(big|little)_endian\(cast\(44, signedbv\[\d+\]\*\), 0, signedbv\[\d+\]\).*
+
+^Generated 1\d* VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/util/simplify_expr.cpp

@@ -1976,10 +1976,13 @@ simplify_exprt::simplify_byte_extract(const byte_extract_exprt &expr)
   // try to refine it down to extracting from a member or an index in an array
   auto subexpr =
     get_subexpression_at_offset(expr.op(), *offset, expr.type(), ns);
-  if(!subexpr.has_value() || subexpr.value() == expr)
-    return unchanged(expr);
+  if(subexpr.has_value() && subexpr.value() != expr)
+    return changed(simplify_rec(subexpr.value())); // recursive call
+
+  if(is_constantt(ns)(expr))
+    return changed(simplify_rec(lower_byte_extract(expr, ns)));
 
-  return changed(simplify_rec(subexpr.value())); // recursive call
+  return unchanged(expr);
 }
 
 simplify_exprt::resultt<>

src/util/simplify_expr_int.cpp

@@ -906,7 +906,14 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr)
             .set_width(
               to_bitvector_type(eb_i.type()).get_width() +
               to_bitvector_type(eb_n.type()).get_width());
-          opi = eb_merged;
+          if(expr.type().id() != eb_merged.type().id())
+          {
+            bitvector_typet bt = to_bitvector_type(expr.type());
+            bt.set_width(to_bitvector_type(eb_merged.type()).get_width());
+            opi = simplify_typecast(typecast_exprt{eb_merged, bt});
+          }
+          else
+            opi = eb_merged;
           // erase opn
           new_expr.operands().erase(new_expr.operands().begin() + i + 1);
           no_change = false;