Add script to automate build & running kani #78
Conversation
jaisnan
changed the title
jaisnan
force-pushed
the
add-script-to-automate-build
branch
from
5ba1b85
to
c18d6d5
Compare
| @@ -35,4 +35,11 @@ jobs: | |||
| submodules: true | |||
|
|
|||
| - name: Run Kani Script | |||
There was a problem hiding this comment.
Should this be named "Test Kani Script?"
There was a problem hiding this comment.
I think this first step is in fact checking the standard library with Kani, right?
There was a problem hiding this comment.
Yes, i shall separate the steps into test kani, following which I shall run kani on the standard library on the whole.
| - name: Run Kani Script without -p | ||
| working-directory: ${{github.workspace}}/head |
There was a problem hiding this comment.
Couldn't the testing of the script itself be done in a separate job?
There was a problem hiding this comment.
I'd initially put it in a separate job, but merged it all into one based on this comment #78 (comment)
There was a problem hiding this comment.
Hmm, but given it's testing the script itself, shouldn't we have a workflow that doest just the script testing, and that workflow should only execute when any of the files relating to the script (the script itself plus toml files perhaps) change?
There was a problem hiding this comment.
Just to clarify, I wasn't saying they had to be merged in the same job. It just wasn't clear to me what each workflow was doing.
I would suggest that you test the script as a separate job of this workflow. But make it clear what each step is testing, so people are not confused. Maybe add some comments explaining what this is testing.
| check_binary_exists() { | ||
| local build_dir="$1" | ||
| local expected_commit="$2" | ||
| local kani_path="$build_dir/scripts/kani" |
There was a problem hiding this comment.
Consider using get_kani_path
| main() { | ||
| local current_dir=$(pwd) | ||
| local build_dir="$WORK_DIR/kani_build" | ||
| local temp_dir_target=$(mktemp -d) |
There was a problem hiding this comment.
Shouldn't this come with something like
cleanup()
{
rm -rf "$temp_dir_target"
}
trap cleanup EXIT?
| "$kani_path" --version | ||
|
|
||
| echo "Running Kani verify-std command..." | ||
| cd $current_dir |
There was a problem hiding this comment.
This should not be necessary.
|
|
||
|
|
||
| main() { | ||
| local current_dir=$(pwd) |
| cd $current_dir | ||
|
|
||
| # Run the command with the provided arguments (if any) | ||
| if [ -n "$command_args" ]; then |
There was a problem hiding this comment.
I don't think this branching is necessary, you can just use "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args either way as you are not using set -u.
Co-authored-by: Michael Tautschnig <mt@debian.org>
| run: head/scripts/run-kani.sh --path ${{github.workspace}}/head | ||
|
|
||
| - name: Run Kani Script with --kani-args and -p | ||
| run: head/scripts/run-kani.sh -p ${{github.workspace}}/head --kani-args --harness ptr::verify::check_read_u128 --harness ptr::unique::verify::check_as_mut |
There was a problem hiding this comment.
I would suggest that you change the arguments to be something that doesn't depend on the harnesses configuration, or something very generic, like --harness ptr, which is less likely to be broken if we rename a harness.
There was a problem hiding this comment.
Since you are changing this file. Can you please rename line 19 (build) or give the workflow a nice name? 😊
kani/features/verify-std--kani-argsto pass arguments to kani command.-psets the working directory.Extras
Cleans up some print statements in the
run_update_with_checksscript.Call-out
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.