Flatten 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>
 
@@ -39,8 +40,11 @@ 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=flatten_byte_extract(expr, ns);
     return convert_bv(tmp);

src/solvers/flattening/boolbv_byte_update.cpp

@@ -8,19 +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/expr_util.h>
 
 #include "bv_endianness_map.h"
+#include "flatten_byte_operators.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))
+  {
+    exprt tmp=flatten_byte_update(expr, ns);
+    return convert_bv(tmp);
+  }
+
   const exprt &op=expr.op0();
   const exprt &offset_expr=expr.offset();
   const exprt &value=expr.value();