diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ivory-quickcheck.cabal b/ivory-quickcheck.cabal new file mode 100644 --- /dev/null +++ b/ivory-quickcheck.cabal @@ -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 diff --git a/src/Ivory/QuickCheck.hs b/src/Ivory/QuickCheck.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/QuickCheck.hs @@ -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) + +-------------------------------------------------------------------------------- + diff --git a/src/Ivory/QuickCheck/Arbitrary.hs b/src/Ivory/QuickCheck/Arbitrary.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/QuickCheck/Arbitrary.hs @@ -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) + +-------------------------------------------------------------------------------- diff --git a/src/Ivory/QuickCheck/Monad.hs b/src/Ivory/QuickCheck/Monad.hs new file mode 100644 --- /dev/null +++ b/src/Ivory/QuickCheck/Monad.hs @@ -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 + +--------------------------------------------------------------------------------