copilot 2.0.1 → 2.0.2
raw patch · 4 files changed
+127/−130 lines, 4 filesdep +copilot-sbvdep +random
Dependencies added: copilot-sbv, random
Files
- Examples/Test.hs +121/−0
- README.md +1/−1
- Tests/Test.hs +0/−127
- copilot.cabal +5/−2
+ Examples/Test.hs view
@@ -0,0 +1,121 @@+--------------------------------------------------------------------------------+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- | A test suite to check for basic functionality.++module Main where++import System.Directory ( removeDirectoryRecursive+ , doesDirectoryExist+ , doesFileExist+ , removeFile )+import qualified Copilot.Compile.C99 as C99+import qualified Copilot.Compile.SBV as SBV+import qualified Copilot.Tools.CBMC as M+import Control.Monad (when)++import AddMult+import Array+--import BadExtVars+import Cast+import ClockExamples+import EngineExample+import Examples+import Examples2+import ExtFuns+import Local+import LTLExamples+import PTLTLExamples+import Random+import RegExpExamples+import StackExamples+import StatExamples+import VotingExamples+++--------------------------------------------------------------------------------++main :: IO ()+main = do+ cleanup+ putStrLn "Testing addMult ..."+ addMult >> cleanup+ putStrLn ""+ putStrLn "Testing array ..."+ array >> cleanup+ putStrLn ""+-- putStrLn "Testing badExtVars ..."+-- badExtVars >> cleanup+ putStrLn ""+ putStrLn "Testing castEx ..."+ castEx >> cleanup+ putStrLn ""+ putStrLn "Testing clockExamples ..."+ clockExamples >> cleanup+ putStrLn ""+ putStrLn "Testing engineExample ..."+ engineExample >> cleanup+ putStrLn ""+ putStrLn "Testing examples ..."+ examples >> cleanup+ putStrLn ""+ putStrLn "Testing examples2 ..."+ examples2 >> cleanup+ putStrLn ""+ putStrLn "Testing extFuns ..."+ extFuns >> cleanup+ putStrLn ""+ putStrLn "Testing localEx ..."+ localEx >> cleanup+ putStrLn ""+ putStrLn "Testing ltlExamples ..."+ ltlExamples >> cleanup+ putStrLn ""+ putStrLn "Testing ptltlExamples ..."+ ptltlExamples >> cleanup+ putStrLn ""+ putStrLn "Testing randomEx ..."+ randomEx >> cleanup+ putStrLn ""+ putStrLn "Testing regExpExamples ..."+ regExpExamples >> cleanup+ putStrLn ""+ putStrLn "Testing stackExamples ..."+ stackExamples >> cleanup+ putStrLn ""+ putStrLn "Testing statExamples ..."+ statExamples >> cleanup+ putStrLn ""+ putStrLn "Testing votingExamples ..."+ votingExamples >> cleanup+ putStrLn ""+ putStrLn ""+ putStrLn "************************************"+ putStrLn " Ok, the basic tests passed. Enjoy!"+ putStrLn "************************************"++--------------------------------------------------------------------------------++cleanup :: IO ()+cleanup = do++ b0 <- doesDirectoryExist SBV.sbvDirName+ when b0 (removeDirectoryRecursive SBV.sbvDirName)++ b1 <- doesDirectoryExist C99.c99DirName+ when b1 (removeDirectoryRecursive C99.c99DirName)++ let cbmc = "cbmc_driver.c"+ b2 <- doesFileExist cbmc+ when b2 (removeFile cbmc)++ let atomCBMC = M.appendPrefix M.atomPrefix C99.c99DirName+ b3 <- doesDirectoryExist atomCBMC+ when b3 (removeDirectoryRecursive atomCBMC)++ let sbvCBMC = M.appendPrefix M.sbvPrefix SBV.sbvDirName+ b4 <- doesDirectoryExist sbvCBMC+ when b4 (removeDirectoryRecursive sbvCBMC)++--------------------------------------------------------------------------------
README.md view
@@ -27,7 +27,7 @@ Currently, this includes the C99 back-end and the SBV back-end. * [copilot-c99](http://hackage.haskell.org/package/copilot-c99) A back-end that- translates to [Atom](http://hackage.haskell.org/package/copilot-cbmc) to+ translates to [Atom](http://hackage.haskell.org/package/atom) to generate hard real-time C code. Optionally, you may which also to install
− Tests/Test.hs
@@ -1,127 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | A very small test suite to check for basic functionality.--{-# LANGUAGE RebindableSyntax #-}--module Main where--import qualified Prelude as P-import Language.Copilot hiding (even, odd)-import Copilot.Compile.C99--import System.Directory (removeFile)---------------------------------------------------------------------------------------- Some utility functions:-----flipflop :: Stream Bool -> Stream Bool-flipflop x = y- where- y = [False] ++ if x then not y else y--nats :: Stream Word64-nats = [0] ++ nats + 1--even :: (P.Integral a, Typed a) => Stream a -> Stream Bool-even x = x `mod` 2 == 0--odd :: (P.Integral a, Typed a) => Stream a -> Stream Bool-odd = not . even--counter :: (Num a, Typed a) => Stream Bool -> Stream a-counter reset = y- where- zy = [0] ++ y- y = if reset then 0 else zy + 1--booleans :: Stream Bool-booleans = [True, True, False] ++ booleans--fib :: Stream Word64-fib = [1, 1] ++ fib + drop 1 fib--bitWise :: Stream Word8-bitWise = ( let a = [ 1, 1, 0 ] ++ a in a )- .^.- ( let b = [ 0, 1, 1 ] ++ b in b )--sumExterns :: Stream Word64-sumExterns =- let- ex1 = extern "e1"- ex2 = extern "e2"- in- ex1 + ex2----------------------------------------------------------------------------------------- An example of a complete copilot specification.----- A specification:-spec :: Spec -spec =- do- -- A trigger with four arguments:- trigger "e" booleans- [ arg fib, arg nats, arg sumExterns, arg bitWise ]-- -- A trigger with two arguments:- trigger "f" booleans- [ arg fib, arg sumExterns ]-- -- A trigger with a single argument:- trigger "g" (flipflop booleans)- [ arg (sumExterns + counter false + 25) ]-- -- A trigger with a single argument (should never fire):- trigger "h" (extern "e3" /= fib)- [ arg (0 :: Stream Int8) ]-- observer "i" (odd nats)----- Some infinite lists for simulating external variables:-e1, e2, e3 :: [Word64]-e1 = [0..]-e2 = 5 : 4 : e2-e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3)--main :: IO ()-main = do- putStrLn "PrettyPrinter:"- putStrLn ""- prettyPrint spec- putStrLn ""- putStrLn ""- putStrLn "Interpreter:"- putStrLn ""- interpret 10 [var "e1" e1, var "e2" e2, var "e3" e3] spec- putStrLn ""- putStrLn ""- putStrLn "Atom compilation:"- reify spec >>= compile defaultParams - cleanUp - putStrLn "*********************************"- putStrLn " Ok, things seem to work. Enjoy!"- putStrLn "*********************************"-- -- Don't assume SBV is installed.- -- putStrLn "Check equivalence:"- -- putStrLn ""- -- putStrLn ""- -- reify spec >>= - -- C.genCBMC C.defaultParams {C.numIterations = 20}------------------------------------------------------------------------------------cleanUp :: IO ()-cleanUp = do- removeFile "copilot.c"- removeFile "copilot.h"- return ()
copilot.cabal view
@@ -1,5 +1,5 @@ name: copilot-version: 2.0.1+version: 2.0.2 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE@@ -37,7 +37,7 @@ executable copilot-regression default-language : Haskell2010- hs-source-dirs : Tests, src+ hs-source-dirs : Examples, src ghc-options : -Wall -fwarn-tabs main-is : Test.hs build-depends:@@ -45,5 +45,8 @@ , copilot-core , copilot-language , copilot-libraries+ , copilot-sbv+ , copilot-cbmc , copilot-c99 >= 0.2 , directory >= 1.1+ , random