diff --git a/examples/ExampleTypes.hs b/examples/ExampleTypes.hs --- a/examples/ExampleTypes.hs +++ b/examples/ExampleTypes.hs @@ -1,13 +1,14 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} module ExampleTypes where -import Ivory.BitData +import Ivory.Language -[bitdata| +[ivory| bitdata SPIBaud :: Bits 3 = spi_baud_div_2 as 0 | spi_baud_div_4 as 1 diff --git a/ivory-hw.cabal b/ivory-hw.cabal --- a/ivory-hw.cabal +++ b/ivory-hw.cabal @@ -2,15 +2,15 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: ivory-hw -version: 0.1.0.0 +version: 0.1.0.3 license: BSD3 license-file: LICENSE author: Galois, Inc. -maintainer: jamesjb@galois.com +maintainer: jamesjb@galois.com, leepike@galois.com copyright: 2013 Galois, Inc. synopsis: Ivory hardware model (STM32F4). description: Hardware model for Ivory. Currently, the STM32F4 is supported; others may be added. -homepage: http://smaccmpilot.org/languages/ivory-introduction.html +homepage: http://ivorylang.org build-type: Simple cabal-version: >= 1.10 category: Language @@ -20,38 +20,25 @@ source-repository this type: git location: https://github.com/GaloisInc/ivory - tag: hackage-hw-0100 + tag: hackage-hw-0103 library exposed-modules: Ivory.HW, Ivory.HW.Reg, Ivory.HW.BitData, - Ivory.HW.Module, - Ivory.HW.SearchDir + Ivory.HW.Module other-modules: Ivory.HW.IOArea, - Ivory.HW.STM32F4, - Ivory.HW.Machine, Ivory.HW.Prim, Paths_ivory_hw, ExampleTypes hs-source-dirs: src, examples - build-depends: base ==4.6.*, + build-depends: base >= 4.6 && < 5, filepath, ivory, - ivory-bitdata, + ivory-artifact, ivory-backend-c default-language: Haskell2010 ghc-options: -Wall - --- executable ivory-hw-example --- main-is: Example.hs --- other-modules: ExampleTypes --- hs-source-dirs: examples --- build-depends: base >= 4.6, --- ivory, --- ivory-backend-c, --- ivory-bitdata, --- ivory-hw diff --git a/src/Ivory/HW.hs b/src/Ivory/HW.hs --- a/src/Ivory/HW.hs +++ b/src/Ivory/HW.hs @@ -10,9 +10,13 @@ Reg(), IvoryIOReg(), mkReg, readReg, writeReg -- * Bit Data I/O registers - , BitDataReg(), mkBitDataReg, getReg, setReg, modifyReg + , BitDataReg(), mkBitDataReg, mkBitDataRegNamed + , getReg, setReg, modifyReg + -- * Dependency Capture + , hw_moduledef, hw_artifacts ) where import Ivory.HW.Reg import Ivory.HW.BitData import Ivory.HW.Prim +import Ivory.HW.Module diff --git a/src/Ivory/HW/BitData.hs b/src/Ivory/HW/BitData.hs --- a/src/Ivory/HW/BitData.hs +++ b/src/Ivory/HW/BitData.hs @@ -8,39 +8,60 @@ module Ivory.HW.BitData where -import Ivory.BitData -import Ivory.Language +import Numeric (showHex) +import Data.List (intercalate) +import Ivory.Language import Ivory.HW.Prim import Ivory.HW.Reg -- | A register associated with a bit data type. -newtype BitDataReg d = BitDataReg (Reg (BitDataRep d)) +data BitDataReg d = + BitDataReg + { bdr_reg :: Reg (BitDataRep d) + , bdr_name :: Maybe String + } +bdrComment :: BitDataReg d -> String -> String -> Ivory eff () +bdrComment r c c' = + comment ("reg " ++ c ++ " " ++ regname ++ ": " ++ c' ) + where + regname = case bdr_name r of + Just n -> n + Nothing -> "0x" ++ (showHex regaddr "") + regaddr = case bdr_reg r of Reg a -> a + -- | Create a bit data register given its address. mkBitDataReg :: IvoryIOReg (BitDataRep d) => Integer -> BitDataReg d -mkBitDataReg = BitDataReg . mkReg +mkBitDataReg a = BitDataReg { bdr_reg = mkReg a, bdr_name = Nothing } +-- | Create a bit data register given its address and name. +mkBitDataRegNamed :: IvoryIOReg (BitDataRep d) => Integer -> String -> BitDataReg d +mkBitDataRegNamed a n = BitDataReg { bdr_reg = mkReg a, bdr_name = Just n } + getReg :: (BitData d, IvoryIOReg (BitDataRep d)) => BitDataReg d -> Ivory eff d -getReg (BitDataReg r) = do - val <- readReg r +getReg r = do + bdrComment r "get" "" + val <- readReg (bdr_reg r) return $ fromRep val -- | Set a register to a value taken from a block of bit -- modifications. The previous value is discarded. setReg :: (BitData d, IvoryIOReg (BitDataRep d)) => BitDataReg d -> BitDataM d a -> Ivory eff a -setReg (BitDataReg r) mf = do - let (result, val) = runBits 0 mf - writeReg r val +setReg r mf = do + let (result, val, ss) = runBits 0 mf + bdrComment r "set" (intercalate ", " ss) + writeReg (bdr_reg r) val return result -- | Modify a register by a set of bit modification actions. modifyReg :: (BitData d, IvoryIOReg (BitDataRep d)) => BitDataReg d -> BitDataM d a -> Ivory eff a -modifyReg (BitDataReg r) mf = do - val <- readReg r - let (result, val') = runBits val mf - writeReg r val' +modifyReg r mf = do + val <- readReg (bdr_reg r) + let (result, val', ss) = runBits val mf + bdrComment r "modify" (intercalate ", " ss) + writeReg (bdr_reg r) val' return result diff --git a/src/Ivory/HW/Machine.hs b/src/Ivory/HW/Machine.hs deleted file mode 100644 --- a/src/Ivory/HW/Machine.hs +++ /dev/null @@ -1,10 +0,0 @@ --- --- Machine.hs --- Imports the current machine module. --- --- Copyright (C) 2013, Galois, Inc. --- All Rights Reserved. --- - -module Ivory.HW.Machine (ioAreas) where - -import Ivory.HW.STM32F4 diff --git a/src/Ivory/HW/Module.hs b/src/Ivory/HW/Module.hs --- a/src/Ivory/HW/Module.hs +++ b/src/Ivory/HW/Module.hs @@ -5,11 +5,15 @@ -- All Rights Reserved. -- -module Ivory.HW.Module where +module Ivory.HW.Module ( + hw_moduledef, + hw_artifacts +) where -import Ivory.Language +import Ivory.HW.Prim +import Ivory.Artifact +import qualified Paths_ivory_hw -hw_moduledef :: ModuleDef -hw_moduledef = do - inclHeader "ivory_hw_prim.h" - sourceDep "ivory_hw_prim.h" +hw_artifacts :: [Located Artifact] +hw_artifacts = + [Incl $ artifactCabalFile Paths_ivory_hw.getDataDir "support/ivory_hw_prim.h"] diff --git a/src/Ivory/HW/Prim.hs b/src/Ivory/HW/Prim.hs --- a/src/Ivory/HW/Prim.hs +++ b/src/Ivory/HW/Prim.hs @@ -11,15 +11,24 @@ import Ivory.Language +hw_moduledef :: ModuleDef +hw_moduledef = do + incl ioRegReadU8 + incl ioRegWriteU8 + incl ioRegReadU16 + incl ioRegWriteU16 + incl ioRegReadU32 + incl ioRegWriteU32 + class IvoryBits a => IvoryIOReg a where ioRegSize :: a -> Integer - ioRegRead :: Def ('[Uint32] :-> a) - ioRegWrite :: Def ('[Uint32, a] :-> ()) + ioRegRead :: Def ('[Uint32] ':-> a) + ioRegWrite :: Def ('[Uint32, a] ':-> ()) -ioRegReadU8 :: Def ('[Uint32] :-> Uint8) +ioRegReadU8 :: Def ('[Uint32] ':-> Uint8) ioRegReadU8 = importProc "ivory_hw_io_read_u8" "ivory_hw_prim.h" -ioRegWriteU8 :: Def ('[Uint32, Uint8] :-> ()) +ioRegWriteU8 :: Def ('[Uint32, Uint8] ':-> ()) ioRegWriteU8 = importProc "ivory_hw_io_write_u8" "ivory_hw_prim.h" instance IvoryIOReg Uint8 where @@ -27,10 +36,10 @@ ioRegRead = ioRegReadU8 ioRegWrite = ioRegWriteU8 -ioRegReadU16 :: Def ('[Uint32] :-> Uint16) +ioRegReadU16 :: Def ('[Uint32] ':-> Uint16) ioRegReadU16 = importProc "ivory_hw_io_read_u16" "ivory_hw_prim.h" -ioRegWriteU16 :: Def ('[Uint32, Uint16] :-> ()) +ioRegWriteU16 :: Def ('[Uint32, Uint16] ':-> ()) ioRegWriteU16 = importProc "ivory_hw_io_write_u16" "ivory_hw_prim.h" instance IvoryIOReg Uint16 where @@ -38,10 +47,10 @@ ioRegRead = ioRegReadU16 ioRegWrite = ioRegWriteU16 -ioRegReadU32 :: Def ('[Uint32] :-> Uint32) +ioRegReadU32 :: Def ('[Uint32] ':-> Uint32) ioRegReadU32 = importProc "ivory_hw_io_read_u32" "ivory_hw_prim.h" -ioRegWriteU32 :: Def ('[Uint32, Uint32] :-> ()) +ioRegWriteU32 :: Def ('[Uint32, Uint32] ':-> ()) ioRegWriteU32 = importProc "ivory_hw_io_write_u32" "ivory_hw_prim.h" instance IvoryIOReg Uint32 where diff --git a/src/Ivory/HW/Reg.hs b/src/Ivory/HW/Reg.hs --- a/src/Ivory/HW/Reg.hs +++ b/src/Ivory/HW/Reg.hs @@ -8,25 +8,18 @@ module Ivory.HW.Reg where -import Numeric (showHex) import Ivory.Language - -import Ivory.HW.IOArea import Ivory.HW.Prim -import Ivory.HW.Machine -- | An I/O register containing a value of type "t". Define registers -- using the "mkReg" functions. data Reg t = Reg Integer --- | Smart constructor that ensures a register address is in bounds --- when created. This raises an error if the address is invalid. +-- | Previously, this was a smart constructor to raise an error if the address +-- is invalid, but we didn't find a way to parameterize the valid address +-- space by the platform, so now mkReg accepts all addresses. mkReg :: forall t. IvoryIOReg t => Integer -> Reg t -mkReg addr = - if (any (addrInBounds addr (ioRegSize (undefined :: t))) ioAreas) - then Reg addr - else error $ "I/O register out of bounds at address 0x" ++ - (showHex addr "") +mkReg addr = Reg addr -- | Read an I/O register, returning an Ivory value. readReg :: IvoryIOReg a => Reg a -> Ivory eff a diff --git a/src/Ivory/HW/STM32F4.hs b/src/Ivory/HW/STM32F4.hs deleted file mode 100644 --- a/src/Ivory/HW/STM32F4.hs +++ /dev/null @@ -1,27 +0,0 @@ --- --- STM32F4.hs --- Machine definition for the STM32F4. --- --- Copyright (C) 2013, Galois, Inc. --- All Rights Reserved. --- - -module Ivory.HW.STM32F4 where - -import Ivory.HW.IOArea - --- STM32F4 I/O memory areas. -ioAPB1, ioAPB2 :: IOArea -ioAPB1 = IOArea 0x40000000 0x40008000 -ioAPB2 = IOArea 0x40010000 0x40015800 - -ioAHB1, ioAHB2, ioAHB3 :: IOArea -ioAHB1 = IOArea 0x40020000 0x40080000 -ioAHB2 = IOArea 0x50000000 0x50060C00 -ioAHB3 = IOArea 0x60000000 0xA0001000 - -ioCM4 :: IOArea -ioCM4 = IOArea 0xE0000000 0xE0100000 - --- | All I/O memory areas for this machine. -ioAreas :: [IOArea] -ioAreas = [ioAPB1, ioAPB2, ioAHB1, ioAHB2, ioAHB3, ioCM4] diff --git a/src/Ivory/HW/SearchDir.hs b/src/Ivory/HW/SearchDir.hs deleted file mode 100644 --- a/src/Ivory/HW/SearchDir.hs +++ /dev/null @@ -1,13 +0,0 @@ - -module Ivory.HW.SearchDir where - -import System.FilePath - -import qualified Paths_ivory_hw - -searchDir :: IO FilePath -searchDir = do - base <- Paths_ivory_hw.getDataDir - return $ base "support" - -