crytic/echidna

Ethereum smart contract fuzzer

echidna's Issues

Build fails in Dockerfile

#20 adds a Dockerfile which I built interactively with success. When I build an image through docker build with the same code, the following error is thrown

regex-tdfa-1.2.2: copy/register

--  While building custom Setup.hs for package megaparsec-6.4.0 using:
      /root/.stack/setup-exe-cache/x86_64-linux-nopie/Cabal-simple_mPHDZzAJ_1.24.2.0_ghc-8.0.2 --builddir=.stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0 build --ghc-options " -ddump-hi -ddump-to-file"
    Process exited with code: ExitFailure 1
    Logs have been written to: /echidna/.stack-work/logs/megaparsec-6.4.0.log

    Configuring megaparsec-6.4.0...
    Building megaparsec-6.4.0...
    Preprocessing library megaparsec-6.4.0...
    [ 1 of 11] Compiling Text.Megaparsec.Pos ( Text/Megaparsec/Pos.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Pos.o )
    [ 2 of 11] Compiling Text.Megaparsec.Stream ( Text/Megaparsec/Stream.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Stream.o )
    [ 3 of 11] Compiling Text.Megaparsec.Error ( Text/Megaparsec/Error.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Error.o )
    [ 4 of 11] Compiling Text.Megaparsec.Error.Builder ( Text/Megaparsec/Error/Builder.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Error/Builder.o )
    [ 5 of 11] Compiling Text.Megaparsec  ( Text/Megaparsec.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec.o )
    
    /tmp/stack1739/megaparsec-6.4.0/Text/Megaparsec.hs:123:1: error:
        Failed to load interface for `Control.Monad.Combinators'
        There are files missing in the `parser-combinators-0.4.0' package,
        try running 'ghc-pkg check'.
        Use -v to see a list of the files searched for.
The command '/bin/sh -c stack upgrade && stack setup && stack install' returned a non-zero code: 1

The logs for megaparsec

cat .stack-work/logs/megaparsec-6.4.0.log
Configuring megaparsec-6.4.0...
Building megaparsec-6.4.0...
Preprocessing library megaparsec-6.4.0...
[ 1 of 11] Compiling Text.Megaparsec.Pos ( Text/Megaparsec/Pos.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Pos.o )
[ 2 of 11] Compiling Text.Megaparsec.Stream ( Text/Megaparsec/Stream.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Stream.o )
[ 3 of 11] Compiling Text.Megaparsec.Error ( Text/Megaparsec/Error.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Error.o )
[ 4 of 11] Compiling Text.Megaparsec.Error.Builder ( Text/Megaparsec/Error/Builder.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Error/Builder.o )
[ 5 of 11] Compiling Text.Megaparsec  ( Text/Megaparsec.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec.o )
[ 6 of 11] Compiling Text.Megaparsec.Char ( Text/Megaparsec/Char.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Char.o )
[ 7 of 11] Compiling Text.Megaparsec.Byte ( Text/Megaparsec/Byte.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Byte.o )
[ 8 of 11] Compiling Text.Megaparsec.Char.Lexer ( Text/Megaparsec/Char/Lexer.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Char/Lexer.o )
[ 9 of 11] Compiling Text.Megaparsec.Byte.Lexer ( Text/Megaparsec/Byte/Lexer.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Byte/Lexer.o )
[10 of 11] Compiling Text.Megaparsec.Expr ( Text/Megaparsec/Expr.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Expr.o )
[11 of 11] Compiling Text.Megaparsec.Perm ( Text/Megaparsec/Perm.hs, .stack-work/dist/x86_64-linux-nopie/Cabal-1.24.2.0/build/Text/Megaparsec/Perm.o )
Installing library in
/mnt/.stack-work/install/x86_64-linux-nopie/lts-8.15/8.0.2/lib/x86_64-linux-ghc-8.0.2/megaparsec-6.4.0-A8Cha6Z23OrgfglI4a3h3
Registering megaparsec-6.4.0...

test fails with seemingly unrelated error

confused why this fails:

$ echidna-test example.sol
example.sol:74:9: Warning: Invoking events without "emit" prefix is deprecated.
        Transfer(0x0, msg.sender, tokens);
        ^-------------------------------^
━━━ example.sol ━━━
  ✗ "echidna_maxSupplyAlwaysGreaterZero" failed after 1 test and 1 shrink.

      │ Call sequence: name();

  ✗ 1 failed.

contract (example.sol):

pragma solidity ^0.4.19;


contract Example {
    uint256 public maxSupply;
    uint256 public price;

    // the owner can withdraw all ether from the contract after funding is finished
    address public ownerAddress;

    // when the sale ends
    uint256 public closingTime;

    /// public ERC20 interface
    uint256 public totalSupply;

    /// public ERC20 interface
    string public symbol;

    /// public ERC20 interface
    string public name;

    uint8 public decimals = 0;

    /// maps addresses to their token balances
    mapping (address => uint256) public balances;

    function Example() public {
        ownerAddress = 0;
        maxSupply = 0;
        closingTime = 10000000;
        price = 10;
        symbol = "EXAMPLE";
        name = "example";
        totalSupply = 0;
    }

    // returns whether the project is fully funded
    function isFunded() public view returns (bool) {
        return totalSupply == maxSupply;
    }

    function isClosingTimeOver() public view returns (bool) {
        // solium-disable-next-line security/no-block-members
        return block.timestamp <= closingTime;
    }

    /// returns whether one can still buy a token
    function isFundable() public view returns (bool) {
        return !isFunded() && !isClosingTimeOver();
    }

    function failedToReachGoalInTime() public view returns (bool) {
        return !isFunded() && isClosingTimeOver();
    }

    // public ERC20 interface
    event Transfer(address indexed from, address indexed to, uint256 tokens);

    /// fallback function
    function () payable public {
        require(isFundable());
        /// must be evenly divisible by price
        require((msg.value % price) == 0);
        uint256 tokens = msg.value / price;
        require(0 < tokens);
        // TODO should sender get up to that many tokens or should it revert
        require(totalSupply + tokens <= maxSupply);

        // mint tokens
        balances[msg.sender] += tokens;
        totalSupply += tokens;
        Transfer(0x0, msg.sender, tokens);
    }

    // the following are invariants checked by the echidna smart fuzzer

    function echidna_maxSupplyAlwaysGreaterZero() public view returns (bool) {
        return maxSupply > 0;
    }
}

context:

echidna-test built from: 159b595

$ solc --version
solc, the solidity compiler commandline interface
Version: 0.4.21+commit.dfe3193c.Darwin.appleclang

echidna_* Functions in separate solidity file

I'm trying to figure out how to use Echidna to fuzz test some TCR contracts. For example,

https://github.com/computablelabs/computable/blob/master/contracts/Registry.sol

I'd prefer not to add on echidna_* functions into these contracts since that would make these contracts different from the canonical TCR contracts. Would there be a way I could make a separate file, say echidna_registry.sol and have all my new functions for fuzz testing in there without modifying the original Registry.sol file?

Perprop config parsing

When perprop parses a config for function names, it doesn't separate the name from the rest of the signature. This results in echidna trying to run a function named (for example) "test()" instead of "test".

Feature request: echidna tests implementation outside of the contract.

Hi, I would like to execute Echidna tests without modifying original contracts, i.e. something along these lines:

Contract under test:

pragma solidity ^0.4.16;

contract C {

  int private state = 0;
  function f(int x) public {
    state = x;
  }
}

and C_echidna.sol with echidna tests:

import "C.sol";

pragma solidity ^0.4.16;

contract CEchidna is C {
  function echidna_revert() public returns (bool) {
    if (state < 0)
      revert();
  }
}

The idea is NOT to modify the contracts under test.

Obviously the problem are private variables and functions as I have just experimented:

root@2ebd02bed9a2:/echidna# echidna-test solidity/echidna_tests/cli_echidna.sol Test --solc-args="--allow-paths=/echidna/solidity"
solidity/echidna_tests/cli_echidna.sol:10:12: Error: Undeclared identifier. Did you mean "log0"?
    return(flag0 || flag1);
           ^---^
solidity/echidna_tests/cli_echidna.sol:10:21: Error: Undeclared identifier. Did you mean "log1"?
    return(flag0 || flag1);
                    ^---^
echidna-test: readCreateProcess: solc "--combined-json=bin-runtime,bin,srcmap,srcmap-runtime,abi,ast" "solidity/echidna_tests/cli_echidna.sol" "--allow-paths=/echidna/solidity" (exit 1): failed
root@2ebd02bed9a2:/echidna# cat solidity/cli.sol 
pragma solidity ^0.4.16;

contract Test {
  bool private flag0=true;
  bool private flag1=true;

  function set0(int val) returns (bool){
    if (val % 10 == 0) {flag0 = false;}
  }
  function set1(int val) returns (bool){
    if (val % 10 == 0 && flag0) {flag1 = false;}
  }
  function echidna_alwaystrue() returns (bool){
    return(true);
  }
  function echidna_sometimesfalse() returns (bool){
    return(flag0 || flag1);
  }
}

Perhaps there would be a way to support this by having on-the-fly test injection into the original contract just before the test is executed. Does it make sense?

Flush stdout in perprop

This would allow other programs to parse the stdout from perprop as a stream, as opposed to receiving all the stdout when the program exits. Since it may take a while for perprop to finish testing a single property, I think this would be good to have.

OS X Install instructions for readline need more details

For me (and I suspect other people) the real solution is to

port install readline +universal
export CPPFLAGS=-I/opt/local/include
export LDFLAGS=-L/opt/local/lib
stack install readline --extra-include-dirs=/usr/local/opt/readline/include --extra-lib-dirs=/usr/local/opt/readline/lib; stack install

(readline is pretty likely to cause some failures during stack otherwise, and the suggested fix is often not quite what people need; there's probably a brew equivalent but I couldn't find it)

echidna_alwaystrue fails on hardcoded return true

I am fuzzing contract that has echidna_alwaystrue method which always returns true:

import "./ERC20.sol";
import "./SafeMath.sol";
import "./SafeERC20.sol";


/**
 * @title Crowdsale
 * @dev Crowdsale is a base contract for managing a token crowdsale,
 * allowing investors to purchase tokens with ether. This contract implements
 * such functionality in its most fundamental form and can be extended to provide additional
 * functionality and/or custom behavior.
 * The external interface represents the basic interface for purchasing tokens, and conform
 * the base architecture for crowdsales. They are *not* intended to be modified / overridden.
 * The internal interface conforms the extensible and modifiable surface of crowdsales. Override
 * the methods to add functionality. Consider using 'super' where appropriate to concatenate
 * behavior.
 */
contract Crowdsale {
  using SafeMath for uint256;
  using SafeERC20 for ERC20;

  // The token being sold
  ERC20 public token;

  // Address where funds are collected
  address public wallet;

  // How many token units a buyer gets per wei.
  // The rate is the conversion between wei and the smallest and indivisible token unit.
  // So, if you are using a rate of 1 with a DetailedERC20 token with 3 decimals called TOK
  // 1 wei will give you 1 unit, or 0.001 TOK.
  uint256 public rate;

  // Amount of wei raised
  uint256 public weiRaised;

  /**
   * Event for token purchase logging
   * @param purchaser who paid for the tokens
   * @param beneficiary who got the tokens
   * @param value weis paid for purchase
   * @param amount amount of tokens purchased
   */
  event TokenPurchase(
    address indexed purchaser,
    address indexed beneficiary,
    uint256 value,
    uint256 amount
  );

  /**
   * @param _rate Number of token units a buyer gets per wei
   * @param _wallet Address where collected funds will be forwarded to
   * @param _token Address of the token being sold
   */
  constructor(uint256 _rate, address _wallet, ERC20 _token) public {
    require(_rate > 0);
    require(_wallet != address(0));
    require(_token != address(0));

    rate = _rate;
    wallet = _wallet;
    token = _token;
  }

  // -----------------------------------------
  // Crowdsale external interface
  // -----------------------------------------

  /**
   * @dev fallback function ***DO NOT OVERRIDE***
   */
  function () external payable {
    buyTokens(msg.sender);
  }

  /**
   * @dev low level token purchase ***DO NOT OVERRIDE***
   * @param _beneficiary Address performing the token purchase
   */
  function buyTokens(address _beneficiary) public payable {

    uint256 weiAmount = msg.value;
    _preValidatePurchase(_beneficiary, weiAmount);

    // calculate token amount to be created
    uint256 tokens = _getTokenAmount(weiAmount);

    // update state
    weiRaised = weiRaised.add(weiAmount);

    _processPurchase(_beneficiary, tokens);
    emit TokenPurchase(
      msg.sender,
      _beneficiary,
      weiAmount,
      tokens
    );

    _updatePurchasingState(_beneficiary, weiAmount);

    _forwardFunds();
    _postValidatePurchase(_beneficiary, weiAmount);
  }


  // -----------------------------------------
  // Internal interface (extensible)
  // -----------------------------------------

  /**
   * @dev Validation of an incoming purchase. Use require statements to revert state when conditions are not met. Use `super` in contracts that inherit from Crowdsale to extend their validations.
   * Example from CappedCrowdsale.sol's _preValidatePurchase method: 
   *   super._preValidatePurchase(_beneficiary, _weiAmount);
   *   require(weiRaised.add(_weiAmount) <= cap);
   * @param _beneficiary Address performing the token purchase
   * @param _weiAmount Value in wei involved in the purchase
   */
  function _preValidatePurchase(
    address _beneficiary,
    uint256 _weiAmount
  )
    internal
  {
    require(_beneficiary != address(0));
    require(_weiAmount != 0);
  }

  /**
   * @dev Validation of an executed purchase. Observe state and use revert statements to undo rollback when valid conditions are not met.
   * @param _beneficiary Address performing the token purchase
   * @param _weiAmount Value in wei involved in the purchase
   */
  function _postValidatePurchase(
    address _beneficiary,
    uint256 _weiAmount
  )
    internal
  {
    // optional override
  }

  /**
   * @dev Source of tokens. Override this method to modify the way in which the crowdsale ultimately gets and sends its tokens.
   * @param _beneficiary Address performing the token purchase
   * @param _tokenAmount Number of tokens to be emitted
   */
  function _deliverTokens(
    address _beneficiary,
    uint256 _tokenAmount
  )
    internal
  {
    token.safeTransfer(_beneficiary, _tokenAmount);
  }

  /**
   * @dev Executed when a purchase has been validated and is ready to be executed. Not necessarily emits/sends tokens.
   * @param _beneficiary Address receiving the tokens
   * @param _tokenAmount Number of tokens to be purchased
   */
  function _processPurchase(
    address _beneficiary,
    uint256 _tokenAmount
  )
    internal
  {
    _deliverTokens(_beneficiary, _tokenAmount);
  }

  /**
   * @dev Override for extensions that require an internal state to check for validity (current user contributions, etc.)
   * @param _beneficiary Address receiving the tokens
   * @param _weiAmount Value in wei involved in the purchase
   */
  function _updatePurchasingState(
    address _beneficiary,
    uint256 _weiAmount
  )
    internal
  {
    // optional override
  }

  /**
   * @dev Override to extend the way in which ether is converted to tokens.
   * @param _weiAmount Value in wei to be converted into tokens
   * @return Number of tokens that can be purchased with the specified _weiAmount
   */
  function _getTokenAmount(uint256 _weiAmount)
    internal view returns (uint256)
  {
    return _weiAmount.mul(rate);
  }

  /**
   * @dev Determines how ETH is stored/forwarded on purchases.
   */
  function _forwardFunds() internal {
    wallet.transfer(msg.value);
  }

  function echidna_alwaystrue() returns (bool) {
    return true;
  }
  
}

and echidna-test fails with error message

✗ "echidna_alwaystrue" failed after 1 test and 1 shrink.

    │ Call sequence: rate();
 
✗ 1 failed.

Check Counter readme failure - openFile Exec.hs does not exist

When running the test example in the readme I get:

○ 0/1 complete (running)
  ↯ "echidna_check_counter" failed after 100 tests and 129 shrinks (shrinking)
echidna-test: lib/Echidna/Exec.hs: openFile: does not exist (No such file or directory)
M

When there is no methods to execute, any test will fail

If a contract does not define any (public) method to execute, like this one:

contract C {
  function echidna_test() returns (bool) {
    return true;
  }
}

then echidna will fail to execute the test:

━━━ test.sol ━━━
  ✗ "echidna_test" failed after 1 test.
  
    
  
  ✗ 1 failed.

It is better to warn the user about this issue and abort the execution.

Have sensible way of managing `sender` and `owner`

Currently Echidna has no canonical way of establishing the sender of a test or the owner of the contract being tested.

Events for final call sequence

It would be great if, after the shrinking phase has completed, the events emitted to the log are output along with the minimized call sequence.

One can obviously replay the execution given the call sequence, but having the logs would likely assist in arriving at an understanding of the failure more quickly.

Inconsistent test results in a simple contract

In this simple contract:

contract TEST {
  function f(bytes1 x) returns (bool) {
        return true;
  }

  function echidna_true() returns (bool) {
    return true;
  }
}

the echidna_true test cannot fail. However the last revision of Echidna reports a failed test when it runs more than one epoch. For instance:

$ echidna-test test.sol --epochs 10
━━━ test.sol ━━━
  ✓ "echidna_true" passed 1000 tests.
  ✓ 1 succeeded.
━━━ test.sol ━━━
  ✗ "echidna_true" failed after 14 tests and 1 shrink.
  
      │ Call sequence: f("");
  
  ✗ 1 failed.
━━━ test.sol ━━━
  ⚐ "echidna_true" gave up after 100 discards, passed 762 tests.
  ⚐ 1 gave up.
━━━ test.sol ━━━
  ✗ "echidna_true" failed after 20 tests and 2 shrinks.
  
      │ Call sequence: f("");
  
  ✗ 1 failed.
  ...

Allow to specify which user calls each method in a contract

Some smart contracts define an address as "owner" to perform certain "privileged" operations. For instance:

contract C {
  uint state = 1;
  address owner;

  function C() {
     owner = msg.sender;
  }

  function only_owner(uint x) public {
      require(msg.sender == owner);
      state = x;
  }

  function echidna_test() public returns (bool) {
      return (state == 1);
  }
}

Unfortunately, Echidna does not allow to specify the use of different users (contract owner, user, attacker) when the transactions are executed. It could be nice to have a command line option for that.

echidna fails to run outside the repository folder

Tried the example solution @japesinator suggested during his ETHCC workshop but does not seem working on the latest solc compiler.

$  echidna-test contracts/testme.sol 
━━━ contracts/testme.sol ━━━
  ○ 0/1 complete (running)
  ↯ "echidna_alwaystrue" failed after 1 test (shrinking)
echidna-test: lib/Echidna/Exec.hs: openFile: does not exist (No such file or directory)

pragma solidity 0.4.21;

contract Canal {
  bool private first_gate_up=false;
  bool private second_gate_up=true;

  function lower(bool first_gate) public returns (bool){
    if(first_gate) {
      if(second_gate_up) {
        first_gate_up = false;
        return(true);
      } else {
        return(false);
      }
    } else {
      if(first_gate_up) {
        second_gate_up = false;
        return true;
      } else {
        return(false);
      }
    }
  }
  function raise(bool first_gate) public {
    if(first_gate) {
      first_gate_up = true;
    } else {
      second_gate_up = true;
    }
  }

  function echidna_alwaystrue() public view returns (bool){
    return (first_gate_up || first_gate_up);
  }
}

Add convenience functions that don't execute in a reader

For the most commonly used bits of the echidna API, we should provide for each f, f' = runReaderT f defaultConfig and document the existence of these new functions

Dump EVM state on test failures

Related to issue #63

One of the files that Manticore outputs for each test case that it generates is a .summary file that lists: addresses, balances, code and storage for contracts, and hashes for known input.

It would be great if Echidna could dump its EVM state on test failures, showing similar output to Manticore.

possibly support arguments in tests

just some thoughts.

i tried

    function echidna_balanceAlwaysLowerEqualTotalSupply(address tokenHolder) public view returns (bool) {
        return balanceOf(tokenHolder) <= totalSupply;
    }

and it aborted with Test "echidna_balanceAlwaysLowerEqualTotalSupply" has arguments, aborting

i understand why.

it could be interesting to support this. it would open up a whole new set of properties that
can be tested with echidna. maybe this is possible by using echidna as a library. i've yet to look into that.

i imagine it could fuzz (argument) addresses first, that occur somewhere in storage of the contract or that it has used before.

statemachine example fails

This is using the latest commit on master: 1612584

With

$ stack --version
Version 1.6.5, Git revision 24ab0d6ff07f28276e082c3ce74dfdeb1a2ca9e9 (5514 commits) x86_64 hpack-0.20.0

When I run the statemachine example:

$ stack examples/state-machine/StateMachine.hs
stack: WARNING! Expecting "stack" at line 1, column 3
stack: WARNING! Missing or unusable stack options specification
stack: WARNING! Using runghc without any additional stack options

examples/state-machine/StateMachine.hs:40:23: error:
    • Couldn't match expected type ‘Data.Text.Internal.Text’
                  with actual type ‘[Char]’
    • In the expression: "coin"
      In the first argument of ‘execCall’, namely ‘("coin", [])’
      In the expression: execCall ("coin", [])

examples/state-machine/StateMachine.hs:51:23: error:
    • Couldn't match expected type ‘Data.Text.Internal.Text’
                  with actual type ‘[Char]’
    • In the expression: "push"
      In the first argument of ‘execCall’, namely ‘("push", [])’
      In the expression: execCall ("push", [])

examples/state-machine/StateMachine.hs:61:23: error:
    • Couldn't match expected type ‘Data.Text.Internal.Text’
                  with actual type ‘[Char]’
    • In the expression: "push"
      In the first argument of ‘execCall’, namely ‘("push", [])’
      In the expression: execCall ("push", [])

Figure out what versions of solc are supported

apparently 0.4.21 is not

gitter or riot channel

a gitter or riot channel for discussion around echidna would be useful

Perprop leaks memory

If you run perprop-exe any solidity contract, like this one:

contract C {
  function f(uint x) returns (uint) { return x; }
  function test() returns (bool) {
    return true;
  }
}

using this config file:

testLimit: 10
sender:
    - address: 0x1
      name: 'sender'
properties:
    - name: 'test'
      return: 'Success'

It will cause a noticeable memory leak (use top to check it). Depending on your system configuration, your OS can kill automatically the perprop-exe execution.

Echidna command-line fails on Debian

It fails with the following error:

`

~/.local/bin/echidna-test solidity/cli.sol

echidna-test: : commitBuffer: invalid argument (invalid character)

uname -a

Linux core 3.16.0-4-amd64 #1 SMP Debian 3.16.39-1+deb8u2 (2017-03-07) x86_64 GNU/Linux
`

(we talked about this at the workshop at ETHCC)

How do I add new addresses?

I want to write solidity tests to use with echidna-test, and I need to use more than 3 addresses. Questions:

1. In what file(s) do I define the new addresses? I see addrList in several *.yaml files in the project.
2. Is there a special utility for generating addresses, or do I just add random ethereum addresses? Do I need to add private keys somewhere?
3. If I want to test how two contracts interact, can I just deploy the second contract within the constructor?

It would be helpful if this information was added to the README file. Thank you.

Self describing test failures

Consider the following snippet:

  …
  function echidna_test() public returns (bool) {
      return (state == 1);
  }

When the test fails, we get the failing call sequence and the knowledge that state != 1. We need to replay the calls to determine what state actually is.

However, if Echidna recognized a special function, say echidna_failure_log, and was able to print out the event log (cf. Issue #62) then test failure may become easier to understand. For example:

  …
  function echidna_test() public returns (bool) {
      return (state == 1);
  }

  event State(uint256 _state);
  function echidna_failure_log() public {
      emit State(state);
  }

Echidna would make a final call to echidna_failure_log after each minimized failing call sequence for each failing test.

Echidna with parallel testing is slower than using sequential testing

I tested echidna using the recently enabled -threaded flag using this smart contract with this command line:

$ time echidna-test test.sol test.sol:TEST

Using the last revision (which uses checkParallel), echidna is taking quite a long time to run:

real	1m9.779s
user	20m20.512s
sys	5m46.520s

This execution uses all the available processors according to top (in this case: 24). However, if you replace the use checkParallel by checkSequential in src/Main.hs, it is faster:

real	0m23.495s
user	0m30.392s
sys	0m9.236s

This execution only uses 1 or 2 processors according to top.

Automated build on Docker Hub

The repository owner can configure automated builds so that users can download it from Docker Hub instead of building it manually!

Inconsistent test results in a simple contract

In this simple contract:

contract TEST {
  uint256 state = 0;

  function f() {
    state = 1; 
    revert();
  }

  function echidna_true() returns (bool) {
    return (state == 0);
  }
}

the echidna_true test cannot fail. However the last revision of Echidna reports a failed test:

  ✗ "echidna_true" failed after 1 test.
  
      │ Call sequence: f();
  
  ✗ 1 failed.
Coverage: 0 unique PCs

Maybe this is an issue of HEVM?

Integration with Remix for debugging

Remix has a feature for loading a ‘scenario’ file (json) that describes a sequence of transactions.

https://remix.readthedocs.io/en/latest/run_tab.html#using-the-recorder

It would be great if Echidna was able to export failing call sequences so that they could be replayed and debugged within Remix.

make echidna-test work without requiring custom constructor

it seems that echidna-test fails with an unhelpful error message if storage vars are not initialized explicitely in a constructor without arguments.

make echidna fuzz constructor arguments (if it doesn't already) and call the constructor so echidna can be used without having to write a special constructor for the contract under test.

see:

#14 (comment)
#14

Download and re-use ghc with stack will speedup the CI test

Right now, ghc is downloaded each time using apt-get: https://travis-ci.org/trailofbits/echidna/jobs/385309324#L460-L473

Instead, it will be nice to download and re-use ghc with stack to speedup the CI tests.

CI tests are broken on master

The fetching of the apt files fails on master:

$ sudo -E apt-get -yq --no-install-suggests --no-install-recommends $TRAVIS_APT_OPTS install ghc-8.2.1
Reading package lists...
Building dependency tree...
Reading state information...
E: Unable to locate package ghc-8.2.1
E: Couldn't find any package by glob 'ghc-8.2.1'
E: Couldn't find any package by regex 'ghc-8.2.1'
apt-get.diagnostics
apt-get install failed
$ cat ~/apt-get-update.log
Ign:1 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty InRelease
Get:2 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates InRelease [65.9 kB]
Hit:3 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-backports InRelease
Hit:4 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty Release
Ign:6 http://dl.google.com/linux/chrome/deb stable InRelease
Get:7 http://dl.google.com/linux/chrome/deb stable Release [1,189 B]
Get:9 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/main Sources [519 kB]
Get:10 http://dl.google.com/linux/chrome/deb stable Release.gpg [819 B]
Get:11 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/universe Sources [258 kB]
Get:12 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/multiverse Sources [7,287 B]
Get:13 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/main amd64 Packages [1,360 kB]
Get:5 http://dl.bintray.com/apache/cassandra 39x InRelease [3,168 B]
Ign:8 http://toolbelt.heroku.com/ubuntu ./ InRelease
Get:15 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/main i386 Packages [1,285 kB]
Hit:14 http://toolbelt.heroku.com/ubuntu ./ Release
Get:16 https://download.docker.com/linux/ubuntu trusty InRelease [26.5 kB]
Get:17 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/main Translation-en [654 kB]
Get:18 http://apt.postgresql.org/pub/repos/apt trusty-pgdg InRelease [61.4 kB]
Get:20 https://dl.hhvm.com/ubuntu trusty InRelease [2,411 B]
Get:21 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/restricted amd64 Packages [21.4 kB]
Get:22 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/restricted i386 Packages [21.1 kB]
Get:23 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/restricted Translation-en [3,704 B]
Get:24 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/universe amd64 Packages [600 kB]
Get:25 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/universe i386 Packages [588 kB]
Get:26 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/universe Translation-en [308 kB]
Get:27 http://dl.google.com/linux/chrome/deb stable/main amd64 Packages [1,111 B]
Get:28 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/multiverse amd64 Packages [16.0 kB]
Get:29 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/multiverse i386 Packages [16.5 kB]
Get:30 http://us-central1.gce.archive.ubuntu.com/ubuntu trusty-updates/multiverse Translation-en [7,680 B]
Get:32 https://download.docker.com/linux/ubuntu trusty/stable amd64 Packages [3,545 B]
Get:33 https://download.docker.com/linux/ubuntu trusty/edge amd64 Packages [4,756 B]
Get:34 https://dl.hhvm.com/ubuntu trusty/main amd64 Packages [1,816 B]
Get:35 http://apt.postgresql.org/pub/repos/apt trusty-pgdg/main amd64 Packages [190 kB]
Hit:36 https://packagecloud.io/computology/apt-backport/ubuntu trusty InRelease
Get:37 https://packagecloud.io/github/git-lfs/ubuntu trusty InRelease [23.2 kB]
Get:38 https://packagecloud.io/rabbitmq/rabbitmq-server/ubuntu trusty InRelease [23.7 kB]
Get:39 http://apt.postgresql.org/pub/repos/apt trusty-pgdg/main i386 Packages [189 kB]
Get:40 https://packagecloud.io/github/git-lfs/ubuntu trusty/main amd64 Packages [6,863 B]
Get:41 https://packagecloud.io/github/git-lfs/ubuntu trusty/main i386 Packages [6,629 B]
Get:42 https://packagecloud.io/rabbitmq/rabbitmq-server/ubuntu trusty/main amd64 Packages [5,515 B]
Get:43 https://packagecloud.io/rabbitmq/rabbitmq-server/ubuntu trusty/main i386 Packages [5,515 B]
Err:44 http://ppa.launchpad.net/chris-lea/redis-server/ubuntu trusty InRelease
  Could not connect to ppa.launchpad.net:80 (91.189.95.83), connection timed out
Err:45 http://ppa.launchpad.net/couchdb/stable/ubuntu trusty InRelease
  Unable to connect to ppa.launchpad.net:http:
Err:46 http://ppa.launchpad.net/git-core/ppa/ubuntu trusty InRelease
  Unable to connect to ppa.launchpad.net:http:
Err:47 http://ppa.launchpad.net/hvr/ghc/ubuntu trusty InRelease
  Unable to connect to ppa.launchpad.net:http:
Err:48 http://ppa.launchpad.net/openjdk-r/ppa/ubuntu trusty InRelease
  Unable to connect to ppa.launchpad.net:http:
Err:49 http://ppa.launchpad.net/pollinate/ppa/ubuntu trusty InRelease
  Unable to connect to ppa.launchpad.net:http:
Err:50 http://ppa.launchpad.net/webupd8team/java/ubuntu trusty InRelease
  Unable to connect to ppa.launchpad.net:http:
Err:51 http://repo.mongodb.org/apt/ubuntu trusty/mongodb-org/3.4 InRelease
  Could not connect to repo.mongodb.org:80 (13.33.160.168), connection timed out
Get:52 http://security.ubuntu.com/ubuntu trusty-security InRelease [65.9 kB]
Get:53 http://security.ubuntu.com/ubuntu trusty-security/main Sources [205 kB]
Get:54 http://security.ubuntu.com/ubuntu trusty-security/restricted Sources [5,050 B]
Get:55 http://security.ubuntu.com/ubuntu trusty-security/universe Sources [94.0 kB]
Get:56 http://security.ubuntu.com/ubuntu trusty-security/multiverse Sources [3,072 B]
Get:57 http://security.ubuntu.com/ubuntu trusty-security/main amd64 Packages [941 kB]
Get:58 http://security.ubuntu.com/ubuntu trusty-security/main i386 Packages [869 kB]
Get:59 http://security.ubuntu.com/ubuntu trusty-security/main Translation-en [496 kB]
Get:60 http://security.ubuntu.com/ubuntu trusty-security/restricted amd64 Packages [18.1 kB]
Get:61 http://security.ubuntu.com/ubuntu trusty-security/restricted i386 Packages [17.8 kB]
Get:62 http://security.ubuntu.com/ubuntu trusty-security/restricted Translation-en [3,272 B]
Get:63 http://security.ubuntu.com/ubuntu trusty-security/universe amd64 Packages [305 kB]
Get:64 http://security.ubuntu.com/ubuntu trusty-security/universe i386 Packages [293 kB]
Get:65 http://security.ubuntu.com/ubuntu trusty-security/universe Translation-en [164 kB]
Get:66 http://security.ubuntu.com/ubuntu trusty-security/multiverse amd64 Packages [4,727 B]
Get:67 http://security.ubuntu.com/ubuntu trusty-security/multiverse i386 Packages [4,878 B]
Get:68 http://security.ubuntu.com/ubuntu trusty-security/multiverse Translation-en [2,426 B]
Fetched 9,781 kB in 10s (894 kB/s)
Reading package lists...
W: Failed to fetch http://ppa.launchpad.net/chris-lea/redis-server/ubuntu/dists/trusty/InRelease  Could not connect to ppa.launchpad.net:80 (91.189.95.83), connection timed out
W: Failed to fetch http://ppa.launchpad.net/couchdb/stable/ubuntu/dists/trusty/InRelease  Unable to connect to ppa.launchpad.net:http:
W: Failed to fetch http://ppa.launchpad.net/git-core/ppa/ubuntu/dists/trusty/InRelease  Unable to connect to ppa.launchpad.net:http:
W: Failed to fetch http://ppa.launchpad.net/hvr/ghc/ubuntu/dists/trusty/InRelease  Unable to connect to ppa.launchpad.net:http:
W: Failed to fetch http://repo.mongodb.org/apt/ubuntu/dists/trusty/mongodb-org/3.4/InRelease  Could not connect to repo.mongodb.org:80 (13.33.160.168), connection timed out
W: Failed to fetch http://ppa.launchpad.net/openjdk-r/ppa/ubuntu/dists/trusty/InRelease  Unable to connect to ppa.launchpad.net:http:
W: Failed to fetch http://ppa.launchpad.net/pollinate/ppa/ubuntu/dists/trusty/InRelease  Unable to connect to ppa.launchpad.net:http:
W: Failed to fetch http://ppa.launchpad.net/webupd8team/java/ubuntu/dists/trusty/InRelease  Unable to connect to ppa.launchpad.net:http:
W: Some index files failed to download. They have been ignored, or old ones used instead.
The command "sudo -E apt-get -yq --no-install-suggests --no-install-recommends $TRAVIS_APT_OPTS install ghc-8.2.1" failed and exited with 100 during .

complete log: https://travis-ci.org/trailofbits/echidna/jobs/414143702

Gas usage tester leaks a lot of memory

If you run the gas usage tester (#86) with this simple solidity contract:

contract TEST {
  function init(address[] _xs, uint256[] _ys) {
        return;
  }
  function echidna_true() returns (bool) {
	return true;
  }
}

It will cause a major memory leak. Be careful if you try to reproduce this issue, since it can produce a large amount of swapping and crash other programs (e.g. internet browsers)

Fuzzing doesn't sufficiently cover different addresses for a transfer

Consider the following simplified token smart contract:

pragma solidity ^0.4.24;

contract TokenTest {
    mapping (address => uint) public balances;
    address[] private addresses;

    constructor () public {
        balances[msg.sender] = 10000;
        addresses.push(msg.sender);
    }

    function transfer(address to, uint256 amount) public returns (bool success) {
        if (balances[msg.sender] < amount) return false;
        // Simulate a bug by commenting out this line. We expect the total number of tokens 
        // in circulation will increase because we forgot to subtract amount from the sender's balance.
        // balances[msg.sender] -= amount;
        balances[to] += amount;
        addresses.push(msg.sender);
        addresses.push(to);
        return true;
    }

    function echidna_totalCannotChange() public returns (bool) {
        uint256 total = 0;
        for (uint i = 0; i<addresses.length; i++) {
            total += balances[addresses[i]];
        }
        return total == 10000;
    }
}

I would expect echidna_totalCannotChange to fail after a trivial call sequence (calling transfer once with any arbitrary values). However, to my surprise, when I run echidna-test it passes.

If I comment out the line if (balances[msg.sender] < amount) return false; then the test fails as expected. What I can gather from this is that when echidna generates addresses for calling transfer, it never tries the address which created the contract (msg.sender in the constructor). Therefore, transfer never actually works and no tokens change hands. Is there any way to improve echidna so that it can catch bugs like the one in the contract above?

fail on selfdestruct

i tried fuzzing a contract that anyone can "kill".
echidna didn't fail.
not sure if this is by design. i think it would make sense to have echidna fail if it manages to selfdestruct a contract. (maybe make this the default but add an option to allow it.)

contract self_destruct.sol:

contract SelfDestruct {
  function kill(address _to) public {
      selfdestruct(_to);
  }
  function echidna_alwaystrue() public pure returns (bool) {
      return true;
  }
}

run:

$ echidna-test self_destruct.sol
self_destruct.sol:1:1: Warning: Source file does not specify required compiler version!Consider adding "pragma solidity ^0.4.21;"
contract SelfDestruct {
^ (Relevant source part starts here and spans across multiple lines).
━━━ self_destruct.sol ━━━
  ✓ "echidna_alwaystrue" passed 10000 tests.
  ✓ 1 succeeded.

commit: 83b8fd5

Echidna does not detect if the contract loops

If the contract to test is buggy and runs forever (or a very long time), echidna does not detect this issue. For instance:

contract C {

  function loop() {
    uint x;
    while (true) 
      x=1; 
  }

  function echidna_true() returns (bool) {
    return true;
  }

}

The solution is to limit the amount of gas in the contract to use and report a failure if it runs out of gas.

test specific contract in file

right now echidna-test loads the first contract in a file and tests it.

this is inflexible and doesn't work well with imports as they appear to echidna as the first contracts in a file.

modify echidna-test and loadSolidity to take contract-name as optional second argument

this would open up a useful pattern where one writes a contract as usual without any echidna related modifications and then inherits a test contract from it that contains the echidna properties and a constructor with 0 params that does the required initialization (see #15).

right now this is not possible since the unmodified contract that is inherited from must come first.

add notice if test failed at initialization already

makes it easier to pinpoint reason for failure

Echidna seems to fails a test that always returns true

I tried to test the following contract:

contract Test {
  function f(int val) returns (bool){
    return(true);
  }
  function echidna_alwaystrue() returns (bool){
    return(true);
  }
}

increasing the amount of tests:

diff --git a/src/Main.hs b/src/Main.hs
index b9280e4..a19c2b6 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -14,6 +14,6 @@ main = getArgs >>= \case
   []  -> putStrLn "Please provide a solidity file to analyze"
   f:_ -> do
     (v,a,ts) <- loadSolidity f
-    let prop t = (PropertyName $ show t, ePropertySeq v a (`checkETest` t) 10)
+    let prop t = (PropertyName $ show t, ePropertySeq v a (`checkETest` t) 1000)
     _ <- checkParallel . Group (GroupName f) $ map prop ts
     return ()

But echidna fails when it runs echidna_alwaystrue:

$ echidna-test test.sol 
━━━ test.sol ━━━
  ↯ "echidna_alwaystrue" failed after 46 tests (shrinking)
  ○ 0/1 complete (running)

(the shrinking seems to take forever, so I don't know what it actually finds)

confused why specific test fails

i have the following shrunk version of a contract i'm working on:

pragma solidity ^0.4.18;

contract Example {
    uint256 public maxSupply;
    uint256 public totalSupply;
    uint256 public price;

    mapping (address => uint256) public balances;

    function Example(
        uint256 _maxSupply,
        uint256 _price
    ) public {
        require(_price > 0);
        require(_maxSupply > 0);

        price = _price;
        maxSupply = _maxSupply;
        totalSupply = 0;
    }

    // returns whether the project is fully funded
    function isFunded() public view returns (bool) {
        return totalSupply == maxSupply;
    }

    function () payable public {
        require(!isFunded());
        require(msg.value == price);
        balances[msg.sender] += 1;
        totalSupply += 1;
    }

    function echidna_totalSupplyNeverGreaterThanMaxSupply() public view returns (bool) {
        return totalSupply <= maxSupply;
    }

    function echidna_balanceLinearToSupply() public view returns (bool) {
        return this.balance == totalSupply * price;
    }
}

testing it fails:

$ echidna-test example.sol
━━━ example.sol ━━━
  ✗ "echidna_balanceLinearToSupply" failed after 1 test and 1 shrink.

      │ Call sequence: totalSupply();

  ✗ "echidna_totalSupplyNeverGreaterThanMaxSupply" failed after 1 test.

      │ Call sequence: totalSupply();

  ✗ 2 failed.

i'm confused why this fails at all and especially why it fails with Call sequence: totalSupply();.

it would be great if you could look into that!

using solc version 0.4.18

Inconsistent test results in a simple contract (2)

In this simple contract:

contract A {}

contract B {
  function f() {
    return;
  }
}
 
contract TEST {

  A[] private xs;
  B b = new B(); 
 
  function g() public {
    return;
  }

  //function add() {
  //  xs.push(new A());
  //}

  function echidna_true() returns (bool) {
    b.f();
    return true;
  }
}

the echidna_true test cannot fail and Echida works as expected. However it reports a failed test when you uncomment the add() function. For instance:

$ echidna-test test.sol test.sol:TEST
━━━ test.sol ━━━
  ✗ "echidna_true" failed after 2 tests.
  
    │ Call sequence: add();
  
  ✗ 1 failed.

Echidna cannot deal with values generated during runtime

Echidna cannot find a failed test case in this type of contracts:

contract C {

   bool unconfirmed = true;
   mapping(bytes32 => int) internal hash;

  function suggest_pair(int i, int j) returns (bytes32) {
    require(i*j != 0);
    bytes32 key = keccak256(i,j);
    hash[key] = i*j;
    return key;
  }

  function confirm_pair(bytes32 key) returns (bool) {
    require(hash[key] != 0);
    unconfirmed = false;
    return true;
  }

  function echidna_not_confirmed() returns (bool) {
    return unconfirmed;
  }
}

One possible workaround is to hook the keccak256 EVM instruction in HEVM and collect a list of possible hashes computed by a contract to replay them. Another possibility is ask the user to define a special function to "generate" values given a seed from solidity:

function echidna_generate_bytes32(uint seed) returns (bytes32) { ... }

and then use echidna to run these value generators in solidity to grab values to re-use in the transaction generation.

Echidna should support message value

As in #31, but with the #70 style config rather than explicit function args

loadSolidity requires the contract path/filename in the selectedContract parameter

When using loadSolidity filePath selectedContract, the selectedContract requires the formatting of: "/path/to/contract.sol:SelectedContract", despite the filePath already being provided to loadSolidity.

Clean up Main.hs logic with DoAndIfThenElse

https://kseo.github.io/posts/2014-01-13-DoAndIfThenElse-language-extension.html

I think our indentation in Main.hs can be kinda misleading, this seems like a nice fix

Properties randomly fail when coverage is enabled

If you run echidna-test with a solidity contract, like this one:

contract C {
  function f(uint[] x) returns (uint) {
    return x[0];
  }
  function echidna_true() returns (bool) {
    return true;
  }
}

using this config file:

testLimit: 100
epochs: 10
range: 1
printCoverage: true

It will cause the echidna_true property to fail from time to time. For instance:

$ echidna-test bug.sol --config test.yaml 
...
"Analyzing contract: bug.sol:C"
━━━ bug.sol ━━━
  ✓ "echidna_true" passed 100 tests.
  ✓ 1 succeeded.
━━━ bug.sol ━━━
  ✓ "echidna_true" passed 100 tests.
  ✓ 1 succeeded.
━━━ bug.sol ━━━
  ✓ "echidna_true" passed 100 tests.
  ✓ 1 succeeded.
━━━ bug.sol ━━━
  ✗ "echidna_true" failed after 28 tests.
  
    
  
  ✗ 1 failed.
━━━ bug.sol ━━━
  ✗ "echidna_true" failed after 26 tests.
  
    
  
  ✗ 1 failed.
━━━ bug.sol ━━━
  ✗ "echidna_true" failed after 81 tests.
  
    
  
  ✗ 1 failed.
━━━ bug.sol ━━━
...

README examples are outdated and wrong

Since the big config refactor, our examples in the README are pretty incorrect. We should fix those. Can we get them in CI?

Coverage causes memory leak

Switching to a hash/arc based coverage scheme in #79 has caused a memory leak.

testLimit property

The testLimit property for perprop should represent the number of transactions run before checking a property, not the number of tests echidna runs for that property.

Solidity issue with compiling

reporting/IFeeToken.sol:4:1: Error: Source "libraries/Initializable.sol" not found: File outside of allowed directories.
import 'libraries/Initializable.sol';
^-----------------------------------^

Solidity doesn't allow files in other directories within a source folder by default:

For security reasons the compiler has restrictions what directories it can access. Paths (and their subdirectories) of source files specified on the commandline and paths defined by remappings are allowed for import statements, but everything else is rejected. Additional paths (and their subdirectories) can be allowed via the --allow-paths /sample/path,/another/sample/path switch.

Echidna should allow passing flags to the solidity compiler so that it can be used for analysis of more complicated contracts. For instance, to resolve this issue it'd be great if I could do something like:

echidna-test path/to/File.sol --allow-paths {path name}