Support for truffle/embark using crytic-compile (#204)

pull/271/head
Gustavo Grieco 5 years ago committed by GitHub
parent 0314d40feb
commit 633155c86e
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
  1. 2
      .gitignore
  2. 7
      .travis.yml
  3. 9
      .travis/install-crytic-compile.sh
  4. 15
      README.md
  5. 1
      examples/solidity/basic/flags.json
  6. 2
      examples/solidity/coverage/harvey.sol
  7. 4
      examples/solidity/coverage/single.sol
  8. 22
      examples/solidity/truffle/metacoin/LICENSE
  9. 1
      examples/solidity/truffle/metacoin/contracts/.placeholder
  10. 8
      examples/solidity/truffle/metacoin/contracts/ConvertLib.sol
  11. 34
      examples/solidity/truffle/metacoin/contracts/MetaCoin.sol
  12. 14
      examples/solidity/truffle/metacoin/contracts/MetaCoinEchidna.sol
  13. 23
      examples/solidity/truffle/metacoin/contracts/Migrations.sol
  14. 5
      examples/solidity/truffle/metacoin/migrations/1_initial_migration.js
  15. 8
      examples/solidity/truffle/metacoin/migrations/2_deploy_contracts.js
  16. 1
      examples/solidity/truffle/metacoin/test/.placeholder
  17. 25
      examples/solidity/truffle/metacoin/test/TestMetacoin.sol
  18. 40
      examples/solidity/truffle/metacoin/test/metacoin.js
  19. 21
      examples/solidity/truffle/metacoin/truffle-config.js
  20. 91
      lib/Echidna/Solidity.hs
  21. 1
      package.yaml
  22. 2
      src/Main.hs
  23. 2
      src/test/Spec.hs

2
.gitignore vendored

@ -18,3 +18,5 @@ cabal.sandbox.config
.stack-work/
cabal.project.local
.HTF/
crytic-export/
echidna.cabal

@ -1,5 +1,8 @@
# Adapted from https://github.com/ChrisPenner/haskell-stack-travis-ci
language: minimal
language: python
python:
- 3.6
sudo: true
cache:
@ -21,6 +24,7 @@ matrix:
STACK_OPTS="--no-run-tests --extra-include-dirs=/usr/local/opt/readline/include --extra-lib-dirs=/usr/local/opt/readline/lib"
LDFLAGS=-L/usr/local/opt/readline/lib CFLAGS=-I/usr/local/opt/readline/include
os: osx
language: minimal
install:
- unset CC
@ -30,6 +34,7 @@ install:
- ./.travis/install-ghr.sh
- ./.travis/install-stack.sh
- ./.travis/install-solc.sh
- ./.travis/install-crytic-compile.sh
script:
- PATH=$HOME/.local/bin:$PATH

@ -0,0 +1,9 @@
if [ "$(uname)" != "Darwin" ]; then
rm -Rf crytic-compile
git clone https://github.com/crytic/crytic-compile --depth 1
cd crytic-compile
python setup.py install
cd ..
fi

@ -47,6 +47,21 @@ $ echidna-test examples/solidity/basic/flags.sol
Echidna should find a a call sequence that falisfies `echidna_sometimesfalse` and should be unable to find a falsifying input for `echidna_alwaystrue`.
### Truffle integration
Echidna can be used to test contracts compiled with [Truffle](https://truffleframework.com/) using [crytic-compile](https://github.com/crytic/crytic-compile). For instance,
we can uncover an integer overflow in the [Metacoin Truffle box](https://github.com/truffle-box/metacoin-box) using a
[contract with Echidna properties to test](examples/solidity/truffle/metacoin/contracts/MetaCoinEchidna.sol):
```
$ cd examples/solidity/truffle/metacoin
$ echidna-test . TEST
...
echidna_convert: failed!💥
Call sequence:
mint(57896044618658097711785492504343953926634992332820282019728792003956564819968)
```
### Configuration options
Echidna's CLI can be used to choose the contract to test and load a configuration file.

File diff suppressed because one or more lines are too long

@ -1,3 +1,5 @@
contract C {}
contract Foo {
bool state = true;
function f(int256 a, int256 b, int256 c) public returns (int256) {

@ -1,9 +1,9 @@
contract C {
bool state = true;
function f(uint x, uint y, uint z) public {
require(x == 12);
require(x == 42424242);
require(y == 8);
require(z == 0);
require(z == 123);
state = false;
return;
}

@ -0,0 +1,22 @@
The MIT License (MIT)
Copyright (c) 2018 Truffle
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.

@ -0,0 +1 @@
This is a placeholder file to ensure the parent directory in the git repository. Feel free to remove.

@ -0,0 +1,8 @@
pragma solidity >=0.4.25 <0.6.0;
library ConvertLib{
function convert(uint amount,uint conversionRate) internal pure returns (uint convertedAmount)
{
return amount * conversionRate;
}
}

@ -0,0 +1,34 @@
pragma solidity >=0.4.25 <0.6.0;
import "./ConvertLib.sol";
// This is just a simple example of a coin-like contract.
// It is not standards compatible and cannot be expected to talk to other
// coin/token contracts. If you want to create a standards-compliant
// token, see: https://github.com/ConsenSys/Tokens. Cheers!
contract MetaCoin {
mapping (address => uint) balances;
event Transfer(address indexed _from, address indexed _to, uint256 _value);
constructor() public {
//balances[tx.origin] = 10000;
}
function sendCoin(address receiver, uint amount) public returns(bool sufficient) {
if (balances[msg.sender] < amount) return false;
balances[msg.sender] -= amount;
balances[receiver] += amount;
emit Transfer(msg.sender, receiver, amount);
return true;
}
function getBalanceInEth(address addr) public view returns(uint){
return ConvertLib.convert(getBalance(addr),2);
}
function getBalance(address addr) public view returns(uint) {
return balances[addr];
}
}

@ -0,0 +1,14 @@
pragma solidity >=0.4.25 <0.6.0;
import "./MetaCoin.sol";
contract TEST is MetaCoin {
function mint(uint ammount) public {
balances[msg.sender] = ammount;
}
function echidna_convert() public view returns (bool) {
return getBalanceInEth(msg.sender) >= getBalance(msg.sender);
}
}

@ -0,0 +1,23 @@
pragma solidity >=0.4.25 <0.6.0;
contract Migrations {
address public owner;
uint public last_completed_migration;
modifier restricted() {
if (msg.sender == owner) _;
}
constructor() public {
owner = msg.sender;
}
function setCompleted(uint completed) public restricted {
last_completed_migration = completed;
}
function upgrade(address new_address) public restricted {
Migrations upgraded = Migrations(new_address);
upgraded.setCompleted(last_completed_migration);
}
}

@ -0,0 +1,5 @@
const Migrations = artifacts.require("Migrations");
module.exports = function(deployer) {
deployer.deploy(Migrations);
};

@ -0,0 +1,8 @@
const ConvertLib = artifacts.require("ConvertLib");
const MetaCoin = artifacts.require("MetaCoin");
module.exports = function(deployer) {
deployer.deploy(ConvertLib);
deployer.link(ConvertLib, MetaCoin);
deployer.deploy(MetaCoin);
};

@ -0,0 +1 @@
This is a placeholder file to ensure the parent directory in the git repository. Feel free to remove.

@ -0,0 +1,25 @@
pragma solidity >=0.4.25 <0.6.0;
import "truffle/Assert.sol";
import "truffle/DeployedAddresses.sol";
import "../contracts/MetaCoin.sol";
contract TestMetacoin {
function testInitialBalanceUsingDeployedContract() public {
MetaCoin meta = MetaCoin(DeployedAddresses.MetaCoin());
uint expected = 10000;
Assert.equal(meta.getBalance(tx.origin), expected, "Owner should have 10000 MetaCoin initially");
}
function testInitialBalanceWithNewMetaCoin() public {
MetaCoin meta = new MetaCoin();
uint expected = 10000;
Assert.equal(meta.getBalance(tx.origin), expected, "Owner should have 10000 MetaCoin initially");
}
}

@ -0,0 +1,40 @@
const MetaCoin = artifacts.require("MetaCoin");
contract('MetaCoin', (accounts) => {
it('should put 10000 MetaCoin in the first account', async () => {
const metaCoinInstance = await MetaCoin.deployed();
const balance = await metaCoinInstance.getBalance.call(accounts[0]);
assert.equal(balance.valueOf(), 10000, "10000 wasn't in the first account");
});
it('should call a function that depends on a linked library', async () => {
const metaCoinInstance = await MetaCoin.deployed();
const metaCoinBalance = (await metaCoinInstance.getBalance.call(accounts[0])).toNumber();
const metaCoinEthBalance = (await metaCoinInstance.getBalanceInEth.call(accounts[0])).toNumber();
assert.equal(metaCoinEthBalance, 2 * metaCoinBalance, 'Library function returned unexpected function, linkage may be broken');
});
it('should send coin correctly', async () => {
const metaCoinInstance = await MetaCoin.deployed();
// Setup 2 accounts.
const accountOne = accounts[0];
const accountTwo = accounts[1];
// Get initial balances of first and second account.
const accountOneStartingBalance = (await metaCoinInstance.getBalance.call(accountOne)).toNumber();
const accountTwoStartingBalance = (await metaCoinInstance.getBalance.call(accountTwo)).toNumber();
// Make transaction from first account to second.
const amount = 10;
await metaCoinInstance.sendCoin(accountTwo, amount, { from: accountOne });
// Get balances of first and second account after the transactions.
const accountOneEndingBalance = (await metaCoinInstance.getBalance.call(accountOne)).toNumber();
const accountTwoEndingBalance = (await metaCoinInstance.getBalance.call(accountTwo)).toNumber();
assert.equal(accountOneEndingBalance, accountOneStartingBalance - amount, "Amount wasn't correctly taken from the sender");
assert.equal(accountTwoEndingBalance, accountTwoStartingBalance + amount, "Amount wasn't correctly sent to the receiver");
});
});

@ -0,0 +1,21 @@
module.exports = {
// Uncommenting the defaults below
// provides for an easier quick-start with Ganache.
// You can also follow this format for other networks;
// see <http://truffleframework.com/docs/advanced/configuration>
// for more details on how to specify configuration options!
/*
networks: {
development: {
host: "127.0.0.1",
port: 7545,
network_id: "*"
},
test: {
host: "127.0.0.1",
port: 7545,
network_id: "*"
}
}
*/
};

@ -16,18 +16,18 @@ import Control.Monad.Reader (MonadReader)
import Control.Monad.State.Strict (execStateT)
import Data.Aeson (Value(..))
import Data.ByteString.Lens (packedChars)
import Data.DoubleWord (Int256, Word256)
import Data.Foldable (toList)
import Data.Has (Has(..))
import Data.List (find, nub, partition)
import Data.List.Lens (prefixed, suffixed)
import Data.Maybe (isNothing)
import Data.Maybe (isNothing, catMaybes)
import Data.Monoid ((<>))
import Data.Text (Text, isPrefixOf, pack, unpack)
import Data.Text (Text, isPrefixOf, isSuffixOf)
import Data.Text.Lens (unpacked)
import Data.Text.Read (decimal, hexadecimal)
import System.Process (readCreateProcess, std_err, proc, StdStream(..))
import Data.Text.Read (decimal)
import System.Process (StdStream(..), readCreateProcess, proc, std_err)
import System.IO (openFile, IOMode(..))
import System.IO.Temp (writeSystemTempFile)
import Echidna.ABI (SolSignature)
import Echidna.Exec (execTx)
@ -84,21 +84,19 @@ data SolConf = SolConf { _contractAddr :: Addr -- ^ Contract address to us
}
makeLenses ''SolConf
-- | Given a file, try to compile it and get a list of its contracts, throwing exceptions if necessary.
-- | Given a file, use its extenstion to check if it is a precompiled contract or try to compile it and
-- get a list of its contracts, throwing exceptions if necessary.
contracts :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x) => FilePath -> m [SolcContract]
contracts fp = do
a <- view (hasLens . solcArgs)
q <- view (hasLens . quiet)
contracts fp = let usual = ["--solc-disable-warnings", "--export-format", "solc"] in do
a <- view (hasLens . solcArgs)
q <- view (hasLens . quiet)
ls <- view (hasLens . solcLibs)
pure (a, q, ls) >>= liftIO . solc >>= (\case
Nothing -> throwM CompileFailure
Just m -> pure . toList $ fst m) where
usual = ["--combined-json=bin-runtime,bin,srcmap,srcmap-runtime,abi,ast", fp]
solc (a, q, ls) = do
stderr <- if q then UseHandle <$> openFile "/dev/null" WriteMode
else pure Inherit
readSolc =<< writeSystemTempFile ""
=<< readCreateProcess (proc "solc" $ usual <> words (a ++ linkLibraries ls)) {std_err = stderr} ""
let solargs = a ++ linkLibraries ls & (usual ++) .
(\sa -> if null sa then [] else ["--solc-args", sa])
maybe (throwM CompileFailure) (pure . toList . fst) =<< liftIO (do
stderr <- if q then UseHandle <$> openFile "/dev/null" WriteMode else pure Inherit
_ <- readCreateProcess (proc "crytic-compile" $ solargs |> fp) {std_err = stderr} ""
readSolc "crytic-export/combined_solc.json")
addresses :: (MonadReader x m, Has SolConf x) => m [AbiValue]
@ -125,7 +123,8 @@ loadLibraries (l:ls) la d vm = loadLibraries ls (la + 1) d =<< loadRest
-- | Generate a string to use as argument in solc to link libraries starting from addrLibrary
linkLibraries :: [String] -> String
linkLibraries [] = ""
linkLibraries ls = "--libraries " ++ concat (imap (\i x -> concat [x, ":", show $ addrLibrary + (toEnum i :: Addr) , ","]) ls)
linkLibraries ls = "--libraries " ++
iconcatMap (\i x -> concat [x, ":", show $ addrLibrary + toEnum i, ","]) ls
-- | Given an optional contract name and a list of 'SolcContract's, try to load the specified
-- contract, or, if not provided, the first contract in the list, into a 'VM' usable for Echidna
@ -141,7 +140,7 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
liftIO $ do
when (isNothing name && length cs > 1 && not q) $
putStrLn "Multiple contracts found in file, only analyzing the first"
unless q . putStrLn $ "Analyzing contract: " <> unpack (c ^. contractName)
unless q . putStrLn $ "Analyzing contract: " <> c ^. contractName . unpacked
-- Local variables
(SolConf ca d ads bala balc pref _ libs _) <- view hasLens
@ -151,7 +150,7 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
(tests, funs) = partition (isPrefixOf pref . fst) abi
-- Select libraries
ls <- mapM (choose cs . Just . pack) libs
ls <- mapM (choose cs . Just . T.pack) libs
-- Make sure everything is ready to use, then ship it
mapM_ (uncurry ensure) [(abi, NoFuncs), (tests, NoTests), (funs, OnlyTests)] -- ABI checks
@ -165,7 +164,7 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
where choose [] _ = throwM NoContracts
choose (c:_) Nothing = return c
choose _ (Just n) = maybe (throwM $ ContractNotFound n) pure $
find ((n ==) . view contractName) cs
find (isSuffixOf n . view contractName) cs
fallback = ("",[])
-- | Given a file and an optional contract name, compile the file as solidity, then, if a name is
@ -173,9 +172,12 @@ loadSpecified name cs = let ensure l e = if l == mempty then throwM e else pure
-- the first contract in the file. Take said contract and return an initial VM state with it loaded,
-- its ABI (as 'SolSignature's), and the names of its Echidna tests. NOTE: unlike 'loadSpecified',
-- contract names passed here don't need the file they occur in specified.
loadSolidity :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x)
--loadSolidity :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x)
-- => FilePath -> Maybe Text -> m (VM, [SolSignature], [Text])
--loadSolidity fp name = contracts fp >>= loadSpecified name
loadWithCryticCompile :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x)
=> FilePath -> Maybe Text -> m (VM, [SolSignature], [Text])
loadSolidity fp name = contracts fp >>= loadSpecified ((pack fp <>) <$> name)
loadWithCryticCompile fp name = contracts fp >>= loadSpecified name
-- | Given the results of 'loadSolidity', assuming a single-contract test, get everything ready
-- for running a 'Campaign' against the tests found.
@ -188,38 +190,41 @@ prepareForTest (v, a, ts) = let r = v ^. state . contract in
-- a testing function.
loadSolTests :: (MonadIO m, MonadThrow m, MonadReader x m, Has SolConf x)
=> FilePath -> Maybe Text -> m (VM, World, [(Text, Addr)])
loadSolTests fp name = loadSolidity fp name >>= prepareForTest
loadSolTests fp name = loadWithCryticCompile fp name >>= prepareForTest
mkValidAbiInt :: Int -> Int256 -> Maybe AbiValue
mkValidAbiInt i x = if abs x <= 2 ^ (i - 1) - 1 then Just $ AbiInt i x else Nothing
mkValidAbiUInt :: Int -> Word256 -> Maybe AbiValue
mkValidAbiUInt i x = if x <= 2 ^ i - 1 then Just $ AbiUInt i x else Nothing
-- | Given a list of 'SolcContract's, try to parse out string and integer literals
extractConstants :: [SolcContract] -> [AbiValue]
extractConstants = nub . concatMap (constants "" . view contractAst) where
-- Tools for parsing numbers and quoted strings from 'Text'
as f = preview $ to f . _Right . _1
asAddr x = as hexadecimal =<< T.stripPrefix "0x" x
asQuoted = preview $ unpacked . prefixed "\"" . suffixed "\"" . packedChars
asDecimal = preview $ to decimal . _Right . _1
asQuoted = preview $ unpacked . prefixed "\"" . suffixed "\"" . packedChars
-- We need this because sometimes @solc@ emits a json string with a type, then a string
-- representation of some value of that type. Why is this? Unclear. Anyway, this lets us match
-- those cases like regular strings
literal t f = \case String (T.words -> ((^? only t) -> m) : y : _) -> m *> f y
_ -> Nothing
literal t f (String (T.words -> ((^? only t) -> m) : y : _)) = m *> f y
literal _ _ _ = Nothing
-- When we get a number, it could be an address, uint, or int. We'll try everything.
dec i = let l f = f <$> [8,16..256] <*> fmap fromIntegral [i-1..i+1] in
AbiAddress i : catMaybes (l mkValidAbiInt ++ l mkValidAbiUInt)
-- 'constants' takes a property name and its 'Value', then tries to find solidity literals
-- CASE ONE: we're looking at a big object with a bunch of little objects, recurse
constants _ (Object o) = concatMap (uncurry constants) $ M.toList o
constants _ (Array a) = concatMap (constants "") a
-- CASE TWO: we're looking at a @type@ or @value@ object, try to parse it
-- 2.1: We're looking at a @value@ starting with "0x", which is how solc represents addresses
-- @value: "0x123"@ ==> @[AbiAddress 291]@
constants "value" (String (asAddr -> Just i)) = [AbiAddress i]
-- 2.2: We're looking at something of the form @type: int_const [...]@, an integer literal
-- @type: "int_const 123"@ ==> @[AbiUInt 8 123, AbiUInt 16 123, ... AbiInt 256 123]@
constants "type" (literal "int_const" (as decimal) -> Just i) =
let l f = f <$> [8,16..256] <*> (fromIntegral <$> ([i-1..i+1] :: [Integer])) in l AbiInt ++ l AbiUInt
-- 2.3: We're looking at something of the form @type: literal_string "[...]"@, a string literal
-- CASE TWO: we're looking at a @type@, try to parse it
-- 2.1: We're looking at a @int_const@ with a decimal number inside, could be an address, int, or uint
-- @type: "int_const 0x12"@ ==> @[AbiAddress 18, AbiUInt 8 18,..., AbiUInt 256 18, AbiInt 8 18,...]@
constants "typeString" (literal "int_const" asDecimal -> Just i) = dec i
-- 2.2: We're looking at something of the form @type: literal_string "[...]"@, a string literal
-- @type: "literal_string \"123\""@ ==> @[AbiString "123", AbiBytes 3 "123"...]@
constants "type" (literal "literal_string" asQuoted -> Just b) =
let size = BS.length b in
([AbiString, AbiBytesDynamic] <&> ($ b)) ++
map (\n -> AbiBytes n (BS.append b (BS.replicate (n - size) 0))) [size .. 32]
constants "typeString" (literal "literal_string" asQuoted -> Just b) =
let size = BS.length b in [AbiString b, AbiBytesDynamic b] ++
fmap (\n -> AbiBytes n . BS.append b $ BS.replicate (n - size) 0) [size..32]
-- CASE THREE: we're at a leaf node with no constants
constants _ _ = []

@ -19,6 +19,7 @@ dependencies:
- deepseq
- directory >= 1.3 && < 1.4
- exceptions >= 0.8.1 && < 0.11
- filepath
- hashable
- hevm
- lens >= 4.15.1 && < 4.17

@ -39,6 +39,6 @@ main = do Options f c conf <- execParser opts
cpg <- flip runReaderT cfg $ do
cs <- contracts f
ads <- addresses
(v,w,ts) <- loadSpecified (pack . (f ++) . (':' :) <$> c) cs >>= prepareForTest
(v,w,ts) <- loadSpecified (pack <$> c) cs >>= prepareForTest
ui v w ts (Just $ mkGenDict 0.15 (extractConstants cs ++ ads) [] g (returnTypes cs))
if not . isSuccess $ cpg then exitWith $ ExitFailure 1 else exitSuccess

@ -44,7 +44,7 @@ compilationTests = testGroup "Compilation and loading tests"
loadFails :: FilePath -> Maybe Text -> String -> (SolException -> Bool) -> TestTree
loadFails fp c e p = testCase fp . catch tryLoad $ assertBool e . p where
tryLoad = runReaderT (loadSolidity fp c >> pure ()) $ defaultConfig & sConf . quiet .~ True
tryLoad = runReaderT (loadWithCryticCompile fp c >> pure ()) $ defaultConfig & sConf . quiet .~ True
-- Extraction Tests

Loading…
Cancel
Save