Simplify extractbits(concatenation(...))

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -20,6 +20,7 @@ Author: Daniel Kroening, [email protected]
 #include "ieee_float.h"
 #include "invariant.h"
 #include "namespace.h"
+#include "pointer_offset_size.h"
 #include "rational.h"
 #include "rational_tools.h"
 #include "std_expr.h"
@@ -1146,6 +1147,32 @@ bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr)
 
     return false;
   }
+  else if(expr.src().id() == ID_concatenation)
+  {
+    // the most-significant bit comes first in an concatenation_exprt, hence we
+    // count down
+    mp_integer offset = width;
+
+    forall_operands(it, expr.src())
+    {
+      mp_integer op_width = pointer_offset_bits(it->type(), ns);
+
+      if(op_width <= 0)
+        return true;
+
+      if(start + 1 == offset && end + op_width == offset)
+      {
+        exprt tmp = *it;
+        if(tmp.type() != expr.type())
+          return true;
+
+        expr.swap(tmp);
+        return false;
+      }
+
+      offset -= op_width;
+    }
+  }
 
   return true;
 }