diff --git a/CHANGELOG b/CHANGELOG --- a/CHANGELOG +++ b/CHANGELOG @@ -1,3 +1,7 @@ +2023-07-07 + * Version bump (3.16). (#448) + * Introduce testing infrastructure. (#413) + 2023-05-07 * Version bump (3.15). (#438) diff --git a/copilot-c99.cabal b/copilot-c99.cabal --- a/copilot-c99.cabal +++ b/copilot-c99.cabal @@ -1,6 +1,6 @@ cabal-version : >= 1.10 name : copilot-c99 -version : 3.15 +version : 3.16 synopsis : A compiler for Copilot targeting C99. description : This package is a back-end from Copilot to C. @@ -45,7 +45,7 @@ , mtl >= 2.2 && < 2.4 , pretty >= 1.1 && < 1.2 - , copilot-core >= 3.15 && < 3.16 + , copilot-core >= 3.16 && < 3.17 , language-c99 >= 0.2.0 && < 0.3 , language-c99-simple >= 0.2.2 && < 0.3 @@ -58,3 +58,38 @@ , Copilot.Compile.C99.External , Copilot.Compile.C99.Compile , Copilot.Compile.C99.Settings + +test-suite unit-tests + type: + exitcode-stdio-1.0 + + main-is: + Main.hs + + other-modules: + Test.Copilot.Compile.C99 + + build-depends: + base + , directory + , HUnit + , QuickCheck + , pretty + , process + , random + , test-framework + , test-framework-hunit + , test-framework-quickcheck2 + , unix + + , copilot-core + , copilot-c99 + + hs-source-dirs: + tests + + default-language: + Haskell2010 + + ghc-options: + -Wall 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-c99. +module Main where + +-- External imports +import Test.Framework (Test, defaultMain) + +-- Internal library modules being tested +import qualified Test.Copilot.Compile.C99 + +-- | Run all unit tests on copilot-c99. +main :: IO () +main = defaultMain tests + +-- | All unit tests in copilot-c99. +tests :: [Test.Framework.Test] +tests = + [ Test.Copilot.Compile.C99.tests + ] diff --git a/tests/Test/Copilot/Compile/C99.hs b/tests/Test/Copilot/Compile/C99.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Copilot/Compile/C99.hs @@ -0,0 +1,955 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- | Test copilot-c99:Copilot.Compile.C99. +module Test.Copilot.Compile.C99 + ( tests ) + where + +-- External imports +import Control.Arrow ((&&&)) +import Control.Exception (IOException, catch) +import Control.Monad (when) +import Data.Bits (Bits, complement) +import Data.List (intercalate) +import Data.Type.Equality (testEquality) +import Data.Typeable (Proxy (..), (:~:) (Refl)) +import GHC.TypeLits (KnownNat, natVal) +import System.Directory (doesFileExist, + getTemporaryDirectory, + removeDirectory, removeFile, + setCurrentDirectory) +import System.IO (hPutStrLn, stderr) +import System.Posix.Temp (mkdtemp) +import System.Process (callProcess, readProcess) +import System.Random (Random) +import Test.Framework (Test, testGroup) +import Test.Framework.Providers.QuickCheck2 (testProperty) +import Test.QuickCheck (Arbitrary, Gen, Property, + arbitrary, choose, elements, + forAll, forAllBlind, frequency, + getPositive, ioProperty, oneof, + vectorOf, (.&&.)) +import Test.QuickCheck.Gen (chooseAny, chooseBoundedIntegral) + +-- External imports: Copilot +import Copilot.Core hiding (Property) +import Copilot.Core.Type.Array (array) + +-- External imports: Modules being tested +import Copilot.Compile.C99 (cSettingsOutputDirectory, compile, compileWith, + mkDefaultCSettings) + +-- * Constants + +-- | All unit tests for copilot-core:Copilot.Core.Type. +tests :: Test.Framework.Test +tests = + testGroup "Copilot.Compile.C99" + [ testProperty "Compile specification" testCompile + , testProperty "Compile specification in custom dir" testCompileCustomDir + , testProperty "Run specification" testRun + , testProperty "Run and compare results" testRunCompare + ] + +-- * Individual tests + +-- | Test compiling a spec. +testCompile :: Property +testCompile = ioProperty $ do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + testDir <- mkdtemp "copilot_test_" + setCurrentDirectory testDir + + compile "copilot_test" spec + r <- compileC "copilot_test" + + -- Remove file produced by GCC + removeFile "copilot_test.o" + + -- Remove files produced by Copilot + removeFile "copilot_test.c" + removeFile "copilot_test.h" + removeFile "copilot_test_types.h" + + setCurrentDirectory tmpDir + removeDirectory testDir + + return r + + where + + spec = Spec streams observers triggers properties + + streams = [ Stream 0 [1] (Const Int8 1) Int8] + observers = [] + triggers = [ Trigger function guard args ] + properties = [] + + function = "func" + + guard = Const Bool True + + args = [] + +-- | Test compiling a spec in a custom directory. +testCompileCustomDir :: Property +testCompileCustomDir = ioProperty $ do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + testDir <- mkdtemp "copilot_test_" + + compileWith (mkDefaultCSettings { cSettingsOutputDirectory = testDir }) + "copilot_test" + spec + + setCurrentDirectory testDir + r <- compileC "copilot_test" + + -- Remove file produced by GCC + removeFile "copilot_test.o" + + -- Remove files produced by Copilot + removeFile "copilot_test.c" + removeFile "copilot_test.h" + removeFile "copilot_test_types.h" + + setCurrentDirectory tmpDir + removeDirectory testDir + + return r + + where + + spec = Spec streams observers triggers properties + + streams = [ Stream 0 [1] (Const Int8 1) Int8] + observers = [] + triggers = [ Trigger function guard args ] + properties = [] + + function = "nop" + + guard = Const Bool True + + args = [] + +-- | Test compiling a spec and running the resulting program. +-- +-- The actual behavior is ignored. +testRun :: Property +testRun = ioProperty $ do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + testDir <- mkdtemp "copilot_test_" + setCurrentDirectory testDir + + compile "copilot_test" spec + r <- compileC "copilot_test" + + let cProgram = unlines + [ "#include \"copilot_test.h\"" + , "" + , "void nop () {" + , "}" + , "" + , "void main () {" + , " step();" + , "}" + ] + + writeFile "main.c" cProgram + + -- Compile a main program + r2 <- compileExecutable "main" [ "copilot_test.o" ] + callProcess "./main" [] + + -- Remove file produced by GCC + removeFile "copilot_test.o" + removeFile "main" + + -- Remove files produced "by hand" + removeFile "main.c" + + -- Remove files produced by Copilot + removeFile "copilot_test.c" + removeFile "copilot_test.h" + removeFile "copilot_test_types.h" + + setCurrentDirectory tmpDir + removeDirectory testDir + + return $ r && r2 + + where + + spec = Spec streams observers triggers properties + + streams = [ Stream 0 [1] (Const Int8 1) Int8] + observers = [] + triggers = [ Trigger function guard args ] + properties = [] + + function = "nop" + + guard = Const Bool True + + args = [] + +-- | Test running compiled spec and comparing the results to the +-- expectation. +testRunCompare :: Property +testRunCompare = + testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int8 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int16 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int32 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Int64 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word8 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word16 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word32 Bool)) + .&&. testRunCompare1 (arbitraryOpIntegralBool :: Gen (TestCase1 Word64 Bool)) + .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Float Bool)) + .&&. testRunCompare1 (arbitraryOpFloatingBool :: Gen (TestCase1 Double Bool)) + .&&. testRunCompare2 (arbitraryArrayNum :: Gen (TestCase2 (Array 2 Int8) Word32 Int8)) + .&&. testRunCompare2 (arbitraryArrayNum :: Gen (TestCase2 (Array 2 Int16) Word32 Int16)) + +-- * Random generators + +-- ** Random function generators + +-- | Generator of functions that produce booleans. +arbitraryOpBool :: Typed a => Gen (Fun a Bool, [a] -> [Bool]) +arbitraryOpBool = + frequency + [ (5, arbitraryOp1Any) + , (5, funCompose1 <$> arbitraryOp1Bool <*> arbitraryOpBool) + , (2, funCompose2 <$> arbitraryOp2Bool <*> arbitraryOpBool <*> arbitraryOpBool) + , (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpBool <*> arbitraryOpBool) + , (1, funCompose2 <$> arbitraryOp2Ord <*> arbitraryOpBool <*> arbitraryOpBool) + ] + +-- | Generator of functions that take Bits and produce booleans. +arbitraryOpBoolBits :: (Typed a, Bits a) => Gen (Fun a Bool, [a] -> [Bool]) +arbitraryOpBoolBits = + frequency + [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpBits <*> arbitraryOpBits) + ] + +-- | Generator of functions that take Nums and produce booleans. +arbitaryOpBoolOrdEqNum :: (Typed a, Eq a, Ord a, Num a) + => Gen (Fun a Bool, [a] -> [Bool]) +arbitaryOpBoolOrdEqNum = + frequency + [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpNum <*> arbitraryOpNum) + , (1, funCompose2 <$> arbitraryOp2Ord <*> arbitraryOpNum <*> arbitraryOpNum) + ] + +-- | Generator of functions that take Floating point numbers and produce +-- booleans. +arbitraryOpBoolEqNumFloat :: (Typed t, Eq t, Num t, Floating t) + => Gen (Fun t Bool, [t] -> [Bool]) +arbitraryOpBoolEqNumFloat = + frequency + [ (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpNum <*> arbitraryOpFloat) + , (1, funCompose2 <$> arbitraryOp2Eq <*> arbitraryOpFloat <*> arbitraryOpNum) + ] + +-- | Generator of functions that take and produce Bits. +arbitraryOpBits :: (Bits t, Typed t) + => Gen (Fun t t, [t] -> [t]) +arbitraryOpBits = elements + [ (Op1 (BwNot typeOf), fmap complement) + ] + +-- | Generator of functions that take and produce Nums. +arbitraryOpNum :: (Typed t, Num t) => Gen (Fun t t, [t] -> [t]) +arbitraryOpNum = elements + [ (Op1 (Abs typeOf), fmap abs) + , (Op1 (Sign typeOf), fmap signum) + ] + +-- | Generator of functions that take an arrays and indicates and produce +-- elements from the array. +arbitraryArrayIx :: forall t n . (Typed t, KnownNat n, Num t) + => Gen ( Fun2 (Array n t) Word32 t + , [Array n t] -> [Word32] -> [t] + ) +arbitraryArrayIx = return + (Op2 (Index typeOf), zipWith (\x y -> arrayelems x !! fromIntegral y)) + +-- | Generator of functions on Floating point numbers. +arbitraryOpFloat :: (Floating t, Typed t) => Gen (Fun t t, [t] -> [t]) +arbitraryOpFloat = 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 of functions on that produce elements of any type. +arbitraryOp1Any :: forall a b + . (Arbitrary b, Typed a, Typed b) + => Gen (Fun a b, [a] -> [b]) +arbitraryOp1Any = oneof $ + [ (\v -> (\_ -> Const typeOf v, fmap (const v))) <$> arbitrary ] + ++ + rest + where + rest | Just Refl <- testEquality t1 t2 + = [return (id, id)] + | otherwise + = [] + + t1 :: Type a + t1 = typeOf + + t2 :: Type b + t2 = typeOf + +-- | Generator of functions on Booleans. +arbitraryOp1Bool :: Gen (Fun Bool Bool, [Bool] -> [Bool]) +arbitraryOp1Bool = elements + [ (Op1 Not, fmap not) + ] + +-- | Generator of binary functions on Booleans. +arbitraryOp2Bool :: Gen (Fun2 Bool Bool Bool, [Bool] -> [Bool] -> [Bool]) +arbitraryOp2Bool = elements + [ (Op2 And, zipWith (&&)) + , (Op2 Or, zipWith (||)) + ] + +-- | Generator of binary functions that take two Eq elements of the same type +-- and return a Bool. +arbitraryOp2Eq :: (Typed t, Eq t) + => Gen (Fun2 t t Bool, [t] -> [t] -> [Bool]) +arbitraryOp2Eq = elements + [ (Op2 (Eq typeOf), zipWith (==)) + , (Op2 (Ne typeOf), zipWith (/=)) + ] + +-- | Generator of binary functions that take two Ord elements of the same type +-- and return a Bool. +arbitraryOp2Ord :: (Typed t, Ord t) + => Gen (Fun2 t t Bool, [t] -> [t] -> [Bool]) +arbitraryOp2Ord = elements + [ (Op2 (Le typeOf), zipWith (<=)) + , (Op2 (Lt typeOf), zipWith (<)) + , (Op2 (Ge typeOf), zipWith (>=)) + , (Op2 (Gt typeOf), zipWith (>)) + ] + +-- ** Random data generators + +-- | Random array generator. +arbitraryArray :: forall n t . (KnownNat n, Random t) => Gen (Array n t) +arbitraryArray = array <$> vectorOf len chooseAny + where + len :: Int + len = fromIntegral $ natVal (Proxy :: Proxy n) + +-- ** Random test case generators + +-- | Generator for test cases on integral numbers that produce booleans. +arbitraryOpIntegralBool :: (Typed t, Bounded t, Integral t, Bits t) + => Gen (TestCase1 t Bool) +arbitraryOpIntegralBool = frequency + [ (5, mkTestCase1 + arbitraryOpBool + (chooseBoundedIntegral (minBound, maxBound))) + + , (2, mkTestCase1 + arbitraryOpBoolBits + (chooseBoundedIntegral (minBound, maxBound))) + + -- we need to use +1 because certain operations overflow the number + , (2, mkTestCase1 + arbitaryOpBoolOrdEqNum + (chooseBoundedIntegral (minBound + 1, maxBound))) + ] + +-- | Generator for test cases on floating-point numbers that produce booleans. +arbitraryOpFloatingBool :: (Random t, Typed t, Floating t, Eq t) + => Gen (TestCase1 t Bool) +arbitraryOpFloatingBool = oneof + [ mkTestCase1 arbitraryOpBoolEqNumFloat chooseAny + ] + +-- | Generator for test cases on Arrays selection producing values of the +-- array. +arbitraryArrayNum :: forall n a + . (KnownNat n, Num a, Random a, Typed a) + => Gen (TestCase2 (Array n a) Word32 a) +arbitraryArrayNum = oneof + [ mkTestCase2 arbitraryArrayIx arbitraryArray gen + ] + where + gen :: Gen Word32 + gen = choose (0, len - 1) + + len :: Word32 + len = fromIntegral $ natVal (Proxy :: Proxy n) + +-- * Semantics + +-- ** Functions + +-- | Unary Copilot function. +type Fun a b = Expr a -> Expr b + +-- | Binary Copilot function. +type Fun2 a b c = Expr a -> Expr b -> Expr c + +-- | Compose functions, paired with the Haskell functions that define their +-- idealized meaning. +funCompose1 :: (Fun b c, [b] -> [c]) + -> (Fun a b, [a] -> [b]) + -> (Fun a c, [a] -> [c]) +funCompose1 (f1, g1) (f2, g2) = (f1 . f2, g1 . g2) + +-- | Compose a binary function, with two functions, one for each argument. +funCompose2 :: (Fun2 b c d, [b] -> [c] -> [d]) + -> (Fun a b, [a] -> [b]) + -> (Fun a c, [a] -> [c]) + -> (Fun a d, [a] -> [d]) +funCompose2 (f1, g1) (f2, g2) (f3, g3) = + (uncurry f1 . (f2 &&& f3), uncurry g1 . (g2 &&& g3)) + +-- ** Test cases + +-- | Test case specification for specs with one input variable and one output. +data TestCase1 a b = TestCase1 + { wrapTC1Expr :: Spec + -- ^ Specification containing a trigger an extern of type 'a' and a trigger + -- with an argument of type 'b'. + + , wrapTC1Fun :: [a] -> [b] + -- ^ Function expected to function in the same way as the Spec being + -- tested. + + , wrapTC1CopInp :: (String -> String, String, String, Gen a) + -- ^ Input specification. + -- + -- - The first element is a function that prints the variable declaration + -- in C. + -- + -- - The second element obtains a C expression that calculates the size of + -- the variable in C. + -- + -- - The third contains the variable name in C. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC1CopOut :: (String, String) + -- ^ Output specification. + -- + -- The first element of the tuple contains the type of the output in C. + -- + -- The second element of the tuple is the formatting string when printing + -- values of the given kind. + } + +-- | Test case specification for specs with two input variables and one output. +data TestCase2 a b c = TestCase2 + { wrapTC2Expr :: Spec + -- ^ Specification containing a trigger an extern of type 'a' and a trigger + -- with an argument of type 'b'. + + , wrapTC2Fun :: [a] -> [b] -> [c] + -- ^ Function expected to function in the same way as the Spec being + -- tested. + + , wrapTC2CopInp1 :: (String -> String, String, String, Gen a) + -- ^ Input specification for the first input. + -- + -- - The first element is a function that prints the variable declaration + -- in C. + -- + -- - The second element obtains a C expression that calculates the size of + -- the variable in C. + -- + -- - The third contains the variable name in C. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC2CopInp2 :: (String -> String, String, String, Gen b) + -- ^ Input specification for the second input. + -- + -- - The first element is a function that prints the variable declaration + -- in C. + -- + -- - The second element obtains a C expression that calculates the size of + -- the variable in C. + -- + -- - The third contains the variable name in C. + -- + -- - The latter contains a randomized generator for values of the given + -- type. + + , wrapTC2CopOut :: (String, String) + -- ^ Output specification. + -- + -- The first element of the tuple contains the type of the output in C. + -- + -- The second element of the tuple is the formatting string when printing + -- values of the given kind. + } + +-- | Generate test cases for expressions that behave like unary functions. +mkTestCase1 :: (Typed a, Typed b) + => Gen (Fun a b, [a] -> [b]) + -> Gen a + -> Gen (TestCase1 a b) +mkTestCase1 genO gen = do + (copilotF, semF) <- genO + + let spec = alwaysTriggerArg1 (UExpr t2 appliedOp) + appliedOp = copilotF (ExternVar t1 varName Nothing) + + return $ + TestCase1 + spec + semF + ( varDeclC t1, sizeC t1, varName, gen ) + ( typeC t2, formatC t2) + + where + + t1 = typeOf + t2 = typeOf + + varName = "input" + +-- | Generate test cases for expressions that behave like binary functions. +mkTestCase2 :: (Typed a, Typed b, Typed c) + => Gen (Fun2 a b c, [a] -> [b] -> [c]) + -> Gen a + -> Gen b + -> Gen (TestCase2 a b c) +mkTestCase2 genO genA genB = do + (copilotF, semF) <- genO + + let spec = alwaysTriggerArg1 (UExpr t3 appliedOp) + appliedOp = copilotF (ExternVar t1 varName1 Nothing) + (ExternVar t2 varName2 Nothing) + + return $ + TestCase2 + spec + semF + ( varDeclC t1, sizeC t1, varName1, genA ) + ( varDeclC t2, sizeC t2, varName2, genB ) + ( typeC t3, formatC t3) + + where + + t1 = typeOf + t2 = typeOf + t3 = typeOf + + varName1 = "input1" + varName2 = "input2" + +-- | Test running a compiled C program and comparing the results. +testRunCompare1 :: (Show a, CShow a, ReadableFromC b, Eq b) + => Gen (TestCase1 a b) -> Property +testRunCompare1 ops = + forAllBlind ops $ \testCase -> + let (TestCase1 copilotSpec haskellFun inputVar outputVar) = testCase + (cTypeInput, size, cInputName, gen) = inputVar + + in forAll (getPositive <$> arbitrary) $ \len -> + + forAll (vectorOf len gen) $ \nums -> do + + let inputs = [ (cTypeInput, size, fmap cshow nums, cInputName) ] + outputs = haskellFun nums + + testRunCompareArg inputs len outputs copilotSpec outputVar + +-- | Test running a compiled C program and comparing the results. +testRunCompare2 :: (Show a1, CShow a1, Show a2, CShow a2, ReadableFromC b, Eq b) + => Gen (TestCase2 a1 a2 b) -> Property +testRunCompare2 ops = + forAllBlind ops $ \testCase -> + let (TestCase2 copilotSpec haskellFun inputVar1 inputVar2 outputVar) = + testCase + + (cTypeInput1, size1, cInputName1, gen1) = inputVar1 + (cTypeInput2, size2, cInputName2, gen2) = inputVar2 + + in forAll (getPositive <$> arbitrary) $ \len -> + forAll (vectorOf len gen1) $ \nums1 -> + forAll (vectorOf len gen2) $ \nums2 -> do + let inputs = [ (cTypeInput1, size1, fmap cshow nums1, cInputName1) + , (cTypeInput2, size2, fmap cshow nums2, cInputName2) + ] + + outputs = haskellFun nums1 nums2 + + testRunCompareArg inputs len outputs copilotSpec outputVar + +-- | Test running a compiled C program and comparing the results, when the +-- program produces one output as an argument to a trigger that always fires. +-- +-- PRE: all lists (second argument) of inputs have the length given as second +-- argument. +-- +-- PRE: the monitoring code this is linked against uses the function +-- @printBack@ with exactly one argument to pass the results. +testRunCompareArg :: (ReadableFromC b, Eq b) + => [(String -> String, String, [String], String)] + -> Int + -> [b] + -> Spec + -> (String, String) + -> Property +testRunCompareArg inputs numInputs nums spec outputVar = + ioProperty $ do + tmpDir <- getTemporaryDirectory + setCurrentDirectory tmpDir + + -- Operate in temporary directory + testDir <- mkdtemp "copilot_test_" + setCurrentDirectory testDir + + -- Produce copilot monitoring code + compile "copilot_test" spec + r <- compileC "copilot_test" + + -- Produce wrapper program + let cProgram = testRunCompareArgCProgram inputs numInputs outputVar + writeFile "main.c" cProgram + + -- Compile main program + r2 <- compileExecutable "main" [ "copilot_test.o" ] + + -- Print result so far (for debugging purposes only) + print r2 + print testDir + + -- Run program and compare result + out <- readProcess "./main" [] "" + let outNums = readFromC <$> lines out + comparison = outNums == nums + + -- Only clean up if the test succeeded; otherwise, we want to inspect it. + when comparison $ do + -- Remove file produced by GCC + removeFile "copilot_test.o" + removeFile "main" + + -- Remove files produced "by hand" + removeFile "main.c" + + -- Remove files produced by Copilot + removeFile "copilot_test.c" + removeFile "copilot_test.h" + removeFile "copilot_test_types.h" + + -- Remove temporary directory + setCurrentDirectory tmpDir + removeDirectory testDir + + return $ r && r2 && comparison + +-- | Return a wrapper C program that runs a loop for a number of iterations, +-- putting values in global variables at every step, running the monitors, and +-- publishing the results of any outputs. +testRunCompareArgCProgram + :: [(String -> String, String, [String], String)] + -> Int + -> (String, String) + -> String +testRunCompareArgCProgram inputs numSteps outputVar = unlines $ + [ "#include " + , "#include " + , "#include " + , "#include " + , "#include " + , "#include \"copilot_test.h\"" + , "" + ] + ++ varDecls ++ + [ "" + , "void printBack (" ++ cTypeRes ++ " num) {" + , " printf(\"" ++ cStr ++ "\\n\", num);" + , "}" + , "" + , "int main () {" + , " int i = 0;" + , " for (i = 0; i < " ++ maxInputsName ++ "; i++) {" + ] + ++ inputUpdates ++ + [ "" + , " step();" + , " }" + , " return 0;" + , "}" + ] + + where + + varDecls :: [String] + varDecls = + [ "int " ++ maxInputsName ++ " = " ++ show numSteps ++ ";" ] + ++ inputVarDecls + + inputVarDecls :: [String] + inputVarDecls = + concatMap + (\(ctypeF, _size, varName, arrVar, arrVals) -> + + let inputsStr = intercalate ", " (arrVals :: [String]) + + in [ ctypeF (arrVar ++ "[]") ++ " = {" ++ inputsStr ++ "};" + , "" + , ctypeF varName ++ ";" + ] + ) + vars + + inputUpdates :: [String] + inputUpdates = concatMap (\(_ctype, size, varName, arrVar, _arrVals) -> + [ " memcpy(&" ++ varName ++ ", &" ++ arrVar ++ "[i], " ++ size ++ ");" + ]) + vars + + (cTypeRes, cStr) = outputVar + + vars = map oneInput inputs + oneInput (cTypeInput, size, inputVals, cInputName) = + (cTypeInput, size, inputVarName, inputArrVarName, inputVals) + where + inputVarName = cInputName + inputArrVarName = cInputName ++ "_s" + + maxInputsName = "MAX_STEPS" + +-- * Auxiliary functions + +-- ** Specs handling + +-- | Build a 'Spec' that triggers at every step, passing the given expression +-- as argument, and execution a function 'printBack'. +alwaysTriggerArg1 :: UExpr -> Spec +alwaysTriggerArg1 = triggerArg1 (Const Bool True) + + where + + -- | Build a 'Spec' that triggers based on a given boolean stream, passing + -- the given expression as argument, and execution a function 'printBack'. + triggerArg1 :: Expr Bool -> UExpr -> Spec + triggerArg1 guard expr = Spec streams observers triggers properties + + where + + streams = [] + observers = [] + properties = [] + + triggers = [ Trigger function guard args ] + function = "printBack" + args = [ expr ] + +-- ** Compilation of C programs + +-- | Compile a C file given its basename. +compileC :: String -> IO Bool +compileC baseName = do + result <- catch (do callProcess "gcc" [ "-c", baseName ++ ".c" ] + return True + ) + (\e -> do + hPutStrLn stderr $ + "copilot-c99: error: compileC: cannot compile " + ++ baseName ++ ".c with gcc" + hPutStrLn stderr $ + "copilot-c99: exception: " ++ show (e :: IOException) + return False + ) + if result + then doesFileExist $ baseName ++ ".o" + else return False + +-- | Compile a C file into an executable, given its basename and files to link +-- with it. +compileExecutable :: String -> [String] -> IO Bool +compileExecutable baseName linked = do + result <- catch (do callProcess "gcc" $ [ baseName ++ ".c" ] + ++ linked + ++ [ "-lm" ] + ++ [ "-o", baseName ] + return True + ) + (\e -> do + hPutStrLn stderr $ + "copilot-c99: error: compileExecutable: cannot compile " + ++ baseName ++ ".c with gcc" + hPutStrLn stderr $ + "copilot-c99: exception: " ++ show (e :: IOException) + return False + ) + if result + then doesFileExist baseName + else return False + +-- ** Interfacing between Haskell and C + +-- | C formatting string that can be used to print values of a given type. +formatC :: Typed a => Type a -> String +formatC Bool = "%d" +formatC Int8 = "%d" +formatC Int16 = "%d" +formatC Int32 = "%d" +formatC Int64 = "%ld" +formatC Word8 = "%d" +formatC Word16 = "%d" +formatC Word32 = "%d" +formatC Word64 = "%ld" +formatC Float = "%f" +formatC Double = "%lf" +formatC _ = error + "copilot-c99 (test): Printing of arrays and structs is not yet supported." + +-- | C type used to store values of a given type. +typeC :: Typed a => Type a -> String +typeC Bool = "bool" +typeC Int8 = "int8_t" +typeC Int16 = "int16_t" +typeC Int32 = "int32_t" +typeC Int64 = "int64_t" +typeC Word8 = "uint8_t" +typeC Word16 = "uint16_t" +typeC Word32 = "uint32_t" +typeC Word64 = "uint64_t" +typeC Float = "float" +typeC Double = "double" +typeC (Array tE) = typeC tE ++ "[]" +typeC _ = error + "copilot-c99 (test): Input variables of type struct are not yet supported." + +-- | C variable declaration for values of a given type. +varDeclC :: Typed a => Type a -> String -> String +varDeclC Bool v = "bool " ++ v +varDeclC Int8 v = "int8_t " ++ v +varDeclC Int16 v = "int16_t " ++ v +varDeclC Int32 v = "int32_t " ++ v +varDeclC Int64 v = "int64_t " ++ v +varDeclC Word8 v = "uint8_t " ++ v +varDeclC Word16 v = "uint16_t " ++ v +varDeclC Word32 v = "uint32_t " ++ v +varDeclC Word64 v = "uint64_t " ++ v +varDeclC Float v = "float " ++ v +varDeclC Double v = "double " ++ v +varDeclC t@(Array tE) v = + typeC tE ++ " " ++ v ++ "[" ++ show (tylength t) ++ "]" +varDeclC _ _ = error + "copilot-c99 (test): Input variables of type struct are not yet supported." + +-- | Expression that calculates the size of a variable of a given type. +sizeC :: Typed a => Type a -> String +sizeC Bool = "sizeof(bool)" +sizeC Int8 = "sizeof(int8_t)" +sizeC Int16 = "sizeof(int16_t)" +sizeC Int32 = "sizeof(int32_t)" +sizeC Int64 = "sizeof(int64_t)" +sizeC Word8 = "sizeof(uint8_t)" +sizeC Word16 = "sizeof(uint16_t)" +sizeC Word32 = "sizeof(uint32_t)" +sizeC Word64 = "sizeof(uint64_t)" +sizeC Float = "sizeof(float)" +sizeC Double = "sizeof(double)" +sizeC t@(Array tE) = show (tylength t) ++ "* sizeof(" ++ typeC tE ++ ")" +sizeC _ = error + "copilot-c99 (test): Input variables of type struct are not yet supported." + +-- | Show a value of a given type in C. +class CShow s where + cshow :: s -> String + +instance CShow Int8 where + cshow = show + +instance CShow Int16 where + cshow = show + +instance CShow Int32 where + cshow = show + +instance CShow Int64 where + cshow = show + +instance CShow Word8 where + cshow = show + +instance CShow Word16 where + cshow = show + +instance CShow Word32 where + cshow = show + +instance CShow Word64 where + cshow = show + +instance CShow Float where + cshow = show + +instance CShow Double where + cshow = show + +instance CShow Bool where + cshow True = "true" + cshow False = "false" + +instance CShow t => CShow (Array n t) where + cshow a = intercalate "," $ map cshow $ arrayelems a + +-- | Read a value of a given type in C. +class ReadableFromC a where + readFromC :: String -> a + +instance ReadableFromC Bool where + readFromC "0" = False + readFromC _ = True + +instance ReadableFromC Int8 where + readFromC = read + +instance ReadableFromC Int16 where + readFromC = read + +instance ReadableFromC Int32 where + readFromC = read + +instance ReadableFromC Int64 where + readFromC = read + +instance ReadableFromC Word8 where + readFromC = read + +instance ReadableFromC Word16 where + readFromC = read + +instance ReadableFromC Word32 where + readFromC = read + +instance ReadableFromC Word64 where + readFromC = read