Skip to content

extends CI to test artifact #5

extends CI to test artifact

extends CI to test artifact #5

Workflow file for this run

name: Verification of NSL Case Study
on:
push:
jobs:
verify:
runs-on: ubuntu-latest
timeout-minutes: 10
container:
image: ghcr.io/viperproject/gobra@sha256:0e7419455a3648d006e8a9957380e94c1a8e52d2d4b1ce2425af852dc275fb29 # Gobra commit f21fe70
steps:
- name: Install prerequisites
run: apt-get update && apt-get install -y git wget jq
- name: Checkout repo
uses: actions/checkout@v3
- name: Install Go
run: |
mkdir tmp
cd tmp
wget --quiet https://go.dev/dl/go1.17.3.linux-amd64.tar.gz
rm -rf /usr/local/go && tar -C /usr/local -xzf go1.17.3.linux-amd64.tar.gz
cd ../
rm -rf tmp
# add go to path
echo "/usr/local/go/bin" >> $GITHUB_PATH
- name: Point Go to repo copy
run: go mod edit -replace github.com/viperproject/ReusableProtocolVerificationLibrary=$GITHUB_WORKSPACE/ReusableVerificationLibrary
working-directory: casestudies/nsl
- name: Compile NSL initiator & responder
run: ./compile.sh
working-directory: casestudies/nsl
- name: Execute NSL initiator & responder
run: ./nsl
working-directory: casestudies/nsl
- name: Setup verification of NSL
run: |
./load-modules.sh "$GITHUB_WORKSPACE/.modules"
mkdir -p $GITHUB_WORKSPACE/.modules/github.com/viperproject
working-directory: casestudies/nsl
- name: Link Reusable Verification Library
run: ln -s $GITHUB_WORKSPACE/ReusableVerificationLibrary .modules/github.com/viperproject/ReusableProtocolVerificationLibrary
- name: Verify NSL initiator role 1
run: |
mkdir -p .gobra
gobraJar="/gobra/gobra.jar"
additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/nsl/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/nsl --parallelizeBranches"
java -Xss128m -jar $gobraJar --recursive -I ./ $additionalGobraArgs --includePackages initiator
working-directory: casestudies/nsl
- name: Verify NSL initiator role 2
run: |
mkdir -p .gobra
gobraJar="/gobra/gobra.jar"
additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/nsl/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/nsl --parallelizeBranches"
java -Xss128m -jar $gobraJar --recursive -I ./ $additionalGobraArgs --includePackages initiator2
working-directory: casestudies/nsl
- name: Verify NSL responder role
run: |
mkdir -p .gobra
gobraJar="/gobra/gobra.jar"
additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/nsl/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/nsl --parallelizeBranches"
java -Xss128m -jar $gobraJar --recursive -I ./ $additionalGobraArgs --includePackages responder
working-directory: casestudies/nsl
- name: Verify NSL trace invariants & main package
run: |
mkdir -p .gobra
gobraJar="/gobra/gobra.jar"
additionalGobraArgs="-I $GITHUB_WORKSPACE/casestudies/nsl/.verification/precedence -I $GITHUB_WORKSPACE/.modules --module github.com/viperproject/ProtocolVerificationCaseStudies/nsl --parallelizeBranches"
# verify packages located in the current directory and in `common`:
java -Xss128m -jar $gobraJar --directory ./ common -I ./ $additionalGobraArgs
working-directory: casestudies/nsl