Skip to content

Commit

Permalink
Kani Workflow Updates (model-checking#214)
Browse files Browse the repository at this point in the history
Update the `kani list` part of our workflow to:
- Be its own step of the workflow so it can run in parallel, which is
nice because it finishes much faster than the other jobs in the Kani
workflow
- Use the new markdown format. This makes the list much more readable
(compare [current
format](https://github.com/model-checking/verify-rust-std/actions/runs/12199714877/attempts/2#summary-34034201022)
to [markdown
format](https://github.com/carolynzech/verify-rust-std/actions/runs/12203155221/attempts/1#summary-34045490103)).

Also remove the Test Kani workflow step, because it's expensive and
duplicates verification work.
  • Loading branch information
carolynzech authored Dec 10, 2024
1 parent 6928d22 commit 16a155a
Show file tree
Hide file tree
Showing 2 changed files with 12 additions and 27 deletions.
37 changes: 11 additions & 26 deletions .github/workflows/kani.yml
Original file line number Diff line number Diff line change
Expand Up @@ -38,18 +38,10 @@ jobs:
# Step 2: Run Kani on the std library (default configuration)
- name: Run Kani Verification
run: head/scripts/run-kani.sh --path ${{github.workspace}}/head

test-kani-script:
name: Test Kani script
runs-on: ${{ matrix.os }}
strategy:
matrix:
os: [ubuntu-latest, macos-latest]
include:
- os: ubuntu-latest
base: ubuntu
- os: macos-latest
base: macos

run-kani-list:
name: Kani List
runs-on: ubuntu-latest
steps:
# Step 1: Check out the repository
- name: Checkout Repository
Expand All @@ -58,25 +50,18 @@ jobs:
path: head
submodules: true

# Step 2: Test Kani verification script with specific arguments
- name: Test Kani script (Custom Args)
run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr --output-format=terse

# Step 3: Test Kani verification script in the repository directory
- name: Test Kani script (In Repo Directory)
working-directory: ${{github.workspace}}/head
run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse

# Step 4: Run list on the std library and add output to job summary
# Step 2: Run list on the std library
- name: Run Kani List
run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head


# Step 3: Add output to job summary
- name: Add Kani List output to job summary
uses: actions/github-script@v6
with:
script: |
const fs = require('fs');
const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8');
const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani-list.md', 'utf8');
await core.summary
.addRaw(kaniOutput)
.write();
.addHeading('Kani List Output', 2)
.addRaw(kaniOutput, false)
.write();
2 changes: 1 addition & 1 deletion scripts/run-kani.sh
Original file line number Diff line number Diff line change
Expand Up @@ -221,7 +221,7 @@ main() {
--cbmc-args --object-bits 12
elif [[ "$run_command" == "list" ]]; then
echo "Running Kani list command..."
"$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std > $path/kani_list.txt
"$kani_path" list -Z list -Z function-contracts -Z mem-predicates -Z float-lib ./library --std --format markdown
fi
}

Expand Down

0 comments on commit 16a155a

Please sign in to comment.