diff --git a/CHANGELOG b/CHANGELOG new file mode 100644 --- /dev/null +++ b/CHANGELOG @@ -0,0 +1,3 @@ +2022-09-07 + * Version bump (3.11). (#376) + * Split copilot-interpreter into separate library. (#361) diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,30 @@ +[![Build Status](https://travis-ci.com/Copilot-Language/copilot.svg?branch=master)](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). diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/copilot-interpreter.cabal b/copilot-interpreter.cabal new file mode 100644 --- /dev/null +++ b/copilot-interpreter.cabal @@ -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 + . + +author: Frank Dedden, Lee Pike, Robin Morisset, Alwyn Goodloe, + Sebastian Niller, Nis Nordbyop Wegmann, Ivan Perez +license: BSD3 +license-file: LICENSE +maintainer: Ivan Perez +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 diff --git a/src/Copilot/Interpret.hs b/src/Copilot/Interpret.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Interpret.hs @@ -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 diff --git a/src/Copilot/Interpret/Error.hs b/src/Copilot/Interpret/Error.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Interpret/Error.hs @@ -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 diff --git a/src/Copilot/Interpret/Eval.hs b/src/Copilot/Interpret/Eval.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Interpret/Eval.hs @@ -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 diff --git a/src/Copilot/Interpret/Render.hs b/src/Copilot/Interpret/Render.hs new file mode 100644 --- /dev/null +++ b/src/Copilot/Interpret/Render.hs @@ -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) diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -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 + ] diff --git a/tests/Test/Copilot/Interpret/Eval.hs b/tests/Test/Copilot/Interpret/Eval.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Copilot/Interpret/Eval.hs @@ -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" diff --git a/tests/Test/Extra.hs b/tests/Test/Extra.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Extra.hs @@ -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