ivory-quickcheck 0.1.0.0 → 0.2.0.3
raw patch · 5 files changed
+643/−261 lines, 5 filesdep +base-compatdep +directorydep +filepathdep ~QuickCheckdep ~base
Dependencies added: base-compat, directory, filepath, ivory-backend-c, ivory-eval, ivory-quickcheck, ivory-stdlib, process, tasty, tasty-hunit
Dependency ranges changed: QuickCheck, base
Files
- ivory-quickcheck.cabal +31/−9
- src/Ivory/QuickCheck.hs +291/−99
- src/Ivory/QuickCheck/Arbitrary.hs +0/−105
- src/Ivory/QuickCheck/Monad.hs +0/−48
- test/Test.hs +321/−0
ivory-quickcheck.cabal view
@@ -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
src/Ivory/QuickCheck.hs view
@@ -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 @<pwd>/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 [])
− src/Ivory/QuickCheck/Arbitrary.hs
@@ -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)----------------------------------------------------------------------------------
− src/Ivory/QuickCheck/Monad.hs
@@ -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----------------------------------------------------------------------------------
+ test/Test.hs view
@@ -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)+ (do ifte_ (y ==? 3)+ (L.assert $ y ==? 0)+ retVoid)+ (do z <- assign x+ -- this *should* fail+ L.assert (z >=? 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 <? 3)+ (do a <- local (ival (9 :: Uint8))+ b <- deref a+ store y b+ )+ (do a <- local (ival (7 :: Uint8))+ b <- deref a+ store y b+ )+ z <- deref y+ L.assert (z <=? 9)+ L.assert (z >=? 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 <? 4)+ ret y++m8 :: Module+m8 = package "foo8" (incl foo8)++-----------------------++[ivory|+struct foo2+{ aFoo :: Stored Uint8+; bFoo :: (Array 4 Uint8)+}+|]++foo9 :: Def ('[Ref s ('L.Struct "foo2")] ':-> ())+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 <? 10)+ $ ensures (\r -> 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 <? 10))+ $ ensures (\r -> 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)