ivory-quickcheck (empty) → 0.1.0.0
raw patch · 6 files changed
+335/−0 lines, 6 filesdep +QuickCheckdep +basedep +ivorysetup-changed
Dependencies added: QuickCheck, base, ivory, monadLib, random
Files
- LICENSE +30/−0
- Setup.hs +2/−0
- ivory-quickcheck.cabal +30/−0
- src/Ivory/QuickCheck.hs +120/−0
- src/Ivory/QuickCheck/Arbitrary.hs +105/−0
- src/Ivory/QuickCheck/Monad.hs +48/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c)2013, Galois, Inc++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Galois, Inc nor the names of its contributors+ may be used to endorse or promote products derived from this software+ without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ivory-quickcheck.cabal view
@@ -0,0 +1,30 @@+name: ivory-quickcheck+version: 0.1.0.0+author: Galois, Inc.+copyright: 2013 Galois, Inc.+maintainer: leepike@galois.com+category: Testing+build-type: Simple+cabal-version: >= 1.10+synopsis: QuickCheck driver for Ivory.+description: Warning! This module is experimental and its implementation may change dramatically.+homepage: http://smaccmpilot.org/languages/ivory-introduction.html+license: BSD3+license-file: LICENSE+source-repository this+ type: git+ location: https://github.com/GaloisInc/ivory+ tag: hackage-qc-0100++library+ exposed-modules: Ivory.QuickCheck,+ Ivory.QuickCheck.Arbitrary,+ Ivory.QuickCheck.Monad+ build-depends: base >= 4.6 && < 4.7,+ monadLib,+ random,+ QuickCheck == 2.6,+ ivory+ hs-source-dirs: src+ default-language: Haskell2010+ ghc-options: -Wall
+ src/Ivory/QuickCheck.hs view
@@ -0,0 +1,120 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | Generate random inputs to Ivory-generated C code.+--+-- Example usage:+-- @+-- [ivory|+-- struct foo+-- { foo_a :: Stored IFloat+-- ; foo_b :: Stored Uint8+-- }+-- |]+--+-- -- Function we want to generate inputs for.+-- func :: Def ('[Uint8+-- , Ref s (Array 3 (Stored Uint8))+-- , Ref s (Struct "foo")+-- ] :-> ())+-- func = proc "func" $ \u arr str -> body $+-- arrayMap $ \ix -> do+-- a <- deref (arr ! ix)+-- b <- deref (str ~> foo_b)+-- store (arr ! ix) (a + b + u)+--+-- type DriverDef = Def ('[] :-> ())+--+-- -- Driver function. Takes lists of the arguments we'll pass to the function+-- -- test.+-- driver :: [Uint8]+-- -> [Init (Array 3 (Stored Uint8))]+-- -> [Init (Struct "foo")]+-- -> DriverDef+-- driver as0 as1 as2 = proc "main" $ body $ do+-- mapM_ oneCall (zip3 as0 as1 as2)+--+-- where+-- oneCall (a0, a1, a2) = do+-- a1' <- local a1+-- a2' <- local a2+-- call_ func a0 a1' a2'+--+-- -- Generate the random values to pass.+-- runTest :: IvoryGen DriverDef+-- runTest = do+-- args0 <- samples num A.arbitrary+-- args1 <- samples num A.arbitrary+-- aFoos <- samples num foo_a+-- bFoos <- samples num foo_b+-- return $ driver args0 args1 (zipWith foo aFoos bFoos)+-- where+-- foo a b = istruct [ a, b ]+-- num = 10+--+-- -- Compile!+-- runTests :: IO ()+-- runTests = do+-- d <- runIO runTest+-- runCompiler [cmodule d] initialOpts { includeDir = "test"+-- , srcDir = "test"+-- , constFold = True+-- }+-- where+-- cmodule d = package "qc" $ do+-- incl d+-- incl func+-- @++module Ivory.QuickCheck+ ( module Ivory.QuickCheck.Monad+ , module Ivory.QuickCheck.Arbitrary+ , Samples(..)+ ) where++++import qualified Test.QuickCheck.Arbitrary as A+import qualified Test.QuickCheck.Gen as G++import Ivory.QuickCheck.Arbitrary+import Ivory.QuickCheck.Monad++import Ivory.Language++import GHC.TypeLits++--------------------------------------------------------------------------------++type Size = Int++class Samples gen res where+ samples :: Size -> gen -> IvoryGen [res]++instance A.Arbitrary a => Samples (G.Gen a) a where+ samples = mkSamples++instance (A.Arbitrary a, SingI len, IvoryInit a, IvoryType a)+ => Samples (G.Gen a) (Init (Array len (Stored a))) where+ samples i gen = mkSamples i mkArr+ where+ mkArr = do+ let sz = fromSing (sing :: Sing len)+ arr <- G.vectorOf (fromInteger sz) gen+ return $ iarray (map ival arr)++instance (A.Arbitrary a, IvoryInit a)+ => Samples (Label sym (Stored a)) (InitStruct sym)+ where+ samples i label = mkSamples i (sampleStoredLabel label)++--------------------------------------------------------------------------------+
+ src/Ivory/QuickCheck/Arbitrary.hs view
@@ -0,0 +1,105 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE FlexibleInstances #-}++{-# OPTIONS_GHC -fno-warn-orphans #-}++-- | Arbitrary instances for Ivory and helper functions.++module Ivory.QuickCheck.Arbitrary where++import qualified Test.QuickCheck.Arbitrary as A+import qualified Test.QuickCheck.Gen as G++import Data.Int+import Data.Word+import Data.String (IsString(fromString))+import GHC.TypeLits++import Ivory.Language++import Ivory.QuickCheck.Monad++--------------------------------------------------------------------------------++instance A.Arbitrary IBool where+ arbitrary = fmap toIvory (A.arbitrary :: G.Gen Bool)+ where toIvory True = true+ toIvory False = false++--------------------------------------------------------------------------------++instance A.Arbitrary IString where+ arbitrary = fmap fromString (A.arbitrary :: G.Gen String)++--------------------------------------------------------------------------------++integralArb :: (Integral a, Num b) => G.Gen a -> G.Gen b+integralArb = fmap fromIntegral++instance A.Arbitrary Uint8 where+ arbitrary = integralArb (A.arbitrary :: G.Gen Word8)++instance A.Arbitrary Uint16 where+ arbitrary = integralArb (A.arbitrary :: G.Gen Word16)++instance A.Arbitrary Uint32 where+ arbitrary = integralArb (A.arbitrary :: G.Gen Word32)++instance A.Arbitrary Uint64 where+ arbitrary = integralArb (A.arbitrary :: G.Gen Word64)++instance A.Arbitrary Sint8 where+ arbitrary = integralArb (A.arbitrary :: G.Gen Int8)++instance A.Arbitrary Sint16 where+ arbitrary = integralArb (A.arbitrary :: G.Gen Int16)++instance A.Arbitrary Sint32 where+ arbitrary = integralArb (A.arbitrary :: G.Gen Int32)++instance A.Arbitrary Sint64 where+ arbitrary = integralArb (A.arbitrary :: G.Gen Int64)++instance A.Arbitrary IFloat where+ arbitrary = fmap ifloat (A.arbitrary :: G.Gen Float)++instance A.Arbitrary IDouble where+ arbitrary = fmap idouble (A.arbitrary :: G.Gen Double)++--------------------------------------------------------------------------------++-- | Random array (of 'Stored' values) initializer.+instance (SingI len, A.Arbitrary a, IvoryType a, IvoryInit a)+ => A.Arbitrary (Init (Array len (Stored a)))+ where+ arbitrary = do+ let sz = fromSing (sing :: Sing len)+ arr <- G.vectorOf (fromInteger sz) A.arbitrary+ return $ iarray (map ival arr)++--------------------------------------------------------------------------------++-- | Random struct label (of 'Stored' values) initializer.+sampleStoredLabel :: (A.Arbitrary a, IvoryInit a)+ => Label sym (Stored a) -> G.Gen (InitStruct sym)+sampleStoredLabel label = do+ v <- A.arbitrary+ return (label .= ival v)++--------------------------------------------------------------------------------++-- | Take a random number generator seed, a number of items to produce, and a+-- generator and produces an increasingly bounded list of items.+mkSamples :: Int -> G.Gen a -> IvoryGen [a]+mkSamples n (G.MkGen f) = mapM go ns+ where+ ns = [0,2..n*2]+ go i = do+ rnd <- get+ return (f rnd i)++--------------------------------------------------------------------------------
+ src/Ivory/QuickCheck/Monad.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE KindSignatures #-}++-- | Monad for generating random C inputs for Ivory programs.++module Ivory.QuickCheck.Monad+ ( IvoryGen()+ , set+ , get+ , run+ , runIO+ ) where++import MonadLib hiding (set, get, lift)+import qualified MonadLib as M+import Control.Applicative (Applicative(..))++import qualified System.Random as R++--------------------------------------------------------------------------------++newtype IvoryGen a = IvoryGen (StateT R.StdGen Id a)+ deriving (Functor, Applicative, Monad)++set :: R.StdGen -> IvoryGen ()+set = IvoryGen . M.set++-- | Get the current random number, split it, use one and put back the other.+get :: IvoryGen R.StdGen+get = do+ rnd <- IvoryGen M.get+ let (r0, r1) = R.split rnd+ set r1+ return r0++run :: R.StdGen -> IvoryGen a -> (a, R.StdGen)+run rnd (IvoryGen st) = runId (runStateT rnd st)++-- | Generate a fresh random value, run the monad with it, and return the+-- result.+runIO :: IvoryGen a -> IO a+runIO igen = do+ rnd <- R.newStdGen+ let (a,_) = run rnd igen+ return a++--------------------------------------------------------------------------------