Skip to content

Commit 297e307

Browse files
kroeningkroening
authored
Merge pull request #5756 from diffblue/smt-lib2-qf-bv-ext
SMT-LIB2 QB_BV extensions
2 parents 6c59fc8 + da7d3bd commit 297e307

File tree

6 files changed

+179
-3
lines changed

6 files changed

+179
-3
lines changed

‎regression/smt2_solver/basic-bv1/weber_qf_bv.desc‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
KNOWNBUG
2+
weber_qf_bv.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--

‎regression/smt2_solver/basic-bv1/weber_qf_bv.smt2‎

Lines changed: 91 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,91 @@
1+
(set-info :smt-lib-version 2.6)
2+
(set-logic QF_BV)
3+
(set-info :source |
4+
Constructed by Tjark Weber to test that the extensions defined
5+
in QF_BV are implemented according to their definition
6+
|)
7+
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
8+
(set-info :category "check")
9+
(set-info :status unsat)
10+
; We use a (reasonably small) fixed bit width m > 0.
11+
(declare-fun s () (_ BitVec 5))
12+
(declare-fun t () (_ BitVec 5))
13+
(declare-fun u () (_ BitVec 5))
14+
(assert (not (and
15+
; Bitvector constants
16+
(= (_ bv13 32) #b00000000000000000000000000001101)
17+
; Bitwise operators
18+
(= (bvnand s t) (bvnot (bvand s t)))
19+
(= (bvnor s t) (bvnot (bvor s t)))
20+
(= (bvxor s t) (bvor (bvand s (bvnot t)) (bvand (bvnot s) t)))
21+
(= (bvxnor s t) (bvor (bvand s t) (bvand (bvnot s) (bvnot t))))
22+
(= (bvcomp s t) (bvand (bvxnor ((_ extract 4 4) s) ((_ extract 4 4) t))
23+
(bvcomp ((_ extract 3 0) s) ((_ extract 3 0) t))))
24+
(= (bvxor s t u) (bvxor (bvxor s t) u))
25+
; Arithmetic operators
26+
(= (bvsub s t) (bvadd s (bvneg t)))
27+
(= (bvsdiv s t) (let ((?msb_s ((_ extract 4 4) s))
28+
(?msb_t ((_ extract 4 4) t)))
29+
(ite (and (= ?msb_s #b0) (= ?msb_t #b0))
30+
(bvudiv s t)
31+
(ite (and (= ?msb_s #b1) (= ?msb_t #b0))
32+
(bvneg (bvudiv (bvneg s) t))
33+
(ite (and (= ?msb_s #b0) (= ?msb_t #b1))
34+
(bvneg (bvudiv s (bvneg t)))
35+
(bvudiv (bvneg s) (bvneg t)))))))
36+
(= (bvsrem s t) (let ((?msb_s ((_ extract 4 4) s))
37+
(?msb_t ((_ extract 4 4) t)))
38+
(ite (and (= ?msb_s #b0) (= ?msb_t #b0))
39+
(bvurem s t)
40+
(ite (and (= ?msb_s #b1) (= ?msb_t #b0))
41+
(bvneg (bvurem (bvneg s) t))
42+
(ite (and (= ?msb_s #b0) (= ?msb_t #b1))
43+
(bvurem s (bvneg t))
44+
(bvneg (bvurem (bvneg s) (bvneg t))))))))
45+
(= (bvsmod s t) (let ((?msb_s ((_ extract 4 4) s))
46+
(?msb_t ((_ extract 4 4) t)))
47+
(let ((abs_s (ite (= ?msb_s #b0) s (bvneg s)))
48+
(abs_t (ite (= ?msb_t #b0) t (bvneg t))))
49+
(let ((u (bvurem abs_s abs_t)))
50+
(ite (= u (_ bv0 5))
51+
u
52+
(ite (and (= ?msb_s #b0) (= ?msb_t #b0))
53+
u
54+
(ite (and (= ?msb_s #b1) (= ?msb_t #b0))
55+
(bvadd (bvneg u) t)
56+
(ite (and (= ?msb_s #b0) (= ?msb_t #b1))
57+
(bvadd u t)
58+
(bvneg u)))))))))
59+
(= (bvule s t) (or (bvult s t) (= s t)))
60+
(= (bvugt s t) (bvult t s))
61+
(= (bvuge s t) (or (bvult t s) (= s t)))
62+
(= (bvslt s t) (or (and (= ((_ extract 4 4) s) #b1)
63+
(= ((_ extract 4 4) t) #b0))
64+
(and (= ((_ extract 4 4) s) ((_ extract 4 4) t))
65+
(bvult s t))))
66+
(= (bvsle s t) (or (and (= ((_ extract 4 4) s) #b1)
67+
(= ((_ extract 4 4) t) #b0))
68+
(and (= ((_ extract 4 4) s) ((_ extract 4 4) t))
69+
(bvule s t))))
70+
(= (bvsgt s t) (bvslt t s))
71+
(= (bvsge s t) (bvsle t s))
72+
; Other operations
73+
(= (bvashr s t) (ite (= ((_ extract 4 4) s) #b0)
74+
(bvlshr s t)
75+
(bvnot (bvlshr (bvnot s) t))))
76+
(= ((_ repeat 1) t) t)
77+
(= ((_ repeat 2) t) (concat t ((_ repeat 1) t)))
78+
(= ((_ zero_extend 0) t) t)
79+
(= ((_ zero_extend 1) t) (concat ((_ repeat 1) #b0) t))
80+
(= ((_ sign_extend 0) t) t)
81+
(= ((_ sign_extend 1) t) (concat ((_ repeat 1) ((_ extract 4 4) t)) t))
82+
(= ((_ rotate_left 0) t) t)
83+
(= ((_ rotate_left 1) t) ((_ rotate_left 0)
84+
(concat ((_ extract 3 0) t) ((_ extract 4 4) t))))
85+
86+
(= ((_ rotate_right 0) t) t)
87+
(= ((_ rotate_right 1) t) ((_ rotate_right 0)
88+
(concat ((_ extract 0 0) t) ((_ extract 4 1) t))))
89+
)))
90+
(check-sat)
91+
(exit)

‎regression/smt2_solver/basic-bv1/weber_qf_bv_without_division.desc‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
weber_qf_bv_without_division.smt2
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^unsat$
7+
--

‎regression/smt2_solver/basic-bv1/weber_qf_bv_without_division.smt2‎

Lines changed: 59 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,59 @@
1+
(set-info :smt-lib-version 2.6)
2+
(set-logic QF_BV)
3+
(set-info :source |
4+
Constructed by Tjark Weber to test that the extensions defined
5+
in QF_BV are implemented according to their definition
6+
|)
7+
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
8+
(set-info :category "check")
9+
(set-info :status unsat)
10+
; We use a (reasonably small) fixed bit width m > 0.
11+
(declare-fun s () (_ BitVec 5))
12+
(declare-fun t () (_ BitVec 5))
13+
(declare-fun u () (_ BitVec 5))
14+
(assert (not (and
15+
; Bitvector constants
16+
(= (_ bv13 32) #b00000000000000000000000000001101)
17+
; Bitwise operators
18+
(= (bvnand s t) (bvnot (bvand s t)))
19+
(= (bvnor s t) (bvnot (bvor s t)))
20+
(= (bvxor s t) (bvor (bvand s (bvnot t)) (bvand (bvnot s) t)))
21+
(= (bvxnor s t) (bvor (bvand s t) (bvand (bvnot s) (bvnot t))))
22+
(= (bvcomp s t) (bvand (bvxnor ((_ extract 4 4) s) ((_ extract 4 4) t))
23+
(bvcomp ((_ extract 3 0) s) ((_ extract 3 0) t))))
24+
(= (bvxor s t u) (bvxor (bvxor s t) u))
25+
; Arithmetic operators
26+
(= (bvsub s t) (bvadd s (bvneg t)))
27+
(= (bvule s t) (or (bvult s t) (= s t)))
28+
(= (bvugt s t) (bvult t s))
29+
(= (bvuge s t) (or (bvult t s) (= s t)))
30+
(= (bvslt s t) (or (and (= ((_ extract 4 4) s) #b1)
31+
(= ((_ extract 4 4) t) #b0))
32+
(and (= ((_ extract 4 4) s) ((_ extract 4 4) t))
33+
(bvult s t))))
34+
(= (bvsle s t) (or (and (= ((_ extract 4 4) s) #b1)
35+
(= ((_ extract 4 4) t) #b0))
36+
(and (= ((_ extract 4 4) s) ((_ extract 4 4) t))
37+
(bvule s t))))
38+
(= (bvsgt s t) (bvslt t s))
39+
(= (bvsge s t) (bvsle t s))
40+
; Other operations
41+
(= (bvashr s t) (ite (= ((_ extract 4 4) s) #b0)
42+
(bvlshr s t)
43+
(bvnot (bvlshr (bvnot s) t))))
44+
(= ((_ repeat 1) t) t)
45+
(= ((_ repeat 2) t) (concat t ((_ repeat 1) t)))
46+
(= ((_ zero_extend 0) t) t)
47+
(= ((_ zero_extend 1) t) (concat ((_ repeat 1) #b0) t))
48+
(= ((_ sign_extend 0) t) t)
49+
(= ((_ sign_extend 1) t) (concat ((_ repeat 1) ((_ extract 4 4) t)) t))
50+
(= ((_ rotate_left 0) t) t)
51+
(= ((_ rotate_left 1) t) ((_ rotate_left 0)
52+
(concat ((_ extract 3 0) t) ((_ extract 4 4) t))))
53+
54+
(= ((_ rotate_right 0) t) t)
55+
(= ((_ rotate_right 1) t) ((_ rotate_right 0)
56+
(concat ((_ extract 0 0) t) ((_ extract 4 1) t))))
57+
)))
58+
(check-sat)
59+
(exit)

‎src/solvers/smt2/smt2_parser.cpp‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -675,7 +675,9 @@ exprt smt2_parsert::function_application()
675675
}
676676
else if(id == ID_repeat)
677677
{
678-
return nil_exprt();
678+
auto i = from_integer(index, integer_typet());
679+
auto width = to_unsignedbv_type(op[0].type()).get_width() * index;
680+
return replication_exprt(i, op[0], unsignedbv_typet(width));
679681
}
680682
else
681683
return nil_exprt();
@@ -871,6 +873,12 @@ void smt2_parsert::setup_expressions()
871873
return binary_predicate(ID_gt, cast_bv_to_signed(operands()));
872874
};
873875

876+
expressions["bvcomp"] = [this] {
877+
auto b0 = from_integer(0, unsignedbv_typet(1));
878+
auto b1 = from_integer(1, unsignedbv_typet(1));
879+
return if_exprt(binary_predicate(ID_equal, operands()), b1, b0);
880+
};
881+
874882
expressions["bvashr"] = [this] {
875883
return cast_bv_to_unsigned(binary(ID_ashr, cast_bv_to_signed(operands())));
876884
};

‎src/util/bitvector_expr.h‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -517,8 +517,12 @@ inline extractbits_exprt &to_extractbits_expr(exprt &expr)
517517
class replication_exprt : public binary_exprt
518518
{
519519
public:
520-
replication_exprt(const constant_exprt &_times, const exprt &_src)
521-
: binary_exprt(_times, ID_replication, _src)
520+
replication_exprt(constant_exprt _times, exprt _src, typet _type)
521+
: binary_exprt(
522+
std::move(_times),
523+
ID_replication,
524+
std::move(_src),
525+
std::move(_type))
522526
{
523527
}
524528

0 commit comments

Comments
 (0)