Workflow file for this run
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
| # 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' |