From a84964ba4cd8e6ca4a9527041a8cfddae27a0c3c Mon Sep 17 00:00:00 2001
From: Hesham Almatary <Hesham.Almatary@nicta.com.au>
Date: Tue, 7 Jun 2016 09:19:31 +1000
Subject: [PATCH] SELFOUR-446 Benchmark: Share kernel entry types with
 user-level

---
 include/benchmark_track.h                    | 56 +++--------------
 include/benchmark_track_types.h              |  1 +
 libsel4/include/sel4/benchmark_track_types.h | 63 ++++++++++++++++++++
 3 files changed, 71 insertions(+), 49 deletions(-)
 create mode 120000 include/benchmark_track_types.h
 create mode 100644 libsel4/include/sel4/benchmark_track_types.h

diff --git a/include/benchmark_track.h b/include/benchmark_track.h
index cd683e54b..de4408d10 100644
--- a/include/benchmark_track.h
+++ b/include/benchmark_track.h
@@ -13,62 +13,15 @@
 
 #include <config.h>
 #include <arch/benchmark.h>
+#include <benchmark_track_types.h>
 #include <arch/api/constants.h>
 #include <machine/io.h>
 
-#if (defined CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || defined DEBUG)
-
 /* we can fill the entire IPC buffer except for word 0, which
  * the kernel overwrites with the message tag */
 #define MAX_IPC_BUFFER_STORAGE_SIZE (sizeof(seL4_IPCBuffer) - sizeof(seL4_Word))
 
-/* the following code can be used at any point in the kernel
- * to determine detail about the kernel entry point */
-typedef enum {
-    Entry_Interrupt,
-    Entry_UnknownSyscall,
-    Entry_UserLevelFault,
-    Entry_VMFault,
-    Entry_Syscall
-} entry_type_t;
-
-/**
- * @brief Kernel entry logging
- *
- * Encapsulates useful info about the cause of the kernel entry
- */
-typedef struct PACKED kernel_entry {
-    word_t path: 3;
-    union {
-        struct {
-            word_t word: 29;
-        };
-        /* Tracked kernel entry info filled from outside this file */
-        struct {
-            word_t syscall_no: 3;
-            word_t cap_type: 5;
-            word_t is_fastpath: 1;
-            word_t invocation_tag: 20;
-        };
-    };
-} kernel_entry_t;
-
-extern kernel_entry_t ksKernelEntry;
-#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || DEBUG */
-
 #ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
-
-typedef struct benchmark_syscall_log_entry {
-    timestamp_t  start_time;
-    uint32_t  duration;
-    kernel_entry_t entry;
-} benchmark_track_kernel_entry_t;
-
-extern timestamp_t ksEnter;
-extern benchmark_track_kernel_entry_t *ksLog;
-extern word_t ksLogIndex;
-extern uint32_t ksLogIndexFinalized;
-
 /**
  *  Calculate the maximum number of kernel entries that can be tracked,
  *  limited by the log buffer size. This is also the number of ksLog entries.
@@ -82,6 +35,12 @@ extern uint32_t ksLogIndexFinalized;
  */
 #define MAX_IPC_BUFFER_STORAGE (MAX_IPC_BUFFER_STORAGE_SIZE / sizeof(benchmark_track_kernel_entry_t))
 
+extern timestamp_t ksEnter;
+extern benchmark_track_kernel_entry_t *ksLog;
+extern word_t ksLogIndex;
+extern uint32_t ksLogIndexFinalized;
+extern kernel_entry_t ksKernelEntry;
+
 /**
  * @brief Fill in logging info for kernel entries
  *
@@ -113,5 +72,4 @@ benchmark_track_start(void)
 }
 
 #endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES */
-
 #endif /* BENCHMARK_TRACK_H */
diff --git a/include/benchmark_track_types.h b/include/benchmark_track_types.h
new file mode 120000
index 000000000..d4e9c6dd4
--- /dev/null
+++ b/include/benchmark_track_types.h
@@ -0,0 +1 @@
+../libsel4/include/sel4/benchmark_track_types.h
\ No newline at end of file
diff --git a/libsel4/include/sel4/benchmark_track_types.h b/libsel4/include/sel4/benchmark_track_types.h
new file mode 100644
index 000000000..ffbb6dea1
--- /dev/null
+++ b/libsel4/include/sel4/benchmark_track_types.h
@@ -0,0 +1,63 @@
+/*
+ * Copyright 2016, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ */
+
+#ifndef BENCHMARK_TRACK_TYPES_H
+#define BENCHMARK_TRACK_TYPES_H
+
+#ifdef HAVE_AUTOCONF
+#include <autoconf.h>
+#endif
+
+#if (defined CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || defined DEBUG)
+
+/* the following code can be used at any point in the kernel
+ * to determine detail about the kernel entry point */
+typedef enum {
+    Entry_Interrupt,
+    Entry_UnknownSyscall,
+    Entry_UserLevelFault,
+    Entry_VMFault,
+    Entry_Syscall
+} entry_type_t;
+
+/**
+ * @brief Kernel entry logging
+ *
+ * Encapsulates useful info about the cause of the kernel entry
+ */
+typedef struct PACKED kernel_entry {
+    seL4_Word path: 3;
+    union {
+        struct {
+            seL4_Word word: 29;
+        };
+        /* Tracked kernel entry info filled from outside this file */
+        struct {
+            seL4_Word syscall_no: 3;
+            seL4_Word cap_type: 5;
+            seL4_Word is_fastpath: 1;
+            seL4_Word invocation_tag: 20;
+        };
+    };
+} kernel_entry_t;
+
+#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES || DEBUG */
+
+#ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
+
+typedef struct benchmark_syscall_log_entry {
+    uint64_t  start_time;
+    uint32_t  duration;
+    kernel_entry_t entry;
+} benchmark_track_kernel_entry_t;
+
+#endif /* CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES */
+
+#endif /* BENCHMARK_TRACK_TYPES_H */