Misinterpretation of stuck result for #assume(false) as depth-bound(0) #607
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: KEVM Performance Test | |
| on: | |
| # Trigger when commenting on an issue or PR, or editing a comment | |
| # Issue/PR MUST already be labeled properly | |
| issue_comment: | |
| types: [created, edited] | |
| jobs: | |
| Prepare: | |
| if: | | |
| contains(github.event.issue.labels.*.name, 'performance') && | |
| ( contains(github.event.comment.body, '/KEVM-perf-run') ) | |
| # Comment must contain this exact string to trigger a test run. | |
| # The comment _may_ also contain a (version) tag for the K version, | |
| # after this trigger, like "/KEVM-perf-run v5.4.32". | |
| runs-on: [Linux, flyweight] | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| steps: | |
| - name: Check User Org Association | |
| run: | | |
| set -euo pipefail | |
| echo $(pwd) | |
| echo "Testing User Org Relationship: $GITHUB_ACTOR" | |
| gh auth status | |
| if ! gh api -H "Accept: application/vnd.github+json" /orgs/runtimeverification/members/$GITHUB_ACTOR; then | |
| exit 1 | |
| fi | |
| - name: Check that we are on a PR | |
| run: | | |
| [ -n "${{ github.event.issue.pull_request }}" ] && echo "OK, we are on a PR" | |
| Profiling: | |
| needs: Prepare | |
| runs-on: [Linux, performance] | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| steps: | |
| - name: Clean _work Folder | |
| run: | | |
| echo "Cleaning Folder" | |
| rm -rf ./* | |
| - name: Determine commit to use | |
| id: determine-commit | |
| run: | | |
| echo "PR_HEAD=$(curl -s ${{ github.event.issue.pull_request.url }} | jq '.head.sha' | xargs echo)" | tee -a $GITHUB_OUTPUT | |
| echo "K_TAG=$(echo ${{ github.event.comment.body }} | grep -oP '(?<=/KEVM-perf-run )v[0-9]+(\.[0-9]+){2} ?')" | tee -a $GITHUB_OUTPUT | |
| - name: Run Tests | |
| run: | | |
| set -euo pipefail | |
| ISSUE_NUMBER=$(cat ${GITHUB_EVENT_PATH} | jq '.issue.number') | |
| PR_HEAD=${{ steps.determine-commit.outputs.PR_HEAD }} | |
| if [ -n "${{ steps.determine-commit.outputs.K_TAG }}" ]; then | |
| K_OVERRIDE="--override-input k-framework github:runtimeverification/k/${{ steps.determine-commit.outputs.K_TAG }}" | |
| K_TAG=${{ steps.determine-commit.outputs.K_TAG }} | |
| else | |
| K_OVERRIDE="" | |
| K_TAG="" | |
| fi | |
| TIMESTAMP=$(date +"%Y%m%dT%H%M%S") | |
| # FIXME can we use a reaction emoji instead? | |
| gh issue comment ${ISSUE_NUMBER} --body "Running KEVM test with ${PR_HEAD:-master} and K version ${K_TAG} as ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| echo "Starting Test Execution" | |
| echo "RUNNING TEST" | |
| nix build github:runtimeverification/evm-semantics#profile \ | |
| --override-input k-framework/haskell-backend github:runtimeverification/haskell-backend/${PR_HEAD} \ | |
| ${K_OVERRIDE} \ | |
| -o KEVM-timing-${TIMESTAMP}-${PR_HEAD}.data | |
| echo "Comparing with current master" | |
| nix build github:runtimeverification/evm-semantics#profile \ | |
| --override-input k-framework/haskell-backend github:runtimeverification/haskell-backend/$GITHUB_SHA \ | |
| ${K_OVERRIDE} \ | |
| -o KEVM-timing-${TIMESTAMP}-master.data | |
| nix run github:runtimeverification/evm-semantics#compare-profiles -- KEVM-timing-$TIMESTAMP-${PR_HEAD}.data KEVM-timing-$TIMESTAMP-master.data | tee KEVM-timing-comparison.data | |
| - name: Publish Results | |
| uses: actions/[email protected] | |
| with: | |
| path: ./KEVM-timing*.data | |
| on-success: | |
| needs: Profiling | |
| runs-on: [Linux, flyweight] | |
| if: ${{ always() && contains(join(needs.*.result, ','), 'success') }} | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| steps: | |
| - run: | | |
| ISSUE_NUMBER=$(cat ${GITHUB_EVENT_PATH} | jq '.issue.number') | |
| gh issue -R ${{ github.repository }} comment ${ISSUE_NUMBER} --body "KEVM test finished: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" | |
| on-failure: | |
| needs: Profiling | |
| runs-on: [Linux, flyweight] | |
| if: ${{ always() && contains(join(needs.*.result, ','), 'failure') }} | |
| env: | |
| GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} | |
| steps: | |
| - run: | | |
| ISSUE_NUMBER=$(cat ${GITHUB_EVENT_PATH} | jq '.issue.number') | |
| gh issue -R ${{ github.repository }} comment ${ISSUE_NUMBER} --body "KEVM test FAILED: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}" |