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
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Overflows.Arithmetic
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test suite for overflow checking
-----------------------------------------------------------------------------
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Overflows.Arithmetic(tests) where
import Data.SBV
import Data.SBV.Dynamic
import Data.SBV.Internals (unSBV, SBV(..))
import Data.SBV.Tools.Overflow
import Utils.SBVTestFramework
-- Test suite
tests :: TestTree
tests = testGroup "Overflows" [testGroup "Arithmetic" ts]
where ts = [ testGroup "add-uf" [ testCase "w8" $ assertIsThm $ underflow svPlus (bvAddO :: SWord8 -> SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ underflow svPlus (bvAddO :: SWord16 -> SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ underflow svPlus (bvAddO :: SWord32 -> SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ underflow svPlus (bvAddO :: SWord64 -> SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ underflow svPlus (bvAddO :: SInt8 -> SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ underflow svPlus (bvAddO :: SInt16 -> SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ underflow svPlus (bvAddO :: SInt32 -> SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ underflow svPlus (bvAddO :: SInt64 -> SInt64 -> (SBool, SBool))
]
, testGroup "add-of" [ testCase "w8" $ assertIsThm $ overflow svPlus (bvAddO :: SWord8 -> SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ overflow svPlus (bvAddO :: SWord16 -> SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ overflow svPlus (bvAddO :: SWord32 -> SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ overflow svPlus (bvAddO :: SWord64 -> SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ overflow svPlus (bvAddO :: SInt8 -> SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ overflow svPlus (bvAddO :: SInt16 -> SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ overflow svPlus (bvAddO :: SInt32 -> SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ overflow svPlus (bvAddO :: SInt64 -> SInt64 -> (SBool, SBool))
]
, testGroup "sub-uf" [ testCase "w8" $ assertIsThm $ underflow svMinus (bvSubO :: SWord8 -> SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ underflow svMinus (bvSubO :: SWord16 -> SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ underflow svMinus (bvSubO :: SWord32 -> SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ underflow svMinus (bvSubO :: SWord64 -> SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ underflow svMinus (bvSubO :: SInt8 -> SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ underflow svMinus (bvSubO :: SInt16 -> SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ underflow svMinus (bvSubO :: SInt32 -> SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ underflow svMinus (bvSubO :: SInt64 -> SInt64 -> (SBool, SBool))
]
, testGroup "sub-of" [ testCase "w8" $ assertIsThm $ overflow svMinus (bvSubO :: SWord8 -> SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ overflow svMinus (bvSubO :: SWord16 -> SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ overflow svMinus (bvSubO :: SWord32 -> SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ overflow svMinus (bvSubO :: SWord64 -> SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ overflow svMinus (bvSubO :: SInt8 -> SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ overflow svMinus (bvSubO :: SInt16 -> SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ overflow svMinus (bvSubO :: SInt32 -> SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ overflow svMinus (bvSubO :: SInt64 -> SInt64 -> (SBool, SBool))
]
, testGroup "mul-uf" [ testCase "w8" $ assertIsThm $ underflow svTimes (bvMulO :: SWord8 -> SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ underflow svTimes (bvMulO :: SWord16 -> SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ underflow svTimes (bvMulO :: SWord32 -> SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ underflow svTimes (bvMulO :: SWord64 -> SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt8 -> SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt16 -> SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt32 -> SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ mulChkU bvMulOFast (bvMulO :: SInt64 -> SInt64 -> (SBool, SBool))
]
, testGroup "mul-of" [ testCase "w8" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord8 -> SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord16 -> SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord32 -> SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SWord64 -> SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt8 -> SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt16 -> SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt32 -> SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ mulChkO bvMulOFast (bvMulO :: SInt64 -> SInt64 -> (SBool, SBool))
]
, testGroup "div-uf" [ testCase "w8" $ assertIsThm $ never svDivide (bvDivO :: SWord8 -> SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ never svDivide (bvDivO :: SWord16 -> SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ never svDivide (bvDivO :: SWord32 -> SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ never svDivide (bvDivO :: SWord64 -> SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ never svDivide (bvDivO :: SInt8 -> SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ never svDivide (bvDivO :: SInt16 -> SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ never svDivide (bvDivO :: SInt32 -> SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ never svDivide (bvDivO :: SInt64 -> SInt64 -> (SBool, SBool))
]
, testGroup "div-of" [ testCase "w8" $ assertIsThm $ never svDivide (bvDivO :: SWord8 -> SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ never svDivide (bvDivO :: SWord16 -> SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ never svDivide (bvDivO :: SWord32 -> SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ never svDivide (bvDivO :: SWord64 -> SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ divChk svDivide (bvDivO :: SInt8 -> SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ divChk svDivide (bvDivO :: SInt16 -> SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ divChk svDivide (bvDivO :: SInt32 -> SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ divChk svDivide (bvDivO :: SInt64 -> SInt64 -> (SBool, SBool))
]
, testGroup "neg-uf" [ testCase "w8" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ underflow1 svNeg0 (bvNegO :: SInt64 -> (SBool, SBool))
]
, testGroup "neg-of" [ testCase "w8" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord8 -> (SBool, SBool))
, testCase "w16" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord16 -> (SBool, SBool))
, testCase "w32" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord32 -> (SBool, SBool))
, testCase "w64" $ assertIsThm $ never1 svNeg0 (bvNegO :: SWord64 -> (SBool, SBool))
, testCase "i8" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt8 -> (SBool, SBool))
, testCase "i16" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt16 -> (SBool, SBool))
, testCase "i32" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt32 -> (SBool, SBool))
, testCase "i64" $ assertIsThm $ overflow1 svNeg0 (bvNegO :: SInt64 -> (SBool, SBool))
]
]
-- 256 bits is large enough to do all these proofs
large :: Int
large = 256
type SLarge = SVal
svNeg0 :: SLarge -> SLarge
svNeg0 v = z `svMinus` v
where z = svInteger (KBounded (hasSign v) large) 0
exactlyWhen :: SBool -> SVal -> SBool
exactlyWhen (SBV a) b = SBV $ (a `svAnd` b) `svOr` (svNot a `svAnd` svNot b)
-- Properly extend to a dynamic signed large vector. This works because we grow to 256 bits, which is high enough.
toLarge :: HasKind a => SBV a -> SLarge
toLarge v
| extra < 0 = error $ "toLarge: Unexpected size: " ++ show (n, large)
| hasSign v = svSignExtend extra (unSBV v)
| True = mkSigned $ svZeroExtend extra (unSBV v)
where n = intSizeOf v
extra = large - n
mkSigned = svFromIntegral (KBounded True large)
-- Multiplication checks are expensive. For these, we simply check that the SBV encodings and the z3 versions are equivalent
mulChkO :: forall a. SymVal a => (SBV a -> SBV a -> (SBool, SBool)) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
mulChkO fast slow = do setLogic Logic_NONE
x <- free "x"
y <- free "y"
let (_, ov1) = x `fast` y
(_, ov2) = x `slow` y
return $ ov1 .== ov2
-- Underflow mults
mulChkU :: forall a. SymVal a => (SBV a -> SBV a -> (SBool, SBool)) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
mulChkU fast slow = do setLogic Logic_NONE
x <- free "x"
y <- free "y"
let (uf1, _) = x `fast` y
(uf2, _) = x `slow` y
return $ uf1 .== uf2
-- Signed division can only underflow under one condition, check that simply instead of trying to do an expensive embedding proof
divChk :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
divChk _op cond = do x <- free "x"
y <- free "y"
let (_, overflowHappens) = x `cond` y
special = (unSBV x `svEqual` topSet) `svAnd` (unSBV y `svEqual` neg1)
n = intSizeOf x
neg1 = svInteger (KBounded True n) (-1)
topSet = svInteger (KBounded True n) (2^(n-1))
return $ overflowHappens `exactlyWhen` special
-- For a few cases, we expect them to "never" overflow. The "embedding proofs" are either too expensive (in case of division), or
-- not possible (in case of negation). We capture these here.
never :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
never _op cond = do x <- free "x"
y <- free "y"
let (underflowHappens, _) = x `cond` y
return $ underflowHappens `exactlyWhen` svFalse
never1 :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate
never1 _op cond = do x <- free "x"
let (underflowHappens, _) = cond x
return $ underflowHappens `exactlyWhen` svFalse
underflow :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
underflow op cond = do x <- free "x"
y <- free "y"
let (underflowHappens, _) = x `cond` y
extResult :: SLarge
extResult = toLarge x `op` toLarge y
return $ underflowHappens `exactlyWhen` (extResult `svLessThan` toLarge (minBound :: SBV a))
overflow :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge -> SLarge) -> (SBV a -> SBV a -> (SBool, SBool)) -> Predicate
overflow op cond = do x <- free "x"
y <- free "y"
let (_, overflowHappens) = x `cond` y
extResult :: SLarge
extResult = toLarge x `op` toLarge y
return $ overflowHappens `exactlyWhen` (extResult `svGreaterThan` toLarge (maxBound :: SBV a))
underflow1 :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate
underflow1 op cond = do x <- free "x"
let (underflowHappens, _) = cond x
extResult :: SLarge
extResult = op $ toLarge x
return $ underflowHappens `exactlyWhen` (extResult `svLessThan` toLarge (minBound :: SBV a))
overflow1 :: forall a. (Integral a, Bounded a, SymVal a) => (SLarge -> SLarge) -> (SBV a -> (SBool, SBool)) -> Predicate
overflow1 op cond = do x <- free "x"
let (_, overflowHappens) = cond x
extResult :: SLarge
extResult = op $ toLarge x
return $ overflowHappens `exactlyWhen` (extResult `svGreaterThan` toLarge (maxBound :: SBV a))
{- HLint ignore module "Reduce duplication" -}
|
