copilot-c99 3.15 → 3.16
raw patch · 4 files changed
+1014/−2 lines, 4 filesdep +HUnitdep +QuickCheckdep +copilot-c99dep ~basedep ~copilot-coredep ~directoryPVP ok
version bump matches the API change (PVP)
Dependencies added: HUnit, QuickCheck, copilot-c99, process, random, test-framework, test-framework-hunit, test-framework-quickcheck2, unix
Dependency ranges changed: base, copilot-core, directory, pretty
API changes (from Hackage documentation)
Files
- CHANGELOG +4/−0
- copilot-c99.cabal +37/−2
- tests/Main.hs +18/−0
- tests/Test/Copilot/Compile/C99.hs +955/−0
CHANGELOG view
@@ -1,3 +1,7 @@+2023-07-07+ * Version bump (3.16). (#448)+ * Introduce testing infrastructure. (#413)+ 2023-05-07 * Version bump (3.15). (#438)
copilot-c99.cabal view
@@ -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
+ tests/Main.hs view
@@ -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+ ]
+ tests/Test/Copilot/Compile/C99.hs view
@@ -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 <stdio.h>"+ , "#include <stdint.h>"+ , "#include <stdbool.h>"+ , "#include <string.h>"+ , "#include <inttypes.h>"+ , "#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