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
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.Basics.DynSign
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test case for <http://github.com/GaloisInc/cryptol/issues/566>
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.Basics.DynSign(tests) where
import Utils.SBVTestFramework hiding (proveWith)
import Data.SBV.Dynamic
import Data.SBV.Internals (genMkSymVar, unSBV, VarContext(..))
prop :: Symbolic SVal
prop = do x <- unSBV <$> genMkSymVar w8 (NonQueryVar Nothing) (Just "x")
let lhs = svUnsign (svSign x `svShiftRight` sfour)
rhs = svExtract 7 0 x `svShiftRight` ufour
return $ lhs `svEqual` rhs
where w8, i8 :: Kind
w8 = kindOf (undefined :: SWord8)
i8 = kindOf (undefined :: SInt8)
sfour = svInteger i8 4
ufour = svInteger w8 4
checkSat :: ThmResult -> Assertion
checkSat r = assert isThm
where isThm = case r of
ThmResult Unsatisfiable{} -> return False :: IO Bool
ThmResult Satisfiable{} -> return True
_ -> error "checkSat: Unexpected result!"
-- Test suite
tests :: TestTree
tests = testGroup "Basics.DynSign"
[ testCase "dynSign" $ checkSat =<< proveWith z3 prop
]
|
