run_tests

#!/usr/bin/env python3
#
# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: BSD-2-Clause
#

import os
import sys
import argparse
import subprocess

# Settings
L4V_ARCH_DEFAULT="ARM"
L4V_ARCH_LIST=["ARM","ARM_HYP","X64","RISCV64"]

# Fetch directory this script is stored in.
DIR=os.path.dirname(os.path.realpath(__file__))

# Add repo version of Isabelle to our path.
os.environ["PATH"] += os.pathsep + DIR

# Enable tracking stuck tasks, and set report interval to 3 seconds
os.environ["ISABELLE_TIMING_LOG"]="3.0s"

# Enable quick_and_dirty mode for various images
if "QUICK_AND_DIRTY" in os.environ:
    os.environ["AINVS_QUICK_AND_DIRTY"]=1
    os.environ["REFINE_QUICK_AND_DIRTY"]=1
    os.environ["CREFINE_QUICK_AND_DIRTY"]=1
    print("Testing with QUICK_AND_DIRTY")

# Lists of excluded tests for different archs
EXCLUDE={}

EXCLUDE["ARM_HYP"]=[
    "Access",
    "Bisim",
    "DRefine",
    "RefineOrphanage",
    "SimplExportAndRefine"]

EXCLUDE["ARM"]=[]

EXCLUDE["X64"]=[
    "Access",
    "AutoCorresSEL4",
    "CamkesDarpaReport",
    "CamkesGlueProofs",
    "DBaseRefine",
    "DSpec",
    "RefineOrphanage",
    "SepTacticsExamples",
    "SimplExportAndRefine",
    "AsmRefine"
]

EXCLUDE["RISCV64"]=[
    "Access",
    "AutoCorresSEL4",
    "DSpec",
    "DBaseRefine",
    "CamkesDarpaReport",
    "CamkesGlueProofs",
    "AsmRefine"
]

# Check EXCLUDE is exhaustive over the available architectures
if not set(L4V_ARCH_LIST) <= set(EXCLUDE.keys()):
    sys.exit("[INTERNAL ERROR] exclusion lists are non-exhaustive")

parser = argparse.ArgumentParser(add_help=False)
parser.add_argument('--l4v-arches', metavar='ARCH,...', type=str,
                    help='test multiple L4V_ARCHs (comma-separated)')
parser.add_argument('--l4v-arch-all', dest='l4v_arches',
                    action='store_const', const=','.join(L4V_ARCH_LIST),
                    help='test all L4V_ARCHes')
parser.add_argument('-h', '--help', action='store_true',
                    help=argparse.SUPPRESS)

args, passthrough_args = parser.parse_known_args()

if args.l4v_arches:
    archs = args.l4v_arches.split(',')
elif "L4V_ARCH" in os.environ:
    archs = [os.environ["L4V_ARCH"]]
else:
    archs = [L4V_ARCH_DEFAULT]

for arch in archs:
    if arch not in L4V_ARCH_LIST:
        sys.exit("Unknown architecture: %s" % arch)

if args.help:
    parser.print_help()
    print('Now printing help for main regression script:')
    print('--------')
    passthrough_args += ['--help']
    archs = archs[:1]

returncode = 0
for arch in archs:
    print("Testing for L4V_ARCH=%s:" % arch)

    os.environ["L4V_ARCH"] = arch
    # Test Orphanage when L4V_ARCH=ARM;
    # we need to set this flag here to test the above equality in the ROOT file.
    # To be removed when we finish proving Orphanage for ARM_HYP and X64
    if arch == "ARM":
        os.environ["L4V_ARCH_IS_ARM"] = arch
        print("Testing Orphanage for ARM")
    elif "L4V_ARCH_IS_ARM" in os.environ:
        del os.environ["L4V_ARCH_IS_ARM"]

    # Arguments:
    args  = ['./misc/regression/run_tests.py']            # Script name
    args += [r for t in EXCLUDE[arch] for r in ['-r', t]] # Exclusion list
    args += passthrough_args                              # Other arguments

    # Run the tests from the script directory.
    # Also collect the last non-zero return code.
    returncode = subprocess.call(args, cwd=DIR) or returncode
sys.exit(returncode)