diff --git a/config.mk b/config.mk index a474ff0ba1..4cc0b38d47 100644 --- a/config.mk +++ b/config.mk @@ -14,7 +14,7 @@ RANLIB ?=ranlib CABAL :=cabal # IDRIS_ENABLE_STATS should not be set in final release # Any flags defined here which alter the RTS API must also be added to src/IRTS/CodegenC.hs -CFLAGS :=-O2 -Wall -std=c99 -pipe -fdata-sections -ffunction-sections -D_POSIX_C_SOURCE=200809L -DHAS_PTHREAD -DIDRIS_ENABLE_STATS $(CFLAGS) +CFLAGS :=-O2 -Wall -std=c99 -pipe -fdata-sections -ffunction-sections -D_POSIX_C_SOURCE=200809L -DIS_THREADED -DHAS_PTHREAD -DIDRIS_ENABLE_STATS $(CFLAGS) # CABALFLAGS := CABALFLAGS += --enable-tests diff --git a/rts/FreeRTOS/README.md b/rts/FreeRTOS/README.md new file mode 100644 index 0000000000..d9f9a85990 --- /dev/null +++ b/rts/FreeRTOS/README.md @@ -0,0 +1,11 @@ +# Idris RTS on FreeRTOS +The Idris RTS compiled without libc ontop of FreeRTOS tasks, using FreeRTOS queues as IPC. This +enables using Idris when programming microcontrollers and smaller systems, but it is also a step +towards the goal of building an Idris Unikernel. + +FreeRTOS was chosen as abstraction layer towards the hardware since it's easy to port to new +architectures, since it's small, and since there already are a lot of port available. + +## How to run Idris on FreeRTOS +See the instructions in the repository, +[mokshasoft/FreeRTOS-community-ports](https://github.com/mokshasoft/FreeRTOS-community-ports/tree/master/Demo/ARM926ejs-GCC-Idris). diff --git a/rts/FreeRTOS/idris_FreeRTOS.c b/rts/FreeRTOS/idris_FreeRTOS.c new file mode 100644 index 0000000000..0e3da6f70e --- /dev/null +++ b/rts/FreeRTOS/idris_FreeRTOS.c @@ -0,0 +1,41 @@ +/* + * Copyright 2020, Mokshasoft AB (mokshasoft.com) + * + * Redistribution and use in source and binary forms, with or without modification, are permitted + * provided that the following conditions are met: + * + * 1. Redistributions of source code must retain the above copyright notice, this list of + * conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright notice, this list of + * conditions and the following disclaimer in the documentation and/or other materials provided + * with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR + * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND + * FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR + * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR + * OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + */ + +#include "idris_FreeRTOS.h" +#include "idris_rts.h" + +void wrapper_vTaskDelay(int delay_ms) +{ + vTaskDelay(delay_ms/portTICK_RATE_MS); +} + +QueueHandle_t wrapper_xQueueCreate(UBaseType_t uxQueueLength) +{ + return xQueueCreate(uxQueueLength, sizeof(void*)); +} + +void wrapper_vQueueDelete(QueueHandle_t xQueue) +{ + vQueueDelete(xQueue); +} diff --git a/rts/FreeRTOS/idris_FreeRTOS.h b/rts/FreeRTOS/idris_FreeRTOS.h new file mode 100644 index 0000000000..e72daa1b77 --- /dev/null +++ b/rts/FreeRTOS/idris_FreeRTOS.h @@ -0,0 +1,37 @@ +/* + * Copyright 2020, Mokshasoft AB (mokshasoft.com) + * + * Redistribution and use in source and binary forms, with or without modification, are permitted + * provided that the following conditions are met: + * + * 1. Redistributions of source code must retain the above copyright notice, this list of + * conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright notice, this list of + * conditions and the following disclaimer in the documentation and/or other materials provided + * with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR + * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND + * FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR + * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR + * OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + */ + +#include +#include + +/* + * Wrappers for FreeRTOS Task Control + */ +void wrapper_vTaskDelay(int delay_ms); + +/* + * Wrappers for FreeRTOS Queue + */ +QueueHandle_t wrapper_xQueueCreate(UBaseType_t uxQueueLength); +void wrapper_vQueueDelete(QueueHandle_t xQueue); diff --git a/rts/FreeRTOS/idris_main.c b/rts/FreeRTOS/idris_main.c new file mode 100644 index 0000000000..5e66999cf9 --- /dev/null +++ b/rts/FreeRTOS/idris_main.c @@ -0,0 +1,79 @@ +/* + * Copyright 2020, Mokshasoft AB (mokshasoft.com) + * + * Redistribution and use in source and binary forms, with or without modification, are permitted + * provided that the following conditions are met: + * + * 1. Redistributions of source code must retain the above copyright notice, this list of + * conditions and the following disclaimer. + * + * 2. Redistributions in binary form must reproduce the above copyright notice, this list of + * conditions and the following disclaimer in the documentation and/or other materials provided + * with the distribution. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR + * IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND + * FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR + * CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR + * SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY + * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR + * OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + */ + +/* The UART part of this code depends on the print driver of the versatilepb, remove or port + * this part of the code if compiling for another platform. + */ + +#include "idris_gmp.h" +#include "idris_opts.h" +#include "idris_rts.h" +#include "idris_stats.h" +#include "print.h" +#include +#include + +void _idris__123_runMain_95_0_125_(VM* vm, VAL* oldbase); + +RTSOpts opts = { + .init_heap_size = 10000, + .max_stack_size = 5000, + .show_summary = 0 +}; + +static void uartLog(const char* msg) { + vDirectPrintMsg(msg); +} + +static void halt() { + for (; ;); +} + +void vRootThread(void* pvParameters) { + 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); +} + +int main() { + // Init print + if (pdFAIL == printInit(0)) { + uartLog("Init print failed\r\n"); + halt(); + } + + // Create root thread + if (pdPASS != xTaskCreate(vRootThread, "root", 2000, NULL, 0, NULL)) { + uartLog("Failed to create root thread\r\n"); + halt(); + } + + // Start the FreeRTOS scheduler + vTaskStartScheduler(); + + // Will not get here unless there is insufficient RAM + uartLog("will not get here\r\n"); + return EXIT_SUCCESS; +} diff --git a/rts/Makefile b/rts/Makefile index 122677c8b3..791c93efc9 100644 --- a/rts/Makefile +++ b/rts/Makefile @@ -2,10 +2,10 @@ include ../config.mk OBJS = idris_rts.o idris_heap.o idris_gc.o idris_gmp.o idris_bitstring.o \ idris_opts.o idris_stats.o idris_utf8.o idris_stdfgn.o \ - idris_buffer.o getline.o idris_net.o + idris_buffer.o getline.o idris_net.o itoa.o HDRS = idris_rts.h idris_heap.h idris_gc.h idris_gmp.h idris_bitstring.h \ idris_opts.h idris_stats.h idris_stdfgn.h idris_net.h \ - idris_buffer.h idris_utf8.h getline.h + idris_buffer.h idris_utf8.h getline.h itoa.h CFLAGS := $(CFLAGS) CFLAGS += $(GMP_INCLUDE_DIR) $(GMP) -DIDRIS_TARGET_OS="\"$(OS)\"" CFLAGS += -DIDRIS_TARGET_TRIPLE="\"$(MACHINE)\"" @@ -16,6 +16,13 @@ else CFLAGS += -fPIC endif +ifdef BARE_METAL + # Using this flag changes the precision of float casts compared to snprintf. + # e.g. 2345.345 get converted to "2345.344970703125" instead of "234.345" + OBJS += ftoa.o + HDRS += ftoa.h +endif + ifndef IDRIS_GMP OBJS += mini-gmp.o HDRS += mini-gmp.h diff --git a/rts/bare-metal/CMakeLists.txt b/rts/bare-metal/CMakeLists.txt new file mode 100644 index 0000000000..963c0725d4 --- /dev/null +++ b/rts/bare-metal/CMakeLists.txt @@ -0,0 +1,41 @@ +cmake_minimum_required(VERSION 3.7.2) + +project(idris-rts-bare-metal C) + +file(GLOB static + rts/idris_rts.c + rts/idris_heap.c + rts/idris_gc.c + rts/idris_gmp.c + rts/idris_bitstring.c + rts/idris_utf8.c + rts/mini-gmp.c + rts/itoa.c + rts/ftoa.c + rts/bare-metal/idris_main.c +) + +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -W -Wall") +# Ignore some warnings +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-parameter") +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-sign-compare") +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-variable") +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-empty-body") +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-maybe-uninitialized") +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wno-unused-but-set-variable") +# Don't use the host machines' environment when cross compiling +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -DIDRIS_TARGET_OS=\"\\\"bare-metal\\\"\"") +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -DBARE_METAL") +execute_process( + COMMAND ${CMAKE_C_COMPILER} -dumpmachine + OUTPUT_VARIABLE MACHINE + OUTPUT_STRIP_TRAILING_WHITESPACE +) +set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -DIDRIS_TARGET_TRIPLE=\"\\\"${MACHINE}\\\"\"") + +add_library(idris-rts-bare-metal EXCLUDE_FROM_ALL ${static}) +target_include_directories(idris-rts-bare-metal PUBLIC rts) +target_link_libraries( + idris-rts-bare-metal + c +) diff --git a/rts/bare-metal/README.md b/rts/bare-metal/README.md new file mode 100644 index 0000000000..62fbcdde3e --- /dev/null +++ b/rts/bare-metal/README.md @@ -0,0 +1,5 @@ +# idris-rts-bare-metal - Idris RTS bare-metal library +The Idris RTS compiled without libc to allow executing Idris apps on bare-metal. + +## How to use this library? +See the instructions in the project repository, [mokshasoft/bare-metal-idris-manifest](https://github.com/mokshasoft/bare-metal-idris-manifest). diff --git a/rts/bare-metal/idris_main.c b/rts/bare-metal/idris_main.c new file mode 100644 index 0000000000..778bfac53e --- /dev/null +++ b/rts/bare-metal/idris_main.c @@ -0,0 +1,31 @@ +#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 = 10000, + .max_stack_size = 5000, + .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 + + // Remove call to terminate since it crashes the application during a free + //Stats stats = terminate(vm); + + return EXIT_SUCCESS; +} diff --git a/rts/ftoa.c b/rts/ftoa.c new file mode 100644 index 0000000000..f0b22d0cb1 --- /dev/null +++ b/rts/ftoa.c @@ -0,0 +1,217 @@ +/*** ftoa.c -- fast float to text converters + * + * Copyright (C) 2010-2017 Ruediger Meier + * Author: Ruediger Meier + * License: BSD 3-Clause, see LICENSE file + * + ***/ + +#include "ftoa.h" +#include "itoa.h" +#include +#include +#include + +typedef union { + int L; + float F; +} LF_t; + + +int ftoa( char *outbuf, float f ) +{ + uint64_t mantissa, int_part, frac_part; + int safe_shift; + uint64_t safe_mask; + short exp2; + LF_t x; + char *p; + + x.F = f; + p = outbuf; + + exp2 = (unsigned char)(x.L >> 23) - 127; + mantissa = (x.L & 0xFFFFFF) | 0x800000; + frac_part = 0; + int_part = 0; + + if( x.L < 0 ) { + *p++ = '-'; + } + + /* Our algorithm works only on exponents >= -36 because safe_mask must + start with at least 4 zero bits. So we quickly print 0.0 here. (We could + do this even for bigger exponents dependently on PRECISION but would be + a useless optimization.) BTW the case f == 0.0 is also handled here. */ + if ( exp2 < -36 ) { +#if defined NO_TRAIL_NULL + *p++ = '0'; +#else + // print 0.000... like "%._f" does + memset( p, '0', PRECISION + 1 + 1); + p[1] = '.'; + p += PRECISION + 1 + 1; +#endif + goto END; + } + + safe_shift = -(exp2 + 1); + safe_mask = 0xFFFFFFFFFFFFFFFFULL >>(64 - 24 - safe_shift); + + if (exp2 >= 64) { + /* |f| >= 2^64 > ULONG_MAX */ + /* NaNs and +-INF are also handled here*/ + int_part = ULONG_MAX; + } else if (exp2 >= 23) { + int_part = mantissa << (exp2 - 23); + } else if (exp2 >= 0) { + int_part = mantissa >> (23 - exp2); + frac_part = (mantissa) & safe_mask; + } else /* if (exp2 < 0) */ { + frac_part = (mantissa & 0xFFFFFF); + } + + if (int_part == 0) { + *p++ = '0'; + } else { + p += itoa_uint64(p, int_part); + } + + if (frac_part != 0) { + *p++ = '.'; + + /* print BCD, calculating digits of frac_part (one more digit is needed + when rounding, less digits are needed when then precision should be + significant*/ + char max = PRECISION; +#ifdef PRECISION_IS_SIGNIFICANT + int cnt_dig = ((p - outbuf) + (x.L < 0 ? 1 : 0) - 1); + max -= (cnt_dig < max) ? cnt_dig : 0; +#endif +#if defined DO_ROUNDING + max++; +#endif + for (char m = 0; m < max; m++) { + /* frac_part *= 10; */ + frac_part = (frac_part << 3) + (frac_part << 1); + + *p++ = (frac_part >> (24 + safe_shift)) + '0'; + frac_part &= safe_mask; + } +#if defined DO_ROUNDING + + int round_int = 0; + p--; + + if( *p >= '5' ) { + char *w = p-1; + if( *w != '.' ) { + if( frac_part != 0 || (*w & 1) ) { + // round up + while( *w == '9' ) { + *w-- = '0'; + } + if( *w != '.' ) { + *w += 1; + } else { + round_int = 1; + } + } + } else { + if( frac_part != 0 || ( (int_part & 1)) ) { + round_int = 1; + } + } + + if( round_int ) { + // we have to round up int_part too + w--; + while( *w == '9' && w >= outbuf && *w != '-' ) { + *w-- = '0'; + } + if( w >= outbuf && *w != '-' ) { + *w += 1; + } else { + // int_part has one digit more now + w++; + p++; + memmove( w+1, w, p-w ); + *w = '1'; + } + } + } +#endif +#if defined NO_TRAIL_NULL + for (; p[-1] == '0'; --p) { + } + if( p[-1] == '.' ) { + p--; + } +#else + } else { + // print _.000... like "%._f" does + *p++ = '.'; + memset( p, '0', PRECISION ); + p += PRECISION; +#endif + } /* if (frac_part != 0) */ + +END: + *p = 0; + return p - outbuf; +} + +#undef PRECISION + + + + +/** + * ftoa_prec_f0: printing floats as rounded integer + * works exactly like sprintf "%.0f" for |f| < 2^64, + * +-ULONG_MAX is printed when |f| >= 2^64 or +-inf or nan, + * round to even like IEEE 754-1985 4.1 says, + * about 20 times faster than sprintf ( exponent range 2^-1, 2^20 ) + */ +int ftoa_prec_f0( char *outbuf, float f ) +{ + char *p = outbuf; + LF_t x; + x.F = f; + + short exp2 = (unsigned char)(x.L >> 23) - 127; + + if( x.L < 0 ) { + *p++ = '-'; + } + + if( exp2 < -1 ) { + /* |f| <= 0.5 */ + *p++ = '0'; + } else { + uint64_t int_part; + uint64_t mantissa = (x.L & 0xFFFFFF) | 0x800000; + if (exp2 >= 64) { + /* |f| >= 2^64 > ULONG_MAX */ + /* NaNs and +-INF are also handled here*/ + int_part = ULONG_MAX; + } else if (exp2 >= 23) { + int_part = mantissa << (exp2 - 23); + /* frac_part is 0 */ + } else { + unsigned int frac_part; + int_part = mantissa >> (23 - exp2); + frac_part = (mantissa << (exp2 + 1)) & 0xFFFFFF; + if( frac_part >= 0x800000 ) { + /* ieee - *.5 round to even */ + if( frac_part != 0x800000 || ( int_part & 1 ) ) { + int_part++; + } + } + } + + p += itoa_uint64(p, int_part); + } + *p = 0; + return p - outbuf; +} diff --git a/rts/ftoa.h b/rts/ftoa.h new file mode 100644 index 0000000000..4bfdcda344 --- /dev/null +++ b/rts/ftoa.h @@ -0,0 +1,5 @@ +#define PRECISION 16 +#define DO_ROUNDING + +int ftoa(char *outbuf, float f); +int ftoa_prec_f0(char *outbuf, float f); diff --git a/rts/idris_bare_metal.h b/rts/idris_bare_metal.h new file mode 100644 index 0000000000..1da81cdf3f --- /dev/null +++ b/rts/idris_bare_metal.h @@ -0,0 +1,15 @@ +#ifndef _IDRIS_BARE_METAL_H +#define _IDRIS_BARE_METAL_H + +#undef assert +#define assert(...) +#define printf(...) +#define fprintf(...) + +#define puts(...) +#define fflush(...) + +#define abort(...) +#define exit(...) + +#endif diff --git a/rts/idris_gc.c b/rts/idris_gc.c index 3f5a5f13ee..755e170e82 100644 --- a/rts/idris_gc.c +++ b/rts/idris_gc.c @@ -2,7 +2,11 @@ #include "idris_rts.h" #include "idris_gc.h" #include "idris_bitstring.h" +#ifndef BARE_METAL #include +#else +#include "idris_bare_metal.h" +#endif static inline VAL copy_plain(VM* vm, VAL x, size_t sz) { VAL cl = iallocate(vm, sz, 1); diff --git a/rts/idris_heap.c b/rts/idris_heap.c index 1ab12a5d8b..06c9d68ff1 100644 --- a/rts/idris_heap.c +++ b/rts/idris_heap.c @@ -4,8 +4,12 @@ #include #include +#ifndef BARE_METAL #include #include +#else +#include "idris_bare_metal.h" +#endif static void c_heap_free_item(CHeap * heap, CHeapItem * item) { diff --git a/rts/idris_rts.c b/rts/idris_rts.c index 9b739ddf7a..e78438c96d 100644 --- a/rts/idris_rts.c +++ b/rts/idris_rts.c @@ -1,11 +1,18 @@ +#ifdef BARE_METAL +#include "idris_bare_metal.h" +#include "ftoa.h" +#else #include +#include // snprintf +#include "getline.h" +#endif // BARE_METAL #include +#include "itoa.h" #include "idris_rts.h" #include "idris_gc.h" #include "idris_utf8.h" #include "idris_bitstring.h" -#include "getline.h" #define STATIC_ASSERT(COND,MSG) typedef char static_assertion_##MSG[(COND)?1:-1] @@ -69,14 +76,18 @@ VM* init_vm(int stack_size, size_t heap_size, pthread_mutex_init(&(vm->inbox_block), NULL); pthread_mutex_init(&(vm->alloc_lock), &rec_attr); pthread_cond_init(&(vm->inbox_waiting), NULL); +#elif defined(HAS_FREERTOS) + vm->xTaskHandle = NULL; +#else + global_vm = vm; +#endif +#ifdef IS_THREADED vm->max_threads = max_threads; vm->processes = 0; vm->creator = NULL; +#endif // IS_THREADED -#else - global_vm = vm; -#endif STATS_LEAVE_INIT(vm->stats) return vm; } @@ -95,6 +106,8 @@ VM* idris_vm(void) { VM* get_vm(void) { #ifdef HAS_PTHREAD return pthread_getspecific(vm_key); +#elif defined(HAS_FREERTOS) + return pvTaskGetThreadLocalStoragePointer(NULL, 0); #else return global_vm; #endif @@ -120,6 +133,8 @@ void init_threadkeys(void) { void init_threaddata(VM *vm) { #ifdef HAS_PTHREAD pthread_setspecific(vm_key, vm); +#elif defined(HAS_FREERTOS) + vTaskSetThreadLocalStoragePointer(NULL, 0, vm); #endif } @@ -144,6 +159,9 @@ Stats terminate(VM* vm) { if (vm->creator != NULL) { vm->creator->processes--; } +#endif +#ifdef HAS_FREERTOS + free(vm); #endif // free(vm); // Set the VM as inactive, so that if any message gets sent to it @@ -509,7 +527,8 @@ void idris_memmove(void* dest, void* src, i_int dest_offset, i_int src_offset, i VAL idris_castIntStr(VM* vm, VAL i) { int x = (int) GETINT(i); String * cl = allocStr(vm, 16, 0); - cl->slen = sprintf(cl->str, "%d", x); + cl->slen = itoa_int64(cl->str, x); + cl->str[cl->slen] = '\0'; return (VAL)cl; } @@ -521,17 +540,20 @@ VAL idris_castBitsStr(VM* vm, VAL i) { case CT_INT: // 8/16 bits // max length 16 bit unsigned int str 5 chars (65,535) cl = allocStr(vm, 6, 0); - cl->slen = sprintf(cl->str, "%" PRIu16, (uint16_t)GETBITS16(i)); + cl->slen = itoa_int32(cl->str, (uint16_t)GETBITS16(i)); + cl->str[cl->slen] = '\0'; break; case CT_BITS32: // max length 32 bit unsigned int str 10 chars (4,294,967,295) cl = allocStr(vm, 11, 0); - cl->slen = sprintf(cl->str, "%" PRIu32, GETBITS32(i)); + cl->slen = itoa_int32(cl->str, GETBITS32(i)); + cl->str[cl->slen] = '\0'; break; case CT_BITS64: // max length 64 bit unsigned int str 20 chars (18,446,744,073,709,551,615) cl = allocStr(vm, 21, 0); - cl->slen = sprintf(cl->str, "%" PRIu64, GETBITS64(i)); + cl->slen = itoa_int64(cl->str, GETBITS64(i)); + cl->str[cl->slen] = '\0'; break; default: fprintf(stderr, "Fatal Error: ClosureType %d, not an integer type", ty); @@ -551,7 +573,12 @@ VAL idris_castStrInt(VM* vm, VAL i) { VAL idris_castFloatStr(VM* vm, VAL i) { String * cl = allocStr(vm, 32, 0); +#ifdef BARE_METAL + cl->slen = ftoa(cl->str, GETFLOAT(i)); + cl->str[cl->slen] = '\0'; +#else cl->slen = snprintf(cl->str, 32, "%.16g", GETFLOAT(i)); +#endif return (VAL)cl; } @@ -589,6 +616,7 @@ VAL idris_strlen(VM* vm, VAL l) { return MKINT((i_int)(idris_utf8_strlen(GETSTR(l)))); } +#ifndef BARE_METAL VAL idris_readStr(VM* vm, FILE* h) { VAL ret; char *buffer = NULL; @@ -619,6 +647,7 @@ VAL idris_readChars(VM* vm, int num, FILE* h) { free(buffer); return ret; } +#endif // BARE_METAL void idris_crash(char* msg) { fprintf(stderr, "%s\n", msg); @@ -791,13 +820,14 @@ VAL idris_systemInfo(VM* vm, VAL index) { return MKSTR(vm, ""); } -#ifdef HAS_PTHREAD +#ifdef IS_THREADED typedef struct { VM* vm; // thread's VM func fn; VAL arg; } ThreadData; +#ifdef HAS_PTHREAD void* runThread(void* arg) { ThreadData* td = (ThreadData*)arg; VM* vm = td->vm; @@ -848,9 +878,59 @@ void* vmThread(VM* callvm, func f, VAL arg) { } } -void* idris_stopThread(VM* vm) { +#elif defined(HAS_FREERTOS) +void runThread(void* arg) { + ThreadData* td = (ThreadData*)arg; + VM* vm = td->vm; + func fn = td->fn; + + init_threaddata(vm); + + TOP(0) = td->arg; + BASETOP(0); + ADDTOP(1); + free(td); + fn(vm, NULL); + + // Stats stats = terminate(vm); + // aggregate_stats(&(td->vm->stats), &stats); +} + +void* vmThread(VM* callvm, func f, VAL arg) { + VM* vm = init_vm( + callvm->stack_max - callvm->valstack, + callvm->heap.size, + callvm->max_threads); + vm->processes=1; // since it can send and receive messages + vm->creator = callvm; + + ThreadData *td = malloc(sizeof(ThreadData)); // free'd in runThread + td->vm = vm; + td->fn = f; + td->arg = copyTo(vm, arg); + + callvm->processes++; + + TaskHandle_t pxCreatedTask; + int ok = xTaskCreate(runThread, "non-root", 2000, td, 0, &pxCreatedTask); + if (ok == pdPASS) { + vm->xTaskHandle = pxCreatedTask; + return vm; + } else { + terminate(vm); + return NULL; + } +} +#endif + +void* idris_stopThread(VM* vm) { +#ifdef HAS_PTHREAD pthread_exit(NULL); +#elif defined(HAS_FREERTOS) + vTaskDelete(vm->xTaskHandle); +#endif + terminate(vm); return NULL; } @@ -919,7 +999,9 @@ VAL copyTo(VM* vm, VAL x) { VAL ret = doCopyTo(vm, x); return ret; } +#endif // IS_THREADED +#ifdef HAS_PTHREAD // Add a message to another VM's message queue int idris_sendMessage(VM* sender, int channel_id, VM* dest, VAL msg) { // FIXME: If GC kicks in in the middle of the copy, we're in trouble. @@ -1104,7 +1186,6 @@ Msg* idris_recvMessageFrom(VM* vm, int channel_id, VM* sender) { } return ret; } -#endif VAL idris_getMsg(Msg* msg) { return msg->msg; @@ -1121,6 +1202,23 @@ int idris_getChannel(Msg* msg) { void idris_freeMsg(Msg* msg) { free(msg); } +#endif // HAS_PTHREAD + +#ifdef HAS_FREERTOS +void idris_queuePut(QueueHandle_t xQueue, VAL msg) { + BaseType_t dummy = xQueueSend(xQueue, (void*)&msg, portMAX_DELAY); +} + +VAL idris_queueGet(VM* vm, QueueHandle_t xQueue) { + VAL msg = NULL; + BaseType_t dummy = xQueueReceive(xQueue, (void*)&msg, portMAX_DELAY); + return doCopyTo(vm, msg); +} +#endif // HAS_FREERTOS + +int isNull(void* ptr) { + return ptr==NULL; +} int idris_errno(void) { return errno; @@ -1154,11 +1252,15 @@ const char* idris_getArg(int i) { } void idris_disableBuffering(void) { - setvbuf(stdin, NULL, _IONBF, 0); - setvbuf(stdout, NULL, _IONBF, 0); +#ifndef BARE_METAL + setvbuf(stdin, NULL, _IONBF, 0); + setvbuf(stdout, NULL, _IONBF, 0); +#endif // BARE_METAL } void stackOverflow(void) { - fprintf(stderr, "Stack overflow"); - exit(-1); +#ifndef BARE_METAL + fprintf(stderr, "Stack overflow"); + exit(-1); +#endif // BARE_METAL } diff --git a/rts/idris_rts.h b/rts/idris_rts.h index 8ad990a5e2..d9ca6030f9 100644 --- a/rts/idris_rts.h +++ b/rts/idris_rts.h @@ -1,14 +1,23 @@ #ifndef _IDRISRTS_H #define _IDRISRTS_H -#include #include +#ifndef BARE_METAL +#include #include +#else +#include "idris_bare_metal.h" +#endif #include #ifdef HAS_PTHREAD #include #include #endif +#ifdef HAS_FREERTOS +#include +#include +#include +#endif // HAS_FREERTOS #include "idris_heap.h" #include "idris_stats.h" @@ -149,11 +158,16 @@ struct VM { Msg* inbox_end; // End of block of memory int inbox_nextid; // Next channel id Msg* inbox_write; // Location of next message to write +#elif defined(HAS_FREERTOS) + TaskHandle_t xTaskHandle; +#endif +#ifdef IS_THREADED int processes; // Number of child processes int max_threads; // maximum number of threads to run in parallel struct VM* creator; // The VM that created this VM, NULL for root VM -#endif +#endif // IS_THREADED + Stats stats; VAL ret; @@ -284,7 +298,7 @@ typedef intptr_t i_int; #define INITFRAME TRACE\ __attribute__((unused)) VAL* myoldbase;\ - void* callres + __attribute__((unused)) void* callres #define REBASE vm->valstack_base = oldbase; return NULL #define RESERVE(x) do { \ @@ -391,6 +405,8 @@ static inline Array * allocArrayF(VM * vm, size_t len, int outer) { #define allocArray(cl, vm, len, o) (cl) = (VAL)allocArrayF(vm, len, o) +int isNull(void* ptr); + int idris_errno(void); char* idris_showerror(int err); @@ -429,6 +445,11 @@ VM* idris_getSender(Msg* msg); int idris_getChannel(Msg* msg); void idris_freeMsg(Msg* msg); +#ifdef HAS_FREERTOS +void idris_queuePut(QueueHandle_t xQueue, VAL msg); +VAL idris_queueGet(VM* vm, QueueHandle_t xQueue); +#endif // HAS_FREERTOS + void idris_trace(VM* vm, const char* func, int line); void dumpVal(VAL r); void dumpStack(VM* vm); @@ -464,10 +485,12 @@ VAL idris_concat(VM* vm, VAL l, VAL r); VAL idris_strlt(VM* vm, VAL l, VAL r); VAL idris_streq(VM* vm, VAL l, VAL r); VAL idris_strlen(VM* vm, VAL l); +#ifndef BARE_METAL // Read a line from a file VAL idris_readStr(VM* vm, FILE* h); // Read up to 'num' characters from a file VAL idris_readChars(VM* vm, int num, FILE* h); +#endif VAL idris_strHead(VM* vm, VAL str); VAL idris_strShift(VM* vm, VAL str, int num); diff --git a/rts/idris_stdfgn.c b/rts/idris_stdfgn.c index e1b9fc858d..13c475ce7e 100644 --- a/rts/idris_stdfgn.c +++ b/rts/idris_stdfgn.c @@ -191,10 +191,6 @@ void *do_popen(const char *cmd, const char *mode) { return f; } -int isNull(void* ptr) { - return ptr==NULL; -} - void* idris_stdin() { return (void*)stdin; } @@ -229,6 +225,7 @@ VAL idris_clock(VM* vm) { } #ifndef SEL4 +#ifndef BARE_METAL int idris_usleep(int usec) { struct timespec t; t.tv_sec = usec / 1000000; @@ -236,6 +233,7 @@ int idris_usleep(int usec) { return nanosleep(&t, NULL); } +#endif // BARE_METAL #endif // SEL4 VAL idris_mkFileError(VM* vm) { diff --git a/rts/idris_stdfgn.h b/rts/idris_stdfgn.h index 5342b981e3..b6c5c4cce5 100644 --- a/rts/idris_stdfgn.h +++ b/rts/idris_stdfgn.h @@ -47,7 +47,6 @@ VAL idris_getString(VM* vm, void* buffer); void* do_popen(const char* cmd, const char* mode); int fpoll(void* h); -int isNull(void* ptr); void* idris_stdin(); char* getEnvPair(int i); @@ -55,7 +54,9 @@ char* getEnvPair(int i); VAL idris_time(); VAL idris_clock(VM* vm); #ifndef SEL4 +#ifndef BARE_METAL int idris_usleep(int usec); +#endif // BARE_METAL #endif // SEL4 void idris_forceGC(); diff --git a/rts/itoa.c b/rts/itoa.c new file mode 100644 index 0000000000..1374a41686 --- /dev/null +++ b/rts/itoa.c @@ -0,0 +1,318 @@ +/*** itoa.c -- fast integer to text converters + * + * Copyright (C) 2010-2017 Ruediger Meier + * Author: Ruediger Meier + * License: BSD 3-Clause, see LICENSE file + * + ***/ + +#include "itoa.h" + +/** + * reverse: reverse first l chars of string s in place + */ +void reverse( char *s, int l ) +{ + int i, j; + char c; + + for (i = 0, j = l-1; i 0); /* delete it */ + + reverse( rev, s - rev); + + return s - begin; +} + + + + +/** + * convert n to characters in s + * s will NOT be zero terminated, return strlen of s + * about 3 times faster than sprintf (in range [INT_MIN/10 - INT_MAX/10]) + * (original function found on http://cboard.cprogramming.com + * itoas() iMalc version updated ver. 0.8) + */ +int itoa_int32( char *s, int32_t snum ) +{ + char *ps = s; + uint32_t num1 = snum, num2, num3, div; + if (snum < 0) { + *ps++ = '-'; + num1 = -snum; + } + if (num1 < 10000) { + if (num1 < 10) goto L1; + if (num1 < 100) goto L2; + if (num1 < 1000) goto L3; + } else { + num2 = num1 / 10000; + num1 -= num2 * 10000; + if (num2 < 10000) { + if (num2 < 10) goto L5; + if (num2 < 100) goto L6; + if (num2 < 1000) goto L7; + } else { + num3 = num2 / 10000; + num2 -= num3 * 10000; + if (num3 >= 10) { + *ps++ = '0' + (char)(div = (num3*6554UL)>>16); + num3 -= div*10; + } + *ps++ = '0' + (char)(num3); + } + *ps++ = '0' + (char)(div = (num2*8389UL)>>23); + num2 -= div*1000; +L7: + *ps++ = '0' + (char)(div = (num2*5243UL)>>19); + num2 -= div*100; +L6: + *ps++ = '0' + (char)(div = (num2*6554UL)>>16); + num2 -= div*10; +L5: + *ps++ = '0' + (char)(num2); + } + *ps++ = '0' + (char)(div = (num1*8389UL)>>23); + num1 -= div*1000; +L3: + *ps++ = '0' + (char)(div = (num1*5243UL)>>19); + num1 -= div*100; +L2: + *ps++ = '0' + (char)(div = (num1*6554UL)>>16); + num1 -= div*10; +L1: + *ps++ = '0' + (char)(num1); + + return ps - s; +} + + + + +int itoa_int64( char *s, int64_t snum ) +{ + char *ps = s; + uint64_t num1 = snum, num2, num3, num4, num5, div; + + if (snum < 0) { + *ps++ = '-'; + num1 = -snum; + } + + if (num1 < 10000) { + if (num1 < 10) goto L1; + if (num1 < 100) goto L2; + if (num1 < 1000) goto L3; + } else { + num2 = num1 / 10000; + num1 -= num2 * 10000; + if (num2 < 10000) { + if (num2 < 10) goto L5; + if (num2 < 100) goto L6; + if (num2 < 1000) goto L7; + } else { + num3 = num2 / 10000; + num2 -= num3 * 10000; + if (num3 < 10000) { + if (num3 < 10) goto L9; + if (num3 < 100) goto L10; + if (num3 < 1000) goto L11; + } else { + num4 = num3 / 10000; + num3 -= num4 * 10000; + if (num4 < 10000) { + if (num4 < 10) goto L13; + if (num4 < 100) goto L14; + if (num4 < 1000) goto L15; + } else { + num5 = num4 / 10000; + num4 -= num5 * 10000; + if (num5 < 10000) { + if (num5 < 10) goto L17; + if (num5 < 100) goto L18; + } + *ps++ = '0' + (char)(div = (num5*5243UL)>>19); + num5 -= div*100; +L18: + *ps++ = '0' + (char)(div = (num5*6554UL)>>16); + num5 -= div*10; +L17: + *ps++ = '0' + (char)(num5); + } + *ps++ = '0' + (char)(div = (num4*8389UL)>>23); + num4 -= div*1000; +L15: + *ps++ = '0' + (char)(div = (num4*5243UL)>>19); + num4 -= div*100; +L14: + *ps++ = '0' + (char)(div = (num4*6554UL)>>16); + num4 -= div*10; +L13: + *ps++ = '0' + (char)(num4); + } + *ps++ = '0' + (char)(div = (num3*8389UL)>>23); + num3 -= div*1000; +L11: + *ps++ = '0' + (char)(div = (num3*5243UL)>>19); + num3 -= div*100; +L10: + *ps++ = '0' + (char)(div = (num3*6554UL)>>16); + num3 -= div*10; +L9: + *ps++ = '0' + (char)(num3); + } + *ps++ = '0' + (char)(div = (num2*8389UL)>>23); + num2 -= div*1000; +L7: + *ps++ = '0' + (char)(div = (num2*5243UL)>>19); + num2 -= div*100; +L6: + *ps++ = '0' + (char)(div = (num2*6554UL)>>16); + num2 -= div*10; +L5: + *ps++ = '0' + (char)(num2); + } + *ps++ = '0' + (char)(div = (num1*8389UL)>>23); + num1 -= div*1000; +L3: + *ps++ = '0' + (char)(div = (num1*5243UL)>>19); + num1 -= div*100; +L2: + *ps++ = '0' + (char)(div = (num1*6554UL)>>16); + num1 -= div*10; +L1: + *ps++ = '0' + (char)(num1); + + return ps - s; + +} + + + + +int itoa_uint64( char *s, uint64_t snum ) +{ + char *ps = s; + uint64_t num1 = snum, num2, num3, num4, num5, div; + + if (num1 < 10000) { + if (num1 < 10) goto L1; + if (num1 < 100) goto L2; + if (num1 < 1000) goto L3; + } else { + num2 = num1 / 10000; + num1 -= num2 * 10000; + if (num2 < 10000) { + if (num2 < 10) goto L5; + if (num2 < 100) goto L6; + if (num2 < 1000) goto L7; + } else { + num3 = num2 / 10000; + num2 -= num3 * 10000; + if (num3 < 10000) { + if (num3 < 10) goto L9; + if (num3 < 100) goto L10; + if (num3 < 1000) goto L11; + } else { + num4 = num3 / 10000; + num3 -= num4 * 10000; + if (num4 < 10000) { + if (num4 < 10) goto L13; + if (num4 < 100) goto L14; + if (num4 < 1000) goto L15; + } else { + num5 = num4 / 10000; + num4 -= num5 * 10000; + if (num5 < 10000) { + if (num5 < 10) goto L17; + if (num5 < 100) goto L18; + if (num5 < 1000) goto L19; + } + + *ps++ = '0' + (char)(div = (num5*8389UL)>>23); + num5 -= div*1000; +L19: + *ps++ = '0' + (char)(div = (num5*5243UL)>>19); + num5 -= div*100; +L18: + *ps++ = '0' + (char)(div = (num5*6554UL)>>16); + num5 -= div*10; +L17: + *ps++ = '0' + (char)(num5); + } + *ps++ = '0' + (char)(div = (num4*8389UL)>>23); + num4 -= div*1000; +L15: + *ps++ = '0' + (char)(div = (num4*5243UL)>>19); + num4 -= div*100; +L14: + *ps++ = '0' + (char)(div = (num4*6554UL)>>16); + num4 -= div*10; +L13: + *ps++ = '0' + (char)(num4); + } + *ps++ = '0' + (char)(div = (num3*8389UL)>>23); + num3 -= div*1000; +L11: + *ps++ = '0' + (char)(div = (num3*5243UL)>>19); + num3 -= div*100; +L10: + *ps++ = '0' + (char)(div = (num3*6554UL)>>16); + num3 -= div*10; +L9: + *ps++ = '0' + (char)(num3); + } + *ps++ = '0' + (char)(div = (num2*8389UL)>>23); + num2 -= div*1000; +L7: + *ps++ = '0' + (char)(div = (num2*5243UL)>>19); + num2 -= div*100; +L6: + *ps++ = '0' + (char)(div = (num2*6554UL)>>16); + num2 -= div*10; +L5: + *ps++ = '0' + (char)(num2); + } + *ps++ = '0' + (char)(div = (num1*8389UL)>>23); + num1 -= div*1000; +L3: + *ps++ = '0' + (char)(div = (num1*5243UL)>>19); + num1 -= div*100; +L2: + *ps++ = '0' + (char)(div = (num1*6554UL)>>16); + num1 -= div*10; +L1: + *ps++ = '0' + (char)(num1); + + return ps - s; + +} diff --git a/rts/itoa.h b/rts/itoa.h new file mode 100644 index 0000000000..a613fd1429 --- /dev/null +++ b/rts/itoa.h @@ -0,0 +1,6 @@ +#include + +int ltoa_simple(char *s, long num); +int itoa_int32(char *s, int32_t snum); +int itoa_int64(char *s, int64_t snum); +int itoa_uint64(char *s, uint64_t snum); diff --git a/rts/mini-gmp.c b/rts/mini-gmp.c index b5a4fe3119..7c76c2c387 100644 --- a/rts/mini-gmp.c +++ b/rts/mini-gmp.c @@ -41,10 +41,14 @@ see https://www.gnu.org/licenses/. */ mpn/generic/sbpi1_div_qr.c, mpn/generic/sub_n.c, mpn/generic/submul_1.c. */ +#ifndef BARE_METAL #include +#include +#else +#include "idris_bare_metal.h" +#endif #include #include -#include #include #include @@ -71,10 +75,14 @@ see https://www.gnu.org/licenses/. */ #define GMP_CMP(a,b) (((a) > (b)) - ((a) < (b))) +#ifndef BARE_METAL #define gmp_assert_nocarry(x) do { \ mp_limb_t __cy = (x); \ assert (__cy == 0); \ } while (0) +#else +#define gmp_assert_nocarry(...) +#endif #define gmp_clz(count, x) do { \ mp_limb_t __clz_x = (x); \ @@ -266,6 +274,7 @@ gmp_default_alloc (size_t size) static void * gmp_default_realloc (void *old, size_t old_size, size_t new_size) { +#ifndef BARE_METAL void * p; p = realloc (old, new_size); @@ -274,6 +283,9 @@ gmp_default_realloc (void *old, size_t old_size, size_t new_size) gmp_die("gmp_default_realloc: Virtual memory exhausted."); return p; +#else + return NULL; +#endif // BARE_METAL } static void @@ -4231,6 +4243,7 @@ mpz_init_set_str (mpz_t r, const char *sp, int base) return mpz_set_str (r, sp, base); } +#ifndef BARE_METAL size_t mpz_out_str (FILE *stream, int base, const mpz_t x) { @@ -4243,6 +4256,7 @@ mpz_out_str (FILE *stream, int base, const mpz_t x) gmp_free (str); return len; } +#endif // BARE_METAL static int diff --git a/rts/seL4/CMakeLists.txt b/rts/seL4/CMakeLists.txt index 8bbc868c2c..9fbb9deecd 100644 --- a/rts/seL4/CMakeLists.txt +++ b/rts/seL4/CMakeLists.txt @@ -13,6 +13,7 @@ file(GLOB static rts/idris_utf8.c rts/idris_stdfgn.c rts/mini-gmp.c + rts/itoa.c rts/idris_buffer.c rts/getline.c rts/idris_net.c