diff --git a/src/CCall.hs b/src/CCall.hs index 8632bde812458e46f96e1d5d6db7855700bfd088..f3936bb2b84202a530e2027ef1c96a5fe96b80d8 100644 --- a/src/CCall.hs +++ b/src/CCall.hs @@ -39,6 +39,7 @@ testCCall -> CCallDesc -> Property testCCall comp c = + counterexample (cStub c) $ counterexample (cCallCmm c) $ ioProperty $ withTempDirectory "." "tmp" $ \tmpDir -> do writeFile (tmpDir </> "test_c.c") (cStub c) writeFile (tmpDir </> "test.cmm") (cCallCmm c) diff --git a/src/Expr.hs b/src/Expr.hs index 4d947e5ec14afe030e3f99c1e99eb1699ac890db..4f9d1d2f04b46f077a0a2062d4f30f138d7ef328 100644 --- a/src/Expr.hs +++ b/src/Expr.hs @@ -17,8 +17,6 @@ module Expr , genExpr ) where -import Data.Foldable (foldl') -import qualified Data.ByteString as BS import Numeric.Natural import Control.Monad import Data.Bits as Bits @@ -29,6 +27,7 @@ import Data.Proxy import Prelude hiding (truncate) import {-# SOURCE #-} RefInterpreter +import {-# SOURCE #-} FExpr import Width import Number @@ -100,6 +99,10 @@ data Expr (width :: Width) where EZeroExt :: forall narrow wide. (KnownWidth narrow, wide `WiderThan` narrow) => Expr narrow -> Expr wide + -- | Floating-point to signed integer conversion + EFSConv :: FExpr width -> Expr width + EFRel :: FRelationalOp -> FExpr width -> FExpr width -> Expr WordSize + ELoad :: Expr WordSize -> Expr width ELit :: Number width -> Expr width @@ -165,6 +168,8 @@ instance KnownWidth width => Arbitrary (Expr width) where ++ [ EZeroExt a ] EZeroExt a -> shrinkUnOp EZeroExt a ++ [ EZeroExt b | EZeroExt b <- pure a, Wider <- pure $ e `compareWidths` b ] + EFSConv a -> EFSConv <$> shrink a + EFRel op a b -> EFRel op <$> shrink a <*> shrink b ELoad a -> shrinkUnOp ELoad a ELit a -> map ELit (shrink a) where @@ -195,6 +200,7 @@ genExpr' _width = sized gen oneof $ [ litGen , loadGen + , EFSConv <$> arbitrary ] ++ arithmeticGens ++ bitwiseGens @@ -257,6 +263,8 @@ genExpr' _width = sized gen | SameWidth <- Proxy @width `compareWidths` Proxy @WordSize = [ do op <- arbitrary binOp (ERel op) + , EFRel @W32 <$> arbitrary <*> arbitrary <*> arbitrary + , EFRel @W64 <$> arbitrary <*> arbitrary <*> arbitrary ] | otherwise = [] diff --git a/src/Expr.hs-boot b/src/Expr.hs-boot index 9d681664a50ff6ec9cec18dd71c80ebeadbb9869..411ec50f17f35566400672c45f9ca4ebbd7fc188 100644 --- a/src/Expr.hs-boot +++ b/src/Expr.hs-boot @@ -2,8 +2,12 @@ module Expr where -import Width (Width) +import Test.QuickCheck + +import Width (Width, KnownWidth) data Expr (width :: Width) type role Expr nominal + +instance (KnownWidth width) => Arbitrary (Expr width) diff --git a/src/RefInterpreter.hs b/src/RefInterpreter.hs index 7d492d32062f6b63b0648eb33cd749b2e0e81087..eb5832b9dbf0120e81bba30f4b492843d523a2c8 100644 --- a/src/RefInterpreter.hs +++ b/src/RefInterpreter.hs @@ -3,6 +3,7 @@ module RefInterpreter , memoryContents , memoryOracle , interpret + , interpretFloat ) where import Data.Bits @@ -12,6 +13,7 @@ import Numeric.Natural import Width import Expr +import FExpr import Number boolVal :: Bool -> Number WordSize @@ -64,6 +66,17 @@ interpret (EZeroExt a) = zeroExtNumber (interpret a) interpret (ELoad off) = memoryOracle $ toUnsigned $ interpret off interpret (ELit n) = n +interpretFloat + :: forall width. (KnownWidth width) + => FExpr width -> FloatType width +interpretFloat (FEAdd a b) = interpretFloat a + interpretFloat b +interpretFloat (FESub a b) = interpretFloat a - interpretFloat b +interpretFloat (FEMul a b) = interpretFloat a - interpretFloat b +interpretFloat (FEQuot a b) = interpretFloat a `quot` interpretFloat b +interpretFloat (FENegate a) = negate (interpretFloat a) +interpretFloat (FFromSInt a) = realToFrac $ toSigned $ interpret a +interpretFloat (FConv a) = realToFrac (interpretFloat a) + memorySize :: Natural memorySize = 1 `shiftL` 22 diff --git a/test-primops.cabal b/test-primops.cabal index c02de6eadf552994a16b42b39c6f5f133d4b7709..3d7630789416876812b6368c807c19cf27e144d2 100644 --- a/test-primops.cabal +++ b/test-primops.cabal @@ -14,6 +14,7 @@ executable test-primops other-modules: Width, Number, Expr, + FExpr, Expr.Parse, Interpreter, ToCmm,