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