{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {- Module : BVDomTest Copyright : (c) Galois Inc, 2020 License : BSD3 Maintainer : rdockins@galois.com This module performs randomized testing of the bitvector abstract domain computations, which are among relatively complex. The intended meaning of the abstract domain computations are specified using Cryptol in "doc/bvdoman.cry" and realated files. In those files soundness properites are proved for the implementations. These tests are intended to supplement those proofs for the actual implementations, which are transliterated from the Cryptol. -} import qualified Data.Bits as Bits import Test.Tasty import Test.Verification import VerifyBindings import Data.Parameterized.NatRepr import Data.Parameterized.Some import qualified What4.Utils.BVDomain as O import qualified What4.Utils.BVDomain.Arith as A import qualified What4.Utils.BVDomain.Bitwise as B import qualified What4.Utils.BVDomain.XOR as X main :: IO () main = defaultMain $ setTestOptions $ testGroup "Bitvector Domain" [ arithDomainTests , bitwiseDomainTests , xorDomainTests , overallDomainTests , transferTests ] data SomeWidth where SW :: (1 <= w) => NatRepr w -> SomeWidth genWidth :: Gen SomeWidth genWidth = do sz <- getSize x <- chooseInt (1, sz+4) case someNat x of Just (Some n) | Just LeqProof <- isPosNat n -> pure (SW n) _ -> error "test panic! genWidth" genBV :: NatRepr w -> Gen Integer genBV w = chooseInteger (minUnsigned w, maxUnsigned w) arithDomainTests :: TestTree arithDomainTests = testGroup "Arith Domain" [ genTest "correct_any" $ do SW n <- genWidth A.correct_any n <$> genBV n , genTest "correct_ubounds" $ do SW n <- genWidth A.correct_ubounds n <$> A.genPair n , genTest "correct_sbounds" $ do SW n <- genWidth A.correct_sbounds n <$> A.genPair n , genTest "correct_singleton" $ do SW n <- genWidth A.correct_singleton n <$> genBV n <*> genBV n , genTest "correct_overlap" $ do SW n <- genWidth A.correct_overlap <$> A.genDomain n <*> A.genDomain n <*> genBV n , genTest "correct_union" $ do SW n <- genWidth A.correct_union n <$> A.genDomain n <*> A.genDomain n <*> genBV n , genTest "correct_zero_ext" $ do SW w <- genWidth SW n <- genWidth let u = addNat w n case testLeq (addNat w (knownNat @1)) u of Nothing -> error "impossible!" Just LeqProof -> do a <- A.genDomain w x <- A.genElement a pure $ A.correct_zero_ext w a u x , genTest "correct_sign_ext" $ do SW w <- genWidth SW n <- genWidth let u = addNat w n case testLeq (addNat w (knownNat @1)) u of Nothing -> error "impossible!" Just LeqProof -> do a <- A.genDomain w x <- A.genElement a pure $ A.correct_sign_ext w a u x , genTest "correct_concat" $ do SW m <- genWidth SW n <- genWidth A.correct_concat m <$> A.genPair m <*> pure n <*> A.genPair n , genTest "correct_shrink" $ do SW i <- genWidth SW n <- genWidth A.correct_shrink i n <$> A.genPair (addNat i n) , genTest "correct_trunc" $ do SW n <- genWidth SW m <- genWidth let w = addNat n m LeqProof <- pure $ addIsLeq n m A.correct_trunc n <$> A.genPair w , genTest "correct_select" $ do SW n <- genWidth SW i <- genWidth SW z <- genWidth let i_n = addNat i n let w = addNat i_n z LeqProof <- pure $ addIsLeq i_n z A.correct_select i n <$> A.genPair w , genTest "correct_add" $ do SW n <- genWidth A.correct_add n <$> A.genPair n <*> A.genPair n , genTest "correct_neg" $ do SW n <- genWidth A.correct_neg n <$> A.genPair n , genTest "correct_not" $ do SW n <- genWidth A.correct_not n <$> A.genPair n , genTest "correct_mul" $ do SW n <- genWidth A.correct_mul n <$> A.genPair n <*> A.genPair n , genTest "correct_scale" $ do SW n <- genWidth A.correct_scale n <$> genBV n <*> A.genPair n , genTest "correct_scale_eq" $ do SW n <- genWidth A.correct_scale_eq n <$> genBV n <*> A.genDomain n , genTest "correct_udiv" $ do SW n <- genWidth A.correct_udiv n <$> A.genPair n <*> A.genPair n , genTest "correct_urem" $ do SW n <- genWidth A.correct_urem n <$> A.genPair n <*> A.genPair n , genTest "correct_sdiv" $ do SW n <- genWidth A.correct_sdiv n <$> A.genPair n <*> A.genPair n , genTest "correct_sdivRange" $ do SW n <- genWidth a <- (,) <$> genBV n <*> genBV n b <- (,) <$> genBV n <*> genBV n x <- genBV n y <- genBV n pure $ A.correct_sdivRange a b x y , genTest "correct_srem" $ do SW n <- genWidth A.correct_srem n <$> A.genPair n <*> A.genPair n , genTest "correct_shl"$ do SW n <- genWidth A.correct_shl n <$> A.genPair n <*> A.genPair n , genTest "correct_lshr"$ do SW n <- genWidth A.correct_lshr n <$> A.genPair n <*> A.genPair n , genTest "correct_ashr"$ do SW n <- genWidth A.correct_ashr n <$> A.genPair n <*> A.genPair n , genTest "correct_eq" $ do SW n <- genWidth A.correct_eq n <$> A.genPair n <*> A.genPair n , genTest "correct_ult" $ do SW n <- genWidth A.correct_ult n <$> A.genPair n <*> A.genPair n , genTest "correct_slt" $ do SW n <- genWidth A.correct_slt n <$> A.genPair n <*> A.genPair n , genTest "correct_unknowns" $ do SW n <- genWidth a <- A.genDomain n x <- A.genElement a y <- A.genElement a pure $ A.correct_unknowns a x y , genTest "correct_bitbounds" $ do SW n <- genWidth A.correct_bitbounds n <$> A.genPair n ] xorDomainTests :: TestTree xorDomainTests = testGroup "XOR Domain" [ genTest "correct_singleton" $ do SW n <- genWidth X.correct_singleton n <$> genBV n <*> genBV n , genTest "correct_xor" $ do SW n <- genWidth X.correct_xor n <$> X.genPair n <*> X.genPair n , genTest "correct_and" $ do SW n <- genWidth X.correct_and n <$> X.genPair n <*> X.genPair n , genTest "correct_and_scalar" $ do SW n <- genWidth X.correct_and_scalar n <$> genBV n <*> X.genPair n , genTest "correct_bitbounds" $ do SW n <- genWidth X.correct_bitbounds <$> X.genDomain n <*> genBV n ] bitwiseDomainTests :: TestTree bitwiseDomainTests = testGroup "Bitwise Domain" [ genTest "correct_any" $ do SW n <- genWidth B.correct_any n <$> genBV n , genTest "correct_singleton" $ do SW n <- genWidth B.correct_singleton n <$> genBV n <*> genBV n , genTest "correct_overlap" $ do SW n <- genWidth B.correct_overlap <$> B.genDomain n <*> B.genDomain n <*> genBV n , genTest "correct_union1" $ do SW n <- genWidth (a,x) <- B.genPair n b <- B.genDomain n pure $ B.correct_union n a b x , genTest "correct_union2" $ do SW n <- genWidth a <- B.genDomain n (b,x) <- B.genPair n pure $ B.correct_union n a b x , genTest "correct_intersection" $ do SW n <- genWidth B.correct_intersection <$> B.genDomain n <*> B.genDomain n <*> genBV n , genTest "correct_zero_ext" $ do SW w <- genWidth SW n <- genWidth let u = addNat w n case testLeq (addNat w (knownNat @1)) u of Nothing -> error "impossible!" Just LeqProof -> do a <- B.genDomain w x <- B.genElement a pure $ B.correct_zero_ext w a u x , genTest "correct_sign_ext" $ do SW w <- genWidth SW n <- genWidth let u = addNat w n case testLeq (addNat w (knownNat @1)) u of Nothing -> error "impossible!" Just LeqProof -> do a <- B.genDomain w x <- B.genElement a pure $ B.correct_sign_ext w a u x , genTest "correct_concat" $ do SW m <- genWidth SW n <- genWidth B.correct_concat m <$> B.genPair m <*> pure n <*> B.genPair n , genTest "correct_shrink" $ do SW i <- genWidth SW n <- genWidth B.correct_shrink i n <$> B.genPair (addNat i n) , genTest "correct_trunc" $ do SW n <- genWidth SW m <- genWidth let w = addNat n m LeqProof <- pure $ addIsLeq n m B.correct_trunc n <$> B.genPair w , genTest "correct_select" $ do SW n <- genWidth SW i <- genWidth SW z <- genWidth let i_n = addNat i n let w = addNat i_n z LeqProof <- pure $ addIsLeq i_n z B.correct_select i n <$> B.genPair w , genTest "correct_shl"$ do SW n <- genWidth B.correct_shl n <$> B.genPair n <*> chooseInteger (0, intValue n) , genTest "correct_lshr"$ do SW n <- genWidth B.correct_lshr n <$> B.genPair n <*> chooseInteger (0, intValue n) , genTest "correct_ashr"$ do SW n <- genWidth B.correct_ashr n <$> B.genPair n <*> chooseInteger (0, intValue n) , genTest "correct_rol"$ do SW n <- genWidth B.correct_rol n <$> B.genPair n <*> chooseInteger (0, intValue n) , genTest "correct_ror"$ do SW n <- genWidth B.correct_ror n <$> B.genPair n <*> chooseInteger (0, intValue n) , genTest "correct_eq" $ do SW n <- genWidth B.correct_eq n <$> B.genPair n <*> B.genPair n , genTest "correct_not" $ do SW n <- genWidth B.correct_not n <$> B.genPair n , genTest "correct_and" $ do SW n <- genWidth B.correct_and n <$> B.genPair n <*> B.genPair n , genTest "correct_or" $ do SW n <- genWidth B.correct_or n <$> B.genPair n <*> B.genPair n , genTest "correct_xor" $ do SW n <- genWidth B.correct_xor n <$> B.genPair n <*> B.genPair n , genTest "correct_testBit" $ do SW n <- genWidth i <- fromInteger <$> chooseInteger (0, intValue n - 1) B.correct_testBit n <$> B.genPair n <*> pure i ] overallDomainTests :: TestTree overallDomainTests = testGroup "Overall Domain" [ -- test that the union of consecutive singletons gives a precise interval genTest "singleton/union size" $ do SW n <- genWidth let w = maxUnsigned n x <- genBV n y <- min 1000 <$> genBV n let as = [ O.singleton n ((x + i) Bits..&. w) | i <- [0 .. y] ] let a = foldl1 O.union as pure $ property (O.size a == y+1) , genTest "correct_bra1" $ do SW n <- genWidth O.correct_bra1 n <$> genBV n <*> genBV n , genTest "correct_bra2" $ do SW n <- genWidth O.correct_bra2 n <$> genBV n <*> genBV n <*> genBV n , genTest "correct_brb1" $ do SW n <- genWidth O.correct_brb1 n <$> genBV n <*> genBV n <*> genBV n , genTest "correct_brb2" $ do SW n <- genWidth O.correct_brb2 n <$> genBV n <*> genBV n <*> genBV n <*> genBV n , genTest "correct_any" $ do SW n <- genWidth O.correct_any n <$> genBV n , genTest "correct_ubounds" $ do SW n <- genWidth O.correct_ubounds n <$> O.genPair n , genTest "correct_sbounds" $ do SW n <- genWidth O.correct_sbounds n <$> O.genPair n , genTest "correct_singleton" $ do SW n <- genWidth O.correct_singleton n <$> genBV n <*> genBV n , genTest "correct_overlap" $ do SW n <- genWidth O.correct_overlap <$> O.genDomain n <*> O.genDomain n <*> genBV n , genTest "precise_overlap" $ do SW n <- genWidth O.precise_overlap <$> O.genDomain n <*> O.genDomain n , genTest "correct_union" $ do SW n <- genWidth O.correct_union n <$> O.genDomain n <*> O.genDomain n <*> genBV n , genTest "correct_zero_ext" $ do SW w <- genWidth SW n <- genWidth let u = addNat w n case testLeq (addNat w (knownNat @1)) u of Nothing -> error "impossible!" Just LeqProof -> do a <- O.genDomain w x <- O.genElement a pure $ O.correct_zero_ext w a u x , genTest "correct_sign_ext" $ do SW w <- genWidth SW n <- genWidth let u = addNat w n case testLeq (addNat w (knownNat @1)) u of Nothing -> error "impossible!" Just LeqProof -> do a <- O.genDomain w x <- O.genElement a pure $ O.correct_sign_ext w a u x , genTest "correct_concat" $ do SW m <- genWidth SW n <- genWidth O.correct_concat m <$> O.genPair m <*> pure n <*> O.genPair n , genTest "correct_select" $ do SW n <- genWidth SW i <- genWidth SW z <- genWidth let i_n = addNat i n let w = addNat i_n z LeqProof <- pure $ addIsLeq i_n z O.correct_select i n <$> O.genPair w , genTest "correct_add" $ do SW n <- genWidth O.correct_add n <$> O.genPair n <*> O.genPair n , genTest "correct_neg" $ do SW n <- genWidth O.correct_neg n <$> O.genPair n , genTest "correct_scale" $ do SW n <- genWidth O.correct_scale n <$> genBV n <*> O.genPair n , genTest "correct_mul" $ do SW n <- genWidth O.correct_mul n <$> O.genPair n <*> O.genPair n , genTest "correct_udiv" $ do SW n <- genWidth O.correct_udiv n <$> O.genPair n <*> O.genPair n , genTest "correct_urem" $ do SW n <- genWidth O.correct_urem n <$> O.genPair n <*> O.genPair n , genTest "correct_sdiv" $ do SW n <- genWidth O.correct_sdiv n <$> O.genPair n <*> O.genPair n , genTest "correct_srem" $ do SW n <- genWidth O.correct_srem n <$> O.genPair n <*> O.genPair n , genTest "correct_shl"$ do SW n <- genWidth O.correct_shl n <$> O.genPair n <*> O.genPair n , genTest "correct_lshr"$ do SW n <- genWidth O.correct_lshr n <$> O.genPair n <*> O.genPair n , genTest "correct_ashr"$ do SW n <- genWidth O.correct_ashr n <$> O.genPair n <*> O.genPair n , genTest "correct_rol"$ do SW n <- genWidth O.correct_rol n <$> O.genPair n <*> O.genPair n , genTest "correct_ror"$ do SW n <- genWidth O.correct_ror n <$> O.genPair n <*> O.genPair n , genTest "correct_eq" $ do SW n <- genWidth O.correct_eq n <$> O.genPair n <*> O.genPair n , genTest "correct_ult" $ do SW n <- genWidth O.correct_ult n <$> O.genPair n <*> O.genPair n , genTest "correct_slt" $ do SW n <- genWidth O.correct_slt n <$> O.genPair n <*> O.genPair n , genTest "correct_not" $ do SW n <- genWidth O.correct_not n <$> O.genPair n , genTest "correct_and" $ do SW n <- genWidth O.correct_and n <$> O.genPair n <*> O.genPair n , genTest "correct_or" $ do SW n <- genWidth O.correct_or n <$> O.genPair n <*> O.genPair n , genTest "correct_xor" $ do SW n <- genWidth O.correct_xor n <$> O.genPair n <*> O.genPair n , genTest "correct_testBit" $ do SW n <- genWidth i <- fromInteger <$> chooseInteger (0, intValue n - 1) O.correct_testBit n <$> O.genPair n <*> pure i , genTest "correct_popcnt" $ do SW n <- genWidth O.correct_popcnt n <$> O.genPair n , genTest "correct_clz" $ do SW n <- genWidth O.correct_clz n <$> O.genPair n , genTest "correct_ctz" $ do SW n <- genWidth O.correct_ctz n <$> O.genPair n ] transferTests :: TestTree transferTests = testGroup "Transfer" [ genTest "correct_arithToBitwise" $ do SW n <- genWidth O.correct_arithToBitwise n <$> A.genPair n , genTest "correct_bitwiseToArith" $ do SW n <- genWidth O.correct_bitwiseToArith n <$> B.genPair n , genTest "correct_bitwiseToXorDomain" $ do SW n <- genWidth O.correct_bitwiseToXorDomain n <$> B.genPair n , genTest "correct_arithToXorDomain" $ do SW n <- genWidth O.correct_arithToXorDomain n <$> A.genPair n , genTest "correct_xorToBitwiseDomain" $ do SW n <- genWidth O.correct_xorToBitwiseDomain n <$> X.genPair n , genTest "correct_asXorDomain" $ do SW n <- genWidth O.correct_asXorDomain n <$> O.genPair n , genTest "correct_fromXorDomain" $ do SW n <- genWidth O.correct_fromXorDomain n <$> X.genPair n ]