Skip to content

Run Echidna tests #1483

Run Echidna tests

Run Echidna tests #1483

Workflow file for this run

name: Run Echidna tests
on:
push:
paths:
- ".github/workflows/echidna.yml"
- "program-analysis/echidna/**/*.sol"
- "program-analysis/echidna/**/*.yml"
branches:
- master
pull_request:
paths:
- ".github/workflows/echidna.yml"
- "program-analysis/echidna/**/*.sol"
- "program-analysis/echidna/**/*.yml"
schedule:
# run CI every day even if no PRs/merges occur
- cron: "0 12 * * *"
jobs:
tests:
name: ${{ matrix.name }}
continue-on-error: ${{ matrix.flaky == true }}
runs-on: ubuntu-22.04
strategy:
fail-fast: false
matrix:
include:
- name: Exercise 1
workdir: program-analysis/echidna/exercises/exercise1/
files: solution.sol
contract: TestToken
outcome: failure
expected: 'echidna_test_balance:\s*failed'
- name: Exercise 2
workdir: program-analysis/echidna/exercises/exercise2/
files: solution.sol
contract: TestToken
outcome: failure
expected: 'echidna_no_transfer:\s*failed'
- name: Exercise 3
workdir: program-analysis/echidna/exercises/exercise3/
files: solution.sol
contract: TestToken
outcome: failure
expected: 'echidna_test_balance:\s*failed'
- name: Exercise 4
workdir: program-analysis/echidna/exercises/exercise4/
files: solution.sol
config: config.yaml
contract: TestToken
outcome: failure
expected: 'transfer(address,uint256):\s*failed'
- name: Exercise 5
workdir: dvdefi/
files: .
config: naivereceiver.yaml
crytic-args: --hardhat-ignore-compile
contract: NaiveReceiverEchidna
outcome: failure
expected: 'echidna_test_contract_balance:\s*failed'
- name: Exercise 6
workdir: dvdefi/
files: .
config: unstoppable.yaml
crytic-args: --hardhat-ignore-compile
contract: UnstoppableEchidna
outcome: failure
expected: 'echidna_testFlashLoan:\s*failed'
- name: Exercise 7
workdir: dvdefi/
files: .
config: sideentrance.yaml
crytic-args: --hardhat-ignore-compile
contract: SideEntranceEchidna
outcome: failure
expected: 'testPoolBalance():\s*failed'
- name: TestToken
workdir: program-analysis/echidna/example/
files: testtoken.sol
contract: TestToken
outcome: failure
expected: 'echidna_balance_under_1000:\s*failed'
- name: Gas estimation
workdir: program-analysis/echidna/example/
files: gas.sol
config: gas.yaml
outcome: success
expected: "f(42,123,"
flaky: true
- name: Multi
workdir: program-analysis/echidna/example/
files: multi.sol
config: filter.yaml
outcome: failure
expected: 'echidna_state4:\s*failed'
- name: Assert
workdir: program-analysis/echidna/example/
files: assert.sol
config: assert.yaml
outcome: failure
expected: 'inc(uint256):\s*failed'
- name: PopsicleBroken
workdir: program-analysis/echidna/example/
files: PopsicleBroken.sol
solc-version: 0.8.4
config: Popsicle.yaml
contract: PopsicleBroken
outcome: failure
expected: 'totalBalanceAfterTransferIsPreserved(address,uint256):\s*failed'
- name: PopsicleFixed
workdir: program-analysis/echidna/example/
files: PopsicleFixed.sol
solc-version: 0.8.4
config: Popsicle.yaml
contract: PopsicleFixed
outcome: success
expected: 'totalBalanceAfterTransferIsPreserved(address,uint256):\s*passing'
- name: TestDepositWithPermit
workdir: program-analysis/echidna/example/
files: TestDepositWithPermit.sol
solc-version: 0.8.0
config: testdeposit.yaml
contract: TestDepositWithPermit
outcome: success
expected: 'testERC20PermitDeposit(uint256):\s*passing'
- name: MultiABI
workdir: program-analysis/echidna/example/
files: allContracts.sol
solc-version: 0.8.0
config: allContracts.yaml
contract: EchidnaTest
outcome: failure
expected: 'test_flag_is_false():\s*failed'
steps:
- name: Checkout repository
uses: actions/checkout@v4
- name: Checkout Damn Vulnerable DeFi solutions
uses: actions/checkout@v4
if: startsWith(matrix.workdir, 'dvdefi')
with:
repository: crytic/damn-vulnerable-defi-echidna
ref: solutions
path: ${{ matrix.workdir }}
- name: Set up Nodejs
uses: actions/setup-node@v3
if: startsWith(matrix.workdir, 'dvdefi')
with:
node-version: 16
- name: Install dependencies and compile
if: startsWith(matrix.workdir, 'dvdefi')
run: |
yarn install --frozen-lockfile
npx hardhat compile --force
working-directory: ${{ matrix.workdir }}
- name: Run Echidna
uses: crytic/echidna-action@v2
id: echidna
continue-on-error: true
with:
files: ${{ matrix.files }}
contract: ${{ matrix.contract }}
config: ${{ matrix.config }}
output-file: ${{ matrix.files }}.out
solc-version: ${{ matrix.solc-version || '0.8.0' }}
echidna-workdir: ${{ matrix.workdir }}
echidna-version: edge
crytic-args: ${{ matrix.crytic-args || '' }}
- name: Verify that the exit code is correct
run: |
if [[ ${{ steps.echidna.outcome }} = ${{ matrix.outcome }} ]]; then
echo "Outcome matches"
else
echo "Outcome mismatch. Expected ${{ matrix.outcome }} but got ${{ steps.echidna.outcome }}"
exit 1
fi
- name: Verify that the output is correct
run: |
if grep -q "${{ matrix.expected }}" "${{ steps.echidna.outputs.output-file }}"; then
echo "Output matches"
else
echo "Output mismatch. Expected something matching '${{ matrix.expected }}'. Got the following:"
cat "${{ steps.echidna.outputs.output-file }}"
exit 1
fi