1#!/usr/bin/env python
2#
3# Copyright (c) 2010-2023 Antmicro
4#
5# This file is licensed under the MIT License.
6# Full license text is available in 'licenses/MIT.txt'.
7#
8
9# This script provides convenience functions for debugging user-space seL4 applications.
10# All of the commands are available under `sel4` prefix, e.g. `sel4 break`, `sel4 thread`, etc.
11# To use this script in GDB you have to source it first, either using `source` command or running
12# GDB with `-x <path/to/gdbscript.py>` argument.
13#
14# Example: break on main function in rootserver thread
15#
16# (gdb) sel4 wait-for-thread rootserver
17# (gdb) sel4 switch-symbols rootserver
18# (gdb) sel4 break rootserver main
19# (gdb) continue
20
21import os
22import os.path
23import sys
24from enum import IntEnum
25from glob import glob
26import pickle
27
28
29def get_envvar(name):
30    if name not in os.environ:
31        raise gdb.GdbError("{} environment variable is not set".format(name))
32    else:
33        return os.environ[name]
34
35
36SYMBOL_AUTOSWITCHING = True
37SOURCE_DIR = get_envvar('SOURCE_DIR')
38sys.path.append(os.path.join(SOURCE_DIR, 'projects', 'capdl', 'python-capdl-tool'))
39
40import capdl
41
42
43class CapDLSource:
44    def __init__(self, spec_pickle):
45        with open(spec_pickle, 'rb') as f:
46            cdl = pickle.load(f)
47
48        self.threads = {obj.name for obj in cdl.obj_space if isinstance(obj, capdl.TCB)}
49        # Add rootserver thread explicitly
50        self.threads.add('rootserver')
51
52    def get_threads(self):
53        return self.threads
54
55
56class ExitUserspaceMode(IntEnum):
57    Never = 0
58    Once = 1
59    Always = 2
60
61
62def source(callable):
63    """Convenience decorator for sourcing gdb commands"""
64    callable()
65    return callable
66
67
68@source
69class seL4(gdb.Command):
70    """Utility functions for debugging seL4 applications"""
71    def __init__(self):
72        super(self.__class__, self).__init__('sel4', gdb.COMMAND_USER, prefix=True)
73
74
75@source
76class seL4Threads(gdb.Command):
77    """Lists all seL4 threads"""
78
79    def __init__(self):
80        super(self.__class__, self).__init__('sel4 threads', gdb.COMMAND_STATUS)
81
82    def invoke(self, arg, from_tty):
83        print('\n'.join(get_threads()))
84
85
86@source
87class seL4Thread(gdb.Command):
88    """Returns current seL4 thread"""
89
90    def __init__(self):
91        super(self.__class__, self).__init__('sel4 thread', gdb.COMMAND_STATUS)
92
93    def invoke(self, arg, from_tty):
94        print(get_current_thread())
95
96
97@source
98class seL4WaitForThread(gdb.Command):
99    """Continues until given thread is available to make operations on.
100
101       This command waits until seL4_DebugNameThread syscall is handled by the kernel,
102       which allows for the use of break and tbreak commands."""
103
104    def __init__(self):
105        super(self.__class__, self).__init__('sel4 wait-for-thread', gdb.COMMAND_BREAKPOINTS)
106
107    def complete(self, text, word):
108        global THREADS
109        return list(component for component in THREADS if component.startswith(text))
110
111    def invoke(self, arg, from_tty):
112        threads = get_threads()
113        thread_exists = next((thread for thread in threads if arg in thread), None)
114        if thread_exists is not None:
115            raise gdb.GdbError("'{}' thread is already loaded".format(thread_exists))
116
117        gdb.execute('mon seL4 BreakOnNamingThread "{}"'.format(arg))
118        gdb.execute('continue')
119
120
121@source
122class seL4SwitchSymbols(gdb.Command):
123    """Forcibly switches symbols to ones of the given component
124
125    sel4 switch-symbols [component]
126
127    Forcibly sets symbol-file to file corresponding to given component.
128    If no component name is given or thread is "default" then default
129    binary is loaded instead."""
130
131    def __init__(self):
132        super(self.__class__, self).__init__('sel4 switch-symbols', gdb.COMMAND_FILES)
133
134    def complete(self, text, word):
135        global BINARIES
136
137        # List all known components, add 'kernel' as an option for DEFAULT_BINARY
138        components = list(BINARIES.keys())
139        components.append('kernel')
140        return list(component for component in components if component.startswith(text))
141
142    def invoke(self, arg, from_tty):
143        if not arg:
144            thread = get_current_thread()
145            switch_symbols(thread, verbose=True)
146        elif arg == 'kernel':
147            switch_symbols(verbose=True)
148        else:
149            switch_symbols(arg, fallback=False, verbose=True)
150
151
152def _sel4_break_complete_helper(text, word):
153    words = text.split(' ')
154    if not text or len(words) <= 1:
155        threads = get_threads()
156        # Extend list of threads with additional special names
157        threads.extend(['user', 'kernel'])
158        return list(thread for thread in threads if thread.startswith(word))
159    elif len(words) == 2:
160        return gdb.COMPLETE_SYMBOL
161    else:
162        return gdb.COMPLETE_NONE
163
164
165def _sel4_break_invoke_helper(command, arg):
166    args = arg.split(' ')
167
168    if command == 'break':
169        exit_userspace_mode = ExitUserspaceMode.Always
170        monitor_command = 'mon seL4 SetBreakpoint'
171    elif command == 'tbreak':
172        exit_userspace_mode = ExitUserspaceMode.Once
173        monitor_command = 'mon seL4 SetTemporaryBreakpoint'
174    else:
175        raise ValueError("'{}' is invalid value for command".format(command))
176
177    if len(args) < 1 or not args[0]:
178        raise gdb.GdbError("sel4 {}: thread argument is required".format(command))
179
180    thread = args[0]
181    symbol_name = args[1] if len(args) >= 2 else None
182
183    if thread == 'kernel':
184        gdb.execute('mon seL4 BreakOnExittingUserspace {}'.format(exit_userspace_mode))
185        return
186
187    if thread == 'user':
188        thread = '<any>'
189
190    if symbol_name:
191        _, hits = gdb.decode_line(symbol_name)
192        for hit in hits:
193            gdb.execute('{} "{}" {}'.format(monitor_command, thread, hex(hit.pc)))
194    else:
195        gdb.execute('{} "{}"'.format(monitor_command, thread))
196
197
198@source
199class seL4Break(gdb.Command):
200    """Creates a breakpoint
201
202    sel4 break thread [address]
203
204    Creates a breakpoint in <thread> on optional <address>
205    If no address is given, the breakpoint will be set on
206    first address after context-switch"""
207
208    def __init__(self):
209        super(self.__class__, self).__init__('sel4 break', gdb.COMMAND_BREAKPOINTS)
210
211    def complete(self, text, word):
212        return _sel4_break_complete_helper(text, word)
213
214    def invoke(self, arg, from_tty):
215        _sel4_break_invoke_helper('break', arg)
216
217
218@source
219class seL4TBreak(gdb.Command):
220    """Creates temporary breakpoint
221
222    sel4 tbreak thread [address]
223
224    Creates temporary breakpoint in <thread> on optional <address>
225    If no address is given, the breakpoint will be set on
226    first address after context-switch"""
227
228    def __init__(self):
229        super(self.__class__, self).__init__('sel4 tbreak', gdb.COMMAND_BREAKPOINTS)
230
231    def complete(self, text, word):
232        return _sel4_break_complete_helper(text, word)
233
234    def invoke(self, arg, from_tty):
235        _sel4_break_invoke_helper('tbreak', arg)
236
237
238@source
239class seL4Delete(gdb.Command):
240    """Removes a breakpoint
241
242    sel4 delete thread [address]
243
244    Removes given breakpoint. If no address is given, the context-switch
245    breakpoint is removed"""
246
247    def __init__(self):
248        super(self.__class__, self).__init__('sel4 delete', gdb.COMMAND_BREAKPOINTS)
249
250    def complete(self, text, word):
251        words = text.split(' ')
252        if not text or len(words) <= 1:
253            threads = get_threads()
254            # Extend list of threads with additional special names
255            threads.extend(['user', 'kernel'])
256            return list(thread for thread in threads if thread.startswith(word))
257        elif len(words) == 2:
258            # Renode returns breakpoints as a table, so we have to parse it
259            # in order to gather completion list
260            chosen_thread = words[0]
261            if chosen_thread == 'user':
262                chosen_thread = '<any>'
263            completions = []
264            for thread, address in get_breakpoints(chosen_thread):
265                if chosen_thread not in thread:
266                    continue
267                if address == '<any>' or not address.startswith(word):
268                    continue
269                completions.append(address)
270            return completions
271        else:
272            return gdb.COMPLETE_NONE
273
274    def invoke(self, arg, from_tty):
275        args = arg.split(' ')
276
277        if len(args) < 1 or not args[0]:
278            raise gdb.GdbError("sel4 delete: thread argument is required")
279
280        thread = args[0] if len(args) >= 1 else None
281        address = args[1] if len(args) >= 2 else None
282
283        if thread == 'kernel':
284            gdb.execute('mon seL4 BreakOnExittingUserspace {}'.format(ExitUserspaceMode.Never))
285            return
286
287        if thread == 'user':
288            thread = '<any>'
289
290        if address:
291            gdb.execute('mon seL4 RemoveBreakpoint "{}" {}'.format(thread, address))
292            gdb.execute('mon seL4 RemoveTemporaryBreakpoint "{}" {}'.format(thread, address))
293        else:
294            gdb.execute('mon seL4 RemoveBreakpoint "{}"'.format(thread))
295            gdb.execute('mon seL4 RemoveTemporaryBreakpoint "{}"'.format(thread))
296
297
298@source
299class seL4DeleteAll(gdb.Command):
300    """Removes all breakpoints assigned to the thread
301
302    sel4 delete-all thread"""
303
304    def __init__(self):
305        super(self.__class__, self).__init__('sel4 delete-all', gdb.COMMAND_BREAKPOINTS)
306
307    def complete(self, text, word):
308        return list(thread for thread in get_threads() if thread.startswith(text))
309
310    def invoke(self, arg, from_tty):
311        gdb.execute('mon seL4 BreakOnExittingUserspace {}'.format(ExitUserspaceMode.Never))
312        if arg:
313            gdb.execute('mon seL4 RemoveAllBreakpoints "{}"'.format(arg))
314        else:
315            gdb.execute('mon seL4 RemoveAllBreakpoints')
316
317
318@source
319class seL4ListBreakpoints(gdb.Command):
320    """Lists all breakpoints
321
322    sel4 list-breakpoints [thread]
323    """
324
325    def __init__(self):
326        super(self.__class__, self).__init__('sel4 list-breakpoints', gdb.COMMAND_BREAKPOINTS)
327
328    def complete(self, text, word):
329        return list(thread for thread in get_threads() if thread.startswith(text))
330
331    def invoke(self, arg, from_tty):
332        if not arg:
333            gdb.execute('mon seL4 GetBreakpoints')
334        else:
335            gdb.execute('mon seL4 GetBreakpoints "{}"'.format(arg))
336
337
338@source
339class seL4Ready(gdb.Command):
340    """Returns ready state of seL4 extensions"""
341
342    def __init__(self):
343        super(self.__class__, self).__init__('sel4 ready', gdb.COMMAND_STATUS)
344
345    def invoke(self, arg, from_tty):
346        gdb.execute('mon seL4 Ready')
347
348
349@source
350class seL4SymbolAutoswitching(gdb.Command):
351    """Enables or disables symbol file autoswitching"""
352
353    def __init__(self):
354        super(self.__class__, self).__init__('sel4 symbol-autoswitching', gdb.COMMAND_USER)
355
356    def invoke(self, arg, from_tty):
357        global SYMBOL_AUTOSWITCHING
358
359        if not arg:
360            print('Symbol autoswitching is {}'.format('enabled' if SYMBOL_AUTOSWITCHING else 'disabled'))
361            return
362
363        if arg.isdigit():
364            arg = bool(int(arg))
365        elif arg in ['True', 'true']:
366            arg = True
367        elif arg in ['False', 'false']:
368            arg = False
369        else:
370            raise gdb.GdbError('{} is invalid argument for sel4 symbol-autoswitching'.format(arg))
371
372        SYMBOL_AUTOSWITCHING = arg
373        print('Symbol autoswitching is now {}'.format('enabled' if SYMBOL_AUTOSWITCHING else 'disabled'))
374
375
376@source
377def find_binaries():
378    global BINARIES, DEFAULT_BINARY
379    BINARIES = {}
380
381    build_dir = get_envvar('BUILD_DIR')
382    # Default binary is kernel, because every other component has its own thread,
383    # including rootserver.
384    DEFAULT_BINARY = os.path.join(build_dir, 'kernel', 'kernel.elf')
385
386    # Find all CAmkES components
387    images_path = os.path.join(build_dir, '*.instance.bin')
388    for image_path in glob(images_path):
389        image_name = os.path.basename(image_path).split('.instance.bin')[0]
390        BINARIES[image_name] = image_path
391
392    # rootserver thread is just capdl-loader
393    BINARIES['rootserver'] = os.path.join(build_dir, 'capdl-loader')
394
395
396@source
397def find_threads():
398    global THREADS
399
400    build_dir = get_envvar('BUILD_DIR')
401    cdl_pickle = os.path.join(build_dir, 'object.pickle')
402    provider = CapDLSource(cdl_pickle)
403    THREADS = provider.get_threads()
404
405
406def get_breakpoints(thread=None):
407    if not thread:
408        breakpoints = gdb.execute('mon seL4 GetBreakpointsPlain', to_string=True).strip()
409    else:
410        breakpoints = gdb.execute('mon seL4 GetBreakpointsPlain "{}"'.format(thread), to_string=True).strip()
411    return [tuple(line.strip().split(':')) for line in breakpoints.splitlines()]
412
413
414def get_current_thread():
415    return gdb.execute('mon seL4 CurrentThread', to_string=True).strip()
416
417
418def get_threads():
419    command_output = gdb.execute('mon seL4 Threads', to_string=True)
420    threads = []
421    for line in command_output.strip().split('\n')[1:-1]:
422        splitted_line = (thread.strip() for thread in line.split(','))
423        threads.extend(thread for thread in splitted_line if thread)
424    return threads
425
426
427def resolve_symbol_file(thread, fallback=True):
428    if thread is None:
429        image_path = DEFAULT_BINARY
430    else:
431        image_name = next((key for key in BINARIES.keys() if key in thread), None)
432        if image_name is not None:
433            image_path = BINARIES[image_name]
434        elif image_name is None and fallback:
435            image_path = DEFAULT_BINARY
436        else:
437            return None
438    return image_path
439
440
441def switch_symbols(thread=None, fallback=True, verbose=False):
442    """Switch symbol-file to the file corresponding to the given thread
443
444    If fallback is set to true and the given thread is not found, it will set
445    symbol-file to DEFAULT_BINARY (def. kernel.elf).
446    If verbose is set to true, symbol-file command will be run in interactive
447    mode and information of switching symbol file will be shown"""
448    global BINARIES, DEFAULT_BINARY
449
450    image_path = resolve_symbol_file(thread, fallback)
451
452    if image_path is None:
453        raise gdb.GdbError("no symbol-file found for thread/component {}".format(thread))
454
455    gdb.execute('symbol-file {}'.format(image_path), from_tty=verbose)
456
457
458def stop_handler(event):
459    if not isinstance(event, gdb.StopEvent):
460        return
461
462    global SYMBOL_AUTOSWITCHING
463
464    if SYMBOL_AUTOSWITCHING:
465        thread = get_current_thread()
466        switch_symbols(thread)
467
468gdb.events.stop.connect(stop_handler)
469