copilot-c99 0.2.1 → 0.2.2

raw patch · 9 files changed

+243/−155 lines, 9 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +1/−1
• copilot-c99.cabal +1/−1
• src/Copilot/Compile/C99.hs +28/−8
• src/Copilot/Compile/C99/C2A.hs +48/−75
• src/Copilot/Compile/C99/MetaTable.hs +10/−4
• src/Copilot/Compile/C99/PrePostCode.hs +8/−10
• src/Copilot/Compile/C99/Test/CheckSpec.hs +76/−27
• src/Copilot/Compile/C99/Test/Driver.hs +65/−23
• test/CopilotC99Test.hs +6/−6

@@ -32,7 +32,7 @@ Dependencies ============= copilot-c99 depends on the-[Atom](http://hackage.haskell.org/package/copilot-cbmc) to generate hard+[Atom](http://hackage.haskell.org/package/copilot-atom) to generate hard real-time C code.  Resources

@@ -1,6 +1,6 @@ cabal-version             : >= 1.10 name                      : copilot-c99-version                   : 0.2.1+version                   : 0.2.2 synopsis                  : A compiler for Copilot targeting C99. description               : This is a back-end from Copilot to the Atom DSL. Please see README.mk for more details. license                   : BSD3

@@ -2,39 +2,59 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- |+-- | Compile through the Atom backend.  module Copilot.Compile.C99   ( compile+  , c99DirName+  , c99FileRoot   , module Copilot.Compile.C99.Params   ) where +import qualified Copilot.Core as Core import Copilot.Compile.Header.C99 (genC99Header) import Copilot.Compile.C99.MetaTable (allocMetaTable) import Copilot.Compile.C99.Params import Copilot.Compile.C99.Phases (schedulePhases) import Copilot.Compile.C99.PrePostCode (preCode, postCode)-import qualified Copilot.Core as Core++ import Language.Atom (Atom) import qualified Language.Atom as Atom+ import Control.Monad (when)+import System.Directory (createDirectory, renameFile, removeFile)  -------------------------------------------------------------------------------- +c99DirName :: String+c99DirName = "copilot-c99"++c99FileRoot :: String+c99FileRoot = "copilot"++--------------------------------------------------------------------------------+ compile :: Params -> Core.Spec -> IO ()-compile params spec0 =-  do-    (schedule, _, _, _, _) <- Atom.compile programName atomDefaults atomProgram-    when (verbose params) $ putStrLn (Atom.reportSchedule schedule)-    genC99Header (prefix params) "." spec+compile params spec0 = do+  createDirectory dirName+  (schedule, _, _, _, _) <- Atom.compile programName atomDefaults atomProgram+  when (verbose params) $ putStrLn (Atom.reportSchedule schedule)+  genC99Header (prefix params) dirName spec+  mv ".c" -- the C file Atom generates+  removeFile (programName ++ ".h")  -- We don't want Atom's .h file, but our own    where+  mv ext = renameFile p (dirName ++ "/" ++ p)+    where p = programName ++ ext +  dirName = withPrefix (prefix params) c99DirName+   spec :: Core.Spec   spec = Core.makeTags spec0    programName :: String-  programName = withPrefix (prefix params) "copilot"+  programName = withPrefix (prefix params) c99FileRoot    atomDefaults :: Atom.Config   atomDefaults =

@@ -13,6 +13,7 @@ import qualified Copilot.Compile.C99.Witness as W import Copilot.Compile.C99.MetaTable import Copilot.Core (Op1 (..), Op2 (..), Op3 (..))+import Copilot.Core.Error (impossible) import qualified Copilot.Core as C import Copilot.Core.Type.Equality ((=~=), coerce, cong) import Data.Map (Map)@@ -53,147 +54,119 @@    ---------------------------------------------------- -  C.Const _ x ->--    A.Const x+  C.Const _ x -> A.Const x    ----------------------------------------------------    C.Drop t i id ->--    let-      Just strmInfo = M.lookup id (streamInfoMap meta)-    in-      drop1 t strmInfo+    let Just strmInfo = M.lookup id (streamInfoMap meta) in+    drop1 t strmInfo      where-     drop1 :: C.Type a -> StreamInfo -> A.E a     drop1 t1       StreamInfo         { streamInfoQueue = que         , streamInfoType  = t2         } =-      let-        Just p = t2 =~= t1-      in-        case W.exprInst t2 of-          W.ExprInst ->-            coerce (cong p) (Q.lookahead (fromIntegral i) que)+      let Just p = t2 =~= t1 in+      case W.exprInst t2 of+        W.ExprInst ->+          coerce (cong p) (Q.lookahead (fromIntegral i) que)    ----------------------------------------------------    C.Local t1 _ name e1 e2 ->--    let-      e1'  = c2aExpr_ e1 env meta-      env' = M.insert name (Local e1' t1) env-    in-      c2aExpr_ e2 env' meta+    let e1'  = c2aExpr_ e1 env meta in+    let env' = M.insert name (Local e1' t1) env in+    c2aExpr_ e2 env' meta    ----------------------------------------------------    C.Var t1 name ->--    let-      Just local = M.lookup name env-    in-      case local of-        Local-          { localAtomExpr = e-          , localType     = t2-          } ->-            let-              Just p = t2 =~= t1-            in-              case W.exprInst t2 of-                W.ExprInst ->-                  coerce (cong p) e+    let Just local = M.lookup name env in+    case local of+      Local+        { localAtomExpr = e+        , localType     = t2+        } ->+          let Just p = t2 =~= t1 in+          case W.exprInst t2 of+            W.ExprInst ->+              coerce (cong p) e    ---------------------------------------------------- -  C.ExternVar t name ->--    let-      Just externInfo = M.lookup name (externInfoMap meta)-    in-      externVar1 t externInfo+  C.ExternVar t name _ ->+    let Just externInfo = M.lookup name (externInfoMap meta) in+    externVar1 t externInfo      where-     externVar1 :: C.Type a -> ExternInfo -> A.E a     externVar1 t1       ExternInfo         { externInfoVar  = v         , externInfoType = t2         } =-      let-        Just p = t2 =~= t1-      in-        coerce (cong p) (A.value v)+      let Just p = t2 =~= t1 in+      coerce (cong p) (A.value v)    ---------------------------------------------------- -  C.ExternFun t name _ (Just tag) ->--    let-      Just extFunInfo = M.lookup (name, tag) (externFunInfoMap meta)+  C.ExternFun t name _ _ maybeTag ->+    let tag = case maybeTag of+                Nothing  -> impossible "c2aExpr_ /ExternFun" "copilot-c99"+                Just tg  -> tg     in-      externFun1 t extFunInfo+    let Just extFunInfo = M.lookup (name, tag) (externFunInfoMap meta) in+    externFun1 t extFunInfo      where-     externFun1 t1       ExternFunInfo         { externFunInfoVar  = var         , externFunInfoType = t2         } =-      let-        Just p = t2 =~= t1-      in-        case W.exprInst t2 of-          W.ExprInst ->-            coerce (cong p) (A.value var)+      let Just p = t2 =~= t1 in+      case W.exprInst t2 of+        W.ExprInst ->+          coerce (cong p) (A.value var)    ---------------------------------------------------- -  C.ExternArray _ t name _ (Just tag) ->--    let-      Just extArrayInfo = M.lookup (name, tag) (externArrayInfoMap meta)+  C.ExternArray _ t name _ _ _ maybeTag -> +    let tag = case maybeTag of+                Nothing  -> impossible "c2aExpr_ /ExternArray" "copilot-c99"+                Just tg  -> tg     in-      externArray1 t extArrayInfo+    let Just extArrayInfo = M.lookup (name, tag) (externArrayInfoMap meta) in+    externArray1 t extArrayInfo      where-     externArray1 t1       ExternArrayInfo         { externArrayInfoVar      = var         , externArrayInfoElemType = t2         } =-      let-        Just p = t2 =~= t1-      in-        case W.exprInst t2 of-          W.ExprInst ->-            coerce (cong p) (A.value var)+      let Just p = t2 =~= t1 in+      case W.exprInst t2 of+        W.ExprInst ->+          coerce (cong p) (A.value var)    ---------------------------------------------------- -  C.Op1 op e ->+  C.Op1 op e -> c2aOp1 op (c2aExpr_ e env meta) -    c2aOp1 op (c2aExpr_ e env meta)+        ----------------------------------------------------    C.Op2 op e1 e2 ->-     c2aOp2 op (c2aExpr_ e1 env meta) (c2aExpr_ e2 env meta)    ----------------------------------------------------    C.Op3 op e1 e2 e3 ->-     c2aOp3 op (c2aExpr_ e1 env meta) (c2aExpr_ e2 env meta)       (c2aExpr_ e3 env meta) 

@@ -20,6 +20,8 @@ import qualified Copilot.Compile.C99.Queue as Q import qualified Copilot.Compile.C99.Witness as W import qualified Copilot.Core as C+import Copilot.Core.Error (impossible)+ import Copilot.Core.External import Data.Map (Map) import qualified Data.Map as M@@ -130,8 +132,10 @@ --------------------------------------------------------------------------------  allocExternArray :: ExtArray -> Atom ((C.Name, C.Tag), ExternArrayInfo)-allocExternArray (ExtArray name elemType idxExpr idxType (Just tag)) =-  do+allocExternArray (ExtArray name elemType idxExpr idxType _ maybeTag) = do+    let tag = case maybeTag of+                Nothing  -> impossible "allocExternArray" "copilot-c99"+                Just tg  -> tg     W.ExprInst <- return (W.exprInst elemType)     v <- A.var (mkExternArrayName name tag) (C.uninitialized elemType)     return ((name, tag), ExternArrayInfo v idxExpr idxType elemType)@@ -139,8 +143,10 @@ --------------------------------------------------------------------------------  allocExternFun :: ExtFun -> Atom ((C.Name, C.Tag), ExternFunInfo)-allocExternFun (ExtFun name t args (Just tag)) =-  do+allocExternFun (ExtFun name t args maybeTag) = do+    let tag = case maybeTag of+                Nothing  -> impossible "allocExternFun" "copilot-c99"+                Just tg  -> tg     W.ExprInst <- return (W.exprInst t)     v <- A.var (mkExternFunName name tag) (C.uninitialized t)     return ((name, tag), ExternFunInfo args v t)

@@ -26,10 +26,7 @@  observerDecl :: Params -> Observer -> String observerDecl params (Observer cs _ t) = typeSpec t ++ " " ++ name ++ ";"--  where--    name = withPrefix (prefix params) cs+  where name = withPrefix (prefix params) cs  -------------------------------------------------------------------------------- @@ -37,9 +34,11 @@ tmpExtFunVar _ ExtFun   { externFunName = name   , externFunType = t---  , externFunArgs = args-  , externFunTag  = Just tag } =-    "static " ++ typeSpec t ++ " " ++ mkTmpExtFunVarName name tag ++ ";"+  , externFunTag  = mtag } =+    case mtag of+      Nothing  -> impossible "tmpExtFunVar" "copilot-c99"+      Just tag -> "static " ++ typeSpec t ++ " " +                    ++ mkTmpExtFunVarName name tag ++ ";"  -------------------------------------------------------------------------------- @@ -52,6 +51,5 @@     , "}"     ] -  where--  step = withPrefix (prefix params) "copilot" ++ "();"+  where step = withPrefix (prefix params) "copilot" ++ "();"+  

@@ -2,35 +2,42 @@ -- Copyright © 2011 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- +{-# LANGUAGE ExistentialQuantification #-}+ module Copilot.Compile.C99.Test.CheckSpec (checkSpec) where -import Copilot.Core ( Spec (..))-import Copilot.Core.Interpret.Eval (eval, ExtEnv(..))-import Copilot.Compile.C99 (compile)+import Copilot.Core ( Spec (..), Trigger(..))+import Copilot.Core.Expr (Name, UExpr (..))+import Copilot.Core.Type.Eq (UVal (..))+import Copilot.Core.Interpret.Eval (eval)+import Copilot.Compile.C99 (compile, c99DirName, c99FileRoot) import Copilot.Compile.C99.Params (Params (..), defaultParams) import Copilot.Compile.C99.Test.Driver (driver) import Copilot.Compile.C99.Test.Iteration (Iteration(..), execTraceToIterations) import Copilot.Compile.C99.Test.ReadCSV (iterationsFromCSV) import Copilot.Core.Type.Show (ShowType(..))+import Copilot.Core.Type.Read (readWithType)  import Data.ByteString (ByteString)+import qualified Data.Map as M+import Data.List (foldl') import qualified Data.ByteString.Char8 as B import qualified Data.Text.IO as TIO-import System.Directory (removeFile)+import System.Directory (removeDirectoryRecursive) import System.Process (system, readProcess) import Control.Monad (when, unless) import Text.PrettyPrint (text, (<+>), ($$), render, vcat, hang)  -------------------------------------------------------------------------------- -checkSpec :: Int -> ExtEnv -> Spec -> IO Bool-checkSpec numIterations env spec = do-  genCFiles numIterations env spec+checkSpec :: Int -> Spec -> IO Bool+checkSpec numIterations spec = do+  genCFiles numIterations spec   compileCFiles   csv <- execute numIterations-  let is1 = iterationsFromCSV csv     -  let is2 = interp numIterations env spec-  let eq = is1 == is2+  let is1 = iterationsFromCSV csv+  let is2 = interp numIterations spec+  let eq = typedOutputs spec is1 == typedOutputs spec is2   unless eq (putStrLn $ showCompare is1 is2)   when eq cleanUp -- Keep things around if there's a failure   return eq@@ -47,40 +54,82 @@  -------------------------------------------------------------------------------- -genCFiles :: Int -> ExtEnv -> Spec -> IO ()-genCFiles numIterations env spec = do+-- mapping triggers to arg values+type TypedIteration = M.Map Name [UVal]++-- list of output values for comparison+typedOutputs :: Spec -> [Iteration] -> [TypedIteration]+typedOutputs Spec { specTriggers = triggers } = +  map recoverTypes++  where+  recoverTypes :: Iteration -> TypedIteration+  recoverTypes Iteration { iterationOutputs = iterMap } = +    M.mapWithKey recoverType iterMap++  recoverType :: Name -> [String] -> [UVal]+  recoverType trigName outs = +    let types = typedTriggerArgs M.! trigName in+    map typedRead (zip types outs)++  typedRead :: (UExpr, String) -> UVal+  typedRead (UExpr { uExprType = t }, output) = +    UVal { uType = t+         , uVal = readWithType t output }++  typedTriggerArgs :: M.Map Name [UExpr]+  typedTriggerArgs = +    foldl' mkMap M.empty triggers+    where +    mkMap mp trig = M.insert (triggerName trig) (triggerArgs trig) mp++--------------------------------------------------------------------------------++driverFile :: String+driverFile = "driver.c"++outputFile :: String+outputFile = "_test"++--------------------------------------------------------------------------------++genCFiles :: Int -> Spec -> IO ()+genCFiles numIterations spec = do   compile (defaultParams { prefix = Nothing, verbose = False }) spec-  TIO.writeFile "driver.c" (driver numIterations env spec)-  return ()+  TIO.writeFile (c99DirName ++ "/" ++ driverFile) +                (driver numIterations spec)  --------------------------------------------------------------------------------  compileCFiles :: IO () compileCFiles = do-  _ <- system $ "gcc copilot.c driver.c -o _test"+  _ <- system $ unwords [ "cd " ++ c99DirName ++ ";"+                        , "gcc"+                        , c99FileRoot ++ ".c" +                        , driverFile +                        , "-o"+                        , outputFile ]   return ()  --------------------------------------------------------------------------------  execute :: Int -> IO ByteString-execute _ = do-  fmap B.pack (readProcess "./_test" [] "")+execute _ =+  fmap B.pack (readProcess ("./" ++ c99DirName ++ "/" ++ outputFile) [] "")  -------------------------------------------------------------------------------- -interp :: Int -> ExtEnv -> Spec -> [Iteration]-interp numIterations env = -  execTraceToIterations . eval C numIterations env +interp :: Int -> Spec -> [Iteration]+interp numIterations = +  execTraceToIterations . eval C numIterations   --------------------------------------------------------------------------------  cleanUp :: IO ()-cleanUp = do-  removeFile "copilot.c"-  removeFile "copilot.h"-  removeFile "driver.c"-  removeFile "_test"-  return ()+cleanUp = removeDirectoryRecursive c99DirName+  -- removeFile $ c99FileRoot ++ ".c"+  -- removeFile $ c99FileRoot ++ ".h"+  -- removeFile driverFile+  -- removeFile outputFile  ---------------------------------------------------------------------------------

@@ -6,15 +6,22 @@  module Copilot.Compile.C99.Test.Driver   ( driver+--  , ExtVars   ) where  import Copilot.Core-  ( Spec (..), Trigger (..), UExpr (..), Type (..), UType (..), Name+  ( Spec(..), Trigger(..), UExpr(..), Type(..), UType(..), Name+  , Expr(..), Stream(..)   )-import Copilot.Core.Type.Dynamic (DynamicF (..))+++import Copilot.Core.Error (impossible)+import Copilot.Core.Type (Typed, typeOf)+import Copilot.Core.Type.Dynamic (DynamicF (..), toDynF) import Copilot.Core.Type.Show (showWithType, ShowType (..))-import Copilot.Core.Interpret.Eval (ExtEnv(..))-import Data.List (intersperse)+--import Copilot.Core.Interpret.Eval (ExtEnv(..))++import Data.List (intersperse, nubBy) import Data.Text (Text) import Data.Text (pack) import Text.PrettyPrint@@ -24,16 +31,57 @@  -------------------------------------------------------------------------------- -driver :: Int -> ExtEnv -> Spec -> Text-driver numIterations env Spec { specTriggers = trigs } =-  pack $ render $+driver :: Int -> Spec -> Text+driver numIterations Spec { specTriggers = trigs +                          , specStreams = streams } +  =+  pack . render $     ppHeader $$     ppEnvDecls numIterations env $$     ppMain numIterations env $$     ppTriggers trigs+  where +  env :: [ExtVars]+  env = nubBy (\(name0,_) (name1,_) -> name0 == name1) +              (concatMap extractExts exprs)+  exprs =    map strmExpr streams+          ++ concatMap triggerArgs trigs +          ++ map uexpr (map triggerGuard trigs)+  strmExpr Stream { streamExpr = expr } = uexpr expr+  uexpr :: Typed a => Expr a -> UExpr+  uexpr e = UExpr { uExprType = typeOf+                  , uExprExpr = e }  -------------------------------------------------------------------------------- +-- XXX will need to be generalized to external arrays and functions at some+-- point.+type  ExtVars = (Name, DynamicF [] Type)++extractExts :: UExpr -> [ExtVars]+extractExts UExpr { uExprExpr = expr } +  = go expr++  where+  go :: Expr a -> [ExtVars]+  go e =+    case e of+      Const _ _                    -> []+      Drop _ _ _                   -> []+      Local _ _ _ e0 e1            -> go e0 ++ go e1+      Var _ _                      -> []+      ExternVar t name mvals       -> +        case mvals of+          Nothing   -> impossible "extractExts" "copilot-c99/Test" +          Just vals -> [(name, toDynF t vals)]+      ExternFun _ _ es _ _         -> concatMap extractExts es+      ExternArray _ _ _ _ idx _ _  -> go idx+      Op1 _ e0                     -> go e0+      Op2 _ e0 e1                  -> go e0 ++ go e1+      Op3 _ e0 e1 e2               -> go e0 ++ go e1 ++ go e2++--------------------------------------------------------------------------------+ ppHeader :: Doc ppHeader =   vcat $@@ -45,8 +93,8 @@  -------------------------------------------------------------------------------- -ppEnvDecls :: Int -> ExtEnv -> Doc-ppEnvDecls numIterations ExtEnv { varEnv = vars } = +ppEnvDecls :: Int -> [ExtVars] -> Doc+ppEnvDecls numIterations vars =    vcat $       [ space       , text "// External variables" @@ -82,8 +130,8 @@  -------------------------------------------------------------------------------- -ppMain :: Int -> ExtEnv -> Doc-ppMain numIterations ExtEnv { varEnv = vars } =+ppMain :: Int -> [ExtVars] -> Doc+ppMain numIterations vars =   vcat $     [ text "int main(int argc, char const *argv[]) {"     , text "  int i;"@@ -112,20 +160,14 @@ ppTriggers = foldr ($$) empty . map ppTrigger  ppTrigger :: Trigger -> Doc-ppTrigger-  Trigger-    { triggerName = name-    , triggerArgs = args } =+ppTrigger Trigger { triggerName = name+                  , triggerArgs = args } +  =   hcat $-    [ text "void" <+>-        text name <+>-        text "(" <>-        ppPars args <>-        text ")"+    [ text "void" <+> text name <+> +           text "(" <> ppPars args <> text ")"     , text "{"-    , nest 2 $-        ppPrintf name args <>-        text ";"+    , nest 2 $ ppPrintf name args <> text ";"     , text "}"     ] 

@@ -7,7 +7,7 @@ module Main (main) where  import Copilot.Core.PrettyPrint (prettyPrint)-import Copilot.Core.Random (randomSpec, randomExtVals)+import Copilot.Core.Random (randomSpec) import Copilot.Core.Random.Weights (Weights (..), simpleWeights) import Copilot.Compile.C99.Test.CheckSpec (checkSpec) @@ -24,8 +24,8 @@     , maxTrigArgs  = 1     , maxObservers = 0     , numStreams   = 3 -    , floatFreq    = 0-    , doubleFreq   = 0 +    , floatFreq    = 1+    , doubleFreq   = 1     , divModFreq   = False     } @@ -36,12 +36,12 @@ testRandomSpec :: IO Bool testRandomSpec = do   g <- newStdGen-  let spec = randomSpec myWeights g-  let env = randomExtVals numIterations spec myWeights g+  let spec = randomSpec numIterations myWeights g+--  let env = randomExtVals numIterations spec myWeights g   putStrLn "------------------------------------------"   putStrLn "Specification to test:"   putStrLn $ prettyPrint spec-  checkSpec numIterations env spec+  checkSpec numIterations spec  main :: IO () main = do