1#!/usr/bin/env python 2# 3# 4# Copyright 2017, CSIRO 5# 6# This software may be distributed and modified according to the terms of 7# the BSD 2-Clause license. Note that NO WARRANTY is provided. 8# See "LICENSE_BSD2.txt" for details. 9# 10# @TAG(NICTA_BSD) 11# 12 13import os 14import sys 15 16# Settings 17L4V_ARCH_DEFAULT="ARM" 18L4V_ARCH_LIST=["ARM","ARM_HYP","X64","RISCV64"] 19 20# Fetch directory this script is stored in. 21DIR=os.path.dirname(os.path.realpath(__file__)) 22 23# Add repo version of Isabelle to our path. 24os.environ["PATH"] += os.pathsep + DIR 25 26# Export L4V_ARCH variable as ARM (Default) 27if not os.environ.has_key("L4V_ARCH"): 28 os.environ["L4V_ARCH"] = L4V_ARCH_DEFAULT 29 30L4V_ARCH=os.environ["L4V_ARCH"] 31 32# Test Orphanage when L4V_ARCH=ARM; 33# we need to set this flag here to test the above equality in the ROOT file. 34# To be removed when we finish proving Orphanage for ARM_HYP and X64 35if L4V_ARCH == "ARM": 36 os.environ["L4V_ARCH_IS_ARM"]= L4V_ARCH 37 print "Testing Orphanage for ARM" 38 39# Check we are using a known Architecture 40if L4V_ARCH not in L4V_ARCH_LIST: 41 sys.exit("Unknown architecture L4V_ARCH=%s" % L4V_ARCH) 42 43print "Testing for L4V_ARCH=%s:" % L4V_ARCH 44 45# enable timing logs in isabelle builds and set report interval to 3 seconds 46os.environ["ISABELLE_TIMING_LOG"]="3.0s" 47 48# Enable quick_and_dirty mode for various images 49if os.environ.has_key("QUICK_AND_DIRTY"): 50 os.environ["AINVS_QUICK_AND_DIRTY"]=1 51 os.environ["REFINE_QUICK_AND_DIRTY"]=1 52 os.environ["CREFINE_QUICK_AND_DIRTY"]=1 53 print "Testing with QUICK_AND_DIRTY" 54 55# Lists of excluded tests for diferent archs 56EXCLUDE={} 57 58EXCLUDE["ARM_HYP"]=[ 59 "Access", 60 "Bisim", 61 "DRefine", 62 "RefineOrphanage", 63 "SimplExportAndRefine"] 64 65EXCLUDE["ARM"]=[] 66 67EXCLUDE["X64"]=[ 68 "Access", 69 "AutoCorresSEL4", 70 "Bisim", 71 "CamkesDarpaReport", 72 "CamkesGlueProofs", 73 "DBaseRefine", 74 "DSpec", 75 "RefineOrphanage", 76 "SepTacticsExamples", 77 "SimplExportAndRefine", 78 "AsmRefine" 79] 80 81EXCLUDE["RISCV64"]=[ 82 "AInvs", 83 "ASepSpec", 84 "DSpec", 85 "c-kernel", 86 "CKernel", 87 "CSpec", 88 "CamkesDarpaReport", 89 "CamkesGlueProofs", 90 "RefineOrphanage", 91 "AsmRefine" 92] 93 94# Check EXCLUDE is exhaustive over the available architectures 95if not set(L4V_ARCH_LIST) <= set(EXCLUDE.keys()): 96 sys.exit("[INTERNAL ERROR] exclusion lists are non-exhaustive") 97 98# Run the tests from the script directory. 99os.chdir(DIR) 100 101# Arguments: 102args = ['./misc/regression/run_tests.py'] # Script name 103args += [r for t in EXCLUDE[L4V_ARCH] for r in ['-r', t]] # Exclusion list 104args += sys.argv[1:] # Other arguments 105 106# Run the thing!! 107os.execvp('./misc/regression/run_tests.py',args) 108