1#!/usr/bin/env python3
2#
3# Copyright 2018, Data61
4# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
5# ABN 41 687 119 230.
6#
7# This software may be distributed and modified according to the terms of
8# the BSD 2-Clause license. Note that NO WARRANTY is provided.
9# See "LICENSE_BSD2.txt" for details.
10#
11# @TAG(DATA61_BSD)
12#
13
14'''
15Set up and run tests for CAmkES capDL refinement proofs.
16'''
17
18import itertools
19import os
20import shutil
21import subprocess
22import sys
23import tempfile
24import time
25
26# Test these apps. Commented-out tests are those that don't work
27# but we have a good idea of what needs to be fixed.
28test_apps = [
29    'adder',
30    #'aeroplage', # x86 only
31    #'alignment', # x86 only
32    'attributes',
33    'binary-semaphore',
34    'cakeml_hello',
35    #'cakeml_regex', # FIXME: requires setting -DCAKEMLDIR in init-build
36    'cakeml_tipc',
37    'cms-donate',
38    'cs-donate',
39    'cs-nodonate',
40    'dataport',
41    #'debug-simple', # x86 only
42    'dhcp',
43    'dma-example',
44    'epit',
45    'event',
46    'event-driven',
47    'exchangestring',
48    'filter',
49    'global-imports',
50    #'hellorust', # x86 only
51    'hierarchical-attributes',
52    'hierarchical-components',
53    #'keyboard', # x86 only
54    'lockserver',
55    'mcs-donate',
56    'mcs-nodonate',
57    'multiassembly',
58    'multiclient',
59    #'multiplier', # camkes ADL model doesn't support int array
60    'mutex',
61    'periodic',
62    #'pit', # x86 only
63    'reversestring',
64    'rotate',
65    #'rumprun_ethernet', # x86 only
66    #'rumprun_hello',    # x86 only
67    #'rumprun_pthreads', # x86 only
68    #'rumprun_rust',     # x86 only
69    'serialserver_polling',
70    'serialserver_interrupt',
71    'serialserver_loopback',
72    'simple',
73    'simplesingleaddressspace',
74    'socket',
75    'structs',
76    'swapcounter',
77    'terminal',
78    'testbufvariant',
79    'testcamkes438',
80    'testcontrolname',
81    'testdataportbifurcate',
82    'testdataportmux',
83    'testdataportmuxflat',
84    'testdataportptrwrap',
85    'testdataportrpc',
86    'testfaulthandlers',
87    'testgrouping',
88    'testgroupingcontrol',
89    'testhardwareinterrupt',
90    'testhwdataportlrgpages',
91    'testnto1mmio',
92    'testnto1overload',
93    'testrefin',
94    'testreplycapprotection',
95    'testsel4notification',
96    'testsingleaddressspaceheap',
97    #'teststringarrays', # camkes ADL model doesn't support array of string
98    'testsyscalls',
99    'testunderscorename',
100    'timeserver',
101    'uart',
102    #'vgatest', # x86 only
103    ]
104
105# Test these option combinations.
106# The first value of each option list will be the default used in this
107# test runner (once we add a command line option for that).
108test_options = {
109    # Having extra fault handler threads and EPs shouldn't matter,
110    # because they are internal to components.
111    'CAmkESFaultHandlers': ['1'],
112
113    # This only gives each component access to its own TCB,
114    # which shouldn't affect the integrity model.
115    'CAmkESProvideTCBCaps': ['1'],
116}
117
118# Default app build options.
119# This builds for the current verified ARM platform, sabre (on QEMU).
120standard_build_config = {
121    'PLATFORM': 'sabre',
122    'ARM': '1',
123    'CAmkESCapDLVerification': '1',
124    'CAmkESCapDLStaticAlloc': '1',
125}
126# TODO: accept extra config on command line
127
128# PLATFORM adjustments.
129override_app_platform = {
130    'serialserver_interrupt': 'exynos5410',
131    'serialserver_polling': 'exynos5410',
132    'serialserver_loopback': 'exynos5410',
133    'uart': 'kzm',
134}
135
136
137# Messages
138# TODO: allow adjusting verbosity
139def info(msg):
140    print('run_tests: info: %s' % msg)
141
142def fatal(msg):
143    print('run_tests: fatal: %s' % msg, file=sys.stderr)
144    sys.exit(1)
145
146def run_cmd(cmdline, **kwargs):
147    '''Run a command, printing its output if it fails'''
148    print('run_tests: command: %s' %
149          ', '.join([repr(cmdline)] + ['%s=%s' % x for x in kwargs.items()]))
150    start = time.time()
151    try:
152        return subprocess.check_output(cmdline, stderr=subprocess.STDOUT, **kwargs)
153    except subprocess.CalledProcessError as exn:
154        print('run_tests: command failed with code %d' % exn.returncode)
155        print(exn.output.decode('utf-8'))
156        raise
157    finally:
158        duration = time.time() - start
159        if duration > 1.0:
160            info('command took %.3g seconds' % duration)
161
162class TempDir():
163    '''Context manager for a temporary directory.'''
164    def __init__(self, prefix=None, parent_dir=None, cleanup_on_error=True):
165        self.prefix = prefix
166        self.parent_dir = parent_dir
167        self.cleanup_on_error = cleanup_on_error
168
169    def __enter__(self):
170        self.filename = tempfile.mkdtemp(prefix=self.prefix, dir=self.parent_dir)
171        return self.filename
172
173    def __exit__(self, exn_type, exn_val, traceback):
174        if exn_type is None or self.cleanup_on_error:
175            shutil.rmtree(self.filename)
176        return False # propagate exceptions
177
178# Expected paths, relative to the root of the camkes project structure
179camkes_tool_rel_dir = 'projects/camkes-tool'
180isabelle_rel_dir    = 'projects/l4v/isabelle'
181l4v_rel_dir         = 'projects/l4v/l4v'
182init_build_rel_path = 'init-build.sh'
183
184# Main.
185# TODO: argparse
186def main():
187    info('Testing %d apps...' % len(test_apps))
188
189    this_script_dir = os.path.dirname(os.path.realpath(__file__))
190    # Expected path to our script
191    if this_script_dir.endswith('projects/camkes-tool/cdl-refine-tests'):
192        # Build in the project root by default
193        camkes_root = os.path.normpath(os.path.join(this_script_dir, '../../..'))
194        if camkes_root != os.getcwd():
195            info('Changing directory to project root: %s' % camkes_root)
196            os.chdir(camkes_root)
197    else:
198        camkes_root = os.getcwd() # guessed
199
200    def get_abs_path(rel_path):
201        '''Resolve a path in the camkes project dir'''
202        return os.path.normpath(os.path.join(camkes_root, rel_path))
203
204    # Find the entry point to the project's build system.
205    init_build_tool = get_abs_path(init_build_rel_path)
206    if not os.path.exists(init_build_tool):
207        fatal('init-build.sh not found at: %s' % init_build_tool)
208
209    # Show the CAmkES version.
210    try:
211        camkes_tool_rev = subprocess.check_output(
212            ['git', 'describe', '--tags'],
213            cwd=get_abs_path(camkes_tool_rel_dir)
214        ).decode('utf-8')
215    except subprocess.CalledProcessError as exn:
216        camkes_tool_rev = 'unknown [error: %s]' % str(exn)
217    info('camkes-tool revision: %s' % camkes_tool_rev)
218
219    # Find Isabelle.
220    isabelle_dir = get_abs_path(isabelle_rel_dir)
221    isabelle_tool = os.path.join(isabelle_dir, 'bin/isabelle')
222    if not os.path.exists(isabelle_tool):
223        fatal('''isabelle not found at: %s
224(Make sure to check out the correct project manifest)''' % isabelle_tool)
225    try:
226        isabelle_rev = subprocess.check_output(
227            ['git', 'describe', '--tags'],
228            cwd=isabelle_dir
229            ).decode('utf-8')
230    except subprocess.CalledProcessError as exn:
231        isabelle_rev = 'unknown [error: %s]' % str(exn)
232    info('Isabelle revision: %s' % isabelle_rev)
233
234    # Find l4v.
235    l4v_dir = get_abs_path(l4v_rel_dir)
236    if not os.path.exists(l4v_dir):
237        fatal('l4v not found at: %s' % l4v_dir)
238    try:
239        l4v_rev = subprocess.check_output(
240            ['git', 'describe', '--tags'],
241            cwd=l4v_dir
242            ).decode('utf-8')
243    except subprocess.CalledProcessError as exn:
244        l4v_rev = 'unknown [error: %s]' % str(exn)
245    info('l4v revision: %s' % l4v_rev)
246
247    # Find ninja-build.
248    ninja_build_tool = 'ninja'
249    try:
250        ninja_version = subprocess.check_output(
251            [ninja_build_tool, '--version']
252            ).decode('utf-8')
253        info('ninja-build version: %s' % ninja_version)
254    except OSError as exn:
255        fatal('''can't run ninja-build tool at: %s
256[%s]''' % (ninja_build_tool, str(exn)))
257
258    # Some of the l4v sessions rely on generated files.
259    # Here, we run l4v's own build system to generate them.
260    # Also pre-build the CAmkES formal model while we're at it.
261
262    # NB: we can't use l4v/run_tests directly because it builds with
263    #     slightly different Isabelle env options, causing our
264    #     'isabelle build' in build_one() to miss the image cache
265    info('Setting up l4v...')
266    run_cmd(['./misc/regression/run_tests.py', '-v', 'CamkesCdlRefine'],
267            cwd=l4v_dir)
268    info('Done setting up l4v')
269
270    # Keep track of which apps or options caused failures.
271    def init_per_opt_counts():
272        return dict(((k, v), 0)
273                    for k, vals in
274                        [('app', test_apps)] + list(test_options.items())
275                    for v in vals)
276    def incr_opt_counts(counts, app_name, build_opts):
277        counts[('app', app_name)] += 1
278        for k, v in build_opts.items():
279            counts[(k, v)] += 1
280    def num_counts(counts):
281        return sum(count for (opt_name, opt_val), count in counts.items()
282                   if opt_name == 'app')
283
284    # Set up test counters.
285    per_opt_tests  = init_per_opt_counts()
286    per_opt_failed = init_per_opt_counts()
287    per_opt_error  = init_per_opt_counts()
288
289    def build_one(app_name, this_build_config):
290        '''Do one test run for the given app and build options.'''
291        # Use temporary directory, but in the project root.
292        # Any other location should also work, but this is the
293        # ���standard��� place for it.
294        with TempDir(prefix='build-%s-' % app_name,
295                     parent_dir=os.getcwd(),
296                     cleanup_on_error=False
297                    ) as build_dir:
298            try:
299                try:
300                    info('Build directory: %s' % build_dir)
301                    app_build_config = dict(standard_build_config)
302                    if app_name in override_app_platform:
303                        app_build_config['PLATFORM'] = override_app_platform[app_name]
304                    build_cmdline = (
305                        [init_build_tool,
306                         '-DCAMKES_APP=%s' % app_name] +
307                        ['-D%s=%s' % opt for opt in sorted(app_build_config.items())] +
308                        ['-D%s=%s' % opt for opt in sorted(this_build_config.items())]
309                        )
310                    run_cmd(build_cmdline, cwd=build_dir)
311                    run_cmd([ninja_build_tool], cwd=build_dir)
312                    info('App build succeeded.')
313
314                    # We expect the build system to generate theory files here
315                    app_thy_dir = os.path.join(build_dir, 'cdl-refine')
316                except (BaseException, Exception):
317                    # failed, but not in proofs
318                    incr_opt_counts(per_opt_error, app_name, this_build_config)
319                    raise
320
321                try:
322                    info('Running proofs...')
323                    isabelle_cmdline = [
324                        'timeout', '1h',
325                        isabelle_tool, 'build',
326                        '-d', l4v_dir,
327                        '-D', app_thy_dir,
328                        '-v'
329                    ]
330                    run_cmd(isabelle_cmdline, cwd=build_dir)
331                except Exception:
332                    # proof failed
333                    incr_opt_counts(per_opt_failed, app_name, this_build_config)
334                    raise
335                except BaseException:
336                    # might be KeyboardInterrupt; not proof failure
337                    incr_opt_counts(per_opt_error, app_name, this_build_config)
338                    raise
339            except (BaseException, Exception) as exn:
340                info('Build directory retained at: %s' % build_dir)
341                raise
342
343    # Main test loop.
344    try:
345        for app_name in test_apps:
346            for this_build_config in map(dict, itertools.product(
347                    *[[(k, v) for v in vals]
348                      for k, vals in sorted(test_options.items())])):
349                incr_opt_counts(per_opt_tests, app_name, this_build_config)
350
351                info('Testing app: %s' % app_name)
352                info('Build config for this test:')
353                if this_build_config:
354                    for k, v in sorted(this_build_config.items()):
355                        info('    %s=%s' % (k, v))
356                else:
357                    info('    (nothing)')
358
359                try:
360                    build_one(app_name, dict(this_build_config))
361                    info('Test succeeded.\n\n')
362                except Exception as exn:
363                    info('Test failed with exception:\n  %s\n\n' % str(exn))
364    except KeyboardInterrupt:
365        info('Aborting tests...')
366
367    num_tests  = num_counts(per_opt_tests)
368    num_failed = num_counts(per_opt_failed)
369    num_error  = num_counts(per_opt_error)
370    num_passed = num_tests - num_failed - num_error
371    info('Summary: %d test(s), %d passed, %d failed, %d error' %
372         (num_tests, num_passed, num_failed, num_error))
373
374    # Print details of which options are associated with failures.
375    for desc, num, per_opt_counts in (
376                ('Failure', num_failed, per_opt_failed),
377                ('Error', num_error, per_opt_error)
378            ):
379        if num:
380            info('%s counts:' % desc)
381            counts = []
382            for (k, v), tests in per_opt_counts.items():
383                failed = per_opt_counts[(k, v)]
384                if failed == 0:
385                    continue
386                counts.append((float(failed) / tests,
387                               failed, tests, k, v))
388            def most_failures(x):
389                frac_failed, failed, tests, k, v = x
390                return (-frac_failed, -failed, k) # tiebreak on k
391            for frac_failed, failed, tests, k, v in sorted(counts, key=most_failures):
392                info('    %d/%d when %s=%s' % (failed, tests, k, v))
393
394    return 1 if num_failed or num_error else 0
395
396if __name__ == '__main__':
397    sys.exit(main())
398