ivory-hw (empty) → 0.1.0.0

raw patch · 14 files changed

+397/−0 lines, 14 filesdep +basedep +filepathdep +ivorysetup-changed

Dependencies added: base, filepath, ivory, ivory-backend-c, ivory-bitdata

Files

• LICENSE +30/−0
• Setup.hs +2/−0
• examples/ExampleTypes.hs +20/−0
• ivory-hw.cabal +57/−0
• src/Ivory/HW.hs +18/−0
• src/Ivory/HW/BitData.hs +46/−0
• src/Ivory/HW/IOArea.hs +20/−0
• src/Ivory/HW/Machine.hs +10/−0
• src/Ivory/HW/Module.hs +15/−0
• src/Ivory/HW/Prim.hs +50/−0
• src/Ivory/HW/Reg.hs +37/−0
• src/Ivory/HW/STM32F4.hs +27/−0
• src/Ivory/HW/SearchDir.hs +13/−0
• support/ivory_hw_prim.h +52/−0

@@ -0,0 +1,30 @@+Copyright (c) 2013, Galois, Inc.++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Galois, Inc. nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

@@ -0,0 +1,20 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE QuasiQuotes #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++module ExampleTypes where++import Ivory.BitData++[bitdata|+ 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+|]

@@ -0,0 +1,57 @@+-- Initial ivory-hw.cabal generated by cabal init.  For further+-- documentation, see http://haskell.org/cabal/users-guide/++name:                ivory-hw+version:             0.1.0.0+license:             BSD3+license-file:        LICENSE+author:              Galois, Inc.+maintainer:          jamesjb@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+build-type:          Simple+cabal-version:       >= 1.10+category:            Language+build-type:          Simple+cabal-version:       >=1.10+data-files: support/ivory_hw_prim.h+source-repository    this+  type:     git+  location: https://github.com/GaloisInc/ivory+  tag:      hackage-hw-0100+++library+  exposed-modules:     Ivory.HW,+                       Ivory.HW.Reg,+                       Ivory.HW.BitData,+                       Ivory.HW.Module,+                       Ivory.HW.SearchDir+  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.*,+                       filepath,+                       ivory,+                       ivory-bitdata,+                       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+

@@ -0,0 +1,18 @@+--+-- HW.hs --- I/O register access from Ivory.+--+-- Copyright (C) 2013, Galois, Inc.+-- All Rights Reserved.+--++module Ivory.HW (+  -- * I/O Registers+  Reg(), IvoryIOReg(), mkReg, readReg, writeReg++  -- * Bit Data I/O registers+  , BitDataReg(), mkBitDataReg, getReg, setReg, modifyReg+) where++import Ivory.HW.Reg+import Ivory.HW.BitData+import Ivory.HW.Prim

@@ -0,0 +1,46 @@+{-# LANGUAGE FlexibleContexts #-}+--+-- BitData.hs --- Linking registers to bitdata.+--+-- Copyright (C) 2013, Galois, Inc.+-- All Rights Reserved.+--++module Ivory.HW.BitData where++import Ivory.BitData+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))++-- | Create a bit data register given its address.+mkBitDataReg :: IvoryIOReg (BitDataRep d) => Integer -> BitDataReg d+mkBitDataReg = BitDataReg . mkReg++getReg :: (BitData d, IvoryIOReg (BitDataRep d))+       => BitDataReg d -> Ivory eff d+getReg (BitDataReg r) = do+  val <- readReg 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+  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'+  return result

@@ -0,0 +1,20 @@+--+-- IOArea.hs --- Memory area type definition.+--+-- Copyright (C) 2013, Galois, Inc.+-- All Rights Reserved.+--++module Ivory.HW.IOArea where++-- | A region of the I/O address space.+data IOArea = IOArea+  { ioAreaStart :: Integer+  , ioAreaEnd   :: Integer+  } deriving Show++-- | "addrInBounds addr size area" returns True if the address range+-- "[addr, addr + size)" lies within the bounds of "area".+addrInBounds :: Integer -> Integer -> IOArea -> Bool+addrInBounds addr size (IOArea start end) =+  (size >= 0) && (addr >= start) && (addr + size <= end)

@@ -0,0 +1,10 @@+--+-- 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

@@ -0,0 +1,15 @@+--+-- Module.hs --- Ivory module for 'ivory-hw'.+--+-- Copyright (C) 2013, Galois, Inc.+-- All Rights Reserved.+--++module Ivory.HW.Module where++import Ivory.Language++hw_moduledef :: ModuleDef+hw_moduledef = do+  inclHeader "ivory_hw_prim.h"+  sourceDep  "ivory_hw_prim.h"

@@ -0,0 +1,50 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeOperators #-}+--+-- Prim.hs --- I/O register primitives.+--+-- Copyright (C) 2013, Galois, Inc.+-- All Rights Reserved.+--++module Ivory.HW.Prim where++import Ivory.Language++class IvoryBits a => IvoryIOReg a where+  ioRegSize  :: a -> Integer+  ioRegRead  :: Def ('[Uint32] :-> a)+  ioRegWrite :: Def ('[Uint32, a] :-> ())++ioRegReadU8 :: Def ('[Uint32] :-> Uint8)+ioRegReadU8 = importProc "ivory_hw_io_read_u8" "ivory_hw_prim.h"++ioRegWriteU8 :: Def ('[Uint32, Uint8] :-> ())+ioRegWriteU8 = importProc "ivory_hw_io_write_u8" "ivory_hw_prim.h"++instance IvoryIOReg Uint8 where+  ioRegSize _  = 1+  ioRegRead  = ioRegReadU8+  ioRegWrite = ioRegWriteU8++ioRegReadU16 :: Def ('[Uint32] :-> Uint16)+ioRegReadU16 = importProc "ivory_hw_io_read_u16" "ivory_hw_prim.h"++ioRegWriteU16 :: Def ('[Uint32, Uint16] :-> ())+ioRegWriteU16 = importProc "ivory_hw_io_write_u16" "ivory_hw_prim.h"++instance IvoryIOReg Uint16 where+  ioRegSize _  = 2+  ioRegRead  = ioRegReadU16+  ioRegWrite = ioRegWriteU16++ioRegReadU32 :: Def ('[Uint32] :-> Uint32)+ioRegReadU32 = importProc "ivory_hw_io_read_u32" "ivory_hw_prim.h"++ioRegWriteU32 :: Def ('[Uint32, Uint32] :-> ())+ioRegWriteU32 = importProc "ivory_hw_io_write_u32" "ivory_hw_prim.h"++instance IvoryIOReg Uint32 where+  ioRegSize _  = 4+  ioRegRead  = ioRegReadU32+  ioRegWrite = ioRegWriteU32

@@ -0,0 +1,37 @@+{-# LANGUAGE ScopedTypeVariables #-}+--+-- Reg.hs --- I/O register access from Ivory.+--+-- Copyright (C) 2013, Galois, Inc.+-- All Rights Reserved.+--++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.+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 "")++-- | Read an I/O register, returning an Ivory value.+readReg :: IvoryIOReg a => Reg a -> Ivory eff a+readReg (Reg addr) = call ioRegRead (fromIntegral addr)++-- | Write an I/O register from an Ivory value.+writeReg :: IvoryIOReg a => Reg a -> a -> Ivory eff ()+writeReg (Reg addr) val = call_ ioRegWrite (fromIntegral addr) val

@@ -0,0 +1,27 @@+--+-- 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]

@@ -0,0 +1,13 @@++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"++

@@ -0,0 +1,52 @@+/* -*- Mode: C; indent-tabs-mode: nil; c-basic-offset: 4 -*- */+/*+ * ivory_hw_prim.h --- Ivory HW primitives for I/O register access.+ *+ * Copyright (C) 2013, Galois, Inc.+ * All Rights Reserved.+ */++#ifndef __SMACCMPILOT_IVORY_HW_PRIM_H__+#define __SMACCMPILOT_IVORY_HW_PRIM_H__++#include <stdint.h>++#ifdef __cplusplus+extern "C" {+#endif++static inline uint8_t ivory_hw_io_read_u8(uint32_t addr)+{+    return *((volatile uint8_t *)addr);+}++static inline void ivory_hw_io_write_u8(uint32_t addr, uint8_t value)+{+    *((volatile uint8_t *)addr) = value;+}++static inline uint16_t ivory_hw_io_read_u16(uint32_t addr)+{+    return *((volatile uint16_t *)addr);+}++static inline void ivory_hw_io_write_u16(uint32_t addr, uint16_t value)+{+    *((volatile uint16_t *)addr) = value;+}++static inline uint32_t ivory_hw_io_read_u32(uint32_t addr)+{+    return *((volatile uint32_t *)addr);+}++static inline void ivory_hw_io_write_u32(uint32_t addr, uint32_t value)+{+    *((volatile uint32_t *)addr) = value;+}++#ifdef __cplusplus+}+#endif++#endif  /* !defined __SMACCMPILOT_IVORY_HW_PRIM_H__ */