Skip to content

Commit

Permalink
adds echidna to test suite [CENT-186]
Browse files Browse the repository at this point in the history
  • Loading branch information
Alec Schaefer committed Aug 9, 2018
1 parent 1fc5d67 commit 05a0bc3
Show file tree
Hide file tree
Showing 6 changed files with 188 additions and 0 deletions.
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -10,3 +10,4 @@ artifacts/
contracts/.DS_Store
token.json
credentials.json
echidna/
3 changes: 3 additions & 0 deletions .gitmodules
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
[submodule "echidna"]
path = echidna
url = [email protected]:trailofbits/echidna.git
37 changes: 37 additions & 0 deletions echidna_tests/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
#Setup

1. Install the full version of [solc] http://solidity.readthedocs.io/en/v0.4.24/installing-solidity.html via homebrew (not npm).

2. Clone the echidna repository by running:
`git submodule update --init --recursive`
(echidna is included in .gitignore)

3. Install stack:
`brew install haskell-stack`

4. Run the following commands from inside the echidna directory.
`stack upgrade
stack setup
stack install`

5. If this gives you errors involving 'readline' on MacOS, try running:
`brew install readline
brew link readline --force
export LDFLAGS=-L/usr/local/opt/readline/lib
export CPPFLAGS=-I/usr/local/opt/readline/include
stack install readline --extra-include-dirs=/usr/local/opt/readline/include --extra-lib-dirs=/usr/local/opt/readline/lib
stack install`

6. Add `/Users/$(whoami)/.local/bin` to your `PATH` variable:
`export PATH=$PATH:/Users/$(whoami)/.local/bin`

7. Open `echidna_tests/config.yaml` in a text editor and replace the words `REPLACE_WITH_PWD`
with the path to your centre-tokens directory. To get this path, run `echo $PWD`.

8. The echidna_tests suite contains negative and positive test files.
* To run the positive tests, open `config.yaml` and set the field `returnType`
to `Success`. Then, run the following command from your centre-tokens directory:
`echidna-test echidna_tests/positive.sol echidna_tests/positive.sol:Test --config="echidna_tests/config.yaml"`
* To run the negative tests, open `config.yaml` and set the field `returnType`
to `Fail or Throw`. Then, run the following command from your centre-tokens directory:
`echidna-test echidna_tests/negative.sol echidna_tests/negative.sol:Test --config="echidna_tests/config.yaml"`
33 changes: 33 additions & 0 deletions echidna_tests/config.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
#Arguments to solc
# PLEASE CHANGE THE LINE BELOW to include the absolute path of your working directory.
solcArgs: openzeppelin-solidity=REPLACE_WITH_PWD/node_modules/openzeppelin-solidity zos-lib=/Users/alecschaefer/Documents/GitHub/centre-tokens/node_modules/zos-lib contracts=REPLACE_WITH_PWD/contracts
#Choose the number of epochs to use in coverage-guided testing
#epochs: 2
#Set the gas limit for each test
#gasLimit: 0xfffff
#Number of tests that will run for each property
testLimit: 10000
#Max call sequence length
range: 10
#Contract's address in the EVM
contractAddr: 0x00a329c0648769a73afac7f9381e08fb43dbea72
#Sender's address in the EVM
sender: 0x00a329c0648769a73afac7f9381e08fb43dbea70
#List of addresses that will be used in all tests
addrList:
- 0x00a329c0648769a73afac7f9381e08fb43dbea70
- 0x00a329c0648769a73afac7f9381e08fb43dbea72
- 0x67518339e369ab3d591d3569ab0a0d83b2ff5198
- 0x0
#Shrink Limit
shrinkLimit: 1000
#Test Prefix
prefix: echidna_
#Print full coverage
printCoverage: false
#Return Type
# - Success: all tests should return true
# - Fail: all tests should return false
# - Throw: all tests should revert
# - Fail or Throw: all tests should either return false or revert
returnType: Fail or Throw
46 changes: 46 additions & 0 deletions echidna_tests/negative.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,46 @@
pragma solidity ^0.4.24;

import "contracts/FiatTokenV1.sol";

contract Test is FiatTokenV1 {

//Note: These are special addresses used by echidna––please don't change.
address testerAddr = 0x00a329c0648769a73afac7f9381e08fb43dbea70;
address otherAddr = 0x67518339e369ab3d591d3569ab0a0d83b2ff5198;
address ownerAddr = 0x00a329c0648769a73afac7f9381e08fb43dbea72;
uint256 initial_totalSupply = 1000000000;

constructor () {
/* config.yaml sets this contract's address to ownerAddr, so we
need to initialize all the contract roles to this address so that calls
from the contract pass funtion modifiers.*/
initialize('Test', '', '', 6, ownerAddr, ownerAddr, ownerAddr, ownerAddr);
configureMinter(ownerAddr, initial_totalSupply);
mint(testerAddr, initial_totalSupply/2);
require(balanceOf(testerAddr) == initial_totalSupply/2);
mint(otherAddr, initial_totalSupply/2);
require(balanceOf(otherAddr) == initial_totalSupply/2);
}

function echidna_failed_transaction() returns (bool) {
uint balance = balanceOf(testerAddr);
transfer(testerAddr, balance+1);
return (true);
}

function echidna_self_approve_and_failed_transferFrom_to_zero() returns (bool) {
uint balance = balanceOf(testerAddr);
approve(testerAddr, 0);
approve(testerAddr, balance);
transferFrom(testerAddr, 0x0, balance);
return (true);
}

function echidna_multiple_approves() returns (bool) {
transfer(ownerAddr, 1);
uint balance = balanceOf(ownerAddr);
approve(testerAddr, balance);
approve(testerAddr, balance);
return (allowed[ownerAddr][testerAddr] == balance);
}
}
68 changes: 68 additions & 0 deletions echidna_tests/positive.sol
Original file line number Diff line number Diff line change
@@ -0,0 +1,68 @@
pragma solidity ^0.4.24;

import "contracts/FiatTokenV1.sol";

contract Test is FiatTokenV1 {

//Note: These are special addresses used by echidna––don't change.
address testerAddr = 0x00a329c0648769a73afac7f9381e08fb43dbea70;
address otherAddr = 0x67518339e369ab3d591d3569ab0a0d83b2ff5198;
address ownerAddr = 0x00a329c0648769a73afac7f9381e08fb43dbea72;
uint256 initial_totalSupply = 1000000000;

constructor () {
/* config.yaml sets this contract's address to ownerAddr, so we
need to initialize all the contract roles to this address so that calls
from the contract pass funtion modifiers.*/
initialize('Test', '', '', 6, ownerAddr, ownerAddr, ownerAddr, ownerAddr);
configureMinter(ownerAddr, initial_totalSupply);
mint(testerAddr, initial_totalSupply/2);
require(balanceOf(testerAddr) == initial_totalSupply/2);
mint(otherAddr, initial_totalSupply/2);
require(balanceOf(otherAddr) == initial_totalSupply/2);
}

function echidna_max_balance() returns (bool) {
// config.yaml specifies testerAddr is always the 'sender' address in transfers.
return (balanceOf(testerAddr) <= initial_totalSupply/2 && balanceOf(otherAddr) >= initial_totalSupply/2);
}

function echidna_no_burn_using_zero() returns (bool) {
return (balanceOf(0x0) == 0);
}

function echidna_self_transfer() returns (bool) {
uint balance = balanceOf(testerAddr);
var b = transfer(testerAddr, balance);
return (balanceOf(testerAddr) == balance && b);
}

function echidna_zero_transfer() returns (bool) {
return (transfer(otherAddr, 0));
}

function echidna_fixed_supply() returns (bool) {
return (totalSupply() == initial_totalSupply);
}

function echidna_self_approve_and_self_transferFrom() returns (bool) {
uint balance = balanceOf(testerAddr);
approve(testerAddr, 0);
approve(testerAddr, balance);
return (transferFrom(testerAddr, testerAddr, balance));
}

function echidna_self_approve_and_transferFrom() returns (bool) {
uint balance = balanceOf(testerAddr);
approve(testerAddr, 0);
approve(testerAddr, balance);
return (transferFrom(testerAddr, otherAddr, balance));
}

function echidna_multiple_approves() returns (bool) {
uint balance = balanceOf(testerAddr);
approve(ownerAddr, balance);
approve(ownerAddr, balance);
return (allowed[testerAddr][ownerAddr] == balance);
}
}

0 comments on commit 05a0bc3

Please sign in to comment.