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