Merge pull request #4333 from mokshasoft/seL4

Makefiles and changes needed for the C RTS on the seL4 microkernel

rts/idris_rts.c

@@ -114,7 +114,7 @@ void init_threaddata(VM *vm) {
 }
 
 void init_signals(void) {
-#if (__linux__ || __APPLE__ || __FreeBSD__ || __DragonFly__)
+#if defined(__linux__) || defined(__APPLE__) || defined(__FreeBSD__) || defined(__DragonFly__)
  signal(SIGPIPE, SIG_IGN);
 #endif
 }
@@ -1225,13 +1225,15 @@ void idris_disableBuffering(void) {
  setvbuf(stdout, NULL, _IONBF, 0);
 }
 
+#ifndef SEL4
 int idris_usleep(int usec) {
  struct timespec t;
  t.tv_sec = usec / 1000000;
  t.tv_nsec = (usec % 1000000) * 1000;
 
  return nanosleep(&t, NULL);
 }
+#endif // SEL4
 
 void stackOverflow(void) {
  fprintf(stderr, "Stack overflow");

rts/idris_rts.h

@@ -9,7 +9,7 @@
 #include <pthread.h>
 #endif
 #include <stdint.h>
-#if (__linux__ || __APPLE__ || __FreeBSD__ || __DragonFly__)
+#if defined(__linux__) || defined(__APPLE__) || defined(__FreeBSD__) || defined(__DragonFly__)
 #include <signal.h>
 #endif
 
@@ -245,7 +245,7 @@ typedef intptr_t i_int;
 #endif
 
 #define INITFRAME TRACE\
- VAL* myoldbase
+ __attribute__((unused)) VAL* myoldbase
 
 #define REBASE vm->valstack_base = oldbase
 #define RESERVE(x) if (vm->valstack_top+(x) > vm->stack_max) { stackOverflow(); } \
@@ -442,7 +442,9 @@ const char *idris_getArg(int i);
 // disable stdin/stdout buffering
 void idris_disableBuffering(void);
 
+#ifndef SEL4
 int idris_usleep(int usec);
+#endif // SEL4
 
 // Handle stack overflow.
 // Just reports an error and exits.

rts/seL4/Kbuild

@@ -0,0 +1,2 @@
+libsel4-idris-rts: $(libc) common
+libs-$(CONFIG_LIBSEL4_IDRIS_RTS) += libsel4-idris-rts

rts/seL4/Kconfig

@@ -0,0 +1,9 @@
+config LIBSEL4_IDRIS_RTS
+ bool "libsel4-idris-rts"
+ default y
+ select HAVE_LIBSEL4_IDRIS_RTS
+ help
+ Idris RTS compiled for seL4
+
+config HAVE_LIBSEL4_IDRIS_RTS
+ bool

rts/seL4/Makefile

@@ -0,0 +1,33 @@
+# Target
+TARGETS := libsel4-idris-rts.a
+
+# Source files required to build the target
+FILES := \
+ idris_rts.c \
+ idris_heap.c \
+ idris_gc.c \
+ idris_gmp.c \
+ idris_bitstring.c \
+ idris_opts.c \
+ idris_stats.c \
+ idris_utf8.c \
+ idris_stdfgn.c \
+ mini-gmp.c \
+ idris_buffer.c \
+ getline.c \
+ idris_net.c \
+ seL4/idris_main.c
+CFILES := $(addprefix rts/,$(FILES))
+
+# Header file directory this library provides
+HDRFILES := $(wildcard ${SOURCE_DIR}/rts/*)
+
+CFLAGS += -W -Wall
+# Don't use the host machines' environment when cross compiling
+CFLAGS += -undef
+CFLAGS += -DIDRIS_TARGET_OS=\"seL4\"
+CFLAGS += -DSEL4
+MACHINE := $(shell $(CC) -dumpmachine)
+CFLAGS += -DIDRIS_TARGET_TRIPLE=\"$(MACHINE)\"
+
+include $(SEL4_COMMON)/common.mk

rts/seL4/idris_main.c

@@ -0,0 +1,32 @@
+#include "idris_gmp.h"
+#include "idris_opts.h"
+#include "idris_rts.h"
+#include "idris_stats.h"
+
+void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase);
+
+RTSOpts opts = {
+ .init_heap_size = 16384000,
+ .max_stack_size = 4096000,
+ .show_summary = 0
+};
+
+int main() {
+ VM* vm = init_vm(opts.max_stack_size, opts.init_heap_size, 1);
+ init_gmpalloc();
+ init_nullaries();
+
+ _idris__123_runMain_95_0_125_(vm, NULL);
+
+#ifdef IDRIS_DEBUG
+ if (opts.show_summary) {
+ idris_gcInfo(vm, 1);
+ }
+#endif
+
+ free_nullaries();
+ // Remove call to terminate since it crashes the application during a free
+ //Stats stats = terminate(vm);
+
+ return EXIT_SUCCESS;
+}