diff --git a/Examples/AddMult.hs b/Examples/AddMult.hs deleted file mode 100644 --- a/Examples/AddMult.hs +++ /dev/null @@ -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 - - --------------------------------------------------------------------------------- diff --git a/Examples/Array.hs b/Examples/Array.hs --- a/Examples/Array.hs +++ b/Examples/Array.hs @@ -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" diff --git a/Examples/Cast.hs b/Examples/Cast.hs deleted file mode 100644 --- a/Examples/Cast.hs +++ /dev/null @@ -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 diff --git a/Examples/ClockExamples.hs b/Examples/ClockExamples.hs deleted file mode 100644 --- a/Examples/ClockExamples.hs +++ /dev/null @@ -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 diff --git a/Examples/EngineExample.hs b/Examples/EngineExample.hs deleted file mode 100644 --- a/Examples/EngineExample.hs +++ /dev/null @@ -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" }) - - diff --git a/Examples/Examples.hs b/Examples/Examples.hs deleted file mode 100644 --- a/Examples/Examples.hs +++ /dev/null @@ -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) --------------------------------------------------------------------------------- diff --git a/Examples/Examples2.hs b/Examples/Examples2.hs deleted file mode 100644 --- a/Examples/Examples2.hs +++ /dev/null @@ -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" }) diff --git a/Examples/ExtFuns.hs b/Examples/ExtFuns.hs deleted file mode 100644 --- a/Examples/ExtFuns.hs +++ /dev/null @@ -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" }) - - --------------------------------------------------------------------------------- diff --git a/Examples/Heater.hs b/Examples/Heater.hs new file mode 100644 --- /dev/null +++ b/Examples/Heater.hs @@ -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" diff --git a/Examples/LTLExamples.hs b/Examples/LTLExamples.hs deleted file mode 100644 --- a/Examples/LTLExamples.hs +++ /dev/null @@ -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 diff --git a/Examples/Languages.hs b/Examples/Languages.hs deleted file mode 100644 --- a/Examples/Languages.hs +++ /dev/null @@ -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" . - -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 ++ diff --git a/Examples/Local.hs b/Examples/Local.hs deleted file mode 100644 --- a/Examples/Local.hs +++ /dev/null @@ -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 - --------------------------------------------------------------------------------- diff --git a/Examples/PTLTLExamples.hs b/Examples/PTLTLExamples.hs deleted file mode 100644 --- a/Examples/PTLTLExamples.hs +++ /dev/null @@ -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 - diff --git a/Examples/Random.hs b/Examples/Random.hs deleted file mode 100644 --- a/Examples/Random.hs +++ /dev/null @@ -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) diff --git a/Examples/RegExpExamples.hs b/Examples/RegExpExamples.hs deleted file mode 100644 --- a/Examples/RegExpExamples.hs +++ /dev/null @@ -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", 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 diff --git a/Examples/Sat.hs b/Examples/Sat.hs deleted file mode 100644 --- a/Examples/Sat.hs +++ /dev/null @@ -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 - ---------------------------------------------------------------------------------- diff --git a/Examples/StackExamples.hs b/Examples/StackExamples.hs deleted file mode 100644 --- a/Examples/StackExamples.hs +++ /dev/null @@ -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 diff --git a/Examples/StatExamples.hs b/Examples/StatExamples.hs deleted file mode 100644 --- a/Examples/StatExamples.hs +++ /dev/null @@ -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 diff --git a/Examples/Struct.hs b/Examples/Struct.hs new file mode 100644 --- /dev/null +++ b/Examples/Struct.hs @@ -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" diff --git a/Examples/Test.hs b/Examples/Test.hs deleted file mode 100644 --- a/Examples/Test.hs +++ /dev/null @@ -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) - --------------------------------------------------------------------------------- diff --git a/Examples/VotingExamples.hs b/Examples/VotingExamples.hs deleted file mode 100644 --- a/Examples/VotingExamples.hs +++ /dev/null @@ -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 diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,106 +1,144 @@ +# Copilot: Stream DSL for hard real-time runtime verification + [![Build Status](https://travis-ci.org/Copilot-Language/Copilot.svg?branch=master)](https://travis-ci.org/Copilot-Language/Copilot) +[![Version on Hackage](https://img.shields.io/hackage/v/copilot.svg)](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 `#` 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 diff --git a/copilot.cabal b/copilot.cabal --- a/copilot.cabal +++ b/copilot.cabal @@ -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 +maintainer: Frank Dedden 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 - . + . . - Examples are available at . + Examples are available at . -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 diff --git a/src/Language/Copilot.hs b/src/Language/Copilot.hs --- a/src/Language/Copilot.hs +++ b/src/Language/Copilot.hs @@ -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 diff --git a/src/Language/Copilot/Main.hs b/src/Language/Copilot/Main.hs new file mode 100644 --- /dev/null +++ b/src/Language/Copilot/Main.hs @@ -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