blob: 0004b356d2f8c2cd63baa2116f032d87e490658e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
|
;;;; TEMPORARY:
(declare trust-bad (th_holds false))
; helper stuff
(program mpz_sub ((x mpz) (y mpz)) mpz
(mp_add x (mp_mul (~1) y)))
(program mp_ispos ((x mpz)) formula
(mp_ifneg x false true))
(program mpz_eq ((x mpz) (y mpz)) formula
(mp_ifzero (mpz_sub x y) true false))
(program mpz_lt ((x mpz) (y mpz)) formula
(mp_ifneg (mpz_sub x y) true false))
(program mpz_lte ((x mpz) (y mpz)) formula
(mp_ifneg (mpz_sub x y) true (mpz_eq x y)))
(program mpz_ ((x mpz) (y mpz)) formula
(mp_ifzero (mpz_sub x y) true false))
; "bitvec" is a term of type "sort"
; (declare BitVec sort)
(declare BitVec (! n mpz sort))
; bit type
(declare bit type)
(declare b0 bit)
(declare b1 bit)
; bit vector type used for constants
(declare bv type)
(declare bvn bv)
(declare bvc (! b bit (! v bv bv)))
; calculate the length of a bitvector
;; (program bv_len ((v bv)) mpz
;; (match v
;; (bvn 0)
;; ((bvc b v') (mp_add (bv_len v') 1))))
; a bv constant term
(declare a_bv
(! n mpz
(! v bv
(term (BitVec n)))))
(program bv_constants_are_disequal ((x bv) (y bv)) formula
(match x
(bvn (fail formula))
((bvc bx x')
(match y
(bvn (fail formula))
((bvc by y') (match bx
(b0 (match by (b0 (bv_constants_are_disequal x' y')) (b1 (true))))
(b1 (match by (b0 (true)) (b1 (bv_constants_are_disequal x' y'))))
))
))
))
(declare bv_disequal_constants
(! n mpz
(! x bv
(! y bv
(! c (^ (bv_constants_are_disequal x y) true)
(th_holds (not (= (BitVec n) (a_bv n x) (a_bv n y)))))))))
; a bv variable
(declare var_bv type)
; a bv variable term
(declare a_var_bv
(! n mpz
(! v var_bv
(term (BitVec n)))))
; bit vector binary operators
(define bvop2
(! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
(term (BitVec n))))))
(declare bvand bvop2)
(declare bvor bvop2)
(declare bvor bvop2)
(declare bvxor bvop2)
(declare bvnand bvop2)
(declare bvnor bvop2)
(declare bvxnor bvop2)
(declare bvmul bvop2)
(declare bvadd bvop2)
(declare bvsub bvop2)
(declare bvudiv bvop2)
(declare bvurem bvop2)
(declare bvsdiv bvop2)
(declare bvsrem bvop2)
(declare bvsmod bvop2)
(declare bvshl bvop2)
(declare bvlshr bvop2)
(declare bvashr bvop2)
(declare concat bvop2)
; bit vector unary operators
(define bvop1
(! n mpz
(! x (term (BitVec n))
(term (BitVec n)))))
(declare bvneg bvop1)
(declare bvnot bvop1)
(declare rotate_left bvop1)
(declare rotate_right bvop1)
(declare bvcomp
(! n mpz
(! t1 (term (BitVec n))
(! t2 (term (BitVec n))
(term (BitVec 1))))))
(declare concat
(! n mpz
(! m mpz
(! m' mpz
(! t1 (term (BitVec m))
(! t2 (term (BitVec m'))
(term (BitVec n))))))))
;; side-condition fails in signature only??
;; (! s (^ (mp_add m m') n)
;; (declare repeat bvopp)
(declare extract
(! n mpz
(! i mpz
(! j mpz
(! m mpz
(! t2 (term (BitVec m))
(term (BitVec n))))))))
(declare zero_extend
(! n mpz
(! i mpz
(! m mpz
(! t2 (term (BitVec m))
(term (BitVec n)))))))
(declare sign_extend
(! n mpz
(! i mpz
(! m mpz
(! t2 (term (BitVec m))
(term (BitVec n)))))))
(declare repeat
(! n mpz
(! i mpz
(! m mpz
(! t2 (term (BitVec m))
(term (BitVec n)))))))
;; TODO: add checks for valid typing for these operators
;; (! c1 (^ (mpz_lte i j)
;; (! c2 (^ (mpz_lt i n) true)
;; (! c3 (^ (mp_ifneg i false true) true)
;; (! c4 (^ (mp_ifneg j false true) true)
;; (! s (^ (mp_add (mpz_sub i j) 1) m)
; bit vector predicates
(define bvpred
(! n mpz
(! x (term (BitVec n))
(! y (term (BitVec n))
formula))))
(declare bvult bvpred)
(declare bvule bvpred)
(declare bvugt bvpred)
(declare bvuge bvpred)
(declare bvslt bvpred)
(declare bvsle bvpred)
(declare bvsgt bvpred)
(declare bvsge bvpred)
|
