Skip to content

Commit 3f670cc

Browse files
thomasspriggsthomasspriggs
committed
Add bitvector theory predicates
1 parent 8952469 commit 3f670cc

File tree

6 files changed

+250
-0
lines changed

6 files changed

+250
-0
lines changed

‎src/solvers/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,7 @@ SRC = $(BOOLEFORCE_SRC) \
192192
smt2/smt2_parser.cpp \
193193
smt2/smt2_tokenizer.cpp \
194194
smt2/smt2irep.cpp \
195+
smt2_incremental/smt_bitvector_theory.cpp \
195196
smt2_incremental/smt_commands.cpp \
196197
smt2_incremental/smt_logics.cpp \
197198
smt2_incremental/smt_options.cpp \

‎src/solvers/smt2_incremental/smt_bitvector_theory.cpp

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,42 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <solvers/smt2_incremental/smt_bitvector_theory.h>
4+
5+
#include <util/invariant.h>
6+
7+
static void validate_bitvector_predicate_arguments(
8+
const smt_termt &left,
9+
const smt_termt &right)
10+
{
11+
const auto left_sort = left.get_sort().cast<smt_bit_vector_sortt>();
12+
INVARIANT(left_sort, "Left operand must have bitvector sort.");
13+
const auto right_sort = right.get_sort().cast<smt_bit_vector_sortt>();
14+
INVARIANT(right_sort, "Right operand must have bitvector sort.");
15+
INVARIANT(
16+
left_sort->bit_width() == right_sort->bit_width(),
17+
"Left and right operands must have the same bit width.");
18+
}
19+
20+
#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \
21+
void smt_bit_vector_theoryt::the_name##t::validate( \
22+
const smt_termt &left, const smt_termt &right) \
23+
{ \
24+
validate_bitvector_predicate_arguments(left, right); \
25+
} \
26+
\
27+
smt_sortt smt_bit_vector_theoryt::the_name##t::return_sort( \
28+
const smt_termt &, const smt_termt &) \
29+
{ \
30+
return smt_bool_sortt{}; \
31+
} \
32+
\
33+
const char *smt_bit_vector_theoryt::the_name##t::identifier() \
34+
{ \
35+
return #the_identifier; \
36+
} \
37+
\
38+
const smt_function_application_termt::factoryt< \
39+
smt_bit_vector_theoryt::the_name##t> \
40+
smt_bit_vector_theoryt::the_name{};
41+
#include "smt_bitvector_theory.def"
42+
#undef SMT_BITVECTOR_THEORY_PREDICATE

‎src/solvers/smt2_incremental/smt_bitvector_theory.def

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
/// \file
2+
/// This set of definitions is used as part of the
3+
/// [X-macro](https://en.wikipedia.org/wiki/X_Macro) pattern. These define the
4+
/// set of bitvector theory functions which are implemented and it is used to
5+
/// automate repetitive parts of the implementation.
6+
SMT_BITVECTOR_THEORY_PREDICATE(bvult, unsigned_less_than)
7+
SMT_BITVECTOR_THEORY_PREDICATE(bvule, unsigned_less_than_or_equal)
8+
SMT_BITVECTOR_THEORY_PREDICATE(bvugt, unsigned_greater_than)
9+
SMT_BITVECTOR_THEORY_PREDICATE(bvuge, unsigned_greater_than_or_equal)
10+
SMT_BITVECTOR_THEORY_PREDICATE(bvslt, signed_less_than)
11+
SMT_BITVECTOR_THEORY_PREDICATE(bvsle, signed_less_than_or_equal)
12+
SMT_BITVECTOR_THEORY_PREDICATE(bvsgt, signed_greater_than)
13+
SMT_BITVECTOR_THEORY_PREDICATE(bvsge, signed_greater_than_or_equal)

‎src/solvers/smt2_incremental/smt_bitvector_theory.h

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
// Author: Diffblue Ltd.
2+
3+
#ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BITVECTOR_THEORY_H
4+
#define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BITVECTOR_THEORY_H
5+
6+
#include <solvers/smt2_incremental/smt_terms.h>
7+
8+
class smt_bit_vector_theoryt
9+
{
10+
public:
11+
#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \
12+
/* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */ \
13+
struct the_name##t final \
14+
{ \
15+
static const char *identifier(); \
16+
static smt_sortt \
17+
return_sort(const smt_termt &left, const smt_termt &right); \
18+
static void validate(const smt_termt &left, const smt_termt &right); \
19+
}; \
20+
static const smt_function_application_termt::factoryt<the_name##t> the_name;
21+
#include "smt_bitvector_theory.def"
22+
#undef SMT_BITVECTOR_THEORY_PREDICATE
23+
};
24+
25+
#endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BITVECTOR_THEORY_H

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,7 @@ SRC += analyses/ai/ai.cpp \
8585
solvers/sat/satcheck_cadical.cpp \
8686
solvers/sat/satcheck_minisat2.cpp \
8787
solvers/smt2/smt2_conv.cpp \
88+
solvers/smt2_incremental/smt_bit_vector_theory.cpp \
8889
solvers/smt2_incremental/smt_commands.cpp \
8990
solvers/smt2_incremental/smt_sorts.cpp \
9091
solvers/smt2_incremental/smt_terms.cpp \

‎unit/solvers/smt2_incremental/smt_bitvector_theory.cpp

Lines changed: 168 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,168 @@
1+
// Author: Diffblue Ltd.
2+
3+
#include <testing-utils/use_catch.h>
4+
5+
#include <solvers/smt2_incremental/smt_bitvector_theory.h>
6+
#include <solvers/smt2_incremental/smt_terms.h>
7+
8+
#include <util/mp_arith.h>
9+
10+
TEST_CASE("SMT bit vector predicates", "[core][smt2_incremental]")
11+
{
12+
const smt_bit_vector_constant_termt two{2, 8};
13+
const smt_bit_vector_constant_termt three{3, 8};
14+
const smt_bool_literal_termt false_term{false};
15+
const smt_bit_vector_constant_termt wider{2, 16};
16+
SECTION("unsigned less than")
17+
{
18+
const auto function_application =
19+
smt_bit_vector_theoryt::unsigned_less_than(two, three);
20+
REQUIRE(
21+
function_application.function_identifier() ==
22+
smt_identifier_termt("bvult", smt_bool_sortt{}));
23+
REQUIRE(function_application.get_sort() == smt_bool_sortt{});
24+
REQUIRE(function_application.arguments().size() == 2);
25+
REQUIRE(function_application.arguments()[0].get() == two);
26+
REQUIRE(function_application.arguments()[1].get() == three);
27+
cbmc_invariants_should_throwt invariants_throw;
28+
CHECK_THROWS(smt_bit_vector_theoryt::unsigned_less_than(false_term, two));
29+
CHECK_THROWS(smt_bit_vector_theoryt::unsigned_less_than(two, false_term));
30+
CHECK_THROWS(smt_bit_vector_theoryt::unsigned_less_than(wider, two));
31+
CHECK_THROWS(smt_bit_vector_theoryt::unsigned_less_than(two, wider));
32+
}
33+
SECTION("unsigned less than or equal")
34+
{
35+
const auto function_application =
36+
smt_bit_vector_theoryt::unsigned_less_than_or_equal(two, three);
37+
REQUIRE(
38+
function_application.function_identifier() ==
39+
smt_identifier_termt("bvule", smt_bool_sortt{}));
40+
REQUIRE(function_application.get_sort() == smt_bool_sortt{});
41+
REQUIRE(function_application.arguments().size() == 2);
42+
REQUIRE(function_application.arguments()[0].get() == two);
43+
REQUIRE(function_application.arguments()[1].get() == three);
44+
cbmc_invariants_should_throwt invariants_throw;
45+
CHECK_THROWS(
46+
smt_bit_vector_theoryt::unsigned_less_than_or_equal(false_term, two));
47+
CHECK_THROWS(
48+
smt_bit_vector_theoryt::unsigned_less_than_or_equal(two, false_term));
49+
CHECK_THROWS(
50+
smt_bit_vector_theoryt::unsigned_less_than_or_equal(wider, two));
51+
CHECK_THROWS(
52+
smt_bit_vector_theoryt::unsigned_less_than_or_equal(two, wider));
53+
}
54+
SECTION("unsigned greater than")
55+
{
56+
const auto function_application =
57+
smt_bit_vector_theoryt::unsigned_greater_than(two, three);
58+
REQUIRE(
59+
function_application.function_identifier() ==
60+
smt_identifier_termt("bvugt", smt_bool_sortt{}));
61+
REQUIRE(function_application.get_sort() == smt_bool_sortt{});
62+
REQUIRE(function_application.arguments().size() == 2);
63+
REQUIRE(function_application.arguments()[0].get() == two);
64+
REQUIRE(function_application.arguments()[1].get() == three);
65+
cbmc_invariants_should_throwt invariants_throw;
66+
CHECK_THROWS(
67+
smt_bit_vector_theoryt::unsigned_greater_than(false_term, two));
68+
CHECK_THROWS(
69+
smt_bit_vector_theoryt::unsigned_greater_than(two, false_term));
70+
CHECK_THROWS(smt_bit_vector_theoryt::unsigned_greater_than(wider, two));
71+
CHECK_THROWS(smt_bit_vector_theoryt::unsigned_greater_than(two, wider));
72+
}
73+
SECTION("unsigned greater than or equal")
74+
{
75+
const auto function_application =
76+
smt_bit_vector_theoryt::unsigned_greater_than_or_equal(two, three);
77+
REQUIRE(
78+
function_application.function_identifier() ==
79+
smt_identifier_termt("bvuge", smt_bool_sortt{}));
80+
REQUIRE(function_application.get_sort() == smt_bool_sortt{});
81+
REQUIRE(function_application.arguments().size() == 2);
82+
REQUIRE(function_application.arguments()[0].get() == two);
83+
REQUIRE(function_application.arguments()[1].get() == three);
84+
cbmc_invariants_should_throwt invariants_throw;
85+
CHECK_THROWS(
86+
smt_bit_vector_theoryt::unsigned_greater_than_or_equal(false_term, two));
87+
CHECK_THROWS(
88+
smt_bit_vector_theoryt::unsigned_greater_than_or_equal(two, false_term));
89+
CHECK_THROWS(
90+
smt_bit_vector_theoryt::unsigned_greater_than_or_equal(wider, two));
91+
CHECK_THROWS(
92+
smt_bit_vector_theoryt::unsigned_greater_than_or_equal(two, wider));
93+
}
94+
SECTION("signed less than")
95+
{
96+
const auto function_application =
97+
smt_bit_vector_theoryt::signed_less_than(two, three);
98+
REQUIRE(
99+
function_application.function_identifier() ==
100+
smt_identifier_termt("bvslt", smt_bool_sortt{}));
101+
REQUIRE(function_application.get_sort() == smt_bool_sortt{});
102+
REQUIRE(function_application.arguments().size() == 2);
103+
REQUIRE(function_application.arguments()[0].get() == two);
104+
REQUIRE(function_application.arguments()[1].get() == three);
105+
cbmc_invariants_should_throwt invariants_throw;
106+
CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than(false_term, two));
107+
CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than(two, false_term));
108+
CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than(wider, two));
109+
CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than(two, wider));
110+
}
111+
SECTION("signed less than or equal")
112+
{
113+
const auto function_application =
114+
smt_bit_vector_theoryt::signed_less_than_or_equal(two, three);
115+
REQUIRE(
116+
function_application.function_identifier() ==
117+
smt_identifier_termt("bvsle", smt_bool_sortt{}));
118+
REQUIRE(function_application.get_sort() == smt_bool_sortt{});
119+
REQUIRE(function_application.arguments().size() == 2);
120+
REQUIRE(function_application.arguments()[0].get() == two);
121+
REQUIRE(function_application.arguments()[1].get() == three);
122+
cbmc_invariants_should_throwt invariants_throw;
123+
CHECK_THROWS(
124+
smt_bit_vector_theoryt::signed_less_than_or_equal(false_term, two));
125+
CHECK_THROWS(
126+
smt_bit_vector_theoryt::signed_less_than_or_equal(two, false_term));
127+
CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than_or_equal(wider, two));
128+
CHECK_THROWS(smt_bit_vector_theoryt::signed_less_than_or_equal(two, wider));
129+
}
130+
SECTION("signed greater than")
131+
{
132+
const auto function_application =
133+
smt_bit_vector_theoryt::signed_greater_than(two, three);
134+
REQUIRE(
135+
function_application.function_identifier() ==
136+
smt_identifier_termt("bvsgt", smt_bool_sortt{}));
137+
REQUIRE(function_application.get_sort() == smt_bool_sortt{});
138+
REQUIRE(function_application.arguments().size() == 2);
139+
REQUIRE(function_application.arguments()[0].get() == two);
140+
REQUIRE(function_application.arguments()[1].get() == three);
141+
cbmc_invariants_should_throwt invariants_throw;
142+
CHECK_THROWS(smt_bit_vector_theoryt::signed_greater_than(false_term, two));
143+
CHECK_THROWS(smt_bit_vector_theoryt::signed_greater_than(two, false_term));
144+
CHECK_THROWS(smt_bit_vector_theoryt::signed_greater_than(wider, two));
145+
CHECK_THROWS(smt_bit_vector_theoryt::signed_greater_than(two, wider));
146+
}
147+
SECTION("signed greater than or equal")
148+
{
149+
const auto function_application =
150+
smt_bit_vector_theoryt::signed_greater_than_or_equal(two, three);
151+
REQUIRE(
152+
function_application.function_identifier() ==
153+
smt_identifier_termt("bvsge", smt_bool_sortt{}));
154+
REQUIRE(function_application.get_sort() == smt_bool_sortt{});
155+
REQUIRE(function_application.arguments().size() == 2);
156+
REQUIRE(function_application.arguments()[0].get() == two);
157+
REQUIRE(function_application.arguments()[1].get() == three);
158+
cbmc_invariants_should_throwt invariants_throw;
159+
CHECK_THROWS(
160+
smt_bit_vector_theoryt::signed_greater_than_or_equal(false_term, two));
161+
CHECK_THROWS(
162+
smt_bit_vector_theoryt::signed_greater_than_or_equal(two, false_term));
163+
CHECK_THROWS(
164+
smt_bit_vector_theoryt::signed_greater_than_or_equal(wider, two));
165+
CHECK_THROWS(
166+
smt_bit_vector_theoryt::signed_greater_than_or_equal(two, wider));
167+
}
168+
}

0 commit comments

Comments
 (0)