Extensions to simplify_byte_extract

Further simplify extracts from arrays and structs

Author: tautschnig

src/util/simplify_expr.cpp

@@ -2061,7 +2061,9 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
       assert(el_size%8==0);
       mp_integer el_bytes=el_size/8;
 
-      if(base_type_eq(expr.type(), op_type_ptr->subtype(), ns))
+      if(base_type_eq(expr.type(), op_type_ptr->subtype(), ns) ||
+         (expr.type().id()==ID_pointer &&
+          op_type_ptr->subtype().id()==ID_pointer))
       {
         if(offset%el_bytes==0)
         {
@@ -2071,6 +2073,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
             index_exprt(
               result,
               from_integer(offset, expr.offset().type()));
+          result.make_typecast(expr.type());
 
           expr.swap(result);
           simplify_rec(expr);
@@ -2128,7 +2131,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
         simplify_member(expr.op());
         expr.offset()=
           from_integer(offset-m_offset_bits/8, expr.offset().type());
-        simplify_rec(expr.offset());
+        simplify_rec(expr);
 
         return false;
       }