diff --git a/THIRD_PARTY_FILES.md b/THIRD_PARTY_FILES.md index 87765e8c6..5d75ca917 100644 --- a/THIRD_PARTY_FILES.md +++ b/THIRD_PARTY_FILES.md @@ -14,6 +14,13 @@ https://github.com/asciidoctor/asciidoctor | ------------ | ----------------------- | ----------- | | MIT | doc/asciidoc/manual.css | Asciidoctor | +The following files are from cJSON https://github.com/DaveGamble/cJSON + +| License | Files | Source | +| ------------ | ----------------------- | ------ | +| MIT | lib/json/cJSON.c | cJSON | +| MIT | lib/json/cJSON.h | cJSON | + CIL === @@ -113,3 +120,28 @@ LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. ``` + +cJSON +===== + +``` +Copyright (c) 2009-2017 Dave Gamble and cJSON contributors + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. +``` diff --git a/editors/sail-mode.el b/editors/sail-mode.el index a1db504e5..06cc110a2 100644 --- a/editors/sail-mode.el +++ b/editors/sail-mode.el @@ -32,7 +32,7 @@ (defconst sail-keywords '("val" "outcome" "function" "type" "struct" "union" "enum" "let" "var" "if" "then" "by" - "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect" + "else" "match" "in" "return" "register" "ref" "forall" "operator" "effect" "config" "overload" "cast" "sizeof" "constant" "constraint" "default" "assert" "newtype" "from" "pure" "impure" "monadic" "infixl" "infixr" "infix" "scattered" "end" "try" "catch" "and" "to" "private" "throw" "clause" "as" "repeat" "until" "while" "do" "foreach" "bitfield" diff --git a/language/jib.ott b/language/jib.ott index bda70256e..54ab25a45 100644 --- a/language/jib.ott +++ b/language/jib.ott @@ -138,6 +138,7 @@ cval :: 'V_' ::= | cval nat0 nat1 :: :: tuple_member | op ( cval0 , ... , cvaln ) :: :: call | cval . id :: :: field + | string0 . ... . stringn :: :: config_key % Note that init / clear are sometimes referred to as create / kill @@ -196,6 +197,8 @@ ctyp :: 'CT_' ::= | poly kid :: :: poly | memory_writes :: :: memory_writes +% Used for configuration, an immutable reference to some json data + | json :: :: json clexp :: 'CL_' ::= | name : ctyp :: :: id diff --git a/language/sail.ott b/language/sail.ott index 3eec12f7c..508edba31 100644 --- a/language/sail.ott +++ b/language/sail.ott @@ -455,8 +455,8 @@ grammar %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% loop :: loop ::= {{ phantom }} - | while :: :: while - | until :: :: until + | while :: :: while + | until :: :: until internal_loop_measure :: 'Measure_' ::= {{ com internal syntax for an optional termination measure for a loop }} @@ -516,8 +516,10 @@ exp :: 'E_' ::= {{ com the value of $[[nexp]]$ at run time }} | return exp :: :: return {{ com return $[[exp]]$ from current function }} - | exit exp :: :: exit - {{ com halt all current execution }} + | exit exp :: :: exit {{ com halt all current execution }} + + | config string1 . ... . stringn :: :: config {{ com model configuration value }} + | ref id :: :: ref | throw exp :: :: throw | try exp catch { pexp1 , ... , pexpn } :: :: try diff --git a/lib/json/LICENSE b/lib/json/LICENSE new file mode 100644 index 000000000..78deb0406 --- /dev/null +++ b/lib/json/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2009-2017 Dave Gamble and cJSON contributors + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. + diff --git a/lib/json/cJSON.c b/lib/json/cJSON.c new file mode 100644 index 000000000..d7c72363d --- /dev/null +++ b/lib/json/cJSON.c @@ -0,0 +1,3164 @@ +/* + Copyright (c) 2009-2017 Dave Gamble and cJSON contributors + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in + all copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + THE SOFTWARE. +*/ + +/* cJSON */ +/* JSON parser in C. */ + +/* disable warnings about old C89 functions in MSVC */ +#if !defined(_CRT_SECURE_NO_DEPRECATE) && defined(_MSC_VER) +#define _CRT_SECURE_NO_DEPRECATE +#endif + +#ifdef __GNUC__ +#pragma GCC visibility push(default) +#endif +#if defined(_MSC_VER) +#pragma warning (push) +/* disable warning about single line comments in system headers */ +#pragma warning (disable : 4001) +#endif + +#include +#include +#include +#include +#include +#include +#include + +#ifdef ENABLE_LOCALES +#include +#endif + +#if defined(_MSC_VER) +#pragma warning (pop) +#endif +#ifdef __GNUC__ +#pragma GCC visibility pop +#endif + +#include "cJSON.h" + +/* define our own boolean type */ +#ifdef true +#undef true +#endif +#define true ((cJSON_bool)1) + +#ifdef false +#undef false +#endif +#define false ((cJSON_bool)0) + +/* define isnan and isinf for ANSI C, if in C99 or above, isnan and isinf has been defined in math.h */ +#ifndef isinf +#define isinf(d) (isnan((d - d)) && !isnan(d)) +#endif +#ifndef isnan +#define isnan(d) (d != d) +#endif + +#ifndef NAN +#ifdef _WIN32 +#define NAN sqrt(-1.0) +#else +#define NAN 0.0/0.0 +#endif +#endif + +typedef struct { + const unsigned char *json; + size_t position; +} error; +static error global_error = { NULL, 0 }; + +CJSON_PUBLIC(const char *) cJSON_GetErrorPtr(void) +{ + return (const char*) (global_error.json + global_error.position); +} + +CJSON_PUBLIC(char *) cJSON_GetStringValue(const cJSON * const item) +{ + if (!cJSON_IsString(item)) + { + return NULL; + } + + return item->valuestring; +} + +CJSON_PUBLIC(double) cJSON_GetNumberValue(const cJSON * const item) +{ + if (!cJSON_IsNumber(item)) + { + return (double) NAN; + } + + return item->valuedouble; +} + +/* This is a safeguard to prevent copy-pasters from using incompatible C and header files */ +#if (CJSON_VERSION_MAJOR != 1) || (CJSON_VERSION_MINOR != 7) || (CJSON_VERSION_PATCH != 18) + #error cJSON.h and cJSON.c have different versions. Make sure that both have the same. +#endif + +CJSON_PUBLIC(const char*) cJSON_Version(void) +{ + static char version[15]; + sprintf(version, "%i.%i.%i", CJSON_VERSION_MAJOR, CJSON_VERSION_MINOR, CJSON_VERSION_PATCH); + + return version; +} + +/* Case insensitive string comparison, doesn't consider two NULL pointers equal though */ +static int case_insensitive_strcmp(const unsigned char *string1, const unsigned char *string2) +{ + if ((string1 == NULL) || (string2 == NULL)) + { + return 1; + } + + if (string1 == string2) + { + return 0; + } + + for(; tolower(*string1) == tolower(*string2); (void)string1++, string2++) + { + if (*string1 == '\0') + { + return 0; + } + } + + return tolower(*string1) - tolower(*string2); +} + +typedef struct internal_hooks +{ + void *(CJSON_CDECL *allocate)(size_t size); + void (CJSON_CDECL *deallocate)(void *pointer); + void *(CJSON_CDECL *reallocate)(void *pointer, size_t size); +} internal_hooks; + +#if defined(_MSC_VER) +/* work around MSVC error C2322: '...' address of dllimport '...' is not static */ +static void * CJSON_CDECL internal_malloc(size_t size) +{ + return malloc(size); +} +static void CJSON_CDECL internal_free(void *pointer) +{ + free(pointer); +} +static void * CJSON_CDECL internal_realloc(void *pointer, size_t size) +{ + return realloc(pointer, size); +} +#else +#define internal_malloc malloc +#define internal_free free +#define internal_realloc realloc +#endif + +/* strlen of character literals resolved at compile time */ +#define static_strlen(string_literal) (sizeof(string_literal) - sizeof("")) + +static internal_hooks global_hooks = { internal_malloc, internal_free, internal_realloc }; + +static unsigned char* cJSON_strdup(const unsigned char* string, const internal_hooks * const hooks) +{ + size_t length = 0; + unsigned char *copy = NULL; + + if (string == NULL) + { + return NULL; + } + + length = strlen((const char*)string) + sizeof(""); + copy = (unsigned char*)hooks->allocate(length); + if (copy == NULL) + { + return NULL; + } + memcpy(copy, string, length); + + return copy; +} + +CJSON_PUBLIC(void) cJSON_InitHooks(cJSON_Hooks* hooks) +{ + if (hooks == NULL) + { + /* Reset hooks */ + global_hooks.allocate = malloc; + global_hooks.deallocate = free; + global_hooks.reallocate = realloc; + return; + } + + global_hooks.allocate = malloc; + if (hooks->malloc_fn != NULL) + { + global_hooks.allocate = hooks->malloc_fn; + } + + global_hooks.deallocate = free; + if (hooks->free_fn != NULL) + { + global_hooks.deallocate = hooks->free_fn; + } + + /* use realloc only if both free and malloc are used */ + global_hooks.reallocate = NULL; + if ((global_hooks.allocate == malloc) && (global_hooks.deallocate == free)) + { + global_hooks.reallocate = realloc; + } +} + +/* Internal constructor. */ +static cJSON *cJSON_New_Item(const internal_hooks * const hooks) +{ + cJSON* node = (cJSON*)hooks->allocate(sizeof(cJSON)); + if (node) + { + memset(node, '\0', sizeof(cJSON)); + } + + return node; +} + +/* Delete a cJSON structure. */ +CJSON_PUBLIC(void) cJSON_Delete(cJSON *item) +{ + cJSON *next = NULL; + while (item != NULL) + { + next = item->next; + if (!(item->type & cJSON_IsReference) && (item->child != NULL)) + { + cJSON_Delete(item->child); + } + if (!(item->type & cJSON_IsReference) && (item->valuestring != NULL)) + { + global_hooks.deallocate(item->valuestring); + item->valuestring = NULL; + } + if (!(item->type & cJSON_StringIsConst) && (item->string != NULL)) + { + global_hooks.deallocate(item->string); + item->string = NULL; + } + global_hooks.deallocate(item); + item = next; + } +} + +/* get the decimal point character of the current locale */ +static unsigned char get_decimal_point(void) +{ +#ifdef ENABLE_LOCALES + struct lconv *lconv = localeconv(); + return (unsigned char) lconv->decimal_point[0]; +#else + return '.'; +#endif +} + +typedef struct +{ + const unsigned char *content; + size_t length; + size_t offset; + size_t depth; /* How deeply nested (in arrays/objects) is the input at the current offset. */ + internal_hooks hooks; +} parse_buffer; + +/* check if the given size is left to read in a given parse buffer (starting with 1) */ +#define can_read(buffer, size) ((buffer != NULL) && (((buffer)->offset + size) <= (buffer)->length)) +/* check if the buffer can be accessed at the given index (starting with 0) */ +#define can_access_at_index(buffer, index) ((buffer != NULL) && (((buffer)->offset + index) < (buffer)->length)) +#define cannot_access_at_index(buffer, index) (!can_access_at_index(buffer, index)) +/* get a pointer to the buffer at the position */ +#define buffer_at_offset(buffer) ((buffer)->content + (buffer)->offset) + +/* Parse the input text to generate a number, and populate the result into item. */ +static cJSON_bool parse_number(cJSON * const item, parse_buffer * const input_buffer) +{ + double number = 0; + unsigned char *after_end = NULL; + unsigned char number_c_string[64]; + unsigned char decimal_point = get_decimal_point(); + size_t i = 0; + + if ((input_buffer == NULL) || (input_buffer->content == NULL)) + { + return false; + } + + /* copy the number into a temporary buffer and replace '.' with the decimal point + * of the current locale (for strtod) + * This also takes care of '\0' not necessarily being available for marking the end of the input */ + for (i = 0; (i < (sizeof(number_c_string) - 1)) && can_access_at_index(input_buffer, i); i++) + { + switch (buffer_at_offset(input_buffer)[i]) + { + case '0': + case '1': + case '2': + case '3': + case '4': + case '5': + case '6': + case '7': + case '8': + case '9': + case '+': + case '-': + case 'e': + case 'E': + number_c_string[i] = buffer_at_offset(input_buffer)[i]; + break; + + case '.': + number_c_string[i] = decimal_point; + break; + + default: + goto loop_end; + } + } +loop_end: + number_c_string[i] = '\0'; + + number = strtod((const char*)number_c_string, (char**)&after_end); + if (number_c_string == after_end) + { + return false; /* parse_error */ + } + + item->valuedouble = number; + + /* use saturation in case of overflow */ + if (number >= INT_MAX) + { + item->valueint = INT_MAX; + } + else if (number <= (double)INT_MIN) + { + item->valueint = INT_MIN; + } + else + { + item->valueint = (int)number; + } + + item->type = cJSON_Number; + + input_buffer->offset += (size_t)(after_end - number_c_string); + return true; +} + +/* don't ask me, but the original cJSON_SetNumberValue returns an integer or double */ +CJSON_PUBLIC(double) cJSON_SetNumberHelper(cJSON *object, double number) +{ + if (number >= INT_MAX) + { + object->valueint = INT_MAX; + } + else if (number <= (double)INT_MIN) + { + object->valueint = INT_MIN; + } + else + { + object->valueint = (int)number; + } + + return object->valuedouble = number; +} + +/* Note: when passing a NULL valuestring, cJSON_SetValuestring treats this as an error and return NULL */ +CJSON_PUBLIC(char*) cJSON_SetValuestring(cJSON *object, const char *valuestring) +{ + char *copy = NULL; + size_t v1_len; + size_t v2_len; + /* if object's type is not cJSON_String or is cJSON_IsReference, it should not set valuestring */ + if ((object == NULL) || !(object->type & cJSON_String) || (object->type & cJSON_IsReference)) + { + return NULL; + } + /* return NULL if the object is corrupted or valuestring is NULL */ + if (object->valuestring == NULL || valuestring == NULL) + { + return NULL; + } + + v1_len = strlen(valuestring); + v2_len = strlen(object->valuestring); + + if (v1_len <= v2_len) + { + /* strcpy does not handle overlapping string: [X1, X2] [Y1, Y2] => X2 < Y1 or Y2 < X1 */ + if (!( valuestring + v1_len < object->valuestring || object->valuestring + v2_len < valuestring )) + { + return NULL; + } + strcpy(object->valuestring, valuestring); + return object->valuestring; + } + copy = (char*) cJSON_strdup((const unsigned char*)valuestring, &global_hooks); + if (copy == NULL) + { + return NULL; + } + if (object->valuestring != NULL) + { + cJSON_free(object->valuestring); + } + object->valuestring = copy; + + return copy; +} + +typedef struct +{ + unsigned char *buffer; + size_t length; + size_t offset; + size_t depth; /* current nesting depth (for formatted printing) */ + cJSON_bool noalloc; + cJSON_bool format; /* is this print a formatted print */ + internal_hooks hooks; +} printbuffer; + +/* realloc printbuffer if necessary to have at least "needed" bytes more */ +static unsigned char* ensure(printbuffer * const p, size_t needed) +{ + unsigned char *newbuffer = NULL; + size_t newsize = 0; + + if ((p == NULL) || (p->buffer == NULL)) + { + return NULL; + } + + if ((p->length > 0) && (p->offset >= p->length)) + { + /* make sure that offset is valid */ + return NULL; + } + + if (needed > INT_MAX) + { + /* sizes bigger than INT_MAX are currently not supported */ + return NULL; + } + + needed += p->offset + 1; + if (needed <= p->length) + { + return p->buffer + p->offset; + } + + if (p->noalloc) { + return NULL; + } + + /* calculate new buffer size */ + if (needed > (INT_MAX / 2)) + { + /* overflow of int, use INT_MAX if possible */ + if (needed <= INT_MAX) + { + newsize = INT_MAX; + } + else + { + return NULL; + } + } + else + { + newsize = needed * 2; + } + + if (p->hooks.reallocate != NULL) + { + /* reallocate with realloc if available */ + newbuffer = (unsigned char*)p->hooks.reallocate(p->buffer, newsize); + if (newbuffer == NULL) + { + p->hooks.deallocate(p->buffer); + p->length = 0; + p->buffer = NULL; + + return NULL; + } + } + else + { + /* otherwise reallocate manually */ + newbuffer = (unsigned char*)p->hooks.allocate(newsize); + if (!newbuffer) + { + p->hooks.deallocate(p->buffer); + p->length = 0; + p->buffer = NULL; + + return NULL; + } + + memcpy(newbuffer, p->buffer, p->offset + 1); + p->hooks.deallocate(p->buffer); + } + p->length = newsize; + p->buffer = newbuffer; + + return newbuffer + p->offset; +} + +/* calculate the new length of the string in a printbuffer and update the offset */ +static void update_offset(printbuffer * const buffer) +{ + const unsigned char *buffer_pointer = NULL; + if ((buffer == NULL) || (buffer->buffer == NULL)) + { + return; + } + buffer_pointer = buffer->buffer + buffer->offset; + + buffer->offset += strlen((const char*)buffer_pointer); +} + +/* securely comparison of floating-point variables */ +static cJSON_bool compare_double(double a, double b) +{ + double maxVal = fabs(a) > fabs(b) ? fabs(a) : fabs(b); + return (fabs(a - b) <= maxVal * DBL_EPSILON); +} + +/* Render the number nicely from the given item into a string. */ +static cJSON_bool print_number(const cJSON * const item, printbuffer * const output_buffer) +{ + unsigned char *output_pointer = NULL; + double d = item->valuedouble; + int length = 0; + size_t i = 0; + unsigned char number_buffer[26] = {0}; /* temporary buffer to print the number into */ + unsigned char decimal_point = get_decimal_point(); + double test = 0.0; + + if (output_buffer == NULL) + { + return false; + } + + /* This checks for NaN and Infinity */ + if (isnan(d) || isinf(d)) + { + length = sprintf((char*)number_buffer, "null"); + } + else if(d == (double)item->valueint) + { + length = sprintf((char*)number_buffer, "%d", item->valueint); + } + else + { + /* Try 15 decimal places of precision to avoid nonsignificant nonzero digits */ + length = sprintf((char*)number_buffer, "%1.15g", d); + + /* Check whether the original double can be recovered */ + if ((sscanf((char*)number_buffer, "%lg", &test) != 1) || !compare_double((double)test, d)) + { + /* If not, print with 17 decimal places of precision */ + length = sprintf((char*)number_buffer, "%1.17g", d); + } + } + + /* sprintf failed or buffer overrun occurred */ + if ((length < 0) || (length > (int)(sizeof(number_buffer) - 1))) + { + return false; + } + + /* reserve appropriate space in the output */ + output_pointer = ensure(output_buffer, (size_t)length + sizeof("")); + if (output_pointer == NULL) + { + return false; + } + + /* copy the printed number to the output and replace locale + * dependent decimal point with '.' */ + for (i = 0; i < ((size_t)length); i++) + { + if (number_buffer[i] == decimal_point) + { + output_pointer[i] = '.'; + continue; + } + + output_pointer[i] = number_buffer[i]; + } + output_pointer[i] = '\0'; + + output_buffer->offset += (size_t)length; + + return true; +} + +/* parse 4 digit hexadecimal number */ +static unsigned parse_hex4(const unsigned char * const input) +{ + unsigned int h = 0; + size_t i = 0; + + for (i = 0; i < 4; i++) + { + /* parse digit */ + if ((input[i] >= '0') && (input[i] <= '9')) + { + h += (unsigned int) input[i] - '0'; + } + else if ((input[i] >= 'A') && (input[i] <= 'F')) + { + h += (unsigned int) 10 + input[i] - 'A'; + } + else if ((input[i] >= 'a') && (input[i] <= 'f')) + { + h += (unsigned int) 10 + input[i] - 'a'; + } + else /* invalid */ + { + return 0; + } + + if (i < 3) + { + /* shift left to make place for the next nibble */ + h = h << 4; + } + } + + return h; +} + +/* converts a UTF-16 literal to UTF-8 + * A literal can be one or two sequences of the form \uXXXX */ +static unsigned char utf16_literal_to_utf8(const unsigned char * const input_pointer, const unsigned char * const input_end, unsigned char **output_pointer) +{ + long unsigned int codepoint = 0; + unsigned int first_code = 0; + const unsigned char *first_sequence = input_pointer; + unsigned char utf8_length = 0; + unsigned char utf8_position = 0; + unsigned char sequence_length = 0; + unsigned char first_byte_mark = 0; + + if ((input_end - first_sequence) < 6) + { + /* input ends unexpectedly */ + goto fail; + } + + /* get the first utf16 sequence */ + first_code = parse_hex4(first_sequence + 2); + + /* check that the code is valid */ + if (((first_code >= 0xDC00) && (first_code <= 0xDFFF))) + { + goto fail; + } + + /* UTF16 surrogate pair */ + if ((first_code >= 0xD800) && (first_code <= 0xDBFF)) + { + const unsigned char *second_sequence = first_sequence + 6; + unsigned int second_code = 0; + sequence_length = 12; /* \uXXXX\uXXXX */ + + if ((input_end - second_sequence) < 6) + { + /* input ends unexpectedly */ + goto fail; + } + + if ((second_sequence[0] != '\\') || (second_sequence[1] != 'u')) + { + /* missing second half of the surrogate pair */ + goto fail; + } + + /* get the second utf16 sequence */ + second_code = parse_hex4(second_sequence + 2); + /* check that the code is valid */ + if ((second_code < 0xDC00) || (second_code > 0xDFFF)) + { + /* invalid second half of the surrogate pair */ + goto fail; + } + + + /* calculate the unicode codepoint from the surrogate pair */ + codepoint = 0x10000 + (((first_code & 0x3FF) << 10) | (second_code & 0x3FF)); + } + else + { + sequence_length = 6; /* \uXXXX */ + codepoint = first_code; + } + + /* encode as UTF-8 + * takes at maximum 4 bytes to encode: + * 11110xxx 10xxxxxx 10xxxxxx 10xxxxxx */ + if (codepoint < 0x80) + { + /* normal ascii, encoding 0xxxxxxx */ + utf8_length = 1; + } + else if (codepoint < 0x800) + { + /* two bytes, encoding 110xxxxx 10xxxxxx */ + utf8_length = 2; + first_byte_mark = 0xC0; /* 11000000 */ + } + else if (codepoint < 0x10000) + { + /* three bytes, encoding 1110xxxx 10xxxxxx 10xxxxxx */ + utf8_length = 3; + first_byte_mark = 0xE0; /* 11100000 */ + } + else if (codepoint <= 0x10FFFF) + { + /* four bytes, encoding 1110xxxx 10xxxxxx 10xxxxxx 10xxxxxx */ + utf8_length = 4; + first_byte_mark = 0xF0; /* 11110000 */ + } + else + { + /* invalid unicode codepoint */ + goto fail; + } + + /* encode as utf8 */ + for (utf8_position = (unsigned char)(utf8_length - 1); utf8_position > 0; utf8_position--) + { + /* 10xxxxxx */ + (*output_pointer)[utf8_position] = (unsigned char)((codepoint | 0x80) & 0xBF); + codepoint >>= 6; + } + /* encode first byte */ + if (utf8_length > 1) + { + (*output_pointer)[0] = (unsigned char)((codepoint | first_byte_mark) & 0xFF); + } + else + { + (*output_pointer)[0] = (unsigned char)(codepoint & 0x7F); + } + + *output_pointer += utf8_length; + + return sequence_length; + +fail: + return 0; +} + +/* Parse the input text into an unescaped cinput, and populate item. */ +static cJSON_bool parse_string(cJSON * const item, parse_buffer * const input_buffer) +{ + const unsigned char *input_pointer = buffer_at_offset(input_buffer) + 1; + const unsigned char *input_end = buffer_at_offset(input_buffer) + 1; + unsigned char *output_pointer = NULL; + unsigned char *output = NULL; + + /* not a string */ + if (buffer_at_offset(input_buffer)[0] != '\"') + { + goto fail; + } + + { + /* calculate approximate size of the output (overestimate) */ + size_t allocation_length = 0; + size_t skipped_bytes = 0; + while (((size_t)(input_end - input_buffer->content) < input_buffer->length) && (*input_end != '\"')) + { + /* is escape sequence */ + if (input_end[0] == '\\') + { + if ((size_t)(input_end + 1 - input_buffer->content) >= input_buffer->length) + { + /* prevent buffer overflow when last input character is a backslash */ + goto fail; + } + skipped_bytes++; + input_end++; + } + input_end++; + } + if (((size_t)(input_end - input_buffer->content) >= input_buffer->length) || (*input_end != '\"')) + { + goto fail; /* string ended unexpectedly */ + } + + /* This is at most how much we need for the output */ + allocation_length = (size_t) (input_end - buffer_at_offset(input_buffer)) - skipped_bytes; + output = (unsigned char*)input_buffer->hooks.allocate(allocation_length + sizeof("")); + if (output == NULL) + { + goto fail; /* allocation failure */ + } + } + + output_pointer = output; + /* loop through the string literal */ + while (input_pointer < input_end) + { + if (*input_pointer != '\\') + { + *output_pointer++ = *input_pointer++; + } + /* escape sequence */ + else + { + unsigned char sequence_length = 2; + if ((input_end - input_pointer) < 1) + { + goto fail; + } + + switch (input_pointer[1]) + { + case 'b': + *output_pointer++ = '\b'; + break; + case 'f': + *output_pointer++ = '\f'; + break; + case 'n': + *output_pointer++ = '\n'; + break; + case 'r': + *output_pointer++ = '\r'; + break; + case 't': + *output_pointer++ = '\t'; + break; + case '\"': + case '\\': + case '/': + *output_pointer++ = input_pointer[1]; + break; + + /* UTF-16 literal */ + case 'u': + sequence_length = utf16_literal_to_utf8(input_pointer, input_end, &output_pointer); + if (sequence_length == 0) + { + /* failed to convert UTF16-literal to UTF-8 */ + goto fail; + } + break; + + default: + goto fail; + } + input_pointer += sequence_length; + } + } + + /* zero terminate the output */ + *output_pointer = '\0'; + + item->type = cJSON_String; + item->valuestring = (char*)output; + + input_buffer->offset = (size_t) (input_end - input_buffer->content); + input_buffer->offset++; + + return true; + +fail: + if (output != NULL) + { + input_buffer->hooks.deallocate(output); + output = NULL; + } + + if (input_pointer != NULL) + { + input_buffer->offset = (size_t)(input_pointer - input_buffer->content); + } + + return false; +} + +/* Render the cstring provided to an escaped version that can be printed. */ +static cJSON_bool print_string_ptr(const unsigned char * const input, printbuffer * const output_buffer) +{ + const unsigned char *input_pointer = NULL; + unsigned char *output = NULL; + unsigned char *output_pointer = NULL; + size_t output_length = 0; + /* numbers of additional characters needed for escaping */ + size_t escape_characters = 0; + + if (output_buffer == NULL) + { + return false; + } + + /* empty string */ + if (input == NULL) + { + output = ensure(output_buffer, sizeof("\"\"")); + if (output == NULL) + { + return false; + } + strcpy((char*)output, "\"\""); + + return true; + } + + /* set "flag" to 1 if something needs to be escaped */ + for (input_pointer = input; *input_pointer; input_pointer++) + { + switch (*input_pointer) + { + case '\"': + case '\\': + case '\b': + case '\f': + case '\n': + case '\r': + case '\t': + /* one character escape sequence */ + escape_characters++; + break; + default: + if (*input_pointer < 32) + { + /* UTF-16 escape sequence uXXXX */ + escape_characters += 5; + } + break; + } + } + output_length = (size_t)(input_pointer - input) + escape_characters; + + output = ensure(output_buffer, output_length + sizeof("\"\"")); + if (output == NULL) + { + return false; + } + + /* no characters have to be escaped */ + if (escape_characters == 0) + { + output[0] = '\"'; + memcpy(output + 1, input, output_length); + output[output_length + 1] = '\"'; + output[output_length + 2] = '\0'; + + return true; + } + + output[0] = '\"'; + output_pointer = output + 1; + /* copy the string */ + for (input_pointer = input; *input_pointer != '\0'; (void)input_pointer++, output_pointer++) + { + if ((*input_pointer > 31) && (*input_pointer != '\"') && (*input_pointer != '\\')) + { + /* normal character, copy */ + *output_pointer = *input_pointer; + } + else + { + /* character needs to be escaped */ + *output_pointer++ = '\\'; + switch (*input_pointer) + { + case '\\': + *output_pointer = '\\'; + break; + case '\"': + *output_pointer = '\"'; + break; + case '\b': + *output_pointer = 'b'; + break; + case '\f': + *output_pointer = 'f'; + break; + case '\n': + *output_pointer = 'n'; + break; + case '\r': + *output_pointer = 'r'; + break; + case '\t': + *output_pointer = 't'; + break; + default: + /* escape and print as unicode codepoint */ + sprintf((char*)output_pointer, "u%04x", *input_pointer); + output_pointer += 4; + break; + } + } + } + output[output_length + 1] = '\"'; + output[output_length + 2] = '\0'; + + return true; +} + +/* Invoke print_string_ptr (which is useful) on an item. */ +static cJSON_bool print_string(const cJSON * const item, printbuffer * const p) +{ + return print_string_ptr((unsigned char*)item->valuestring, p); +} + +/* Predeclare these prototypes. */ +static cJSON_bool parse_value(cJSON * const item, parse_buffer * const input_buffer); +static cJSON_bool print_value(const cJSON * const item, printbuffer * const output_buffer); +static cJSON_bool parse_array(cJSON * const item, parse_buffer * const input_buffer); +static cJSON_bool print_array(const cJSON * const item, printbuffer * const output_buffer); +static cJSON_bool parse_object(cJSON * const item, parse_buffer * const input_buffer); +static cJSON_bool print_object(const cJSON * const item, printbuffer * const output_buffer); + +/* Utility to jump whitespace and cr/lf */ +static parse_buffer *buffer_skip_whitespace(parse_buffer * const buffer) +{ + if ((buffer == NULL) || (buffer->content == NULL)) + { + return NULL; + } + + if (cannot_access_at_index(buffer, 0)) + { + return buffer; + } + + while (can_access_at_index(buffer, 0) && (buffer_at_offset(buffer)[0] <= 32)) + { + buffer->offset++; + } + + if (buffer->offset == buffer->length) + { + buffer->offset--; + } + + return buffer; +} + +/* skip the UTF-8 BOM (byte order mark) if it is at the beginning of a buffer */ +static parse_buffer *skip_utf8_bom(parse_buffer * const buffer) +{ + if ((buffer == NULL) || (buffer->content == NULL) || (buffer->offset != 0)) + { + return NULL; + } + + if (can_access_at_index(buffer, 4) && (strncmp((const char*)buffer_at_offset(buffer), "\xEF\xBB\xBF", 3) == 0)) + { + buffer->offset += 3; + } + + return buffer; +} + +CJSON_PUBLIC(cJSON *) cJSON_ParseWithOpts(const char *value, const char **return_parse_end, cJSON_bool require_null_terminated) +{ + size_t buffer_length; + + if (NULL == value) + { + return NULL; + } + + /* Adding null character size due to require_null_terminated. */ + buffer_length = strlen(value) + sizeof(""); + + return cJSON_ParseWithLengthOpts(value, buffer_length, return_parse_end, require_null_terminated); +} + +/* Parse an object - create a new root, and populate. */ +CJSON_PUBLIC(cJSON *) cJSON_ParseWithLengthOpts(const char *value, size_t buffer_length, const char **return_parse_end, cJSON_bool require_null_terminated) +{ + parse_buffer buffer = { 0, 0, 0, 0, { 0, 0, 0 } }; + cJSON *item = NULL; + + /* reset error position */ + global_error.json = NULL; + global_error.position = 0; + + if (value == NULL || 0 == buffer_length) + { + goto fail; + } + + buffer.content = (const unsigned char*)value; + buffer.length = buffer_length; + buffer.offset = 0; + buffer.hooks = global_hooks; + + item = cJSON_New_Item(&global_hooks); + if (item == NULL) /* memory fail */ + { + goto fail; + } + + if (!parse_value(item, buffer_skip_whitespace(skip_utf8_bom(&buffer)))) + { + /* parse failure. ep is set. */ + goto fail; + } + + /* if we require null-terminated JSON without appended garbage, skip and then check for a null terminator */ + if (require_null_terminated) + { + buffer_skip_whitespace(&buffer); + if ((buffer.offset >= buffer.length) || buffer_at_offset(&buffer)[0] != '\0') + { + goto fail; + } + } + if (return_parse_end) + { + *return_parse_end = (const char*)buffer_at_offset(&buffer); + } + + return item; + +fail: + if (item != NULL) + { + cJSON_Delete(item); + } + + if (value != NULL) + { + error local_error; + local_error.json = (const unsigned char*)value; + local_error.position = 0; + + if (buffer.offset < buffer.length) + { + local_error.position = buffer.offset; + } + else if (buffer.length > 0) + { + local_error.position = buffer.length - 1; + } + + if (return_parse_end != NULL) + { + *return_parse_end = (const char*)local_error.json + local_error.position; + } + + global_error = local_error; + } + + return NULL; +} + +/* Default options for cJSON_Parse */ +CJSON_PUBLIC(cJSON *) cJSON_Parse(const char *value) +{ + return cJSON_ParseWithOpts(value, 0, 0); +} + +CJSON_PUBLIC(cJSON *) cJSON_ParseWithLength(const char *value, size_t buffer_length) +{ + return cJSON_ParseWithLengthOpts(value, buffer_length, 0, 0); +} + +#define cjson_min(a, b) (((a) < (b)) ? (a) : (b)) + +static unsigned char *print(const cJSON * const item, cJSON_bool format, const internal_hooks * const hooks) +{ + static const size_t default_buffer_size = 256; + printbuffer buffer[1]; + unsigned char *printed = NULL; + + memset(buffer, 0, sizeof(buffer)); + + /* create buffer */ + buffer->buffer = (unsigned char*) hooks->allocate(default_buffer_size); + buffer->length = default_buffer_size; + buffer->format = format; + buffer->hooks = *hooks; + if (buffer->buffer == NULL) + { + goto fail; + } + + /* print the value */ + if (!print_value(item, buffer)) + { + goto fail; + } + update_offset(buffer); + + /* check if reallocate is available */ + if (hooks->reallocate != NULL) + { + printed = (unsigned char*) hooks->reallocate(buffer->buffer, buffer->offset + 1); + if (printed == NULL) { + goto fail; + } + buffer->buffer = NULL; + } + else /* otherwise copy the JSON over to a new buffer */ + { + printed = (unsigned char*) hooks->allocate(buffer->offset + 1); + if (printed == NULL) + { + goto fail; + } + memcpy(printed, buffer->buffer, cjson_min(buffer->length, buffer->offset + 1)); + printed[buffer->offset] = '\0'; /* just to be sure */ + + /* free the buffer */ + hooks->deallocate(buffer->buffer); + buffer->buffer = NULL; + } + + return printed; + +fail: + if (buffer->buffer != NULL) + { + hooks->deallocate(buffer->buffer); + buffer->buffer = NULL; + } + + if (printed != NULL) + { + hooks->deallocate(printed); + printed = NULL; + } + + return NULL; +} + +/* Render a cJSON item/entity/structure to text. */ +CJSON_PUBLIC(char *) cJSON_Print(const cJSON *item) +{ + return (char*)print(item, true, &global_hooks); +} + +CJSON_PUBLIC(char *) cJSON_PrintUnformatted(const cJSON *item) +{ + return (char*)print(item, false, &global_hooks); +} + +CJSON_PUBLIC(char *) cJSON_PrintBuffered(const cJSON *item, int prebuffer, cJSON_bool fmt) +{ + printbuffer p = { 0, 0, 0, 0, 0, 0, { 0, 0, 0 } }; + + if (prebuffer < 0) + { + return NULL; + } + + p.buffer = (unsigned char*)global_hooks.allocate((size_t)prebuffer); + if (!p.buffer) + { + return NULL; + } + + p.length = (size_t)prebuffer; + p.offset = 0; + p.noalloc = false; + p.format = fmt; + p.hooks = global_hooks; + + if (!print_value(item, &p)) + { + global_hooks.deallocate(p.buffer); + p.buffer = NULL; + return NULL; + } + + return (char*)p.buffer; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_PrintPreallocated(cJSON *item, char *buffer, const int length, const cJSON_bool format) +{ + printbuffer p = { 0, 0, 0, 0, 0, 0, { 0, 0, 0 } }; + + if ((length < 0) || (buffer == NULL)) + { + return false; + } + + p.buffer = (unsigned char*)buffer; + p.length = (size_t)length; + p.offset = 0; + p.noalloc = true; + p.format = format; + p.hooks = global_hooks; + + return print_value(item, &p); +} + +/* Parser core - when encountering text, process appropriately. */ +static cJSON_bool parse_value(cJSON * const item, parse_buffer * const input_buffer) +{ + if ((input_buffer == NULL) || (input_buffer->content == NULL)) + { + return false; /* no input */ + } + + /* parse the different types of values */ + /* null */ + if (can_read(input_buffer, 4) && (strncmp((const char*)buffer_at_offset(input_buffer), "null", 4) == 0)) + { + item->type = cJSON_NULL; + input_buffer->offset += 4; + return true; + } + /* false */ + if (can_read(input_buffer, 5) && (strncmp((const char*)buffer_at_offset(input_buffer), "false", 5) == 0)) + { + item->type = cJSON_False; + input_buffer->offset += 5; + return true; + } + /* true */ + if (can_read(input_buffer, 4) && (strncmp((const char*)buffer_at_offset(input_buffer), "true", 4) == 0)) + { + item->type = cJSON_True; + item->valueint = 1; + input_buffer->offset += 4; + return true; + } + /* string */ + if (can_access_at_index(input_buffer, 0) && (buffer_at_offset(input_buffer)[0] == '\"')) + { + return parse_string(item, input_buffer); + } + /* number */ + if (can_access_at_index(input_buffer, 0) && ((buffer_at_offset(input_buffer)[0] == '-') || ((buffer_at_offset(input_buffer)[0] >= '0') && (buffer_at_offset(input_buffer)[0] <= '9')))) + { + return parse_number(item, input_buffer); + } + /* array */ + if (can_access_at_index(input_buffer, 0) && (buffer_at_offset(input_buffer)[0] == '[')) + { + return parse_array(item, input_buffer); + } + /* object */ + if (can_access_at_index(input_buffer, 0) && (buffer_at_offset(input_buffer)[0] == '{')) + { + return parse_object(item, input_buffer); + } + + return false; +} + +/* Render a value to text. */ +static cJSON_bool print_value(const cJSON * const item, printbuffer * const output_buffer) +{ + unsigned char *output = NULL; + + if ((item == NULL) || (output_buffer == NULL)) + { + return false; + } + + switch ((item->type) & 0xFF) + { + case cJSON_NULL: + output = ensure(output_buffer, 5); + if (output == NULL) + { + return false; + } + strcpy((char*)output, "null"); + return true; + + case cJSON_False: + output = ensure(output_buffer, 6); + if (output == NULL) + { + return false; + } + strcpy((char*)output, "false"); + return true; + + case cJSON_True: + output = ensure(output_buffer, 5); + if (output == NULL) + { + return false; + } + strcpy((char*)output, "true"); + return true; + + case cJSON_Number: + return print_number(item, output_buffer); + + case cJSON_Raw: + { + size_t raw_length = 0; + if (item->valuestring == NULL) + { + return false; + } + + raw_length = strlen(item->valuestring) + sizeof(""); + output = ensure(output_buffer, raw_length); + if (output == NULL) + { + return false; + } + memcpy(output, item->valuestring, raw_length); + return true; + } + + case cJSON_String: + return print_string(item, output_buffer); + + case cJSON_Array: + return print_array(item, output_buffer); + + case cJSON_Object: + return print_object(item, output_buffer); + + default: + return false; + } +} + +/* Build an array from input text. */ +static cJSON_bool parse_array(cJSON * const item, parse_buffer * const input_buffer) +{ + cJSON *head = NULL; /* head of the linked list */ + cJSON *current_item = NULL; + + if (input_buffer->depth >= CJSON_NESTING_LIMIT) + { + return false; /* to deeply nested */ + } + input_buffer->depth++; + + if (buffer_at_offset(input_buffer)[0] != '[') + { + /* not an array */ + goto fail; + } + + input_buffer->offset++; + buffer_skip_whitespace(input_buffer); + if (can_access_at_index(input_buffer, 0) && (buffer_at_offset(input_buffer)[0] == ']')) + { + /* empty array */ + goto success; + } + + /* check if we skipped to the end of the buffer */ + if (cannot_access_at_index(input_buffer, 0)) + { + input_buffer->offset--; + goto fail; + } + + /* step back to character in front of the first element */ + input_buffer->offset--; + /* loop through the comma separated array elements */ + do + { + /* allocate next item */ + cJSON *new_item = cJSON_New_Item(&(input_buffer->hooks)); + if (new_item == NULL) + { + goto fail; /* allocation failure */ + } + + /* attach next item to list */ + if (head == NULL) + { + /* start the linked list */ + current_item = head = new_item; + } + else + { + /* add to the end and advance */ + current_item->next = new_item; + new_item->prev = current_item; + current_item = new_item; + } + + /* parse next value */ + input_buffer->offset++; + buffer_skip_whitespace(input_buffer); + if (!parse_value(current_item, input_buffer)) + { + goto fail; /* failed to parse value */ + } + buffer_skip_whitespace(input_buffer); + } + while (can_access_at_index(input_buffer, 0) && (buffer_at_offset(input_buffer)[0] == ',')); + + if (cannot_access_at_index(input_buffer, 0) || buffer_at_offset(input_buffer)[0] != ']') + { + goto fail; /* expected end of array */ + } + +success: + input_buffer->depth--; + + if (head != NULL) { + head->prev = current_item; + } + + item->type = cJSON_Array; + item->child = head; + + input_buffer->offset++; + + return true; + +fail: + if (head != NULL) + { + cJSON_Delete(head); + } + + return false; +} + +/* Render an array to text */ +static cJSON_bool print_array(const cJSON * const item, printbuffer * const output_buffer) +{ + unsigned char *output_pointer = NULL; + size_t length = 0; + cJSON *current_element = item->child; + + if (output_buffer == NULL) + { + return false; + } + + /* Compose the output array. */ + /* opening square bracket */ + output_pointer = ensure(output_buffer, 1); + if (output_pointer == NULL) + { + return false; + } + + *output_pointer = '['; + output_buffer->offset++; + output_buffer->depth++; + + while (current_element != NULL) + { + if (!print_value(current_element, output_buffer)) + { + return false; + } + update_offset(output_buffer); + if (current_element->next) + { + length = (size_t) (output_buffer->format ? 2 : 1); + output_pointer = ensure(output_buffer, length + 1); + if (output_pointer == NULL) + { + return false; + } + *output_pointer++ = ','; + if(output_buffer->format) + { + *output_pointer++ = ' '; + } + *output_pointer = '\0'; + output_buffer->offset += length; + } + current_element = current_element->next; + } + + output_pointer = ensure(output_buffer, 2); + if (output_pointer == NULL) + { + return false; + } + *output_pointer++ = ']'; + *output_pointer = '\0'; + output_buffer->depth--; + + return true; +} + +/* Build an object from the text. */ +static cJSON_bool parse_object(cJSON * const item, parse_buffer * const input_buffer) +{ + cJSON *head = NULL; /* linked list head */ + cJSON *current_item = NULL; + + if (input_buffer->depth >= CJSON_NESTING_LIMIT) + { + return false; /* to deeply nested */ + } + input_buffer->depth++; + + if (cannot_access_at_index(input_buffer, 0) || (buffer_at_offset(input_buffer)[0] != '{')) + { + goto fail; /* not an object */ + } + + input_buffer->offset++; + buffer_skip_whitespace(input_buffer); + if (can_access_at_index(input_buffer, 0) && (buffer_at_offset(input_buffer)[0] == '}')) + { + goto success; /* empty object */ + } + + /* check if we skipped to the end of the buffer */ + if (cannot_access_at_index(input_buffer, 0)) + { + input_buffer->offset--; + goto fail; + } + + /* step back to character in front of the first element */ + input_buffer->offset--; + /* loop through the comma separated array elements */ + do + { + /* allocate next item */ + cJSON *new_item = cJSON_New_Item(&(input_buffer->hooks)); + if (new_item == NULL) + { + goto fail; /* allocation failure */ + } + + /* attach next item to list */ + if (head == NULL) + { + /* start the linked list */ + current_item = head = new_item; + } + else + { + /* add to the end and advance */ + current_item->next = new_item; + new_item->prev = current_item; + current_item = new_item; + } + + if (cannot_access_at_index(input_buffer, 1)) + { + goto fail; /* nothing comes after the comma */ + } + + /* parse the name of the child */ + input_buffer->offset++; + buffer_skip_whitespace(input_buffer); + if (!parse_string(current_item, input_buffer)) + { + goto fail; /* failed to parse name */ + } + buffer_skip_whitespace(input_buffer); + + /* swap valuestring and string, because we parsed the name */ + current_item->string = current_item->valuestring; + current_item->valuestring = NULL; + + if (cannot_access_at_index(input_buffer, 0) || (buffer_at_offset(input_buffer)[0] != ':')) + { + goto fail; /* invalid object */ + } + + /* parse the value */ + input_buffer->offset++; + buffer_skip_whitespace(input_buffer); + if (!parse_value(current_item, input_buffer)) + { + goto fail; /* failed to parse value */ + } + buffer_skip_whitespace(input_buffer); + } + while (can_access_at_index(input_buffer, 0) && (buffer_at_offset(input_buffer)[0] == ',')); + + if (cannot_access_at_index(input_buffer, 0) || (buffer_at_offset(input_buffer)[0] != '}')) + { + goto fail; /* expected end of object */ + } + +success: + input_buffer->depth--; + + if (head != NULL) { + head->prev = current_item; + } + + item->type = cJSON_Object; + item->child = head; + + input_buffer->offset++; + return true; + +fail: + if (head != NULL) + { + cJSON_Delete(head); + } + + return false; +} + +/* Render an object to text. */ +static cJSON_bool print_object(const cJSON * const item, printbuffer * const output_buffer) +{ + unsigned char *output_pointer = NULL; + size_t length = 0; + cJSON *current_item = item->child; + + if (output_buffer == NULL) + { + return false; + } + + /* Compose the output: */ + length = (size_t) (output_buffer->format ? 2 : 1); /* fmt: {\n */ + output_pointer = ensure(output_buffer, length + 1); + if (output_pointer == NULL) + { + return false; + } + + *output_pointer++ = '{'; + output_buffer->depth++; + if (output_buffer->format) + { + *output_pointer++ = '\n'; + } + output_buffer->offset += length; + + while (current_item) + { + if (output_buffer->format) + { + size_t i; + output_pointer = ensure(output_buffer, output_buffer->depth); + if (output_pointer == NULL) + { + return false; + } + for (i = 0; i < output_buffer->depth; i++) + { + *output_pointer++ = '\t'; + } + output_buffer->offset += output_buffer->depth; + } + + /* print key */ + if (!print_string_ptr((unsigned char*)current_item->string, output_buffer)) + { + return false; + } + update_offset(output_buffer); + + length = (size_t) (output_buffer->format ? 2 : 1); + output_pointer = ensure(output_buffer, length); + if (output_pointer == NULL) + { + return false; + } + *output_pointer++ = ':'; + if (output_buffer->format) + { + *output_pointer++ = '\t'; + } + output_buffer->offset += length; + + /* print value */ + if (!print_value(current_item, output_buffer)) + { + return false; + } + update_offset(output_buffer); + + /* print comma if not last */ + length = ((size_t)(output_buffer->format ? 1 : 0) + (size_t)(current_item->next ? 1 : 0)); + output_pointer = ensure(output_buffer, length + 1); + if (output_pointer == NULL) + { + return false; + } + if (current_item->next) + { + *output_pointer++ = ','; + } + + if (output_buffer->format) + { + *output_pointer++ = '\n'; + } + *output_pointer = '\0'; + output_buffer->offset += length; + + current_item = current_item->next; + } + + output_pointer = ensure(output_buffer, output_buffer->format ? (output_buffer->depth + 1) : 2); + if (output_pointer == NULL) + { + return false; + } + if (output_buffer->format) + { + size_t i; + for (i = 0; i < (output_buffer->depth - 1); i++) + { + *output_pointer++ = '\t'; + } + } + *output_pointer++ = '}'; + *output_pointer = '\0'; + output_buffer->depth--; + + return true; +} + +/* Get Array size/item / object item. */ +CJSON_PUBLIC(int) cJSON_GetArraySize(const cJSON *array) +{ + cJSON *child = NULL; + size_t size = 0; + + if (array == NULL) + { + return 0; + } + + child = array->child; + + while(child != NULL) + { + size++; + child = child->next; + } + + /* FIXME: Can overflow here. Cannot be fixed without breaking the API */ + + return (int)size; +} + +static cJSON* get_array_item(const cJSON *array, size_t index) +{ + cJSON *current_child = NULL; + + if (array == NULL) + { + return NULL; + } + + current_child = array->child; + while ((current_child != NULL) && (index > 0)) + { + index--; + current_child = current_child->next; + } + + return current_child; +} + +CJSON_PUBLIC(cJSON *) cJSON_GetArrayItem(const cJSON *array, int index) +{ + if (index < 0) + { + return NULL; + } + + return get_array_item(array, (size_t)index); +} + +static cJSON *get_object_item(const cJSON * const object, const char * const name, const cJSON_bool case_sensitive) +{ + cJSON *current_element = NULL; + + if ((object == NULL) || (name == NULL)) + { + return NULL; + } + + current_element = object->child; + if (case_sensitive) + { + while ((current_element != NULL) && (current_element->string != NULL) && (strcmp(name, current_element->string) != 0)) + { + current_element = current_element->next; + } + } + else + { + while ((current_element != NULL) && (case_insensitive_strcmp((const unsigned char*)name, (const unsigned char*)(current_element->string)) != 0)) + { + current_element = current_element->next; + } + } + + if ((current_element == NULL) || (current_element->string == NULL)) { + return NULL; + } + + return current_element; +} + +CJSON_PUBLIC(cJSON *) cJSON_GetObjectItem(const cJSON * const object, const char * const string) +{ + return get_object_item(object, string, false); +} + +CJSON_PUBLIC(cJSON *) cJSON_GetObjectItemCaseSensitive(const cJSON * const object, const char * const string) +{ + return get_object_item(object, string, true); +} + +CJSON_PUBLIC(cJSON_bool) cJSON_HasObjectItem(const cJSON *object, const char *string) +{ + return cJSON_GetObjectItem(object, string) ? 1 : 0; +} + +/* Utility for array list handling. */ +static void suffix_object(cJSON *prev, cJSON *item) +{ + prev->next = item; + item->prev = prev; +} + +/* Utility for handling references. */ +static cJSON *create_reference(const cJSON *item, const internal_hooks * const hooks) +{ + cJSON *reference = NULL; + if (item == NULL) + { + return NULL; + } + + reference = cJSON_New_Item(hooks); + if (reference == NULL) + { + return NULL; + } + + memcpy(reference, item, sizeof(cJSON)); + reference->string = NULL; + reference->type |= cJSON_IsReference; + reference->next = reference->prev = NULL; + return reference; +} + +static cJSON_bool add_item_to_array(cJSON *array, cJSON *item) +{ + cJSON *child = NULL; + + if ((item == NULL) || (array == NULL) || (array == item)) + { + return false; + } + + child = array->child; + /* + * To find the last item in array quickly, we use prev in array + */ + if (child == NULL) + { + /* list is empty, start new one */ + array->child = item; + item->prev = item; + item->next = NULL; + } + else + { + /* append to the end */ + if (child->prev) + { + suffix_object(child->prev, item); + array->child->prev = item; + } + } + + return true; +} + +/* Add item to array/object. */ +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemToArray(cJSON *array, cJSON *item) +{ + return add_item_to_array(array, item); +} + +#if defined(__clang__) || (defined(__GNUC__) && ((__GNUC__ > 4) || ((__GNUC__ == 4) && (__GNUC_MINOR__ > 5)))) + #pragma GCC diagnostic push +#endif +#ifdef __GNUC__ +#pragma GCC diagnostic ignored "-Wcast-qual" +#endif +/* helper function to cast away const */ +static void* cast_away_const(const void* string) +{ + return (void*)string; +} +#if defined(__clang__) || (defined(__GNUC__) && ((__GNUC__ > 4) || ((__GNUC__ == 4) && (__GNUC_MINOR__ > 5)))) + #pragma GCC diagnostic pop +#endif + + +static cJSON_bool add_item_to_object(cJSON * const object, const char * const string, cJSON * const item, const internal_hooks * const hooks, const cJSON_bool constant_key) +{ + char *new_key = NULL; + int new_type = cJSON_Invalid; + + if ((object == NULL) || (string == NULL) || (item == NULL) || (object == item)) + { + return false; + } + + if (constant_key) + { + new_key = (char*)cast_away_const(string); + new_type = item->type | cJSON_StringIsConst; + } + else + { + new_key = (char*)cJSON_strdup((const unsigned char*)string, hooks); + if (new_key == NULL) + { + return false; + } + + new_type = item->type & ~cJSON_StringIsConst; + } + + if (!(item->type & cJSON_StringIsConst) && (item->string != NULL)) + { + hooks->deallocate(item->string); + } + + item->string = new_key; + item->type = new_type; + + return add_item_to_array(object, item); +} + +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemToObject(cJSON *object, const char *string, cJSON *item) +{ + return add_item_to_object(object, string, item, &global_hooks, false); +} + +/* Add an item to an object with constant string as key */ +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemToObjectCS(cJSON *object, const char *string, cJSON *item) +{ + return add_item_to_object(object, string, item, &global_hooks, true); +} + +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemReferenceToArray(cJSON *array, cJSON *item) +{ + if (array == NULL) + { + return false; + } + + return add_item_to_array(array, create_reference(item, &global_hooks)); +} + +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemReferenceToObject(cJSON *object, const char *string, cJSON *item) +{ + if ((object == NULL) || (string == NULL)) + { + return false; + } + + return add_item_to_object(object, string, create_reference(item, &global_hooks), &global_hooks, false); +} + +CJSON_PUBLIC(cJSON*) cJSON_AddNullToObject(cJSON * const object, const char * const name) +{ + cJSON *null = cJSON_CreateNull(); + if (add_item_to_object(object, name, null, &global_hooks, false)) + { + return null; + } + + cJSON_Delete(null); + return NULL; +} + +CJSON_PUBLIC(cJSON*) cJSON_AddTrueToObject(cJSON * const object, const char * const name) +{ + cJSON *true_item = cJSON_CreateTrue(); + if (add_item_to_object(object, name, true_item, &global_hooks, false)) + { + return true_item; + } + + cJSON_Delete(true_item); + return NULL; +} + +CJSON_PUBLIC(cJSON*) cJSON_AddFalseToObject(cJSON * const object, const char * const name) +{ + cJSON *false_item = cJSON_CreateFalse(); + if (add_item_to_object(object, name, false_item, &global_hooks, false)) + { + return false_item; + } + + cJSON_Delete(false_item); + return NULL; +} + +CJSON_PUBLIC(cJSON*) cJSON_AddBoolToObject(cJSON * const object, const char * const name, const cJSON_bool boolean) +{ + cJSON *bool_item = cJSON_CreateBool(boolean); + if (add_item_to_object(object, name, bool_item, &global_hooks, false)) + { + return bool_item; + } + + cJSON_Delete(bool_item); + return NULL; +} + +CJSON_PUBLIC(cJSON*) cJSON_AddNumberToObject(cJSON * const object, const char * const name, const double number) +{ + cJSON *number_item = cJSON_CreateNumber(number); + if (add_item_to_object(object, name, number_item, &global_hooks, false)) + { + return number_item; + } + + cJSON_Delete(number_item); + return NULL; +} + +CJSON_PUBLIC(cJSON*) cJSON_AddStringToObject(cJSON * const object, const char * const name, const char * const string) +{ + cJSON *string_item = cJSON_CreateString(string); + if (add_item_to_object(object, name, string_item, &global_hooks, false)) + { + return string_item; + } + + cJSON_Delete(string_item); + return NULL; +} + +CJSON_PUBLIC(cJSON*) cJSON_AddRawToObject(cJSON * const object, const char * const name, const char * const raw) +{ + cJSON *raw_item = cJSON_CreateRaw(raw); + if (add_item_to_object(object, name, raw_item, &global_hooks, false)) + { + return raw_item; + } + + cJSON_Delete(raw_item); + return NULL; +} + +CJSON_PUBLIC(cJSON*) cJSON_AddObjectToObject(cJSON * const object, const char * const name) +{ + cJSON *object_item = cJSON_CreateObject(); + if (add_item_to_object(object, name, object_item, &global_hooks, false)) + { + return object_item; + } + + cJSON_Delete(object_item); + return NULL; +} + +CJSON_PUBLIC(cJSON*) cJSON_AddArrayToObject(cJSON * const object, const char * const name) +{ + cJSON *array = cJSON_CreateArray(); + if (add_item_to_object(object, name, array, &global_hooks, false)) + { + return array; + } + + cJSON_Delete(array); + return NULL; +} + +CJSON_PUBLIC(cJSON *) cJSON_DetachItemViaPointer(cJSON *parent, cJSON * const item) +{ + if ((parent == NULL) || (item == NULL) || (item != parent->child && item->prev == NULL)) + { + return NULL; + } + + if (item != parent->child) + { + /* not the first element */ + item->prev->next = item->next; + } + if (item->next != NULL) + { + /* not the last element */ + item->next->prev = item->prev; + } + + if (item == parent->child) + { + /* first element */ + parent->child = item->next; + } + else if (item->next == NULL) + { + /* last element */ + parent->child->prev = item->prev; + } + + /* make sure the detached item doesn't point anywhere anymore */ + item->prev = NULL; + item->next = NULL; + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_DetachItemFromArray(cJSON *array, int which) +{ + if (which < 0) + { + return NULL; + } + + return cJSON_DetachItemViaPointer(array, get_array_item(array, (size_t)which)); +} + +CJSON_PUBLIC(void) cJSON_DeleteItemFromArray(cJSON *array, int which) +{ + cJSON_Delete(cJSON_DetachItemFromArray(array, which)); +} + +CJSON_PUBLIC(cJSON *) cJSON_DetachItemFromObject(cJSON *object, const char *string) +{ + cJSON *to_detach = cJSON_GetObjectItem(object, string); + + return cJSON_DetachItemViaPointer(object, to_detach); +} + +CJSON_PUBLIC(cJSON *) cJSON_DetachItemFromObjectCaseSensitive(cJSON *object, const char *string) +{ + cJSON *to_detach = cJSON_GetObjectItemCaseSensitive(object, string); + + return cJSON_DetachItemViaPointer(object, to_detach); +} + +CJSON_PUBLIC(void) cJSON_DeleteItemFromObject(cJSON *object, const char *string) +{ + cJSON_Delete(cJSON_DetachItemFromObject(object, string)); +} + +CJSON_PUBLIC(void) cJSON_DeleteItemFromObjectCaseSensitive(cJSON *object, const char *string) +{ + cJSON_Delete(cJSON_DetachItemFromObjectCaseSensitive(object, string)); +} + +/* Replace array/object items with new ones. */ +CJSON_PUBLIC(cJSON_bool) cJSON_InsertItemInArray(cJSON *array, int which, cJSON *newitem) +{ + cJSON *after_inserted = NULL; + + if (which < 0 || newitem == NULL) + { + return false; + } + + after_inserted = get_array_item(array, (size_t)which); + if (after_inserted == NULL) + { + return add_item_to_array(array, newitem); + } + + if (after_inserted != array->child && after_inserted->prev == NULL) { + /* return false if after_inserted is a corrupted array item */ + return false; + } + + newitem->next = after_inserted; + newitem->prev = after_inserted->prev; + after_inserted->prev = newitem; + if (after_inserted == array->child) + { + array->child = newitem; + } + else + { + newitem->prev->next = newitem; + } + return true; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_ReplaceItemViaPointer(cJSON * const parent, cJSON * const item, cJSON * replacement) +{ + if ((parent == NULL) || (parent->child == NULL) || (replacement == NULL) || (item == NULL)) + { + return false; + } + + if (replacement == item) + { + return true; + } + + replacement->next = item->next; + replacement->prev = item->prev; + + if (replacement->next != NULL) + { + replacement->next->prev = replacement; + } + if (parent->child == item) + { + if (parent->child->prev == parent->child) + { + replacement->prev = replacement; + } + parent->child = replacement; + } + else + { /* + * To find the last item in array quickly, we use prev in array. + * We can't modify the last item's next pointer where this item was the parent's child + */ + if (replacement->prev != NULL) + { + replacement->prev->next = replacement; + } + if (replacement->next == NULL) + { + parent->child->prev = replacement; + } + } + + item->next = NULL; + item->prev = NULL; + cJSON_Delete(item); + + return true; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_ReplaceItemInArray(cJSON *array, int which, cJSON *newitem) +{ + if (which < 0) + { + return false; + } + + return cJSON_ReplaceItemViaPointer(array, get_array_item(array, (size_t)which), newitem); +} + +static cJSON_bool replace_item_in_object(cJSON *object, const char *string, cJSON *replacement, cJSON_bool case_sensitive) +{ + if ((replacement == NULL) || (string == NULL)) + { + return false; + } + + /* replace the name in the replacement */ + if (!(replacement->type & cJSON_StringIsConst) && (replacement->string != NULL)) + { + cJSON_free(replacement->string); + } + replacement->string = (char*)cJSON_strdup((const unsigned char*)string, &global_hooks); + if (replacement->string == NULL) + { + return false; + } + + replacement->type &= ~cJSON_StringIsConst; + + return cJSON_ReplaceItemViaPointer(object, get_object_item(object, string, case_sensitive), replacement); +} + +CJSON_PUBLIC(cJSON_bool) cJSON_ReplaceItemInObject(cJSON *object, const char *string, cJSON *newitem) +{ + return replace_item_in_object(object, string, newitem, false); +} + +CJSON_PUBLIC(cJSON_bool) cJSON_ReplaceItemInObjectCaseSensitive(cJSON *object, const char *string, cJSON *newitem) +{ + return replace_item_in_object(object, string, newitem, true); +} + +/* Create basic types: */ +CJSON_PUBLIC(cJSON *) cJSON_CreateNull(void) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if(item) + { + item->type = cJSON_NULL; + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateTrue(void) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if(item) + { + item->type = cJSON_True; + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateFalse(void) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if(item) + { + item->type = cJSON_False; + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateBool(cJSON_bool boolean) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if(item) + { + item->type = boolean ? cJSON_True : cJSON_False; + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateNumber(double num) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if(item) + { + item->type = cJSON_Number; + item->valuedouble = num; + + /* use saturation in case of overflow */ + if (num >= INT_MAX) + { + item->valueint = INT_MAX; + } + else if (num <= (double)INT_MIN) + { + item->valueint = INT_MIN; + } + else + { + item->valueint = (int)num; + } + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateString(const char *string) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if(item) + { + item->type = cJSON_String; + item->valuestring = (char*)cJSON_strdup((const unsigned char*)string, &global_hooks); + if(!item->valuestring) + { + cJSON_Delete(item); + return NULL; + } + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateStringReference(const char *string) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if (item != NULL) + { + item->type = cJSON_String | cJSON_IsReference; + item->valuestring = (char*)cast_away_const(string); + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateObjectReference(const cJSON *child) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if (item != NULL) { + item->type = cJSON_Object | cJSON_IsReference; + item->child = (cJSON*)cast_away_const(child); + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateArrayReference(const cJSON *child) { + cJSON *item = cJSON_New_Item(&global_hooks); + if (item != NULL) { + item->type = cJSON_Array | cJSON_IsReference; + item->child = (cJSON*)cast_away_const(child); + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateRaw(const char *raw) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if(item) + { + item->type = cJSON_Raw; + item->valuestring = (char*)cJSON_strdup((const unsigned char*)raw, &global_hooks); + if(!item->valuestring) + { + cJSON_Delete(item); + return NULL; + } + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateArray(void) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if(item) + { + item->type=cJSON_Array; + } + + return item; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateObject(void) +{ + cJSON *item = cJSON_New_Item(&global_hooks); + if (item) + { + item->type = cJSON_Object; + } + + return item; +} + +/* Create Arrays: */ +CJSON_PUBLIC(cJSON *) cJSON_CreateIntArray(const int *numbers, int count) +{ + size_t i = 0; + cJSON *n = NULL; + cJSON *p = NULL; + cJSON *a = NULL; + + if ((count < 0) || (numbers == NULL)) + { + return NULL; + } + + a = cJSON_CreateArray(); + + for(i = 0; a && (i < (size_t)count); i++) + { + n = cJSON_CreateNumber(numbers[i]); + if (!n) + { + cJSON_Delete(a); + return NULL; + } + if(!i) + { + a->child = n; + } + else + { + suffix_object(p, n); + } + p = n; + } + + if (a && a->child) { + a->child->prev = n; + } + + return a; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateFloatArray(const float *numbers, int count) +{ + size_t i = 0; + cJSON *n = NULL; + cJSON *p = NULL; + cJSON *a = NULL; + + if ((count < 0) || (numbers == NULL)) + { + return NULL; + } + + a = cJSON_CreateArray(); + + for(i = 0; a && (i < (size_t)count); i++) + { + n = cJSON_CreateNumber((double)numbers[i]); + if(!n) + { + cJSON_Delete(a); + return NULL; + } + if(!i) + { + a->child = n; + } + else + { + suffix_object(p, n); + } + p = n; + } + + if (a && a->child) { + a->child->prev = n; + } + + return a; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateDoubleArray(const double *numbers, int count) +{ + size_t i = 0; + cJSON *n = NULL; + cJSON *p = NULL; + cJSON *a = NULL; + + if ((count < 0) || (numbers == NULL)) + { + return NULL; + } + + a = cJSON_CreateArray(); + + for(i = 0; a && (i < (size_t)count); i++) + { + n = cJSON_CreateNumber(numbers[i]); + if(!n) + { + cJSON_Delete(a); + return NULL; + } + if(!i) + { + a->child = n; + } + else + { + suffix_object(p, n); + } + p = n; + } + + if (a && a->child) { + a->child->prev = n; + } + + return a; +} + +CJSON_PUBLIC(cJSON *) cJSON_CreateStringArray(const char *const *strings, int count) +{ + size_t i = 0; + cJSON *n = NULL; + cJSON *p = NULL; + cJSON *a = NULL; + + if ((count < 0) || (strings == NULL)) + { + return NULL; + } + + a = cJSON_CreateArray(); + + for (i = 0; a && (i < (size_t)count); i++) + { + n = cJSON_CreateString(strings[i]); + if(!n) + { + cJSON_Delete(a); + return NULL; + } + if(!i) + { + a->child = n; + } + else + { + suffix_object(p,n); + } + p = n; + } + + if (a && a->child) { + a->child->prev = n; + } + + return a; +} + +/* Duplication */ +cJSON * cJSON_Duplicate_rec(const cJSON *item, size_t depth, cJSON_bool recurse); + +CJSON_PUBLIC(cJSON *) cJSON_Duplicate(const cJSON *item, cJSON_bool recurse) +{ + return cJSON_Duplicate_rec(item, 0, recurse ); +} + +cJSON * cJSON_Duplicate_rec(const cJSON *item, size_t depth, cJSON_bool recurse) +{ + cJSON *newitem = NULL; + cJSON *child = NULL; + cJSON *next = NULL; + cJSON *newchild = NULL; + + /* Bail on bad ptr */ + if (!item) + { + goto fail; + } + /* Create new item */ + newitem = cJSON_New_Item(&global_hooks); + if (!newitem) + { + goto fail; + } + /* Copy over all vars */ + newitem->type = item->type & (~cJSON_IsReference); + newitem->valueint = item->valueint; + newitem->valuedouble = item->valuedouble; + if (item->valuestring) + { + newitem->valuestring = (char*)cJSON_strdup((unsigned char*)item->valuestring, &global_hooks); + if (!newitem->valuestring) + { + goto fail; + } + } + if (item->string) + { + newitem->string = (item->type&cJSON_StringIsConst) ? item->string : (char*)cJSON_strdup((unsigned char*)item->string, &global_hooks); + if (!newitem->string) + { + goto fail; + } + } + /* If non-recursive, then we're done! */ + if (!recurse) + { + return newitem; + } + /* Walk the ->next chain for the child. */ + child = item->child; + while (child != NULL) + { + if(depth >= CJSON_CIRCULAR_LIMIT) { + goto fail; + } + newchild = cJSON_Duplicate_rec(child, depth + 1, true); /* Duplicate (with recurse) each item in the ->next chain */ + if (!newchild) + { + goto fail; + } + if (next != NULL) + { + /* If newitem->child already set, then crosswire ->prev and ->next and move on */ + next->next = newchild; + newchild->prev = next; + next = newchild; + } + else + { + /* Set newitem->child and move to it */ + newitem->child = newchild; + next = newchild; + } + child = child->next; + } + if (newitem && newitem->child) + { + newitem->child->prev = newchild; + } + + return newitem; + +fail: + if (newitem != NULL) + { + cJSON_Delete(newitem); + } + + return NULL; +} + +static void skip_oneline_comment(char **input) +{ + *input += static_strlen("//"); + + for (; (*input)[0] != '\0'; ++(*input)) + { + if ((*input)[0] == '\n') { + *input += static_strlen("\n"); + return; + } + } +} + +static void skip_multiline_comment(char **input) +{ + *input += static_strlen("/*"); + + for (; (*input)[0] != '\0'; ++(*input)) + { + if (((*input)[0] == '*') && ((*input)[1] == '/')) + { + *input += static_strlen("*/"); + return; + } + } +} + +static void minify_string(char **input, char **output) { + (*output)[0] = (*input)[0]; + *input += static_strlen("\""); + *output += static_strlen("\""); + + + for (; (*input)[0] != '\0'; (void)++(*input), ++(*output)) { + (*output)[0] = (*input)[0]; + + if ((*input)[0] == '\"') { + (*output)[0] = '\"'; + *input += static_strlen("\""); + *output += static_strlen("\""); + return; + } else if (((*input)[0] == '\\') && ((*input)[1] == '\"')) { + (*output)[1] = (*input)[1]; + *input += static_strlen("\""); + *output += static_strlen("\""); + } + } +} + +CJSON_PUBLIC(void) cJSON_Minify(char *json) +{ + char *into = json; + + if (json == NULL) + { + return; + } + + while (json[0] != '\0') + { + switch (json[0]) + { + case ' ': + case '\t': + case '\r': + case '\n': + json++; + break; + + case '/': + if (json[1] == '/') + { + skip_oneline_comment(&json); + } + else if (json[1] == '*') + { + skip_multiline_comment(&json); + } else { + json++; + } + break; + + case '\"': + minify_string(&json, (char**)&into); + break; + + default: + into[0] = json[0]; + json++; + into++; + } + } + + /* and null-terminate. */ + *into = '\0'; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_IsInvalid(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xFF) == cJSON_Invalid; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_IsFalse(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xFF) == cJSON_False; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_IsTrue(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xff) == cJSON_True; +} + + +CJSON_PUBLIC(cJSON_bool) cJSON_IsBool(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & (cJSON_True | cJSON_False)) != 0; +} +CJSON_PUBLIC(cJSON_bool) cJSON_IsNull(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xFF) == cJSON_NULL; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_IsNumber(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xFF) == cJSON_Number; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_IsString(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xFF) == cJSON_String; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_IsArray(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xFF) == cJSON_Array; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_IsObject(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xFF) == cJSON_Object; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_IsRaw(const cJSON * const item) +{ + if (item == NULL) + { + return false; + } + + return (item->type & 0xFF) == cJSON_Raw; +} + +CJSON_PUBLIC(cJSON_bool) cJSON_Compare(const cJSON * const a, const cJSON * const b, const cJSON_bool case_sensitive) +{ + if ((a == NULL) || (b == NULL) || ((a->type & 0xFF) != (b->type & 0xFF))) + { + return false; + } + + /* check if type is valid */ + switch (a->type & 0xFF) + { + case cJSON_False: + case cJSON_True: + case cJSON_NULL: + case cJSON_Number: + case cJSON_String: + case cJSON_Raw: + case cJSON_Array: + case cJSON_Object: + break; + + default: + return false; + } + + /* identical objects are equal */ + if (a == b) + { + return true; + } + + switch (a->type & 0xFF) + { + /* in these cases and equal type is enough */ + case cJSON_False: + case cJSON_True: + case cJSON_NULL: + return true; + + case cJSON_Number: + if (compare_double(a->valuedouble, b->valuedouble)) + { + return true; + } + return false; + + case cJSON_String: + case cJSON_Raw: + if ((a->valuestring == NULL) || (b->valuestring == NULL)) + { + return false; + } + if (strcmp(a->valuestring, b->valuestring) == 0) + { + return true; + } + + return false; + + case cJSON_Array: + { + cJSON *a_element = a->child; + cJSON *b_element = b->child; + + for (; (a_element != NULL) && (b_element != NULL);) + { + if (!cJSON_Compare(a_element, b_element, case_sensitive)) + { + return false; + } + + a_element = a_element->next; + b_element = b_element->next; + } + + /* one of the arrays is longer than the other */ + if (a_element != b_element) { + return false; + } + + return true; + } + + case cJSON_Object: + { + cJSON *a_element = NULL; + cJSON *b_element = NULL; + cJSON_ArrayForEach(a_element, a) + { + /* TODO This has O(n^2) runtime, which is horrible! */ + b_element = get_object_item(b, a_element->string, case_sensitive); + if (b_element == NULL) + { + return false; + } + + if (!cJSON_Compare(a_element, b_element, case_sensitive)) + { + return false; + } + } + + /* doing this twice, once on a and b to prevent true comparison if a subset of b + * TODO: Do this the proper way, this is just a fix for now */ + cJSON_ArrayForEach(b_element, b) + { + a_element = get_object_item(a, b_element->string, case_sensitive); + if (a_element == NULL) + { + return false; + } + + if (!cJSON_Compare(b_element, a_element, case_sensitive)) + { + return false; + } + } + + return true; + } + + default: + return false; + } +} + +CJSON_PUBLIC(void *) cJSON_malloc(size_t size) +{ + return global_hooks.allocate(size); +} + +CJSON_PUBLIC(void) cJSON_free(void *object) +{ + global_hooks.deallocate(object); + object = NULL; +} diff --git a/lib/json/cJSON.h b/lib/json/cJSON.h new file mode 100644 index 000000000..37520bbcf --- /dev/null +++ b/lib/json/cJSON.h @@ -0,0 +1,306 @@ +/* + Copyright (c) 2009-2017 Dave Gamble and cJSON contributors + + Permission is hereby granted, free of charge, to any person obtaining a copy + of this software and associated documentation files (the "Software"), to deal + in the Software without restriction, including without limitation the rights + to use, copy, modify, merge, publish, distribute, sublicense, and/or sell + copies of the Software, and to permit persons to whom the Software is + furnished to do so, subject to the following conditions: + + The above copyright notice and this permission notice shall be included in + all copies or substantial portions of the Software. + + THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN + THE SOFTWARE. +*/ + +#ifndef cJSON__h +#define cJSON__h + +#ifdef __cplusplus +extern "C" +{ +#endif + +#if !defined(__WINDOWS__) && (defined(WIN32) || defined(WIN64) || defined(_MSC_VER) || defined(_WIN32)) +#define __WINDOWS__ +#endif + +#ifdef __WINDOWS__ + +/* When compiling for windows, we specify a specific calling convention to avoid issues where we are being called from a project with a different default calling convention. For windows you have 3 define options: + +CJSON_HIDE_SYMBOLS - Define this in the case where you don't want to ever dllexport symbols +CJSON_EXPORT_SYMBOLS - Define this on library build when you want to dllexport symbols (default) +CJSON_IMPORT_SYMBOLS - Define this if you want to dllimport symbol + +For *nix builds that support visibility attribute, you can define similar behavior by + +setting default visibility to hidden by adding +-fvisibility=hidden (for gcc) +or +-xldscope=hidden (for sun cc) +to CFLAGS + +then using the CJSON_API_VISIBILITY flag to "export" the same symbols the way CJSON_EXPORT_SYMBOLS does + +*/ + +#define CJSON_CDECL __cdecl +#define CJSON_STDCALL __stdcall + +/* export symbols by default, this is necessary for copy pasting the C and header file */ +#if !defined(CJSON_HIDE_SYMBOLS) && !defined(CJSON_IMPORT_SYMBOLS) && !defined(CJSON_EXPORT_SYMBOLS) +#define CJSON_EXPORT_SYMBOLS +#endif + +#if defined(CJSON_HIDE_SYMBOLS) +#define CJSON_PUBLIC(type) type CJSON_STDCALL +#elif defined(CJSON_EXPORT_SYMBOLS) +#define CJSON_PUBLIC(type) __declspec(dllexport) type CJSON_STDCALL +#elif defined(CJSON_IMPORT_SYMBOLS) +#define CJSON_PUBLIC(type) __declspec(dllimport) type CJSON_STDCALL +#endif +#else /* !__WINDOWS__ */ +#define CJSON_CDECL +#define CJSON_STDCALL + +#if (defined(__GNUC__) || defined(__SUNPRO_CC) || defined (__SUNPRO_C)) && defined(CJSON_API_VISIBILITY) +#define CJSON_PUBLIC(type) __attribute__((visibility("default"))) type +#else +#define CJSON_PUBLIC(type) type +#endif +#endif + +/* project version */ +#define CJSON_VERSION_MAJOR 1 +#define CJSON_VERSION_MINOR 7 +#define CJSON_VERSION_PATCH 18 + +#include + +/* cJSON Types: */ +#define cJSON_Invalid (0) +#define cJSON_False (1 << 0) +#define cJSON_True (1 << 1) +#define cJSON_NULL (1 << 2) +#define cJSON_Number (1 << 3) +#define cJSON_String (1 << 4) +#define cJSON_Array (1 << 5) +#define cJSON_Object (1 << 6) +#define cJSON_Raw (1 << 7) /* raw json */ + +#define cJSON_IsReference 256 +#define cJSON_StringIsConst 512 + +/* The cJSON structure: */ +typedef struct cJSON +{ + /* next/prev allow you to walk array/object chains. Alternatively, use GetArraySize/GetArrayItem/GetObjectItem */ + struct cJSON *next; + struct cJSON *prev; + /* An array or object item will have a child pointer pointing to a chain of the items in the array/object. */ + struct cJSON *child; + + /* The type of the item, as above. */ + int type; + + /* The item's string, if type==cJSON_String and type == cJSON_Raw */ + char *valuestring; + /* writing to valueint is DEPRECATED, use cJSON_SetNumberValue instead */ + int valueint; + /* The item's number, if type==cJSON_Number */ + double valuedouble; + + /* The item's name string, if this item is the child of, or is in the list of subitems of an object. */ + char *string; +} cJSON; + +typedef struct cJSON_Hooks +{ + /* malloc/free are CDECL on Windows regardless of the default calling convention of the compiler, so ensure the hooks allow passing those functions directly. */ + void *(CJSON_CDECL *malloc_fn)(size_t sz); + void (CJSON_CDECL *free_fn)(void *ptr); +} cJSON_Hooks; + +typedef int cJSON_bool; + +/* Limits how deeply nested arrays/objects can be before cJSON rejects to parse them. + * This is to prevent stack overflows. */ +#ifndef CJSON_NESTING_LIMIT +#define CJSON_NESTING_LIMIT 1000 +#endif + +/* Limits the length of circular references can be before cJSON rejects to parse them. + * This is to prevent stack overflows. */ +#ifndef CJSON_CIRCULAR_LIMIT +#define CJSON_CIRCULAR_LIMIT 10000 +#endif + +/* returns the version of cJSON as a string */ +CJSON_PUBLIC(const char*) cJSON_Version(void); + +/* Supply malloc, realloc and free functions to cJSON */ +CJSON_PUBLIC(void) cJSON_InitHooks(cJSON_Hooks* hooks); + +/* Memory Management: the caller is always responsible to free the results from all variants of cJSON_Parse (with cJSON_Delete) and cJSON_Print (with stdlib free, cJSON_Hooks.free_fn, or cJSON_free as appropriate). The exception is cJSON_PrintPreallocated, where the caller has full responsibility of the buffer. */ +/* Supply a block of JSON, and this returns a cJSON object you can interrogate. */ +CJSON_PUBLIC(cJSON *) cJSON_Parse(const char *value); +CJSON_PUBLIC(cJSON *) cJSON_ParseWithLength(const char *value, size_t buffer_length); +/* ParseWithOpts allows you to require (and check) that the JSON is null terminated, and to retrieve the pointer to the final byte parsed. */ +/* If you supply a ptr in return_parse_end and parsing fails, then return_parse_end will contain a pointer to the error so will match cJSON_GetErrorPtr(). */ +CJSON_PUBLIC(cJSON *) cJSON_ParseWithOpts(const char *value, const char **return_parse_end, cJSON_bool require_null_terminated); +CJSON_PUBLIC(cJSON *) cJSON_ParseWithLengthOpts(const char *value, size_t buffer_length, const char **return_parse_end, cJSON_bool require_null_terminated); + +/* Render a cJSON entity to text for transfer/storage. */ +CJSON_PUBLIC(char *) cJSON_Print(const cJSON *item); +/* Render a cJSON entity to text for transfer/storage without any formatting. */ +CJSON_PUBLIC(char *) cJSON_PrintUnformatted(const cJSON *item); +/* Render a cJSON entity to text using a buffered strategy. prebuffer is a guess at the final size. guessing well reduces reallocation. fmt=0 gives unformatted, =1 gives formatted */ +CJSON_PUBLIC(char *) cJSON_PrintBuffered(const cJSON *item, int prebuffer, cJSON_bool fmt); +/* Render a cJSON entity to text using a buffer already allocated in memory with given length. Returns 1 on success and 0 on failure. */ +/* NOTE: cJSON is not always 100% accurate in estimating how much memory it will use, so to be safe allocate 5 bytes more than you actually need */ +CJSON_PUBLIC(cJSON_bool) cJSON_PrintPreallocated(cJSON *item, char *buffer, const int length, const cJSON_bool format); +/* Delete a cJSON entity and all subentities. */ +CJSON_PUBLIC(void) cJSON_Delete(cJSON *item); + +/* Returns the number of items in an array (or object). */ +CJSON_PUBLIC(int) cJSON_GetArraySize(const cJSON *array); +/* Retrieve item number "index" from array "array". Returns NULL if unsuccessful. */ +CJSON_PUBLIC(cJSON *) cJSON_GetArrayItem(const cJSON *array, int index); +/* Get item "string" from object. Case insensitive. */ +CJSON_PUBLIC(cJSON *) cJSON_GetObjectItem(const cJSON * const object, const char * const string); +CJSON_PUBLIC(cJSON *) cJSON_GetObjectItemCaseSensitive(const cJSON * const object, const char * const string); +CJSON_PUBLIC(cJSON_bool) cJSON_HasObjectItem(const cJSON *object, const char *string); +/* For analysing failed parses. This returns a pointer to the parse error. You'll probably need to look a few chars back to make sense of it. Defined when cJSON_Parse() returns 0. 0 when cJSON_Parse() succeeds. */ +CJSON_PUBLIC(const char *) cJSON_GetErrorPtr(void); + +/* Check item type and return its value */ +CJSON_PUBLIC(char *) cJSON_GetStringValue(const cJSON * const item); +CJSON_PUBLIC(double) cJSON_GetNumberValue(const cJSON * const item); + +/* These functions check the type of an item */ +CJSON_PUBLIC(cJSON_bool) cJSON_IsInvalid(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsFalse(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsTrue(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsBool(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsNull(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsNumber(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsString(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsArray(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsObject(const cJSON * const item); +CJSON_PUBLIC(cJSON_bool) cJSON_IsRaw(const cJSON * const item); + +/* These calls create a cJSON item of the appropriate type. */ +CJSON_PUBLIC(cJSON *) cJSON_CreateNull(void); +CJSON_PUBLIC(cJSON *) cJSON_CreateTrue(void); +CJSON_PUBLIC(cJSON *) cJSON_CreateFalse(void); +CJSON_PUBLIC(cJSON *) cJSON_CreateBool(cJSON_bool boolean); +CJSON_PUBLIC(cJSON *) cJSON_CreateNumber(double num); +CJSON_PUBLIC(cJSON *) cJSON_CreateString(const char *string); +/* raw json */ +CJSON_PUBLIC(cJSON *) cJSON_CreateRaw(const char *raw); +CJSON_PUBLIC(cJSON *) cJSON_CreateArray(void); +CJSON_PUBLIC(cJSON *) cJSON_CreateObject(void); + +/* Create a string where valuestring references a string so + * it will not be freed by cJSON_Delete */ +CJSON_PUBLIC(cJSON *) cJSON_CreateStringReference(const char *string); +/* Create an object/array that only references it's elements so + * they will not be freed by cJSON_Delete */ +CJSON_PUBLIC(cJSON *) cJSON_CreateObjectReference(const cJSON *child); +CJSON_PUBLIC(cJSON *) cJSON_CreateArrayReference(const cJSON *child); + +/* These utilities create an Array of count items. + * The parameter count cannot be greater than the number of elements in the number array, otherwise array access will be out of bounds.*/ +CJSON_PUBLIC(cJSON *) cJSON_CreateIntArray(const int *numbers, int count); +CJSON_PUBLIC(cJSON *) cJSON_CreateFloatArray(const float *numbers, int count); +CJSON_PUBLIC(cJSON *) cJSON_CreateDoubleArray(const double *numbers, int count); +CJSON_PUBLIC(cJSON *) cJSON_CreateStringArray(const char *const *strings, int count); + +/* Append item to the specified array/object. */ +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemToArray(cJSON *array, cJSON *item); +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemToObject(cJSON *object, const char *string, cJSON *item); +/* Use this when string is definitely const (i.e. a literal, or as good as), and will definitely survive the cJSON object. + * WARNING: When this function was used, make sure to always check that (item->type & cJSON_StringIsConst) is zero before + * writing to `item->string` */ +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemToObjectCS(cJSON *object, const char *string, cJSON *item); +/* Append reference to item to the specified array/object. Use this when you want to add an existing cJSON to a new cJSON, but don't want to corrupt your existing cJSON. */ +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemReferenceToArray(cJSON *array, cJSON *item); +CJSON_PUBLIC(cJSON_bool) cJSON_AddItemReferenceToObject(cJSON *object, const char *string, cJSON *item); + +/* Remove/Detach items from Arrays/Objects. */ +CJSON_PUBLIC(cJSON *) cJSON_DetachItemViaPointer(cJSON *parent, cJSON * const item); +CJSON_PUBLIC(cJSON *) cJSON_DetachItemFromArray(cJSON *array, int which); +CJSON_PUBLIC(void) cJSON_DeleteItemFromArray(cJSON *array, int which); +CJSON_PUBLIC(cJSON *) cJSON_DetachItemFromObject(cJSON *object, const char *string); +CJSON_PUBLIC(cJSON *) cJSON_DetachItemFromObjectCaseSensitive(cJSON *object, const char *string); +CJSON_PUBLIC(void) cJSON_DeleteItemFromObject(cJSON *object, const char *string); +CJSON_PUBLIC(void) cJSON_DeleteItemFromObjectCaseSensitive(cJSON *object, const char *string); + +/* Update array items. */ +CJSON_PUBLIC(cJSON_bool) cJSON_InsertItemInArray(cJSON *array, int which, cJSON *newitem); /* Shifts pre-existing items to the right. */ +CJSON_PUBLIC(cJSON_bool) cJSON_ReplaceItemViaPointer(cJSON * const parent, cJSON * const item, cJSON * replacement); +CJSON_PUBLIC(cJSON_bool) cJSON_ReplaceItemInArray(cJSON *array, int which, cJSON *newitem); +CJSON_PUBLIC(cJSON_bool) cJSON_ReplaceItemInObject(cJSON *object,const char *string,cJSON *newitem); +CJSON_PUBLIC(cJSON_bool) cJSON_ReplaceItemInObjectCaseSensitive(cJSON *object,const char *string,cJSON *newitem); + +/* Duplicate a cJSON item */ +CJSON_PUBLIC(cJSON *) cJSON_Duplicate(const cJSON *item, cJSON_bool recurse); +/* Duplicate will create a new, identical cJSON item to the one you pass, in new memory that will + * need to be released. With recurse!=0, it will duplicate any children connected to the item. + * The item->next and ->prev pointers are always zero on return from Duplicate. */ +/* Recursively compare two cJSON items for equality. If either a or b is NULL or invalid, they will be considered unequal. + * case_sensitive determines if object keys are treated case sensitive (1) or case insensitive (0) */ +CJSON_PUBLIC(cJSON_bool) cJSON_Compare(const cJSON * const a, const cJSON * const b, const cJSON_bool case_sensitive); + +/* Minify a strings, remove blank characters(such as ' ', '\t', '\r', '\n') from strings. + * The input pointer json cannot point to a read-only address area, such as a string constant, + * but should point to a readable and writable address area. */ +CJSON_PUBLIC(void) cJSON_Minify(char *json); + +/* Helper functions for creating and adding items to an object at the same time. + * They return the added item or NULL on failure. */ +CJSON_PUBLIC(cJSON*) cJSON_AddNullToObject(cJSON * const object, const char * const name); +CJSON_PUBLIC(cJSON*) cJSON_AddTrueToObject(cJSON * const object, const char * const name); +CJSON_PUBLIC(cJSON*) cJSON_AddFalseToObject(cJSON * const object, const char * const name); +CJSON_PUBLIC(cJSON*) cJSON_AddBoolToObject(cJSON * const object, const char * const name, const cJSON_bool boolean); +CJSON_PUBLIC(cJSON*) cJSON_AddNumberToObject(cJSON * const object, const char * const name, const double number); +CJSON_PUBLIC(cJSON*) cJSON_AddStringToObject(cJSON * const object, const char * const name, const char * const string); +CJSON_PUBLIC(cJSON*) cJSON_AddRawToObject(cJSON * const object, const char * const name, const char * const raw); +CJSON_PUBLIC(cJSON*) cJSON_AddObjectToObject(cJSON * const object, const char * const name); +CJSON_PUBLIC(cJSON*) cJSON_AddArrayToObject(cJSON * const object, const char * const name); + +/* When assigning an integer value, it needs to be propagated to valuedouble too. */ +#define cJSON_SetIntValue(object, number) ((object) ? (object)->valueint = (object)->valuedouble = (number) : (number)) +/* helper for the cJSON_SetNumberValue macro */ +CJSON_PUBLIC(double) cJSON_SetNumberHelper(cJSON *object, double number); +#define cJSON_SetNumberValue(object, number) ((object != NULL) ? cJSON_SetNumberHelper(object, (double)number) : (number)) +/* Change the valuestring of a cJSON_String object, only takes effect when type of object is cJSON_String */ +CJSON_PUBLIC(char*) cJSON_SetValuestring(cJSON *object, const char *valuestring); + +/* If the object is not a boolean type this does nothing and returns cJSON_Invalid else it returns the new type*/ +#define cJSON_SetBoolValue(object, boolValue) ( \ + (object != NULL && ((object)->type & (cJSON_False|cJSON_True))) ? \ + (object)->type=((object)->type &(~(cJSON_False|cJSON_True)))|((boolValue)?cJSON_True:cJSON_False) : \ + cJSON_Invalid\ +) + +/* Macro for iterating over an array or object */ +#define cJSON_ArrayForEach(element, array) for(element = (array != NULL) ? (array)->child : NULL; element != NULL; element = element->next) + +/* malloc/free objects using the malloc/free functions that have been set with cJSON_InitHooks */ +CJSON_PUBLIC(void *) cJSON_malloc(size_t size); +CJSON_PUBLIC(void) cJSON_free(void *object); + +#ifdef __cplusplus +} +#endif + +#endif diff --git a/lib/json/sail_config.c b/lib/json/sail_config.c new file mode 100644 index 000000000..27ce02020 --- /dev/null +++ b/lib/json/sail_config.c @@ -0,0 +1,201 @@ +/****************************************************************************/ +/* Sail */ +/* */ +/* Sail and the Sail architecture models here, comprising all files and */ +/* directories except the ASL-derived Sail code in the aarch64 directory, */ +/* are subject to the BSD two-clause licence below. */ +/* */ +/* The ASL derived parts of the ARMv8.3 specification in */ +/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */ +/* */ +/* Copyright (c) 2024 */ +/* Alasdair Armstrong */ +/* */ +/* All rights reserved. */ +/* */ +/* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous */ +/* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA */ +/* KTF funding, and donations from Arm. This project has received */ +/* funding from the European Research Council (ERC) under the European */ +/* Union’s Horizon 2020 research and innovation programme (grant */ +/* agreement No 789108, ELVER). */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */ +/* and FA8750-10-C-0237 ("CTSRD"). */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/****************************************************************************/ + +#include "sail_config.h" +#include "cJSON.h" + +#ifdef __cplusplus +extern "C" { +#endif + +struct sail_json +{ + cJSON json; +}; + +typedef struct sail_json* sail_config_json; + +static cJSON *sail_config; + +void sail_config_set_file(const char *path) +{ + cJSON_Hooks hooks; + hooks.malloc_fn = &sail_malloc; + hooks.free_fn = &sail_free; + cJSON_InitHooks(&hooks); + + FILE *f = fopen(path, "rb"); + fseek(f, 0, SEEK_END); + long fsize = ftell(f); + fseek(f, 0, SEEK_SET); + + char *buffer = (char *)sail_malloc(fsize + 1); + fread(buffer, fsize, 1, f); + buffer[fsize] = 0; + fclose(f); + + sail_config = cJSON_Parse(buffer); + + if (!sail_config) { + sail_assert(false, "Failed to parse configuration"); + } + + sail_free(buffer); +} + +void sail_config_cleanup(void) +{ + sail_free(sail_config); +} + +void sail_config_get_string(sail_string *str, size_t n, const char *key[]) +{ + cJSON *json = (cJSON *)sail_config; + + sail_free(*str); + + for (int i = 0; i < n; i++) { + if (cJSON_IsObject(json)) { + json = cJSON_GetObjectItemCaseSensitive(json, key[i]); + } else { + sail_assert(false, "Failed to access config item"); + } + } + + if (cJSON_IsString(json)) { + *str = cJSON_GetStringValue(json); + } else { + sail_assert(false, "Expected string value in config"); + } +} + +sail_config_json sail_config_get(size_t n, const char *key[]) +{ + sail_config_json result; + cJSON *json = (cJSON *)sail_config; + + for (int i = 0; i < n; i++) { + if (cJSON_IsObject(json)) { + json = cJSON_GetObjectItemCaseSensitive(json, key[i]); + } else { + sail_assert(false, "Failed to access config item"); + } + } + + return (sail_config_json)json; +} + +bool sail_config_is_object(const sail_config_json config) +{ + return cJSON_IsObject((cJSON *)config); +} + +bool sail_config_object_has_key(const sail_config_json config, const sail_string key) +{ + return cJSON_HasObjectItem((cJSON *)config, key); +} + +sail_config_json sail_config_object_key(const sail_config_json config, const sail_string key) +{ + return (sail_config_json)cJSON_GetObjectItemCaseSensitive((cJSON *)config, key); +} + +bool sail_config_is_string(const sail_config_json config) +{ + return cJSON_IsString((cJSON *)config); +} + +bool sail_config_is_array(const sail_config_json config) +{ + return cJSON_IsArray((cJSON *)config); +} + +bool sail_config_is_bool_array(const sail_config_json config) +{ + if (!sail_config_is_array(config)) { + return false; + } + + int len = cJSON_GetArraySize((cJSON *)config); + + cJSON *value; + cJSON_ArrayForEach(value, ((cJSON*)config)) { + if (!cJSON_IsBool(value)) { + return false; + } + } + + return true; +} + +bool sail_config_is_bool_array_with_size(const sail_config_json config, mach_int expected) +{ + if (!sail_config_is_bool_array(config)) { + return false; + } + + int len = cJSON_GetArraySize((cJSON *)config); + + return (mach_int)len == expected; +} + +void sail_config_unwrap_string(sail_string *str, const sail_config_json config) +{ + *str = cJSON_GetStringValue((cJSON *)config); +} + +void sail_config_unwrap_int(sail_int *n, const sail_config_json config) +{ + char *str = cJSON_GetStringValue((cJSON *)config); + mpz_set_str(*n, str, 10); +} + +void sail_config_unwrap_bits(lbits *bv, const sail_config_json config) +{ + cJSON *json = (cJSON *)config; + + mp_bitcnt_t len = (mp_bitcnt_t)cJSON_GetArraySize(json); + bv->len = len; + mpz_set_ui(*bv->bits, 0); + + mp_bitcnt_t i = 0; + cJSON *bit; + cJSON_ArrayForEach(bit, json) { + if (cJSON_IsTrue(bit)) { + mpz_setbit(*bv->bits, len - i - 1); + } + i++; + } +} + +#ifdef __cplusplus +} +#endif diff --git a/lib/json/sail_config.h b/lib/json/sail_config.h new file mode 100644 index 000000000..fa4b7f6d1 --- /dev/null +++ b/lib/json/sail_config.h @@ -0,0 +1,105 @@ +/****************************************************************************/ +/* Sail */ +/* */ +/* Sail and the Sail architecture models here, comprising all files and */ +/* directories except the ASL-derived Sail code in the aarch64 directory, */ +/* are subject to the BSD two-clause licence below. */ +/* */ +/* The ASL derived parts of the ARMv8.3 specification in */ +/* aarch64/no_vector and aarch64/full are copyright ARM Ltd. */ +/* */ +/* Copyright (c) 2024 */ +/* Alasdair Armstrong */ +/* */ +/* All rights reserved. */ +/* */ +/* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous */ +/* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA */ +/* KTF funding, and donations from Arm. This project has received */ +/* funding from the European Research Council (ERC) under the European */ +/* Union’s Horizon 2020 research and innovation programme (grant */ +/* agreement No 789108, ELVER). */ +/* */ +/* This software was developed by SRI International and the University of */ +/* Cambridge Computer Laboratory (Department of Computer Science and */ +/* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") */ +/* and FA8750-10-C-0237 ("CTSRD"). */ +/* */ +/* SPDX-License-Identifier: BSD-2-Clause */ +/****************************************************************************/ + +#ifndef SAIL_CONFIG_H +#define SAIL_CONFIG_H + +/* + * This file implements the runtime configuration of a Sail model + * using a JSON configuration file. + * + * It abstracts away the particular details of the exact JSON library + * that is being used. + */ + +#include "sail.h" +#include "sail_failure.h" +#include "cJSON.h" + +#ifdef __cplusplus +extern "C" { +#endif + +struct sail_json; + +typedef struct sail_json* sail_config_json; + +/* + * This file sets the runtime JSON config file + */ +void sail_config_set_file(const char *path); + +/* + * Deallocate any memory used by the configuration. + * + * After using this, other functions in this module are no long safe to call. + */ +void sail_config_cleanup(); + +/* + * Extract a string value from the JSON configuration. + */ +void sail_config_get_string(sail_string *str, const size_t n, const_sail_string key[]); + +/* + * For more complex Sail types than just strings, Sail will generate code that will + * destructure the JSON values using the following function calls. + * + * In general, it will test if the JSON is the type it expects, and + * only then access the fields. The behaviour of these functions is + * not guaranteed if the JSON does not have the correct type. + */ + +sail_config_json sail_config_get(const size_t n, const_sail_string key[]); + +bool sail_config_is_object(const sail_config_json config); + +bool sail_config_object_has_key(const sail_config_json config, const sail_string key); + +sail_config_json sail_config_object_key(const sail_config_json config, const sail_string key); + +bool sail_config_is_string(const sail_config_json config); + +bool sail_config_is_array(const sail_config_json config); +bool sail_config_is_bool_array(const sail_config_json config); +bool sail_config_is_bool_array_with_size(const sail_config_json config, mach_int expected); + +void sail_config_unwrap_string(sail_string *str, const sail_config_json config); + +void sail_config_unwrap_int(sail_int *n, const sail_config_json config); + +void sail_config_unwrap_bits(lbits *bv, const sail_config_json config); + +#ifdef __cplusplus +} +#endif + +#endif diff --git a/src/bin/dune b/src/bin/dune index 38c3f278c..9b9feee9c 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -184,6 +184,8 @@ (%{workspace_root}/lib/sail.c as lib/sail.c) (%{workspace_root}/lib/sail.h as lib/sail.h) (%{workspace_root}/lib/sail.tex as lib/sail.tex) + (%{workspace_root}/lib/json/cJSON.c as lib/json/cJSON.c) + (%{workspace_root}/lib/json/cJSON.h as lib/json/cJSON.h) (%{workspace_root}/lib/sail_coverage.h as lib/sail_coverage.h) (%{workspace_root}/lib/sail_failure.c as lib/sail_failure.c) (%{workspace_root}/lib/sail_failure.h as lib/sail_failure.h) diff --git a/src/bin/repl.ml b/src/bin/repl.ml index 455b75a92..87054b467 100644 --- a/src/bin/repl.ml +++ b/src/bin/repl.ml @@ -71,7 +71,7 @@ type istate = { display_options : display_options; state : Interpreter.lstate * Interpreter.gstate; default_sail_dir : string; - config : Yojson.Basic.t option; + config : Yojson.Safe.t option; } let shrink_istate istate : Interactive.State.istate = diff --git a/src/bin/repl.mli b/src/bin/repl.mli index 4b59204b5..401c0294b 100644 --- a/src/bin/repl.mli +++ b/src/bin/repl.mli @@ -59,7 +59,7 @@ val start_repl : ?banner:bool -> ?commands:string list -> ?auto_rewrites:bool -> - config:Yojson.Basic.t option -> + config:Yojson.Safe.t option -> options:(Arg.key * Arg.spec * Arg.doc) list -> Initial_check.ctx -> Type_check.Env.t -> diff --git a/src/bin/sail.ml b/src/bin/sail.ml index dad0f27b6..3c8e70fab 100644 --- a/src/bin/sail.ml +++ b/src/bin/sail.ml @@ -430,7 +430,24 @@ let file_to_string filename = close_in chan; Buffer.contents buf -let run_sail (config : Yojson.Basic.t option) tgt = +let apply_model_config env ast = + match !opt_config_file with + | Some file -> + if Sys.file_exists file then ( + let json = + try Yojson.Safe.from_file ~fname:file ~lnum:0 file + with Yojson.Json_error message -> + raise + (Reporting.err_general Parse_ast.Unknown + (Printf.sprintf "Failed to parse configuration file:\n%s" message) + ) + in + Config.rewrite_ast env json ast + ) + else raise (Reporting.err_general Parse_ast.Unknown (Printf.sprintf "Configuration file %s does not exist" file)) + | None -> Config.rewrite_ast env (`Assoc []) ast + +let run_sail (config : Yojson.Safe.t option) tgt = Target.run_pre_parse_hook tgt (); let project_files, frees = @@ -489,6 +506,7 @@ let run_sail (config : Yojson.Basic.t option) tgt = ) in let ast = Frontend.instantiate_abstract_types (Some tgt) !opt_instantiations ast in + let ast = apply_model_config env ast in let ast, env = Frontend.initial_rewrite effect_info env ast in let ast, env = match !opt_splice with [] -> (ast, env) | files -> Splice.splice_files ctx ast (List.rev files) in let effect_info = Effects.infer_side_effects (Target.asserts_termination tgt) ast in @@ -504,7 +522,7 @@ let run_sail (config : Yojson.Basic.t option) tgt = (ctx, ast, env, effect_info) -let run_sail_format (config : Yojson.Basic.t option) = +let run_sail_format (config : Yojson.Safe.t option) = let is_format_file f = match !opt_format_only with [] -> true | files -> List.exists (fun f' -> f = f') files in let is_skipped_file f = match !opt_format_skip with [] -> false | files -> List.exists (fun f' -> f = f') files in let module Config = struct @@ -557,7 +575,7 @@ let rec find_file_above ?prev_inode_opt dir file = else None with Unix.Unix_error _ -> None -let get_config_file () = +let get_implicit_config_file override_file = let check_exists file = if Sys.file_exists file then Some file else ( @@ -565,7 +583,7 @@ let get_config_file () = None ) in - match !opt_config_file with + match override_file with | Some file -> check_exists file | None -> ( match Sys.getenv_opt "SAIL_CONFIG" with @@ -574,7 +592,7 @@ let get_config_file () = ) let parse_config_file file = - try Some (Yojson.Basic.from_file ~fname:file ~lnum:0 file) + try Some (Yojson.Safe.from_file ~fname:file ~lnum:0 file) with Yojson.Json_error message -> Reporting.warn "" Parse_ast.Unknown (Printf.sprintf "Failed to parse configuration file: %s" message); None @@ -603,7 +621,7 @@ let main () = Arg.parse_dynamic options (fun s -> opt_free_arguments := !opt_free_arguments @ [s]) usage_msg; - let config = Option.bind (get_config_file ()) parse_config_file in + let config = Option.bind (get_implicit_config_file None) parse_config_file in feature_check (); @@ -626,6 +644,7 @@ let main () = print_endline version_full; exit 0 ); + if !opt_show_sail_dir then ( print_endline (Reporting.get_sail_dir Locations.sail_dir); exit 0 diff --git a/src/lib/anf.ml b/src/lib/anf.ml index b57602ca3..6271d0b61 100644 --- a/src/lib/anf.ml +++ b/src/lib/anf.ml @@ -57,13 +57,15 @@ module Big_int = Nat_big_num (* 1. Conversion to A-normal form (ANF) *) (**************************************************************************) +type function_id = Sail_function of id | Pure_extern of id | Extern of id + type anf_annot = { loc : l; env : Env.t; uannot : uannot } type 'a aexp = AE_aux of 'a aexp_aux * anf_annot and 'a aexp_aux = | AE_val of 'a aval - | AE_app of id * 'a aval list * 'a + | AE_app of function_id * 'a aval list * 'a | AE_typ of 'a aexp * 'a | AE_assign of 'a alexp * 'a aexp | AE_let of mut * id * 'a * 'a aexp * 'a aexp * 'a @@ -289,7 +291,9 @@ let rec is_pure_aexp effect_info (AE_aux (aexp, { uannot; _ })) = | Some _ -> true | None -> ( match aexp with - | AE_app (f, _, _) -> Effects.function_is_pure f effect_info + | AE_app (Sail_function f, _, _) -> Effects.function_is_pure f effect_info + | AE_app (Pure_extern f, _, _) -> true + | AE_app (Extern f, _, _) -> false | AE_typ (aexp, _) -> is_pure_aexp effect_info aexp | AE_let (Immutable, _, _, aexp1, aexp2, _) -> is_pure_aexp effect_info aexp1 && is_pure_aexp effect_info aexp2 | AE_match (_, arms, _) -> @@ -456,6 +460,11 @@ let pp_order = function Ord_aux (Ord_inc, _) -> string "inc" | Ord_aux (Ord_dec, let pp_id id = string (string_of_id id) +let pp_function_id = function + | Sail_function id -> pp_id id + | Pure_extern id -> string "pure_extern" ^^ space ^^ pp_id id + | Extern id -> string "extern" ^^ space ^^ pp_id id + let rec pp_alexp = function | AL_id (id, typ) -> pp_annot typ (pp_id id) | AL_addr (id, typ) -> string "*" ^^ parens (pp_annot typ (pp_id id)) @@ -474,7 +483,7 @@ let rec pp_aexp (AE_aux (aexp, annot)) = | AE_val v -> pp_aval v | AE_typ (aexp, typ) -> pp_annot typ (string "$" ^^ pp_aexp aexp) | AE_assign (alexp, aexp) -> pp_alexp alexp ^^ string " := " ^^ pp_aexp aexp - | AE_app (id, args, typ) -> pp_annot typ (pp_id id ^^ parens (separate_map (comma ^^ space) pp_aval args)) + | AE_app (id, args, typ) -> pp_annot typ (pp_function_id id ^^ parens (separate_map (comma ^^ space) pp_aval args)) | AE_short_circuit (SC_or, aval, aexp) -> pp_aval aval ^^ string " || " ^^ pp_aexp aexp | AE_short_circuit (SC_and, aval, aexp) -> pp_aval aval ^^ string " && " ^^ pp_aexp aexp | AE_let (mut, id, id_typ, binding, body, typ) -> @@ -740,7 +749,7 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) = let aexps = List.map anf exps in let avals = List.map to_aval aexps in let wrap = List.fold_left (fun f g x -> f (g x)) (fun x -> x) (List.map snd avals) in - wrap (mk_aexp (AE_app (id, List.map fst avals, typ_of exp))) + wrap (mk_aexp (AE_app (Sail_function id, List.map fst avals, typ_of exp))) | E_throw exn_exp -> let aexp = anf exn_exp in let aval, wrap = to_aval aexp in @@ -758,13 +767,13 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) = let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_assert", [aval1; aval2], unit_typ)))) + wrap1 (wrap2 (mk_aexp (AE_app (Extern (mk_id "sail_assert"), [aval1; aval2], unit_typ)))) | E_cons (exp1, exp2) -> let aexp1 = anf exp1 in let aexp2 = anf exp2 in let aval1, wrap1 = to_aval aexp1 in let aval2, wrap2 = to_aval aexp2 in - wrap1 (wrap2 (mk_aexp (AE_app (mk_id "sail_cons", [aval1; aval2], typ_of exp)))) + wrap1 (wrap2 (mk_aexp (AE_app (Extern (mk_id "sail_cons"), [aval1; aval2], typ_of exp)))) | E_id id -> let lvar = Env.lookup_id id (env_of exp) in begin @@ -773,6 +782,9 @@ let rec anf (E_aux (e_aux, (l, tannot)) as exp) = | E_ref id -> let lvar = Env.lookup_id id (env_of exp) in mk_aexp (AE_val (AV_ref (id, lvar))) + | E_config key -> + let anf_key_part part = AV_lit (mk_lit (L_string part), string_typ) in + mk_aexp (AE_app (Extern (mk_id "sail_config_get"), List.map anf_key_part key, typ_of exp)) | E_match (match_exp, pexps) -> let match_aval, match_wrap = to_aval (anf match_exp) in let anf_pexp (Pat_aux (pat_aux, (l, tannot))) = diff --git a/src/lib/anf.mli b/src/lib/anf.mli index 29228c3c5..ca2d4874c 100644 --- a/src/lib/anf.mli +++ b/src/lib/anf.mli @@ -78,6 +78,8 @@ open Ast_util open Jib open Type_check +type function_id = Sail_function of id | Pure_extern of id | Extern of id + (** Each ANF expression has an annotation which contains the location of the original Sail expression, it's typing environment, and the uannot type containing any attributes attached to the original @@ -88,7 +90,7 @@ type 'a aexp = AE_aux of 'a aexp_aux * anf_annot and 'a aexp_aux = | AE_val of 'a aval - | AE_app of id * 'a aval list * 'a + | AE_app of function_id * 'a aval list * 'a | AE_typ of 'a aexp * 'a | AE_assign of 'a alexp * 'a aexp | AE_let of mut * id * 'a * 'a aexp * 'a aexp * 'a @@ -155,7 +157,7 @@ val aexp_typ : typ aexp -> typ val map_aval : (anf_annot -> 'a aval -> 'a aval) -> 'a aexp -> 'a aexp (** Map over all function calls in an ANF expression *) -val map_functions : (anf_annot -> id -> 'a aval list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp +val map_functions : (anf_annot -> function_id -> 'a aval list -> 'a -> 'a aexp_aux) -> 'a aexp -> 'a aexp (** This function 'folds' an [aexp] applying the provided function to all leaf subexpressions, then applying the function to their diff --git a/src/lib/ast_util.ml b/src/lib/ast_util.ml index 5e2ddbe43..931b5783a 100644 --- a/src/lib/ast_util.ml +++ b/src/lib/ast_util.ml @@ -842,6 +842,7 @@ and map_exp_annot_aux f = function | E_id id -> E_id id | E_ref id -> E_ref id | E_lit lit -> E_lit lit + | E_config key -> E_config key | E_typ (typ, exp) -> E_typ (typ, map_exp_annot f exp) | E_app (id, xs) -> E_app (id, List.map (map_exp_annot f) xs) | E_app_infix (x, op, y) -> E_app_infix (map_exp_annot f x, op, map_exp_annot f y) @@ -1278,6 +1279,7 @@ let rec string_of_exp (E_aux (exp, _)) = | E_throw exp -> "throw " ^ string_of_exp exp | E_cons (x, xs) -> string_of_exp x ^ " :: " ^ string_of_exp xs | E_list xs -> "[|" ^ string_of_list ", " string_of_exp xs ^ "|]" + | E_config key -> "config " ^ string_of_list "." (fun s -> s) key | E_struct_update (exp, fexps) -> "struct { " ^ string_of_exp exp ^ " with " ^ string_of_list "; " string_of_fexp fexps ^ " }" | E_struct fexps -> "struct { " ^ string_of_list "; " string_of_fexp fexps ^ " }" @@ -1748,6 +1750,7 @@ let rec subst id value (E_aux (e_aux, annot) as exp) = | E_block exps -> E_block (List.map (subst id value) exps) | E_id id' -> if Id.compare id id' = 0 then unaux_exp value else E_id id' | E_lit lit -> E_lit lit + | E_config parts -> E_config parts | E_typ (typ, exp) -> E_typ (typ, subst id value exp) | E_app (fn, exps) -> E_app (fn, List.map (subst id value) exps) | E_app_infix (exp1, op, exp2) -> E_app_infix (subst id value exp1, op, subst id value exp2) @@ -1986,6 +1989,7 @@ let rec locate : 'a. (l -> l) -> 'a exp -> 'a exp = | E_block exps -> E_block (List.map (locate f) exps) | E_id id -> E_id (locate_id f id) | E_lit lit -> E_lit (locate_lit f lit) + | E_config parts -> E_config parts | E_typ (typ, exp) -> E_typ (locate_typ f typ, locate f exp) | E_app (id, exps) -> E_app (locate_id f id, List.map (locate f) exps) | E_app_infix (exp1, op, exp2) -> E_app_infix (locate f exp1, locate_id f op, locate f exp2) diff --git a/src/lib/chunk_ast.ml b/src/lib/chunk_ast.ml index b17ef70e6..c96d7f235 100644 --- a/src/lib/chunk_ast.ml +++ b/src/lib/chunk_ast.ml @@ -775,6 +775,7 @@ let rec chunk_exp comments chunks (E_aux (aux, l)) = match aux with | E_id id -> Queue.add (Atom (string_of_id id)) chunks | E_ref id -> Queue.add (Atom ("ref " ^ string_of_id id)) chunks + | E_config s -> Queue.add (Atom ("config " ^ s)) chunks | E_lit lit -> Queue.add (chunk_of_lit lit) chunks | E_attribute (attr, arg, exp) -> Queue.add (Atom (Ast_util.string_of_attribute attr arg)) chunks; diff --git a/src/lib/config.ml b/src/lib/config.ml new file mode 100644 index 000000000..e271d7e0f --- /dev/null +++ b/src/lib/config.ml @@ -0,0 +1,218 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2025 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* SPDX-License-Identifier: BSD-2-Clause *) +(****************************************************************************) + +open Ast +open Ast_util +open Rewriter +open Type_check + +module J = Yojson.Safe +module StringMap = Util.StringMap + +module ConfigTypes : sig + type t + + val create : unit -> t + + val find_opt : at:Ast.l -> string list -> t -> (Ast.l * typ) option + + val update_type : string list -> Ast.l -> typ -> t -> bool + + val insert : string list -> Ast.l -> typ -> t -> unit +end = struct + open Util.Option_monad + open Error_format + + type t = Sail_value of { mutable loc : Ast.l; mutable typ : typ } | Object of (string, t) Hashtbl.t + + (* Random is false here for deterministic error messages *) + let create () = Object (Hashtbl.create ~random:false 16) + + let rec get_example = function + | Sail_value { loc; typ } -> Some (loc, typ) + | Object tbl -> Hashtbl.fold (fun _ value acc -> if Option.is_none acc then get_example value else acc) tbl None + + let find_opt ~at:l full_parts map = + let rec go parts map = + match (parts, map) with + | part :: parts, Object tbl -> + let* map = Hashtbl.find_opt tbl part in + go parts map + | part :: _, Sail_value { loc; typ } -> + let msg = + Seq + [ + Line + (Printf.sprintf + "Attempting to access key %s from configuration that has already been interpreted as type %s" part + (string_of_typ typ) + ); + Location ("", Some "interpreted here", loc, Seq []); + ] + in + let b = Buffer.create 1024 in + format_message msg (buffer_formatter b); + raise (Reporting.err_typ l (Buffer.contents b)) + | [], Sail_value { loc; typ } -> Some (loc, typ) + | [], obj -> + let full_parts = String.concat "." full_parts in + let extra_info msg = + match get_example obj with + | Some (l, typ) -> Seq [msg; Line ""; Line "For example:"; Location ("", Some "used here", l, Seq [])] + | None -> msg + in + let msg = + Line (Printf.sprintf "Attempting to access key %s, but various subkeys have already been used" full_parts) + in + let b = Buffer.create 1024 in + format_message (extra_info msg) (buffer_formatter b); + raise (Reporting.err_general l (Buffer.contents b)) + in + go full_parts map + + let rec insert parts l typ map = + match (parts, map) with + | [part], Object tbl -> Hashtbl.replace tbl part (Sail_value { loc = l; typ }) + | part :: parts, Object tbl -> ( + match Hashtbl.find_opt tbl part with + | Some map -> insert parts l typ map + | None -> + Hashtbl.add tbl part (create ()); + insert (part :: parts) l typ map + ) + | _ -> Reporting.unreachable l __POS__ "Failed to insert into config type map" + + let rec update_type parts l typ map = + match (parts, map) with + | part :: parts, Object tbl -> ( + match Hashtbl.find_opt tbl part with Some map -> update_type parts l typ map | None -> false + ) + | [], Sail_value v -> + v.loc <- l; + v.typ <- typ; + true + | _ -> false +end + +let find_json ~at:l full_parts json = + let rec go parts json = + match (parts, json) with + | [], json -> Some json + | part :: parts, `Assoc obj -> ( + match List.assoc_opt part obj with Some json -> go parts json | None -> None + ) + | parts, json -> + let full_parts = String.concat "." full_parts in + let parts = String.concat "." parts in + Printf.sprintf "Attempting to access configuration %s of %s, but JSON is %s" parts full_parts (J.to_string json) + |> Reporting.err_general l |> raise + in + go full_parts json + +let json_bit ~at:l = function + | `Bool true -> '1' + | `Bool false -> '0' + | json -> raise (Reporting.err_general l (Printf.sprintf "Failed to interpret %s as a bit" (J.to_string json))) + +let sail_exp_from_json ~at:l env typ = function + | `Int n -> mk_lit_exp ~loc:l (L_num (Big_int.of_int n)) + | `Intlit n -> mk_lit_exp ~loc:l (L_num (Big_int.of_string n)) + | `String s -> + if Option.is_some (Type_check.destruct_numeric typ) then mk_lit_exp ~loc:l (L_num (Big_int.of_string s)) + else mk_lit_exp ~loc:l (L_string s) + | `List jsons when Option.is_some (Type_check.destruct_bitvector env typ) -> + L_bin (List.map (json_bit ~at:l) jsons |> List.to_seq |> String.of_seq) |> mk_lit_exp ~loc:l + | _ -> assert false + +let rewrite_exp global_env types json (aux, annot) = + match aux with + | E_config parts -> ( + let typ = typ_of_annot annot in + let typ = + match ConfigTypes.find_opt ~at:(fst annot) parts types with + | Some (prev_l, prev_typ) -> + if subtype_check global_env prev_typ typ then prev_typ + else if subtype_check global_env typ prev_typ then ( + let (_ : bool) = ConfigTypes.update_type parts (fst annot) typ types in + typ + ) + else + let open Error_format in + let msg = + Seq + [ + Line "Incompatible types for configuration option found:"; + List + [ + ("Type " ^ string_of_typ typ ^ " found here", Seq []); + ("Type " ^ string_of_typ prev_typ ^ " found as previous type", Seq []); + ]; + Line ""; + Location ("", Some "previous type found here", prev_l, Seq []); + ] + in + let b = Buffer.create 1024 in + format_message msg (buffer_formatter b); + raise (Reporting.err_typ (fst annot) (Buffer.contents b)) + | None -> + ConfigTypes.insert parts (fst annot) typ types; + typ + in + match find_json ~at:(fst annot) parts json with + | None -> E_aux (aux, annot) + | Some json -> ( + try + let exp = sail_exp_from_json ~at:(fst annot) global_env typ json in + Type_check.check_exp (env_of_annot annot) exp typ + with Type_error.Type_error (l, err) -> raise (Type_error.to_reporting_exn l err) + ) + ) + | _ -> E_aux (aux, annot) + +let rewrite_ast global_env json ast = + let types = ConfigTypes.create () in + let alg = { id_exp_alg with e_aux = rewrite_exp global_env types json } in + rewrite_ast_base { rewriters_base with rewrite_exp = (fun _ -> fold_exp alg) } ast diff --git a/src/lib/config.mli b/src/lib/config.mli new file mode 100644 index 000000000..ec0825ac4 --- /dev/null +++ b/src/lib/config.mli @@ -0,0 +1,49 @@ +(****************************************************************************) +(* Sail *) +(* *) +(* Sail and the Sail architecture models here, comprising all files and *) +(* directories except the ASL-derived Sail code in the aarch64 directory, *) +(* are subject to the BSD two-clause licence below. *) +(* *) +(* The ASL derived parts of the ARMv8.3 specification in *) +(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *) +(* *) +(* Copyright (c) 2013-2025 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Alasdair Armstrong *) +(* Brian Campbell *) +(* Thomas Bauereiss *) +(* Anthony Fox *) +(* Jon French *) +(* Dominic Mulligan *) +(* Stephen Kell *) +(* Mark Wassell *) +(* Alastair Reid (Arm Ltd) *) +(* *) +(* All rights reserved. *) +(* *) +(* This work was partially supported by EPSRC grant EP/K008528/1 REMS: Rigorous *) +(* Engineering for Mainstream Systems, an ARM iCASE award, EPSRC IAA *) +(* KTF funding, and donations from Arm. This project has received *) +(* funding from the European Research Council (ERC) under the European *) +(* Union’s Horizon 2020 research and innovation programme (grant *) +(* agreement No 789108, ELVER). *) +(* *) +(* This software was developed by SRI International and the University of *) +(* Cambridge Computer Laboratory (Department of Computer Science and *) +(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *) +(* and FA8750-10-C-0237 ("CTSRD"). *) +(* *) +(* SPDX-License-Identifier: BSD-2-Clause *) +(****************************************************************************) + +open Type_check + +val rewrite_ast : env -> Yojson.Safe.t -> typed_ast -> typed_ast diff --git a/src/lib/constant_propagation.ml b/src/lib/constant_propagation.ml index 99be000de..66c6a2497 100644 --- a/src/lib/constant_propagation.ml +++ b/src/lib/constant_propagation.ml @@ -356,7 +356,7 @@ let const_props target ast = ), assigns ) - | E_lit _ | E_sizeof _ | E_constraint _ -> (exp, assigns) + | E_lit _ | E_sizeof _ | E_constraint _ | E_config _ -> (exp, assigns) | E_typ (t, e') -> let e'', assigns = const_prop_exp substs assigns e' in if is_value e'' then (reduce_cast t e'' l annot, assigns) else re (E_typ (t, e'')) assigns diff --git a/src/lib/format_sail.ml b/src/lib/format_sail.ml index f0d8e5d67..c5326c746 100644 --- a/src/lib/format_sail.ml +++ b/src/lib/format_sail.ml @@ -372,7 +372,7 @@ let int_option k = function | json -> Reporting.simple_warn (Printf.sprintf "Argument for key %s must be an integer, got %s instead. Using default value." k - (Yojson.Basic.to_string json) + (Yojson.Safe.to_string json) ); None @@ -381,7 +381,7 @@ let bool_option k = function | json -> Reporting.simple_warn (Printf.sprintf "Argument for key %s must be a boolean, got %s instead. Using default value." k - (Yojson.Basic.to_string json) + (Yojson.Safe.to_string json) ); None @@ -391,14 +391,14 @@ let float_option k = function | json -> Reporting.simple_warn (Printf.sprintf "Argument for key %s must be a number, got %s instead. Using default value." k - (Yojson.Basic.to_string json) + (Yojson.Safe.to_string json) ); None let get_option ~key:k ~keys:ks ~read ~default:d = List.assoc_opt k ks |> (fun opt -> Option.bind opt (read k)) |> Option.value ~default:d -let config_from_json (json : Yojson.Basic.t) = +let config_from_json (json : Yojson.Safe.t) = match json with | `Assoc keys -> begin diff --git a/src/lib/format_sail.mli b/src/lib/format_sail.mli index 1891f1f65..0be32a595 100644 --- a/src/lib/format_sail.mli +++ b/src/lib/format_sail.mli @@ -59,7 +59,7 @@ type config = { (** Read the config struct from a json object. Raises err_general if the json is not an object, and warns about any invalid keys. *) -val config_from_json : Yojson.Basic.t -> config +val config_from_json : Yojson.Safe.t -> config val default_config : config diff --git a/src/lib/initial_check.ml b/src/lib/initial_check.ml index 030969dc6..c9647d6db 100644 --- a/src/lib/initial_check.ml +++ b/src/lib/initial_check.ml @@ -1225,6 +1225,14 @@ and to_ast_fpat ctx (P.FP_aux (aux, l)) = | FP_field (field, pat) -> (to_ast_id ctx field, to_ast_pat ctx pat) | FP_wild -> Reporting.unreachable l __POS__ "Unexpected field wildcard" +let rec is_config (P.E_aux (aux, _)) = + match aux with + | P.E_field (exp, field) -> begin + match is_config exp with None -> None | Some key -> Some (string_of_parse_id field :: key) + end + | P.E_config root -> Some [root] + | _ -> None + let rec to_ast_letbind ctx (P.LB_aux (lb, l) : P.letbind) : uannot letbind = LB_aux ((match lb with P.LB_val (pat, exp) -> LB_val (to_ast_pat ctx pat, to_ast_exp ctx exp)), (l, empty_uannot)) @@ -1303,7 +1311,11 @@ and to_ast_exp ctx exp = | Some fexps -> E_struct_update (to_ast_exp ctx exp, fexps) | _ -> raise (Reporting.err_unreachable l __POS__ "to_ast_fexps with true returned none") ) - | P.E_field (exp, id) -> E_field (to_ast_exp ctx exp, to_ast_id ctx id) + | P.E_field (exp, field) -> ( + match is_config exp with + | None -> E_field (to_ast_exp ctx exp, to_ast_id ctx field) + | Some key -> E_config (List.rev (string_of_parse_id field :: key)) + ) | P.E_match (exp, pexps) -> E_match (to_ast_exp ctx exp, List.map (to_ast_case ctx) pexps) | P.E_try (exp, pexps) -> E_try (to_ast_exp ctx exp, List.map (to_ast_case ctx) pexps) | P.E_let (leb, exp) -> E_let (to_ast_letbind ctx leb, to_ast_exp ctx exp) @@ -1313,6 +1325,7 @@ and to_ast_exp ctx exp = | P.E_constraint nc -> E_constraint (to_ast_constraint ctx nc) | P.E_exit exp -> E_exit (to_ast_exp ctx exp) | P.E_throw exp -> E_throw (to_ast_exp ctx exp) + | P.E_config key -> E_config [key] | P.E_return exp -> E_return (to_ast_exp ctx exp) | P.E_assert (cond, msg) -> E_assert (to_ast_exp ctx cond, to_ast_exp ctx msg) | P.E_internal_plet (pat, exp1, exp2) -> diff --git a/src/lib/interactive.ml b/src/lib/interactive.ml index 48080379e..9fa0d4abf 100644 --- a/src/lib/interactive.ml +++ b/src/lib/interactive.ml @@ -58,7 +58,7 @@ module State = struct effect_info : Effects.side_effect_info; env : Type_check.Env.t; default_sail_dir : string; - config : Yojson.Basic.t option; + config : Yojson.Safe.t option; } let initial_istate config default_sail_dir = diff --git a/src/lib/interactive.mli b/src/lib/interactive.mli index 79394b5b4..d1c23f619 100644 --- a/src/lib/interactive.mli +++ b/src/lib/interactive.mli @@ -60,10 +60,10 @@ module State : sig effect_info : Effects.side_effect_info; env : Type_check.Env.t; default_sail_dir : string; - config : Yojson.Basic.t option; + config : Yojson.Safe.t option; } - val initial_istate : Yojson.Basic.t option -> string -> istate + val initial_istate : Yojson.Safe.t option -> string -> istate end val arg : string -> string diff --git a/src/lib/jib_compile.ml b/src/lib/jib_compile.ml index fb2707088..77ebb1252 100644 --- a/src/lib/jib_compile.ml +++ b/src/lib/jib_compile.ml @@ -204,6 +204,7 @@ let rec mangle_string_of_ctyp ctx = function | CT_string -> "s" | CT_float n -> "f" ^ string_of_int n | CT_rounding_mode -> "m" + | CT_json -> "j" | CT_enum (id, _) -> "E" ^ string_of_id id ^ "%" | CT_ref ctyp -> "&" ^ mangle_string_of_ctyp ctx ctyp | CT_memory_writes -> "w" @@ -343,6 +344,8 @@ module Make (C : CONFIG) = struct end | _ -> [] + let unit_cval = V_lit (VL_unit, CT_unit) + let rec compile_aval l ctx = function | AV_cval (cval, typ) -> let ctyp = cval_ctyp cval in @@ -616,6 +619,68 @@ module Make (C : CONFIG) = struct !cleanup ) + let compile_extern l ctx id args = + let setup = ref [] in + let cleanup = ref [] in + + let setup_arg aval = + let arg_setup, cval, arg_cleanup = compile_aval l ctx aval in + setup := List.rev arg_setup @ !setup; + cleanup := arg_cleanup @ !cleanup; + cval + in + + let setup_args = List.map setup_arg args in + + (List.rev !setup, (fun clexp -> iextern l clexp (id, []) setup_args), !cleanup) + + let compile_config l ctx args typ = + let ctyp = ctyp_of_typ ctx typ in + + let key = + List.map + (function + | AV_lit (L_aux (L_string part, _), _) -> part + | _ -> Reporting.unreachable l __POS__ "Invalid argument when compiling config key" + ) + args + in + let args = [V_lit (VL_int (Big_int.of_int (List.length key)), CT_fint 64); V_config_key key] in + + let config_extract ctyp ~validate ~extract = + let json = ngensym () in + let valid = ngensym () in + let value = ngensym () in + ( [ + idecl l CT_json json; + iextern l (CL_id (json, CT_json)) (mk_id "sail_config_get", []) args; + idecl l CT_bool valid; + iextern l (CL_id (valid, CT_bool)) (mk_id (fst validate), []) ([V_id (json, CT_json)] @ snd validate); + iif l (V_call (Bnot, [V_id (valid, CT_bool)])) [ibad_config l] [] CT_unit; + idecl l ctyp value; + iextern l (CL_id (value, ctyp)) (mk_id extract, []) [V_id (json, CT_json)]; + ], + (fun clexp -> icopy l clexp (V_id (value, ctyp))), + [iclear ctyp value; iclear CT_json json] + ) + in + + match ctyp with + | CT_string -> ([], (fun clexp -> iextern l clexp (mk_id "sail_config_get_string", []) args), []) + | CT_unit -> ([], (fun clexp -> icopy l clexp unit_cval), []) + | CT_lint -> + let gs = ngensym () in + ( [idecl l CT_json gs; iextern l (CL_id (gs, CT_json)) (mk_id "sail_config_get", []) args], + (fun clexp -> iextern l clexp (mk_id "sail_config_unwrap_int", []) [V_id (gs, CT_json)]), + [iclear CT_json gs] + ) + | CT_lbits -> config_extract CT_lbits ~validate:("sail_config_is_bool_array", []) ~extract:"sail_config_unwrap_bits" + | CT_fbits n -> + config_extract CT_lbits + ~validate:("sail_config_is_bool_array_with_size", [V_lit (VL_int (Big_int.of_int n), CT_fint 64)]) + ~extract:"sail_config_unwrap_bits" + | _ -> Reporting.unreachable l __POS__ "Invalid configuration type" + let rec apat_ctyp ctx (AP_aux (apat, { env; _ })) = let ctx = { ctx with local_env = env } in match apat with @@ -729,8 +794,6 @@ module Make (C : CONFIG) = struct end | AP_nil _ -> ([on_failure l (V_call (Bnot, [V_call (List_is_empty, [cval])]))], [], [], ctx) - let unit_cval = V_lit (VL_unit, CT_unit) - let rec compile_alexp ctx alexp = match alexp with | AL_id (id, typ) -> @@ -777,13 +840,16 @@ module Make (C : CONFIG) = struct let ctx = { ctx with locals = Bindings.add id (mut, binding_ctyp) ctx.locals } in let setup, call, cleanup = compile_aexp ctx body in (letb_setup @ setup, call, cleanup @ letb_cleanup) - | AE_app (id, vs, _) -> + | AE_app (Sail_function id, vs, _) -> if Option.is_some (get_attribute "mapping_guarded" uannot) then ( let override_id = append_id id "_infallible" in if Bindings.mem override_id ctx.valspecs then compile_funcall ~override_id l ctx id vs else compile_funcall l ctx id vs ) else compile_funcall l ctx id vs + | AE_app (Pure_extern id, args, _) -> compile_extern l ctx id args + | AE_app (Extern id, args, typ) -> + if string_of_id id = "sail_config_get" then compile_config l ctx args typ else compile_extern l ctx id args | AE_val aval -> let setup, cval, cleanup = compile_aval l ctx aval in (setup, (fun clexp -> icopy l clexp cval), cleanup) @@ -1822,6 +1888,7 @@ module Make (C : CONFIG) = struct | DEF_fixity _ -> ([], ctx) | DEF_pragma ("abstract", id_str, _) -> ([CDEF_aux (CDEF_pragma ("abstract", id_str), def_annot)], ctx) | DEF_pragma ("c_in_main", source, _) -> ([CDEF_aux (CDEF_pragma ("c_in_main", source), def_annot)], ctx) + | DEF_pragma ("c_in_main_post", source, _) -> ([CDEF_aux (CDEF_pragma ("c_in_main_post", source), def_annot)], ctx) (* We just ignore any pragmas we don't want to deal with. *) | DEF_pragma _ -> ([], ctx) (* Termination measures only needed for Coq, and other theorem prover output *) @@ -2275,31 +2342,31 @@ module Make (C : CONFIG) = struct let precise_call call tail = match call with - | I_aux (I_funcall (CR_one clexp, extern, (id, ctyp_args), args), ((_, l) as aux)) as instr -> begin + | I_aux (I_funcall (CR_one clexp, true, (id, _), args), ((_, l) as aux)) as instr -> + if string_of_id id = "sail_cons" then ( + match args with + | [hd_arg; tl_arg] -> + let ctyp_arg = ctyp_suprema (cval_ctyp hd_arg) in + if not (ctyp_equal (cval_ctyp hd_arg) ctyp_arg) then ( + let gs = ngensym () in + let cast = [idecl l ctyp_arg gs; icopy l (CL_id (gs, ctyp_arg)) hd_arg] in + let cleanup = [iclear ~loc:l ctyp_arg gs] in + [ + iblock + (cast + @ [I_aux (I_funcall (CR_one clexp, true, (id, []), [V_id (gs, ctyp_arg); tl_arg]), aux)] + @ tail @ cleanup + ); + ] + ) + else instr :: tail + | _ -> + (* cons must have two arguments *) + Reporting.unreachable (id_loc id) __POS__ "Invalid cons call" + ) + else instr :: tail + | I_aux (I_funcall (CR_one clexp, false, (id, ctyp_args), args), ((_, l) as aux)) as instr -> begin match get_function_typ id with - | None when string_of_id id = "sail_cons" -> begin - match (ctyp_args, args) with - | [ctyp_arg], [hd_arg; tl_arg] -> - if not (ctyp_equal (cval_ctyp hd_arg) ctyp_arg) then ( - let gs = ngensym () in - let cast = [idecl l ctyp_arg gs; icopy l (CL_id (gs, ctyp_arg)) hd_arg] in - let cleanup = [iclear ~loc:l ctyp_arg gs] in - [ - iblock - (cast - @ [ - I_aux (I_funcall (CR_one clexp, extern, (id, ctyp_args), [V_id (gs, ctyp_arg); tl_arg]), aux); - ] - @ tail @ cleanup - ); - ] - ) - else instr :: tail - | _ -> - (* cons must have a single type parameter and two arguments *) - Reporting.unreachable (id_loc id) __POS__ "Invalid cons call" - end - | None -> instr :: tail | Some (param_ctyps, ret_ctyp) when C.make_call_precise ctx id param_ctyps ret_ctyp -> if List.compare_lengths args param_ctyps <> 0 then Reporting.unreachable (id_loc id) __POS__ @@ -2333,11 +2400,12 @@ module Make (C : CONFIG) = struct [ iblock1 (casts @ ret_setup - @ [I_aux (I_funcall (CR_one clexp, extern, (id, ctyp_args), args), aux)] + @ [I_aux (I_funcall (CR_one clexp, false, (id, ctyp_args), args), aux)] @ tail @ ret_cleanup @ cleanup ); ] | Some _ -> instr :: tail + | None -> instr :: tail end | instr -> instr :: tail in @@ -2465,13 +2533,3 @@ module Make (C : CONFIG) = struct let cdefs = sort_ctype_defs false cdefs in (cdefs, ctx) end - -let add_special_functions env effect_info = - let assert_vs = Initial_check.extern_of_string (mk_id "sail_assert") "(bool, string) -> unit" in - let exit_vs = Initial_check.extern_of_string (mk_id "sail_exit") "unit -> unit" in - let cons_vs = Initial_check.extern_of_string (mk_id "sail_cons") "forall ('a : Type). ('a, list('a)) -> list('a)" in - - let effect_info = Effects.add_monadic_built_in (mk_id "sail_assert") effect_info in - let effect_info = Effects.add_monadic_built_in (mk_id "sail_exit") effect_info in - - (snd (Type_error.check_defs env [assert_vs; exit_vs; cons_vs]), effect_info) diff --git a/src/lib/jib_compile.mli b/src/lib/jib_compile.mli index 4459c11e2..849af0db6 100644 --- a/src/lib/jib_compile.mli +++ b/src/lib/jib_compile.mli @@ -181,8 +181,3 @@ module Make (C : CONFIG) : sig val compile_ast : ctx -> typed_ast -> cdef list * ctx end - -(** Adds some special functions to the environment that are used to - convert several Sail language features, these are sail_assert, - sail_exit, and sail_cons. *) -val add_special_functions : Env.t -> Effects.side_effect_info -> Env.t * Effects.side_effect_info diff --git a/src/lib/jib_optimize.ml b/src/lib/jib_optimize.ml index de4a064b6..41338986c 100644 --- a/src/lib/jib_optimize.ml +++ b/src/lib/jib_optimize.ml @@ -151,6 +151,7 @@ let rec cval_subst id subst = function | V_ctor_unwrap (cval, ctor, ctyp) -> V_ctor_unwrap (cval_subst id subst cval, ctor, ctyp) | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> (field, cval_subst id subst cval)) fields, ctyp) | V_tuple (members, ctyp) -> V_tuple (List.map (cval_subst id subst) members, ctyp) + | V_config_key parts -> V_config_key parts let rec cval_map_id f = function | V_id (id, ctyp) -> V_id (f id, ctyp) @@ -163,6 +164,7 @@ let rec cval_map_id f = function | V_ctor_unwrap (cval, ctor, ctyp) -> V_ctor_unwrap (cval_map_id f cval, ctor, ctyp) | V_struct (fields, ctyp) -> V_struct (List.map (fun (field, cval) -> (field, cval_map_id f cval)) fields, ctyp) | V_tuple (members, ctyp) -> V_tuple (List.map (cval_map_id f) members, ctyp) + | V_config_key parts -> V_config_key parts module Remove_undefined = struct open Jib @@ -470,7 +472,7 @@ let remove_tuples cdefs ctx = List.fold_left (fun cts (_, ctyp) -> CTSet.union (all_tuples ctyp) cts) CTSet.empty id_ctyps | CT_list ctyp | CT_vector ctyp | CT_fvector (_, ctyp) | CT_ref ctyp -> all_tuples ctyp | CT_lint | CT_fint _ | CT_lbits | CT_sbits _ | CT_fbits _ | CT_constant _ | CT_float _ | CT_unit | CT_bool - | CT_real | CT_bit | CT_poly _ | CT_string | CT_enum _ | CT_rounding_mode | CT_memory_writes -> + | CT_real | CT_bit | CT_poly _ | CT_string | CT_enum _ | CT_rounding_mode | CT_memory_writes | CT_json -> CTSet.empty in let rec tuple_depth = function @@ -479,7 +481,7 @@ let remove_tuples cdefs ctx = List.fold_left (fun d (_, ctyp) -> max (tuple_depth ctyp) d) 0 id_ctyps | CT_list ctyp | CT_vector ctyp | CT_fvector (_, ctyp) | CT_ref ctyp -> tuple_depth ctyp | CT_lint | CT_fint _ | CT_lbits | CT_sbits _ | CT_fbits _ | CT_constant _ | CT_unit | CT_bool | CT_real | CT_bit - | CT_poly _ | CT_string | CT_enum _ | CT_float _ | CT_rounding_mode | CT_memory_writes -> + | CT_poly _ | CT_string | CT_enum _ | CT_float _ | CT_rounding_mode | CT_memory_writes | CT_json -> 0 in let rec fix_tuples = function @@ -494,12 +496,14 @@ let remove_tuples cdefs ctx = | CT_fvector (n, ctyp) -> CT_fvector (n, fix_tuples ctyp) | CT_ref ctyp -> CT_ref (fix_tuples ctyp) | ( CT_lint | CT_fint _ | CT_lbits | CT_sbits _ | CT_fbits _ | CT_constant _ | CT_float _ | CT_unit | CT_bool - | CT_real | CT_bit | CT_poly _ | CT_string | CT_enum _ | CT_rounding_mode | CT_memory_writes ) as ctyp -> + | CT_real | CT_bit | CT_poly _ | CT_string | CT_enum _ | CT_rounding_mode | CT_memory_writes | CT_json ) as ctyp + -> ctyp and fix_cval = function | V_id (id, ctyp) -> V_id (id, ctyp) | V_member (id, ctyp) -> V_member (id, ctyp) | V_lit (vl, ctyp) -> V_lit (vl, ctyp) + | V_config_key parts -> V_config_key parts | V_ctor_kind (cval, ctor, ctyp) -> V_ctor_kind (fix_cval cval, ctor, ctyp) | V_ctor_unwrap (cval, ctor, ctyp) -> V_ctor_unwrap (fix_cval cval, ctor, ctyp) | V_tuple_member (cval, _, n) -> diff --git a/src/lib/jib_ssa.ml b/src/lib/jib_ssa.ml index 4ab64f03c..fc266deb5 100644 --- a/src/lib/jib_ssa.ml +++ b/src/lib/jib_ssa.ml @@ -541,6 +541,7 @@ let rename_variables globals graph root children = ) | V_member (id, ctyp) -> V_member (id, ctyp) | V_lit (vl, ctyp) -> V_lit (vl, ctyp) + | V_config_key parts -> V_config_key parts | V_call (id, fs) -> V_call (id, List.map fold_cval fs) | V_field (f, field) -> V_field (fold_cval f, field) | V_tuple_member (f, len, n) -> V_tuple_member (fold_cval f, len, n) diff --git a/src/lib/jib_util.ml b/src/lib/jib_util.ml index 7d00fa411..2c6a467c0 100644 --- a/src/lib/jib_util.ml +++ b/src/lib/jib_util.ml @@ -114,6 +114,8 @@ let imatch_failure l = I_aux (I_exit "match", (instr_number (), l)) let iexit l = I_aux (I_exit "explicit", (instr_number (), l)) +let ibad_config l = I_aux (I_exit "bad config", (instr_number (), l)) + let iraw ?loc:(l = Parse_ast.Unknown) str = I_aux (I_raw str, (instr_number (), l)) let ijump l cval label = I_aux (I_jump (cval, label), (instr_number (), l)) @@ -258,6 +260,7 @@ let rec string_of_ctyp = function | CT_real -> "%real" | CT_string -> "%string" | CT_memory_writes -> "%memory_writes" + | CT_json -> "%json" | CT_tup ctyps -> "(" ^ Util.string_of_list ", " string_of_ctyp ctyps ^ ")" | CT_struct (id, _fields) -> "%struct " ^ Util.zencode_string (string_of_id id) | CT_enum (id, _) -> "%enum " ^ Util.zencode_string (string_of_id id) @@ -329,6 +332,7 @@ let rec string_of_cval = function | _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Struct without struct type found" end | V_tuple (members, _) -> "(" ^ Util.string_of_list ", " string_of_cval members ^ ")" + | V_config_key parts -> "config " ^ String.concat "." parts let rec string_of_clexp = function | CL_id (id, ctyp) -> string_of_name id @@ -389,7 +393,7 @@ let string_of_instr i = Document.to_string (doc_instr i) let rec map_ctyp f = function | ( CT_lint | CT_fint _ | CT_constant _ | CT_lbits | CT_fbits _ | CT_sbits _ | CT_float _ | CT_rounding_mode | CT_bit - | CT_unit | CT_bool | CT_real | CT_string | CT_poly _ | CT_enum _ | CT_memory_writes ) as ctyp -> + | CT_unit | CT_bool | CT_real | CT_string | CT_poly _ | CT_enum _ | CT_memory_writes | CT_json ) as ctyp -> f ctyp | CT_tup ctyps -> f (CT_tup (List.map (map_ctyp f) ctyps)) | CT_ref ctyp -> f (CT_ref (map_ctyp f ctyp)) @@ -404,7 +408,7 @@ let rec ctyp_has pred ctyp = || match ctyp with | CT_lint | CT_fint _ | CT_constant _ | CT_lbits | CT_fbits _ | CT_sbits _ | CT_float _ | CT_rounding_mode | CT_bit - | CT_unit | CT_bool | CT_real | CT_string | CT_poly _ | CT_enum _ | CT_memory_writes -> + | CT_unit | CT_bool | CT_real | CT_string | CT_poly _ | CT_enum _ | CT_memory_writes | CT_json -> false | CT_tup ctyps -> List.exists (ctyp_has pred) ctyps | CT_ref ctyp | CT_vector ctyp | CT_fvector (_, ctyp) | CT_list ctyp -> ctyp_has pred ctyp @@ -481,6 +485,9 @@ let rec ctyp_compare ctyp1 ctyp2 = | CT_string, CT_string -> 0 | CT_string, _ -> 1 | _, CT_string -> -1 + | CT_json, CT_json -> 0 + | CT_json, _ -> 1 + | _, CT_json -> -1 | CT_ref ctyp1, CT_ref ctyp2 -> ctyp_compare ctyp1 ctyp2 | CT_ref _, _ -> 1 | _, CT_ref _ -> -1 @@ -552,6 +559,7 @@ let rec ctyp_suprema = function | CT_bool -> CT_bool | CT_real -> CT_real | CT_bit -> CT_bit + | CT_json -> CT_json | CT_tup ctyps -> CT_tup (List.map ctyp_suprema ctyps) | CT_string -> CT_string | CT_float n -> CT_float n @@ -618,7 +626,7 @@ let rec ctyp_ids = function | CT_tup ctyps -> List.fold_left (fun ids ctyp -> IdSet.union (ctyp_ids ctyp) ids) IdSet.empty ctyps | CT_vector ctyp | CT_fvector (_, ctyp) | CT_list ctyp | CT_ref ctyp -> ctyp_ids ctyp | CT_lint | CT_fint _ | CT_constant _ | CT_lbits | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit - | CT_string | CT_poly _ | CT_float _ | CT_rounding_mode | CT_memory_writes -> + | CT_string | CT_poly _ | CT_float _ | CT_rounding_mode | CT_memory_writes | CT_json -> IdSet.empty let rec subst_poly substs = function @@ -631,12 +639,12 @@ let rec subst_poly substs = function | CT_variant (id, ctors) -> CT_variant (id, List.map (fun (ctor_id, ctyp) -> (ctor_id, subst_poly substs ctyp)) ctors) | CT_struct (id, fields) -> CT_struct (id, List.map (fun (ctor_id, ctyp) -> (ctor_id, subst_poly substs ctyp)) fields) | ( CT_lint | CT_fint _ | CT_constant _ | CT_unit | CT_bool | CT_bit | CT_string | CT_real | CT_lbits | CT_fbits _ - | CT_sbits _ | CT_enum _ | CT_float _ | CT_rounding_mode | CT_memory_writes ) as ctyp -> + | CT_sbits _ | CT_enum _ | CT_float _ | CT_rounding_mode | CT_memory_writes | CT_json ) as ctyp -> ctyp let rec is_polymorphic = function | CT_lint | CT_fint _ | CT_constant _ | CT_lbits | CT_fbits _ | CT_sbits _ | CT_bit | CT_unit | CT_bool | CT_real - | CT_string | CT_float _ | CT_rounding_mode | CT_memory_writes -> + | CT_string | CT_float _ | CT_rounding_mode | CT_memory_writes | CT_json -> false | CT_tup ctyps -> List.exists is_polymorphic ctyps | CT_enum _ -> false @@ -646,7 +654,7 @@ let rec is_polymorphic = function let rec cval_deps = function | V_id (id, _) -> NameSet.singleton id - | V_lit _ | V_member _ -> NameSet.empty + | V_lit _ | V_member _ | V_config_key _ -> NameSet.empty | V_field (cval, _) | V_tuple_member (cval, _, _) -> cval_deps cval | V_call (_, cvals) | V_tuple (cvals, _) -> List.fold_left NameSet.union NameSet.empty (List.map cval_deps cvals) | V_ctor_kind (cval, _, _) -> cval_deps cval @@ -737,6 +745,7 @@ let rec map_cval_ctyp f = function | V_id (id, ctyp) -> V_id (id, f ctyp) | V_member (id, ctyp) -> V_member (id, f ctyp) | V_lit (vl, ctyp) -> V_lit (vl, f ctyp) + | V_config_key parts -> V_config_key parts | V_ctor_kind (cval, (id, unifiers), ctyp) -> V_ctor_kind (map_cval_ctyp f cval, (id, List.map f unifiers), f ctyp) | V_ctor_unwrap (cval, (id, unifiers), ctyp) -> V_ctor_unwrap (map_cval_ctyp f cval, (id, List.map f unifiers), f ctyp) | V_tuple_member (cval, i, j) -> V_tuple_member (map_cval_ctyp f cval, i, j) @@ -1020,6 +1029,7 @@ and cval_ctyp = function | V_struct (_, ctyp) -> ctyp | V_tuple (_, ctyp) -> ctyp | V_call (op, vs) -> infer_call op vs + | V_config_key _ -> CT_list CT_string let rec clexp_ctyp = function | CL_id (_, ctyp) -> ctyp diff --git a/src/lib/jib_util.mli b/src/lib/jib_util.mli index 535195911..5844b0e29 100644 --- a/src/lib/jib_util.mli +++ b/src/lib/jib_util.mli @@ -77,6 +77,7 @@ val ilabel : ?loc:l -> string -> instr val igoto : ?loc:l -> string -> instr val iundefined : ?loc:l -> ctyp -> instr val imatch_failure : l -> instr +val ibad_config : l -> instr val iexit : l -> instr val iraw : ?loc:l -> string -> instr val ijump : l -> cval -> string -> instr diff --git a/src/lib/jib_visitor.ml b/src/lib/jib_visitor.ml index 9aa68bd58..a2153176d 100644 --- a/src/lib/jib_visitor.ml +++ b/src/lib/jib_visitor.ml @@ -24,7 +24,7 @@ let rec visit_ctyp vis outer_ctyp = let aux vis no_change = match no_change with | CT_lint | CT_fint _ | CT_constant _ | CT_lbits | CT_sbits _ | CT_fbits _ | CT_unit | CT_bool | CT_bit | CT_string - | CT_real | CT_float _ | CT_rounding_mode | CT_memory_writes | CT_poly _ -> + | CT_real | CT_float _ | CT_rounding_mode | CT_memory_writes | CT_poly _ | CT_json -> no_change | CT_tup ctyps -> let ctyps' = visit_ctyps vis ctyps in @@ -164,6 +164,7 @@ let rec visit_cval vis outer_cval = let cval' = visit_cval vis cval in let id' = visit_id vis id in if cval == cval' && id == id' then no_change else V_field (cval', id') + | V_config_key _ -> no_change in do_visit vis (vis#vcval outer_cval) aux outer_cval diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index c3ce11fc2..51f5886dd 100644 --- a/src/lib/lexer.mll +++ b/src/lib/lexer.mll @@ -62,6 +62,7 @@ let kw_table = ("bitone", (fun _ -> Bitone)); ("by", (fun _ -> By)); ("match", (fun _ -> Match)); + ("config", (fun _ -> Config)); ("clause", (fun _ -> Clause)); ("dec", (fun _ -> Dec)); ("operator", (fun _ -> Op)); diff --git a/src/lib/monomorphise.ml b/src/lib/monomorphise.ml index 44dc43965..5d0c7eea3 100644 --- a/src/lib/monomorphise.ml +++ b/src/lib/monomorphise.ml @@ -1048,7 +1048,7 @@ let split_defs target all_errors (splits : split_req list) env ast = let re e = E_aux (e, annot) in match e with | E_block es -> re (E_block (List.map map_exp es)) - | E_id _ | E_lit _ | E_sizeof _ | E_constraint _ | E_ref _ | E_internal_value _ -> ea + | E_id _ | E_lit _ | E_sizeof _ | E_constraint _ | E_ref _ | E_internal_value _ | E_config _ -> ea | E_typ (t, e') -> re (E_typ (t, map_exp e')) | E_app (id, es) -> let es' = List.map map_exp es in @@ -2257,6 +2257,7 @@ module Analysis = struct ) end | E_lit _ -> (dempty, assigns, empty) + | E_config _ -> (dempty, assigns, empty) | E_typ (_, e) -> analyse_sub env assigns e | E_app (id, args) when string_of_id id = "bitvector_length" -> begin match destruct_atom_nexp (env_of_annot (l, annot)) (typ_of_annot (l, annot)) with diff --git a/src/lib/parse_ast.ml b/src/lib/parse_ast.ml index 4765437fb..7a4137d7d 100644 --- a/src/lib/parse_ast.ml +++ b/src/lib/parse_ast.ml @@ -238,6 +238,7 @@ and exp_aux = | E_sizeof of atyp | E_constraint of atyp | E_exit of exp + | E_config of string | E_throw of exp | E_try of exp * pexp list | E_return of exp diff --git a/src/lib/parser.mly b/src/lib/parser.mly index cac4c5b3d..e025b5c90 100644 --- a/src/lib/parser.mly +++ b/src/lib/parser.mly @@ -213,7 +213,7 @@ let set_syntax_deprecated l = /*Terminals with no content*/ -%token And As Assert Bitzero Bitone By Match Clause Dec Default Effect End Op +%token And As Assert Bitzero Bitone By Match Config Clause Dec Default Effect End Op %token Enum Else False Forall Foreach Overload Function_ Mapping If_ In Inc Let_ INT NAT ORDER BOOL Cast %token Pure Impure Monadic Register Return Scattered Sizeof Struct Then True TwoCaret TYPE Typedef %token Undefined Union Newtype With Val Outcome Constraint Throw Try Catch Exit Bitfield Constant @@ -758,6 +758,8 @@ block: atomic_exp: | atomic_exp Colon atomic_typ { mk_exp (E_typ ($3, $1)) $startpos $endpos } + | Config Id + { mk_exp (E_config $2) $startpos $endpos } | lit { mk_exp (E_lit $1) $startpos $endpos } | id MinusGt id Unit diff --git a/src/lib/preprocess.ml b/src/lib/preprocess.ml index 25bf61fd1..81f128eb2 100644 --- a/src/lib/preprocess.ml +++ b/src/lib/preprocess.ml @@ -151,6 +151,7 @@ let all_pragmas = "target_set"; "non_exec"; "c_in_main"; + "c_in_main_post"; ] let wrap_include l file = function diff --git a/src/lib/pretty_print_sail.ml b/src/lib/pretty_print_sail.ml index 83fabe14d..c68334ff8 100644 --- a/src/lib/pretty_print_sail.ml +++ b/src/lib/pretty_print_sail.ml @@ -535,6 +535,7 @@ module Printer (Config : PRINT_CONFIG) = struct | E_id id -> doc_id id | E_ref id -> string "ref" ^^ space ^^ doc_id id | E_field (exp, id) -> doc_atomic_exp exp ^^ dot ^^ doc_id id + | E_config key -> string "config" ^^ space ^^ separate_map dot string key | E_sizeof (Nexp_aux (Nexp_var kid, _)) -> doc_kid kid | E_sizeof nexp -> string "sizeof" ^^ parens (doc_nexp nexp) (* Format a function with a unit argument as f() rather than f(()) *) diff --git a/src/lib/rewriter.ml b/src/lib/rewriter.ml index f4e22a9b6..f391a6b44 100644 --- a/src/lib/rewriter.ml +++ b/src/lib/rewriter.ml @@ -177,7 +177,7 @@ let rewrite_exp rewriters (E_aux (exp, (l, annot))) = let rewrite = rewriters.rewrite_exp rewriters in match exp with | E_block exps -> rewrap (E_block (List.map rewrite exps)) - | E_id _ | E_lit _ -> rewrap exp + | E_id _ | E_lit _ | E_config _ -> rewrap exp | E_typ (typ, exp) -> rewrap (E_typ (typ, rewrite exp)) | E_app (id, exps) -> rewrap (E_app (id, List.map rewrite exps)) | E_app_infix (el, id, er) -> rewrap (E_app_infix (rewrite el, id, rewrite er)) @@ -504,6 +504,7 @@ type ( 'a, e_constraint : n_constraint -> 'exp_aux; e_exit : 'exp -> 'exp_aux; e_throw : 'exp -> 'exp_aux; + e_config : string list -> 'exp_aux; e_return : 'exp -> 'exp_aux; e_assert : 'exp * 'exp -> 'exp_aux; e_var : 'lexp * 'exp * 'exp -> 'exp_aux; @@ -574,6 +575,7 @@ let rec fold_exp_aux alg = function | E_constraint nc -> alg.e_constraint nc | E_exit e -> alg.e_exit (fold_exp alg e) | E_throw e -> alg.e_throw (fold_exp alg e) + | E_config key -> alg.e_config key | E_return e -> alg.e_return (fold_exp alg e) | E_assert (e1, e2) -> alg.e_assert (fold_exp alg e1, fold_exp alg e2) | E_var (lexp, e1, e2) -> alg.e_var (fold_lexp alg lexp, fold_exp alg e1, fold_exp alg e2) @@ -652,6 +654,7 @@ let id_exp_alg = e_constraint = (fun nc -> E_constraint nc); e_exit = (fun e1 -> E_exit e1); e_throw = (fun e1 -> E_throw e1); + e_config = (fun key -> E_config key); e_return = (fun e1 -> E_return e1); e_assert = (fun (e1, e2) -> E_assert (e1, e2)); e_var = (fun (lexp, e2, e3) -> E_var (lexp, e2, e3)); @@ -783,6 +786,7 @@ let compute_exp_alg bot join = e_constraint = (fun nc -> (bot, E_constraint nc)); e_exit = (fun (v1, e1) -> (v1, E_exit e1)); e_throw = (fun (v1, e1) -> (v1, E_throw e1)); + e_config = (fun key -> (bot, E_config key)); e_return = (fun (v1, e1) -> (v1, E_return e1)); e_assert = (fun ((v1, e1), (v2, e2)) -> (join v1 v2, E_assert (e1, e2))); e_var = (fun ((vl, lexp), (v2, e2), (v3, e3)) -> (join_list [vl; v2; v3], E_var (lexp, e2, e3))); @@ -882,6 +886,7 @@ let pure_exp_alg bot join = e_constraint = (fun nc -> bot); e_exit = (fun v1 -> v1); e_throw = (fun v1 -> v1); + e_config = (fun _ -> bot); e_return = (fun v1 -> v1); e_assert = (fun (v1, v2) -> join v1 v2); e_var = (fun (vl, v2, v3) -> join_list [vl; v2; v3]); @@ -997,7 +1002,7 @@ let default_fold_exp f x (E_aux (e, ann) as exp) = (x, []) es in (x, re (E_block (List.rev es))) - | E_id _ | E_ref _ | E_lit _ -> (x, exp) + | E_id _ | E_ref _ | E_lit _ | E_config _ -> (x, exp) | E_typ (typ, e) -> let x, e = f x e in (x, re (E_typ (typ, e))) diff --git a/src/lib/rewriter.mli b/src/lib/rewriter.mli index 6b9146135..7db63e5eb 100644 --- a/src/lib/rewriter.mli +++ b/src/lib/rewriter.mli @@ -159,6 +159,7 @@ type ( 'a, e_constraint : n_constraint -> 'exp_aux; e_exit : 'exp -> 'exp_aux; e_throw : 'exp -> 'exp_aux; + e_config : string list -> 'exp_aux; e_return : 'exp -> 'exp_aux; e_assert : 'exp * 'exp -> 'exp_aux; e_var : 'lexp * 'exp * 'exp -> 'exp_aux; diff --git a/src/lib/rewrites.ml b/src/lib/rewrites.ml index 328705d0e..fa9c33e9c 100644 --- a/src/lib/rewrites.ml +++ b/src/lib/rewrites.ml @@ -2315,9 +2315,10 @@ let rewrite_ast_letbind_effects effect_info env = let pure_rewrap e = purify (rewrap e) in match exp_aux with | E_block es -> failwith "E_block should have been removed till now" - | E_id id -> k exp - | E_ref id -> k exp + | E_id _ -> k exp + | E_ref _ -> k exp | E_lit _ -> k exp + | E_config _ -> k exp | E_typ (typ, exp') -> n_exp_name exp' (fun exp' -> k (pure_rewrap (E_typ (typ, exp')))) | E_app (op_bool, [l; r]) when string_of_id op_bool = "and_bool" || string_of_id op_bool = "or_bool" -> (* Leave effectful operands of Boolean "and"/"or" in place to allow diff --git a/src/lib/smt_gen.ml b/src/lib/smt_gen.ml index da924c61f..5058a9016 100644 --- a/src/lib/smt_gen.ml +++ b/src/lib/smt_gen.ml @@ -427,6 +427,10 @@ module Make (Config : CONFIG) (Primop_gen : PRIMOP_GEN) = struct | V_tuple _ | V_tuple_member _ -> let* l = current_location in Reporting.unreachable l __POS__ "Found tuple value, which should have been removed before SMT generation" + | V_config_key _ -> + let* l = current_location in + Reporting.unreachable l __POS__ + "Found config key value, which should have been removed before SMT generation" ) (* [bvzeint esz cval] (BitVector Zero Extend INTeger), takes a cval diff --git a/src/lib/spec_analysis.ml b/src/lib/spec_analysis.ml index 0f0cbc851..ece9f6a6a 100644 --- a/src/lib/spec_analysis.ml +++ b/src/lib/spec_analysis.ml @@ -182,7 +182,7 @@ let nexp_subst_fns substs = let re e = E_aux (e, (l, s_tannot annot)) in match e with | E_block es -> re (E_block (List.map s_exp es)) - | E_id _ | E_ref _ | E_lit _ | E_internal_value _ -> re e + | E_id _ | E_ref _ | E_lit _ | E_internal_value _ | E_config _ -> re e | E_sizeof ne -> begin let ne' = subst_kids_nexp substs ne in match ne' with Nexp_aux (Nexp_constant i, l) -> re (E_lit (L_aux (L_num i, l))) | _ -> re (E_sizeof ne') diff --git a/src/lib/target.ml b/src/lib/target.ml index 16e4d179a..d1e40a41a 100644 --- a/src/lib/target.ml +++ b/src/lib/target.ml @@ -60,6 +60,7 @@ type target = { action : string option -> istate -> unit; asserts_termination : bool; supports_abstract_types : bool; + supports_runtime_config : bool; } let name tgt = tgt.name @@ -78,6 +79,8 @@ let asserts_termination tgt = tgt.asserts_termination let supports_abstract_types tgt = tgt.supports_abstract_types +let supports_runtime_config tgt = tgt.supports_runtime_config + let registered = ref [] let targets = ref StringMap.empty @@ -85,7 +88,7 @@ let the_target = ref None let register ~name ?flag ?description:desc ?(options = []) ?(pre_parse_hook = fun () -> ()) ?(pre_initial_check_hook = fun _ -> ()) ?(pre_rewrites_hook = fun _ _ _ -> ()) ?(rewrites = []) - ?(asserts_termination = false) ?(supports_abstract_types = false) action = + ?(asserts_termination = false) ?(supports_abstract_types = false) ?(supports_runtime_config = false) action = let set_target () = match !the_target with | None -> the_target := Some name @@ -106,6 +109,7 @@ let register ~name ?flag ?description:desc ?(options = []) ?(pre_parse_hook = fu action; asserts_termination; supports_abstract_types; + supports_runtime_config; } in registered := name :: !registered; diff --git a/src/lib/target.mli b/src/lib/target.mli index d360cd170..a282cc8a8 100644 --- a/src/lib/target.mli +++ b/src/lib/target.mli @@ -98,6 +98,7 @@ val supports_abstract_types : target -> bool @param ?rewrites A sequence of Sail to Sail rewrite passes for the target @param ?asserts_termination Whether termination measures are enforced by assertions in the target @param ?supports_abstract_types Whether the target supports abstract types to be passed to the target + @param ?supports_runtime_config Whether the target supports runtime configuration The final unnamed parameter is the main backend function that is called after the frontend has finished processing the input. @@ -113,6 +114,7 @@ val register : ?rewrites:(string * Rewrites.rewriter_arg list) list -> ?asserts_termination:bool -> ?supports_abstract_types:bool -> + ?supports_runtime_config:bool -> (string option -> Interactive.State.istate -> unit) -> target diff --git a/src/lib/type_check.ml b/src/lib/type_check.ml index 88d344822..d9b107f7c 100644 --- a/src/lib/type_check.ml +++ b/src/lib/type_check.ml @@ -2282,6 +2282,7 @@ let rec check_exp env (E_aux (exp_aux, (l, uannot)) as exp : uannot exp) (Typ_au | None -> typ_error l "Cannot use return outside a function" in annot_exp (E_return checked_exp) typ + | E_config key, _ -> annot_exp (E_config key) typ | E_tuple exps, Typ_tuple typs when List.length exps = List.length typs -> let checked_exps = List.map2 (fun exp typ -> crule check_exp env exp typ) exps typs in annot_exp (E_tuple checked_exps) typ diff --git a/src/sail_c_backend/c_backend.ml b/src/sail_c_backend/c_backend.ml index 2db3bbc7e..ff859cb4c 100644 --- a/src/sail_c_backend/c_backend.ml +++ b/src/sail_c_backend/c_backend.ml @@ -124,6 +124,8 @@ let rec is_stack_ctyp ctyp = | CT_poly _ -> true | CT_float _ -> true | CT_rounding_mode -> true + (* Is a reference to some immutable JSON data *) + | CT_json -> true | CT_constant n -> Big_int.less_equal (min_int 64) n && Big_int.greater_equal n (max_int 64) | CT_memory_writes -> false @@ -185,6 +187,7 @@ let rec sgen_ctyp_name = function | CT_fvector (_, typ) -> sgen_ctyp_name (CT_vector typ) | CT_string -> "sail_string" | CT_real -> "real" + | CT_json -> "sail_config_json" | CT_ref ctyp -> "ref_" ^ sgen_ctyp_name ctyp | CT_float n -> "float" ^ string_of_int n | CT_rounding_mode -> "rounding_mode" @@ -462,7 +465,7 @@ end) : CONFIG = struct AE_aux (aexp, annot) let analyze_primop' ctx id args typ = - let no_change = AE_app (id, args, typ) in + let no_change = AE_app (Sail_function id, args, typ) in let args = List.map (c_aval ctx) args in let extern = if ctx_is_extern id ctx then ctx_get_extern id ctx else failwith "Not extern" in @@ -564,7 +567,10 @@ end) : CONFIG = struct let analyze_primop ctx id args typ = let no_change = AE_app (id, args, typ) in - if !optimize_primops then (try analyze_primop' ctx id args typ with Failure _ -> no_change) else no_change + match id with + | Sail_function id -> + if !optimize_primops then (try analyze_primop' ctx id args typ with Failure _ -> no_change) else no_change + | _ -> no_change let optimize_anf ctx aexp = analyze_functions ctx analyze_primop (c_literals ctx aexp) @@ -918,6 +924,7 @@ let rec sgen_ctyp = function | CT_fvector (_, typ) -> sgen_ctyp (CT_vector typ) | CT_string -> "sail_string" | CT_real -> "real" + | CT_json -> "sail_config_json" | CT_ref ctyp -> sgen_ctyp ctyp ^ "*" | CT_float n -> "float" ^ string_of_int n ^ "_t" | CT_rounding_mode -> "uint_fast8_t" @@ -963,6 +970,8 @@ let rec sgen_cval = function Printf.sprintf "{%s}" (Util.string_of_list ", " (fun (field, cval) -> zencode_id field ^ " = " ^ sgen_cval cval) fields) | V_ctor_unwrap (f, ctor, _) -> Printf.sprintf "%s.variants.%s" (sgen_cval f) (sgen_uid ctor) + | V_config_key parts -> + Printf.sprintf "(const_sail_string[]){%s}" (Util.string_of_list ", " (fun part -> "\"" ^ part ^ "\"") parts) | V_tuple _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Cannot generate C value for a tuple literal" and sgen_call op cvals = @@ -1252,9 +1261,9 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) = match (fname, ctyp) with | "internal_pick", _ -> Printf.sprintf "pick_%s" (sgen_ctyp_name ctyp) | "sail_cons", _ -> begin - match snd f with - | [ctyp] -> Util.zencode_string ("cons#" ^ string_of_ctyp ctyp) - | _ -> c_error "cons without specified type" + match Option.map cval_ctyp (List.nth_opt args 0) with + | Some ctyp -> Util.zencode_string ("cons#" ^ string_of_ctyp (ctyp_suprema ctyp)) + | None -> c_error "cons without specified type" end | "eq_anything", _ -> begin match args with @@ -2029,7 +2038,7 @@ let rec ctyp_dependencies = function | CT_struct (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors) | CT_variant (_, ctors) -> List.concat (List.map (fun (_, ctyp) -> ctyp_dependencies ctyp) ctors) | CT_lint | CT_fint _ | CT_lbits | CT_fbits _ | CT_sbits _ | CT_unit | CT_bool | CT_real | CT_bit | CT_string - | CT_enum _ | CT_poly _ | CT_constant _ | CT_float _ | CT_rounding_mode | CT_memory_writes -> + | CT_enum _ | CT_poly _ | CT_constant _ | CT_float _ | CT_rounding_mode | CT_memory_writes | CT_json -> [] let codegen_ctg = function @@ -2079,7 +2088,6 @@ let jib_of_ast env effect_info ast = let module Jibc = Make (C_config (struct let branch_coverage = !opt_branch_coverage end)) in - let env, effect_info = add_special_functions env effect_info in let ctx = initial_ctx env effect_info in Jibc.compile_ast ctx ast @@ -2212,14 +2220,21 @@ let compile_ast env effect_info output_chan c_includes ast = in let model_main = - let extra = + let extra_pre = List.filter_map (function CDEF_aux (CDEF_pragma ("c_in_main", arg), _) -> Some (" " ^ arg) | _ -> None) cdefs in + let extra_post = + List.filter_map + (function CDEF_aux (CDEF_pragma ("c_in_main_post", arg), _) -> Some (" " ^ arg) | _ -> None) + cdefs + in separate hardline ( if !opt_no_main then [] else List.map string - (["int main(int argc, char *argv[])"; "{"] @ extra @ [" return model_main(argc, argv);"; "}"]) + (["int main(int argc, char *argv[])"; "{"; " int retcode;"] + @ extra_pre @ [" retcode = model_main(argc, argv);"] @ extra_post @ [" return retcode;"; "}"] + ) ) in let end_extern_cpp = separate hardline (List.map string [""; "#ifdef __cplusplus"; "}"; "#endif"]) in diff --git a/src/sail_c_backend/sail_plugin_c.ml b/src/sail_c_backend/sail_plugin_c.ml index 13670e812..ae85d32af 100644 --- a/src/sail_c_backend/sail_plugin_c.ml +++ b/src/sail_c_backend/sail_plugin_c.ml @@ -151,4 +151,6 @@ let c_target out_file { ast; effect_info; env; _ } = flush output_chan; if close then close_out output_chan -let _ = Target.register ~name:"c" ~options:c_options ~rewrites:c_rewrites ~supports_abstract_types:true c_target +let _ = + Target.register ~name:"c" ~options:c_options ~rewrites:c_rewrites ~supports_abstract_types:true + ~supports_runtime_config:true c_target diff --git a/src/sail_coq_backend/pretty_print_coq.ml b/src/sail_coq_backend/pretty_print_coq.ml index 7a5a72b88..4b652fa51 100644 --- a/src/sail_coq_backend/pretty_print_coq.ml +++ b/src/sail_coq_backend/pretty_print_coq.ml @@ -2199,6 +2199,9 @@ let doc_exp, doc_let = | E_constraint nc -> wrap_parens (doc_nc_exp ctxt (env_of full_exp) nc) | E_internal_assume (nc, e1) -> string "(* " ^^ doc_nc_exp ctxt (env_of full_exp) nc ^^ string " *)" ^/^ wrap_parens (expN e1) + | E_config _ -> + raise + (Reporting.err_unreachable l __POS__ "Configuration expression should have been removed before Coq generation") | E_internal_value _ -> raise (Reporting.err_unreachable l __POS__ "unsupported internal expression encountered while pretty-printing") (* TODO: no dep pairs now, what should this be? *) diff --git a/src/sail_doc_backend/html_source.ml b/src/sail_doc_backend/html_source.ml index b60336933..6d620bc68 100644 --- a/src/sail_doc_backend/html_source.ml +++ b/src/sail_doc_backend/html_source.ml @@ -89,7 +89,7 @@ let highlights ~filename ~contents = | And | As | Assert | By | Match | Clause | Dec | Op | Default | Effect | End | Enum | Else | Exit | Cast | Forall | Foreach | Function_ | Mapping | Overload | Throw | Try | Catch | If_ | In | Inc | Var | Ref | Pure | Impure | Monadic | Register | Return | Scattered | Sizeof | Constraint | Constant | Struct | Then | Typedef | Union - | Newtype | With | Val | Outcome | Instantiation | Impl | Private | Repeat | Until | While | Do | Mutual + | Newtype | With | Val | Outcome | Instantiation | Impl | Private | Repeat | Until | While | Do | Mutual | Config | Configuration | TerminationMeasure | Forwards | Backwards | Let_ | Bitfield -> mark Highlight.Keyword; go () diff --git a/src/sail_lean_backend/pretty_print_lean.ml b/src/sail_lean_backend/pretty_print_lean.ml index bd49c7009..0b5bd4b42 100644 --- a/src/sail_lean_backend/pretty_print_lean.ml +++ b/src/sail_lean_backend/pretty_print_lean.ml @@ -187,6 +187,7 @@ let string_of_exp_con (E_aux (e, _)) = | E_tuple _ -> "E_tuple" | E_vector _ -> "E_vector" | E_let _ -> "E_let" + | E_config _ -> "E_config" let rec doc_exp (E_aux (e, (l, annot)) as full_exp) = let env = env_of_tannot annot in diff --git a/src/sail_lem_backend/pretty_print_lem.ml b/src/sail_lem_backend/pretty_print_lem.ml index 403c3094f..ef00092af 100644 --- a/src/sail_lem_backend/pretty_print_lem.ml +++ b/src/sail_lem_backend/pretty_print_lem.ml @@ -1149,6 +1149,9 @@ let doc_exp_lem, doc_let_lem = | E_constraint _ -> string "true" | E_internal_assume (nc, e1) -> string "(* " ^^ string (string_of_n_constraint nc) ^^ string " *)" ^/^ wrap_parens (expN e1) + | E_config _ -> + raise + (Reporting.err_unreachable l __POS__ "Configuration expression should have been removed before Lem generation") | E_internal_value _ -> raise (Reporting.err_unreachable l __POS__ "unsupported internal expression encountered while pretty-printing") and if_exp ctxt (elseif : bool) c t e = diff --git a/src/sail_smt_backend/jib_smt.ml b/src/sail_smt_backend/jib_smt.ml index 6f7f04aa4..4ba3b7917 100644 --- a/src/sail_smt_backend/jib_smt.ml +++ b/src/sail_smt_backend/jib_smt.ml @@ -327,21 +327,12 @@ module Make (Config : CONFIG) = struct let* l = Smt_gen.current_location in Reporting.unreachable l __POS__ ("No registers with ctyp: " ^ string_of_ctyp ctyp) end - | CT_list _ -> + | CT_list _ | CT_float _ -> let* l = Smt_gen.current_location in - raise (Reporting.err_todo l "Lists not yet supported in SMT generation") - | CT_float _ | CT_rounding_mode -> + raise (Reporting.err_todo l "Lists and floats not yet supported in SMT generation") + | (CT_rounding_mode | CT_tup _ | CT_poly _ | CT_memory_writes | CT_json) as ctyp -> let* l = Smt_gen.current_location in - Reporting.unreachable l __POS__ "Floating point in SMT property" - | CT_tup _ -> - let* l = Smt_gen.current_location in - Reporting.unreachable l __POS__ "Tuples should be re-written before SMT generation" - | CT_poly _ -> - let* l = Smt_gen.current_location in - Reporting.unreachable l __POS__ "Found polymorphic type in SMT property" - | CT_memory_writes -> - let* l = Smt_gen.current_location in - Reporting.unreachable l __POS__ "Found memory writes type in SMT property" + ksprintf (Reporting.unreachable l __POS__) "Found unsupported type %s in SMT generation" (string_of_ctyp ctyp) (* When generating SMT when we encounter joins between two or more blocks such as in the example below, we have to generate a muxer @@ -527,21 +518,13 @@ module Make (Config : CONFIG) = struct | I_funcall (CR_one (CL_id (id, ret_ctyp)), extern, (function_id, _), args) -> if ctx_is_extern function_id ctx then ( let name = ctx_get_extern function_id ctx in - if name = "sail_assert" then ( - match args with - | [assertion; _] -> - let* smt = Smt.smt_cval assertion in - let* _ = add_event state Assertion (Fn ("not", [smt])) in - return [] - | _ -> Reporting.unreachable l __POS__ "Bad arguments for assertion" - ) - else if name = "sail_assume" then ( + if name = "sail_assume" then ( match args with | [assumption] -> let* smt = Smt.smt_cval assumption in let* _ = add_event state Assumption smt in return [] - | _ -> Reporting.unreachable l __POS__ "Bad arguments for assertion" + | _ -> Reporting.unreachable l __POS__ "Bad arguments for sail_assume" ) else if name = "sqrt_real" then ( match args with @@ -556,6 +539,14 @@ module Make (Config : CONFIG) = struct | None -> raise (Reporting.err_general l ("No generator " ^ string_of_id function_id)) ) ) + else if extern && string_of_id function_id = "sail_assert" then ( + match args with + | [assertion; _] -> + let* smt = Smt.smt_cval assertion in + let* _ = add_event state Assertion (Fn ("not", [smt])) in + return [] + | _ -> Reporting.unreachable l __POS__ "Bad arguments for assertion" + ) else if extern && string_of_id function_id = "internal_vector_init" then singleton (declare_const id ret_ctyp) else if extern && string_of_id function_id = "internal_vector_update" then ( match args with @@ -1346,7 +1337,6 @@ let compile ~unroll_limit env effect_info ast = let module Jibc = Jib_compile.Make (CompileConfig (struct let unroll_limit = unroll_limit end)) in - let env, effect_info = Jib_compile.add_special_functions env effect_info in let ctx = Jib_compile.initial_ctx ~for_target:"c" env effect_info in let t = Profile.start () in let cdefs, ctx = Jibc.compile_ast ctx ast in diff --git a/src/sail_sv_backend/jib_sv.ml b/src/sail_sv_backend/jib_sv.ml index c7fab8e5b..db291c737 100644 --- a/src/sail_sv_backend/jib_sv.ml +++ b/src/sail_sv_backend/jib_sv.ml @@ -273,7 +273,11 @@ class footprint_visitor ctx registers (footprint : direct_footprint) : jib_visit | I_aux (I_exit _, _) -> footprint.exits <- true; SkipChildren - | I_aux (I_funcall (_, _, (id, _), args), (l, _)) -> + | I_aux (I_funcall (_, true, (id, _), args), (l, _)) -> + let name = string_of_id id in + if name = "sail_assert" then footprint.contains_assert <- true; + DoChildren + | I_aux (I_funcall (_, false, (id, _), args), (l, _)) -> let open Util.Option_monad in if ctx_is_extern id ctx then ( let name = ctx_get_extern id ctx in @@ -297,7 +301,6 @@ class footprint_visitor ctx registers (footprint : direct_footprint) : jib_visit end | _ -> () ) - else if name = "sail_assert" then footprint.contains_assert <- true ); DoChildren | _ -> DoChildren @@ -673,6 +676,7 @@ module Make (Config : CONFIG) = struct | CT_memory_writes -> simple_type "sail_memory_writes" | CT_tup _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Tuple type should not reach SV backend" | CT_poly _ -> Reporting.unreachable Parse_ast.Unknown __POS__ "Polymorphic type should not reach SV backend" + | CT_json -> Reporting.unreachable Parse_ast.Unknown __POS__ "JSON type should not reach SV backend" module Smt = Smt_gen.Make @@ -1215,6 +1219,61 @@ module Make (Config : CONFIG) = struct ) (List.combine args (List.combine arg_ctyps conversions)) + let extern_generate l ctx creturn id name args = + let wrap aux = return (Some (SVS_aux (aux, l))) in + match Smt.builtin ~allow_io:false name with + | Some generator -> + let clexp = + match creturn with + | CR_one clexp -> clexp + | CR_multi clexps -> + Reporting.unreachable l __POS__ + (sprintf "Multiple return generator primitive found: %s (%s)" name + (Util.string_of_list ", " string_of_clexp clexps) + ) + in + let* value = Smt_gen.fmap (Smt_exp.simp SimpSet.empty) (generator args (clexp_ctyp clexp)) in + begin + (* We can optimize R = store(R, i x) into R[i] = x *) + match (clexp, value) with + | CL_id (v, _), Store (_, _, Var v', i, x) when Name.compare v v' = 0 -> + wrap (SVS_assign (SVP_index (SVP_id v, i), x)) + | _, _ -> + let updates, lexp = svir_clexp clexp in + wrap (with_updates l updates (SVS_assign (lexp, value))) + end + | None -> ( + match Primops.generate_module ~at:l name with + | Some generator -> + let generated_name = generator args (creturn_ctyp creturn) in + let* args = mapM Smt.smt_cval args in + let updates, ret = svir_creturn creturn in + wrap (with_updates l updates (SVS_call (ret, SVN_string generated_name, args))) + | None -> + let _, _, _, uannot = Bindings.find id ctx.valspecs in + let arity = List.length args in + let* arg_convs, ret_conv, is_function = + match get_sv_attribute "sv_module" uannot with + | Some obj, (module ModuleAttr) -> + let module Attr = AttributeParser (ModuleAttr) in + let types = Attr.get_types ~arity (Some obj) in + let return_type = Attr.get_return_type (Some obj) in + return (types, return_type, false) + | None, _ -> + let attr, (module FunctionAttr) = get_sv_attribute "sv_function" uannot in + let module Attr = AttributeParser (FunctionAttr) in + let types = Attr.get_types ~arity attr in + let return_type = Attr.get_return_type attr in + return (types, return_type, true) + in + let* args = fmap (List.map fst) (convert_arguments args arg_convs) in + let* aux = + if is_function then convert_return l creturn (fun ret -> SVS_assign (ret, Fn (name, args))) ret_conv + else convert_return l creturn (fun ret -> SVS_call (ret, SVN_string name, args)) ret_conv + in + wrap aux + ) + let rec svir_instr ?pathcond spec_info ctx (I_aux (aux, (_, l))) = let wrap aux = return (Some (SVS_aux (aux, l))) in match aux with @@ -1238,84 +1297,28 @@ module Make (Config : CONFIG) = struct | I_funcall (creturn, preserve_name, (id, _), args) -> if ctx_is_extern id ctx then ( let name = ctx_get_extern id ctx in - if name = "sail_assert" then - if Config.no_assertions then wrap SVS_skip - else ( - let _, ret = svir_creturn creturn in - match args with - | [cond; msg] -> - let* cond = Smt.smt_cval cond in - let* msg = Smt.smt_cval msg in - (* If the assert is only reachable under some path-condition, then the assert should pass - whenever the path-condition is not true. *) - let cond = - match pathcond with - | Some pathcond -> - Fn - ( "or", - [Fn ("not", [pathcond]); Fn ("not", [Var (Name (mk_id "assert_reachable#", -1))]); cond] - ) - | None -> cond - in - wrap (SVS_block [SVS_aux (SVS_assert (cond, msg), l); SVS_aux (SVS_assign (ret, Unit), l)]) - | _ -> Reporting.unreachable l __POS__ "Invalid arguments for sail_assert" - ) + extern_generate l ctx creturn id name args + ) + else if Id.compare id (mk_id "sail_assert") = 0 then + if Config.no_assertions then wrap SVS_skip else ( - match Smt.builtin ~allow_io:false name with - | Some generator -> - let clexp = - match creturn with - | CR_one clexp -> clexp - | CR_multi clexps -> - Reporting.unreachable l __POS__ - (sprintf "Multiple return generator primitive found: %s (%s)" name - (Util.string_of_list ", " string_of_clexp clexps) - ) + let _, ret = svir_creturn creturn in + match args with + | [cond; msg] -> + let* cond = Smt.smt_cval cond in + let* msg = Smt.smt_cval msg in + (* If the assert is only reachable under some path-condition, then the assert should pass + whenever the path-condition is not true. *) + let cond = + match pathcond with + | Some pathcond -> + Fn ("or", [Fn ("not", [pathcond]); Fn ("not", [Var (Name (mk_id "assert_reachable#", -1))]); cond]) + | None -> cond in - let* value = Smt_gen.fmap (Smt_exp.simp SimpSet.empty) (generator args (clexp_ctyp clexp)) in - begin - (* We can optimize R = store(R, i x) into R[i] = x *) - match (clexp, value) with - | CL_id (v, _), Store (_, _, Var v', i, x) when Name.compare v v' = 0 -> - wrap (SVS_assign (SVP_index (SVP_id v, i), x)) - | _, _ -> - let updates, lexp = svir_clexp clexp in - wrap (with_updates l updates (SVS_assign (lexp, value))) - end - | None -> ( - match Primops.generate_module ~at:l name with - | Some generator -> - let generated_name = generator args (creturn_ctyp creturn) in - let* args = mapM Smt.smt_cval args in - let updates, ret = svir_creturn creturn in - wrap (with_updates l updates (SVS_call (ret, SVN_string generated_name, args))) - | None -> - let _, _, _, uannot = Bindings.find id ctx.valspecs in - let arity = List.length args in - let* arg_convs, ret_conv, is_function = - match get_sv_attribute "sv_module" uannot with - | Some obj, (module ModuleAttr) -> - let module Attr = AttributeParser (ModuleAttr) in - let types = Attr.get_types ~arity (Some obj) in - let return_type = Attr.get_return_type (Some obj) in - return (types, return_type, false) - | None, _ -> - let attr, (module FunctionAttr) = get_sv_attribute "sv_function" uannot in - let module Attr = AttributeParser (FunctionAttr) in - let types = Attr.get_types ~arity attr in - let return_type = Attr.get_return_type attr in - return (types, return_type, true) - in - let* args = fmap (List.map fst) (convert_arguments args arg_convs) in - let* aux = - if is_function then - convert_return l creturn (fun ret -> SVS_assign (ret, Fn (name, args))) ret_conv - else convert_return l creturn (fun ret -> SVS_call (ret, SVN_string name, args)) ret_conv - in - wrap aux - ) + wrap (SVS_block [SVS_aux (SVS_assert (cond, msg), l); SVS_aux (SVS_assign (ret, Unit), l)]) + | _ -> Reporting.unreachable l __POS__ "Invalid arguments for sail_assert" ) - ) + else if Id.compare id (mk_id "sail_cons") = 0 then extern_generate l ctx creturn id "sail_cons" args else if Id.compare id (mk_id "update_fbits") = 0 then let* rhs = svir_update_fbits args in let updates, ret = svir_creturn creturn in diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml index bdda41ed3..67d02bfdf 100644 --- a/src/sail_sv_backend/sail_plugin_sv.ml +++ b/src/sail_sv_backend/sail_plugin_sv.ml @@ -368,7 +368,6 @@ let jib_of_ast make_call_precise env ast effect_info = let module Jibc = Make (Verilog_config (struct let make_call_precise = make_call_precise end)) in - let env, effect_info = add_special_functions env effect_info in let ctx = initial_ctx env effect_info in Jibc.compile_ast ctx ast diff --git a/test/c/config_test.expect b/test/c/config_test.expect new file mode 100644 index 000000000..552f5a1ed --- /dev/null +++ b/test/c/config_test.expect @@ -0,0 +1,3 @@ +Hello, World! +n = 13438537428731902344561435823034520154709854735643 +bv = 0b10000 diff --git a/test/c/config_test.json b/test/c/config_test.json new file mode 100644 index 000000000..d4ac01466 --- /dev/null +++ b/test/c/config_test.json @@ -0,0 +1,7 @@ +{ + "hello": { + "world": "Hello, World!", + "number": "13438537428731902344561435823034520154709854735643", + "bits" : [true, false, false, false, false] + } +} diff --git a/test/c/config_test.sail b/test/c/config_test.sail new file mode 100644 index 000000000..5412508e7 --- /dev/null +++ b/test/c/config_test.sail @@ -0,0 +1,22 @@ +default Order dec + +$include + +$iftarget c +$c_in_main sail_config_set_file("config_test.json"); +$c_in_main_post sail_config_cleanup(); +$else +$option --config ../c/config_test.json +$endif + +$iftarget systemverilog +$option --sv-int-size 256 +$endif + +val main : unit -> unit + +function main() = { + print_endline(config hello.world); + print_int("n = ", config hello.number : int); + print_bits("bv = ", config hello.bits : bits(5)); +} diff --git a/test/c/run_tests.py b/test/c/run_tests.py index 3eb967bac..d886b4288 100755 --- a/test/c/run_tests.py +++ b/test/c/run_tests.py @@ -13,7 +13,7 @@ sail_dir = get_sail_dir() sail = get_sail() -targets = get_targets(['c', 'interpreter', 'ocaml']) +targets = get_targets(['c', 'cpp', 'interpreter', 'ocaml']) print("Sail is {}".format(sail)) print("Sail dir is {}".format(sail_dir)) @@ -38,6 +38,9 @@ def test_c(name, c_opts, sail_opts, valgrind, compiler='cc'): basename = os.path.splitext(os.path.basename(filename))[0] tests[filename] = os.fork() if tests[filename] == 0: + if basename.startswith('config'): + sail_opts += ' --c-include sail_config.h' + c_opts += ' \'{}\'/lib/json/*.c -I \'{}\'/lib/json'.format(sail_dir, sail_dir) step('\'{}\' -no_warn -c {} {} 1> {}.c'.format(sail, sail_opts, filename, basename)) step('{} {} {}.c \'{}\'/lib/*.c -lgmp -I \'{}\'/lib -o {}.bin'.format(compiler, c_opts, basename, sail_dir, sail_dir, basename)) step('./{}.bin > {}.result 2> {}.err_result'.format(basename, basename, basename), expected_status = 1 if basename.startswith('fail') else 0) @@ -203,13 +206,15 @@ def test_coq(name): if 'c' in targets: #xml += test_c2('unoptimized C', '', '', True) xml += test_c('unoptimized C', '', '', False) - xml += test_c('unoptimized C with C++ compiler', '-xc++', '', False, compiler='c++') xml += test_c('optimized C', '-O2', '-O', True) - xml += test_c('optimized C with C++ compiler', '-xc++ -O2', '-O', True, compiler='c++') xml += test_c('constant folding', '', '-Oconstant_fold', False) #xml += test_c('monomorphised C', '-O2', '-O -Oconstant_fold -auto_mono', True) xml += test_c('undefined behavior sanitised', '-O2 -fsanitize=undefined', '-O', False) +if 'cpp' in targets: + xml += test_c('unoptimized C with C++ compiler', '-xc++', '', False, compiler='c++') + xml += test_c('optimized C with C++ compiler', '-xc++ -O2', '-O', True, compiler='c++') + if 'interpreter' in targets: xml += test_interpreter('interpreter') diff --git a/test/typecheck/fail/config_mismatch.expect b/test/typecheck/fail/config_mismatch.expect new file mode 100644 index 000000000..c0da1dcbf --- /dev/null +++ b/test/typecheck/fail/config_mismatch.expect @@ -0,0 +1,11 @@ +Type error: +fail/config_mismatch.sail:9.18-28: +9 | print_int("", config a.b : int); +  | ^--------^ +  | Incompatible types for configuration option found: +  | * Type int found here +  | * Type string found as previous type +  | +  | fail/config_mismatch.sail:8.18-28: +  | 8 | print_endline(config a.b); +  |  | ^--------^ previous type found here diff --git a/test/typecheck/fail/config_mismatch.sail b/test/typecheck/fail/config_mismatch.sail new file mode 100644 index 000000000..2242bd8c0 --- /dev/null +++ b/test/typecheck/fail/config_mismatch.sail @@ -0,0 +1,10 @@ +default Order dec + +$include + +val main : unit -> unit + +function main() = { + print_endline(config a.b); + print_int("", config a.b : int); +} diff --git a/test/typecheck/fail/config_non_bit.expect b/test/typecheck/fail/config_non_bit.expect new file mode 100644 index 000000000..7c2e1ccea --- /dev/null +++ b/test/typecheck/fail/config_non_bit.expect @@ -0,0 +1,5 @@ +Error: +fail/config_non_bit.sail:10.20-28: +10 | let _ : bits(5) = config k +  | ^------^ +  | Failed to interpret "not a bit" as a bit diff --git a/test/typecheck/fail/config_non_bit.json b/test/typecheck/fail/config_non_bit.json new file mode 100644 index 000000000..8b09e7068 --- /dev/null +++ b/test/typecheck/fail/config_non_bit.json @@ -0,0 +1,3 @@ +{ + "k" : [true, false, false, true, "not a bit"] +} diff --git a/test/typecheck/fail/config_non_bit.sail b/test/typecheck/fail/config_non_bit.sail new file mode 100644 index 000000000..910ff477d --- /dev/null +++ b/test/typecheck/fail/config_non_bit.sail @@ -0,0 +1,11 @@ +default Order dec + +$include + +$option --config fail/config_non_bit.json + +val main : unit -> unit + +function main() = { + let _ : bits(5) = config k +} diff --git a/test/typecheck/fail/config_subkey.expect b/test/typecheck/fail/config_subkey.expect new file mode 100644 index 000000000..f5b385f8f --- /dev/null +++ b/test/typecheck/fail/config_subkey.expect @@ -0,0 +1,10 @@ +Error: +fail/config_subkey.sail:9.18-28: +9 | print_endline(config a.b : string); +  | ^--------^ +  | Attempting to access key a.b, but various subkeys have already been used +  | +  | For example: +  | fail/config_subkey.sail:8.18-30: +  | 8 | print_endline(config a.b.c : string); +  |  | ^----------^ used here diff --git a/test/typecheck/fail/config_subkey.sail b/test/typecheck/fail/config_subkey.sail new file mode 100644 index 000000000..efd1a4474 --- /dev/null +++ b/test/typecheck/fail/config_subkey.sail @@ -0,0 +1,10 @@ +default Order dec + +$include + +val main : unit -> unit + +function main() = { + print_endline(config a.b.c : string); + print_endline(config a.b : string); +}