diff --git a/ivory-quickcheck.cabal b/ivory-quickcheck.cabal --- a/ivory-quickcheck.cabal +++ b/ivory-quickcheck.cabal @@ -1,5 +1,5 @@ name: ivory-quickcheck -version: 0.1.0.0 +version: 0.2.0.3 author: Galois, Inc. copyright: 2013 Galois, Inc. maintainer: leepike@galois.com @@ -8,23 +8,45 @@ 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 +homepage: http://ivorylang.org license: BSD3 license-file: LICENSE source-repository this type: git location: https://github.com/GaloisInc/ivory - tag: hackage-qc-0100 + tag: hackage-qc-0103 library - exposed-modules: Ivory.QuickCheck, - Ivory.QuickCheck.Arbitrary, - Ivory.QuickCheck.Monad - build-depends: base >= 4.6 && < 4.7, + exposed-modules: Ivory.QuickCheck + build-depends: base >= 4.6 && < 5, + base-compat, monadLib, random, - QuickCheck == 2.6, - ivory + QuickCheck >= 2.7, + ivory, + ivory-backend-c, + ivory-eval hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall + +test-suite test + hs-source-dirs: test + type: exitcode-stdio-1.0 + main-is: Test.hs + ghc-options: -Wall + build-depends: base >= 4.6 && < 5 + , base-compat + , filepath + , directory + , process + , tasty >= 0.10 + , tasty-hunit + , monadLib + , QuickCheck + , ivory + , ivory-backend-c + , ivory-quickcheck + , ivory-stdlib + + default-language: Haskell2010 diff --git a/src/Ivory/QuickCheck.hs b/src/Ivory/QuickCheck.hs --- a/src/Ivory/QuickCheck.hs +++ b/src/Ivory/QuickCheck.hs @@ -1,120 +1,312 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE KindSignatures #-} {-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE QuasiQuotes #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE CPP #-} -{-# OPTIONS_GHC -fno-warn-orphans #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} --- | Generate random inputs to Ivory-generated C code. +-- | Check properties of Ivory programs using random inputs. -- -- 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 --- @ +-- +-- > [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 -> +-- > ensures_ (checkStored (arr ! 0) (\r -> r >? u)) $ +-- > body $ +-- > arrayMap $ \ix -> do +-- > a <- deref (arr ! ix) +-- > b <- deref (str ~> foo_b) +-- > store (arr ! ix) (a + b + u) +-- > +-- > -- Module containing our function +-- > cmodule :: Module +-- > cmodule = package "module" $ do +-- > defStruct (Proxy :: Proxy "foo") +-- > incl func +-- > +-- > -- Running @mkTest@ will produce a C program in @/test@ that will check +-- > -- @func@'s contract on 10 random inputs. +-- > mkTest :: IO () +-- > mkTest = check 10 [] cmodule (contract func) -module Ivory.QuickCheck - ( module Ivory.QuickCheck.Monad - , module Ivory.QuickCheck.Arbitrary - , Samples(..) - ) where +module Ivory.QuickCheck (check, checkWith, contract) where +import Prelude () +import Prelude.Compat +import Control.Monad (replicateM,forM) +import Data.IORef (IORef,newIORef,readIORef,writeIORef) +import Data.List (transpose,find) +import Ivory.Compile.C.CmdlineFrontend +import qualified Ivory.Eval as E +import Ivory.Language +import Ivory.Language.Proc +import qualified Ivory.Language.Syntax as I +import System.IO.Unsafe (unsafeInterleaveIO) -import qualified Test.QuickCheck.Arbitrary as A -import qualified Test.QuickCheck.Gen as G +import qualified Test.QuickCheck.Arbitrary as A +import qualified Test.QuickCheck.Gen as G -import Ivory.QuickCheck.Arbitrary -import Ivory.QuickCheck.Monad +import Data.Int +import Data.Word -import Ivory.Language +-- XXX: DEBUG +-- import Debug.Trace -import GHC.TypeLits +-- | Generate a random C program to check that the property holds. The +-- generated program will be placed in the @test@ subdirectory. +checkWith :: Int -- ^ The number of inputs to generate. + -> Opts -- ^ Options to pass to the Ivory compiler. + -> [Module] -- ^ Modules we need to have in scope. + -> Module -- ^ The defining module. + -> Def (args ':-> IBool) -- ^ The property to check. + -> IO () +checkWith n opts deps m prop@(DefProc p) = do + inputs <- sampleProc m p n + let main = DefProc I.Proc { I.procSym = "main" + , I.procRetTy = I.TyInt I.Int32 + , I.procArgs = [] + , I.procBody = concat inputs ++ [I.Return $ I.Typed (I.TyInt I.Int32) (I.ExpLit (I.LitInteger 0))] + , I.procRequires = [] + , I.procEnsures = [] + } + let test = package (I.modName m ++ "__test") $ do + depend m + incl prop + incl main + runCompiler ([m, test]++deps) [] opts -- initialOpts { outDir = Just "test" } +checkWith _ _ _ _ _ = error "I can only check normal Ivory procs!" --------------------------------------------------------------------------------- +-- | Generate a random C program to check that the property holds. The +-- generated program will be placed in the @test@ subdirectory. +check :: Int -- ^ The number of inputs to generate. + -> [Module] -- ^ Modules we need to have in scope. + -> Module -- ^ The defining module. + -> Def (args ':-> IBool) -- ^ The property to check. + -> IO () +check n deps m p = checkWith n (initialOpts { outDir = Just "test"}) deps m p -type Size = Int +-- | Make a @check@able property from an arbitrary Ivory procedure. The +-- property will simply check that the contracts are satisfied. +contract :: Def (args ':-> res) -> Def (args ':-> IBool) +contract (DefProc (I.Proc {..})) + = DefProc I.Proc + { I.procSym = procSym ++ "__contract_check" + , I.procRetTy = I.TyBool + , I.procArgs = procArgs + , I.procBody = [ I.Call procRetTy Nothing (I.NameSym procSym) + [ I.Typed t (I.ExpVar v) | I.Typed t v <- procArgs ] + , I.Return (I.Typed I.TyBool (I.ExpLit (I.LitBool True))) + ] + , I.procRequires = procRequires + , I.procEnsures = [] + } +contract _ = error "I can only check contracts of normal Ivory procs!" -class Samples gen res where - samples :: Size -> gen -> IvoryGen [res] +mkUnique :: (?counter :: IORef Integer) => IO Integer +mkUnique = do + i <- readIORef ?counter + writeIORef ?counter (i+1) + return i -instance A.Arbitrary a => Samples (G.Gen a) a where - samples = mkSamples +sampleProc :: Module -> I.Proc -> Int -> IO [I.Block] +sampleProc m@(I.Module {..}) p@(I.Proc {..}) n + = do c <- newIORef 0 + let ?counter = c + allInits <- fmap transpose $ forM procArgs $ \ (I.Typed t _) -> + sampleType m t + allAreas <- fmap transpose $ forM (getVisible modAreas) $ \ I.Area {..} -> do + inits <- sampleType m areaType + lazyMapIO (\ (var, blck) -> do + let store = case areaType of + I.TyArr _ _ -> I.RefCopy + I.TyStruct _ -> I.RefCopy + I.TyRef _ -> I.RefCopy -- XXX: this shouldn't actually appear + _ -> I.Store + return $ blck ++ [ store areaType (I.ExpAddrOfGlobal areaSym) (I.ExpVar var)]) + inits + --XXX: Refactor! + let validInits = + [ (inits, areas) | (inits, areas) <- zipLonger allInits allAreas + , let (vars, blcks) = unzip inits + , let asgnv = [ I.Assign ty arg (I.ExpVar var) + | (I.Typed ty arg, var) <- zip procArgs vars + ] + , E.runEval (E.openModule m (do + E.evalBlock (concat blcks ++ asgnv ++ concat areas) + E.evalRequires procRequires)) + == Right True + ] + forM (take n validInits) $ \ (args, areas) -> do + let (vars, inits) = unzip args + chk <- mkCheck p vars + return (concat inits ++ concat areas ++ chk) -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) +getVisible :: I.Visible a -> [a] +getVisible xs = I.public xs ++ I.private xs -instance (A.Arbitrary a, IvoryInit a) - => Samples (Label sym (Stored a)) (InitStruct sym) +mkCheck :: (?counter :: IORef Integer) + => I.Proc -> [I.Var] -> IO I.Block +mkCheck (I.Proc {..}) args = do + n <- mkUnique + let b = mkVar n + let c = [ I.Call I.TyBool (Just b) (I.NameSym procSym) + [ I.Typed t (I.ExpVar v) | (I.Typed t _, v) <- zip procArgs args ] + , I.Assert (I.ExpVar b) ] + return c + +sampleType :: (?counter :: IORef Integer) + => Module -> I.Type -> IO [(I.Var, I.Block)] +sampleType m t = case t of + I.TyInt sz + -> lazyMapIO (mkLocal t) =<< sampleInt sz + I.TyWord sz + -> lazyMapIO (mkLocal t) =<< sampleWord sz + I.TyIndex i + -> lazyMapIO (mkLocal t) =<< sampleIndex i + I.TyBool + -> lazyMapIO (mkLocal t) =<< sampleBool + I.TyChar + -> lazyMapIO (mkLocal t) =<< sampleChar + I.TyFloat + -> lazyMapIO (mkLocal t) =<< sampleFloat + I.TyDouble + -> lazyMapIO (mkLocal t) =<< sampleDouble + I.TyRef ty + -> lazyMapIO (mkRef ty) =<< sampleType m ty + I.TyConstRef ty + -> lazyMapIO (mkRef ty) =<< sampleType m ty + I.TyArr len ty + -> sampleArray m len ty + I.TyStruct ty + -> sampleStruct m ty + I.TyProc _ _ -> err + I.TyVoid -> err + I.TyPtr _ -> err + I.TyCArray _ -> err + I.TyOpaque -> err where - samples i label = mkSamples i (sampleStoredLabel label) + err = error $ "I don't know how to make values of type '" ++ show t ++ "'!" --------------------------------------------------------------------------------- +mkLocal :: (?counter :: IORef Integer) => I.Type -> I.Init -> IO (I.Var, I.Block) +mkLocal ty init = do + n <- mkUnique + let v = mkVar n + return (v, [I.Local ty v init]) +mkRef :: (?counter :: IORef Integer) => I.Type -> (I.Var, I.Block) + -> IO (I.Var, I.Block) +mkRef ty (v, init) = do + n <- mkUnique + let r = I.VarName ("ref" ++ show n) + return (r, init ++ [ I.AllocRef ty r (I.NameVar v) ]) + +mkVar :: Integer -> I.Var +mkVar n = I.VarName ("var" ++ show n) + +mk :: G.Gen a -> IO [a] +mk g = G.generate (G.infiniteListOf g) + +sampleInt :: I.IntSize -> IO [I.Init] +sampleInt sz = do + xs <- gen + return [ I.InitExpr (I.TyInt sz) (I.ExpLit (I.LitInteger x)) | x <- xs ] + where + gen = case sz of + I.Int8 -> fmap fromIntegral <$> mk (A.arbitrary :: G.Gen Int8) + I.Int16 -> fmap fromIntegral <$> mk (A.arbitrary :: G.Gen Int16) + I.Int32 -> fmap fromIntegral <$> mk (A.arbitrary :: G.Gen Int32) + I.Int64 -> fmap fromIntegral <$> mk (A.arbitrary :: G.Gen Int64) + +sampleWord :: I.WordSize -> IO [I.Init] +sampleWord sz = do + xs <- gen + return [ I.InitExpr (I.TyWord sz) (I.ExpLit (I.LitInteger x)) + | x <- xs + ] + where + gen = case sz of + I.Word8 -> fmap fromIntegral <$> mk (A.arbitrary :: G.Gen Word8) + I.Word16 -> fmap fromIntegral <$> mk (A.arbitrary :: G.Gen Word16) + I.Word32 -> fmap fromIntegral <$> mk (A.arbitrary :: G.Gen Word32) + I.Word64 -> fmap fromIntegral <$> mk (A.arbitrary :: G.Gen Word64) + +sampleIndex :: Integer -> IO [I.Init] +sampleIndex ix = do + xs <- mk (A.arbitrary :: G.Gen Word64) + return [ I.InitExpr (I.TyIndex ix) + (I.ExpLit (I.LitInteger (fromIntegral x `mod` ix))) + | x <- xs + ] + +sampleBool :: IO [I.Init] +sampleBool = do + bs <- mk A.arbitrary + return [I.InitExpr I.TyBool (I.ExpLit (I.LitBool b)) | b <- bs] + +sampleChar :: IO [I.Init] +sampleChar = do + cs <- mk A.arbitrary + return [I.InitExpr I.TyChar (I.ExpLit (I.LitChar c)) | c <- cs] + +sampleFloat :: IO [I.Init] +sampleFloat = do + cs <- mk A.arbitrary + return [I.InitExpr I.TyFloat (I.ExpLit (I.LitFloat c)) | c <- cs] + +sampleDouble :: IO [I.Init] +sampleDouble = do + cs <- mk A.arbitrary + return [I.InitExpr I.TyDouble (I.ExpLit (I.LitDouble c)) | c <- cs] + +sampleStruct :: (?counter :: IORef Integer) + => I.Module -> String -> IO [(I.Var, I.Block)] +sampleStruct m@(I.Module {..}) ty + = case find (\s -> ty == I.structName s) structs of + Just (I.Struct _ fields) -> repeatIO $ do + (vars, blcks) <- fmap unzip $ forM fields $ \ (I.Typed t _) -> + head <$> sampleType m t + let init = zipWith (\ (I.Typed t f) v -> (f, I.InitExpr t (I.ExpVar v))) + fields vars + (v, blck) <- mkLocal (I.TyStruct ty) (I.InitStruct init) + return (v, concat blcks ++ blck) + _ -> error ("I don't know how to construct a '" ++ ty ++ "'!") + where + structs = I.public modStructs ++ I.private modStructs + +sampleArray :: (?counter :: IORef Integer) + => I.Module -> Int -> I.Type + -> IO [(I.Var, I.Block)] +sampleArray m len ty = repeatIO $ do + (vars, blcks) <- unzip <$> replicateM len (head <$> sampleType m ty) + let init = [ I.InitExpr ty (I.ExpVar v) | v <- vars ] + (v, blck) <- mkLocal (I.TyArr len ty) (I.InitArray init) + return (v, concat blcks ++ blck) + +repeatIO :: IO a -> IO [a] +repeatIO doThis = do + x <- doThis + xs <- unsafeInterleaveIO (repeatIO doThis) + return (x : xs) + +lazyMapIO :: (a -> IO b) -> [a] -> IO [b] +lazyMapIO _ [] = return [] +lazyMapIO f (a:as) = do + b <- f a + bs <- unsafeInterleaveIO (lazyMapIO f as) + return (b : bs) + +zipLonger :: [[a]] -> [[b]] -> [([a], [b])] +zipLonger as bs = zip (as ++ repeat []) (bs ++ repeat []) diff --git a/src/Ivory/QuickCheck/Arbitrary.hs b/src/Ivory/QuickCheck/Arbitrary.hs deleted file mode 100644 --- a/src/Ivory/QuickCheck/Arbitrary.hs +++ /dev/null @@ -1,105 +0,0 @@ -{-# 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 deleted file mode 100644 --- a/src/Ivory/QuickCheck/Monad.hs +++ /dev/null @@ -1,48 +0,0 @@ -{-# 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 - --------------------------------------------------------------------------------- diff --git a/test/Test.hs b/test/Test.hs new file mode 100644 --- /dev/null +++ b/test/Test.hs @@ -0,0 +1,321 @@ +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-name-shadowing #-} + +module Main where + +import qualified Ivory.Language as L +import Ivory.Language hiding (Struct, assert, true, false, proc) +import qualified Ivory.Language.Proc as I +import qualified Ivory.Language.Syntax as I +import qualified Ivory.Stdlib as L +import Ivory.Compile.C.CmdlineFrontend + +import Control.Monad (when) +import System.Directory +import System.Exit +import System.FilePath.Posix +import System.IO +import System.Process + +import Ivory.QuickCheck (checkWith,contract) + +import Text.Printf + +import Test.Tasty (TestTree,defaultMain,testGroup) +import Test.Tasty.HUnit (assertBool,testCase) + + +main :: IO () +main = defaultMain tests + +tests :: TestTree +tests = testGroup "Tests" [ shouldPass, shouldFail ] + +shouldPass :: TestTree +shouldPass = testGroup "should be safe" + [ mkSuccess foo6 m6 + , mkSuccess foo7 m7 + , mkSuccess foo8 m8 + , mkSuccess foo9 m9 + , mkSuccess foo10 m10 + , mkSuccess foo11 m11 + , mkSuccess foo12 m12 + , mkSuccess foo13 m13 + , mkSuccess foo15 m15 + , mkSuccess foo17 m17 + , mkSuccess foo18 m18 + , mkSuccess foo19 m19 + , mkSuccess test_max mmax + ] + +shouldFail :: TestTree +shouldFail = testGroup "should be unsafe" + [ mkFailure foo1 m1 + , mkFailure foo14 m14 + ] + +mkSuccess :: Def (args ':-> res) -> Module -> TestTree +mkSuccess d@(~(I.DefProc p)) m = testCase (I.procSym p) $ do + (o, r) <- quickCheck d m + assertBool ("Expected quickcheck to pass: output:\n" ++ o) r + +mkFailure :: Def (args ':-> res) -> Module -> TestTree +mkFailure d@(~(I.DefProc p)) m = testCase (I.procSym p) $ do + (o, r) <- quickCheck d m + assertBool ("Expected quickcheck to fail: output:\n" ++ o) (not r) + + +quickCheck :: Def (args ':-> res) -> Module -> IO (String, Bool) +quickCheck d@(~(I.DefProc p)) m = do + tmpDir <- getTemporaryDirectory + let testDir = tmpDir "ivory-quickcheck" I.procSym p + b <- doesDirectoryExist testDir + when b $ removeDirectoryRecursive testDir + checkWith 100 (initialOpts { outDir = Just testDir }) [] m (contract d) + let cmd = printf "(cd %s && cc -std=c99 -DIVORY_TEST *.c && ./a.out)" testDir + (_,oh,eh,pid) <- runInteractiveCommand cmd + code <- waitForProcess pid + out <- hGetContents oh + err <- hGetContents eh + return (out ++ "\n" ++ err, code == ExitSuccess) + +-------------------------------------------------------------------------------- +-- test modules + +foo1 :: Def ('[Ix 10, Ix 10] ':-> ()) +foo1 = L.proc "foo1" $ \y x -> body $ do + ifte_ (y =? 3)) + retVoid + +m1 :: Module +m1 = package "foo1" (incl foo1) + +----------------------- + +foo6 :: Def ('[Uint8] ':-> ()) +foo6 = L.proc "foo6" $ \x -> body $ do + y <- local (ival (0 :: Uint8)) + ifte_ (x =? 7) + +m6 :: Module +m6 = package "foo6" (incl foo6) + +----------------------- + +foo7 :: Def ('[Uint8, Uint8] ':-> Uint8) +foo7 = L.proc "foo7" $ \x y -> + requires (x + y <=? 255) + $ body $ do + ret (x + y) + +m7 :: Module +m7 = package "foo7" (incl foo7) + +----------------------- + +foo8 :: Def ('[Uint8] ':-> Uint8) +foo8 = L.proc "foo8" $ \x -> body $ do + let y = x .% 3 + L.assert (y ()) +foo9 = L.proc "foo9" $ \f -> body $ do + st <- local (istruct [aFoo .= ival 0]) + a <- deref (st ~> aFoo) + L.assert (a ==? 0) + store (f ~> aFoo) 3 + store (f ~> bFoo ! 0) 1 + store (f ~> aFoo) 4 + x <- deref (f ~> aFoo) + y <- deref (f ~> bFoo ! 0) + L.assert (x ==? 4 L..&& y ==? 1) + +m9 :: Module +m9 = package "foo9" $ do + defStruct (Proxy :: Proxy "foo2") + incl foo9 + +----------------------- + +foo10 :: Def ('[Uint8] ':-> Uint8) +foo10 = L.proc "foo10" $ \x -> + requires (x r ==? x + 1) + $ body $ do + r <- assign $ x + 1 + ret r + +m10 :: Module +m10 = package "foo10" (incl foo10) + +----------------------- + +foo11 :: Def ('[Ix 10] ':-> ()) +foo11 = L.proc "foo11" $ \n -> body $ do + x <- local (ival (0 :: Sint8)) + for n $ \i -> do + x' <- deref x + store x $ x' + safeCast i + +m11 :: Module +m11 = package "foo11" (incl foo11) + +----------------------- + +foo12 :: Def ('[Uint8] ':-> Uint8) +foo12 = L.proc "foo12" $ \n -> + ensures (\r -> r ==? n) + $ body $ do + ifte_ (n ==? 0) + (ret n) + (do n' <- L.call foo12 (n-1) + ret (n' + 1)) + +m12 :: Module +m12 = package "foo12" (incl foo12) + +----------------------- + +foo13 :: Def ('[Uint8, Uint8] ':-> Uint8) +foo13 = L.proc "foo13" $ \x y -> + requires (x <=? 15) + $ requires (y <=? 15) + $ body $ ret (x * y) + +m13 :: Module +m13 = package "foo13" (incl foo13) + +----------------------- + +foo14 :: Def ('[Uint8, Uint8] ':-> Uint8) +foo14 = L.proc "foo14" $ \x y -> + ensures (\r -> r >=? x L..&& r >=? y) $ + body $ ret (x * y) + +m14 :: Module +m14 = package "foo14" (incl foo14) + +----------------------- + +foo15 :: Def ('[Ix 10] ':-> Uint8) +foo15 = L.proc "foo15" $ \n -> + ensures (\r -> r <=? 5) $ + body $ do + n `times` \i -> do + ifte_ (i >? 5) (ret 5) (ret $ safeCast i) + ret 4 -- FIXME: Ivory.Opts.TypeCheck doesn't see above `ret`s + +m15 :: Module +m15 = package "foo15" (incl foo15) + +----------------------- + +foo17 :: Def ('[ Ref 'Global ('Array 10 ('Stored Uint32))] ':-> ()) +foo17 = L.proc "foo17" $ \a -> body $ do + b <- local (iarray [ival 0, ival 1]) + refCopy b a + arrayMap (\ix -> store (a ! (ix :: Ix 10)) 1) + retVoid + +m17 :: Module +m17 = package "foo17" (incl foo17) + +----------------------- + +foo18 :: Def ('[Ref s ('L.Struct "foo2")] ':-> Ref s ('L.Struct "foo2")) +foo18 = L.proc "foo18" $ \f -> + requires (checkStored (f ~> aFoo) (\a -> a >? 0)) + $ requires (checkStored (f ~> aFoo) (\a -> a checkStored (r ~> aFoo) (\a -> a >? 1)) + $ body $ do + a <- deref (f ~> aFoo) + L.assert (a >? 0) + + store (f ~> aFoo) (a + 1) + ret f + +m18 :: Module +m18 = package "foo18" $ do + defStruct (Proxy :: Proxy "foo2") + incl foo18 + +----------------------- + +ppm_valid_area :: MemArea ('Stored IBool) +ppm_valid_area = area "ppm_valid" Nothing + +foo19 :: Def('[Ref s ('Array 1 ('Stored Uint32))] ':-> ()) +foo19 = L.proc "foo19" $ \ppms -> body $ do + all_good <- local (ival L.true) + ppm_last <- local (iarray []) + let ppm_valid = addrOf ppm_valid_area + arrayMap $ \ix -> do + x <- deref (ppms ! ix) + L.unless (x >=? 800 L..&& x <=? 2000) + (store all_good L.false) + + b <- deref all_good + L.unless b (store ppm_valid L.false) + L.when b $ do + (arrayMap $ \ix -> (deref (ppms ! ix) >>= store (ppm_last ! ix))) + store ppm_valid L.true + + valid <- deref ppm_valid + ppm <- deref (ppm_last ! 0) + L.assert (L.iNot valid .|| (ppm >=? 800 L..&& ppm <=? 2000)) + retVoid + +m19 :: Module +m19 = package "foo19" $ do + defMemArea ppm_valid_area + incl foo19 + +----------------------- + +[ivory| +int32_t test_max(int32_t a, int32_t b) { + return (a > b) ? a : b; +} +{ + post(return >= a && return >= b); + post(return == a || return == b); +} +|] + +mmax :: Module +mmax = package "max" (incl test_max)