Merge pull request #3290 from tautschnig/move-flatten-byte-ops

Move flatten_byte_* to lowering [blocks: #2068, #2501]

Author: kroening

src/solvers/Makefile

@@ -138,12 +138,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/bdd_expr.cpp \

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -16,10 +16,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/std_expr.h>
 #include <util/throw_with_nested.h>
 
+#include <solvers/lowering/expr_lowering.h>
+#include <solvers/lowering/flatten_byte_extract_exceptions.h>
+
 #include "bv_conversion_exceptions.h"
 #include "bv_endianness_map.h"
-#include "flatten_byte_extract_exceptions.h"
-#include "flatten_byte_operators.h"
 
 bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 {

src/solvers/flattening/boolbv_equality.cpp

@@ -12,8 +12,9 @@ Author: Daniel Kroening, [email protected]
 #include <util/base_type.h>
 #include <util/invariant.h>
 
+#include <solvers/lowering/expr_lowering.h>
+
 #include "bv_conversion_exceptions.h"
-#include "flatten_byte_operators.h"
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)
 {

src/solvers/flattening/flatten_byte_operators.h

@@ -6,7 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include "flatten_byte_operators.h"
+#include "expr_lowering.h"
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "flatten_byte_extract_exceptions.h"
 
+// clang-format off
+
 /// rewrite an object into its individual bytes
 /// \par parameters: src  object to unpack
 /// little_endian  true, iff assumed endianness is little-endian
@@ -664,3 +666,4 @@ exprt flatten_byte_operators(
   else
     return tmp;
 }
+// clang-format on

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

@@ -11,9 +11,19 @@ Author: Michael Tautschnig
 
 #include <util/expr.h>
 
+class byte_extract_exprt;
+class byte_update_exprt;
 class namespacet;
 class popcount_exprt;
 
+exprt flatten_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
+
+exprt flatten_byte_update(const byte_update_exprt &src, const namespacet &ns);
+
+exprt flatten_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

@@ -28,7 +28,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <solvers/flattening/boolbv_width.h>
 #include <solvers/flattening/c_bit_field_replacement_type.h>
-#include <solvers/flattening/flatten_byte_operators.h>
 #include <solvers/floatbv/float_bv.h>
 #include <solvers/lowering/expr_lowering.h>