From 86e46d0f353c87a4fc4f3f834dcb04f8df0aae70 Mon Sep 17 00:00:00 2001
From: Petr Rockai <me@mornfall.net>
Date: Mon, 13 Jan 2020 22:29:25 +0000
Subject: [PATCH] dios: Make assertion of debug mode into a platform-dependent
hook.
---
dios/arch/divm/debug.c | 7 +++++++
dios/arch/klee/debug.c | 1 +
dios/libc/sys/trace.cpp | 2 +-
dios/sys/debug.hpp | 4 +++-
4 files changed, 12 insertions(+), 2 deletions(-)
create mode 100644 dios/arch/divm/debug.c
create mode 100644 dios/arch/klee/debug.c
diff --git a/dios/arch/divm/debug.c b/dios/arch/divm/debug.c
new file mode 100644
index 000000000..bed03db70
--- /dev/null
+++ b/dios/arch/divm/debug.c
@@ -0,0 +1,7 @@
+#include <sys/divm.h>
+#include <dios.h> /* __dios_assert */
+
+void __dios_assert_debug()
+{
+ __dios_assert( ( __vm_ctl_flag( 0, 0 ) & _VM_CF_DebugMode ) && __vm_ctl_get( _VM_CR_User3 ) );
+}
diff --git a/dios/arch/klee/debug.c b/dios/arch/klee/debug.c
new file mode 100644
index 000000000..008094422
--- /dev/null
+++ b/dios/arch/klee/debug.c
@@ -0,0 +1 @@
+void __dios_assert_debug() {}
diff --git a/dios/libc/sys/trace.cpp b/dios/libc/sys/trace.cpp
index ef9158e96..d53d54db8 100644
--- a/dios/libc/sys/trace.cpp
+++ b/dios/libc/sys/trace.cpp
@@ -89,7 +89,7 @@ __inline static void traceInternalV( int shift, const char *fmt, va_list ap ) no
void __dios_trace_internal( int indent, const char *fmt, ... ) noexcept
{
- __dios_assert( __dios::have_debug() );
+ __dios_assert_debug();
va_list ap;
va_start( ap, fmt );
__dios::traceInternalV( indent, fmt, ap );
diff --git a/dios/sys/debug.hpp b/dios/sys/debug.hpp
index 8aef0fbdc..2e9e9beb9 100644
--- a/dios/sys/debug.hpp
+++ b/dios/sys/debug.hpp
@@ -27,6 +27,8 @@
#define DIOS_DBG( ... ) __dios_trace_f( __VA_ARGS__ )
+extern "C" void __dios_assert_debug() noexcept;
+
/* Data that is not part of the execution of the system, but instead only
* serves to generate human-readable outputs during counterexample generation.
* None of this is instantiated during standard execution, since the code that
@@ -67,7 +69,7 @@ namespace __dios
__vm_trace( _VM_T_Text, "have_debug() failed in debug mode" );
__vm_ctl_set( _VM_CR_Flags, 0 ); /* fault & force abandonment of the debug call */
}
- __dios_assert( have_debug() );
+ __dios_assert_debug();
void *dbg = __vm_ctl_get( _VM_CR_User3 );
return *static_cast< Debug * >( dbg );
}
--
GitLab