Skip to content

Commit 6c59fc8

Browse files
kroeningkroening
authored
Merge pull request #5759 from diffblue/bitvector_expr_h
move bitvector-related expression classes into separate header file
2 parents 0f57d77 + 7b0cc28 commit 6c59fc8

35 files changed

+772
-711
lines changed

‎jbmc/src/java_bytecode/character_refine_preprocess.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Date: March 2017
1616
#include "character_refine_preprocess.h"
1717

1818
#include <util/arith_tools.h>
19+
#include <util/bitvector_expr.h>
1920
#include <util/std_expr.h>
2021

2122
/// converts based on a function on expressions

‎jbmc/src/java_bytecode/java_string_library_preprocess.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,8 +17,10 @@ Date: April 2017
1717
/// java.lang.StringBuilder, java.lang.StringBuffer.
1818

1919
#include <goto-programs/class_identifier.h>
20+
2021
#include <util/allocate_objects.h>
2122
#include <util/arith_tools.h>
23+
#include <util/bitvector_expr.h>
2224
#include <util/c_types.h>
2325
#include <util/expr_initializer.h>
2426
#include <util/fresh_symbol.h>

‎scripts/expected_doxygen_warnings.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,7 @@ warning: Include graph for 'cbmc_parse_options.cpp' not generated, too many node
8383
warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8484
warning: Included by graph for 'goto_functions.h' not generated, too many nodes (66), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8585
warning: Included by graph for 'goto_model.h' not generated, too many nodes (109), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
86-
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (181), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
86+
warning: Included by graph for 'arith_tools.h' not generated, too many nodes (182), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8787
warning: Included by graph for 'c_types.h' not generated, too many nodes (110), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8888
warning: Included by graph for 'config.h' not generated, too many nodes (85), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
8989
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)
9696
warning: Included by graph for 'prefix.h' not generated, too many nodes (86), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9797
warning: Included by graph for 'simplify_expr.h' not generated, too many nodes (76), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
9898
warning: Included by graph for 'std_code.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
99-
warning: Included by graph for 'std_expr.h' not generated, too many nodes (247), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
99+
warning: Included by graph for 'std_expr.h' not generated, too many nodes (248), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
100100
warning: Included by graph for 'std_types.h' not generated, too many nodes (124), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
101101
warning: Included by graph for 'symbol_table.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.

‎src/analyses/goto_check.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515

1616
#include <util/arith_tools.h>
1717
#include <util/array_name.h>
18+
#include <util/bitvector_expr.h>
1819
#include <util/c_types.h>
1920
#include <util/config.h>
2021
#include <util/cprover_prefix.h>

‎src/analyses/goto_rw.cpp

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -14,15 +14,16 @@ Date: April 2010
1414
#include <limits>
1515
#include <memory>
1616

17-
#include <util/expr_util.h>
18-
#include <util/std_code.h>
19-
#include <util/std_expr.h>
20-
#include <util/pointer_offset_size.h>
17+
#include <util/arith_tools.h>
18+
#include <util/bitvector_expr.h>
2119
#include <util/byte_operators.h>
2220
#include <util/endianness_map.h>
23-
#include <util/arith_tools.h>
24-
#include <util/simplify_expr.h>
21+
#include <util/expr_util.h>
2522
#include <util/make_unique.h>
23+
#include <util/pointer_offset_size.h>
24+
#include <util/simplify_expr.h>
25+
#include <util/std_code.h>
26+
#include <util/std_expr.h>
2627

2728
#include <langapi/language_util.h>
2829

‎src/ansi-c/c_typecheck_base.h

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,13 @@ Author: Daniel Kroening, [email protected]
1212
#ifndef CPROVER_ANSI_C_C_TYPECHECK_BASE_H
1313
#define CPROVER_ANSI_C_C_TYPECHECK_BASE_H
1414

15-
#include <util/symbol_table.h>
16-
#include <util/typecheck.h>
15+
#include <util/bitvector_expr.h>
1716
#include <util/namespace.h>
1817
#include <util/std_code.h>
1918
#include <util/std_expr.h>
2019
#include <util/std_types.h>
20+
#include <util/symbol_table.h>
21+
#include <util/typecheck.h>
2122

2223
#include "ansi_c_declaration.h"
2324
#include "designator.h"

‎src/ansi-c/expr2c_class.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ Author: Daniel Kroening, [email protected]
1616
#include <unordered_map>
1717
#include <unordered_set>
1818

19+
#include <util/bitvector_expr.h>
1920
#include <util/byte_operators.h>
2021
#include <util/mathematical_expr.h>
2122
#include <util/std_code.h>

‎src/goto-programs/interpreter_evaluate.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111

1212
#include "interpreter_class.h"
1313

14+
#include <util/bitvector_expr.h>
1415
#include <util/byte_operators.h>
1516
#include <util/fixedbv.h>
1617
#include <util/ieee_float.h>

‎src/solvers/flattening/boolbv.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ Author: Daniel Kroening, [email protected]
1313
#include <set>
1414

1515
#include <util/arith_tools.h>
16+
#include <util/bitvector_expr.h>
1617
#include <util/magic.h>
1718
#include <util/mp_arith.h>
1819
#include <util/prefix.h>

‎src/solvers/flattening/boolbv.h

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,10 +26,13 @@ Author: Daniel Kroening, [email protected]
2626
#include "boolbv_map.h"
2727
#include "arrays.h"
2828

29+
class array_comprehension_exprt;
30+
class bswap_exprt;
31+
class concatenation_exprt;
2932
class extractbit_exprt;
3033
class extractbits_exprt;
31-
class array_comprehension_exprt;
3234
class member_exprt;
35+
class replication_exprt;
3336

3437
class boolbvt:public arrayst
3538
{

‎src/solvers/flattening/boolbv_bitwise.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,10 @@ Author: Daniel Kroening, [email protected]
66
77
\*******************************************************************/
88

9-
109
#include "boolbv.h"
1110

11+
#include <util/bitvector_expr.h>
12+
1213
bvt boolbvt::convert_bitwise(const exprt &expr)
1314
{
1415
const std::size_t width = boolbv_width(expr.type());

‎src/solvers/flattening/boolbv_bswap.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ Author: Michael Tautschnig
88

99
#include "boolbv.h"
1010

11+
#include <util/bitvector_expr.h>
1112
#include <util/invariant.h>
1213

1314
bvt boolbvt::convert_bswap(const bswap_exprt &expr)

‎src/solvers/flattening/boolbv_concatenation.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ Author: Daniel Kroening, [email protected]
88

99
#include "boolbv.h"
1010

11+
#include <util/bitvector_expr.h>
1112
#include <util/invariant.h>
1213

1314
bvt boolbvt::convert_concatenation(const concatenation_exprt &expr)

‎src/solvers/flattening/boolbv_extractbit.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#include <algorithm>
1212

1313
#include <util/arith_tools.h>
14+
#include <util/bitvector_expr.h>
1415
#include <util/exception_utils.h>
1516
#include <util/std_expr.h>
1617
#include <util/std_types.h>

‎src/solvers/flattening/boolbv_extractbits.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "boolbv.h"
1010

1111
#include <util/arith_tools.h>
12+
#include <util/bitvector_expr.h>
1213

1314
bvt boolbvt::convert_extractbits(const extractbits_exprt &expr)
1415
{

‎src/solvers/flattening/boolbv_replication.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "boolbv.h"
1010

1111
#include <util/arith_tools.h>
12+
#include <util/bitvector_expr.h>
1213

1314
bvt boolbvt::convert_replication(const replication_exprt &expr)
1415
{

‎src/solvers/flattening/bv_pointers.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
99
#include "bv_pointers.h"
1010

1111
#include <util/arith_tools.h>
12+
#include <util/bitvector_expr.h>
1213
#include <util/c_types.h>
1314
#include <util/config.h>
1415
#include <util/exception_utils.h>

‎src/solvers/floatbv/float_bv.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,8 +10,9 @@ Author: Daniel Kroening, [email protected]
1010

1111
#include <algorithm>
1212

13-
#include <util/std_expr.h>
1413
#include <util/arith_tools.h>
14+
#include <util/bitvector_expr.h>
15+
#include <util/std_expr.h>
1516

1617
exprt float_bvt::convert(const exprt &expr) const
1718
{

‎src/solvers/lowering/byte_operators.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#include <algorithm>
1212

1313
#include <util/arith_tools.h>
14+
#include <util/bitvector_expr.h>
1415
#include <util/byte_operators.h>
1516
#include <util/c_types.h>
1617
#include <util/endianness_map.h>

‎src/solvers/lowering/popcount.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: Michael Tautschnig
99
#include "expr_lowering.h"
1010

1111
#include <util/arith_tools.h>
12+
#include <util/bitvector_expr.h>
1213
#include <util/invariant.h>
1314
#include <util/pointer_offset_size.h>
1415
#include <util/std_expr.h>

‎src/solvers/qbf/qdimacs_core.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,7 @@ Author: CM Wintersteiger
99
#include "qdimacs_core.h"
1010

1111
#include <util/arith_tools.h>
12+
#include <util/bitvector_expr.h>
1213
#include <util/std_expr.h>
1314

1415
void qdimacs_coret::simplify_extractbits(exprt &expr) const

‎src/solvers/smt2/smt2_conv.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@ Author: Daniel Kroening, [email protected]
1212
#include "smt2_conv.h"
1313

1414
#include <util/arith_tools.h>
15+
#include <util/bitvector_expr.h>
1516
#include <util/c_types.h>
1617
#include <util/config.h>
1718
#include <util/expr_iterator.h>

‎src/solvers/smt2/smt2_parser.cpp

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#include "smt2_format.h"
1212

1313
#include <util/arith_tools.h>
14+
#include <util/bitvector_expr.h>
1415
#include <util/ieee_float.h>
1516
#include <util/invariant.h>
1617
#include <util/mathematical_expr.h>

‎src/solvers/strings/string_constraint_generator_float.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,10 +11,12 @@ Author: Romain Brenguier, [email protected]
1111
/// Generates string constraints for functions generating strings from other
1212
/// types, in particular int, long, float, double, char, bool
1313

14-
#include <solvers/floatbv/float_bv.h>
15-
1614
#include "string_constraint_generator.h"
1715

16+
#include <util/bitvector_expr.h>
17+
18+
#include <solvers/floatbv/float_bv.h>
19+
1820
/// Gets the unbiased exponent in a floating-point bit-vector
1921
///
2022
/// \todo Refactor with float_bv.cpp float_utils.h

‎src/solvers/strings/string_format_builtin_function.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ Author: Romain Brenguier, Joel Allred
1616
#include "format_specifier.h"
1717
#include "string_format_builtin_function.h"
1818
#include "string_refinement_util.h"
19+
20+
#include <util/bitvector_expr.h>
1921
#include <util/range.h>
2022
#include <util/simplify_expr.h>
2123
#include <util/symbol_table.h>

‎src/util/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ SRC = allocate_objects.cpp \
33
array_element_from_pointer.cpp \
44
array_name.cpp \
55
base_type.cpp \
6+
bitvector_expr.cpp \
67
bv_arithmetic.cpp \
78
byte_operators.cpp \
89
c_types.cpp \

‎src/util/bitvector_expr.cpp

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
/*******************************************************************\
2+
3+
Module: API to expression classes for bitvectors
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "bitvector_expr.h"
10+
11+
#include "arith_tools.h"
12+
#include "mathematical_types.h"
13+
14+
shift_exprt::shift_exprt(
15+
exprt _src,
16+
const irep_idt &_id,
17+
const std::size_t _distance)
18+
: binary_exprt(std::move(_src), _id, from_integer(_distance, integer_typet()))
19+
{
20+
}
21+
22+
extractbit_exprt::extractbit_exprt(exprt _src, const std::size_t _index)
23+
: binary_predicate_exprt(
24+
std::move(_src),
25+
ID_extractbit,
26+
from_integer(_index, integer_typet()))
27+
{
28+
}
29+
30+
extractbits_exprt::extractbits_exprt(
31+
exprt _src,
32+
const std::size_t _upper,
33+
const std::size_t _lower,
34+
typet _type)
35+
: expr_protectedt(ID_extractbits, std::move(_type))
36+
{
37+
PRECONDITION(_upper >= _lower);
38+
add_to_operands(
39+
std::move(_src),
40+
from_integer(_upper, integer_typet()),
41+
from_integer(_lower, integer_typet()));
42+
}

0 commit comments

Comments
 (0)