content: {-# 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.IO as IO
  import qualified System.Process as Proc
  
  -- Modules being tested
  import           Lang.Crucible.LLVM.Internal (assertionsEnabled)
  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 =
    parseBitCodeFromFileWithWarnings file >>=
      \case
        Left err -> pure $ Left $ "Couldn't parse LLVM bitcode from file"
                                  ++ file ++ "\n" ++ show err
        Right (m, warnings) -> do
          unless (null warnings) $
            IO.hPrint IO.stderr $ ppParseWarnings warnings
          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"
           [ -- See Note [Asserts] in crucible-llvm
             testCase "assertions enabled" $ do
               assertsEnabled <- assertionsEnabled
               assertBool "assertions should be enabled" assertsEnabled
           , 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
  