copilot-interpreter (empty) → 3.11
raw patch · 12 files changed
+1563/−0 lines, 12 filesdep +QuickCheckdep +basedep +copilot-coresetup-changed
Dependencies added: QuickCheck, base, copilot-core, copilot-interpreter, pretty, test-framework, test-framework-quickcheck2
Files
- CHANGELOG +3/−0
- LICENSE +29/−0
- README.md +30/−0
- Setup.hs +2/−0
- copilot-interpreter.cabal +87/−0
- src/Copilot/Interpret.hs +29/−0
- src/Copilot/Interpret/Error.hs +12/−0
- src/Copilot/Interpret/Eval.hs +396/−0
- src/Copilot/Interpret/Render.hs +122/−0
- tests/Main.hs +18/−0
- tests/Test/Copilot/Interpret/Eval.hs +804/−0
- tests/Test/Extra.hs +31/−0
+ CHANGELOG view
@@ -0,0 +1,3 @@+2022-09-07+ * Version bump (3.11). (#376)+ * Split copilot-interpreter into separate library. (#361)
+ LICENSE view
@@ -0,0 +1,29 @@+2009+BSD3 License terms++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++Redistributions of source code must retain the above copyright+notice, this list of conditions and the following disclaimer.++Redistributions in binary form must reproduce the above copyright+notice, this list of conditions and the following disclaimer in the+documentation and/or other materials provided with the distribution.++Neither the name of the developers nor the names of its contributors+may be used to endorse or promote products derived from this software+without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,30 @@+[](https://app.travis-ci.com/github/Copilot-Language/copilot)++# Copilot: a stream DSL+The interpreter, which evaluates Copilot specifications and prints+their results over time.++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.++Programs can be interpreted for testing (with the library copilot-interpreter),+or translated C99 code to be incorporated in a project, or as a standalone+application. The C99 backend ensures us that the output is constant in memory+and time, making it suitable for systems with hard realtime requirements.++## Installation+Copilot-interpreter can be found on+[Hackage](https://hackage.haskell.org/package/copilot-interpreter). It is typically+only installed as part of the complete Copilot distribution. For installation+instructions, please refer to the [Copilot+website](https://copilot-language.github.io).++## Further information+For further information, install instructions and documentation, please visit+the Copilot website:+[https://copilot-language.github.io](https://copilot-language.github.io)++## License+Copilot is distributed under the BSD-3-Clause license, which can be found+[here](https://raw.githubusercontent.com/Copilot-Language/copilot/master/copilot-interpreter/LICENSE).
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ copilot-interpreter.cabal view
@@ -0,0 +1,87 @@+cabal-version: >=1.10+name: copilot-interpreter+version: 3.11+synopsis: Interpreter for Copilot.+description:+ Interpreter for Copilot.+ .+ Copilot is a stream (i.e., infinite lists) domain-specific language (DSL) in+ Haskell that compiles into embedded C. Copilot contains an interpreter,+ multiple back-end compilers, and other verification tools.+ .+ A tutorial, examples, and other information are available at+ <https://copilot-language.github.io>.++author: Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe,+ Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez+license: BSD3+license-file: LICENSE+maintainer: Ivan Perez <ivan.perezdominguez@nasa.gov>+homepage: https://copilot-language.github.io+bug-reports: https://github.com/Copilot-Language/copilot/issues+stability: Experimental+category: Language, Embedded+build-type: Simple+extra-source-files: README.md, CHANGELOG++x-curation: uncurated++source-repository head+ type: git+ location: https://github.com/Copilot-Language/copilot.git+ subdir: copilot-interpreter++library++ default-language: Haskell2010++ hs-source-dirs: src++ ghc-options:+ -Wall++ build-depends:+ base >= 4.9 && < 5,+ pretty >= 1.0 && < 1.2,++ copilot-core++ exposed-modules:++ Copilot.Interpret+ Copilot.Interpret.Eval++ other-modules:++ Copilot.Interpret.Error+ Copilot.Interpret.Render++test-suite unit-tests+ type:+ exitcode-stdio-1.0++ main-is:+ Main.hs++ other-modules:+ Test.Extra+ Test.Copilot.Interpret.Eval++ build-depends:+ base+ , QuickCheck+ , pretty+ , test-framework+ , test-framework-quickcheck2++ , copilot-core+ , copilot-interpreter++ hs-source-dirs:+ tests++ default-language:+ Haskell2010++ ghc-options:+ -Wall
+ src/Copilot/Interpret.hs view
@@ -0,0 +1,29 @@+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.++-- | An interpreter for Copilot specifications.++{-# LANGUAGE Safe #-}++module Copilot.Interpret+ ( Format (..)+ , interpret+ ) where++import Copilot.Core+import Copilot.Interpret.Eval+import Copilot.Interpret.Render++-- | Output format for the results of a Copilot spec interpretation.+data Format = Table | CSV++-- | Interpret a Copilot specification.+interpret :: Format -- ^ Format to be used for the output.+ -> Int -- ^ Number of steps to interpret.+ -> Spec -- ^ Specification to interpret.+ -> String+interpret format k spec =+ case format of+ Table -> renderAsTable e+ CSV -> renderAsCSV e+ where+ e = eval Haskell k spec
+ src/Copilot/Interpret/Error.hs view
@@ -0,0 +1,12 @@+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.++{-# LANGUAGE Safe #-}++-- | Custom functions to report error messages to users.+module Copilot.Interpret.Error+ ( badUsage ) where++-- | Report an error due to an error detected by Copilot (e.g., user error).+badUsage :: String -- ^ Description of the error.+ -> a+badUsage msg = error $ "Copilot error: " ++ msg
+ src/Copilot/Interpret/Eval.hs view
@@ -0,0 +1,396 @@+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.++-- | A tagless interpreter for Copilot specifications.++{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE Safe #-}++module Copilot.Interpret.Eval+ ( Env+ , Output+ , ExecTrace (..)+ , eval+ , ShowType (..)+ ) where++import Copilot.Core (Expr (..), Field (..), Id, Name, Observer (..),+ Op1 (..), Op2 (..), Op3 (..), Spec, Stream (..),+ Trigger (..), Type (..), UExpr (..), arrayelems,+ specObservers, specStreams, specTriggers)+import Copilot.Interpret.Error (badUsage)++import Prelude hiding (id)+import qualified Prelude as P++import Control.Exception (Exception, throw)+import Data.Bits (complement, shiftL, shiftR, xor, (.&.), (.|.))+import Data.Dynamic (Dynamic, fromDynamic, toDyn)+import Data.List (transpose)+import Data.Maybe (fromJust)+import Data.Typeable (Typeable)++-- | Exceptions that may be thrown during interpretation of a Copilot+-- specification.+data InterpException+ = ArrayWrongSize Name Int -- ^ Extern array has incorrect size.+ | ArrayIdxOutofBounds Name Int Int -- ^ Index out-of-bounds exception.+ | DivideByZero -- ^ Division by zero.+ | NotEnoughValues Name Int -- ^ For one or more streams, not enough+ -- values are available to simulate the+ -- number of steps requested.+ | NoExtsInterp Name -- ^ One of the externs used by the+ -- specification does not declare+ -- sample values to be used during+ -- simulation.+ deriving Typeable++-- | Show a descriptive message of the exception.+instance Show InterpException where+ ---------------------------------------+ show (ArrayWrongSize name expectedSize) =+ badUsage $ "in the environment for external array " ++ name+ ++ ", we expect a list of length " ++ show expectedSize+ ++ ", but the length of the array you supplied is of a different length."+ ---------------------------------------+ show (ArrayIdxOutofBounds name index size) =+ badUsage $ "in the environment for external array " ++ name+ ++ ", you gave an index of " ++ show index+ ++ " where the size of the array is " ++ show size ++ "; the size must "+ ++ " be strictly greater than the index."+ ---------------------------------------+ show DivideByZero =+ badUsage "divide by zero."+ ---------------------------------------+ show (NotEnoughValues name k) =+ badUsage $ "on the " ++ show k ++ "th iteration, we ran out of "+ ++ "values for simulating the external element " ++ name ++ "."+ ---------------------------------------+ show (NoExtsInterp name) =+ badUsage $ "in a call of external symbol " ++ name ++ ", you did not "+ ++ "provide an expression for interpretation. In your external "+ ++ "declaration, you need to provide a 'Just strm', where 'strm' is "+ ++ "some stream with which to simulate the function."+ ---------------------------------------++-- | Allow throwing and catching 'InterpException' using Haskell's standard+-- exception mechanisms.+instance Exception InterpException++-- | An environment that contains an association between (stream or extern)+-- names and their values.+type Env nm = [(nm, Dynamic)]++-- | The simulation output is defined as a string. Different backends may+-- choose to format their results differently.+type Output = String++-- | An execution trace, containing the traces associated to each individual+-- monitor trigger and observer.+data ExecTrace = ExecTrace+ { interpTriggers :: [(String, [Maybe [Output]])]++ -- ^ Map from trigger names to their optional output, which is a list of+ -- strings representing their values. The output may be 'Nothing' if the+ -- guard for the trigger was false. The order is important, since we+ -- compare the arg lists between the interpreter and backends.++ , interpObservers :: [(String, [Output])]+ -- ^ Map from observer names to their outputs.+ }+ deriving Show++-- We could write this in a beautiful lazy style like above, but that creates a+-- space leak in the interpreter that is hard to fix while maintaining laziness.+-- We take a more brute-force appraoch below.++-- | Evaluate a specification for a number of steps.+eval :: ShowType -- ^ Show booleans as @0@\/@1@ (C) or @True@\/@False@+ -- (Haskell).+ -> Int -- ^ Number of steps to evaluate.+ -> Spec -- ^ Specification to evaluate.+ -> ExecTrace+eval showType k spec =++ let initStrms = map initStrm (specStreams spec) in++ let strms = evalStreams k (specStreams spec) initStrms in++ let trigs = map (evalTrigger showType k strms)+ (specTriggers spec) in++ let obsvs = map (evalObserver showType k strms)+ (specObservers spec) in++ strms `seq` ExecTrace+ { interpTriggers =+ zip (map triggerName (specTriggers spec)) trigs+ , interpObservers =+ zip (map observerName (specObservers spec)) obsvs+ }++-- | An environment that contains an association between (stream or extern)+-- names and their values.+type LocalEnv = [(Name, Dynamic)]++-- | Evaluate an expression for a number of steps, obtaining the value+-- of the sample at that time.+evalExpr_ :: Typeable a => Int -> Expr a -> LocalEnv -> Env Id -> a+evalExpr_ k e0 locs strms = case e0 of+ Const _ x -> x+ Drop t i id ->+ let Just buff = lookup id strms >>= fromDynamic in+ reverse buff !! (fromIntegral i + k)+ Local t1 _ name e1 e2 ->+ let x = evalExpr_ k e1 locs strms in+ let locs' = (name, toDyn x) : locs in+ x `seq` locs' `seq` evalExpr_ k e2 locs' strms+ Var t name -> fromJust $ lookup name locs >>= fromDynamic+ ExternVar _ name xs -> evalExternVar k name xs+ Op1 op e1 ->+ let ev1 = evalExpr_ k e1 locs strms in+ let op1 = evalOp1 op in+ ev1 `seq` op1 `seq` op1 ev1+ Op2 op e1 e2 ->+ let ev1 = evalExpr_ k e1 locs strms in+ let ev2 = evalExpr_ k e2 locs strms in+ let op2 = evalOp2 op in+ ev1 `seq` ev2 `seq` op2 `seq` op2 ev1 ev2+ Op3 op e1 e2 e3 ->+ let ev1 = evalExpr_ k e1 locs strms in+ let ev2 = evalExpr_ k e2 locs strms in+ let ev3 = evalExpr_ k e3 locs strms in+ let op3 = evalOp3 op in+ ev1 `seq` ev2 `seq` ev3 `seq` op3 `seq` op3 ev1 ev2 ev3+ Label _ _ e1 ->+ let ev1 = evalExpr_ k e1 locs strms in+ ev1++-- | Evaluate an extern stream for a number of steps, obtaining the value of+-- the sample at that time.+evalExternVar :: Int -> Name -> Maybe [a] -> a+evalExternVar k name exts =+ case exts of+ Nothing -> throw (NoExtsInterp name)+ Just xs ->+ case safeIndex k xs of+ Nothing -> throw (NotEnoughValues name k)+ Just x -> x++-- | Evaluate an 'Copilot.Core.Operators.Op1' by producing an equivalent+-- Haskell function operating on the same types as the+-- 'Copilot.Core.Operators.Op1'.+evalOp1 :: Op1 a b -> (a -> b)+evalOp1 op = case op of+ Not -> P.not+ Abs _ -> P.abs+ Sign _ -> P.signum+ Recip _ -> P.recip+ Exp _ -> P.exp+ Sqrt _ -> P.sqrt+ Log _ -> P.log+ Sin _ -> P.sin+ Tan _ -> P.tan+ Cos _ -> P.cos+ Asin _ -> P.asin+ Atan _ -> P.atan+ Acos _ -> P.acos+ Sinh _ -> P.sinh+ Tanh _ -> P.tanh+ Cosh _ -> P.cosh+ Asinh _ -> P.asinh+ Atanh _ -> P.atanh+ Acosh _ -> P.acosh+ Ceiling _ -> P.fromIntegral . idI . P.ceiling+ Floor _ -> P.fromIntegral . idI . P.floor+ BwNot _ -> complement+ Cast _ _ -> P.fromIntegral+ GetField (Struct _) _ f -> unfield . f+ where+ -- Used to help GHC pick a return type for ceiling/floor+ idI :: Integer -> Integer+ idI = P.id++ -- Extract value from field+ unfield (Field v) = v++-- | Evaluate an 'Copilot.Core.Operators.Op2' by producing an equivalent+-- Haskell function operating on the same types as the+-- 'Copilot.Core.Operators.Op2'.+evalOp2 :: Op2 a b c -> (a -> b -> c)+evalOp2 op = case op of+ And -> (&&)+ Or -> (||)+ Add _ -> (+)+ Sub _ -> (-)+ Mul _ -> (*)+ Mod _ -> (catchZero P.mod)+ Div _ -> (catchZero P.quot)+ Fdiv _ -> (P./)+ Pow _ -> (P.**)+ Logb _ -> P.logBase+ Atan2 _ -> P.atan2+ Eq _ -> (==)+ Ne _ -> (/=)+ Le _ -> (<=)+ Ge _ -> (>=)+ Lt _ -> (<)+ Gt _ -> (>)+ BwAnd _ -> (.&.)+ BwOr _ -> (.|.)+ BwXor _ -> (xor)+ BwShiftL _ _ -> ( \ !a !b -> shiftL a $! fromIntegral b )+ BwShiftR _ _ -> ( \ !a !b -> shiftR a $! fromIntegral b )+ Index _ -> \xs n -> (arrayelems xs) !! (fromIntegral n)++-- | Apply a function to two numbers, so long as the second one is+-- not zero.+--+-- Used to detect attempts at dividing by zero and produce the appropriate+-- 'InterpException'.+catchZero :: Integral a => (a -> a -> a) -> (a -> a -> a)+catchZero _ _ 0 = throw DivideByZero+catchZero f x y = f x y++-- | Evaluate an 'Copilot.Core.Operators.Op3' by producing an equivalent+-- Haskell function operating on the same types as the+-- 'Copilot.Core.Operators.Op3'.+evalOp3 :: Op3 a b c d -> (a -> b -> c -> d)+evalOp3 (Mux _) = \ !v !x !y -> if v then x else y++-- | Turn a stream into a key-value pair that can be added to an 'Env' for+-- simulation.+initStrm :: Stream -> (Id, Dynamic)+initStrm Stream { streamId = id+ , streamBuffer = buffer+ , streamExprType = t } =+ (id, toDyn (reverse buffer))++-- | Evaluate several streams for a number of steps, producing the environment+-- at the end of the evaluation.+evalStreams :: Int -> [Stream] -> Env Id -> Env Id+evalStreams top specStrms initStrms =+ -- XXX actually only need to compute until shortest stream is of length k+ -- XXX this should just be a foldl' over [0,1..k]+ evalStreams_ 0 initStrms+ where+ evalStreams_ :: Int -> Env Id -> Env Id+ evalStreams_ k strms | k == top = strms+ evalStreams_ k strms | otherwise =+ evalStreams_ (k+1) $! strms_+ where+ strms_ = map evalStream specStrms+ evalStream Stream { streamId = id+ , streamExpr = e+ , streamExprType = t } =+ let xs = fromJust $ lookup id strms >>= fromDynamic in+ let x = evalExpr_ k e [] strms in+ let ls = x `seq` (x:xs) in+ (id, toDyn ls)++-- | Evaluate a trigger for a number of steps.+evalTrigger :: ShowType -- ^ Show booleans as @0@/@1@ (C) or+ -- @True@/@False@ (Haskell).+ -> Int -- ^ Number of steps to evaluate.+ -> Env Id -- ^ Environment to use with known+ -- stream-value associations.+ -> Trigger -- ^ Trigger to evaluate.+ -> [Maybe [Output]]+evalTrigger showType k strms+ Trigger+ { triggerGuard = e+ , triggerArgs = args+ } = map tag (zip bs vs)++ where+ tag :: (Bool, a) -> Maybe a+ tag (True, x) = Just x+ tag (False, _) = Nothing++ -- Is the guard true?+ bs :: [Bool]+ bs = evalExprs_ k e strms++ -- The argument outputs.+ vs :: [[Output]]+ vs = if null args then replicate k [] -- might be 0 args.+ else transpose $ map evalUExpr args++ evalUExpr :: UExpr -> [Output]+ evalUExpr (UExpr t e1) =+ map (showWithType showType t) (evalExprs_ k e1 strms)++-- | Evaluate an observer for a number of steps.+evalObserver :: ShowType -- ^ Show booleans as @0@/@1@ (C) or @True@/@False@+ -- (Haskell).+ -> Int -- ^ Number of steps to evaluate.+ -> Env Id -- ^ Environment to use with known stream-value+ -- associations.+ -> Observer -- ^ Observer to evaluate.+ -> [Output]+evalObserver showType k strms+ Observer+ { observerExpr = e+ , observerExprType = t }+ = map (showWithType showType t) (evalExprs_ k e strms)++-- | Evaluate an expression for a number of steps, producing a list with the+-- changing value of the expression until that time.+evalExprs_ :: Typeable a => Int -> Expr a -> Env Id -> [a]+evalExprs_ k e strms =+ map (\i -> evalExpr_ i e [] strms) [0..(k-1)]++-- | Safe indexing (!!) on possibly infininite lists.+safeIndex :: Int -> [a] -> Maybe a+safeIndex i ls =+ let ls' = take (i+1) ls in+ if length ls' > i then Just (ls' !! i)+ else Nothing++-- * Auxiliary++-- Are we proving equivalence with a C backend, in which case we want to show+-- Booleans as '0' and '1'.++-- | Target language for showing a typed value. Used to adapt the+-- representation of booleans.+data ShowType = C | Haskell++-- | Show a value. The representation depends on the type and the target+-- language. Booleans are represented differently depending on the backend.+showWithType :: ShowType -> Type a -> a -> String+showWithType showT t x =+ case showT of+ C -> case t of+ Bool -> if x then "1" else "0"+ _ -> sw+ Haskell -> case t of+ Bool -> if x then "true" else "false"+ _ -> sw+ where+ sw = case showWit t of+ ShowWit -> show x++-- * Auxiliary show instance++-- | Witness datatype for showing a value, used by 'showWithType'.+data ShowWit a = Show a => ShowWit++-- | Turn a type into a show witness.+showWit :: Type a -> ShowWit a+showWit t =+ case t of+ Bool -> ShowWit+ Int8 -> ShowWit+ Int16 -> ShowWit+ Int32 -> ShowWit+ Int64 -> ShowWit+ Word8 -> ShowWit+ Word16 -> ShowWit+ Word32 -> ShowWit+ Word64 -> ShowWit+ Float -> ShowWit+ Double -> ShowWit+ Array t -> ShowWit+ Struct t -> ShowWit
+ src/Copilot/Interpret/Render.hs view
@@ -0,0 +1,122 @@+-- Copyright © 2011 National Institute of Aerospace / Galois, Inc.++-- | Pretty-print the results of a simulation.++{-# LANGUAGE Safe #-}++module Copilot.Interpret.Render+ ( renderAsTable+ , renderAsCSV+ ) where++import Data.List (intersperse, transpose, foldl')+import Data.Maybe (catMaybes)+import Copilot.Interpret.Eval (Output, ExecTrace (..))+import Text.PrettyPrint++import Prelude hiding ((<>))++-- | Render an execution trace as a table, formatted to faciliate readability.+renderAsTable :: ExecTrace -> String+renderAsTable+ ExecTrace+ { interpTriggers = trigs+ , interpObservers = obsvs } = ( render+ . asColumns+ . transpose+ . (:) (ppTriggerNames ++ ppObserverNames)+ . transpose+ ) (ppTriggerOutputs ++ ppObserverOutputs)+ where++ ppTriggerNames :: [Doc]+ ppTriggerNames = map (text . (++ ":")) (map fst trigs)++ ppObserverNames :: [Doc]+ ppObserverNames = map (text . (++ ":")) (map fst obsvs)++ ppTriggerOutputs :: [[Doc]]+ ppTriggerOutputs = map (map ppTriggerOutput) (map snd trigs)++ ppTriggerOutput :: Maybe [Output] -> Doc+ ppTriggerOutput (Just vs) = text $ "(" ++ concat (intersperse "," vs) ++ ")"+ ppTriggerOutput Nothing = text "--"++ ppObserverOutputs :: [[Doc]]+ ppObserverOutputs = map (map text) (map snd obsvs)++-- | Render an execution trace as using comma-separate value (CSV) format.+renderAsCSV :: ExecTrace -> String+renderAsCSV = render . unfold++-- | Pretty print all the steps of the execution trace and concatenate the+-- results.+unfold :: ExecTrace -> Doc+unfold r =+ case step r of+ (cs, Nothing) -> cs+ (cs, Just r') -> cs $$ unfold r'++-- | Pretty print the state of the triggers, and provide a continuation+-- for the execution trace at the next point in time.+step :: ExecTrace -> (Doc, Maybe ExecTrace)+step ExecTrace+ { interpTriggers = trigs+ } =+ if null trigs then (empty, Nothing)+ else (foldl' ($$) empty (text "#" : ppTriggerOutputs), tails)++ where++ ppTriggerOutputs :: [Doc]+ ppTriggerOutputs =+ catMaybes+ . fmap ppTriggerOutput+ . map (fmap head)+ $ trigs++ ppTriggerOutput :: (String, Maybe [Output]) -> Maybe Doc+ ppTriggerOutput (_, Nothing) = Nothing+ ppTriggerOutput (cs, Just xs) = Just $+ text cs <> text "," <>+ (foldr (<>) empty . map text . intersperse ",") xs++ tails :: Maybe ExecTrace+ tails =+ if any null (fmap (tail.snd) trigs)+ then Nothing+ else Just+ ExecTrace+ { interpTriggers = map (fmap tail) trigs+ , interpObservers = []+ }++-- Copied from pretty-ncols because of incompatibility with newer GHC versions.+asColumns :: [[Doc]] -> Doc+asColumns = flip asColumnsWithBuff $ 1++asColumnsWithBuff :: [[Doc]] -> Int -> Doc+asColumnsWithBuff lls q = normalize+ where+ normalize = vcat $ map hsep+ $ map (\x -> pad (length x) longColumnLen empty x)+ $ pad' longEntryLen q+ $ transpose lls -- normalize column height+ longColumnLen = maximum (map length lls)+ longEntryLen = maximum $ map docLen (concat lls)++docLen d = length $ render d++-- | Pad a string on the right to reach an expected length.+pad :: Int -> Int -> a -> [a] -> [a]+pad lx max b ls = ls ++ replicate (max - lx) b++-- | Pad a list of strings on the right with spaces.+pad' :: Int -- ^ Mininum number of spaces to add+ -> Int -- ^ Maximum number of spaces to add+ -> [[Doc]] -- ^ List of documents to pad+ -> [[Doc]]+pad' _ _ [] = []+pad' mx q (ls:xs) = map buf ls : pad' mx q xs+ where+ buf x = x <> (hcat $ replicate q space) <> (hcat $ replicate (mx - (docLen x)) space)
+ tests/Main.hs view
@@ -0,0 +1,18 @@+-- | Test copilot-core.+module Main where++-- External imports+import Test.Framework (Test, defaultMain)++-- Internal library modules being tested+import qualified Test.Copilot.Interpret.Eval++-- | Run all unit tests on copilot-core.+main :: IO ()+main = defaultMain tests++-- | All unit tests in copilot-core.+tests :: [Test.Framework.Test]+tests =+ [ Test.Copilot.Interpret.Eval.tests+ ]
+ tests/Test/Copilot/Interpret/Eval.hs view
@@ -0,0 +1,804 @@+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE GADTs #-}+-- | Test copilot-core:Copilot.Core.Interpret.Eval.+--+-- The gist of this evaluation is in 'SemanticsP' and 'checkSemanticsP' which+-- evaluates an expression using Copilot's evaluator and compares it against+-- its expected meaning.+module Test.Copilot.Interpret.Eval where++-- External imports+import Data.Bits (Bits, complement, shiftL, shiftR,+ xor, (.&.), (.|.))+import Data.Int (Int16, Int32, Int64, Int8)+import Data.List (lookup)+import Data.Maybe (fromMaybe)+import Data.Typeable (Typeable)+import Data.Word (Word16, Word32, Word64, Word8)+import Test.Framework (Test, testGroup)+import Test.Framework.Providers.QuickCheck2 (testProperty)+import Test.QuickCheck (Arbitrary, Gen, Property,+ arbitrary, chooseInt, elements,+ forAll, forAllShow, frequency,+ getPositive, oneof, suchThat,+ vectorOf)+import Text.PrettyPrint.HughesPJ (render)++-- Internal imports: library modules being tested+import Copilot.Core.Expr (Expr (Const, Drop, Op1, Op2, Op3),+ UExpr (UExpr))+import Copilot.Core.Operators (Op1 (..), Op2 (..), Op3 (..))+import Copilot.Core.PrettyPrint (ppExpr)+import Copilot.Core.Spec (Observer (..), Spec (..), Stream (Stream))+import Copilot.Core.Type (Type (..), Typed (typeOf))+import Copilot.Interpret.Eval (ExecTrace (interpObservers),+ ShowType (Haskell), eval)++-- Internal imports: auxiliary functions+import Test.Extra (apply1, apply2, apply3)++-- * Constants++-- | Max length of the traces being tested.+maxTraceLength :: Int+maxTraceLength = 200++-- | All unit tests for copilot-core:Copilot.Core.Interpret.Eval.+tests :: Test.Framework.Test+tests =+ testGroup "Copilot.Core.Interpret.Eval"+ [ testProperty "eval Expr" testEvalExpr+ , testProperty "eval Expr with Drop" testEvalExprWithDrop+ ]++-- * Individual tests++-- | Test for expression evaluation.+testEvalExpr :: Property+testEvalExpr =+ forAll (chooseInt (0, maxTraceLength)) $ \steps ->+ forAllShow arbitrarySemanticsP (semanticsShowK steps) $ \pair ->+ checkSemanticsP steps [] pair++-- | Test for expression evaluation with a drop.+testEvalExprWithDrop :: Property+testEvalExprWithDrop =+ forAll (chooseInt (0, maxTraceLength)) $ \steps ->+ forAllShow arbitrarySemanticsP (semanticsShowK steps) $ \pair ->+ forAllShow (arbitraryDrop pair) (semanticsShowK steps . snd) $ \(str, sem) ->+ checkSemanticsP steps [str] sem++-- * Random generators++-- ** Random SemanticsP generators++-- | An arbitrary expression, paired with its expected meaning.+--+-- See the function 'checkSemanticsP' to evaluate the pair.+arbitrarySemanticsP :: Gen SemanticsP+arbitrarySemanticsP = oneof+ [ SemanticsP <$> (arbitraryBoolExpr :: Gen (Semantics Bool))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Int8))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Int16))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Int32))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Int64))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Word8))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Word16))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Word32))+ , SemanticsP <$> (arbitraryNumExpr :: Gen (Semantics Word64))+ , SemanticsP <$> (arbitraryFloatingExpr :: Gen (Semantics Float))+ , SemanticsP <$> (arbitraryFloatingExpr :: Gen (Semantics Double))+ , SemanticsP <$> (arbitraryRealFracExpr :: Gen (Semantics Float))+ , SemanticsP <$> (arbitraryRealFracExpr :: Gen (Semantics Double))+ , SemanticsP <$> (arbitraryRealFloatExpr :: Gen (Semantics Float))+ , SemanticsP <$> (arbitraryRealFloatExpr :: Gen (Semantics Double))+ , SemanticsP <$> (arbitraryFractionalExpr :: Gen (Semantics Float))+ , SemanticsP <$> (arbitraryFractionalExpr :: Gen (Semantics Double))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Int8))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Int16))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Int32))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Int64))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Word8))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Word16))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Word32))+ , SemanticsP <$> (arbitraryIntegralExpr :: Gen (Semantics Word64))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Bool))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Int8))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Int16))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Int32))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Int64))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Word8))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Word16))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Word32))+ , SemanticsP <$> (arbitraryBitsExpr :: Gen (Semantics Word64))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int8))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int16))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int32))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Int64))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word8))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word16))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word32))+ , SemanticsP <$> (arbitraryBitsIntegralExpr :: Gen (Semantics Word64))+ ]++-- | Generate an arbitrary drop by taking an expression, adding a number of+-- elements to it, and then dropping some.+arbitraryDrop :: SemanticsP -> Gen (Stream, SemanticsP)+arbitraryDrop (SemanticsP (expr, meaning)) = do+ -- Randomly generate a list of elements+ prependLength <- getPositive <$> arbitrary+ buffer <- vectorOf prependLength arbitrary++ -- Build the stream with the buffer+ let streamId = 0+ stream = Stream streamId buffer expr typeOf++ -- Select how many elements to drop from the stream (up to the length of the+ -- buffer)+ dropLength <- chooseInt (0, prependLength)++ -- Build a drop expression that drops those many elements, paired with its+ -- meaning.+ let expr' = Drop typeOf (fromIntegral dropLength) streamId+ meaning' = drop dropLength buffer ++ meaning++ return (stream, SemanticsP (expr', meaning'))++-- ** Random Expr generators++-- | An arbitrary constant expression of any type, paired with its expected+-- meaning.+arbitraryConst :: (Arbitrary t, Typed t)+ => Gen (Expr t, [t])+arbitraryConst = (\v -> (Const typeOf v, repeat v)) <$> arbitrary++-- | An arbitrary boolean expression, paired with its expected meaning.+arbitraryBoolExpr :: Gen (Expr Bool, [Bool])+arbitraryBoolExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryBoolOp1 <*> arbitraryBoolExpr)++ , (1, apply2 <$> arbitraryBoolOp2+ <*> arbitraryBoolExpr+ <*> arbitraryBoolExpr)++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBoolExpr+ <*> arbitraryBoolExpr)++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Expr Int8, [Int8])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Expr Int16, [Int16])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Expr Int32, [Int32])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Expr Int64, [Int64])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Expr Word8, [Word8])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Expr Word16, [Word16])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Expr Word32, [Word32])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryBitsExpr+ <*> (arbitraryBitsExpr :: Gen (Expr Word64, [Word64])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Int8, [Int8])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Int16, [Int16])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Int32, [Int32])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Int64, [Int64])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Word8, [Word8])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Word16, [Word16])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Word32, [Word32])))++ , (1, apply2 <$> arbitraryEqOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Word64, [Word64])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Int8, [Int8])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Int16, [Int16])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Int32, [Int32])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Int64, [Int64])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Word8, [Word8])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Word16, [Word16])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Word32, [Word32])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryNumExpr+ <*> (arbitraryNumExpr :: Gen (Expr Word64, [Word64])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryFloatingExpr+ <*> (arbitraryFloatingExpr :: Gen (Expr Float, [Float])))++ , (1, apply2 <$> arbitraryOrdOp2+ <*> arbitraryFloatingExpr+ <*> (arbitraryFloatingExpr :: Gen (Expr Double, [Double])))++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryBoolExpr+ <*> arbitraryBoolExpr)+ ]++-- | An arbitrary numeric expression, paired with its expected meaning.+arbitraryNumExpr :: (Arbitrary t, Typed t, Num t)+ => Gen (Expr t, [t])+arbitraryNumExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryNumExpr)++ , (2, apply2 <$> arbitraryNumOp2 <*> arbitraryNumExpr <*> arbitraryNumExpr)++ , (2, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryNumExpr+ <*> arbitraryNumExpr)+ ]++-- | An arbitrary floating point expression, paired with its expected meaning.+arbitraryFloatingExpr :: (Arbitrary t, Typed t, Floating t)+ => Gen (Expr t, [t])+arbitraryFloatingExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryFloatingOp1 <*> arbitraryFloatingExpr)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryFloatingExpr)++ , (2, apply2 <$> arbitraryFloatingOp2+ <*> arbitraryFloatingExpr+ <*> arbitraryFloatingExpr)++ , (2, apply2 <$> arbitraryNumOp2+ <*> arbitraryFloatingExpr+ <*> arbitraryFloatingExpr)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryFloatingExpr+ <*> arbitraryFloatingExpr)+ ]++-- | An arbitrary realfrac expression, paired with its expected meaning.+arbitraryRealFracExpr :: (Arbitrary t, Typed t, RealFrac t)+ => Gen (Expr t, [t])+arbitraryRealFracExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (2, apply1 <$> arbitraryRealFracOp1 <*> arbitraryRealFracExpr)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryRealFracExpr)++ , (1, apply2 <$> arbitraryNumOp2+ <*> arbitraryRealFracExpr+ <*> arbitraryRealFracExpr)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryRealFracExpr+ <*> arbitraryRealFracExpr)+ ]++-- | An arbitrary realfloat expression, paired with its expected meaning.+arbitraryRealFloatExpr :: (Arbitrary t, Typed t, RealFloat t)+ => Gen (Expr t, [t])+arbitraryRealFloatExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (2, apply1 <$> arbitraryNumOp1 <*> arbitraryRealFloatExpr)++ , (5, apply2 <$> arbitraryRealFloatOp2+ <*> arbitraryRealFloatExpr+ <*> arbitraryRealFloatExpr)++ , (1, apply2 <$> arbitraryNumOp2+ <*> arbitraryRealFloatExpr+ <*> arbitraryRealFloatExpr)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryRealFloatExpr+ <*> arbitraryRealFloatExpr)+ ]++-- | An arbitrary fractional expression, paired with its expected meaning.+--+-- We add the constraint Eq because we sometimes need to make sure numbers are+-- not zero.+arbitraryFractionalExpr :: (Arbitrary t, Typed t, Fractional t, Eq t)+ => Gen (Expr t, [t])+arbitraryFractionalExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryFractionalOp1 <*> arbitraryFractionalExpr)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryFractionalExpr)++ , (2, apply2 <$> arbitraryFractionalOp2+ <*> arbitraryFractionalExpr+ <*> arbitraryFractionalExprNonZero)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryFractionalExpr+ <*> arbitraryFractionalExpr)+ ]+ where++ -- Generator for fractional expressions that are never zero.+ --+ -- The list is infinite, so this generator checks up to maxTraceLength+ -- elements.+ arbitraryFractionalExprNonZero = arbitraryFractionalExpr+ `suchThat` (notElem 0 . take maxTraceLength . snd)++-- | An arbitrary integral expression, paired with its expected meaning.+--+-- We add the constraint Eq because we sometimes need to make sure numbers are+-- not zero.+arbitraryIntegralExpr :: (Arbitrary t, Typed t, Integral t, Eq t)+ => Gen (Expr t, [t])+arbitraryIntegralExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryNumOp1 <*> arbitraryIntegralExpr)++ , (2, apply2 <$> arbitraryNumOp2+ <*> arbitraryIntegralExpr+ <*> arbitraryIntegralExpr)++ , (2, apply2 <$> arbitraryIntegralOp2+ <*> arbitraryIntegralExpr+ <*> arbitraryIntegralExprNonZero)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryIntegralExpr+ <*> arbitraryIntegralExpr)+ ]+ where++ -- Generator for integral expressions that are never zero.+ --+ -- The list is infinite, so this generator checks up to maxTraceLength+ -- elements.+ arbitraryIntegralExprNonZero = arbitraryIntegralExpr+ `suchThat` (notElem 0 . take maxTraceLength . snd)++-- | An arbitrary Bits expression, paired with its expected meaning.+arbitraryBitsExpr :: (Arbitrary t, Typed t, Bits t)+ => Gen (Expr t, [t])+arbitraryBitsExpr =+ -- We use frequency instead of oneof because the random expression generator+ -- seems to generate expressions that are too large and the test fails due+ -- to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (5, apply1 <$> arbitraryBitsOp1 <*> arbitraryBitsExpr)++ , (2, apply2 <$> arbitraryBitsOp2+ <*> arbitraryBitsExpr+ <*> arbitraryBitsExpr)++ , (2, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryBitsExpr <*> arbitraryBitsExpr)+ ]++-- | An arbitrary expression for types that are instances of Bits and Integral,+-- paired with its expected meaning.+arbitraryBitsIntegralExpr :: (Arbitrary t, Typed t, Bits t, Integral t)+ => Gen (Expr t, [t])+arbitraryBitsIntegralExpr =+ -- We use frequency instead of oneof because the random expression+ -- generator seems to generate expressions that are too large and the+ -- test fails due to running out of memory.+ frequency+ [ (10, arbitraryConst)++ , (2, apply1 <$> arbitraryNumOp1 <*> arbitraryBitsIntegralExpr)++ , (1, apply2 <$> arbitraryNumOp2+ <*> arbitraryBitsIntegralExpr+ <*> arbitraryBitsIntegralExpr)++ , (5, apply2 <$> arbitraryBitsIntegralOp2+ <*> arbitraryBitsIntegralExpr+ <*> arbitraryBitsIntegralExprConstPos)++ , (1, apply3 <$> arbitraryITEOp3+ <*> arbitraryBoolExpr+ <*> arbitraryBitsIntegralExpr+ <*> arbitraryBitsIntegralExpr)+ ]+ where++ -- Generator for constant bit integral expressions that, when converted to+ -- type 't', result in a positive number. We use a constant generator, as+ -- opposed to a generator based on the more comprehensive+ -- arbitraryBitsIntegralExpr, because the latter runs out of memory easily+ -- when nested and filtered with suchThat.+ arbitraryBitsIntegralExprConstPos =+ (\v -> (Const typeOf v, repeat v)) <$> intThatFits+ where+ -- In this context:+ --+ -- intThatFits :: Gen t+ intThatFits =+ suchThat arbitrary ((> 0) . (\x -> (fromIntegral x) :: Int))++-- ** Operators++-- *** Op 1++-- | Generator for arbitrary boolean operators with arity 1, paired with their+-- expected meaning.+arbitraryBoolOp1 :: Gen (Expr Bool -> Expr Bool, [Bool] -> [Bool])+arbitraryBoolOp1 = elements+ [ (Op1 Not, fmap not)+ ]++-- | Generator for arbitrary numeric operators with arity 1, paired with their+-- expected meaning.+arbitraryNumOp1 :: (Typed t, Num t)+ => Gen (Expr t -> Expr t, [t] -> [t])+arbitraryNumOp1 = elements+ [ (Op1 (Abs typeOf), fmap abs)+ , (Op1 (Sign typeOf), fmap signum)+ ]++-- | Generator for arbitrary floating point operators with arity 1, paired with+-- their expected meaning.+arbitraryFloatingOp1 :: (Typed t, Floating t)+ => Gen (Expr t -> Expr t, [t] -> [t])+arbitraryFloatingOp1 = elements+ [ (Op1 (Exp typeOf), fmap exp)+ , (Op1 (Sqrt typeOf), fmap sqrt)+ , (Op1 (Log typeOf), fmap log)+ , (Op1 (Sin typeOf), fmap sin)+ , (Op1 (Tan typeOf), fmap tan)+ , (Op1 (Cos typeOf), fmap cos)+ , (Op1 (Asin typeOf), fmap asin)+ , (Op1 (Atan typeOf), fmap atan)+ , (Op1 (Acos typeOf), fmap acos)+ , (Op1 (Sinh typeOf), fmap sinh)+ , (Op1 (Tanh typeOf), fmap tanh)+ , (Op1 (Cosh typeOf), fmap cosh)+ , (Op1 (Asinh typeOf), fmap asinh)+ , (Op1 (Atanh typeOf), fmap atanh)+ , (Op1 (Acosh typeOf), fmap acosh)+ ]++-- | Generator for arbitrary realfrac operators with arity 1, paired with their+-- expected meaning.+arbitraryRealFracOp1 :: (Typed t, RealFrac t)+ => Gen (Expr t -> Expr t, [t] -> [t])+arbitraryRealFracOp1 = elements+ [ (Op1 (Ceiling typeOf), fmap (fromIntegral . idI . ceiling))+ , (Op1 (Floor typeOf), fmap (fromIntegral . idI . floor))+ ]+ where+ -- Auxiliary function to help the compiler determine which integral type+ -- the result of ceiling must be converted to. An Integer ensures that the+ -- result fits and there is no loss of precision due to the intermediate+ -- casting.+ idI :: Integer -> Integer+ idI = id++-- | Generator for arbitrary fractional operators with arity 1, paired with+-- their expected meaning.+arbitraryFractionalOp1 :: (Typed t, Fractional t)+ => Gen (Expr t -> Expr t, [t] -> [t])+arbitraryFractionalOp1 = elements+ [ (Op1 (Recip typeOf), fmap recip)+ ]++-- | Generator for arbitrary bitwise operators with arity 1, paired with their+-- expected meaning.+arbitraryBitsOp1 :: (Typed t, Bits t)+ => Gen (Expr t -> Expr t, [t] -> [t])+arbitraryBitsOp1 = elements+ [ (Op1 (BwNot typeOf), fmap complement)+ ]++-- *** Op 2++-- | Generator for arbitrary boolean operators with arity 2, paired with their+-- expected meaning.+arbitraryBoolOp2 :: Gen ( Expr Bool -> Expr Bool -> Expr Bool+ , [Bool] -> [Bool] -> [Bool]+ )+arbitraryBoolOp2 = elements+ [ (Op2 And, zipWith (&&))+ , (Op2 Or, zipWith (||))+ ]++-- | Generator for arbitrary numeric operators with arity 2, paired with their+-- expected meaning.+arbitraryNumOp2 :: (Typed t, Num t)+ => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])+arbitraryNumOp2 = elements+ [ (Op2 (Add typeOf), zipWith (+))+ , (Op2 (Sub typeOf), zipWith (-))+ , (Op2 (Mul typeOf), zipWith (*))+ ]++-- | Generator for arbitrary integral operators with arity 2, paired with their+-- expected meaning.+arbitraryIntegralOp2 :: (Typed t, Integral t)+ => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])+arbitraryIntegralOp2 = elements+ [ (Op2 (Mod typeOf), zipWith mod)+ , (Op2 (Div typeOf), zipWith quot)+ ]++-- | Generator for arbitrary fractional operators with arity 2, paired with+-- their expected meaning.+arbitraryFractionalOp2 :: (Typed t, Fractional t)+ => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])+arbitraryFractionalOp2 = elements+ [ (Op2 (Fdiv typeOf), zipWith (/))+ ]++-- | Generator for arbitrary floating point operators with arity 2, paired with+-- their expected meaning.+arbitraryFloatingOp2 :: (Typed t, Floating t)+ => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])+arbitraryFloatingOp2 = elements+ [ (Op2 (Pow typeOf), zipWith (**))+ , (Op2 (Logb typeOf), zipWith logBase)+ ]++-- | Generator for arbitrary floating point operators with arity 2, paired with+-- their expected meaning.+arbitraryRealFloatOp2 :: (Typed t, RealFloat t)+ => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])+arbitraryRealFloatOp2 = elements+ [ (Op2 (Atan2 typeOf), zipWith atan2)+ ]++-- | Generator for arbitrary equality operators with arity 2, paired with their+-- expected meaning.+arbitraryEqOp2 :: (Typed t, Eq t)+ => Gen (Expr t -> Expr t -> Expr Bool, [t] -> [t] -> [Bool])+arbitraryEqOp2 = elements+ [ (Op2 (Eq typeOf), zipWith (==))+ , (Op2 (Ne typeOf), zipWith (/=))+ ]++-- | Generator for arbitrary ordering operators with arity 2, paired with their+-- expected meaning.+arbitraryOrdOp2 :: (Typed t, Ord t)+ => Gen (Expr t -> Expr t -> Expr Bool, [t] -> [t] -> [Bool])+arbitraryOrdOp2 = elements+ [ (Op2 (Le typeOf), zipWith (<=))+ , (Op2 (Lt typeOf), zipWith (<))+ , (Op2 (Ge typeOf), zipWith (>=))+ , (Op2 (Gt typeOf), zipWith (>))+ ]++-- | Generator for arbitrary bitwise operators with arity 2, paired with their+-- expected meaning.+arbitraryBitsOp2 :: (Typed t, Bits t)+ => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])+arbitraryBitsOp2 = elements+ [ (Op2 (BwAnd typeOf), zipWith (.&.))+ , (Op2 (BwOr typeOf), zipWith (.|.))+ , (Op2 (BwXor typeOf), zipWith xor)+ ]++-- | Generator for arbitrary bit shifting operators with arity 2, paired with+-- their expected meaning.+--+-- This generator is a bit more strict in its type signature than the+-- underlying bit-shifting operators being tested, since it enforces both the+-- value being manipulated and the value that indicates how much to shift by to+-- have the same type.+arbitraryBitsIntegralOp2 :: (Typed t, Bits t, Integral t)+ => Gen (Expr t -> Expr t -> Expr t, [t] -> [t] -> [t])+arbitraryBitsIntegralOp2 = elements+ [ (Op2 (BwShiftL typeOf typeOf), zipWith (\x y -> shiftL x (fromIntegral y)))+ , (Op2 (BwShiftR typeOf typeOf), zipWith (\x y -> shiftR x (fromIntegral y)))+ ]++-- *** Op 3++-- | Generator for if-then-else operator (with arity 3), paired with its+-- expected meaning.+--+-- Although this is constant and there is nothing arbitrary, we use the same+-- structure and naming convention as with others for simplicity.+arbitraryITEOp3 :: (Arbitrary t, Typed t)+ => Gen ( Expr Bool -> Expr t -> Expr t -> Expr t+ , [Bool] -> [t] -> [t] -> [t]+ )+arbitraryITEOp3 = return+ (Op3 (Mux typeOf), zipWith3 (\x y z -> if x then y else z))++-- * Semantics++-- | Type that pairs an expression with its meaning as an infinite stream.+type Semantics t = (Expr t, [t])++-- | A phantom semantics pair is an existential type that encloses an+-- expression and its expected meaning as an infinite list of values.+--+-- It is needed by the arbitrary expression generator, to create a+-- heterogeneous list.+data SemanticsP = forall t+ . (Typeable t, Read t, Eq t, Show t, Typed t, Arbitrary t)+ => SemanticsP+ { semanticsPair :: (Expr t, [t])+ }++-- | Show function for test triplets that limits the accompanying list+-- to a certain length.+semanticsShowK :: Int -> SemanticsP -> String+semanticsShowK steps (SemanticsP (expr, exprList)) =+ show (showType ty, render $ ppExpr expr, take steps exprList)++ where++ -- Type of the expression. The type is enforced by _u below.+ ty = typeOf++ -- We want to show the type. To help GHC determine that the type t is the+ -- same as the expression's (expr), we use an UExpr, which has an+ -- additional constraint. This definition serves no other purpose than to+ -- help enforce that constraint.+ _u = UExpr ty expr++-- | Check that the expression in the semantics pair is evaluated to the given+-- list, up to a number of steps.+--+-- Some operations will overflow and return NaN. Because comparing any NaN+-- will, as per IEEE 754, always fail (i.e., return False), we handle that+-- specific case by stating that the test succeeds if any expected values+-- is NaN.+checkSemanticsP :: Int -> [Stream] -> SemanticsP -> Bool+checkSemanticsP steps streams (SemanticsP (expr, exprList)) =+ any isNaN' expectation || resultValues == expectation+ where+ -- Limit expectation to the number of evaluation steps.+ expectation = take steps exprList++ -- Obtain the results by looking up the observer in the spec+ -- and parsing the results into Haskell values.+ resultValues = fmap readResult results+ results = lookupWithDefault testObserverName []+ $ interpObservers trace++ -- Spec with just one observer of one expression.+ trace = eval Haskell steps spec+ spec = Spec streams observers [] []+ observers = [Observer testObserverName expr typeOf]++ -- Fixed name for the observer. Used to obtain the result from the+ -- trace. It should be the only observer in the trace.+ testObserverName :: String+ testObserverName = "res"++ -- | Is NaN with Eq requirement only.+ isNaN' :: Eq a => a -> Bool+ isNaN' x = x /= x++-- * Auxiliary++-- | Read a Haskell value from the output of the evaluator.+readResult :: Read a => String -> a+readResult = read . readResult'+ where+ readResult' :: String -> String+ readResult' "false" = "False"+ readResult' "true" = "True"+ readResult' s = s++-- | Variant of 'lookup' with an additional default value returned when the key+-- provided is not found in the map.+lookupWithDefault :: Ord k => k -> v -> [(k, v)] -> v+lookupWithDefault k def = fromMaybe def . lookup k++-- | Show Copilot Core type.+showType :: Type a -> String+showType t =+ case t of+ Bool -> "Bool"+ Int8 -> "Int8"+ Int16 -> "Int16"+ Int32 -> "Int32"+ Int64 -> "Int64"+ Word8 -> "Word8"+ Word16 -> "Word16"+ Word32 -> "Word32"+ Word64 -> "Word64"+ Float -> "Float"+ Double -> "Double"+ Array t -> "Array " ++ showType t+ Struct t -> "Struct"
+ tests/Test/Extra.hs view
@@ -0,0 +1,31 @@+-- | Auxiliary testing helper functions.+module Test.Extra where++-- External imports+import Control.Arrow ((***))++-- * Function application++-- | Apply a tuple with two functions to a tuple of arguments.+apply1 :: (a1 -> b1, a2 -> b2) -- ^ Pair with functions+ -> (a1, a2) -- ^ Pair with arguments+ -> (b1, b2) -- ^ Pair with results+apply1 = uncurry (***)++-- | Apply a tuple with two functions on two arguments to their tupled+-- arguments.+apply2 :: (a1 -> b1 -> c1, a2 -> b2 -> c2) -- ^ Pair with functions+ -> (a1, a2) -- ^ Pair with first arguments+ -> (b1, b2) -- ^ Pair with second arguments+ -> (c1, c2) -- ^ Pair with results+apply2 fs = apply1 . apply1 fs++-- | Apply a tuple with two functions on three arguments to their tupled+-- arguments.+apply3 :: (a1 -> b1 -> c1 -> d1, a2 -> b2 -> c2 -> d2)+ -- ^ Pair with functions+ -> (a1, a2) -- ^ Pair with first arguments+ -> (b1, b2) -- ^ Pair with second arguments+ -> (c1, c2) -- ^ Pair with third arguments+ -> (d1, d2) -- ^ Pair with results+apply3 fs = apply2 . apply1 fs