Merge pull request #12 from distrap/srk/cblpsPatches

Forward port pending PRs from `GaloisInc/ivory`

ivory-backend-c/ivory-backend-c.cabal

@@ -30,15 +30,16 @@ library
   other-modules:        Paths_ivory_backend_c
 
   build-depends:        base >= 4.7 && < 5,
+                        ivory,
+                        ivory-artifact,
+                        ivory-opts,
+                        directory,
+                        filepath,
                         language-c-quote >= 0.13,
-                        srcloc,
                         mainland-pretty >= 0.6,
                         monadLib >= 3.7,
-                        directory,
-                        filepath,
-                        ivory,
-                        ivory-opts,
-                        ivory-artifact
+                        pretty >= 1.1,
+                        srcloc,
   hs-source-dirs:       src
   default-language:     Haskell2010
 

ivory-backend-c/src/Ivory/Compile/C/CmdlineFrontend.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE FlexibleContexts #-}
+
 module Ivory.Compile.C.CmdlineFrontend
   ( compile
   , compileWith
@@ -9,11 +11,9 @@ module Ivory.Compile.C.CmdlineFrontend
   , outputCompiler
   ) where
 
-import           Data.List                               (intercalate, nub,
-                                                          (\\))
-import qualified Ivory.Compile.C                         as C
 import qualified Paths_ivory_backend_c                   as P
 
+import qualified Ivory.Compile.C                         as C
 import           Ivory.Compile.C.CmdlineFrontend.Options
 
 import           Ivory.Artifact
@@ -31,11 +31,16 @@ import qualified Ivory.Opts.TypeCheck                    as T
 
 
 import           Control.Monad                           (when)
-import           Data.List                               (foldl')
+import           Data.List                               (foldl', intercalate,
+                                                          nub, (\\))
 import           Data.Maybe                              (catMaybes, mapMaybe)
+import           MonadLib                                (WriterM, put,
+                                                          runWriterT)
 import           System.Directory                        (createDirectoryIfMissing)
 import           System.Environment                      (getArgs)
 import           System.FilePath                         (addExtension, (</>))
+import           System.IO                               (hPutStrLn, stderr)
+import           Text.PrettyPrint                        (Doc, render, vcat)
 
 import qualified Data.Maybe
 
@@ -56,7 +61,8 @@ runCompiler ms as os = runCompilerWith ms as os
 -- | Main compile function.
 runCompilerWith :: [Module] -> [Located Artifact] -> Opts -> IO ()
 runCompilerWith modules artifacts opts = do
-  cmodules <- compileUnits modules opts
+  (cmodules, errors) <- runWriterT $ compileUnits modules opts
+  hPutStrLn stderr $ render $ vcat errors
   if outProcSyms opts
     then C.outputProcSyms modules
     else outputCompiler cmodules artifacts opts
@@ -106,7 +112,7 @@ outputmodules opts cmodules user_artifacts = do
   output :: FilePath -> FilePath -> (C.CompileUnits -> String)
          -> C.CompileUnits
          -> IO ()
-  output dir ext render m = outputHelper fout (render m)
+  output dir ext renderUnits m = outputHelper fout (renderUnits m)
     where fout = addExtension (dir </> (C.unitName m)) ext
 
   renderHeader cu = C.renderHdr (C.headers cu) (C.unitName cu)
@@ -123,21 +129,21 @@ outputmodules opts cmodules user_artifacts = do
     out = writeFile fname contents
 
 -- | Compile, type-check, and optimize modules, but don't generate C files.
-compileUnits ::[Module] -> Opts -> IO [C.CompileUnits]
+compileUnits :: WriterM m [Doc] => [Module] -> Opts -> m [C.CompileUnits]
 compileUnits modules opts = do
 
   when (tcErrors opts) $ do
     let ts = map T.typeCheck modules
     let anyTs = or (map T.existErrors ts)
     let b = tcWarnings opts
-    mapM_ (T.showTyChkModule b) ts
+    mapM_ (\t -> put [T.showTyChkModule b t]) ts
     when anyTs (error "Type-checking failed!")
 
   when (scErrors opts) $ do
     let ds = S.dupDefs modules
-    S.showDupDefs ds
+    put [S.showDupDefs ds]
     let ss = S.sanityCheck modules
-    mapM_ S.showSanityChkModule ss
+    mapM_ (\s -> put [S.showSanityChkModule s]) ss
     let anySs = or (map S.existErrors ss)
     when anySs (error "Sanity-check failed!")
 

ivory-examples/examples/AddrOfRegression.hs

@@ -27,7 +27,7 @@ test1 = do
   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
@@ -43,7 +43,7 @@ test1_noarray = do
   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
 
@@ -58,7 +58,7 @@ test2 = do
   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,7 +67,7 @@ test3 :: ModuleDef
 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
     arrayMap $ \ix ->

ivory-examples/examples/Alloc.hs

@@ -26,27 +26,27 @@ struct Str {
 
 |]
 
-test :: Def ('[Ref s ('Struct "Foo")] ':-> Ref s ('Stored Uint32))
+test :: Def ('[Ref s ('Struct "Foo")] :-> Ref s ('Stored Uint32))
 test  = proc "alloc_test" (\ pid -> body (ret (pid ~> i)))
 
-get_p :: Def ('[] ':-> Uint32)
+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)) ] ':-> ())
+                 , 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
@@ -70,56 +70,56 @@ bad_alloc = proc "bad_alloc" $ body $ do
   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] ':-> ())
+                   , 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 :: 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)
   2 `downTo` 0 $ (\ix -> store (arr ! (ix :: Ix 15)) 1)
   0 `upTo`   2 $ (\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)
@@ -130,12 +130,12 @@ arrayTest  = area "arrayTest" $ Just $ iarray
   ]
 
 -- 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)
 
 -- 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)
@@ -144,12 +144,12 @@ foo2 = proc "foo2" $ \str -> body $ do
 ---------------------------------------------
 
 -- Testing matrices
-mat1 :: Def ('[ConstRef s ('Array 1 ('Array 2 ('Stored Uint32)))] ':-> Uint32)
+mat1 :: Def ('[ConstRef s ('Array 1 ('Array 2 ('Stored Uint32)))] :-> Uint32)
 mat1 = proc "mat1" $ \arr -> body $ do
   v <- deref (arr ! 1 ! 0)
   ret v
 
-mat2 :: Def ('[] ':-> Uint32)
+mat2 :: Def ('[] :-> Uint32)
 mat2 = proc "mat2" $ body $ do
   arr <- local ((iarray [iarray [ival 0, ival 1]]) :: Init ('Array 1 ('Array 2 ('Stored Uint32))))
   arr2 <- local ((iarray [iarray [ival 3, ival 3]]) :: Init ('Array 1 ('Array 2 ('Stored Uint32))))

ivory-examples/examples/Area.hs

@@ -23,11 +23,11 @@ val  = area "value" (Just (istruct [field .= ival 0]))
 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

ivory-examples/examples/Array.hs

@@ -14,14 +14,14 @@ cmodule = package "Array" $ do
 runArrayExample :: IO ()
 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 :: Def('[IBool] :-> IFloat)
 arrayTernary = proc "arrayTernary" $ \b -> body $ do
   a1 <- local (vs 1)
   a2 <- local (vs 2)

ivory-examples/examples/BitData.hs

@@ -80,14 +80,14 @@ import Ivory.Language.BitData.BitData (BitType)
    }
 |]
 
-test1 :: Def ('[Uint16] ':-> Uint16)
+test1 :: Def ('[Uint16] :-> Uint16)
 test1 = proc "test1" $ \x -> body $
   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 :: Def ('[Uint32] :-> Uint8)
 test2 = proc "test2" $ \x -> body $ do
   let d = fromRep x :: NVIC_ISER
   ret $ toRep (d #. nvic_iser_setena #! 0)
@@ -109,7 +109,7 @@ forBitArray_ arr f =
     f (arr #! i)
 
 -- | Test looping over the elements of a bit array:
-test3 :: Def ('[Uint32] ':-> Uint32)
+test3 :: Def ('[Uint32] :-> Uint32)
 test3 = proc "test3" $ \x -> body $ do
   let d = fromRep x
   total <- local (ival 0)
@@ -119,7 +119,7 @@ test3 = proc "test3" $ \x -> body $ do
     store total (x' + y)
   ret =<< deref total
 
-get_baud :: Def ('[Uint16] ':-> Uint8)
+get_baud :: Def ('[Uint16] :-> Uint8)
 get_baud = proc "get_baud" $ \x -> body $ do
   let d = fromRep x
   ret (toRep (d #. spi_cr1_br))

ivory-examples/examples/Bits.hs

@@ -19,7 +19,7 @@ cmodule = package "Bits" $ do
   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
@@ -28,7 +28,7 @@ test1 = proc "test1" $ \u8 u16 u32 u64 -> body $ do
   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)
@@ -49,7 +49,7 @@ extractUint32 x = fst $ runState x $ do
   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
@@ -69,7 +69,7 @@ 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
@@ -79,10 +79,10 @@ test4 = proc "test4" $ body $ do
   clearBit n 3
   ret =<< deref n
 
-test5 :: Def ('[Sint8] ':-> Uint8)
+test5 :: Def ('[Sint8] :-> Uint8)
 test5 = proc "test5" $ \s -> body $
   ret (twosComplementRep s)
 
-test6 :: Def ('[Uint8] ':-> Sint8)
+test6 :: Def ('[Uint8] :-> Sint8)
 test6 = proc "test6" $ \s -> body $
   ret (twosComplementCast s)