{-# LANGUAGE QuasiQuotes #-}

module Main where

{-|
Description : CLI tests

This module contains simple CLI test cases to make sure we don't accidentally
break the hevm CLI interface.

-}

import Test.Hspec
import System.Process (readProcessWithExitCode)
import System.Exit (ExitCode(..))
import Data.List.Split (splitOn)
import Data.Text qualified as T
import Data.String.Here
import System.IO.Temp
import System.Directory (doesFileExist, removeFile)

import EVM.Solidity
import EVM.Types qualified as Types
import EVM.Effects
import EVM.Test.Utils

testEnv :: Env
testEnv = Env { config = defaultConfig {
  dumpQueries = False
  , dumpExprs = False
  , dumpEndStates = False
  , debug = False
  , dumpTrace = False
  , decomposeStorage = True
  , verb = 1
  } }

runForge :: FilePath -> [String] -> IO (ExitCode, String, String)
runForge testFile extraOptions = do
  withSystemTempDirectory "dapp-test" $ \root -> do
    let projectType = Foundry
    ret <- runEnv testEnv $ compileWithForge root testFile
    case ret of
      Left e -> do
        putStrLn e
        Types.internalError $ "Error compiling test file " <> show testFile <> " in directory "
          <> show root <> " using project type " <> show projectType
      Right _ -> do
        let options = ["run", "exe:hevm", "--", "test" , "--root", root] <> extraOptions
        (exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" options ""
        pure (exitCode, stdout, stderr)

main :: IO ()
main = do
  hspec $
    describe "CLI" $ do
      it "hevm help works" $ do
        (_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "--help"] ""
        stdout `shouldContain` "Usage: hevm"
        stdout `shouldContain` "test"
        stdout `shouldContain` "equivalence"
        stdout `shouldContain` "symbolic"
        stdout `shouldContain` "exec"
        stdout `shouldContain` "version"

      it "hevm symbolic tutorial works -- FAIL" $ do
        Just symbBin <- runApp $ solcRuntime (T.pack "MyContract") (T.pack [i|
          contract MyContract {
            function simple_symb() public pure {
              uint i;
              i = 1;
              assert(i == 2);
            }
          }
        |])
        let symbHex = Types.bsToHex symbBin
        (exitCode, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex] ""
        stdout `shouldContain` "Discovered the following"
        exitCode `shouldBe` ExitFailure 1

        (exitCode2, stdout2, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex, "--sig", "nonexistent()"] ""
        stdout2 `shouldContain` "QED"
        exitCode2 `shouldBe` ExitSuccess

      it "hevm equivalence tutorial works -- FAIL" $ do
        let torun = splitOn " " "equivalence --code-a 60003560000260005260016000f3 --code-b 7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff60005260016000f3"
        (exitCode, stdout, _) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
        stdout `shouldContain` "Not equivalent"
        stdout `shouldContain` "FAIL"
        exitCode `shouldBe` ExitFailure 1

      it "hevm equivalence tutorial works -- PASS" $ do
        Just a <- runApp $ solcRuntime (T.pack "MyContract") (T.pack [i|
          contract MyContract {
            mapping (address => uint) balances;
            function my_adder(address recv, uint amt) public {
              if (balances[recv] + amt >= 100) { revert(); }
              balances[recv] += amt;
            }
          }
        |])
        let aHex = Types.bsToHex a
        Just b <- runApp $ solcRuntime (T.pack "MyContract") (T.pack [i|
          contract MyContract {
            mapping (address => uint) balances;
            function my_adder(address recv, uint amt) public {
              if (balances[recv] + amt >= 100) { revert(); }
              balances[recv] += amt/2;
              balances[recv] += amt/2;
              if (amt % 2 != 0) balances[recv]++;
            }
          }
        |])
        let bHex = Types.bsToHex b
        (exitCode, stdout, _) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--", "equivalence" , "--code-a", aHex, "--code-b", bHex ]) ""
        stdout `shouldContain` "No discrepancies found"
        stdout `shouldContain` "PASS"
        exitCode `shouldBe` ExitSuccess

      it "hevm concrete tutorial works" $ do
        let torun = splitOn " " "exec --code 0x647175696e6550383480393834f3 --gas 0xff"
        (exitCode, stdout, _) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
        stdout `shouldContain` "Return: 0x64"
        exitCode `shouldBe` ExitSuccess

      it "empty solver is always unknown" $ do
        Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
           contract C {
             function myfun(uint a) public returns (uint) {
                 uint ret = 4*a;
                 assert(ret == 4);
                 return ret;
             }
           }
          |])
        let hexStr = Types.bsToHex c
        (_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--solver", "empty", "--code", hexStr] ""
        stdout `shouldContain` "SMT solver says: Result unknown by SMT solver"

      -- file "devcon_example.yul" from "eq-all-yul-optimization-tests" in test.hs
      -- we check that at least one UNSAT cache hit happens, i.e. the unsat cache is not
      -- completely broken
      it "unsat-cache" $ do
        let a = [i| {
          calldatacopy(0,0,1024)
              sstore(0, array_sum(calldataload(0)))
              function array_sum(x) -> sum {
                  let length := calldataload(x)
                  for { let i := 0 } lt(i, length) { i := add(i, 1) } {
                      sum := add(sum, array_load(x, i))
                  }
              }
              function array_load(x, i) -> v {
                  let len := calldataload(x)
                  if iszero(lt(i, len)) { revert(0, 0) }
                  let data := add(x, 0x20)
                  v := calldataload(add(data, mul(i, 0x20)))
              }
          } |]
        let b = [i| {
          calldatacopy(0,0,1024)
               {
                   let _1 := calldataload(0)
                   let sum := 0
                   let length := calldataload(_1)
                   let i := 0
                   for { } true { i := add(i, 1) }
                   {
                       let _2 := iszero(lt(i, length))
                       if _2 { break }
                       _2 := 0
                       sum := add(sum, calldataload(add(add(_1, shl(5, i)), 0x20)))
                   }
                   sstore(0, sum)
               }
           } |]
        Right aPrgm <- yul (T.pack "") $ T.pack a
        Right bPrgm <- yul (T.pack "") $ T.pack b
        let hexStrA = Types.bsToHex aPrgm
            hexStrB = Types.bsToHex bPrgm
        (_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "equivalence", "--num-solvers", "1", "--debug", "--code-a", hexStrA, "--code-b", hexStrB] ""
        stdout `shouldContain` "Qed found via cache"
      it "crash-of-hevm" $ do
        let hexStrA = "608060405234801561001057600080fd5b506004361061002b5760003560e01c8063efa2978514610030575b600080fd5b61004361003e3660046102ad565b610045565b005b60006100508561007a565b9050600061005d866100a8565b905080821461006e5761006e61034c565b50505050505050505050565b600061008761032e6103aa565b8261009457610197610098565b61013e5b6100a291906103e2565b92915050565b60006100b561032e6103aa565b6100be906103aa565b6100c7906103aa565b82806100d1575060005b806100da575060005b61013157605a6100ea60006103aa565b6100f3906103aa565b6100ff6001605a610404565b61010b6001605a610404565b61011891166101976103e2565b6101229190610493565b61012c9190610493565b610149565b604061013f8161013e6103e2565b6101499190610493565b61015391906103e2565b61016061032e60006103e2565b83801561016b575060015b15801590610177575060015b80156101a05750831515801561018b575060015b15158015610197575060015b806101a0575060005b610251576101976101b3605a602d610493565b602d60006101c2600182610493565b6101cd906001610404565b6101d8906001610404565b6101e1906103aa565b6101ea906103aa565b6101f491906103e2565b6101ff90605a610404565b604e61020c8160016103e2565b6102169190610493565b61022490600116605a610404565b1661022e906103aa565b61023891906103e2565b6102429190610493565b61024c9190610493565b610283565b604561025f8161013e6103e2565b6102699190610493565b60456102778161013e6103e2565b6102819190610493565b165b61028d91906103e2565b1692915050565b80358015155b81146100a257600080fd5b80358061029a565b600080600080600080600080610100898b0312156102ca57600080fd5b6102d48a8a610294565b97506102e38a60208b01610294565b96506102f28a60408b016102a5565b95506103018a60608b016102a5565b94506103108a60808b01610294565b935061031f8a60a08b016102a5565b925061032e8a60c08b01610294565b915061033d8a60e08b016102a5565b90509295985092959890939650565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60007f800000000000000000000000000000000000000000000000000000000000000082036103db576103db61037b565b5060000390565b818103600083128015838313168383129190911617156100a2576100a261037b565b60008261043a577f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f800000000000000000000000000000000000000000000000000000000000000082147fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff8414161561048e5761048e61037b565b500590565b80820160008212801584831290811690159190911617156100a2576100a261037b56fea26469706673582212200a37769e5bf4b8b890caac8ab643126d55feb821a0201d2f674203f23fa666ad64736f6c634300081e0033"

        (exitCode, _, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", hexStrA] ""
        stderr `shouldNotContain` "CallStack"
        exitCode `shouldBe` ExitSuccess

      -- both should fail with address 0x1234 -- a SPECIFIC address, not a ranomly generated one
      it "keccak-assumptions-setup" $ do
        (exitCode, stdout, stderr) <- runForge "test/contracts/fail/keccak-preimage-setup.sol" []
        stderr `shouldNotContain` "CallStack"
        stdout `shouldContain` "[validated]"
        stdout `shouldContain` "0x0000000000000000000000000000000000001234"
        exitCode `shouldBe` (ExitFailure 1)
      it "keccak-assumptions-constructor" $ do
        (exitCode, stdout, stderr) <- runForge "test/contracts/fail/keccak-preimage-constructor.sol" []
        stderr `shouldNotContain` "CallStack"
        stdout `shouldContain` "[validated]"
        stdout `shouldContain` "0x0000000000000000000000000000000000001234"
        exitCode `shouldBe` (ExitFailure 1)
      it "keccak-wrong-preimage" $ do
        (exitCode, stdout, stderr) <- runForge "test/contracts/fail/keccak-wrong-preimage.sol" []
        stderr `shouldNotContain` "CallStack"
        stdout `shouldContain` "[not reproducible]"
        exitCode `shouldBe` (ExitFailure 1)
      it "only-deployed-contracts" $ do
        (_, stdout, stderr) <- runForge "test/contracts/pass/only-deployed-contracts.sol" ["--only-deployed"]
        stderr `shouldNotContain` "CallStack"
        stdout `shouldContain` "[PASS]"
      it "only-deployed-contracts-force-addr" $ do
        (_, stdout, stderr) <- runForge "test/contracts/pass/only-deployed-force-addr.sol" ["--only-deployed"]
        stderr `shouldNotContain` "CallStack"
        stdout `shouldContain` "[FAIL]"
        stdout `shouldContain` "[validated]"
        stderr `shouldNotContain` "not reproducible"
      it "should-fail" $ do
        (_, stdout, stderr) <- runForge "test/contracts/fail/should-fail.sol" []
        stderr `shouldNotContain` "CallStack"
        stdout `shouldContain` "[FAIL]"
        stdout `shouldContain` "[validated]"
      it "dump unsolved" $ do
        -- >>> (139487132679483*2347234698674) % 982374892374389278894734
        -- 278198683154907855159120
        Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
           contract C {
             function stuff(uint a, uint b) public returns (uint) {
                 uint c = 0;
                 unchecked {
                 c = (a * b) % 982374892374389278894734;
                 }
                 assert (c != 278198683154907855159120);
                 return c;
             }
           }
          |])
        let hexStr = Types.bsToHex c
        _ <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", hexStr, "--smttimeout", "1", "--dump-unsolved", "."] ""
        let filename = "query-unsolved-0.smt2"
        fileExists <- doesFileExist filename
        shouldBe fileExists True
        removeFile filename
      it "rpc-mock" $ do
        (_, stdout, stderr) <- runForge "test/contracts/fail/rpc-test.sol"
          ["--rpc", "http://mock.mock", "--prefix", "test_attack_symbolic"
          , "--number", "10307563", "--mock-file", "test/contracts/fail/rpc-test-mock.json"]
        stdout `shouldContain` "[FAIL]"
        stderr `shouldNotContain` "CallStack"