ivory-hw 0.1.0.0 → 0.1.0.3
raw patch · 10 files changed
+80/−111 lines, 10 filesdep +ivory-artifactdep −ivory-bitdatadep ~base
Dependencies added: ivory-artifact
Dependencies removed: ivory-bitdata
Dependency ranges changed: base
Files
- examples/ExampleTypes.hs +3/−2
- ivory-hw.cabal +7/−20
- src/Ivory/HW.hs +5/−1
- src/Ivory/HW/BitData.hs +34/−13
- src/Ivory/HW/Machine.hs +0/−10
- src/Ivory/HW/Module.hs +10/−6
- src/Ivory/HW/Prim.hs +17/−8
- src/Ivory/HW/Reg.hs +4/−11
- src/Ivory/HW/STM32F4.hs +0/−27
- src/Ivory/HW/SearchDir.hs +0/−13
examples/ExampleTypes.hs view
@@ -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
ivory-hw.cabal view
@@ -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
src/Ivory/HW.hs view
@@ -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
src/Ivory/HW/BitData.hs view
@@ -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
− src/Ivory/HW/Machine.hs
@@ -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
src/Ivory/HW/Module.hs view
@@ -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"]
src/Ivory/HW/Prim.hs view
@@ -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
src/Ivory/HW/Reg.hs view
@@ -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
− src/Ivory/HW/STM32F4.hs
@@ -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]
− src/Ivory/HW/SearchDir.hs
@@ -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"--