Move byte operator lowering to util

There is nothing solvers-specific taking place in this code. Moving this
to util enable future use by expression simplification.

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

@@ -6,12 +6,11 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include "boolbv.h"
-
-#include <util/std_expr.h>
+#include <util/byte_operators.h>
 #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

src/util/byte_operators.h

@@ -6,19 +6,17 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
-#include <util/arith_tools.h>
-#include <util/bitvector_expr.h>
-#include <util/byte_operators.h>
-#include <util/c_types.h>
-#include <util/endianness_map.h>
-#include <util/expr_util.h>
-#include <util/namespace.h>
-#include <util/narrow.h>
-#include <util/pointer_offset_size.h>
-#include <util/simplify_expr.h>
-#include <util/string_constant.h>
-
-#include "expr_lowering.h"
+#include "arith_tools.h"
+#include "bitvector_expr.h"
+#include "byte_operators.h"
+#include "c_types.h"
+#include "endianness_map.h"
+#include "expr_util.h"
+#include "namespace.h"
+#include "narrow.h"
+#include "pointer_offset_size.h"
+#include "simplify_expr.h"
+#include "string_constant.h"
 
 #include <algorithm>
 

src/solvers/lowering/byte_operators.cpp renamed to src/util/lower_byte_operators.cpp

@@ -94,7 +94,6 @@ SRC += analyses/ai/ai.cpp \
        pointer-analysis/value_set.cpp \
        solvers/bdd/miniBDD/miniBDD.cpp \
        solvers/floatbv/float_utils.cpp \
-       solvers/lowering/byte_operators.cpp \
        solvers/prop/bdd_expr.cpp \
        solvers/sat/external_sat.cpp \
        solvers/sat/satcheck_cadical.cpp \
@@ -159,6 +158,7 @@ SRC += analyses/ai/ai.cpp \
        util/json_array.cpp \
        util/json_object.cpp \
        util/lazy.cpp \
+       util/lower_byte_operators.cpp \
        util/memory_info.cpp \
        util/message.cpp \
        util/optional.cpp \

unit/Makefile

@@ -6,10 +6,6 @@
 
 \*******************************************************************/
 
-#include <testing-utils/use_catch.h>
-
-#include <solvers/lowering/expr_lowering.h>
-
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
@@ -24,7 +20,9 @@
 #include <util/string_constant.h>
 #include <util/symbol_table.h>
 
-TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("byte extract and bits", "[core][util][lowering][byte_extract]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness
@@ -94,7 +92,7 @@ TEST_CASE("byte extract and bits", "[core][solvers][lowering][byte_extract]")
   }
 }
 
-SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
+SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness
@@ -362,7 +360,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
   }
 }
 
-SCENARIO("byte_update_lowering", "[core][solvers][lowering][byte_update]")
+SCENARIO("byte_update_lowering", "[core][util][lowering][byte_update]")
 {
   // this test does require a proper architecture to be set so that byte extract
   // uses adequate endianness