Move flatten_byte_* to lowering

The operations in this code are not tied to Boolean flattening and instead do
rewrites that are usable within any back-end.

Author: tautschnig

src/solvers/Makefile

@@ -132,12 +132,12 @@ SRC = $(BOOLEFORCE_SRC) \
       flattening/bv_utils.cpp \
       flattening/c_bit_field_replacement_type.cpp \
       flattening/equality.cpp \
-      flattening/flatten_byte_operators.cpp \
       flattening/functions.cpp \
       flattening/pointer_logic.cpp \
       floatbv/float_bv.cpp \
       floatbv/float_utils.cpp \
       floatbv/float_approximation.cpp \
+      lowering/byte_operators.cpp \
       lowering/popcount.cpp \
       miniBDD/miniBDD.cpp \
       prop/aig.cpp \

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -15,7 +15,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/byte_operators.h>
 #include <util/endianness_map.h>
 
-#include "flatten_byte_operators.h"
+#include <solvers/lowering/expr_lowering.h>
 
 bvt map_bv(const endianness_mapt &map, const bvt &src)
 {
@@ -42,7 +42,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
   // if we extract from an unbounded array, call the flattening code
   if(is_unbounded_array(expr.op().type()))
   {
-    exprt tmp=flatten_byte_extract(expr, ns);
+    exprt tmp = lower_byte_extract(expr, ns);
     return convert_bv(tmp);
   }
 

src/solvers/flattening/boolbv_equality.cpp

@@ -12,7 +12,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/base_type.h>
 #include <util/invariant.h>
 
-#include "flatten_byte_operators.h"
+#include <solvers/lowering/expr_lowering.h>
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
@@ -30,8 +30,8 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
 
     if(has_byte_operator(expr))
     {
-      exprt tmp=flatten_byte_operators(expr, ns);
-      return record_array_equality(to_equal_expr(tmp));
+      return
+        record_array_equality(to_equal_expr(lower_byte_operators(expr, ns)));
     }
 
     return record_array_equality(expr);

src/solvers/flattening/flatten_byte_operators.h

@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/replace_symbol.h>
 #include <util/simplify_expr.h>
 
-#include "flatten_byte_operators.h"
+#include "expr_lowering.h"
 
 /// rewrite an object into its individual bytes
 /// \par parameters: src  object to unpack
@@ -144,9 +144,7 @@ static exprt unpack_rec(
 
 /// rewrite byte extraction from an array to byte extraction from a
 /// concatenation of array index expressions
-exprt flatten_byte_extract(
-  const byte_extract_exprt &src,
-  const namespacet &ns)
+exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns)
 {
   // General notes about endianness and the bit-vector conversion:
   // A single byte with value 0b10001000 is stored (in irept) as
@@ -244,7 +242,7 @@ exprt flatten_byte_extract(
         tmp.type()=subtype;
         tmp.offset()=new_offset;
 
-        array.copy_to_operands(flatten_byte_extract(tmp, ns));
+        array.copy_to_operands(lower_byte_extract(tmp, ns));
       }
 
       return simplify_expr(array, ns);
@@ -337,7 +335,7 @@ exprt flatten_byte_extract(
   }
 }
 
-exprt flatten_byte_update(
+static exprt lower_byte_update(
   const byte_update_exprt &src,
   const namespacet &ns,
   bool negative_offset)
@@ -393,13 +391,13 @@ exprt flatten_byte_update(
                 ID_byte_extract_little_endian:
                 src.id()==ID_byte_update_big_endian?
                   ID_byte_extract_big_endian:
-                    throw "unexpected src.id() in flatten_byte_update",
+                    throw "unexpected src.id() in lower_byte_update",
               subtype);
 
             byte_extract_expr.op()=src.op2();
             byte_extract_expr.offset()=i_expr;
 
-            new_value=flatten_byte_extract(byte_extract_expr, ns);
+            new_value=lower_byte_extract(byte_extract_expr, ns);
           }
 
           const plus_exprt where(src.op1(), i_expr);
@@ -462,15 +460,15 @@ exprt flatten_byte_update(
               ID_byte_extract_little_endian :
               src.id()==ID_byte_update_big_endian ?
               ID_byte_extract_big_endian :
-              throw "unexpected src.id() in flatten_byte_update";
+              throw "unexpected src.id() in lower_byte_update";
             byte_extract_exprt byte_extract_expr(
               extract_opcode,
               element_size<sub_size ? src.op2().type() : subtype);
 
             byte_extract_expr.op()=src.op2();
             byte_extract_expr.offset()=stored_value_offset;
 
-            new_value=flatten_byte_extract(byte_extract_expr, ns);
+            new_value=lower_byte_extract(byte_extract_expr, ns);
           }
 
           // Where does the value we just extracted align in this cell?
@@ -501,7 +499,7 @@ exprt flatten_byte_update(
           // Call recursively, the array is gone!
           // The last parameter indicates that the
           exprt flattened_byte_update_expr=
-            flatten_byte_update(byte_update_expr, ns, is_last_cell);
+            lower_byte_update(byte_update_expr, ns, is_last_cell);
 
           with_exprt with_expr(
             result, cell_index, flattened_byte_update_expr);
@@ -515,7 +513,7 @@ exprt flatten_byte_update(
     else
     {
       throw
-        "flatten_byte_update can only do arrays of scalars right now, "
+        "lower_byte_update can only do arrays of scalars right now, "
         "but got "+subtype.id_string();
     }
   }
@@ -531,7 +529,7 @@ exprt flatten_byte_update(
     std::size_t width=integer2size_t(type_width);
 
     if(element_size*8>width)
-      throw "flatten_byte_update to update element that is too large";
+      throw "lower_byte_update to update element that is too large";
 
     // build mask
     exprt mask=
@@ -584,16 +582,16 @@ exprt flatten_byte_update(
   }
   else
   {
-    throw "flatten_byte_update can only do array and scalars "
+    throw "lower_byte_update can only do array and scalars "
           "right now, but got "+t.id_string();
   }
 }
 
-exprt flatten_byte_update(
+static exprt lower_byte_update(
   const byte_update_exprt &src,
   const namespacet &ns)
 {
-  return flatten_byte_update(src, ns, false);
+  return lower_byte_update(src, ns, false);
 }
 
 bool has_byte_operator(const exprt &src)
@@ -611,25 +609,23 @@ bool has_byte_operator(const exprt &src)
   return false;
 }
 
-exprt flatten_byte_operators(
-  const exprt &src,
-  const namespacet &ns)
+exprt lower_byte_operators(const exprt &src, const namespacet &ns)
 {
   exprt tmp=src;
 
   // destroys any sharing, should use hash table
   Forall_operands(it, tmp)
   {
-    exprt tmp=flatten_byte_operators(*it, ns);
+    exprt tmp=lower_byte_operators(*it, ns);
     it->swap(tmp);
   }
 
   if(src.id()==ID_byte_update_little_endian ||
      src.id()==ID_byte_update_big_endian)
-    return flatten_byte_update(to_byte_update_expr(tmp), ns);
+    return lower_byte_update(to_byte_update_expr(tmp), ns);
   else if(src.id()==ID_byte_extract_little_endian ||
           src.id()==ID_byte_extract_big_endian)
-    return flatten_byte_extract(to_byte_extract_expr(tmp), ns);
+    return lower_byte_extract(to_byte_extract_expr(tmp), ns);
   else
     return tmp;
 }

src/solvers/flattening/flatten_byte_operators.cpp renamed to src/solvers/lowering/byte_operators.cpp

@@ -11,9 +11,16 @@ Author: Michael Tautschnig
 
 #include <util/expr.h>
 
+class byte_extract_exprt;
 class namespacet;
 class popcount_exprt;
 
+exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
+
+exprt lower_byte_operators(const exprt &src, const namespacet &ns);
+
+bool has_byte_operator(const exprt &src);
+
 /// Lower a popcount_exprt to arithmetic and logic expressions
 /// \param expr  Input expression to be translated
 /// \param ns  Namespace for type lookups

src/solvers/lowering/expr_lowering.h

@@ -27,8 +27,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/pointer_logic.h>
-#include <solvers/flattening/flatten_byte_operators.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
+#include <solvers/lowering/expr_lowering.h>
 
 void smt1_convt::print_assignment(std::ostream &out) const
 {
@@ -356,7 +356,7 @@ void smt1_convt::convert_byte_extract(
   bool bool_as_bv)
 {
   // we just run the flattener
-  exprt flattened_expr=flatten_byte_extract(expr, ns);
+  exprt flattened_expr = lower_byte_extract(expr, ns);
   convert_expr(flattened_expr, bool_as_bv);
 }
 

src/solvers/smt1/smt1_conv.cpp

@@ -29,9 +29,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/string_constant.h>
 
 #include <solvers/flattening/boolbv_width.h>
-#include <solvers/flattening/flatten_byte_operators.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
 #include <solvers/floatbv/float_bv.h>
+#include <solvers/lowering/expr_lowering.h>
 
 // Mark different kinds of error condition
 // General
@@ -598,7 +598,7 @@ void smt2_convt::convert_address_of_rec(
 void smt2_convt::convert_byte_extract(const byte_extract_exprt &expr)
 {
   // we just run the flattener
-  exprt flattened_expr=flatten_byte_extract(expr, ns);
+  exprt flattened_expr = lower_byte_extract(expr, ns);
   unflatten(wheret::BEGIN, expr.type());
   convert_expr(flattened_expr);
   unflatten(wheret::END, expr.type());