Merge pull request #7330 from tautschnig/feature/move-byte-op-lowering

Move byte-operator lowering to util [depends-on: #7329]

Author: tautschnig

src/solvers/Makefile

@@ -140,7 +140,6 @@ SRC = $(BOOLEFORCE_SRC) \
       floatbv/float_bv.cpp \
       floatbv/float_utils.cpp \
       floatbv/float_approximation.cpp \
-      lowering/byte_operators.cpp \
       lowering/functions.cpp \
       bdd/miniBDD/miniBDD.cpp \
       prop/bdd_expr.cpp \

src/solvers/flattening/boolbv_byte_extract.cpp

@@ -14,8 +14,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
 
-#include <solvers/lowering/expr_lowering.h>
-
 bvt map_bv(const endianness_mapt &map, const bvt &src)
 {
   PRECONDITION(map.number_of_bits() == src.size());

src/solvers/flattening/boolbv_byte_update.cpp

@@ -12,8 +12,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/byte_operators.h>
 #include <util/invariant.h>
 
-#include <solvers/lowering/expr_lowering.h>
-
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
   // if we update (from) an unbounded array, lower the expression as the array

src/solvers/flattening/boolbv_equality.cpp

@@ -10,8 +10,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/invariant.h>
 #include <util/std_expr.h>
 
-#include <solvers/lowering/expr_lowering.h>
-
 #include "boolbv.h"
 
 literalt boolbvt::convert_equality(const equal_exprt &expr)

src/solvers/flattening/boolbv_index.cpp

@@ -18,8 +18,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
-#include <solvers/lowering/expr_lowering.h>
-
 bvt boolbvt::convert_index(const index_exprt &expr)
 {
   const exprt &array=expr.array();

src/solvers/lowering/expr_lowering.h

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

src/solvers/smt2/smt2_conv.cpp

@@ -3,6 +3,7 @@
 #include "smt2_incremental_decision_procedure.h"
 
 #include <util/arith_tools.h>
+#include <util/byte_operators.h>
 #include <util/expr.h>
 #include <util/namespace.h>
 #include <util/nodiscard.h>
@@ -11,7 +12,6 @@
 #include <util/string_utils.h>
 #include <util/symbol.h>
 
-#include <solvers/lowering/expr_lowering.h>
 #include <solvers/smt2_incremental/ast/smt_commands.h>
 #include <solvers/smt2_incremental/ast/smt_responses.h>
 #include <solvers/smt2_incremental/ast/smt_terms.h>

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -46,6 +46,7 @@ SRC = arith_tools.cpp \
       json_stream.cpp \
       lispexpr.cpp \
       lispirep.cpp \
+      lower_byte_operators.cpp \
       mathematical_expr.cpp \
       mathematical_types.cpp \
       memory_info.cpp \

src/util/Makefile

@@ -166,4 +166,30 @@ make_byte_update(const exprt &_op, const exprt &_offset, const exprt &_value);
 /// update expression.
 bool has_byte_operator(const exprt &src);
 
+/// Rewrite a byte extract expression to more fundamental operations.
+/// \param src: Byte extract expression
+/// \param ns: Namespace
+/// \return Semantically equivalent expression such that the top-level
+///   expression no longer is a \ref byte_extract_exprt or
+///   \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
+///   byte operators from any operands of \p src.
+exprt lower_byte_extract(const byte_extract_exprt &src, const namespacet &ns);
+
+/// Rewrite a byte update expression to more fundamental operations.
+/// \param src: Byte update expression
+/// \param ns: Namespace
+/// \return Semantically equivalent expression such that the top-level
+///   expression no longer is a \ref byte_extract_exprt or
+///   \ref byte_update_exprt. Use \ref lower_byte_operators to also remove all
+///   byte operators from any operands of \p src.
+exprt lower_byte_update(const byte_update_exprt &src, const namespacet &ns);
+
+/// Rewrite an expression possibly containing byte-extract or -update
+/// expressions to more fundamental operations.
+/// \param src: Input expression
+/// \param ns: Namespace
+/// \return Semantically equivalent expression that does not contain any \ref
+///   byte_extract_exprt or \ref byte_update_exprt.
+exprt lower_byte_operators(const exprt &src, const namespacet &ns);
+
 #endif // CPROVER_UTIL_BYTE_OPERATORS_H