Share personal scripts (#229)

verification/scripts/verification-scripts/install-gobra.py

@@ -0,0 +1,111 @@
+## Script to install and manage versions of Gobra
+
+import argparse
+from pathlib import Path
+import os
+import shutil
+import time
+import utils
+
+INSTAL_DIR = utils.read_env_var_or_crash('GOBRA_INSTALLS')
+GOBRA_REPO = utils.read_env_var_or_crash('GOBRA_REPO')
+GOBRA_CMD_FILE = utils.read_env_var_or_crash('GOBRA_CMD_FILE')
+USER_TMP_DIR = utils.read_env_var_or_crash('USER_TMP_FOLDER')
+DEFAULT_FILE = '.default'
+GOBRA_VERSION_FILE = Path(INSTAL_DIR) / DEFAULT_FILE
+USER_TMP_DIR_PATH = Path(USER_TMP_DIR) 
+
+# TODO:
+# - init command that setups up all directories, touches the cmd file and makes it executable (chmod)
+# - the thread model is a bit loose yet. This script may allow for shell injection
+# - allow the user to specify the branch of silicon and fetch it
+
+def cli_parser():
+    # create the top-level parser
+    parser = argparse.ArgumentParser(prog='gobra-install')
+    parser.set_defaults(func=lambda _: parser.print_help())
+    subparsers = parser.add_subparsers()
+
+    parser_install = subparsers.add_parser('install', help='install a Gobra version')
+    parser_install.add_argument('branch')
+    parser_install.add_argument('--set', action=argparse.BooleanOptionalAction)
+    parser_install.set_defaults(func=install)
+
+    parser_list = subparsers.add_parser('list', help='list all installed versions of Gobra')
+    parser_list.set_defaults(func=list_gobra)
+
+    parser_set = subparsers.add_parser('set', help='set version of Gobra to run by default')
+    parser_set.add_argument('version')
+    parser_set.set_defaults(func=set_gobra)
+    return parser
+
+def install(args):
+    assert utils.isvalidgitbranch(args.branch), "The provided branch name is not a valid identifier"
+    clone = f'git clone --recurse-submodules {GOBRA_REPO}'
+    change_branch = f'git checkout {args.branch} > /dev/null 2>&1'
+    assembly = 'sbt assembly'
+
+    target_dir = USER_TMP_DIR_PATH / 'gobra'
+    date = time.strftime('%Y%m%d%H%M%S')
+    output_dir = f'{args.branch}_{date}'
+    output_dir_path = Path(INSTAL_DIR) / output_dir
+
+    if not os.path.exists(target_dir):
+        os.chdir(USER_TMP_DIR_PATH)
+        exit_code = os.system(clone)
+        if exit_code != 0:
+            exit("Failed to clone repo")
+    os.chdir(target_dir)
+    exit_code = os.system(change_branch)
+    if exit_code != 0:
+        exit(f'Branch {args.branch} not found')
+    exit_code = os.system('git pull')
+    if exit_code != 0:
+        exit("Failed to pull the most recent version of the branch")
+    exit_code = os.system(assembly)
+    if exit_code != 0:
+        exit("Failed to build Gobra")
+    os.mkdir(output_dir_path)
+    shutil.move(USER_TMP_DIR_PATH / 'gobra' / 'target' / 'scala-2.13' / 'gobra.jar', output_dir_path)
+    if args.set:
+        set_gobra_helper(output_dir)
+
+def list_gobra(args):
+    files = os.listdir(INSTAL_DIR)
+    default = None
+    if GOBRA_VERSION_FILE.name in files:
+        with open(GOBRA_VERSION_FILE, 'r') as gobra_version_file:
+            default = gobra_version_file.read().strip()
+    print("Installed versions:")
+    for f in files:
+        if f == GOBRA_VERSION_FILE.name:
+            pass
+        elif f == default:
+            print(f'* {f}')
+        else:
+            print(f'- {f}')
+
+def set_gobra(args):
+    assert utils.isvalidgitbranch(args.version), "The provided version name is not a valid identifier"
+    if not os.path.exists(Path(INSTAL_DIR) / args.version):
+        exit("The version could not be found")
+    set_gobra_helper(args.version)
+
+def set_gobra_helper(version):
+    Path(GOBRA_VERSION_FILE).touch(exist_ok=True)
+    Path(GOBRA_CMD_FILE).touch(exist_ok=True)
+    with open(GOBRA_VERSION_FILE, 'w') as gobra_version_file:
+        gobra_version_file.write(version)
+    with open(GOBRA_CMD_FILE, 'w') as gobra_cmd_file:
+        shebang = '#!/usr/bin/env bash\n'
+        path_exec = Path(INSTAL_DIR) / version / 'gobra.jar'
+        cmd = f'java -Xss128m -Xmx4g -jar {path_exec} "$@"'
+        # generate executable file
+        gobra_cmd_file.write(shebang)
+        gobra_cmd_file.write(cmd)
+
+if __name__ == "__main__":
+    parser = cli_parser()
+    args = parser.parse_args()
+    args.func(args)
+

verification/scripts/verification-scripts/scion-verify.py

@@ -0,0 +1,29 @@
+## 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)

verification/scripts/verification-scripts/scion/defs.py

@@ -0,0 +1,146 @@
+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)

verification/scripts/verification-scripts/scion/path_scion.py

@@ -0,0 +1,27 @@
+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,
+)

verification/scripts/verification-scripts/scion/router.py

@@ -0,0 +1,27 @@
+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,
+)

verification/scripts/verification-scripts/utils.py

@@ -0,0 +1,19 @@
+import os
+import re
+
+def read_env_var_or_crash(name):
+    val = os.getenv(name)
+    if val is None:
+        print(f'Environment variable {name} not found.')
+        print('If the environment var contains a path, please ensure it is an absolut path.')
+        exit(1)
+    else:
+        return val
+
+def run_cmd_or_exit(cmd, err_msg):
+    exit_code = os.system(cmd)
+    if exit_code != 0:
+        exit(err_msg)
+
+def isvalidgitbranch(str):
+    return re.fullmatch(r"([a-zA-Z0-9_])+", str) is not None