Skip to content

Workflow file for this run

# This Source Code Form is subject to the terms of the Mozilla Public
# License, v. 2.0. If a copy of the MPL was not distributed with this
# file, You can obtain one at http://mozilla.org/MPL/2.0/.
#
# Copyright (c) 2011-2020 ETH Zurich.
name: Verify the router and its dependencies
on:
push:
branches:
- master
pull_request: # run this workflow on every pull_request
env:
headerOnly: 1
module: 'github.com/scionproto/scion'
includePaths: '. verification/dependencies'
assumeInjectivityOnInhale: '1'
parallelizeBranches: '0'
checkConsistency: '1'
imageVersion: 'latest'
mceMode: 'od'
requireTriggers: '1'
useZ3API: '0'
viperBackend: 'SILICON'
disableNL: '0'
unsafeWildcardOptimization: '1'
overflow: '0'
jobs:
verify-deps:
runs-on: ubuntu-latest
steps:
- name: Checkout the VerifiedSCION repository
uses: actions/checkout@v3
# Skip caching for now, the Github action right now is very limited.
# - name: Cache the verification results
# uses: actions/cache@v3
# env:
# cache-name: gobra-cache
# with:
# path: ${{ runner.workspace }}/.gobra/cache.json
# key: ${{ env.cache-name }}
# We split the verification of the entire repository into
# multiple steps. This provides a more fine-grained log in
# Github Workflow's interface and it allows more fine-grained
# control over the settings applied to each package (this last
# point could be also be solved by adapting the action to allow
# per package config).
- name: Verify the packages in the 'verification' directory
uses: viperproject/gobra-action@main
with:
projectLocation: 'VerifiedSCION/verification'
recursive: 1
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: './dependencies/ ..' # relative to project location
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/addr'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/addr'
timeout: 10m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
statsFile: '/stats/stats_addr.json'
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/experimental/epic'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/experimental/epic'
timeout: 7m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/log'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/log'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/private/serrors'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/private/serrors'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/scrypto'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/scrypto'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/slayers'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/slayers'
timeout: 25m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/slayers/path'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/slayers/path'
timeout: 10m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/slayers/path/empty'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/slayers/path/empty'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/slayers/path/epic'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/slayers/path/epic'
# timeout increased; we were having frequent timeouts before
timeout: 10m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/slayers/path/onehop'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/slayers/path/onehop'
timeout: 10m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'pkg/slayers/path/scion'
uses: viperproject/gobra-action@main
with:
packages: 'pkg/slayers/path/scion'
timeout: 30m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'private/topology'
uses: viperproject/gobra-action@main
with:
packages: 'private/topology'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'private/topology/underlay'
uses: viperproject/gobra-action@main
with:
packages: 'private/topology/underlay'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'private/underlay/conn'
uses: viperproject/gobra-action@main
with:
packages: 'private/underlay/conn'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'private/underlay/sockctrl'
uses: viperproject/gobra-action@main
with:
packages: 'private/underlay/sockctrl'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'router/bfd'
uses: viperproject/gobra-action@main
with:
packages: 'router/bfd'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Verify package 'router/control'
uses: viperproject/gobra-action@main
with:
packages: 'router/control'
timeout: 5m
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
parallelizeBranches: ${{ env.parallelizeBranches }}
imageVersion: ${{ env.imageVersion }}
mceMode: ${{ env.mceMode }}
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: ${{ env.disableNL }}
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: ${{ env.unsafeWildcardOptimization }}
- name: Upload the verification report
uses: actions/upload-artifact@v4
with:
name: stats_addr.json
path: /stats/stats_addr.json
if-no-files-found: error # could also be 'warn' or 'ignore'
verify-router:
runs-on: ubuntu-latest
steps:
- name: Checkout the VerifiedSCION repository
uses: actions/checkout@v3
- name: Verify package 'router/'
uses: viperproject/gobra-action@main
with:
packages: 'router/'
timeout: 6h
headerOnly: ${{ env.headerOnly }}
module: ${{ env.module }}
includePaths: ${{ env.includePaths }}
assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
checkConsistency: ${{ env.checkConsistency }}
# Due to a bug introduced in https://github.com/viperproject/gobra/pull/776,
# we must currently disable the chopper, otherwise we well-founded orders
# for termination checking are not available at the chopped Viper parts.
# We should reenable it whenever possible, as it reduces verification time in
# ~8 min (20%).
# chop: 10
parallelizeBranches: '1'
conditionalizePermissions: '1'
moreJoins: 'impure'
imageVersion: ${{ env.imageVersion }}
mceMode: 'on'
requireTriggers: ${{ env.requireTriggers }}
overflow: ${{ env.overflow }}
useZ3API: ${{ env.useZ3API }}
disableNL: '0'
viperBackend: ${{ env.viperBackend }}
unsafeWildcardOptimization: '0'