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