{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module Main where
-- Crucible
import Lang.Crucible.FunctionHandle ( newHandleAllocator )
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Some
import Data.Parameterized.NatRepr
import Data.Parameterized.SymbolRepr ( SomeSym(SomeSym) )
-- LLVM
import qualified Text.LLVM.AST as L
import Text.LLVM.AST (Module)
import Data.LLVM.BitCode
-- Tasty
import Test.Tasty
import Test.Tasty.HUnit
import qualified Test.Tasty.Options as TO
import qualified Test.Tasty.Runners as TR
import qualified Test.Tasty.Sugar as TS
-- General
import Control.Lens (view)
import Control.Monad
import Data.Either ( fromRight )
import Data.Maybe ( catMaybes )
import GHC.TypeLits
import qualified Data.Map.Strict as Map
import Data.Proxy ( Proxy(..) )
import qualified System.Directory as Dir
import System.Environment ( lookupEnv )
import System.Exit ( ExitCode(..) )
import System.FilePath ( (-<.>), splitExtension, splitFileName )
import qualified System.Process as Proc
-- Modules being tested
import Lang.Crucible.LLVM.MemModel ( mkMemVar )
import Lang.Crucible.LLVM.MemType
import Lang.Crucible.LLVM.Translation
import TestFunctions
import TestGlobals
import TestMemory
import TestTranslation
data LLVMAssembler (source :: Symbol) = LLVMAssembler String
deriving (Eq, Show)
instance TO.IsOption (SomeSym LLVMAssembler) where
defaultValue = SomeSym $ LLVMAssembler @"default" "llvm-as"
parseValue = Just . SomeSym . LLVMAssembler @"option"
optionName = pure "llvm-assembler"
optionHelp = pure $ unwords ["The LLVM assembler to use on .ll files"
,"(overrides the LLVM_AS environment variable,"
,"default is \"llvm-as\")"]
data Clang (source :: Symbol) = Clang String
deriving (Eq, Show)
instance TO.IsOption (SomeSym Clang) where
defaultValue = SomeSym $ Clang @"default" "clang"
parseValue = Just . SomeSym . Clang @"option"
optionName = pure "clang"
optionHelp = pure $ unwords ["The clang binary to use to compile C files"
,"(overrides the CLANG environment variable,"
,"default is \"clang\")"]
optionSource :: opt (source :: Symbol) -> Proxy source
optionSource _ = Proxy
doProc :: String -> [String] -> IO ProcResult
doProc !exe !args = do
(exitCode, stdout, stderr) <- Proc.readProcessWithExitCode exe args ""
pure $ (exitCodeToInt exitCode, stdout, stderr)
where exitCodeToInt ExitSuccess = 0
exitCodeToInt (ExitFailure i) = i
type ProcResult = (Int, String, String)
assertProcSuccess :: String -> String -> ProcResult -> Assertion
assertProcSuccess msg file (exitCode, stdout, stderr) = do
when (exitCode /= 0) $ do
putStrLn $ msg ++ " " ++ file ++ " failure"
putStrLn stdout
putStrLn stderr
exitCode == 0 @? msg ++ " " ++ file ++ " attempt failed with " ++ show exitCode
-- | Compile a C file with clang, returning the exit code
compile :: Clang "executable" -> FilePath -> IO ProcResult
compile (Clang clang) !file = doProc clang ["-emit-llvm", "-g", "-O0", "-c", file]
-- | Assemble a ll file with llvm-as, returning the exit code
assemble :: LLVMAssembler "executable" -> FilePath -> FilePath -> IO ProcResult
assemble (LLVMAssembler llvm_as) !inputFile !outputFile =
doProc llvm_as ["-o", outputFile, inputFile]
-- | Parse an LLVM bit-code file.
-- Mostly copied from crucible-c.
parseLLVM :: FilePath -> IO (Either String Module)
parseLLVM !file =
parseBitCodeFromFile file >>=
\case
Left err -> pure $ Left $ "Couldn't parse LLVM bitcode from file"
++ file ++ "\n" ++ show err
Right m -> pure $ Right m
llvmTestIngredients :: [TR.Ingredient]
llvmTestIngredients = includingOptions [ TO.Option (Proxy @(SomeSym LLVMAssembler))
, TO.Option (Proxy @(SomeSym Clang))
] :
includingOptions TS.sugarOptions :
TS.sugarIngredients [cCube, lCube] <>
defaultIngredients
cCube, lCube :: TS.CUBE
cCube = TS.mkCUBE { TS.inputDirs = ["test/c"]
, TS.rootName = "*.c"
, TS.separators = "."
, TS.expectedSuffix = "checks"
}
lCube = cCube { TS.inputDirs = ["test/ll"]
, TS.rootName = "*.ll"
}
main :: IO ()
main = do
do testSweets <- concat <$> (mapM TS.findSugar [cCube, lCube])
fileTests <- TS.withSugarGroups testSweets testGroup $
\sweets _ expectation -> do
-- The expected file contains a list of the tests to run
-- on the LLVM translation.
checklist <- lines <$> readFile (TS.expectedFile expectation)
return $
testBuildTranslation (TS.rootFile sweets) $
(\getTrans -> testGroup "checks" $ map (transCheck getTrans) checklist)
defaultMainWithIngredients llvmTestIngredients $
testGroup "Tests"
[ functionTests
, globalTests
, memoryTests
, translationTests
, testGroup "Input Files" $ fileTests
]
testBuildTranslation :: FilePath -> (IO (Some ModuleTranslation) -> TestTree) -> [TestTree]
testBuildTranslation srcPath llvmTransTests =
-- n.b. srcPath may be a relative path
let (dName, srcName) = splitFileName srcPath
(fName, ext) = splitExtension srcName
bcPath = srcPath -<.> ".bc"
(_, bcName) = splitFileName bcPath
genBCName = case ext of
".c" -> "compile " <> fName
".ll" -> "assemble " <> fName
_ -> error $ "Cannot build LLVM bitcode file from a " ++ ext ++ " file"
parseBCName = "parse " ++ fName ++ " bitcode"
translateName = "translate " ++ fName
c_compile =
if (ext == ".c")
then
Just $ askOption $ \(SomeSym clangOption :: SomeSym Clang) ->
testCase genBCName $ do
clang <-
let src = optionSource clangOption in
case sameSymbol src (Proxy :: Proxy "option") of
Just Refl -> let Clang c = clangOption in return $ Clang c
_ -> case sameSymbol src (Proxy :: Proxy "default") of
Just Refl -> maybe (Clang "clang") Clang <$> lookupEnv "CLANG"
_ -> error $ "Unknown Clang specification type: " <> symbolVal src
assertProcSuccess "compile" srcPath =<<
Dir.withCurrentDirectory dName (compile clang srcName)
else Nothing
llvm_assemble =
if (ext == ".ll")
then Just $ askOption $ \(SomeSym assemblerOption :: SomeSym LLVMAssembler) ->
testCase genBCName $ do
llvm_as <-
let src = optionSource assemblerOption in
case sameSymbol src (Proxy :: Proxy "option") of
Just Refl -> let LLVMAssembler a = assemblerOption
in return $ LLVMAssembler a
_ -> case sameSymbol src (Proxy :: Proxy "default") of
Just Refl -> maybe (LLVMAssembler "llvm-as") LLVMAssembler <$>
lookupEnv "LLVM_AS"
_ -> error $ "Unknown LLVM Assembler specification type: " <> symbolVal src
assertProcSuccess "assemble" srcPath =<<
Dir.withCurrentDirectory dName (assemble llvm_as srcName bcName)
else Nothing
parse_bitcode =
testCase parseBCName $
parseLLVM bcPath >>= \case
Left err -> do
putStrLn $ "Failed to parse " ++ bcPath
putStrLn err
err @?= ""
Right _ -> pure ()
trans = do halloc <- newHandleAllocator
let ?transOpts = defaultTranslationOptions
memVar <- mkMemVar "buildTranslation_test_llvm_memory" halloc
m <- (translateModule halloc memVar =<<
(fromRight (error "parsing was already verified") <$> parseLLVM bcPath))
return m
translate_bitcode =
testCase translateName $ do
trans >>= \(Some modTrans) ->
not (null $ view modTransDefs modTrans) @? "Translation of " ++ bcPath ++ " was empty (failed?)"
in catMaybes
[ c_compile
, llvm_assemble
, Just $ after AllSucceed genBCName parse_bitcode
, Just $ after AllSucceed parseBCName translate_bitcode
, Just $ after AllSucceed translateName (llvmTransTests trans)
]
transCheck :: IO (Some ModuleTranslation) -> String -> TestTree
transCheck getTrans = \case
"extern_int" ->
testCase "valid global extern variable reference" $ do
Some t <- getTrans
Map.singleton (L.Symbol "extern_int") (Right (i32, Nothing)) @=?
Map.map snd (view globalInitMap t)
"x=42" ->
testCase "valid global integer symbol reference" $ do
Some t <- getTrans
Map.singleton (L.Symbol "x") (Right $ (i32, Just $ IntConst (knownNat @32) (BV.mkBV knownNat 42))) @=?
Map.map snd (view globalInitMap t)
"z.xx=17" ->
testCase "valid global struct field symbol reference" $ do
Some t <- getTrans
IntConst (knownNat @32) (BV.mkBV knownNat 17) @=?
case snd <$> Map.lookup (L.Symbol "z") (view globalInitMap t) of
Just (Right (_, Just (StructConst _ (x : _)))) -> x
_ -> IntConst (knownNat @1) (BV.zero knownNat)
"x uninitialized" ->
testCase "valid global unitialized variable reference" $ do
Some t <- getTrans
Map.singleton (L.Symbol "x") (Right $ (i32, Just $ ZeroConst i32)) @=?
Map.map snd (view globalInitMap t)
-- We're really just checking that the translation succeeds without
-- exceptions.
"" -> testCase "no additional checks" $ return ()
other -> testCase other $ assertFailure $ "Unknown check: " <> other