Lower byte_{extract,update} when pointers are involved

Author: tautschnig

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 #include <cassert>
 
 #include <util/arith_tools.h>
+#include <util/expr_util.h>
 #include <util/std_expr.h>
 #include <util/byte_operators.h>
 #include <util/endianness_map.h>
@@ -39,8 +40,12 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   if(expr.operands().size()!=2)
     throw "byte_extract takes two operands";
 
-  // if we extract from an unbounded array, call the flattening code
-  if(is_unbounded_array(expr.op().type()))
+  // if we extract from an unbounded array or a data type that
+  // includes pointers, call the flattening code
+  if(
+    is_unbounded_array(expr.op().type()) ||
+    has_subtype(expr.type(), ID_pointer, ns) ||
+    has_subtype(expr.op().type(), ID_pointer, ns))
   {
     exprt tmp = lower_byte_extract(expr, ns);
     return convert_bv(tmp);

src/solvers/flattening/boolbv_byte_update.cpp

@@ -8,18 +8,30 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv.h"
 
-#include <iostream>
 #include <cassert>
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/endianness_map.h>
+#include <util/expr_util.h>
+
+#include <solvers/lowering/expr_lowering.h>
 
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
   if(expr.operands().size()!=3)
     throw "byte_update takes three operands";
 
+  // if we update an unbounded array or a data type that
+  // includes pointers, call the flattening code
+  if(
+    is_unbounded_array(expr.op().type()) ||
+    has_subtype(expr.value().type(), ID_pointer, ns) ||
+    has_subtype(expr.op0().type(), ID_pointer, ns))
+  {
+    return convert_bv(lower_byte_update(expr, ns));
+  }
+
   const exprt &op=expr.op0();
   const exprt &offset_expr=expr.offset();
   const exprt &value=expr.value();

src/solvers/lowering/byte_operators.cpp

@@ -878,9 +878,7 @@ static exprt lower_byte_update(
   }
 }
 
-static exprt lower_byte_update(
-  const byte_update_exprt &src,
-  const namespacet &ns)
+exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns)
 {
   return lower_byte_update(src, ns, false);
 }

src/solvers/lowering/expr_lowering.h

@@ -12,11 +12,14 @@ Author: Michael Tautschnig
 #include <util/expr.h>
 
 class byte_extract_exprt;
+class byte_update_exprt;
 class namespacet;
 class popcount_exprt;
 
 exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
 
+exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);
+
 exprt lower_byte_operators(const exprt &src, const namespacet &ns);
 
 bool has_byte_operator(const exprt &src);