Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CLI upgrade for more control and less duplication #691

Merged
merged 13 commits into from
Mar 31, 2025
Merged
3 changes: 3 additions & 0 deletions .github/workflows/build.yml
Original file line number Diff line number Diff line change
@@ -64,6 +64,9 @@ jobs:
# if we run this in nix build we often get killed due to oom in ci
- name: run ethereum tests
run: nix develop --command bash -c "cabal --active-repositories=:none run ethereum-tests"
# if we run this in nix build, it complains about running in a sandbox
- name: run cli tests
run: nix develop --command bash -c "cabal --active-repositories=:none run cli-test"

build-windows-bitwuzla:
name: bitwuzla-build (win64 target)
3 changes: 3 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -45,6 +45,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
- Allow user to change the verbosity level via `--verb`. For the moment, this is only to
print some warnings related to zero-address dereference and to print `hemv test`'s
output in case of failure
- Simple test cases for the CLI

## Fixed
- We now try to simplify expressions fully before trying to cast them to a concrete value
@@ -76,6 +77,8 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
determining when (Eq a b) is true when a==b modulo commutativity
- `hevm test`'s flag ` --verbose` is now `--verb`, which also increases verbosity
for other elements of the system
- We now use Options.Applicative and a rather different way of parsing CLI options.
This should give us much better control over the CLI options and their parsing.

## [0.54.2] - 2024-12-12

704 changes: 389 additions & 315 deletions cli/cli.hs

Large diffs are not rendered by default.

37 changes: 33 additions & 4 deletions hevm.cabal
Original file line number Diff line number Diff line change
@@ -12,7 +12,7 @@ homepage:
license:
AGPL-3.0-only
author:
dxo, Martin Lundfall, Mikael Brockman
dxo, Martin Lundfall, Mikael Brockman, Martin Blicha, Zoe Paraskevopoulou, Mate Soos
maintainer:
git@d-xo.org
category:
@@ -89,6 +89,7 @@ common shared

library
import: shared
default-language: GHC2021
exposed-modules:
EVM,
EVM.ABI,
@@ -190,6 +191,7 @@ library

executable hevm
import: shared
default-language: GHC2021
hs-source-dirs:
cli
main-is:
@@ -203,21 +205,23 @@ executable hevm
base,
bytestring,
data-dword,
directory,
directory >= 1.3.6 && < 1.4,
filepath,
hevm,
optparse-generic,
optparse-applicative >= 0.18.0.0 && < 0.20.0.0,
text,
optics-core,
githash,
githash >= 0.1.5 && < 0.2,
witch,
unliftio-core,
with-utf8,
split,

--- Test Helpers ---

common test-base
import: shared
default-language: GHC2021
hs-source-dirs:
test
other-modules:
@@ -254,13 +258,15 @@ common test-base

library test-utils
import: test-base
default-language: GHC2021
exposed-modules:
EVM.Test.Utils
EVM.Test.Tracing
EVM.Test.BlockchainTests

common test-common
import: test-base
default-language: GHC2021
if flag(devel)
ghc-options: -threaded -with-rtsopts=-N
build-depends:
@@ -274,6 +280,7 @@ common test-common

test-suite test
import: test-common
default-language: GHC2021
type:
exitcode-stdio-1.0
main-is:
@@ -291,22 +298,44 @@ test-suite test
-- suite to make it easy to skip them when running nix-build
test-suite rpc-tests
import: test-common
default-language: GHC2021
type:
exitcode-stdio-1.0
main-is:
rpc.hs

test-suite ethereum-tests
import: test-common
default-language: GHC2021
type:
exitcode-stdio-1.0
main-is:
BlockchainTests.hs

test-suite cli-test
type:
exitcode-stdio-1.0
default-language: GHC2021
hs-source-dirs:
test
main-is:
clitest.hs
build-depends:
base,
hevm,
hspec,
process,
text,
bytestring,
filepath,
split,
here,

--- Benchmarks ---

benchmark bench
import: shared
default-language: GHC2021
type:
exitcode-stdio-1.0
main-is:
5 changes: 3 additions & 2 deletions src/EVM/Solidity.hs
Original file line number Diff line number Diff line change
@@ -50,7 +50,7 @@
import Control.Applicative
import Control.Monad
import Control.Monad.IO.Unlift
import Data.Aeson hiding (json)

Check warning on line 53 in src/EVM/Solidity.hs

GitHub Actions / build (windows-latest)

Module ‘Data.Aeson’ does not export ‘json’
import Data.Aeson.Types
import Data.Aeson.Optics
import Data.Aeson.Key qualified as Key
@@ -399,8 +399,9 @@
functionAbi f = do
json <- solc Solidity ("contract ABI { function " <> f <> " public {}}")
let (Contracts sol, _, _) = fromMaybe
(internalError . T.unpack $ "unable to parse solc output:\n" <> json)
(readStdJSON json)
(internalError . T.unpack $ "while trying to parse function signature `"
<> f <> "`, unable to parse solc output:\n" <> json)
(readStdJSON json)
case Map.toList (fromJust (Map.lookup "hevm.sol:ABI" sol)).abiMap of
[(_,b)] -> pure b
_ -> internalError "unexpected abi format"
1 change: 0 additions & 1 deletion src/EVM/UnitTest.hs
Original file line number Diff line number Diff line change
@@ -51,7 +51,6 @@ data UnitTestOptions s = UnitTestOptions
, maxIter :: Maybe Integer
, askSmtIters :: Integer
, smtTimeout :: Maybe Natural
, solver :: Maybe Text
, match :: Text
, dapp :: DappInfo
, testParams :: TestVMParams
1 change: 0 additions & 1 deletion test/EVM/Test/Utils.hs
Original file line number Diff line number Diff line change
@@ -58,7 +58,6 @@ testOpts solvers root buildOutput match maxIter allowFFI rpcinfo = do
, maxIter = maxIter
, askSmtIters = 1
, smtTimeout = Nothing
, solver = Nothing
, match = match
, testParams = params
, dapp = srcInfo
119 changes: 119 additions & 0 deletions test/clitest.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,119 @@
{-# 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 (readProcess, readProcessWithExitCode)
import System.FilePath ((</>))
import System.Exit (ExitCode(..))
import Data.List.Split (splitOn)
import Data.Text qualified as T
import Data.String.Here

import EVM.Solidity
import EVM.Effects
import EVM.Types


main :: IO ()
main = do
hspec $
describe "CLI" $ do
it "hevm help works" $ do
(exitCode, stdout, stderr) <- 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 = bsToHex symbBin
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", symbHex] ""
stdout `shouldContain` "Discovered the following"
exitCode `shouldBe` ExitFailure 1

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

it "hevm equivalence tutorial works -- FAIL" $ do
let torun = splitOn " " "equivalence --code-a 60003560000260005260016000f3 --code-b 7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff60005260016000f3"
(exitCode, stdout, stderr) <- 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 = 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 = bsToHex b
(exitCode, stdout, stderr) <- 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, stderr) <- readProcessWithExitCode "cabal" (["run", "exe:hevm", "--" ] ++ torun) ""
stdout `shouldContain` "Return: 0x64"
exitCode `shouldBe` ExitSuccess

it "warning on zero address" $ do
Just c <- runApp $ solcRuntime (T.pack "C") (T.pack [i|
contract Target {
function get() external view returns (uint256) {
return 55;
}
}
contract C {
Target mm;
function retFor() public returns (uint256) {
Target target = Target(address(0));
uint256 ret = target.get();
assert(ret == 4);
return ret;
}
}
|])
let hexStr = bsToHex c
(exitCode, stdout, stderr) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--code", hexStr] ""
stdout `shouldContain` "Warning: fetching contract at address 0"