1{-# LANGUAGE DataKinds #-}
2{-# LANGUAGE FlexibleContexts #-}
3{-# LANGUAGE LambdaCase #-}
4{-# LANGUAGE OverloadedStrings #-}
5{-# LANGUAGE RankNTypes #-}
6{-# LANGUAGE TypeFamilies #-}
7{-# LANGUAGE TypeApplications #-}
8
9{-|
10Module      : ExprsTest test
11Copyright   : (c) Galois Inc, 2020
12License     : BSD3
13Maintainer  : kquick@galois.com
14
15This module provides some verification of selected What4 Expressions.
16There are a number of simplifications, subsumptions, and other rewrite
17rules used for these What4 expressions; this module is intended to
18verify the correctness of those.
19-}
20
21import           Control.Monad.IO.Class ( liftIO )
22import           Data.Bits
23import qualified Data.BitVector.Sized as BV
24import           Data.Parameterized.Nonce
25import           GenWhat4Expr
26import           Hedgehog
27import qualified Hedgehog.Gen as Gen
28import qualified Hedgehog.Range as Range
29import           Test.Tasty
30import           Test.Tasty.HUnit
31import           Test.Tasty.Hedgehog
32import           What4.Concrete
33import           What4.Expr
34import           What4.Interface
35
36
37data State t = State
38type IteExprBuilder t fs = ExprBuilder t State fs
39
40withTestSolver :: (forall t. IteExprBuilder t (Flags FloatIEEE) -> IO a) -> IO a
41withTestSolver f = withIONonceGenerator $ \nonce_gen ->
42  f =<< newExprBuilder FloatIEEERepr State nonce_gen
43
44
45-- | Test natDiv and natMod properties described at their declaration
46-- site in What4.Interface
47testIntDivModProps :: TestTree
48testIntDivModProps =
49  testProperty "d <- intDiv sym x y; m <- intMod sym x y ===> y * d + m == x and 0 <= m < y" $
50  property $ do
51    xn <- forAll $ Gen.integral $ Range.linear (negate 1000) (1000 :: Integer)
52    -- no zero; avoid div-by-zero
53    yn <- forAll $ (Gen.choice [ Gen.integral $ Range.linear 1 (2000 :: Integer)
54                               , Gen.integral $ Range.linear (-2000) (-1)])
55    dm <- liftIO $ withTestSolver $ \sym -> do
56      x <- intLit sym xn
57      y <- intLit sym yn
58      d <- intDiv sym x y
59      m <- intMod sym x y
60      return (asConcrete d, asConcrete m)
61    case dm of
62      (Just dnc, Just mnc) -> do
63        let dn = fromConcreteInteger dnc
64        let mn = fromConcreteInteger mnc
65        annotateShow (xn, yn, dn, mn)
66        yn * dn + mn === xn
67        diff mn (\m y -> 0 <= m && m < abs y) yn
68      _ -> failure
69
70testInt :: TestTree
71testInt = testGroup "int operators"
72  [ testProperty "n * m == m * n" $
73    property $ do
74      n <- forAll $ Gen.integral $ Range.linear (-1000) 1000
75      m <- forAll $ Gen.integral $ Range.linear (-1000) 1000
76      (nm, mn) <- liftIO $ withTestSolver $ \sym -> do
77        n_lit <- intLit sym n
78        m_lit <- intLit sym m
79        nm <- intMul sym n_lit m_lit
80        mn <- intMul sym m_lit n_lit
81        return (asConcrete nm, asConcrete mn)
82      nm === mn
83  , testProperty "|n| >= 0" $
84    property $ do
85      n_random <- forAll $ Gen.integral $ Range.linear (-1000) 10
86      n_abs <- liftIO $ withTestSolver $ \sym -> do
87        n <- intLit sym n_random
88        n_abs <- intAbs sym n
89        return (asConcrete n_abs)
90      case fromConcreteInteger <$> n_abs of
91        Just nabs -> do
92          nabs === abs n_random
93          diff nabs (>=) 0
94        _ -> failure
95  , testIntDivMod
96  ]
97
98testIntDivMod :: TestTree
99testIntDivMod = testGroup "integer division and mod"
100  [ testProperty "y * (div x y) + (mod x y) == x" $
101    property $ do
102      x <- forAll $ Gen.integral $ Range.linear (-1000) 1000
103      y <- forAll $ Gen.choice -- skip 0
104           [ Gen.integral $ Range.linear (-1000) (-1)
105           , Gen.integral $ Range.linear 1 1000
106           ]
107      result <- liftIO $ withTestSolver $ \sym -> do
108        x_lit <- intLit sym x
109        y_lit <- intLit sym y
110        divxy <- intDiv sym x_lit y_lit
111        modxy <- intMod sym x_lit y_lit
112        return (asConcrete y_lit, asConcrete divxy, asConcrete modxy, asConcrete x_lit)
113      case result of
114        (Just y_c, Just divxy_c, Just modxy_c, Just x_c) -> do
115          let y' = fromConcreteInteger y_c
116          let x' = fromConcreteInteger x_c
117          let divxy = fromConcreteInteger divxy_c
118          let modxy = fromConcreteInteger modxy_c
119          y' * divxy + modxy === x'
120          diff 0 (<=) modxy
121          diff modxy (<) (abs y')
122        _ -> failure
123  , testProperty "mod x y == mod x (- y) == mod x (abs y)" $
124    property $ do
125      x <- forAll $ Gen.integral $ Range.linear (-1000) 1000
126      y <- forAll $ Gen.choice -- skip 0
127           [ Gen.integral $ Range.linear (-1000) (-1)
128           , Gen.integral $ Range.linear 1 1000
129           ]
130      result <- liftIO $ withTestSolver $ \sym -> do
131        x_lit <- intLit sym x
132        y_lit <- intLit sym y
133        modxy <- intMod sym x_lit y_lit
134        y_neg <- intLit sym (-y)
135        y_abs <- intAbs sym y_lit
136        modxNegy <- intMod sym x_lit y_neg
137        modxAbsy <- intMod sym x_lit y_abs
138        return (asConcrete modxy, asConcrete modxNegy, asConcrete modxAbsy)
139      case result of
140        (Just modxy_c, Just modxNegy_c, Just modxAbsy_c) -> do
141          let modxy = fromConcreteInteger modxy_c
142          let modxNegy = fromConcreteInteger modxNegy_c
143          let modxAbsy = fromConcreteInteger modxAbsy_c
144          annotateShow (modxy, modxNegy)
145          modxy === modxNegy
146          annotateShow (modxNegy, modxAbsy)
147          modxNegy === modxAbsy
148        _ -> failure
149  , testProperty "div x (-y) == -(div x y)" $
150    property $ do
151      x <- forAll $ Gen.integral $ Range.linear (-1000) 1000
152      y <- forAll $ Gen.choice -- skip 0
153           [ Gen.integral $ Range.linear (-1000) (-1)
154           , Gen.integral $ Range.linear 1 1000
155           ]
156      result <- liftIO $ withTestSolver $ \sym -> do
157        x_lit <- intLit sym x
158        y_lit <- intLit sym y
159        divxy <- intDiv sym x_lit y_lit
160        y_neg <- intLit sym (-y)
161        divxNegy <- intDiv sym x_lit y_neg
162        negdivxy <- intNeg sym divxy
163        return (asConcrete divxNegy, asConcrete negdivxy)
164      case result of
165        (Just divxNegy_c, Just negdivxy_c) -> do
166          let divxNegy = fromConcreteInteger divxNegy_c
167          let negdivxy = fromConcreteInteger negdivxy_c
168          divxNegy === negdivxy
169        _ -> failure
170  ]
171
172testBvIsNeg :: TestTree
173testBvIsNeg = testGroup "bvIsNeg"
174  [
175    -- bvLit value is an Integer; the Integer itself is signed.
176    -- Verify that signed Integers count as negative values.
177
178    testCase "-1.32 bvIsNeg.32" $ do
179      r <- liftIO $ withTestSolver $ \sym -> do
180        v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat ((-1) .&. allbits32))
181        asConcrete <$> bvIsNeg sym v
182      Just (ConcreteBool True) @=? r
183
184  , testCase "-1 bvIsNeg.32" $ do
185      r <- liftIO $ withTestSolver $ \sym -> do
186        v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat (-1))
187        asConcrete <$> bvIsNeg sym v
188      Just (ConcreteBool True) @=? r
189
190    -- Check a couple of corner cases
191
192  , testCase "0xffffffff bvIsNeg.32" $ do
193      r <- liftIO $ withTestSolver $ \sym -> do
194        v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat allbits32)
195        asConcrete <$> bvIsNeg sym v
196      Just (ConcreteBool True) @=? r
197
198  , testCase "0x80000000 bvIsNeg.32" $ do
199      r <- liftIO $ withTestSolver $ \sym -> do
200        v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat 0x80000000)
201        asConcrete <$> bvIsNeg sym v
202      Just (ConcreteBool True) @=? r
203
204  , testCase "0x7fffffff !bvIsNeg.32" $ do
205      r <- liftIO $ withTestSolver $ \sym -> do
206        v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat 0x7fffffff)
207        asConcrete <$> bvIsNeg sym v
208      Just (ConcreteBool False) @=? r
209
210  , testCase "0 !bvIsNeg.32" $ do
211      r <- liftIO $ withTestSolver $ \sym -> do
212        v <- bvLit sym (knownRepr :: NatRepr 32) (BV.zero knownNat)
213        asConcrete <$> bvIsNeg sym v
214      Just (ConcreteBool False) @=? r
215
216  , testProperty "bvIsNeg.32" $ property $ do
217      i <- forAll $ Gen.integral $ Range.linear (-10) (-1)
218      r <- liftIO $ withTestSolver $ \sym -> do
219        v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat i)
220        asConcrete <$> bvIsNeg sym v
221      Just (ConcreteBool True) === r
222
223  , testProperty "!bvIsNeg.32" $ property $ do
224      i <- forAll $ Gen.integral $ Range.linear 0 10
225      r <- liftIO $ withTestSolver $ \sym -> do
226        v <- bvLit sym (knownRepr :: NatRepr 32) (BV.mkBV knownNat i)
227        asConcrete <$> bvIsNeg sym v
228      Just (ConcreteBool False) === r
229  ]
230
231testInjectiveConversions :: TestTree
232testInjectiveConversions = testGroup "injective conversion"
233  [ testProperty "realToInteger" $ property $ do
234    i <- forAll $ Gen.integral $ Range.linear (-1000) 1000
235    liftIO $ withTestSolver $ \sym -> do
236      r_lit <- realLit sym (fromIntegral i)
237      rti <- realToInteger sym r_lit
238      Just i @=? (fromConcreteInteger <$> asConcrete rti)
239  , testProperty "bvToInteger" $ property $ do
240    i <- forAll $ Gen.integral $ Range.linear 0 255
241    liftIO $ withTestSolver $ \sym -> do
242      b_lit <- bvLit sym knownRepr (BV.mkBV (knownNat @8) (fromIntegral i))
243      int <- bvToInteger sym b_lit
244      Just i @=? (fromConcreteInteger <$> asConcrete int)
245  , testProperty "sbvToInteger" $ property $ do
246    i <- forAll $ Gen.integral $ Range.linear (-128) 127
247    liftIO $ withTestSolver $ \sym -> do
248      b_lit <- bvLit sym knownRepr (BV.mkBV (knownNat @8) (fromIntegral i))
249      int <- sbvToInteger sym b_lit
250      Just i @=? (fromConcreteInteger <$> asConcrete int)
251  , testProperty "predToBV" $ property $ do
252    b <- forAll $ Gen.integral $ Range.linear 0 1
253    liftIO $ withTestSolver $ \sym -> do
254      let p = if b == 1 then truePred sym else falsePred sym
255      let w = knownRepr :: NatRepr 8
256      b_lit <- predToBV sym p w
257      int <- bvToInteger sym b_lit
258      Just b @=? (fromConcreteInteger <$> asConcrete int)
259  , testIntegerToBV
260  ]
261
262testIntegerToBV :: TestTree
263testIntegerToBV = testGroup "integerToBV"
264  [ testProperty "bvToInteger (integerToBv x w) == mod x (2^w)" $ property $ do
265    x <- forAll $ Gen.integral $ Range.linear (-1000) 1000
266    liftIO $ withTestSolver $ \sym -> do
267      let w' = 8 :: Integer
268      let w = knownRepr :: NatRepr 8
269      x_lit <- intLit sym x
270      itobv <- integerToBV sym x_lit w
271      bvtoi <- bvToInteger sym itobv
272      (fromConcreteInteger <$> asConcrete bvtoi) @=? Just (x `mod` 2^w')
273  , testProperty "bvToInteger (integerToBV x w) == x when 0 <= x < 2^w" $ property $ do
274    let w = 8 :: Integer
275    x <- forAll $ Gen.integral $ Range.linear 0 (2^w-1)
276    liftIO $ withTestSolver $ \sym -> do
277      let w' = knownRepr :: NatRepr 8
278      x_lit <- intLit sym x
279      itobv <- integerToBV sym x_lit w'
280      bvtoi <- bvToInteger sym itobv
281      (fromConcreteInteger <$> asConcrete bvtoi) @=? Just x
282  , testProperty "sbvToInteger (integerToBV x w) == mod (x + 2^(w-1)) (2^w) - 2^(w-1)" $ property $ do
283    let w = 8 :: Integer
284    x <- forAll $ Gen.integral $ Range.linear (-1000) 1000
285    liftIO $ withTestSolver $ \sym -> do
286      let w' = knownRepr :: NatRepr 8
287      x_lit <- intLit sym x
288      itobv <- integerToBV sym x_lit w'
289      sbvtoi <- sbvToInteger sym itobv
290      (fromConcreteInteger <$> asConcrete sbvtoi) @=? Just (mod (x + 2^(w-1)) (2^w) - 2^(w-1))
291  , testProperty "sbvToInteger (integerToBV x w) == x when -2^(w-1) <= x < 2^(w-1)" $ property $ do
292    let w = 8 :: Integer
293    x <- forAll $ Gen.integral $ Range.linear (-(2^(w-1))) (2^(w-1)-1)
294    liftIO $ withTestSolver $ \sym -> do
295      let w' = knownRepr :: NatRepr 8
296      x_lit <- intLit sym x
297      itobv <- integerToBV sym x_lit w'
298      sbvtoi <- sbvToInteger sym itobv
299      (fromConcreteInteger <$> asConcrete sbvtoi) @=? Just x
300  , testProperty "integerToBV (bvToInteger y) w == y when y is a SymBV sym w" $ property $ do
301    x <- forAll $ Gen.integral $ Range.linear (-1000) 1000
302    liftIO $ withTestSolver $ \sym -> do
303      let w' = knownRepr :: NatRepr 8
304      y <- bvLit sym knownRepr (BV.mkBV (knownNat @8) x)
305      bvtoi <- bvToInteger sym y
306      itobv <- integerToBV sym bvtoi w'
307      itobv @=? y
308  , testProperty "integerToBV (sbvToInteger y) w == y when y is a SymBV sym w" $ property $ do
309    x <- forAll $ Gen.integral $ Range.linear (-1000) 1000
310    liftIO $ withTestSolver $ \sym -> do
311      let w' = knownRepr :: NatRepr 8
312      y <- bvLit sym knownRepr (BV.mkBV (knownNat @8) x)
313      sbvtoi <- sbvToInteger sym y
314      itobv <- integerToBV sym sbvtoi w'
315      itobv @=? y
316  ]
317
318----------------------------------------------------------------------
319
320main :: IO ()
321main = defaultMain $ testGroup "What4 Expressions"
322  [
323    testIntDivModProps
324  , testBvIsNeg
325  , testInt
326  , testProperty "stringEmpty" $ property $ do
327    s <- liftIO $ withTestSolver $ \sym -> do
328      s <- stringEmpty sym UnicodeRepr
329      return (asConcrete s)
330    (fromConcreteString <$> s) === Just ""
331  , testInjectiveConversions
332  ]
333