Merge pull request #5759 from diffblue/bitvector_expr_h

kroening · web-flow · commit 6c59fc821654 · 2021-01-18T12:13:39.000Z
move bitvector-related expression classes into separate header file
diff --git a/jbmc/src/java_bytecode/character_refine_preprocess.cpp b/jbmc/src/java_bytecode/character_refine_preprocess.cpp
@@ -16,6 +16,7 @@ Date:   March 2017
 #include "character_refine_preprocess.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/std_expr.h>
 
 /// converts based on a function on expressions
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -17,8 +17,10 @@ Date:   April 2017
 ///   java.lang.StringBuilder, java.lang.StringBuffer.
 
 #include <goto-programs/class_identifier.h>
+
 #include <util/allocate_objects.h>
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/expr_initializer.h>
 #include <util/fresh_symbol.h>
diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt
@@ -83,7 +83,7 @@ warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many node
 warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'exception_utils.h' not generated, too many nodes (61), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
@@ -96,6 +96,6 @@ warning: Included by graph for 'namespace.h' not generated, too many nodes (112)
 warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'std_expr.h' not generated, too many nodes (247), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'std_expr.h' not generated, too many nodes (248), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/arith_tools.h>
 #include <util/array_name.h>
+#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/cprover_prefix.h>
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
@@ -14,15 +14,16 @@ Date: April 2010
 #include <limits>
 #include <memory>
 
-#include <util/expr_util.h>
-#include <util/std_code.h>
-#include <util/std_expr.h>
-#include <util/pointer_offset_size.h>
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/endianness_map.h>
-#include <util/arith_tools.h>
-#include <util/simplify_expr.h>
+#include <util/expr_util.h>
 #include <util/make_unique.h>
+#include <util/pointer_offset_size.h>
+#include <util/simplify_expr.h>
+#include <util/std_code.h>
+#include <util/std_expr.h>
 
 #include <langapi/language_util.h>
 
diff --git a/src/ansi-c/c_typecheck_base.h b/src/ansi-c/c_typecheck_base.h
@@ -12,12 +12,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_ANSI_C_C_TYPECHECK_BASE_H
 #define CPROVER_ANSI_C_C_TYPECHECK_BASE_H
 
-#include <util/symbol_table.h>
-#include <util/typecheck.h>
+#include <util/bitvector_expr.h>
 #include <util/namespace.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
+#include <util/symbol_table.h>
+#include <util/typecheck.h>
 
 #include "ansi_c_declaration.h"
 #include "designator.h"
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
@@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unordered_map>
 #include <unordered_set>
 
+#include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/mathematical_expr.h>
 #include <util/std_code.h>
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "interpreter_class.h"
 
+#include <util/bitvector_expr.h>
 #include <util/byte_operators.h>
 #include <util/fixedbv.h>
 #include <util/ieee_float.h>
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
@@ -13,6 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <set>
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/magic.h>
 #include <util/mp_arith.h>
 #include <util/prefix.h>
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
@@ -26,10 +26,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv_map.h"
 #include "arrays.h"
 
+class array_comprehension_exprt;
+class bswap_exprt;
+class concatenation_exprt;
 class extractbit_exprt;
 class extractbits_exprt;
-class array_comprehension_exprt;
 class member_exprt;
+class replication_exprt;
 
 class boolbvt:public arrayst
 {
diff --git a/src/solvers/flattening/boolbv_bitwise.cpp b/src/solvers/flattening/boolbv_bitwise.cpp
@@ -6,9 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
+#include <util/bitvector_expr.h>
+
 bvt boolbvt::convert_bitwise(const exprt &expr)
 {
   const std::size_t width = boolbv_width(expr.type());
diff --git a/src/solvers/flattening/boolbv_bswap.cpp b/src/solvers/flattening/boolbv_bswap.cpp
@@ -8,6 +8,7 @@ Author: Michael Tautschnig
 
 #include "boolbv.h"
 
+#include <util/bitvector_expr.h>
 #include <util/invariant.h>
 
 bvt boolbvt::convert_bswap(const bswap_exprt &expr)
diff --git a/src/solvers/flattening/boolbv_concatenation.cpp b/src/solvers/flattening/boolbv_concatenation.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
+#include <util/bitvector_expr.h>
 #include <util/invariant.h>
 
 bvt boolbvt::convert_concatenation(const concatenation_exprt &expr)
diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/exception_utils.h>
 #include <util/std_expr.h>
 #include <util/std_types.h>
diff --git a/src/solvers/flattening/boolbv_extractbits.cpp b/src/solvers/flattening/boolbv_extractbits.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 
 bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
 {
diff --git a/src/solvers/flattening/boolbv_replication.cpp b/src/solvers/flattening/boolbv_replication.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 
 bvt boolbvt::convert_replication(const replication_exprt &expr)
 {
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
@@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "bv_pointers.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
@@ -10,8 +10,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <algorithm>
 
-#include <util/std_expr.h>
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/std_expr.h>
 
 exprt float_bvt::convert(const exprt &expr) const
 {
diff --git a/src/solvers/lowering/byte_operators.cpp b/src/solvers/lowering/byte_operators.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 #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>
diff --git a/src/solvers/lowering/popcount.cpp b/src/solvers/lowering/popcount.cpp
@@ -9,6 +9,7 @@ Author: Michael Tautschnig
 #include "expr_lowering.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/invariant.h>
 #include <util/pointer_offset_size.h>
 #include <util/std_expr.h>
diff --git a/src/solvers/qbf/qdimacs_core.cpp b/src/solvers/qbf/qdimacs_core.cpp
@@ -9,6 +9,7 @@ Author: CM Wintersteiger
 #include "qdimacs_core.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/std_expr.h>
 
 void qdimacs_coret::simplify_extractbits(exprt &expr) const
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
@@ -12,6 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "smt2_conv.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/expr_iterator.h>
diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp
@@ -11,6 +11,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "smt2_format.h"
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/mathematical_expr.h>
diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp
@@ -11,10 +11,12 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com
 /// Generates string constraints for functions generating strings from other
 /// types, in particular int, long, float, double, char, bool
 
-#include <solvers/floatbv/float_bv.h>
-
 #include "string_constraint_generator.h"
 
+#include <util/bitvector_expr.h>
+
+#include <solvers/floatbv/float_bv.h>
+
 /// Gets the unbiased exponent in a floating-point bit-vector
 ///
 /// \todo Refactor with float_bv.cpp float_utils.h
diff --git a/src/solvers/strings/string_format_builtin_function.cpp b/src/solvers/strings/string_format_builtin_function.cpp
@@ -16,6 +16,8 @@ Author: Romain Brenguier, Joel Allred
 #include "format_specifier.h"
 #include "string_format_builtin_function.h"
 #include "string_refinement_util.h"
+
+#include <util/bitvector_expr.h>
 #include <util/range.h>
 #include <util/simplify_expr.h>
 #include <util/symbol_table.h>
diff --git a/src/util/Makefile b/src/util/Makefile
@@ -3,6 +3,7 @@ SRC = allocate_objects.cpp \
       array_element_from_pointer.cpp \
       array_name.cpp \
       base_type.cpp \
+      bitvector_expr.cpp \
       bv_arithmetic.cpp \
       byte_operators.cpp \
       c_types.cpp \
diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp
@@ -0,0 +1,42 @@
+/*******************************************************************\
+
+Module: API to expression classes for bitvectors
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "bitvector_expr.h"
+
+#include "arith_tools.h"
+#include "mathematical_types.h"
+
+shift_exprt::shift_exprt(
+  exprt _src,
+  const irep_idt &_id,
+  const std::size_t _distance)
+  : binary_exprt(std::move(_src), _id, from_integer(_distance, integer_typet()))
+{
+}
+
+extractbit_exprt::extractbit_exprt(exprt _src, const std::size_t _index)
+  : binary_predicate_exprt(
+      std::move(_src),
+      ID_extractbit,
+      from_integer(_index, integer_typet()))
+{
+}
+
+extractbits_exprt::extractbits_exprt(
+  exprt _src,
+  const std::size_t _upper,
+  const std::size_t _lower,
+  typet _type)
+  : expr_protectedt(ID_extractbits, std::move(_type))
+{
+  PRECONDITION(_upper >= _lower);
+  add_to_operands(
+    std::move(_src),
+    from_integer(_upper, integer_typet()),
+    from_integer(_lower, integer_typet()));
+}
diff --git a/src/util/bitvector_expr.h b/src/util/bitvector_expr.h
diff --git a/src/util/interval.cpp b/src/util/interval.cpp
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
