diff --git a/examples/AddrOfRegression.hs b/examples/AddrOfRegression.hs --- a/examples/AddrOfRegression.hs +++ b/examples/AddrOfRegression.hs @@ -21,13 +21,13 @@ defMemArea param_info_area incl t1 where - param_info_area :: MemArea (Array 512 (Struct "param_info")) + param_info_area :: MemArea ('Array 512 ('Struct "param_info")) param_info_area = area "g_param_info" Nothing - param_info_ref :: Ref Global (Array 512 (Struct "param_info")) + param_info_ref :: Ref 'Global ('Array 512 ('Struct "param_info")) param_info_ref = addrOf param_info_area - t1 :: Def ('[]:->()) + t1 :: Def ('[] ':-> ()) t1 = proc "t1" $ body $ do arrayMap $ \ix -> store ((param_info_ref ! ix) ~> param_requested) 1 @@ -37,13 +37,13 @@ defMemArea param_info_area incl t1 where - param_info_area :: MemArea (Struct "param_info") + param_info_area :: MemArea ('Struct "param_info") param_info_area = area "single_param_info" Nothing - param_info_ref :: Ref Global (Struct "param_info") + param_info_ref :: Ref 'Global ('Struct "param_info") param_info_ref = addrOf param_info_area - t1 :: Def ('[]:->()) + t1 :: Def ('[] ':-> ()) t1 = proc "t1_noarray" $ body $ do store (param_info_ref ~> param_requested) 1 @@ -52,13 +52,13 @@ defMemArea atom_array_area incl t2 where - atom_array_area :: MemArea (Array 512 (Stored IFloat)) + atom_array_area :: MemArea ('Array 512 ('Stored IFloat)) atom_array_area = area "atom_array" Nothing - atom_array_ref :: Ref Global (Array 512 (Stored IFloat)) + atom_array_ref :: Ref 'Global ('Array 512 ('Stored IFloat)) atom_array_ref = addrOf atom_array_area - t2 :: Def ('[]:->()) + t2 :: Def ('[] ':-> ()) t2 = proc "t2" $ body $ do arrayMap $ \ix -> store (atom_array_ref ! ix) 1 @@ -67,9 +67,9 @@ test3 = do incl t3 where - t3 :: Def ('[]:->()) + t3 :: Def ('[] ':-> ()) t3 = proc "t3" $ body $ do - (stack_array :: Ref (Stack s) (Array 512 (Stored IFloat))) <- local izero + (stack_array :: Ref ('Stack s) ('Array 512 ('Stored IFloat))) <- local izero arrayMap $ \ix -> store (stack_array ! ix) 1 diff --git a/examples/Alloc.hs b/examples/Alloc.hs --- a/examples/Alloc.hs +++ b/examples/Alloc.hs @@ -26,26 +26,27 @@ |] -test :: Def ('[Ref s (Struct "Foo")] :-> Ref s (Stored Uint32)) -test = proc "test" (\ pid -> body (ret (pid ~> i))) +test :: Def ('[Ref s ('Struct "Foo")] ':-> Ref s ('Stored Uint32)) +test = proc "alloc_test" (\ pid -> body (ret (pid ~> i))) -alloc_test :: Def ('[] :-> Uint32) -alloc_test = proc "alloc_test" $ body $ do +get_p :: Def ('[] ':-> Uint32) +get_p = proc "get_p" $ body $ do pid <- local (istruct []) ret =<< deref (pid ~> d) -memcpy1 :: Def ('[ Ref a (Struct "Foo"), Ref a (Struct "Foo") ] :-> Uint32) +memcpy1 :: Def ('[ Ref a ('Struct "Foo"), Ref a ('Struct "Foo") ] ':-> Uint32) memcpy1 = proc "memcpy1" $ \a b -> body $ do refCopy b a ret =<< deref (b ~> i) -memcpy2 :: Def ('[ Ref a (Array 10 (Stored Uint32)), Ref a (Array 10 (Stored Uint32)) ] :-> ()) +memcpy2 :: Def ('[ Ref a ('Array 10 ('Stored Uint32)) + , Ref a ('Array 10 ('Stored Uint32)) ] ':-> ()) memcpy2 = proc "memcpy2" $ \a b -> body $ do refCopy b a arrayMap (\ix -> store (a ! (ix :: Ix 10)) 1) retVoid -memcpy3 :: Def ('[ Ref Global (Array 10 (Stored Uint32))] :-> ()) +memcpy3 :: Def ('[ Ref 'Global ('Array 10 ('Stored Uint32))] ':-> ()) memcpy3 = proc "memcpy3" $ \a -> body $ do b <- local (iarray $ replicate 10 (ival $ 0)) refCopy b a @@ -69,59 +70,61 @@ ret (pid~>i) -} -arrMap :: Def ('[Ref s (Array 15 (Stored Sint32))] :-> ()) +arrMap :: Def ('[Ref s ('Array 15 ('Stored Sint32))] ':-> ()) arrMap = proc "arrMap" $ \ arr -> body $ do arrayMap (\ix -> store (arr ! (ix :: Ix 15)) 1) retVoid -- String copy test ------------------------- -ptrstrcpy :: Def ('[Ref s (CArray (Stored IChar)), IString, Uint32] :-> ()) +ptrstrcpy :: Def ('[ Ref s ('CArray ('Stored IChar)) + , IString + , Uint32] ':-> ()) ptrstrcpy = proc "ptrstrcpy" $ \ _ _ _ -> body $ do retVoid -callstrcpy :: Def ('[] :-> ()) +callstrcpy :: Def ('[] ':-> ()) callstrcpy = proc "callstrcpy" $ body $ do buf' <- local (iarray []) call_ mystrcpy buf' "hello" retVoid -- | Safely copy a string literal into a character array. -mystrcpy :: Def ('[Ref s (Array 10 (Stored IChar)), IString] :-> ()) +mystrcpy :: Def ('[Ref s ('Array 10 ('Stored IChar)), IString] ':-> ()) mystrcpy = proc "mystrcpy" $ \ buf s -> body $ do buf' <- assign $ toCArray buf call_ ptrstrcpy buf' s (arrayLen buf) retVoid -assign_test :: Def ('[] :-> ()) +assign_test :: Def ('[] ':-> ()) assign_test = proc "assign_test" $ body $ do val <- local (istruct []) _ <- assign (val ~> p) retVoid -bar :: Def ('[] :-> ()) -bar = proc "var" $ body $ do - pid <- local $ istruct [i .= ival 3, i .= ival 7] +bar :: Def ('[] ':-> ()) +bar = proc "bar" $ body $ do + pid <- local $ istruct [i .= ival 3] arr <- local $ iarray [ ival c | c <- replicate 10 (char 'a') ] call_ mystrcpy arr "hello" store (pid~>i) 4 -castIx :: Def ('[Ix 253] :-> Uint8) +castIx :: Def ('[Ix 253] ':-> Uint8) castIx = proc "castIx" $ \ix -> body $ do ret $ safeCast (ix :: Ix 253) -loopTest :: Def ('[Ref s (Array 15 (Stored Sint32))] :-> ()) +loopTest :: Def ('[Ref s ('Array 15 ('Stored Sint32))] ':-> ()) loopTest = proc "loopTest" $ \ arr -> body $ do arrayMap (\ix -> store (arr ! (ix :: Ix 15)) 1) times 3 (\ix -> store (arr ! (ix :: Ix 15)) 1) for 0 (\ix -> store (arr ! (ix :: Ix 15)) 1) retVoid -testToIx :: Def ('[Sint32, Ref s (Array 10 (Stored Uint32))] :-> Ref s (Stored Uint32)) +testToIx :: Def ('[Sint32, Ref s ('Array 10 ('Stored Uint32))] ':-> Ref s ('Stored Uint32)) testToIx = proc "testToIx" $ \ ind arr -> body $ do let idx = toIx ind :: Ix 10 ret (arr ! idx) -arrayTest :: MemArea (Array 10 (Struct "Foo")) +arrayTest :: MemArea ('Array 10 ('Struct "Foo")) arrayTest = area "arrayTest" $ Just $ iarray [ istruct [ i .= ival 10 ] ] @@ -136,7 +139,7 @@ -- ], procRequires = [], procEnsures = Nothing}) -- uint32_t n_deref0 = *&n_var0->i; -foo :: Def ('[Ref s (Struct "Foo")] :-> Uint32) +foo :: Def ('[Ref s ('Struct "Foo")] ':-> Uint32) foo = proc "foo" $ \str -> body $ do ret =<< deref (str ~> i) @@ -152,7 +155,7 @@ -- [], procEnsures = Nothing}) -- uint32_t n_deref0 = *&n_var0->p[0 % 10]; -foo2 :: Def ('[Ref s (Struct "Foo")] :-> Uint32) +foo2 :: Def ('[Ref s ('Struct "Foo")] ':-> Uint32) foo2 = proc "foo2" $ \str -> body $ do let arr = (str ~> p) let x = arr ! (0 :: Ix 10) @@ -170,16 +173,12 @@ defStruct (Proxy :: Proxy "Foo") defStruct (Proxy :: Proxy "Str") incl test - incl alloc_test + incl get_p incl arrMap - incl ptrstrcpy incl mystrcpy - incl callstrcpy - incl assign_test - incl bar incl castIx incl loopTest @@ -187,11 +186,10 @@ incl memcpy2 incl testToIx incl memcpy3 - defMemArea arrayTest runAlloc :: IO () -runAlloc = runCompiler [cmodule] initialOpts { stdOut = True } +runAlloc = runCompiler [cmodule] [] initialOpts { outDir = Nothing } -test2 :: [[String]] +test2 :: String test2 = showModule (compileModule cmodule) diff --git a/examples/Area.hs b/examples/Area.hs --- a/examples/Area.hs +++ b/examples/Area.hs @@ -7,7 +7,7 @@ module Area where import Ivory.Language - +import Ivory.Compile.C.CmdlineFrontend [ivory| @@ -17,17 +17,17 @@ |] -val :: MemArea (Struct "val") -val = area "val" (Just (istruct [field .= ival 0])) +val :: MemArea ('Struct "val") +val = area "value" (Just (istruct [field .= ival 0])) -cval :: ConstMemArea (Struct "val") +cval :: ConstMemArea ('Struct "val") cval = constArea "cval" (istruct [field .= ival 10]) -getVal :: Def ('[] :-> Uint32) +getVal :: Def ('[] ':-> Uint32) getVal = proc "getVal" $ body $ do ret =<< deref (addrOf val ~> field) -setVal :: Def ('[Uint32] :-> ()) +setVal :: Def ('[Uint32] ':-> ()) setVal = proc "setVal" $ \ n -> body $ do store (addrOf val ~> field) n retVoid @@ -39,3 +39,6 @@ defMemArea val defConstMemArea cval defStruct (Proxy :: Proxy "val") + +main :: IO () +main = runCompiler [cmodule] [] initialOpts { outDir = Nothing, constFold = True } diff --git a/examples/Array.hs b/examples/Array.hs --- a/examples/Array.hs +++ b/examples/Array.hs @@ -7,13 +7,26 @@ import Ivory.Compile.C.CmdlineFrontend cmodule :: Module -cmodule = package "Array" $ incl arrayExample +cmodule = package "Array" $ do + incl arrayExample + incl arrayTernary runArrayExample :: IO () -runArrayExample = runCompiler [cmodule] initialOpts { stdOut = True } +runArrayExample = runCompiler [cmodule] [] initialOpts { outDir = Nothing } -arrayExample :: Def('[Ref s (Array 4 (Stored Uint8)), Uint8] :-> ()) +arrayExample :: Def('[Ref s ('Array 4 ('Stored Uint8)), Uint8] ':-> ()) arrayExample = proc "arrayExample" $ \arr n -> body $ do arrayMap $ \ ix -> do v <- deref (arr ! ix) store (arr ! ix) (v + n) + + +arrayTernary :: Def('[IBool] ':-> IFloat) +arrayTernary = proc "arrayTernary" $ \b -> body $ do + a1 <- local (vs 1) + a2 <- local (vs 2) + ares <- assign (b ? (a1, a2)) + deref (ares ! 3) >>= ret + where + vs :: IFloat -> Init ('Array 4 ('Stored IFloat)) + vs v = iarray (map ival [v, v, v, v]) diff --git a/examples/BitData.hs b/examples/BitData.hs new file mode 100644 --- /dev/null +++ b/examples/BitData.hs @@ -0,0 +1,144 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +{-# OPTIONS_GHC -fno-warn-missing-signatures #-} + +module BitData where + +import Control.Monad + +import Ivory.Language +import Ivory.Compile.C.CmdlineFrontend + +import BitDataTypes +import Ivory.Language.BitData.Array (ArraySize) +import Ivory.Language.BitData.Bits (BitSize) +import Ivory.Language.BitData.BitData (BitType) + +[ivory| + + bitdata SPI_CR1 :: Bits 16 = spi_cr1 + { spi_cr1_bidimode :: Bit + , spi_cr1_bidioe :: Bit + , spi_cr1_crcen :: Bit + , spi_cr1_crcnext :: Bit + , spi_cr1_dff :: Bit + , spi_cr1_rxonly :: Bit + , spi_cr1_ssm :: Bit + , spi_cr1_ssi :: Bit + , spi_cr1_lsbfirst :: Bit + , spi_cr1_spe :: Bit + , spi_cr1_br :: SPIBaud + , spi_cr1_mstr :: Bit + , spi_cr1_cpol :: Bit + , spi_cr1_cpha :: Bit + } + + -- The "SPI_CR2" register defined using a layout clause. + bitdata SPI_CR2 :: Bits 16 = spi_cr2 + { spi_cr2_txeie :: Bit + , spi_cr2_rxneie :: Bit + , spi_cr2_errie :: Bit + , spi_cr2_frf :: Bit + , spi_cr2_ssoe :: Bit + , spi_cr2_txdmaen :: Bit + , spi_cr2_rxdmaen :: Bit + } as 8b0 # spi_cr2_txeie # spi_cr2_rxneie # spi_cr2_errie # spi_cr2_frf + # 1b0 # spi_cr2_ssoe # spi_cr2_txdmaen # spi_cr2_rxdmaen + + -- The "SPI_CR2" register defined using the default layout and + -- padding fields. + bitdata Alt_SPI_CR2 :: Bits 16 = alt_spi_cr2 + { _ :: Bits 8 + , alt_spi_cr2_txeie :: Bit + , alt_spi_cr2_rxneie :: Bit + , alt_spi_cr2_errie :: Bit + , alt_spi_cr2_frf :: Bit + , _ :: Bit + , alt_spi_cr2_ssoe :: Bit + , alt_spi_cr2_txdmaen :: Bit + , alt_spi_cr2_rxdmaen :: Bit + } + + -- The "NVIC_ISER" register is an array of 32 bits. + -- + -- We will want to access the array both at Ivory run-time using an + -- "Ix 32" and at code generation time using a Haskell integer. + bitdata NVIC_ISER :: Bits 32 = nvic_iser + { nvic_iser_setena :: BitArray 32 Bit + } + + -- A bit data type with an array of 4-bit integers. + bitdata ArrayTest :: Bits 32 = array_test + { at_4bits :: BitArray 8 (Bits 4) + } +|] + +test1 :: Def ('[Uint16] ':-> Uint16) +test1 = proc "test1" $ \x -> body $ do + ret $ withBits x $ do + clearBit spi_cr1_cpha + setBit spi_cr1_cpol + setField spi_cr1_br spi_baud_div_8 + +test2 :: Def ('[Uint32] ':-> Uint8) +test2 = proc "test2" $ \x -> body $ do + let d = fromRep x :: NVIC_ISER + ret $ toRep (d #. nvic_iser_setena #! 0) + +-- | Iterate over the elements of a bit array. +forBitArray_ :: + ( ANat n + , BitCast (BitRep (ArraySize n a)) (BitRep (BitSize (BitType a))) + , IvoryStore (BitRep (ArraySize n a)) + , IvoryOrd (BitRep (ArraySize n a)) + , IvoryZeroVal (BitRep (ArraySize n a)) + , IvoryInit (BitRep (ArraySize n a)) + , BitData a + , ANat (BitSize a) + , ANat (ArraySize n a) + ) => BitArray n a -> (a -> Ivory eff ()) -> Ivory eff () +forBitArray_ arr f = + forM_ [0..bitLength arr] $ \i -> + f (arr #! i) + +-- | Test looping over the elements of a bit array: +test3 :: Def ('[Uint32] ':-> Uint32) +test3 = proc "test3" $ \x -> body $ do + let d = fromRep x + total <- local (ival 0) + forBitArray_ (d #. at_4bits) $ \i -> do + x' <- deref total + let y = safeCast (toRep i) + store total (x' + y) + ret =<< deref total + +get_baud :: Def ('[Uint16] ':-> Uint8) +get_baud = proc "get_baud" $ \x -> body $ do + let d = fromRep x + ret (toRep (d #. spi_cr1_br)) + +-- | Examples from Ivory paper: +[ivory| + bitdata CtrlReg :: Bits 8 = ctrl_reg + { ctrl_tx_enable :: Bit + , ctrl_rx_enable :: Bit + , ctrl_baud_rate :: BaudRate + } as 0b0000 # ctrl_tx_enable # ctrl_rx_enable # ctrl_baud_rate +|] + +cmodule :: Module +cmodule = package "hw" $ do + incl get_baud + incl test1 + incl test2 + incl test3 + +main :: IO () +main = runCompiler [cmodule] [] (initialOpts {outDir = Nothing, constFold = True}) diff --git a/examples/BitDataTypes.hs b/examples/BitDataTypes.hs new file mode 100644 --- /dev/null +++ b/examples/BitDataTypes.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} + +module BitDataTypes where + +import Ivory.Language + +[ivory| + bitdata SPIBaud :: Bits 3 + = spi_baud_div_2 as 0 + | spi_baud_div_4 as 1 + | spi_baud_div_8 as 2 + | spi_baud_div_16 as 3 + | spi_baud_div_32 as 4 + | spi_baud_div_64 as 5 + | spi_baud_div_128 as 6 + | spi_baud_div_256 as 7 +|] + +-- | Examples from Ivory paper. +[ivory| + bitdata BaudRate :: Bits 2 + = baud_9600 as 0b00 + | baud_19200 as 0b01 + | baud_38400 as 0b10 + -- bit pattern 0b11 is invalid +|] diff --git a/examples/Bits.hs b/examples/Bits.hs --- a/examples/Bits.hs +++ b/examples/Bits.hs @@ -4,11 +4,11 @@ module Bits (runBits, cmodule) where import Ivory.Compile.C.CmdlineFrontend -import Ivory.Language +import Ivory.Language hiding (setBit, clearBit, runBits) import MonadLib.Monads (runState, sets) runBits :: IO () -runBits = runCompiler [cmodule] initialOpts {stdOut = True} +runBits = runCompiler [cmodule] [] initialOpts {outDir = Nothing} cmodule :: Module cmodule = package "Bits" $ do @@ -16,8 +16,10 @@ incl test2 incl test3 incl test4 + incl test5 + incl test6 -test1 :: Def ('[Uint8, Uint16, Uint32, Uint64] :-> Uint64) +test1 :: Def ('[Uint8, Uint16, Uint32, Uint64] ':-> Uint64) test1 = proc "test1" $ \u8 u16 u32 u64 -> body $ do a <- assign $ u8 .& 0xFF b <- assign $ u16 .& 0xFF00 @@ -26,7 +28,7 @@ ret $ (safeCast a) .| (safeCast b) .| (safeCast c) .| d -- | Convert an array of four 8-bit integers into a 32-bit integer. -test2 :: Def ('[Ref s (Array 4 (Stored Uint8))] :-> Uint32) +test2 :: Def ('[Ref s ('Array 4 ('Stored Uint8))] ':-> Uint32) test2 = proc "test2" $ \arr -> body $ do a <- deref (arr ! 0) b <- deref (arr ! 1) @@ -47,7 +49,7 @@ return (a, b, c, d) -- | Convert a 32-bit integer to an array of 8-bit integers. -test3 :: Def ('[Uint32, Ref s (Array 4 (Stored Uint8))] :-> ()) +test3 :: Def ('[Uint32, Ref s ('Array 4 ('Stored Uint8))] ':-> ()) test3 = proc "test3" $ \n arr -> body $ do let (a, b, c, d) = extractUint32 n store (arr ! 0) d @@ -56,18 +58,18 @@ store (arr ! 3) a setBit :: (IvoryBits a, IvoryStore a) - => (Ref s (Stored a)) -> Int -> Ivory eff () + => (Ref s ('Stored a)) -> Int -> Ivory eff () setBit ref bit = do val <- deref ref store ref (val .| (1 `iShiftL` (fromIntegral bit))) clearBit :: (IvoryBits a, IvoryStore a) - => (Ref s (Stored a)) -> Int -> Ivory eff () + => (Ref s ('Stored a)) -> Int -> Ivory eff () clearBit ref bit = do val <- deref ref store ref (val .& (iComplement (1 `iShiftL` (fromIntegral bit)))) -test4 :: Def ('[] :-> Uint32) +test4 :: Def ('[] ':-> Uint32) test4 = proc "test4" $ body $ do n <- local (ival 0) setBit n 1 @@ -76,3 +78,11 @@ setBit n 8 clearBit n 3 ret =<< deref n + +test5 :: Def ('[Sint8] ':-> Uint8) +test5 = proc "test5" $ \s -> body $ + ret (twosComplementRep s) + +test6 :: Def ('[Uint8] ':-> Sint8) +test6 = proc "test6" $ \s -> body $ + ret (twosComplementCast s) diff --git a/examples/ConcreteFile.hs b/examples/ConcreteFile.hs new file mode 100644 --- /dev/null +++ b/examples/ConcreteFile.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE OverloadedStrings #-} + +{-# OPTIONS_GHC -fno-warn-orphans -fno-warn-unused-binds -fno-warn-unused-matches #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-missing-signatures #-} + +-- +-- C-like syntax for Ivory, parsed from a file. +-- +-- Copyright (C) 2014, Galois, Inc. +-- All rights reserved. +-- + +module ConcreteFile where + +import Ivory.Language +import Ivory.Stdlib +import Ivory.Compile.C.CmdlineFrontend + +e :: IBool +e = (4::Sint32) >? 3 + +type SomeInt = Uint32 + +macroStmts :: + (Num a, IvoryStore a, IvoryInit a, GetAlloc eff ~ 'Scope s) + => a -> a -> Ivory eff () +macroStmts x y = do + a <- local (ival 0) + store a (x + y) + +macroStmtsRet :: + (Num a, IvoryStore a, IvoryInit a, GetAlloc eff ~ 'Scope s) + => a -> a -> Ivory eff a +macroStmtsRet x y = do + a <- local (ival 0) + store a (x + y) + return =<< deref a + +macroExp :: IvoryOrd a => a -> a -> IBool +macroExp x y = do + x Uint32 -> Ix n +toIx' ix = toIx (twosComplementCast ix) + +concreteIvory :: Module +concreteIvory = package "concreteIvory" $ do + incl printf + incl printf2 + +[ivoryFile|examples/file.ivory|] + +main :: IO () +main = runCompiler [concreteIvory, examplesfile, stdlibStringModule] stdlibStringArtifacts + initialOpts {outDir = Just "concrete-ivory", constFold = True} + + diff --git a/examples/Cond.hs b/examples/Cond.hs --- a/examples/Cond.hs +++ b/examples/Cond.hs @@ -7,7 +7,7 @@ import Ivory.Compile.C.CmdlineFrontend import Prelude hiding (exp) -add :: Def ('[Uint32,Uint32] :-> Uint32) +add :: Def ('[Uint32,Uint32] ':-> Uint32) add = proc "add" $ \ x y -> ensures (\r -> r ==? x + y) $ body @@ -18,7 +18,7 @@ -- Testing assertions with choice expression -foo :: Def ('[IFloat,IFloat,IFloat] :-> IFloat) +foo :: Def ('[IFloat,IFloat,IFloat] ':-> IFloat) foo = proc "foo" $ \x y z -> body $ do let cond = 2/x ==? 5 let tCond = 6/y ==? 7 @@ -29,6 +29,7 @@ fooMod = package "fooM" $ incl foo runFoo :: IO () -runFoo = runCompiler [fooMod] initialOpts { stdOut = True - , divZero = True - } +runFoo = runCompiler [fooMod] [] + initialOpts { outDir = Nothing + , divZero = True + } diff --git a/examples/Coroutine.hs b/examples/Coroutine.hs new file mode 100644 --- /dev/null +++ b/examples/Coroutine.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} + +module Coroutine where + +import Ivory.Language +import Ivory.Compile.C.CmdlineFrontend + +-- No-op "action" for the coroutine to trigger +emit :: Def ('[Sint32] ':-> ()) +emit = proc "emit" $ \ _ -> body $ retVoid + +sequenced :: Coroutine ('Stored Sint32) +sequenced = coroutine "sequenced" $ CoroutineBody $ \ yield -> do + forever $ do + call_ emit 1 + v <- yield >>= deref + ifte_ (v ==? 1) breakOut (return ()) + call_ emit 2 + forever $ do + v <- yield >>= deref + ifte_ (v ==? 2) + (call_ emit 3) + (call_ emit 2) + +run :: Def ('[IBool, ConstRef s ('Stored Sint32)] ':-> ()) +run = proc "run" $ \ doInit arg -> body $ coroutineRun sequenced doInit arg + +cmodule :: Module +cmodule = package "sequenced" $ do + incl emit + incl run + coroutineDef sequenced + +main :: IO () +main = compile [cmodule] [] diff --git a/examples/Factorial.hs b/examples/Factorial.hs --- a/examples/Factorial.hs +++ b/examples/Factorial.hs @@ -6,7 +6,7 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -factorial :: Def ('[Sint32] :-> Sint32) +factorial :: Def ('[Sint32] ':-> Sint32) factorial = proc "factorial" $ \ n -> -- These are made up requires/ensures for testing purposes. ensures (\r -> n ),(<*>)) - -- Recursive implementation of fib -fib_rec :: Def ('[Uint32] :-> Uint64) +fib_rec :: Def ('[Uint32] ':-> Uint64) fib_rec = proc "fib_rec" (\n -> body (ret =<< call fib_rec_aux 0 1 n)) -fib_rec_aux :: Def ('[Uint32,Uint32,Uint32] :-> Uint64) +fib_rec_aux :: Def ('[Uint32,Uint32,Uint32] ':-> Uint64) fib_rec_aux = proc "fib_rec_aux" $ \ a b n -> body $ do ifte_ (n ==? 0) (ret (safeCast a)) @@ -23,19 +25,23 @@ -- Loop implementation of fib. -fib_loop :: Def ('[Ix 1000] :-> Uint32) +fib_loop :: Def ('[Ix 1000] ':-> Uint32) fib_loop = proc "fib_loop" $ \ n -> body $ do a <- local (ival 0) - b <- local (ival 0) - - n `times` \ _ -> do + b <- local (ival 1) + comment "before loop" + n `times` \ _ix -> do + comment "inside top of loop" a' <- deref a b' <- deref b store a b' store b (a' + b') + comment "inside end of loop" + comment "after end of loop" result <- deref a ret result + -- comment "after return" -- Loop implementation of fib, using a structure instead -- of two discrete variables. @@ -46,7 +52,7 @@ } |] -fib_struct_loop :: Def ('[Ix 1000] :-> Uint32) +fib_struct_loop :: Def ('[Ix 1000] ':-> Uint32) fib_struct_loop = proc "fib_struct_loop" $ \ n -> body $ do state <- local (istruct [ sa .= ival 0 , sb .= ival 0 ]) @@ -68,4 +74,4 @@ incl fib_struct_loop runFibLoop :: IO () -runFibLoop = runCompiler [cmodule] initialOpts { stdOut = True, constFold = True } +runFibLoop = runCompiler [cmodule] [] initialOpts { outDir = Nothing, constFold = True } diff --git a/examples/FibTutorial.hs b/examples/FibTutorial.hs deleted file mode 100644 --- a/examples/FibTutorial.hs +++ /dev/null @@ -1,26 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeOperators #-} - -import Ivory.Language -import qualified Ivory.Compile.C.CmdlineFrontend as C (compile) - -fib_loop :: Def ('[Ix 1000] :-> Uint32) -fib_loop = proc "fib_loop" $ \ n -> body $ do - a <- local (ival 0) - b <- local (ival 1) - - n `times` \ _ -> do - a' <- deref a - b' <- deref b - store a b' - store b (a' + b') - - result <- deref a - ret result - -fib_tutorial_module :: Module -fib_tutorial_module = package "fib_tutorial" $ do - incl fib_loop - -main :: IO () -main = C.compile [ fib_tutorial_module ] diff --git a/examples/Float.hs b/examples/Float.hs --- a/examples/Float.hs +++ b/examples/Float.hs @@ -7,15 +7,15 @@ import Ivory.Language runFloat :: IO () -runFloat = runCompiler [cmodule] initialOpts { stdOut = True } +runFloat = runCompiler [cmodule] [] initialOpts { outDir = Nothing } cmodule :: Module cmodule = package "Float" $ do incl test1 incl test2 -test1 :: Def ('[IFloat] :-> Sint32) +test1 :: Def ('[IFloat] ':-> Sint32) test1 = proc "test1" (\ f -> body (ret (castDefault f))) -test2 :: Def ('[Sint32] :-> IFloat) +test2 :: Def ('[Sint32] ':-> IFloat) test2 = proc "test2" (\ i -> body (ret (safeCast i))) diff --git a/examples/Forever.hs b/examples/Forever.hs --- a/examples/Forever.hs +++ b/examples/Forever.hs @@ -6,7 +6,7 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -factorial :: Def ('[Sint32] :-> Sint32) +factorial :: Def ('[Sint32] ':-> Sint32) factorial = proc "factorial" $ \ n -> -- These are made up requires/ensures for testing purposes. ensures (\r -> n ()) +printResult :: Def ('[Sint32] ':-> ()) printResult = proc "print_result" $ \_ -> body retVoid -foreverFactorial :: Def ('[Sint32] :-> ()) +foreverFactorial :: Def ('[Sint32] ':-> ()) foreverFactorial = proc "forever_factorial" $ \ n -> body $ do forever $ do res <- call factorial n @@ -33,5 +33,5 @@ incl foreverFactorial runFactorial :: IO () -runFactorial = runCompiler [cmodule] initialOpts { stdOut = True } +runFactorial = runCompiler [cmodule] [] initialOpts { outDir = Nothing } diff --git a/examples/FunPtr.hs b/examples/FunPtr.hs --- a/examples/FunPtr.hs +++ b/examples/FunPtr.hs @@ -6,17 +6,17 @@ import Ivory.Compile.C.CmdlineFrontend import Ivory.Language -f :: Def ('[Sint32] :-> Sint32) +f :: Def ('[Sint32] ':-> Sint32) f = proc "f" (\ n -> body (ret (n + 1))) -invoke :: Def ('[ ProcPtr ('[Sint32] :-> Sint32), Sint32] :-> Sint32) +invoke :: Def ('[ ProcPtr ('[Sint32] ':-> Sint32), Sint32] ':-> Sint32) invoke = proc "invoke" (\ k n -> body (ret =<< indirect k n)) -test :: Def ('[] :-> Sint32) -test = proc "test" (body (ret =<< call invoke (procPtr f) 10)) +test :: Def ('[] ':-> Sint32) +test = proc "fun_ptr_test" (body (ret =<< call invoke (procPtr f) 10)) runFunPtr :: IO () -runFunPtr = runCompiler [cmodule] initialOpts { stdOut = True } +runFunPtr = runCompiler [cmodule] [] initialOpts { outDir = Nothing } cmodule :: Module cmodule = package "FunPtr" $ do diff --git a/examples/Loop.hs b/examples/Loop.hs new file mode 100644 --- /dev/null +++ b/examples/Loop.hs @@ -0,0 +1,19 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} + +module Loop where + +import Ivory.Language +import Ivory.Compile.C.CmdlineFrontend + +cmodule :: Module +cmodule = package "Loop" $ do + incl loopTest0 + +runLoopExample :: IO () +runLoopExample = runCompiler [cmodule] [] initialOpts { outDir = Nothing } + +loopTest0 :: Def ('[] ':-> ()) +loopTest0 = proc "loopTest" $ body $ + do (0 :: Ix 1) `times` \ _ -> return () + retVoid diff --git a/examples/Overflow.hs b/examples/Overflow.hs --- a/examples/Overflow.hs +++ b/examples/Overflow.hs @@ -6,25 +6,27 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -ovf1 :: Def ('[Sint8] :-> Sint8) +ovf1 :: Def ('[Sint8] ':-> Sint8) ovf1 = proc "ovf1" $ \ n -> body $ ifte_ (n Sint8) +ovf2 :: Def ('[Sint8] ':-> Sint8) ovf2 = proc "ovf2" $ \ n -> requires (n IBool) +ovf3 :: Def ('[IFloat, IFloat, IBool] ':-> IFloat) ovf3 = proc "ovf3" $ \ n m o -> body $ do - x <- assign (n / m / o) - ret $ x >? (n / m) +-- x <- assign (n / m / o) + ret $ (o ? (n / m, m / n)) cmodule :: Module -cmodule = package "Overflow" $ incl ovf1 >> incl ovf2 >> incl ovf3 +cmodule = package "Overflow" $ --incl ovf1 >> incl ovf2 >> + incl ovf3 writeOverflow :: Opts -> IO () -writeOverflow opts = runCompiler [cmodule] - opts { constFold = True, overflow = True, divZero = True } +writeOverflow opts = runCompiler [cmodule] [] + opts { constFold = False, overflow = False, divZero = True, outDir = Nothing } + diff --git a/examples/PID.hs b/examples/PID.hs --- a/examples/PID.hs +++ b/examples/PID.hs @@ -45,11 +45,11 @@ ki = 0.1 kd = 0.1 -pidUpdate :: Def ('[ Ref s (Struct "PID") +pidUpdate :: Def ('[ Ref s ('Struct "PID") , SP , PV , Time ] - :-> IFloat) + ':-> IFloat) pidUpdate = proc "pid_update" $ \ pid sp pv dt -> -- These are made up requires/ensures for testing purposes. @@ -67,16 +67,32 @@ store (pid ~> pid_err) err ret err +foo :: Def ('[ Ref s ('Array 3 ('Stored Uint32)) + , Ref s ('Array 3 ('Stored Uint32)) ] ':-> ()) +foo = proc "foo" $ \a b -> +-- requires (*a!0 < *b!0) + requires (checkStored (a ! 0) + (\v -> (checkStored (b ! 0) + (\v1 -> v IFloat) +foobar :: Def ('[Uint8] ':-> Uint8) +foobar = proc "foobar" $ \x -> body $ do + ret (x `iShiftR` (3 `iDiv` 2)) + +alloc_test :: Def ('[] ':-> IFloat) alloc_test = proc "alloc_test" $ body $ do pid <- local (istruct [pid_i .= ival 1]) ret =<< deref (pid ~> pid_i) diff --git a/examples/PublicPrivate.hs b/examples/PublicPrivate.hs --- a/examples/PublicPrivate.hs +++ b/examples/PublicPrivate.hs @@ -5,42 +5,44 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverloadedStrings #-} +-- | Example of a private struct, defined as a global memory area, with a public +-- access function. + module PublicPrivate where import Ivory.Language import Ivory.Compile.C.CmdlineFrontend - [ivory| -struct Foo { i :: Stored Uint32 } -struct Bar { name :: Array 32 (Stored IChar) } +struct Foo { foo_i :: Stored Sint32 + ; foo_cnt :: Stored Uint32 + } |] -privateHelper1 :: Def ('[Ref s (Struct "Foo")] :-> Ref s (Stored Uint32)) -privateHelper1 = proc "private_helper1" (\s -> body (ret (s ~> i))) - -privateHelper2 :: Def ('[] :-> ()) -privateHelper2 = proc "private_helper2" $ body retVoid +privateFoo :: MemArea ('Struct "Foo") +privateFoo = area "private_foo" $ + Just (istruct [foo_i .= ival 0, foo_cnt .= ival 0]) -publicFunction :: Def ('[Ref s (Struct "Bar")] :-> Uint32) -publicFunction = proc "public_function" $ \_ -> body $ do - a <- call privateHelper1 (addrOf privateFoo) - call_ privateHelper2 - ret =<< deref a +privUpdate :: Def ('[Sint32] ':-> ()) +privUpdate = proc "privUpdate" $ \v -> body $ do + let foo = addrOf privateFoo + curr <- deref (foo ~> foo_cnt) + store (foo ~> foo_i) v + store (foo~> foo_cnt) (curr+1) -privateFoo :: MemArea (Struct "Foo") -privateFoo = area "private_foo" Nothing +pubUpdate :: Def ('[Sint32] ':-> ()) +pubUpdate = proc "pubUpdate" $ \v -> body $ do + call_ privUpdate v cmodule :: Module cmodule = package "PublicPrivate" $ do private $ do defStruct (Proxy :: Proxy "Foo") defMemArea privateFoo - incl privateHelper1 - incl privateHelper2 + incl privUpdate public $ do - defStruct (Proxy :: Proxy "Bar") - incl publicFunction + incl pubUpdate runPublicPrivate :: IO () -runPublicPrivate = runCompiler [cmodule] initialOpts { stdOut = True, constFold = True } +runPublicPrivate = runCompiler [cmodule] [] + initialOpts { outDir = Nothing, constFold = True } diff --git a/examples/QC.hs b/examples/QC.hs deleted file mode 100644 --- a/examples/QC.hs +++ /dev/null @@ -1,72 +0,0 @@ -{-# OPTIONS_GHC -fno-warn-orphans #-} -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE QuasiQuotes #-} -{-# LANGUAGE FlexibleInstances #-} - -module QC where - -import Ivory.Compile.C.CmdlineFrontend -import Ivory.Language -import Ivory.QuickCheck -import Test.QuickCheck.Arbitrary - -[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 arbitrary - args1 <- samples num 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 diff --git a/examples/SizeOf.hs b/examples/SizeOf.hs --- a/examples/SizeOf.hs +++ b/examples/SizeOf.hs @@ -19,8 +19,8 @@ |] -test :: Def ('[] :-> Uint8) -test = proc "test" (body (ret (sizeOf (Proxy :: Proxy (Struct "foo"))))) +test :: Def ('[] ':-> Uint8) +test = proc "sizeof_test" (body (ret (sizeOf (Proxy :: Proxy ('Struct "foo"))))) cmodule :: Module cmodule = package "SizeOf" $ do diff --git a/examples/String.hs b/examples/String.hs --- a/examples/String.hs +++ b/examples/String.hs @@ -7,22 +7,23 @@ import Ivory.Language import Ivory.Compile.C.CmdlineFrontend -printf :: Def ('[IString] :-> Sint32) +printf :: Def ('[IString] ':-> Sint32) printf = importProc "printf" "stdio.h" -printf2 :: Def ('[IString,Sint32] :-> Sint32) +printf2 :: Def ('[IString,Sint32] ':-> Sint32) printf2 = importProc "printf" "stdio.h" -test :: Def ('[] :-> ()) +test :: Def ('[] ':-> ()) test = proc "test" $ body $ do call_ printf "Hello, world\n" call_ printf2 "howdy, %i \n" 3 retVoid runString :: IO () -runString = runCompiler [cmodule] initialOpts { stdOut = True } +runString = runCompiler [cmodule] [] initialOpts { outDir = Nothing } +-- Don't collide with string.h (case-insensitive on Mac) cmodule :: Module -cmodule = package "String" $ do +cmodule = package "String_ex" $ do incl printf incl test diff --git a/examples/TestClang.hs b/examples/TestClang.hs deleted file mode 100644 --- a/examples/TestClang.hs +++ /dev/null @@ -1,60 +0,0 @@ -import System.Environment - -import qualified PID -import qualified FibLoop -import qualified Factorial -import qualified String -import qualified FunPtr -import qualified Overflow -import qualified Float -import qualified Alloc -import qualified Area -import qualified Cond -import qualified Forever -import qualified PublicPrivate -import qualified Bits -import qualified SizeOf -import qualified AddrOfRegression -import qualified Array - -import Ivory.Compile.C.CmdlineFrontend -import Ivory.Language (Module(),moduleName) -import Ivory.Stdlib (stdlibModules) - -import qualified Ivory.Stdlib.SearchDir as S - -main :: IO () -main = do - args <- getArgs - let path = head args - let opts = initialOpts { includeDir = path, srcDir = path - , rtIncludeDir = Nothing } - - mapM_ (compileExample opts) modules - - putStrLn "Compiling: Overflow" - Overflow.writeOverflow opts - -compileExample :: Opts -> Module -> IO () -compileExample opts m = do - putStrLn ("Compiling: " ++ moduleName m) - runCompilerWith Nothing (Just [S.searchDir]) [m] opts - -modules :: [Module] -modules = [ PID.cmodule - , FibLoop.cmodule - , Factorial.cmodule - , String.cmodule - , FunPtr.cmodule - , Overflow.cmodule - , Float.cmodule - , Alloc.cmodule - , Area.cmodule - , Cond.cmodule - , Forever.cmodule - , PublicPrivate.cmodule - , Bits.cmodule - , SizeOf.cmodule - , AddrOfRegression.cmodule - , Array.cmodule - ] ++ stdlibModules diff --git a/examples/TestExamples.hs b/examples/TestExamples.hs new file mode 100644 --- /dev/null +++ b/examples/TestExamples.hs @@ -0,0 +1,64 @@ +import System.Environment + +import qualified PID +import qualified FibLoop +import qualified Factorial +import qualified String +import qualified FunPtr +import qualified Overflow +import qualified Float +import qualified Alloc +import qualified Area +import qualified Cond +import qualified Forever +import qualified PublicPrivate +import qualified Bits +import qualified SizeOf +import qualified AddrOfRegression +import qualified Array +import qualified ConcreteFile +import qualified Coroutine +import qualified Loop + +import Control.Monad (when) +import Ivory.Compile.C.CmdlineFrontend +import Ivory.Stdlib.String +import Ivory.Language (Module()) +import Ivory.Stdlib (stdlibModules) + +main :: IO () +main = do + args <- getArgs + when (null args) + (error "Binary takes a path to srcs and headers as an argument") + let path = head args + let opts = initialOpts { outDir = Just path, srcLocs = True } + compileExample opts modules + +compileExample :: Opts -> [Module] -> IO () +compileExample opts ms = runCompiler ms stdlibStringArtifacts opts + +modules :: [Module] +modules = [ PID.cmodule + , FibLoop.cmodule + , Factorial.cmodule + , String.cmodule + , FunPtr.cmodule + , Overflow.cmodule + , Float.cmodule + , Alloc.cmodule + , Area.cmodule + , Cond.cmodule + , Forever.cmodule + , PublicPrivate.cmodule + , Bits.cmodule + , SizeOf.cmodule + , AddrOfRegression.cmodule + , Array.cmodule + , Overflow.cmodule + , Coroutine.cmodule + , ConcreteFile.concreteIvory + , ConcreteFile.examplesfile + , Loop.cmodule + , stdlibStringModule + ] ++ stdlibModules diff --git a/ivory-examples.cabal b/ivory-examples.cabal --- a/ivory-examples.cabal +++ b/ivory-examples.cabal @@ -1,7 +1,7 @@ name: ivory-examples -version: 0.1.0.2 +version: 0.1.0.3 author: Galois, Inc -maintainer: trevor@galois.com +maintainer: trevor@galois.com, leepike@galois.com copyright: 2013 Galois, Inc. category: Language synopsis: Ivory examples. @@ -14,29 +14,10 @@ source-repository this type: git location: https://github.com/GaloisInc/ivory - tag: hackage-examples-0102 - - -executable ivory-fibtutorial - main-is: FibTutorial.hs - hs-source-dirs: examples - build-depends: base >= 4.6, - pretty >= 1.1, - monadLib >= 3.7, - template-haskell >= 2.8, - mainland-pretty >= 0.2.4, - wl-pprint, - ivory, - ivory-opts, - ivory-backend-c, - ivory-quickcheck, - ivory-stdlib, - QuickCheck - default-language: Haskell2010 - ghc-options: -Wall + tag: hackage-examples-0103 executable ivory-c-clang-test - main-is: TestClang.hs + main-is: TestExamples.hs other-modules: PID, FibLoop, Factorial, @@ -53,19 +34,21 @@ SizeOf, AddrOfRegression, Array, - QC + BitData, + BitDataTypes, + ConcreteFile, + Coroutine, + Loop hs-source-dirs: examples - build-depends: base >= 4.6 && < 4.7, + build-depends: base >= 4.6 && < 5, + base-compat, pretty >= 1.1, monadLib >= 3.7, template-haskell >= 2.8, - mainland-pretty >= 0.2.4, - wl-pprint, ivory, ivory-opts, - ivory-quickcheck, ivory-backend-c, ivory-stdlib, QuickCheck default-language: Haskell2010 - ghc-options: -Wall + ghc-options: -Wall