diff --git a/verification/configs/README.md b/verification/configs/README.md new file mode 100644 index 000000000..5793a50cf --- /dev/null +++ b/verification/configs/README.md @@ -0,0 +1,6 @@ +# Verification job configurations +They can be passed to [gobrago](https://github.com/jcp19/gobrago/tree/main) to verify things with little hassle. + +TODO: +- [ ] Deprecate the `verification/scripts` folder +- [ ] Deprecate the use of the current gobra-action. Instead, rely on a simpler action containing only java and gobrago and use the .json files listed in this folder to verify all packages diff --git a/verification/configs/path.json b/verification/configs/path.json new file mode 100644 index 000000000..8002ee0cf --- /dev/null +++ b/verification/configs/path.json @@ -0,0 +1,11 @@ +{ + "includes": [ + "../..", + "../../verification/dependencies" + ], + "mce_mode": "on", + "module": "github.com/scionproto/scion", + "more_joins": "off", + "parallelize_branches": true, + "pkg_path": "../../pkg/slayers/path/", +} \ No newline at end of file diff --git a/verification/scripts/benchmark/main.go b/verification/scripts/benchmark/main.go new file mode 100644 index 000000000..6550a1534 --- /dev/null +++ b/verification/scripts/benchmark/main.go @@ -0,0 +1,116 @@ +// Copyright 2024 ETH Zurich +// +// Licensed under the Apache License, Version 2.0 (the "License"); +// you may not use this file except in compliance with the License. +// You may obtain a copy of the License at +// +// http://www.apache.org/licenses/LICENSE-2.0 +// +// Unless required by applicable law or agreed to in writing, software +// distributed under the License is distributed on an "AS IS" BASIS, +// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. +// See the License for the specific language governing permissions and +// limitations under the License. + +// This file is meant to be used as a script to benchmarks the verification +// of the dependencies of the router. By default, this runs each relevant +// package three times and reports the results as a .csv. + +package main + +import ( + "fmt" + "log" + "os/exec" + "path/filepath" + "strings" + "time" + // "github.com/jcp19/gobrago" +) + +const runs = 3 +const gobraCmd = "/usr/bin/java -Xss1g -Xmx4g -jar" +const gobraFlags = "/Users/joao/tools/gobra/master_20240414185033/gobra.jar" + +var commands = map[string]string{ + "verification": "--recursive --projectRoot ./verification --backend SILICON --chop 1 -I ./verification/dependencies . --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/addr": "-p ./pkg/addr --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/experimental/epic": "-p ./pkg/experimental/epic --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/log": "-p ./pkg/log --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/private/serrors": "-p ./pkg/private/serrors --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/scrypto": "-p ./pkg/scrypto --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/slayers": "-p ./pkg/slayers --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/slayers/path": "-p ./pkg/slayers/path --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/slayers/path/empty": "-p ./pkg/slayers/path/empty --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/slayers/path/epic": "-p ./pkg/slayers/path/epic --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/slayers/path/onehop": "-p ./pkg/slayers/path/onehop --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "pkg/slayers/path/scion": "-p ./pkg/slayers/path/scion --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "private/topology": "-p ./private/topology --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "private/topology/underlay": "-p ./private/topology/underlay --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "private/underlay/conn": "-p ./private/underlay/conn --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "private/underlay/sockctrl": " -p ./private/underlay/sockctrl --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "router/bfd": "-p ./router/bfd --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", + "router/control": "-p ./router/control --backend SILICON --chop 1 -I . ./verification/dependencies --cacheFile .gobra/cache.json --onlyFilesWithHeader -m github.com/scionproto/scion --assumeInjectivityOnInhale --checkConsistency --mceMode=od --requireTriggers --unsafeWildcardOptimization", +} + +var rootPath = func() string { + path, err := filepath.Abs("../../configs") + if err != nil { + panic(err) + } + return path +}() + +var gobraCfgFile = filepath.Join(rootPath, "gobra.json") + +// maps unique ids to their cfg files +var jobCfgFiles = map[string]string{ + // dataplane + "router": filepath.Join(rootPath, "router.json"), + // first-party dependencies + "pkg/addr": filepath.Join(rootPath, "addr.json"), + "pkg/experimental/epic": filepath.Join(rootPath, "eepic.json"), + "pkg/log": filepath.Join(rootPath, "log.json"), + "pkg/private/serrors": filepath.Join(rootPath, "serrors.json"), + "pkg/scrypto": filepath.Join(rootPath, "scrypto.json"), + "pkg/slayers": filepath.Join(rootPath, "slayers.json"), + "pkg/slayers/path": filepath.Join(rootPath, "path.json"), + "pkg/slayers/path/empty": filepath.Join(rootPath, "pempty.json"), + "pkg/slayers/path/epic": filepath.Join(rootPath, "pepic.json"), + "pkg/slayers/path/onehop": filepath.Join(rootPath, "ponehop.json"), + "pkg/slayers/path/scion": filepath.Join(rootPath, "pscion.json"), + "private/topology": filepath.Join(rootPath, "topology.json"), + "private/topology/underlay": filepath.Join(rootPath, "underlay.json"), + "private/underlay/conn": filepath.Join(rootPath, "conn.json"), + "private/underlay/sockctrl": filepath.Join(rootPath, "sockctrl.json"), + "router/bfd": filepath.Join(rootPath, "bfd.json"), + "router/control": filepath.Join(rootPath, "control.json"), + // third-party lib specs and utils + "dependencies": filepath.Join(rootPath, "dependencies.json"), +} + +func main() { + var verificationTimes = map[string]([]float64){} + for pkg, cmdSuffix := range commands { + fmt.Println("Benchmarking ", pkg) + for i := 0; i < runs; i += 1 { + fmt.Println("Run: ", i+1) + start := time.Now() + cmdStr := strings.Join([]string{gobraCmd, gobraFlags, cmdSuffix}, " ") + cmd := exec.Command("zsh", "-c", cmdStr) + if output, err := cmd.CombinedOutput(); err != nil { + outputStr := string(output) + log.Fatal(outputStr) + return + } + elapsed := time.Since(start) + verificationTimes[pkg] = append(verificationTimes[pkg], elapsed.Seconds()) + } + } + fmt.Println("Verification times as csv:") + fmt.Println("--------------------------") + fmt.Println("Package, Run 1 (s), Run 2 (s), Run 3 (s)") + for pkg, times := range verificationTimes { + fmt.Println(pkg, ",", times[0], ",", times[1], ",", times[2]) + } +} diff --git a/verification/scripts/verification-scripts/scion-verify.py b/verification/scripts/verification-scripts/scion-verify.py deleted file mode 100644 index bdd5271da..000000000 --- a/verification/scripts/verification-scripts/scion-verify.py +++ /dev/null @@ -1,29 +0,0 @@ -## Script to easily verify packages of SCION - -import argparse -from scion import defs, router, path_scion - -def cli_parser(): - # create the top-level parser - parser = argparse.ArgumentParser(prog='scion-verify') - parser.set_defaults(func=lambda _: parser.print_help()) - subparsers = parser.add_subparsers() - - parser_router = subparsers.add_parser('router', help='verify the border router') - parser_router.set_defaults(func=verify_router) - - parser_path_scion = subparsers.add_parser('pscion', help='verify the path/scion package') - parser_path_scion.set_defaults(func=verify_path_scion) - - return parser - -def verify_router(_): - defs.call_gobra(router.dataplane_cfg) - -def verify_path_scion(_): - defs.call_gobra(path_scion.path_cfg) - -if __name__ == "__main__": - parser = cli_parser() - args = parser.parse_args() - args.func(args) diff --git a/verification/scripts/verification-scripts/scion/ __init__.py b/verification/scripts/verification-scripts/scion/ __init__.py deleted file mode 100644 index e69de29bb..000000000 diff --git a/verification/scripts/verification-scripts/scion/defs.py b/verification/scripts/verification-scripts/scion/defs.py deleted file mode 100644 index f60fc0ee8..000000000 --- a/verification/scripts/verification-scripts/scion/defs.py +++ /dev/null @@ -1,146 +0,0 @@ -import os -import platform -import utils -from pathlib import Path - -# TODO: -# - a very lax thread model is assumed. In the future, perform proper sanitization of inputs - -# env -VERIFIEDSCION_DIR_VAR_NAME = 'VERIFIEDSCION_PATH' -VERIFIEDSCION_DIR = utils.read_env_var_or_crash(VERIFIEDSCION_DIR_VAR_NAME) -VERIFIEDSCION_PATH = Path(VERIFIEDSCION_DIR) - -def relative_path(rel_path): - path: Path = Path(VERIFIEDSCION_PATH) / rel_path - return str(path) - -default_includes = [ - VERIFIEDSCION_PATH, - VERIFIEDSCION_PATH / "verification" / "dependencies", -] - -default_module = "github.com/scionproto/scion" - -class GobraConfig: - def __init__(self, - assumeInjectivityOnInhale = True, - backend = "SILICON", - checkConsistency = True, - chop = None, - conditionalizePermissions = False, - directory = list(), - includePackages = default_includes, - # the name of the option below in Gobra is 'input', but this - # is a keyword in python. - inputs = list(), - testFiles = list(), - mceMode = "on", - module = default_module, - onlyFilesWithHeader = True, - parallelizeBranches = False, - printVpr = True, - projectRoot = None, - recursive = False, - requireTriggers = True): - self.assumeInjectivityOnInhale = assumeInjectivityOnInhale - self.backend = backend - self.checkConsistency = checkConsistency - self.chop = chop - self.conditionalizePermissions = conditionalizePermissions - self.directory = directory - self.includePackages = includePackages - self.inputs = inputs - self.testFiles = testFiles - self.mceMode = mceMode - self.module = module - self.onlyFilesWithHeader = onlyFilesWithHeader - self.parallelizeBranches = parallelizeBranches - self.printVpr = printVpr - self.projectRoot = projectRoot - self.recursive = recursive - self.requireTriggers = requireTriggers - - def to_flag_str(self) -> str: - flag_str: str = 'gobra' - if self.assumeInjectivityOnInhale: - flag_str = flag_str + ' --assumeInjectivityOnInhale' - flag_str = flag_str + f' --backend={self.backend}' - if self.checkConsistency: - flag_str = flag_str + ' --checkConsistency' - if self.chop is not None: - flag_str = flag_str + f' chop={self.chop}' - if self.conditionalizePermissions: - flag_str = flag_str + ' --conditionalizePermissions' - if self.directory: - dir_str = ' '.join(self.directory) - flag_str = flag_str + f' --directory {dir_str}' - if self.includePackages: - # TODO: this takes a list of Paths, the other options take a list of - # strs. Make it uniform - include_paths = map(os.path.abspath, self.includePackages) - include_path = ' '.join(include_paths) - flag_str = flag_str + f' -I {include_path}' - if self.inputs or self.testFiles: - all_inputs = self.inputs + self.testFiles - inputs = ' '.join(all_inputs) - flag_str = flag_str + f' -i {inputs}' - flag_str = flag_str + f' --mceMode {self.mceMode}' - flag_str = flag_str + f' -m {self.module}' - if self.onlyFilesWithHeader: - flag_str = flag_str + ' --onlyFilesWithHeader' - if self.parallelizeBranches: - flag_str = flag_str + ' --parallelizeBranches' - if self.printVpr: - flag_str = flag_str + ' --printVpr' - if self.projectRoot is not None: - exit("Project root option not yet implemented") - if self.recursive: - flag_str = flag_str + ' --recursive' - if self.requireTriggers: - flag_str = flag_str + ' --requireTriggers' - return flag_str - - def notification_str(self): - flag_str = '' - if self.directory: - dir_str = ' '.join(self.directory) - flag_str = flag_str + f' --directory {dir_str}' - if self.inputs or self.testFiles: - all_inputs = self.inputs + self.testFiles - inputs = ' '.join(all_inputs) - flag_str = flag_str + f' -i {inputs}' - flag_str = flag_str + f' --mceMode {self.mceMode}' - if self.parallelizeBranches: - flag_str = flag_str + ' --parallelizeBranches' - if self.printVpr: - flag_str = flag_str + ' --printVpr' - if self.recursive: - flag_str = flag_str + ' --recursive' - return flag_str - - - -def record_run(): - # TODO: save the config that was executed (flags), - # save a zip of scion package (without .git), - # save the commits or the name of the Gobra, silicon, and viperserver - # deps, verification time, - pass - -def call_gobra(config: GobraConfig, color=True, sound=False, notification=False): - cmd_str = config.to_flag_str() - print(f'Running {cmd_str}') - color_cmd_suffix = "| grep --color=always 'Error at: <.*>.*\|$'" - if color: - cmd_str = f'{cmd_str} {color_cmd_suffix}' - # not working - # result_success = os.system(cmd_str) == 0 - os.system(cmd_str) - if sound: - print('\a\a\a\a') - if notification and platform.system() == 'Darwin': - # not working - # result_msg = "SUCCESS" if result_success else "FAILURE" - mac_notification = f"osascript -e 'display notification \"{config.notification_str()}\" with title \"Verification Finished\"'" - os.system(mac_notification) diff --git a/verification/scripts/verification-scripts/scion/path_scion.py b/verification/scripts/verification-scripts/scion/path_scion.py deleted file mode 100644 index b4255a004..000000000 --- a/verification/scripts/verification-scripts/scion/path_scion.py +++ /dev/null @@ -1,27 +0,0 @@ -from . import defs - -path_files_rel_paths = [ - "pkg/slayers/path/scion/base.go", - "pkg/slayers/path/scion/base_spec.gobra", - "pkg/slayers/path/scion/decoded.go", - "pkg/slayers/path/scion/decoded_spec.gobra", - "pkg/slayers/path/scion/raw.go", - "pkg/slayers/path/scion/raw_spec.gobra", -] - -path_test_files_rel_paths = [ - "pkg/slayers/path/scion/base_spec_test.gobra", - "pkg/slayers/path/scion/decoded_spec_test.gobra", - "pkg/slayers/path/scion/raw_spec_test.gobra", -] - -path_files = list(map(defs.relative_path, path_files_rel_paths)) -path_test_files = list(map(defs.relative_path, path_test_files_rel_paths)) - -path_cfg = defs.GobraConfig( - inputs = path_files, - # testFiles = dataplane_test_files_rel_paths, - conditionalizePermissions = False, - mceMode = "on", - parallelizeBranches = True, -) diff --git a/verification/scripts/verification-scripts/scion/router.py b/verification/scripts/verification-scripts/scion/router.py deleted file mode 100644 index d606db359..000000000 --- a/verification/scripts/verification-scripts/scion/router.py +++ /dev/null @@ -1,27 +0,0 @@ -from . import defs - -dataplane_files_rel_paths = [ - "router/dataplane.go", - "router/bfd_spec.gobra", - "router/dataplane_spec.gobra", - "router/metrics_spec.gobra", - "router/metrics.go", - "router/svc_spec.gobra", - "router/svc.go", -] - -dataplane_test_files_rel_paths = [ - "router/dataplane_spec_test.gobra", - "router/svc_spec_test.gobra", -] - -dataplane_files = list(map(defs.relative_path, dataplane_files_rel_paths)) -dataplane_test_files = list(map(defs.relative_path, dataplane_test_files_rel_paths)) - -dataplane_cfg = defs.GobraConfig( - inputs = dataplane_files, - # testFiles = dataplane_test_files_rel_paths, - conditionalizePermissions = True, - mceMode = "on", - parallelizeBranches = True, -)