1/*
2 * Copyright 2017, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13#pragma once
14
15#include <sel4/config.h>
16#include <sel4/types.h>
17#include <sel4/arch/constants.h>
18#include <sel4/simple_types.h>
19#include <sel4/benchmark_tracepoints_types.h>
20#include <sel4/arch/syscalls.h>
21#include <inttypes.h>
22
23#if CONFIG_MAX_NUM_TRACE_POINTS > 0
24#define KERNEL_MAX_NUM_LOG_ENTRIES (BIT(seL4_LargePageBits) / sizeof(benchmark_tracepoint_log_entry_t))
25typedef benchmark_tracepoint_log_entry_t  kernel_log_entry_t;
26#else
27#define KERNEL_MAX_NUM_LOG_ENTRIES 0
28typedef void *kernel_log_entry_t;
29#endif
30
31/* Copies up to n entries from the kernel's internal log to the specified array,
32 * returning the number of entries copied.
33 */
34unsigned int kernel_logging_sync_log(kernel_log_entry_t log[], unsigned int n);
35
36/* Returns the key field of a log entry. */
37static inline seL4_Word kernel_logging_entry_get_key(kernel_log_entry_t *entry)
38{
39#if CONFIG_MAX_NUM_TRACE_POINTS > 0
40    return entry->id;
41#else
42    return 0;
43#endif
44}
45
46/* Sets the key field of a log entry to a given value. */
47static inline void kernel_logging_entry_set_key(kernel_log_entry_t *entry, seL4_Word key)
48{
49#if CONFIG_MAX_NUM_TRACE_POINTS > 0
50    entry->id = key;
51#endif
52}
53
54/* Returns the data field of a log entry. */
55static inline seL4_Word kernel_logging_entry_get_data(kernel_log_entry_t *entry)
56{
57#if CONFIG_MAX_NUM_TRACE_POINTS > 0
58    return entry->duration;
59#else
60    return 0;
61#endif
62}
63
64/* Sets the data field of a log entry to a given value. */
65static inline void kernel_logging_entry_set_data(kernel_log_entry_t *entry, seL4_Word data)
66{
67#if CONFIG_MAX_NUM_TRACE_POINTS > 0
68    entry->duration = data;
69#endif
70}
71
72/* Resets the log buffer to contain no entries. */
73static inline void kernel_logging_reset_log(void)
74{
75#ifdef CONFIG_ENABLE_BENCHMARKS
76    seL4_BenchmarkResetLog();
77#endif /* CONFIG_ENABLE_BENCHMARKS */
78}
79
80/* Calls to kernel_logging_sync_log will extract entries created before
81 * the most-recent call to this function. Call this function before calling
82 * kernel_logging_sync_log. */
83static inline void kernel_logging_finalize_log(void)
84{
85#ifdef CONFIG_ENABLE_BENCHMARKS
86    seL4_BenchmarkFinalizeLog();
87#endif /* CONFIG_ENABLE_BENCHMARKS */
88}
89
90/* Tell the kernel about the allocated user-level buffer
91 * so that it can write to it. Note, this function has to
92 * be called before kernel_logging_reset_log.
93 *
94 * @logBuffer_cap should be a cap of a large frame size.
95 */
96static inline seL4_Error kernel_logging_set_log_buffer(seL4_CPtr logBuffer_cap)
97{
98#ifdef CONFIG_KERNEL_LOG_BUFFER
99    return seL4_BenchmarkSetLogBuffer(logBuffer_cap);
100#else
101    return seL4_NoError;
102#endif /* CONFIG_KERNEL_LOG_BUFFER */
103}
104