copilot-c99 3.1.2 → 3.2
raw patch · 10 files changed
+312/−17 lines, 10 filesdep +QuickCheckdep +copilot-c99dep +copilot-languagedep ~basedep ~copilot-coredep ~language-c99PVP ok
version bump matches the API change (PVP)
Dependencies added: QuickCheck, copilot-c99, copilot-language, csv, hspec, process
Dependency ranges changed: base, copilot-core, language-c99, language-c99-simple, pretty
API changes (from Hackage documentation)
+ Copilot.Compile.C99.Translate: explicitty :: Type a -> Expr -> Expr
Files
- CHANGELOG +15/−0
- copilot-c99.cabal +23/−2
- src/Copilot/Compile/C99/CodeGen.hs +1/−1
- src/Copilot/Compile/C99/Compile.hs +4/−0
- src/Copilot/Compile/C99/Translate.hs +23/−14
- testing/Copilot/Compile/C99/Driver.hs +128/−0
- testing/Copilot/Compile/C99/Property/MatchesInterpreter.hs +41/−0
- testing/Copilot/Compile/C99/Property/SequencePoint.hs +30/−0
- testing/Copilot/Compile/C99/Test.hs +32/−0
- testing/Main.hs +15/−0
CHANGELOG view
@@ -1,3 +1,18 @@+2020-12-06+ * Version bump (3.2).+ * Implemented arrays in test driver (#37).+ * Fixed nested array initialisation bug (#40).+ * Fixed length of buffer allocation for n-dimensional arrays (#39).+ * Fixed printing of long ints in test suite (#36).+ * Fixed printing of unsigned ints in test suite (#36).+ * Fixed '-Wsequence-point' warnings from GCC (#34).+ * Split Property.hs (#33).+ * Removed 'Test' from module paths (#32).+ * Made compiletest take compiler options as an argument (#31).+ * Fixed problem with property and empty string in driver CSV (#30).+ * Added comma to output of driver to match the interpreter (#29).+ * Implemented basic quickcheck based testing (#28).+ 2020-03-30 * Version bump (3.1.2) * Fixed bug where stream buffers are updated too soon. (#21)
copilot-c99.cabal view
@@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-c99-version : 3.1.2+version : 3.2 synopsis : A compiler for Copilot targeting C99. description : This package is a back-end from Copilot to C.@@ -41,7 +41,7 @@ , mtl >= 2.2 && < 2.3 , pretty >= 1.1 && < 1.2 - , copilot-core >= 3.1 && < 3.2+ , copilot-core >= 3.2 && < 3.3 , language-c99 >= 0.1.1 && < 0.2 , language-c99-util >= 0.1.1 && < 0.2 , language-c99-simple >= 0.1.1 && < 0.2@@ -52,3 +52,24 @@ , Copilot.Compile.C99.CodeGen , Copilot.Compile.C99.External , Copilot.Compile.C99.Compile++test-suite test+ type: exitcode-stdio-1.0+ default-language: Haskell2010+ hs-source-dirs: testing+ main-is: Main.hs+ other-modules: Copilot.Compile.C99.Driver+ , Copilot.Compile.C99.Test+ , Copilot.Compile.C99.Property.MatchesInterpreter+ , Copilot.Compile.C99.Property.SequencePoint+ build-depends: base+ , copilot-core+ , copilot-c99 >= 3.2 && < 3.3+ , copilot-language >= 3.2 && < 3.3+ , language-c99 >= 0.1.2 && < 0.2+ , language-c99-simple+ , pretty >= 1.1.3 && < 1.2+ , process >= 1.6.5 && < 1.7+ , QuickCheck >= 2.14 && < 2.15+ , csv >= 0.1.2 && < 0.2+ , hspec >= 2.7.1 && < 2.8
src/Copilot/Compile/C99/CodeGen.hs view
@@ -87,7 +87,7 @@ indexupdate = C.Expr $ index_var C..= (incindex C..% bufflength) where bufflength = C.LitInt $ fromIntegral $ length buff- incindex = (C..++) index_var+ incindex = index_var C..+ C.LitInt 1 tmp_var = streamname sid ++ "_tmp" buff_var = C.Ident $ streamname sid
src/Copilot/Compile/C99/Compile.hs view
@@ -22,9 +22,13 @@ hfile = render $ pretty $ C.translate $ compileh spec -- TODO: find a nicer solution using annotated AST's+ -- Should figure out exactly which headers are needed, based on what+ -- is used. cmacros = unlines [ "#include <stdint.h>" , "#include <stdbool.h>" , "#include <string.h>"+ , "#include <stdlib.h>"+ , "#include <math.h>" , "" , "#include \"" ++ prefix ++ ".h\"" , ""
src/Copilot/Compile/C99/Translate.hs view
@@ -112,23 +112,32 @@ constty :: Type a -> a -> C.Expr constty ty = case ty of Bool -> C.LitBool- Int8 -> C.LitInt . fromIntegral- Int16 -> C.LitInt . fromIntegral- Int32 -> C.LitInt . fromIntegral- Int64 -> C.LitInt . fromIntegral- Word8 -> C.LitInt . fromIntegral- Word16 -> C.LitInt . fromIntegral- Word32 -> C.LitInt . fromIntegral- Word64 -> C.LitInt . fromIntegral- Float -> C.LitFloat- Double -> C.LitDouble+ Int8 -> explicitty ty . C.LitInt . fromIntegral+ Int16 -> explicitty ty . C.LitInt . fromIntegral+ Int32 -> explicitty ty . C.LitInt . fromIntegral+ Int64 -> explicitty ty . C.LitInt . fromIntegral+ Word8 -> explicitty ty . C.LitInt . fromIntegral+ Word16 -> explicitty ty . C.LitInt . fromIntegral+ Word32 -> explicitty ty . C.LitInt . fromIntegral+ Word64 -> explicitty ty . C.LitInt . fromIntegral+ Float -> explicitty ty . C.LitFloat+ Double -> explicitty ty . C.LitDouble Struct _ -> \v -> C.InitVal (transtypename ty) (map fieldinit (toValues v)) where fieldinit (Value ty (Field val)) = C.InitExpr $ constty ty val- Array ty' -> \v -> C.InitVal (transtypename ty) (map valinit (arrayelems v))+ Array ty' -> \v -> C.InitVal (transtypename ty) (vals v) where- valinit = C.InitExpr . constty ty'+ vals v = constarray ty' (arrayelems v) + constarray :: Type a -> [a] -> [C.Init]+ constarray ty xs = case ty of+ Array ty' -> constarray ty' (concatMap arrayelems xs)+ _ -> map (C.InitExpr . constty ty) xs+++explicitty :: Type a -> C.Expr -> C.Expr+explicitty ty = C.Cast (transtypename ty)+ -- | Translate a Copilot type to a C99 type. transtype :: Type a -> C.Type transtype ty = case ty of@@ -143,8 +152,8 @@ Word64 -> C.TypeSpec $ C.TypedefName "uint64_t" Float -> C.TypeSpec C.Float Double -> C.TypeSpec C.Double- Array ty' -> C.Array (transtype ty') size where- size = Just $ C.LitInt $ fromIntegral $ tysize ty+ Array ty' -> C.Array (transtype ty') length where+ length = Just $ C.LitInt $ fromIntegral $ tylength ty Struct s -> C.TypeSpec $ C.Struct (typename s) -- | Translate a Copilot type intro a C typename
+ testing/Copilot/Compile/C99/Driver.hs view
@@ -0,0 +1,128 @@+{-# LANGUAGE GADTs #-}++module Copilot.Compile.C99.Driver (writedriver) where++import Data.List (intersperse)++import Language.C99.Simple as C99++import Copilot.Core as Core+ ( Spec (..)+ , UExpr (..)+ , Trigger (..)+ , Type (..)+ , Value (..)+ , toValues+ , fieldname+ , tylength+ )+import Copilot.Compile.C99.Translate (transtype)+import Copilot.Compile.C99.Util (argnames)++import Text.PrettyPrint (render)+import Language.C99.Simple (translate)+import Language.C99.Pretty (pretty)+++-- | Write the complete driver .c file code based on the specification.+writedriver :: String -> Spec -> Int -> String+writedriver specname spec iters = unlines (includes) ++ code+ where+ includes = [ "#include <stdio.h>"+ , "#include <stdint.h>"+ , "#include <stdbool.h>"+ , "#include \"" ++ specname ++ ".h\""+ ]+ code = render $ pretty $ translate $ mktransunit spec iters+++-- | Write a C driver mimicking Copilot's interpreter.+mktransunit :: Spec -> Int -> TransUnit+mktransunit spec iters = TransUnit vardefs fundefs+ where+ vardefs = []+ fundefs = ctriggers ++ [ mkmain iters spec ]+ ctriggers = map mktrigger (specTriggers spec)+++-- | Write a trigger function which prints all its arguments in a CSV like+-- format.+mktrigger :: Trigger -> FunDef+mktrigger (Trigger name guard args) = FunDef returntype name params [] body+ where+ returntype = TypeSpec Void+ namedargs = zip (argnames name) args+ params = map mkparam namedargs+ body = [Expr $ mkprintfcsv name namedargs]++ mkparam :: (String, UExpr) -> Param+ mkparam (name, UExpr ty _) = Param (transtype ty) name+++-- | Write the main function. The purpose of this function is to call the+-- step-function a number of times.+mkmain :: Int -> Spec -> FunDef+mkmain iters spec = FunDef (TypeSpec Int) "main" params decln body+ where+ params = [ Param (TypeSpec Int) "argc"+ , Param (Const $ C99.Array (Ptr $ TypeSpec Char) Nothing) "argv"+ ]+ decln = [VarDecln Nothing (TypeSpec Int) "i" (Just $ InitExpr $ LitInt 0)]+ body = [For (Ident "i" .= LitInt 0)+ (Ident "i" .< LitInt (fromIntegral iters))+ (UnaryOp Inc (Ident "i"))+ [ Expr $ Funcall (Ident "printf") [LitString "#\n"]+ , Expr $ Funcall (Ident "step") []+ ]+ ]+++-- | Write a call to printf with a format resembling CSV.+mkprintfcsv :: String -> [(String, UExpr)] -> Expr+mkprintfcsv trigname namedargs = Funcall (Ident "printf") (fmt:vals)+ where+ fmt = LitString $ trigname ++ "," ++ concat (intersperse "," argfmt) ++ "\n"+ argfmt = map (uexprfmt.snd) namedargs+ vals = concatMap (\(name, UExpr ty _) -> mkidents name ty) namedargs++ uexprfmt :: UExpr -> String+ uexprfmt (UExpr ty _) = tyfmt ty++ tyfmt :: Core.Type a -> String+ tyfmt ty = case ty of+ Core.Bool -> "%s"+ Core.Int8 -> "%d"+ Core.Int16 -> "%d"+ Core.Int32 -> "%d"+ Core.Int64 -> "%ld"+ Core.Word8 -> "%u"+ Core.Word16 -> "%u"+ Core.Word32 -> "%u"+ Core.Word64 -> "%lu"+ Core.Float -> "%f"+ Core.Double -> "%f"+ Core.Struct s -> "<" ++ elems ++ ">"+ where+ elems = concat $ intersperse "," $ map fieldfmt (toValues s)+ fieldfmt :: Core.Value a -> String+ fieldfmt (Core.Value ty f) = Core.fieldname f ++ ":" ++ tyfmt ty+ Core.Array ty' -> "[" ++ elems ++ "]"+ where+ elems = concat $ intersperse "," $ map tyfmt types+ types = replicate (Core.tylength ty) ty'++ mkidents :: String -> Core.Type a -> [Expr]+ mkidents name ty = case ty of+ Core.Struct _ -> error "mkidents: Struct not implemented yet."+ Core.Array _ -> idents ty [Ident name]+ where+ idents :: Core.Type a -> [Expr] -> [Expr]+ idents ty' es = case ty' of+ Core.Array ty'' -> idents ty'' [ Index es' (LitInt i)+ | es' <- es+ , i <- take (tylength ty') [0..]+ ]+ Core.Bool -> [Cond g (LitString "True") (LitString "False") | g <- es]+ _ -> es+ Core.Bool -> [Cond (Ident name) (LitString "true") (LitString "false")]+ _ -> [Ident name]
+ testing/Copilot/Compile/C99/Property/MatchesInterpreter.hs view
@@ -0,0 +1,41 @@+module Copilot.Compile.C99.Property.MatchesInterpreter where++import Data.Either (isRight)++import Text.CSV+import Test.QuickCheck+import Test.QuickCheck.Monadic++-- We import Copilot.Language vs Language.Copilot* as that would create a+-- dependency cycle. It forces us to import from multiple files however.+import Copilot.Core.Interpret (interpret, Format(..))+import Copilot.Language (Spec)+import Copilot.Language.Reify (reify)+import Copilot.Language.Arbitrary++import Copilot.Compile.C99.Test+++-- | For a given specification, the output of the driver should match the+-- output of Copilots interpreter.+prop_matches_interpreter :: Spec -> Property+prop_matches_interpreter langspec = monadicIO $ do+ let specname = "testspec"+ mainfile = specname ++ "_main.c"+ iters = 30+ spec <- run $ reify langspec+ run $ writetest specname mainfile spec iters+ run $ compiletest specname mainfile ["-Wall", "-pedantic-errors"]++ -- Run the interpreter and parse CSV.+ let interpout = interpret CSV iters spec+ interpcsv = parseCSV "" interpout+ interpparsed = counterexample "Interpreter output parse failed."+ (isRight interpcsv)++ -- Run the test and parse CSV.+ c99out <- run $ runtest specname+ let c99csv = init <$> parseCSV "" c99out+ c99parsed = counterexample "C99 output parse failed." (isRight c99csv)++ return $ c99parsed .&&. interpparsed .&&. c99csv === interpcsv
+ testing/Copilot/Compile/C99/Property/SequencePoint.hs view
@@ -0,0 +1,30 @@+module Copilot.Compile.C99.Property.SequencePoint where++import Copilot.Core.Interpret (interpret, Format(..))+import Copilot.Language as C+import Copilot.Language.Reify (reify)++import Copilot.Compile.C99.Test+++-- | The code generator does not produce code that raises -Wsequence-point+-- warnings in GCC.+-- We test this by generating code for a minimal specification that would raise+-- a warning. We compile the spec with the proper flags to the C compiler, in+-- case it compiles fine, we know that error didn't raise. In case of an+-- exception, we never reach `return True`.+-- Issue #34: Fix '-Wsequence-point' warnings from GCC+prop_sequencepoint :: IO Bool+prop_sequencepoint = do+ let specname = "sequencepoint_test"+ mainfile = specname Prelude.++ "_main.c"++ let testspec = trigger "sequencepoint_test" true [arg s0]+ where+ s0 :: Stream Int8+ s0 = [1, 2] C.++ s0 -- Buffer shoud hold >1 elems to raise warning.++ spec <- reify testspec+ writetest specname mainfile spec 1+ compiletest specname mainfile ["-Wsequence-point", "-Werror"]+ return True
+ testing/Copilot/Compile/C99/Test.hs view
@@ -0,0 +1,32 @@+module Copilot.Compile.C99.Test where++import System.Process (readProcess)++import Copilot.Core (Spec)+import Copilot.Compile.C99 (compile)++import Copilot.Compile.C99.Driver+++-- | Compile the specification and generate the test driver, then write these+-- to specname.[ch] and a main file.+writetest :: String -> String -> Spec -> Int -> IO ()+writetest specname mainfile spec iters = do+ let drivercode = writedriver specname spec iters+ writeFile mainfile drivercode+ compile specname spec+++-- | Compile the C code to using GCC to a binary.+-- This function fails if the files names specname.c and mainfile do not exist.+compiletest :: String -> String -> [String] -> IO String+compiletest specname mainfile cflags = do+ let output = ["-o", specname]+ cfiles = [mainfile, specname ++ ".c"]+ args = cflags ++ output ++ cfiles+ readProcess "gcc" args ""+++-- | Run the compiled specification and driver.+runtest :: String -> IO String+runtest specname = readProcess ("./" ++ specname) [] ""
+ testing/Main.hs view
@@ -0,0 +1,15 @@+module Main where++import Test.Hspec+import Test.QuickCheck++import Copilot.Compile.C99.Property.MatchesInterpreter+import Copilot.Compile.C99.Property.SequencePoint++main = hspec $ do+ describe "copilot-c99" $ do+ it "generates C99 code that matches the semantics of the interpreter." $ do+ property prop_matches_interpreter++ it "does not raise a sequence-point warning when updating the index." $ do+ prop_sequencepoint >>= shouldBe True