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