Run Echidna tests #1413
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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 |