copilot 2.2.1 → 3.0
raw patch · 25 files changed
+299/−1439 lines, 25 filesdep +filepathdep +optparse-applicativedep −copilot-cbmcdep −copilot-sbvdep −randomdep ~basedep ~copilot-c99dep ~copilot-corenew-uploaderPVP ok
version bump matches the API change (PVP)
Dependencies added: filepath, optparse-applicative
Dependencies removed: copilot-cbmc, copilot-sbv, random
Dependency ranges changed: base, copilot-c99, copilot-core, copilot-language, copilot-libraries, copilot-theorem, directory
API changes (from Hackage documentation)
+ Language.Copilot: copilotMain :: Interpreter -> Printer -> Compiler -> Spec -> IO ()
+ Language.Copilot: defaultMain :: Compiler -> Spec -> IO ()
+ Language.Copilot.Main: copilotMain :: Interpreter -> Printer -> Compiler -> Spec -> IO ()
+ Language.Copilot.Main: defaultMain :: Compiler -> Spec -> IO ()
Files
- Examples/AddMult.hs +0/−35
- Examples/Array.hs +26/−36
- Examples/Cast.hs +0/−32
- Examples/ClockExamples.hs +0/−28
- Examples/EngineExample.hs +0/−41
- Examples/Examples.hs +0/−168
- Examples/Examples2.hs +0/−75
- Examples/ExtFuns.hs +0/−60
- Examples/Heater.hs +34/−0
- Examples/LTLExamples.hs +0/−48
- Examples/Languages.hs +0/−216
- Examples/Local.hs +0/−43
- Examples/PTLTLExamples.hs +0/−78
- Examples/Random.hs +0/−21
- Examples/RegExpExamples.hs +0/−49
- Examples/Sat.hs +0/−67
- Examples/StackExamples.hs +0/−34
- Examples/StatExamples.hs +0/−41
- Examples/Struct.hs +45/−0
- Examples/Test.hs +0/−176
- Examples/VotingExamples.hs +0/−61
- README.md +115/−77
- copilot.cabal +22/−53
- src/Language/Copilot.hs +4/−0
- src/Language/Copilot/Main.hs +53/−0
− Examples/AddMult.hs
@@ -1,35 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Another small example.--module AddMult ( addMult ) where--import Prelude ()-import Language.Copilot------------------------------------------------------------------------------------spec :: Spec-spec = - trigger "f" true [ arg $ mult 5 ]-- where- mult :: Word64 -> Stream Word64- mult 0 = 1- mult i = constant i * mult (i-1)--addMult :: IO ()-addMult = do- putStrLn "PrettyPrinter:"- putStrLn ""- prettyPrint spec- putStrLn ""- putStrLn ""- putStrLn "Interpreter:"- putStrLn ""- interpret 100 spec-----------------------------------------------------------------------------------
Examples/Array.hs view
@@ -1,47 +1,37 @@ ----------------------------------------------------------------------------------- Copyright © 2011 National Institute of Aerospace / Galois, Inc.+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc. -------------------------------------------------------------------------------- --- | Example in sampling external arrays.--{-# LANGUAGE RebindableSyntax #-}--module Array ( array ) where--import Language.Copilot hiding (cycle)-import Data.List (cycle)---import qualified Copilot.Compile.C99 as C-import qualified Copilot.Compile.SBV as S----------------------------------------------------------------------------------+-- This is a simple example for arrays. As a program, it does not make much+-- sense, however it shows of the features of arrays nicely. -extArr :: Stream Word32-extArr = externArray "arr1" arrIdx 5 (Just $ repeat [7,8,9,10,11])+-- Enable compiler extension for type-level data, necesary for the array length.+{-# LANGUAGE DataKinds #-} -arrIdx :: Stream Word32-arrIdx = [0] ++ (arrIdx + 1) `mod` 4+module Array where -arrIdx2 :: Stream Word8-arrIdx2 = extern "idx2" (Just [0,0..])+import Language.Copilot+import Copilot.Compile.C99 -extArr2 :: Stream Word16 -> Stream Word32-extArr2 idx = externArray "arr2" idx 4 (Just $ repeat [1,2,3,4])+import Prelude hiding ((++), (>)) -extArr3 :: Stream Word32-extArr3 = extArr2 (cast $ externW8 "idx3" (Just $ cycle [0,1,2])) +-- Lets define an array of length 2.+-- Make the buffer of the streams 3 elements long.+arr :: Stream (Array 2 Bool)+arr = [ array [True, False]+ , array [True, True]+ , array [False, False]] ++ arr -spec :: Spec-spec = trigger "trigger" true [ arg extArr- , arg (extArr2 (cast arrIdx2))- , arg extArr3--- Throws an exception since the index is too big for the array!--- , arg (extArr2 5)- ]+-- Refer to an external array.+exarr :: Stream (Array 3 Int8)+exarr = extern "exarr" Nothing -array :: IO ()-array = do--- reify spec >>= C.compile C.defaultParams - interpret 10 spec- reify spec >>= S.compile S.defaultParams +spec = do+ -- A trigger that fires 'func' when the first element of 'arr' is True.+ -- It passes the current value of exarr as an argument.+ -- The prototype of 'func' would be:+ -- void func (int8_t arg[3]);+ trigger "func" (arr .!! 0) [arg exarr] ---------------------------------------------------------------------------------+-- Compile the spec+main = reify spec >>= compile "array"
− Examples/Cast.hs
@@ -1,32 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE RebindableSyntax #-}---- Examples of casting types. --module Cast ( castEx ) where--import Language.Copilot hiding (even, odd)-import Copilot.Compile.C99--b :: Stream Bool-b = [True] ++ not b--i :: Stream Int8-i = cast b--x :: Stream Word16-x = [0] ++ x + 1--y :: Stream Int32-y = 1 + cast x--spec :: Spec-spec = trigger "trigger" true [arg y, arg i]--castEx :: IO ()-castEx = do - interpret 10 spec- reify spec >>= compile defaultParams
− Examples/ClockExamples.hs
@@ -1,28 +0,0 @@--- | Clocks library tests.--module ClockExamples ( clockExamples ) where--import Prelude ( putStrLn, IO, Bool )-import Copilot.Language-import Copilot.Library.Clocks--p :: Word8-p = 5 --clkStream, clk1Stream :: Stream Bool-clkStream = clk ( period p ) ( phase 0 )-clk1Stream = clk1 ( period p ) ( phase 0 )---clockTest :: Spec-clockTest = do- observer "clk" clkStream- observer "clk1" clk1Stream---clockExamples :: IO ()-clockExamples = do- prettyPrint clockTest- putStrLn ""- putStrLn ""- interpret 10 clockTest
− Examples/EngineExample.hs
@@ -1,41 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.-----------------------------------------------------------------------------------{-# LANGUAGE RebindableSyntax #-}--module EngineExample ( engineExample ) where--import Language.Copilot-import qualified Prelude as P---import qualified Copilot.Compile.SBV as S--{- - "If the majority of the engine temperature probes exeeds 250 degrees, then the- cooler is engaged and remains engaged until the majority of the engine- temperature probes drop to 250 or below. Otherwise, trigger an immediate- shutdown of the engine." -}--engineMonitor :: Spec-engineMonitor = do- trigger "shutoff" (not ok) [arg maj]-- where- vals = [ externW8 "tmp_probe_0" two51- , externW8 "tmp_probe_1" two51- , externW8 "tmp_probe_2" zero]- exceed = map (> 250) vals- maj = majority exceed- checkMaj = aMajority exceed maj- ok = alwaysBeen ((maj && checkMaj) ==> extern "cooler" cooler) -- two51 = Just $ [251, 251] P.++ repeat (250 :: Word8)- zero = Just $ repeat (0 :: Word8)- cooler = Just $ [True, True] P.++ repeat False--engineExample :: IO ()-engineExample = interpret 10 engineMonitor---- reify engineMonitor >>= S.compile (S.Params { S.prefix = Just "engine" })- -
− Examples/Examples.hs
@@ -1,168 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Some Copilot examples.--{-# LANGUAGE RebindableSyntax #-}--module Examples ( examples ) where--import qualified Prelude as P-import Language.Copilot hiding (even, odd)---import Copilot.Compile.C99-import qualified Copilot.Tools.CBMC as C----------------------------------------------------------------------------------------- Some utility functions:-----{---implyStream :: Stream Bool -> Stream Bool -> Stream Bool-implyStream p q = not p || q---extEven :: Stream Bool-extEven = externX `mod` 2 == 0--oddSpec :: Spec-oddSpec = trigger "f" true [arg (odd nats)]--prop :: Stream Bool-prop = (x - x') <= 5 && (x - x') <= (-5)- where- x :: Stream Int32- x = [0] ++ cast externX- x' = drop 1 x--externX :: Stream Int8-externX = extern "x" (Just [0..])--foo :: Spec-foo = do- let x = cast externX :: Stream Int16- trigger "trigger" true [arg $ x < 3]- observer "debug_x" x--latch :: Stream Bool -> Stream Bool-latch x = out- where out = if x then not st else st- st = [False] ++ out--latch' :: Stream Bool -> Stream Bool-latch' x = out- where out = x `xor` st- st = [False] ++ out--ext :: Stream Word8-ext = [1] ++ ext + extern "e0" (Just [2,4..])---}--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 :: (Eq a, 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" (Just e1)- ex2 = extern "e2" (Just e2)- in ex1 + ex2--latch :: Stream Bool -> Stream Bool-latch x = y- where - y = if x then not z else z- z = [False] ++ y----- Some infinite lists for simulating external variables:-e1, e2 :: [Word64]-e1 = [0..]-e2 = 5 : 4 : e2-a :: Stream Bool-a = [False, False, True, True ] ++ a---------------------------------------------------------------------------------------- An example of a complete copilot specification.------- A specification:-spec :: Spec -spec = do-- -- A trigger with four arguments:- trigger "e" true -- booleans- [ arg fib, arg nats, arg sumExterns, arg bitWise ]-- -- A trigger with two arguments:- trigger "f" booleans- [ arg fib, arg sumExterns ]--- [ arg fib, arg nats ]-- -- A trigger with a single argument:- trigger "g" (flipflop booleans)- [ arg (sumExterns + counter false + 25) ]--- [ arg (counter false + 25 :: Stream Int32) ]-- -- A trigger with a single argument (should never fire):- let e3 = [1, 1] P.++ zipWith (+) e3 (P.drop 1 e3)- trigger "h" (extern "e3" (Just e3) /= fib)- [ arg (0 :: Stream Int8) ]-- observer "i" (odd nats)--examples :: IO ()-examples = do- putStrLn "PrettyPrinter:"- putStrLn ""- prettyPrint spec- putStrLn ""- putStrLn ""- putStrLn "Interpreter:"- putStrLn ""- interpret 10 spec- -- putStrLn ""- -- putStrLn ""- -- putStrLn "Atom:"- -- reify spec >>= compile defaultParams - putStrLn "Check equivalence:"- putStrLn ""- putStrLn ""- reify spec >>= - C.genCBMC C.defaultParams {C.numIterations = 20}--test :: Spec-test = do- observer "obs" (latch a)---------------------------------------------------------------------------------
− Examples/Examples2.hs
@@ -1,75 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Some more Copilot examples.--{-# LANGUAGE RebindableSyntax #-}--module Examples2 ( examples2 ) where--import Prelude ()-import Language.Copilot--import qualified Copilot.Compile.SBV as S--import qualified Data.List as L------------------------------------------------------------------------------------{--alt2 :: Stream Word64-alt2 = [0,1,2] ++ alt2 + 1--alt3 :: Stream Bool-alt3 = [True,True,False] ++ alt3--fib' :: Stream Word64-fib' = [0, 1] ++ fib' + drop 1 fib--fib :: Stream Word64-fib = [0, 1] ++ fib + drop 1 fib--fibSpec :: Spec-fibSpec = do- trigger "fib_out" true [arg fib]--counter :: Stream Bool -> Stream Bool - -> Stream Int32-counter inc reset = cnt- where - cnt = if reset then 0- else if inc then z + 1- else z- z = [0] ++ cnt--}--nats :: Stream Word64-nats = [0] ++ nats + 1--alt :: Stream Bool-alt = [True] ++ not alt--logic :: Stream Bool-logic = [True, False] ++ logic || drop 1 logic--sumExterns :: Stream Word64-sumExterns =- let- e1 = extern "e1" (Just [0..])- e2 = extern "e2" (Just $ L.cycle [2,3,4])- in- e1 + e2 + e1--spec :: Spec-spec = do- trigger "trig1" alt [ arg $ nats < 3- , arg sumExterns - , arg logic- ]--examples2 :: IO ()-examples2 = do--- reify fibSpec >>= S.compile S.defaultParams--- reify spec >>= S.compile S.defaultParams - reify spec >>= S.compile (S.Params { S.prefix = Just "secondexamplespec" })
− Examples/ExtFuns.hs
@@ -1,60 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Example in sampling external functions.--{-# LANGUAGE RebindableSyntax #-}--module ExtFuns ( extFuns ) where--import Language.Copilot -import qualified Copilot.Compile.C99 as C-import qualified Copilot.Compile.SBV as S---import qualified Copilot.Tools.CBMC as B------------------------------------------------------------------------------------doubles :: Stream Word16-doubles = [0,1] ++ doubles + 1--------------------------------------------------------------------------------------- Function func0 and it's environment for interpreting-func0 :: Stream Word16-func0 = externFun "func0" [ arg x, arg doubles ]- (Just $ cast x + doubles)- where x = externW8 "x" (Just [0..])--------------------------------------------------------------------------------------- Function func1 and it's environment for interpreting-func1 :: Stream Bool-func1 = externFun "func1" [] (Just $ [False] ++ not func1)- -------------------------------------------------------------------------------------- Function func0 with another set of args and it's environment for interpreting-func2 :: Stream Word16-func2 = externFun "func0" [ arg $ constW8 3, arg $ constW16 4 ]- (Just $ cast (constW8 3) + constW16 4)-------------------------------------------------------------------------------------a :: Stream Word16-a = func0 + func0--spec :: Spec-spec = trigger "trigger" true [ arg func0- , arg func1- , arg func2- , arg a ]- -extFuns :: IO ()-extFuns = do- interpret 10 spec---- reify spec >>= C.compile C.defaultParams - reify spec >>= S.compile (S.Params { S.prefix = Just "externFunSpec" })-----------------------------------------------------------------------------------
+ Examples/Heater.hs view
@@ -0,0 +1,34 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- This is a simple example with basic usage. It implements a simple home+-- heating system: It heats when temp gets too low, and stops when it is high+-- enough. It read temperature as an byte (range -50C to 100C) and translates+-- this to Celcius.++module Heater where++import Language.Copilot+import Copilot.Compile.C99++import Prelude hiding ((>), (<), div)++-- External temperature as a byte, range of -50C to 100C+temp :: Stream Int8+temp = extern "temperature" Nothing++-- Calculate temperature in Celcius.+-- We need to cast the Int8 to a Float. Note that it is an unsafeCast, as there+-- is no direct relation between Int8 and Float.+ctemp :: Stream Float+ctemp = ((unsafeCast temp) / 150.0) - 50.0++spec = do+ -- Triggers that fire when the ctemp is too low or too hight,+ -- pass the current ctemp as an argument.+ trigger "heaton" (ctemp < 18.0) [arg ctemp]+ trigger "heafoff" (ctemp > 21.0) [arg ctemp]++-- Compile the spec+main = reify spec >>= compile "heater"
− Examples/LTLExamples.hs
@@ -1,48 +0,0 @@-module LTLExamples where--import qualified Prelude as P-import Language.Copilot--------------------- LTL tests ----------------------testAlways :: Int -> Int -> Stream Bool-testAlways i1 i2 = let input = replicate i1 P.True P.++ [ False ] ++ true- in always i2 input--testNext :: Stream Bool-testNext = let input = [ False, False, True ] ++ input- in next input--testFuture :: Int -> Int -> Stream Bool-testFuture i1 i2 = let input = replicate i1 False P.++ [ True ] ++ false- in eventually i2 input--testUntil :: Int -> Int -> Int -> Stream Bool-testUntil i1 i2 i3 =- let t0 = replicate i1 True ++ false- t1 = replicate ( i2 - 1 ) False P.++ [ True ] ++ false- in until i3 t0 t1--testRelease :: Int -> Int -> Int -> Stream Bool-testRelease i1 i2 i3 =- let t0 = replicate i1 True ++ false- t1 = replicate ( i2 - 1 ) False P.++ [ True ] ++ false- in release i3 t1 t0--ltlTest :: Spec-ltlTest = do- trigger "testAlways1" true [ arg $ testAlways 0 0 ]- trigger "testAlways2" true [ arg $ testAlways 5 1 ]- trigger "testNext" true [ arg $ testNext ]- trigger "testFuture" true [ arg $ testFuture 12 10 ]- trigger "testUntil" true [ arg $ testUntil 5 6 4 ]- trigger "testRelease" true [ arg $ testRelease 5 5 4 ]--ltlExamples :: IO ()-ltlExamples = do- prettyPrint ltlTest- putStrLn ""- putStrLn ""- interpret 20 ltlTest
− Examples/Languages.hs
@@ -1,216 +0,0 @@--- | Examples of parsing various languages. We'll assume input tokens come from--- an external variable. Assume the input doesn't given tokens outside the--- alphabet, and the result is always delayed by one w.r.t. the input stream.---- Copilot can compute at least NP-Complete problems.--{-# LANGUAGE RebindableSyntax #-}--module Languages (languages) where--import Language.Copilot-import qualified Prelude as P-import qualified Data.List as L-------------------------------------------------------------------------------------- Regular expressions--{- -We'll build a Copilot program to accept the regular language over the alphabet-{0,1} that contains an even number of 0s. --}--reAccept :: Spec-reAccept = do - observer "accept" accept- observer "string" string- where- accept :: Stream Bool- accept = [True] ++ if string == 0- then if accept then false- else true- else accept-- -- Input tokens.- string :: Stream Word8- string = [0] ++ if string == 0 then 1 else 0---- interpret 10 reAccept------------------------------------------------------------------------------------------------------------------------------------------------------------------------- Context-free Grammars--{--This Copilot program recognizes <0^n 1^n>, for n >= 0. --}--cfAccept :: Int -> Spec-cfAccept n = do- observer "accept" accept- observer "string" string- where- accept :: Stream Bool- accept = if zerosSeen == 0 - then true- else false-- zerosSeen :: Stream Word64- zerosSeen = [0] ++ if string == 0 - then zerosSeen + 1- else zerosSeen - 1-- -- Input tokens.- string :: Stream Word8- string = L.replicate n 0 P.++ L.replicate n 1 ++ 0 -- don't care about part of- -- stream after ++---- interpret 40 (cfAccept 10)------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Context-sensitive grammars--{--This Copilot program recognizes <0^n 1^n 2^n>, for n >= 0. --}--csAccept :: Int -> Spec-csAccept n = do- observer "accept" accept- observer "string" string- where- accept :: Stream Bool- accept = if zerosSeen == 0 && onesSeen == 0- then true- else false-- zerosSeen :: Stream Word64- zerosSeen = [0] ++ if string == 0- then zerosSeen + 1- else if string == 1 - then zerosSeen - 1- else zerosSeen-- onesSeen :: Stream Word64- onesSeen = [0] ++ if string == 1- then onesSeen + 1- else if string == 0 - then onesSeen- else onesSeen - 1-- -- Input tokens.- string :: Stream Word8- string = L.replicate n 0 P.++ L.replicate n 1 P.++ L.replicate n 2 - ++ 0 -- don't care about part of- -- stream after ++---- interpret 40 (csAccept 5)------------------------------------------------------------------------------------------------------------------------------------------------------------------------ Context-sensitive grammars--{--This Copilot program recognizes the "copy language" <xx | x \in {0,1}*>.--Note: the "trick" is to encode the history of streams in a bitvector. Thus, we-can only recognize arbitrarily long words if we have arbitrarily long-bitvectors. There is nothing in Copilot preventing this, but the largest base-type is currently a Word64. --Without this encoding, we couldn't build a recognizers, because we can't-generate new streams on the fly or look back arbitrarily far in the history of a-stream; both are fixed at compile time.---}---copyAccept :: Spec-copyAccept = do- observer "accept" accept- observer "hist" hist- observer "string" string- observer "cnt" cnt- where-- accept :: Stream Bool- accept = if cnt `mod` 2 == 1 then false else bottom == top - where- halfCnt = cnt `div` 2- zeroBot = (complement $ (2^halfCnt) - 1) .&. hist- top = zeroBot .>>. halfCnt- bottom = hist - zeroBot-- hist :: Stream Word64- hist = [0] ++ ((2^cnt) * cast string) + hist-- cnt :: Stream Word64- cnt = [0] ++ cnt + 1-- -- Input tokens.- string :: Stream Word8- string = let x = [1,0,0,1,0,1] in - x P.++ x- ++ 0 -- don't care about part of- -- stream after ++-------------------------------------------------------------------------------------languages :: IO ()-languages = do- interpret 20 reAccept - interpret 20 (cfAccept 10)- interpret 20 (csAccept 10)- interpret 20 copyAccept-------------------------------------------------------------------------------------- -- Recognize the language of arbitrarily long sequence of prime numbers.---- -- Sieve of Eratosthenes--- primes :: Word64 -> [Word64]--- primes n = primes' 2 nums---- where --- nums = [2..n] ---- f :: Word64 -> [Word64] -> [Word64]--- f x = L.filter (\a -> P.not (P.rem a x P.== 0 P.&& a P.> x))---- primes' :: Word64 -> [Word64] -> [Word64]--- primes' x ls = let ls' = f x ls in--- -- Can't use rebinded if-the-else syntax--- case ls' P.== ls of--- True -> ls--- False -> primes' (x P.+ 1) ls'---- primesInf :: [Word64]--- primesInf = foldr primes' [2] [3..]---- where ---- -- returns divisors that evenly divide x--- f :: Word64 -> [Word64] -> Bool--- f x ls = ls `seq` (L.or $ map (\a -> P.rem x a P.== 0) ls)--- -- L.filter (\a -> P.rem x a P.== 0)---- primes' :: Word64 -> [Word64] -> [Word64]--- primes' next prms = case prms `seq` f next prms of--- True -> prms `seq` (next:prms)--- False -> prms------ primesAccept :: Word64 -> Spec--- primesAccept n = do--- observer "primes" primesStrm--- observer "accept" accept---- where--- -- Assume we are implementing a Sieve of Eratosthenes--- accept :: Stream Word64--- accept = ---- primesStrm :: Stream Word64--- primesStrm = primes n ++ 0 -- don't care about rest of values after ++
− Examples/Local.hs
@@ -1,43 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Example demonstrating local variables.--module Local ( localEx ) where--import Prelude ()-import Language.Copilot------------------------------------------------------------------------------------nats :: Stream Int32-nats = [0] ++ (1 + nats)--strm :: Stream Int32-strm =- local (nats + 1) $ \nats' -> nats' + nats'---- The above code corresponds to------ strm :: Stream Int32--- strm =--- let x = nats * nats--- in x + x--spec :: Spec-spec = do- trigger "strm" true [arg strm]--- trigger "strm" true [arg $ replStrm 100000]--- trigger "strm" true [arg $ replStrm_ 100000 10000]- -- observer "nats" nats- -- observer "strm" strm------------------------------------------------------------------------------------localEx :: IO ()-localEx = do- interpret 20 spec- prettyPrint spec----------------------------------------------------------------------------------
− Examples/PTLTLExamples.hs
@@ -1,78 +0,0 @@--- | The examples are for testing the ptLTL library--module PTLTLExamples ( ptltlExamples ) where --import Language.Copilot-import Prelude ()-import qualified Data.List as L----- | test of previous-previousTestData :: Stream Bool-previousTestData = [ True, False ] ++ previousTestData--previousTest :: Spec-previousTest = do- observer "previousTest" ( previous previousTestData )----- | test of alwaysBeen-alwaysBeenTestData :: Stream Bool-alwaysBeenTestData = [ True, True, True, True, True, True, True, False ]- ++ alwaysBeenTestData--alwaysBeenTest :: Spec-alwaysBeenTest = do- observer "testAlwaysBeen" ( alwaysBeen alwaysBeenTestData )----- | test of eventuallyPrevious-eventuallyPrevTestData :: Stream Bool-eventuallyPrevTestData = [ False, False, False, False, False, True, False ]- ++ eventuallyPrevTestData--eventuallyPrevTest :: Spec-eventuallyPrevTest = observer "eventuallyPrevTest"- ( eventuallyPrev eventuallyPrevTestData )----- | test of since-sinceTestData1 :: Stream Bool-sinceTestData1 = [ False, False, False ] ++ true--sinceTestData2 :: Stream Bool-sinceTestData2 = [ False, False, True, False, False, False, False ]- ++ sinceTestData2--sinceTest :: Spec-sinceTest = observer "sinceTest"- ( sinceTestData1 `since` sinceTestData2 )----- | test since with external variables-sinceExtTest :: Spec-sinceExtTest = observer "sinceExtTest"- ( extern "e1" (Just e1) `since` extern "e2" (Just e2))---- | external variables-e1, e2 :: [Bool]-e1 = replicate 10 False L.++ repeat True-e2 = replicate 9 False L.++ [ True ] L.++ repeat False--ptltlExamples :: IO ()-ptltlExamples = do- prettyPrint previousTest- interpret 20 previousTest-- prettyPrint alwaysBeenTest- interpret 20 alwaysBeenTest-- prettyPrint eventuallyPrevTest- interpret 20 eventuallyPrevTest-- prettyPrint sinceTest- interpret 20 sinceTest-- prettyPrint sinceExtTest- interpret 20 sinceExtTest-
− Examples/Random.hs
@@ -1,21 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Generate a random spec and pretty-print it.--module Random ( randomEx ) where--import Copilot.Core.PrettyPrint as P-import Copilot.Core.Random (randomSpec)-import Copilot.Core.Random.Weights (simpleWeights)-import System.Random (newStdGen)--randomEx :: IO ()-randomEx = do- g <- newStdGen- let p = randomSpec 10 simpleWeights g -- have to give a dummy number of rounds- -- to simulate to generate a- -- spec---mostly used for- -- interpreting/QuickCheck testing.- putStrLn (P.prettyPrint p)
− Examples/RegExpExamples.hs
@@ -1,49 +0,0 @@--- | Regular expression library tests for the--- copilotRegexp and copilotRegexpB functions--module RegExpExamples ( regExpExamples ) where--import qualified Prelude as P-import Language.Copilot--reset :: Stream Bool-reset = [ False ] ++ cycle [ False, False, False, True ]----- | Regular expression matching on integral streams-s :: Stream Int8-s = extern "e" (Just $ P.cycle [ 0, 1 ])--test1 :: Stream Bool-test1 = copilotRegexp s "(<0>?<0>?<1>)+|<2>?<3>+" reset----- | Regular expressions over boolean streams--s0, s1, s2, s3, s4, s5 :: Stream Bool-s0 = [ True, False, False, False, False, False ] ++ s1-s1 = [ False, True, False, False, False, False ] ++ s2-s2 = [ False, False, True, False, False, False ] ++ s3-s3 = [ False, False, False, True, False, False ] ++ s4-s4 = [ False, False, False, False, True, False ] ++ s5-s5 = [ False, False, False, False, False, True ] ++ s0---test2 :: Stream Bool-test2 = copilotRegexpB- "<s0><s1><s2><s3><s4><s5>(<s0>|<s1>|<s2>|<s3>|<s4>|<s5>)+"- [ ( "s0", s0 )- , ( "s1", s1 )- , ( "s2", s2 )- , ( "s3", s3 )- , ( "s4", s4 )- , ( "s5", s5 ) ] false--spec :: Spec-spec = do- observer "test1" test1- observer "test2" test2- observer "reset" reset--regExpExamples :: IO ()-regExpExamples = interpret 15 spec
− Examples/Sat.hs
@@ -1,67 +0,0 @@--- | Example of a simple SAT solver (simply constructs the truth table) in--- Copilot.---- {-# LANGUAGE RebindableSyntax #-}--module Sat where--import Language.Copilot-import qualified Prelude as P-import Control.Monad (foldM_)--------------------------------------------------------------------------------------- | Number of sat variables and a Boolean function over those variables.-type SatFunc = (Int, [Stream Bool] -> Stream Bool)---- Takes a Sat function and returns the stream of variables and a SAT function.-sat :: SatFunc -> ([Stream Bool], Stream Bool)-sat (i,f) = (xs, res)- where- -- If it becomes true, it stays true.- res = [False] ++ (f xs || res)-- xs = xs' i-- xs' 0 = []- xs' n = clk (period $ 2 P.^ n) (phase (0 :: Int)) : xs' (n P.- 1)--satSpec :: SatFunc -> Spec-satSpec f = do- observer "sat" (snd $ sat f)- observer "done" done- foldM_ mkObs (0 :: Int) xs-- where- xs = fst $ sat f- cnt :: Stream Word64 -- Would need to be extended depending on number of- -- variables.- cnt = [1] ++ cnt + 1- done = cnt == (2 P.^ length xs)- mkObs idx strm = do observer ("obs" P.++ show idx) strm- return (idx P.+ 1)---f0 :: SatFunc---f0 = (3, \[a,b,c] -> a && (b || (not c)))-f0 = (3, f) - where - f [a,b,c] = a && (b || (not c))- f _ = error "Bad SAT function."--f1 :: SatFunc-f1 = (9, f')- where- f' [a,b,c,d,e,f,g,h,i] = - a && b && c && d && e && - f && g && h && i && i && not i- f' _ = error "Bad SAT function."---- | Run the interpreter long enough to get an answer.-runFunc :: SatFunc -> IO ()-runFunc f = interpret (2 P.^ fst f) (satSpec f)--satExamples :: IO ()-satExamples = runFunc f0 >> runFunc f1-----------------------------------------------------------------------------------
− Examples/StackExamples.hs
@@ -1,34 +0,0 @@--- | Stack library tests.--module StackExamples ( stackExamples ) where--import qualified Prelude as P-import Language.Copilot---- push a counter from 1 to 5 onto the stack-pushSignal :: Stream Bool-pushSignal = replicate 5 True ++ false--pushValue :: Stream Word16-pushValue = [ 1 ] ++ pushValue + 1---- then wait one tick and pop 6 values off the stack again--- ( leaving the default/start value )-popSignal :: Stream Bool-popSignal = replicate 6 False P.++ replicate 6 True ++ false---- all operations on a stack of depth 5, of type Word16 and with--- start/default value 0-stackStream :: Stream Word16-stackStream = stack (5::Int) 0 popSignal pushSignal pushValue--stackTest :: Spec-stackTest = - observer "stack" stackStream--stackExamples :: IO ()-stackExamples = do- prettyPrint stackTest- putStrLn ""- putStrLn ""- interpret 15 stackTest
− Examples/StatExamples.hs
@@ -1,41 +0,0 @@-module StatExamples ( statExamples ) where---- | Statistics examples--import Prelude ()-import Language.Copilot--inputData :: Stream Word16-inputData = replicate 5 0 ++ inputData + 5--inputFData :: Stream Float-inputFData = replicate 5 0 ++ inputFData + 5---minV :: Stream Word16-minV = min 3 inputData--maxV :: Stream Word16-maxV = max 3 inputData--sumV :: Stream Word16-sumV = sum 3 inputData--meanV :: Stream Float-meanV = mean 3 inputFData---statisticsTest :: Spec-statisticsTest = do- observer "minV" minV- observer "maxV" maxV- observer "sumV" sumV- observer "meanV" meanV---statExamples :: IO ()-statExamples = do- prettyPrint statisticsTest- putStrLn ""- putStrLn ""- interpret 20 statisticsTest
+ Examples/Struct.hs view
@@ -0,0 +1,45 @@+--------------------------------------------------------------------------------+-- Copyright © 2019 National Institute of Aerospace / Galois, Inc.+--------------------------------------------------------------------------------++-- Example showing the use of structs with a vector datatype.++{-# LANGUAGE DataKinds #-}++module Struct where++import Language.Copilot+import Copilot.Compile.C99++import Prelude hiding ((>), (<), div, (++))+++data Vec = Vec+ { x :: Field "x" Float+ , y :: Field "y" Float+ }++instance Struct Vec where+ typename _ = "vec" -- Name of the type in C++ -- Function to translate Vec to list of Value's, order should match struct.+ toValues v = [ Value Float (x v)+ , Value Float (y v)+ ]++-- We need to provide an instance to Typed with a bogus Vec+instance Typed Vec where+ typeOf = Struct (Vec (Field 0) (Field 0))+++vecs :: Stream Vec+vecs = [ Vec (Field 1) (Field 2)+ , Vec (Field 12) (Field 8)+ ] ++ vecs+++spec = do+ -- Trigger that always executes, splits the vec into seperate args.+ trigger "split" true [arg $ vecs # x, arg $ vecs # y]++main = reify spec >>= compile "struct"
− Examples/Test.hs
@@ -1,176 +0,0 @@------------------------------------------------------------------------------------ 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, unless)-import Data.Maybe (catMaybes)--import AddMult-import Array---import BadExtVars-import Cast-import ClockExamples-import EngineExample-import Examples-import Examples2-import ExtFuns-import Languages-import Local-import LTLExamples-import PTLTLExamples-import Random-import RegExpExamples-import Sat-import StackExamples-import StatExamples-import VotingExamples-------------------------------------------------------------------------------------main :: IO ()-main = do- ls <- checkExists- when (null ls) runTests- unless (null ls) $ do putStrLn "*** Warning! ***"- putStrLn "Cannot run tests in this directory. You have the following files or directories that would be deleted: "- mapM_ putStrLn ls- -runTests :: IO ()-runTests = 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 language ..."- languages >> 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 satExamples ..."- satExamples >> 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 "************************************"------------------------------------------------------------------------------------cbmcName :: String-cbmcName = "cbmc_driver.c"--exam2Name :: String-exam2Name = "secondexamplespec_copilot-sbv-codegen"--examsbvName :: String-examsbvName = "externFunSpec_copilot-sbv-codegen"---atomCBMC :: String-atomCBMC = M.appendPrefix M.atomPrefix C99.c99DirName--sbvCBMC :: String-sbvCBMC = M.appendPrefix M.sbvPrefix SBV.sbvDirName------------------------------------------------------------------------------------checkExists :: IO [String]-checkExists = do- b0 <- nmBool doesDirectoryExist SBV.sbvDirName- b1 <- nmBool doesDirectoryExist C99.c99DirName- b2 <- nmBool doesFileExist cbmcName- b3 <- nmBool doesDirectoryExist atomCBMC- b4 <- nmBool doesDirectoryExist sbvCBMC- return $ catMaybes $ map getName [b0, b1, b2, b3, b4]-- where- getName (nm, bool) = if bool then Just nm else Nothing- nmBool f nm = do b <- f nm - return (nm, b)------------------------------------------------------------------------------------cleanup :: IO ()-cleanup = do-- b0 <- doesDirectoryExist SBV.sbvDirName- when b0 (removeDirectoryRecursive SBV.sbvDirName)-- b1 <- doesDirectoryExist C99.c99DirName- when b1 (removeDirectoryRecursive C99.c99DirName)-- b2 <- doesFileExist cbmcName- when b2 (removeFile cbmcName)-- b3 <- doesDirectoryExist atomCBMC- when b3 (removeDirectoryRecursive atomCBMC)-- b4 <- doesDirectoryExist sbvCBMC- when b4 (removeDirectoryRecursive sbvCBMC)-- b5 <- doesDirectoryExist exam2Name- when b5 (removeDirectoryRecursive exam2Name)- -- b6 <- doesDirectoryExist examsbvName- when b6 (removeDirectoryRecursive examsbvName)----------------------------------------------------------------------------------
− Examples/VotingExamples.hs
@@ -1,61 +0,0 @@------------------------------------------------------------------------------------ Copyright © 2011 National Institute of Aerospace / Galois, Inc.------------------------------------------------------------------------------------- | Fault-tolerant voting examples.--{-# LANGUAGE RebindableSyntax #-}--module VotingExamples ( votingExamples ) where--import Language.Copilot------------------------------------------------------------------------------------vote :: Spec-vote = do - trigger "maj" true [ arg maj ]-- trigger "aMaj" true - [ arg $ aMajority xs maj ]-- where-- maj = majority xs- xs = concat (replicate 1 ls)- ls = [a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z]-- a = [0] ++ a + 1 :: Stream Word32- b = [0] ++ b + 1- c = [0] ++ c + 1- d = [0] ++ d + 1- e = [1] ++ e + 1- f = [1] ++ f + 1- g = [1] ++ g + 1- h = [1] ++ h + 1- i = [1] ++ i + 1- j = [1] ++ j + 1- k = [1] ++ k + 1- l = [1] ++ l + 1- m = [1] ++ m + 1- n = [1] ++ n + 1- o = [1] ++ o + 1- p = [1] ++ p + 1- q = [1] ++ q + 1- r = [1] ++ r + 1- s = [1] ++ s + 1- t = [1] ++ t + 1- u = [1] ++ u + 1- v = [1] ++ v + 1- w = [1] ++ w + 1- x = [1] ++ x + 1- y = [1] ++ y + 1- z = [1] ++ z + 1------------------------------------------------------------------------------------votingExamples :: IO ()-votingExamples =- do- interpret 20 vote--- prettyPrint vote
README.md view
@@ -1,106 +1,144 @@+# Copilot: Stream DSL for hard real-time runtime verification+ [](https://travis-ci.org/Copilot-Language/Copilot)+[](https://hackage.haskell.org/package/copilot) -Copilot: a stream DSL-====================================-Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in-Haskell that compiles into embedded C. Copilot is similar in spirit to-languages like Lustre. Copilot contains an interpreter, multiple back-end-compilers, and other verification tools.+Copilot is a runtime verification framework written in Haskell. It allows the+user to write programs in a simple but powerful way using a stream-based+approach. -Resources-=========-Copilot is comprised of a number of sub-projects which are automatically-installed when you install Copilot from Hackage, as described below. (These are-tracked as Git submodules in Copilot.)+Programs can be interpreted for testing, or translated C99 code to be+incorporated in a project, or as a standalone application. The C99 backend+output is constant in memory and time, making it suitable for systems with hard+realtime requirements. -* [copilot-language](http://hackage.haskell.org/package/copilot-language) The- front-end of Copilot defining the user language. -* [copilot-libraries](http://hackage.haskell.org/package/copilot-libraries)- User-supplied libraries for Copilot, including linear-temporal logic,- fault-tolerant voting, regular expressions, etc.+## Installation+There are two ways to install Copilot: -* [copilot-core](http://hackage.haskell.org/package/copilot-core) The core- language, which efficiently represents Copilot expressions. The core is only- of interest to implementers wishing to add a new back-end to Copilot.+* From Hackage (recommended): -* [copilot-cbmc](http://hackage.haskell.org/package/copilot-cbmc) A tool to- generate a driver using CBMC, a third-party tool (see Dependencies below) that- proves that the code generated by different C back-ends is equivalent.- Currently, this includes the C99 back-end and the SBV back-end.+ The Copilot library is cabalized. Assuming you have cabal, the GHC+ compiler installed (the+ [Haskell Platform](http://hackage.haskell.org/platform/) is the easiest way+ to obtain these), and an Internet connection, it should merely be a matter of running: -* [copilot-c99](http://hackage.haskell.org/package/copilot-c99) A back-end that- translates to [Atom](http://hackage.haskell.org/package/atom) to- generate hard real-time C code.+ cabal install copilot -Optionally, you may which also to install+* Building from source from the GitHub repositories (typically, one would only+ go this route to develop Copilot): -* [copilot-sbv](http://hackage.haskell.org/package/copilot-sbv) Another back-end- that translates to [SBV](http://hackage.haskell.org/package/sbv), using its- code generator to generate hard real-time C code as well. The ad+ git clone https://github.com/Copilot-Language/Copilot.git+ cd Copilot+ git submodule update --init --remote+ make -* [copilot-discussion](https://github.com/Copilot-Language/copilot-discussion)- Contains a tutorial, todos, and other items regarding the Copilot system.+Note there is a TravisCI build (linked to at the top of this README) if you+have trouble building/installing. -**Sources** for each package are available on Github as well. Just go to-[Github](github.com) and search for the package of interest. Feel free to fork! -Comments, bug reports, and patches are always welcome. Send them to leepike @-gmail.com+## Example+Here follows a simple example of a heating system. Other examples can be found+in the [Examples+directory](https://github.com/Copilot-Language/Copilot/tree/master/Examples)+of the main repository. -Examples-=========-Please see the files under the Examples directory for a number of examples-showing the syntax, use of libraries, and use of the interpreter and back-ends.-The examples is the best way to start.+ -- This is a simple example with basic usage. It implements a simple home+ -- heating system: It heats when temp gets too low, and stops when it is high+ -- enough. It read temperature as an byte (range -50C to 100C) and translates+ -- this to Celcius. -Installation-============+ module Heater where -* From Hackage:+ import Language.Copilot+ import Copilot.Compile.C99 - The Copilot library is cabalized. Assuming you have cabal and the GHC compiler- installed (the [Haskell Platform](http://hackage.haskell.org/platform/) is the- easiest way to obtain these), it should merely be a matter of running+ import Prelude hiding ((>), (<), div) - cabal install copilot+ -- External temperature as a byte, range of -50C to 100C+ temp :: Stream Int8+ temp = extern "temperature" Nothing - with an Internet connection. Please see the INSTALL file for installation- details.+ -- Calculate temperature in Celcius.+ -- We need to cast the Int8 to a Float. Note that it is an unsafeCast, as there+ -- is no direct relation between Int8 and Float.+ ctemp :: Stream Float+ ctemp = ((unsafeCast temp) / 150.0) - 50.0 -* From GitHub:+ spec = do+ -- Triggers that fire when the ctemp is too low or too hight,+ -- pass the current ctemp as an argument.+ trigger "heaton" (ctemp < 18.0) [arg ctemp]+ trigger "heafoff" (ctemp > 21.0) [arg ctemp] - git clone https://github.com/Copilot-Language/Copilot.git- git submodule update --init- make test+ -- Compile the spec+ main = reify spec >>= compile "heater" -Once the installation is done, you can run the executable `XXX` which will-execute the regression test suite for sbv on your machine. -Note there is a TravisCI build (linked to at the top of this README) if you have-trouble building/installing.+## Contributions+Feel free to open new issues and send pull requests. -Dependencies-=============-copilot-cbmc depends on the C model-checker, CBMC.-[CBMC](http://www.cprover.org/cbmc/) is a bounded model-checker for C code. We-use CBMC to prove that two back-ends generating C generate semantically-equivalent C, to help detect bugs in C back-ends.+In order to contribute to Copilot, please use the following steps which will+make the process of evaluating and including your changes much easier: -For compiling it with CompCert (activated by default for SBV backend), you need-to install it, with its Standard C library ( http://compcert.inria.fr/ ).+* Create an issue for every individual change or problem with Copilot. Document+ the issue well. -Copyright, License-==================-Copilot is distributed with the BSD3 license. The license file contains the-[BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.+* Always comment on the issues you are addressing in every commit. Be+ descriptive, and use the syntax `#<issue_number>` so that we can track+ changes and issues easily. -Thanks-======-Copilot was developed, in part, with support from NASA's Aviation Safety-Program, Contract #NNL08AD13T. Copilot was developed jointly by Galois,-Inc. and the National Institute of Aerospace.+* Every commit should mention one issue and, ideally, only one. -The following people have contributed to Copilot: Lee Pike, Nis Wegmann,-Sebastian Niller, Robin Morisset, Alwyn Goodloe, and Levent Erkok.+* Do not send a PR or commit that addresses multiple problems, unless they are+ related and cannot be separated. +* Do not commit to master directly, except for branch merges. Make sure you+ always merge onto master using `--no-ff` so that we can tell that features+ were addressed separately, completed, tested, and then merged. If you are a+ Copilot developer, create a branch for every issue you are addressing, complete+ it, and then merge onto master. Document every commit in every branch,+ including the last merge commit, stating the issues it addresses or closes.++This process is similar to [Git+Flow](http://nvie.com/posts/a-successful-git-branching-model/). The equivalent+of Git Flow's master branch is our latest tag, and the equivalent of Git Flow's+develop branch is our master.+++## Further information+For further information, including documentation and a tutorial, please visit+the Copilot website:+[https://copilot-language.github.io](https://copilot-language.github.io).+++## Acknowledgements+We are grateful for NASA Contract NNL08AD13T to Galois, Inc. and the National+Institute of Aerospace, which partially supported this work.+++## License+Copilot is distributed under the BSD-3-Clause license, which can be found+[here](https://raw.githubusercontent.com/Copilot-Language/Copilot/master/LICENSE).+++## The Copilot Team+The development of Copilot spans across several years. During these years+the following people have helped develop Copilot (in no particular order):++* Lee Pike+* Alwyn Goodloe (maintainer)+* Robin Morisset+* Levent Erkők+* Sebastian Niller+* Nis Wegmann+* Chris Hathhorn+* Eli Mendelson+* Jonathan Laurent+* Laura Titolo+* Georges-Axel Jolayan+* Macallan Cruff+* Ryan Spring+* Lauren Pick+* Frank Dedden (maintainer: contact at dev@dedden.net)+* Ivan Perez
copilot.cabal view
@@ -1,14 +1,14 @@ name: copilot-version: 2.2.1+version: 3.0 cabal-version: >= 1.10 license: BSD3 license-file: LICENSE-author: Nis Nordby Wegmann, Lee Pike, Robin Morisset, Sebastian Niller, Alwyn Goodloe+author: Frank Dedden, Nis Nordby Wegmann, Lee Pike, Robin Morisset, Sebastian Niller, Alwyn Goodloe synopsis: A stream DSL for writing embedded C programs. build-type: Simple-maintainer: Lee Pike <leepike@galois.com>+maintainer: Frank Dedden <dev@dedden.net> category: Language, Embedded-homepage: http://leepike.github.com/Copilot/+homepage: https://copilot-language.github.io stability: Experimental description: This package is the main entry-point for using Copilot.@@ -17,15 +17,19 @@ Haskell that compiles into embedded C. Copilot contains an interpreter, multiple back-end compilers, and other verification tools. A tutorial, bug reports, and todos are available at- <https://github.com/leepike/copilot-discussion>.+ <https://github.com/Copilot-Language/copilot-discussion>. .- Examples are available at <https://github.com/leepike/Copilot/tree/master/Examples>.+ Examples are available at <https://github.com/Copilot-Language/Copilot/tree/master/Examples>. -extra-source-files: README.md+extra-source-files: + README.md+ Examples/Heater.hs+ Examples/Array.hs+ Examples/Struct.hs source-repository head type: git- location: git://github.com/leepike/Copilot.git+ location: https://github.com/Copilot-Language/Copilot.git library hs-source-dirs: src@@ -33,53 +37,18 @@ ghc-options: -Wall -fwarn-tabs- -auto-all- -caf-all -fno-warn-orphans build-depends:- base >= 4.0 && < 5- , copilot-core >= 2.2.1- , copilot-theorem >= 2.2.1- , copilot-language >= 2.2.1- , copilot-libraries >= 2.2.1- , copilot-sbv >= 2.2.1- , copilot-cbmc >= 2.2.1- , copilot-c99 >= 2.2.1+ base >= 4.9 && < 5+ , optparse-applicative >= 0.14 && < 0.15+ , directory >= 1.3 && < 1.4+ , filepath >= 1.4 && < 1.5 - exposed-modules: Language.Copilot+ , copilot-core >= 3.0 && < 3.1+ , copilot-theorem >= 3.0 && < 3.1+ , copilot-language >= 3.0 && < 3.1+ , copilot-libraries >= 3.0 && < 3.1+ , copilot-c99 >= 3.0 && < 3.1 -executable copilot-regression- default-language : Haskell2010- hs-source-dirs : Examples, src- ghc-options : -Wall -fwarn-tabs- main-is : Test.hs- build-depends:- base >= 4.0 && < 5- , copilot-core >= 2.2.1- , copilot-theorem >= 2.2.1- , copilot-language >= 2.2.1- , copilot-libraries >= 2.2.1- , copilot-sbv >= 2.2.1- , copilot-cbmc >= 2.2.1- , copilot-c99 >= 2.2.1- , directory >= 1.2.1- , random- other-modules: AddMult- , Array- , Cast- , ClockExamples- , EngineExample- , Examples- , Examples2- , ExtFuns- , Languages- , Local- , LTLExamples- , PTLTLExamples- , Random- , RegExpExamples- , Sat- , StackExamples- , StatExamples- , VotingExamples + exposed-modules: Language.Copilot, Language.Copilot.Main
src/Language/Copilot.hs view
@@ -17,6 +17,9 @@ -- , module Copilot.Library.Utils -- , module Copilot.Library.Voting -- , module Copilot.Library.Stacks++ , copilotMain+ , defaultMain ) where import Copilot.Language@@ -38,3 +41,4 @@ -- import Copilot.Library.Voting -- import Copilot.Library.Stacks +import Language.Copilot.Main
+ src/Language/Copilot/Main.hs view
@@ -0,0 +1,53 @@+module Language.Copilot.Main ( copilotMain, defaultMain ) where++import qualified Copilot.Core as C (Spec)+import Copilot.Language (interpret, prettyPrint)+import Copilot.Language.Reify (reify)+import Copilot.Language (Spec)++import Options.Applicative+import Data.Semigroup ((<>))+import Control.Monad (when)+++type Interpreter = Integer -> Spec -> IO ()+type Compiler = FilePath -> C.Spec -> IO ()+type Printer = Spec -> IO ()+++data CmdArgs = CmdArgs+ { aoutput :: String+ , acompile :: Bool+ , apretty :: Bool+ , ainterpret :: Int+ }++cmdargs :: Parser CmdArgs+cmdargs = CmdArgs+ <$> strOption (long "output" <> short 'o' <> value "."+ <> help "Output directory of C files")+ <*> switch (long "justrun" <> short 'c'+ <> help "Do NOT produce *.c and *.h files as output")+ <*> switch (long "print" <> short 'p'+ <> help "Pretty print the specification")+ <*> option auto (long "interpret" <> short 'i' <> value 0+ <> metavar "INT" <> showDefault+ <> help "Interpret specification and write result to output")+++copilotMain :: Interpreter -> Printer -> Compiler -> Spec -> IO ()+copilotMain interp pretty comp spec = main =<< execParser opts where+ opts = info (cmdargs <**> helper) fullDesc++ main :: CmdArgs -> IO ()+ main args = do+ let iters = ainterpret args+ when (apretty args) $ pretty spec+ when (iters Prelude.> 0) $ interp (fromIntegral iters) spec++ when (not $ acompile args) $ do+ spec' <- reify spec+ comp (aoutput args) spec'++defaultMain :: Compiler -> Spec -> IO ()+defaultMain = copilotMain interpret prettyPrint