1#!/usr/bin/env python 2# -*- coding: utf-8 -*- 3 4# 5# Copyright 2017, Data61 6# Commonwealth Scientific and Industrial Research Organisation (CSIRO) 7# ABN 41 687 119 230. 8# 9# This software may be distributed and modified according to the terms of 10# the BSD 2-Clause license. Note that NO WARRANTY is provided. 11# See "LICENSE_BSD2.txt" for details. 12# 13# @TAG(DATA61_BSD) 14# 15 16''' 17This file contains unit test cases related to the seL4Notification connector. 18''' 19 20from __future__ import absolute_import, division, print_function, \ 21 unicode_literals 22 23import os, re, shutil, six, subprocess, sys, unittest 24from pycparser import c_ast, c_generator, c_parser 25 26ME = os.path.abspath(__file__) 27MY_DIR = os.path.dirname(ME) 28 29# Make CAmkES importable 30sys.path.append(os.path.join(os.path.dirname(ME), '../../..')) 31 32from camkes.internal.tests.utils import CAmkESTest, spin_available 33 34class TestSel4Notification(CAmkESTest): 35 def test_locking_protocol(self): 36 ''' 37 The seL4Notification connector uses a binary semaphore internally to protect 38 accesses to callback registration. Any functions contained on the "to" 39 side, if they acquire this semaphore, are expected to release it before 40 exiting. In an early draft of the connector code, there was a single 41 execution path where we failed to release the semaphore. This test case 42 validates that we always release the semaphore when appropriate, and 43 never release it without having first acquired it. 44 45 Note that the static analysis performed in this test case is highly 46 simplified and specialised for this connector code. It makes many 47 assumptions about code idioms and over approximations of the control 48 flow. If you are modifying the seL4Notification connector code in any 49 non-trivial way, do not expect to get by without having to modify this 50 test case. 51 52 Some specific limitations of the static analysis: 53 - No support for `for` loops, `do-while` loops, `switch`, ternary 54 conditionals, `goto`, `asm`, attributes and more; 55 - `while` loops are treated as executing 0 or 1 times; 56 - No shortcut logic (e.g. `0 && lock()` would be considered lock 57 acquisition); 58 - No support for `break`; 59 - No restriction on recursive acquisition of the semaphore (even 60 though the one we're using doesn't support recursive acquisition); 61 - No support for // style comments; 62 - Probably more 63 ''' 64 src = munge(os.path.join(MY_DIR, '../seL4Notification-to.template.c')) 65 ast = parse(src) 66 for node in ast.ext: 67 # Test all contained functions. 68 if isinstance(node, c_ast.FuncDef): 69 check_termination(src, node.decl.name, node.body.block_items) 70 71 @unittest.skipIf(not spin_available(), 'Spin not found') 72 def test_sel4notification_safety(self): 73 pml = os.path.join(MY_DIR, 'sel4notification.pml') 74 75 tmp = self.mkdtemp() 76 77 subprocess.check_call(['spin', '-a', pml], cwd=tmp) 78 79 pan_safety = os.path.join(tmp, 'pan-safety') 80 subprocess.check_call(['gcc', '-o', pan_safety, '-O3', '-DREACH', 81 '-DSAFETY', 'pan.c'], cwd=tmp, universal_newlines=True) 82 83 p = subprocess.Popen([pan_safety], stdout=subprocess.PIPE, 84 stderr=subprocess.PIPE, universal_newlines=True) 85 stdout, stderr = p.communicate() 86 87 if p.returncode != 0: 88 self.fail('pan-safety returned %s' % p.returncode) 89 90 if stdout.find('errors: 0') < 0: 91 self.fail('pan-safety failed:\n%s' % stdout) 92 93 @unittest.skipIf(not spin_available(), 'Spin not found') 94 def test_sel4notification_liveness(self): 95 pml = os.path.join(MY_DIR, 'sel4notification.pml') 96 97 tmp = self.mkdtemp() 98 99 subprocess.check_call(['spin', '-a', '-m', pml], cwd=tmp) 100 101 pan_liveness = os.path.join(tmp, 'pan-safety') 102 subprocess.check_call(['gcc', '-o', pan_liveness, '-O3', '-DNP', 103 '-DNOREDUCE', 'pan.c'], cwd=tmp) 104 105 p = subprocess.Popen([pan_liveness, '-l', 'm100000'], 106 stdout=subprocess.PIPE, stderr=subprocess.PIPE, 107 universal_newlines=True) 108 stdout, stderr = p.communicate() 109 110 if p.returncode != 0: 111 self.fail('pan-liveness returned %s' % p.returncode) 112 113 if stdout.find('errors: 0') < 0: 114 self.fail('pan-liveness failed:\n%s' % stdout) 115 116# A brief prelude to the seL4Notification-to.template.c source to give it some types 117# it expects in the absence of the libsel4 headers. 118HEADER = ''' 119 typedef int seL4_CPtr; 120 typedef unsigned long seL4_Word; 121''' 122 123def munge(filename): 124 ''' 125 Tweak the seL4Notification-to.template.c source to suppress some external 126 references and constructs pycparser can't handle. 127 ''' 128 stripped = reduce(lambda acc, x: re.sub(x[0], x[1], acc, flags=re.MULTILINE), 129 130 # Turn template variable definitions into source variable definitions. 131 ((r'/\*-\s*set\s+(notification|handoff|lock)\s*=.*?-\*/', 132 r'static seL4_CPtr \g<1>;'), 133 (r'/\*-\s*set\s+badge_magic\s*=.*?-\*/', 134 r'static seL4_Word badge_magic;'), 135 136 # Turn template variable reference into source variable references. 137 (r'/\*\?\s*(notification|handoff|lock|badge_magic)\s*\?\*/', r'\g<1>'), 138 139 # Remove comments. 140 (r'/\*(.|\n)*?\*/', ''), 141 142 # Remove usage of the UNUSED macro. 143 (r'\sUNUSED\s', ' '), 144 145 # Remove CPP directives. 146 (r'^#.*?$', ''), 147 148 # Remove CAmkES error invocations. 149 (r'ERR\((.|\n)*?{(.|\n)*?}(.|\n)*?{(.|\n)*?}\)\);', '')), 150 151 open(filename, 'rt').read()) 152 return '%s%s' % (HEADER, stripped) 153 154def parse(string): 155 ''' 156 Parse C source code into a pycparser AST. 157 ''' 158 return c_parser.CParser().parse(string) 159 160def lock_operations(statement): 161 ''' 162 Find the number of `lock()` operations within a statement. Note that we 163 count `unlock()` as -1 to compute a total. This function makes many 164 simplifications, including performing no control flow analysis, and thus 165 may be inaccurate. 166 ''' 167 ops = 0 168 if isinstance(statement, c_ast.FuncCall): 169 if statement.name.name == 'lock': 170 ops = 1 171 elif statement.name.name == 'unlock': 172 ops = -1 173 174 # Descend into this node's children if it has any. 175 if isinstance(statement, c_ast.Node): 176 ops += sum(lock_operations(x) for x in statement.children()) 177 elif isinstance(statement, tuple): 178 ops += sum(lock_operations(x) for x in statement) 179 180 return ops 181 182class LockProtocolError(Exception): 183 ''' 184 An error indicating a failure to release a lock or too many lock releases 185 on an exit path. 186 ''' 187 188 def __init__(self, message, source, node=None): 189 if node is not None: 190 # Compute a pretty printed version of the source code indicating the 191 # terminating line of execution that leads to the error. 192 content = six.cStringIO() 193 for lineno, line in enumerate(source.split('\n')): 194 content.write('%s %s\n' % 195 ('>' if lineno == int(node.coord.line) else ' ', line)) 196 super(LockProtocolError, self).__init__('%s\n%s' % 197 (message, content.getvalue())) 198 else: 199 super(LockProtocolError, self).__init__(message) 200 201def check_termination(source, name, statements, accumulated=None, locks=0): 202 ''' 203 Ensure the lock protocol is preserved on all paths through this series of 204 statements. 205 206 source - source code containing these statements (for diagnostics) 207 name - name of the containing function 208 statements - statements to analyse 209 accumulated - statements we have passed leading up to the current series 210 locks - number of locks we currently hold 211 ''' 212 213 if accumulated is None: 214 accumulated = [] 215 216 if statements is None: 217 statements = [] 218 219 for index, statement in enumerate(statements): 220 221 if isinstance(statement, c_ast.While): 222 # For `while` loops, we assume the condition is always evaluated 223 # and then the body is executed either 0 or 1 times. The recursive 224 # call here is the 1 case and the continuing (fall through) 225 # execution is the 0 case. 226 locks += lock_operations(statement.cond) 227 if locks < 0: 228 raise LockProtocolError('lock release while no lock held in ' 229 '%s at line %s' % (name, statement.coord.line), source, 230 statement) 231 check_termination(source, name, statement.stmt.block_items + 232 statements[index+1:], accumulated + statements[:index+1], 233 locks) 234 235 elif isinstance(statement, c_ast.If): 236 # For `if` statements, we assume any lock operations in the 237 # condition expression are only relevant for the else branch. This 238 # is based on the following idiom for taking a lock: 239 # 240 # if (lock() != 0) { 241 # /* failure case; lock() should not be counted */ 242 # } else { 243 # /* success case; lock() should be counted */ 244 # } 245 246 # If branch. 247 check_termination(source, name, ([statement.iftrue] if 248 statement.iftrue is not None else []) + statements[index+1:], 249 accumulated + statements[:index+1], locks) 250 251 # Else branch. 252 locks += lock_operations(statement.cond) 253 if locks < 0: 254 raise LockProtocolError('lock release while no lock held in ' 255 '%s at else branch of line %s' % (name, 256 statement.coord.line), source, statement) 257 check_termination(source, name, ([statement.iffalse] if 258 statement.iffalse is not None else []) + statements[index+1:], 259 accumulated + statements[:index+1], locks) 260 261 # Together, the recursive calls have handled the remainder of this 262 # function, so no need to continue. 263 return 264 265 elif isinstance(statement, (c_ast.Return, c_ast.Continue)): 266 # We've reached a termination point of this function. Note that we 267 # count a `continue` statement as a point of termination. This is 268 # based on the following idiom for restarting a function, which we 269 # assume is the only use of `continue`: 270 # 271 # void foo() { 272 # while (true) { 273 # ... 274 # continue; /* restart function */ 275 # ... 276 # } 277 # } 278 279 # Take into account any lock operations in the return expression 280 # itself, though we expect there to be none. 281 locks += lock_operations(statement) 282 283 if locks > 0: 284 raise LockProtocolError('%s locks potentially held when ' 285 'exiting %s at line %s' % (locks, name, 286 statement.coord.line), source, statement) 287 elif locks < 0: 288 raise LockProtocolError('%s too many lock releases ' 289 'potentially executed before exiting %s at line %s' % 290 (-locks, name, statement.coord.line), source, statement) 291 292 # Otherwise, we're good. 293 294 return 295 296 elif isinstance(statement, c_ast.Compound): 297 # Statement block. Recurse into it. 298 check_termination(source, name, (statement.block_items or []) + 299 statements[index+1:], accumulated + statements[:index+1], 300 locks) 301 return 302 303 else: 304 # Regular statement. Count its locks. 305 locks += lock_operations(statement) 306 307 # If we reached here, this function terminated without a return statement 308 # (perfectly valid for a `void` function). 309 310 # Find the last statement executed in case we need to raise an exception. 311 if len(statements) > 0: 312 last = statements[-1] 313 elif len(accumulated) > 0: 314 last = accumulated[-1] 315 else: 316 last = None 317 318 if last is None: 319 location = 'end of function' 320 else: 321 location = 'line %s' % last.coord.line 322 323 if locks > 0: 324 raise LockProtocolError('%s locks potentially held when exiting %s at ' 325 '%s' % (locks, name, location), source, last) 326 elif locks < 0: 327 raise LockProtocolError('%s too many lock releases potentially ' 328 'executed before exiting %s at %s' % (-locks, name, location), 329 source, last) 330 331 # If we reached here, the function conformed to the protocol in an 332 # execution that reached its end. 333 334if __name__ == '__main__': 335 unittest.main() 336