From fc9602cc5fdb4b628204a0f50908a8bc5fa8a377 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 16 Oct 2024 11:20:57 -0500 Subject: [PATCH] a few minor fixes to support the ULM better (#1157) * some improved function prototypes in header files * make BLOCK_SIZE a macro * extract out some basic header file content to its own file that does not declare any undefined symbols * better support for serialization/deserialization --- bindings/c/include/kllvm-c/kllvm-c.h | 2 + bindings/c/lib.cpp | 1 - include/runtime/alloc.h | 2 +- include/runtime/collect.h | 1 + include/runtime/header.h | 180 ++--------------------- include/runtime/types.h | 163 ++++++++++++++++++++ lib/codegen/EmitConfigParser.cpp | 4 +- runtime/alloc/arena.cpp | 2 +- runtime/util/ConfigurationParser.cpp | 13 ++ runtime/util/ConfigurationSerializer.cpp | 54 ++++--- unittests/runtime-arithmetic/inttest.cpp | 1 - unittests/runtime-collections/lists.cpp | 1 - unittests/runtime-strings/CMakeLists.txt | 2 +- 13 files changed, 231 insertions(+), 195 deletions(-) create mode 100644 include/runtime/types.h diff --git a/bindings/c/include/kllvm-c/kllvm-c.h b/bindings/c/include/kllvm-c/kllvm-c.h index 43a5263f5..8531f68cb 100644 --- a/bindings/c/include/kllvm-c/kllvm-c.h +++ b/bindings/c/include/kllvm-c/kllvm-c.h @@ -131,6 +131,8 @@ void kore_simplify_binary( block *take_steps(int64_t depth, block *term); +void init_static_objects(void); + /* kore_sort */ char *kore_sort_dump(kore_sort const *); diff --git a/bindings/c/lib.cpp b/bindings/c/lib.cpp index 7c65ee793..9613289d9 100644 --- a/bindings/c/lib.cpp +++ b/bindings/c/lib.cpp @@ -67,7 +67,6 @@ auto managed(kore_symbol *ptr) { */ extern "C" { -void init_static_objects(); void free_all_kore_mem(); bool hook_BYTES_mutableBytesEnabled(); } diff --git a/include/runtime/alloc.h b/include/runtime/alloc.h index b625b4363..d94ed0c5b 100644 --- a/include/runtime/alloc.h +++ b/include/runtime/alloc.h @@ -7,7 +7,7 @@ extern "C" { // The maximum single allocation size in bytes. // A contiguous area larger than that size cannot be allocated in any arena. -extern size_t const BLOCK_SIZE; +#define BLOCK_SIZE (1024 * 1024) #define YOUNGSPACE_ID 0 #define OLDSPACE_ID 1 diff --git a/include/runtime/collect.h b/include/runtime/collect.h index 4324870ba..a4ef7d2b0 100644 --- a/include/runtime/collect.h +++ b/include/runtime/collect.h @@ -39,6 +39,7 @@ void migrate_set(void *s); void migrate_collection_node(void **node_ptr); void set_kore_memory_functions_for_gmp(void); void kore_collect(void **, uint8_t, layoutitem *, bool force = false); +void free_all_kore_mem(); } #ifdef GC_DBG diff --git a/include/runtime/header.h b/include/runtime/header.h index 366afa414..000ec7cd2 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -6,14 +6,11 @@ #include #include -#include -#include - #include #include "config/macros.h" -#include "runtime/alloc.h" #include "runtime/fmt_error_handling.h" +#include "runtime/types.h" #ifndef IMMER_TAGGED_NODE #define IMMER_TAGGED_NODE 0 @@ -42,68 +39,7 @@ struct match_log { #define STRUCT_BASE(struct_type, member_name, member_addr) \ ((struct_type *)((char *)(member_addr)-offsetof(struct_type, member_name))) - extern "C" { -// llvm: blockheader = type { i64 } -using blockheader = struct blockheader { - uint64_t hdr; -}; - -// A value b of type block* is either a constant or a block. -// if (((uintptr_t)b) & 3) == 3, then it is a bound variable and -// ((uintptr_t)b) >> 32 is the debruijn index. If ((uintptr_t)b) & 3 == 1) -// then it is a symbol with 0 arguments and ((uintptr_t)b) >> 32 is the tag -// of the symbol. Otherwise, if ((uintptr_t)b) & 1 == 0 then it is a pointer to -// a block. -// llvm: block = type { %blockheader, [0 x i64 *] } -using block = struct block { - blockheader h; - uint64_t *children[]; -}; - -// llvm: string = type { %blockheader, [0 x i8] } -using string = struct string { - blockheader h; - char data[]; -}; - -// llvm: stringbuffer = type { i64, i64, %string* } -using stringbuffer = struct stringbuffer { - blockheader h; - uint64_t strlen; - string *contents; -}; - -using mpz_hdr = struct mpz_hdr { - blockheader h; - mpz_t i; -}; - -using floating = struct floating { - uint64_t exp; // number of bits in exponent range - mpfr_t f; -}; - -using floating_hdr = struct floating_hdr { - blockheader h; - floating f; -}; - -using layoutitem = struct layoutitem { - uint64_t offset; - uint16_t cat; -}; - -using layout = struct layout { - uint8_t nargs; - layoutitem *args; -}; - -using writer = struct { - FILE *file; - stringbuffer *buffer; -}; - bool hook_KEQUAL_lt(block *, block *); bool hook_KEQUAL_eq(block *, block *); bool during_gc(void); @@ -115,82 +51,6 @@ void hash_exit(void); extern bool gc_enabled; } -__attribute__((always_inline)) constexpr uint64_t len_hdr(uint64_t hdr) { - return hdr & LENGTH_MASK; -} - -template -__attribute__((always_inline)) constexpr uint64_t len(T const *s) { - return len_hdr(s->h.hdr); -} - -template -__attribute__((always_inline)) constexpr void init_with_len(T *s, uint64_t l) { - s->h.hdr = l | (l > BLOCK_SIZE - sizeof(char *) ? NOT_YOUNG_OBJECT_BIT : 0); -} - -__attribute__((always_inline)) constexpr uint64_t size_hdr(uint64_t hdr) { - return ((hdr >> 32) & 0xff) * 8; -} - -__attribute__((always_inline)) constexpr uint64_t layout_hdr(uint64_t hdr) { - return hdr >> LAYOUT_OFFSET; -} - -template -__attribute__((always_inline)) constexpr uint64_t get_layout(T const *s) { - return layout_hdr((s)->h.hdr); -} - -__attribute__((always_inline)) constexpr uint64_t tag_hdr(uint64_t hdr) { - return hdr & TAG_MASK; -} - -template -__attribute__((always_inline)) constexpr uint64_t tag(T const *s) { - return tag_hdr(s->h.hdr); -} - -__attribute__((always_inline)) constexpr bool -is_in_young_gen_hdr(uint64_t hdr) { - return !(hdr & NOT_YOUNG_OBJECT_BIT); -} - -__attribute__((always_inline)) constexpr bool is_in_old_gen_hdr(uint64_t hdr) { - return (hdr & NOT_YOUNG_OBJECT_BIT) && (hdr & AGE_MASK); -} - -template -__attribute__((always_inline)) constexpr void reset_gc(T *s) { - constexpr auto all_gc_mask = NOT_YOUNG_OBJECT_BIT | AGE_MASK | FWD_PTR_BIT; - s->h.hdr = s->h.hdr & ~all_gc_mask; -} - -__attribute__((always_inline)) inline block *leaf_block(uint64_t tag) { - auto value = uintptr_t{(tag << 32) | 1}; - return reinterpret_cast(value); -} - -__attribute__((always_inline)) inline block *variable_block(uint64_t tag) { - auto value = uintptr_t{(tag << 32) | 3}; - return reinterpret_cast(value); -} - -template -__attribute__((always_inline)) inline bool is_leaf_block(T const *b) { - return reinterpret_cast(b) & 1; -} - -template -__attribute__((always_inline)) inline bool is_variable_block(T const *b) { - return (reinterpret_cast(b) & 3) == 3; -} - -template -__attribute__((always_inline)) constexpr bool is_heap_block(T const *s) { - return is_in_young_gen_hdr(s->h.hdr) || is_in_old_gen_hdr(s->h.hdr); -} - class k_elem { public: k_elem() @@ -274,20 +134,6 @@ using setiter = struct setiter { set *set_item{}; }; -using SortFloat = floating *; -using SortInt = mpz_ptr; -using SortString = string *; -using SortBytes = string *; -using SortStringBuffer = stringbuffer *; -using SortK = block *; -using SortKItem = block *; -using SortIOInt = block *; -using SortIOFile = block *; -using SortIOString = block *; -using SortJSON = block *; -using SortEndianness = block *; -using SortSignedness = block *; -using SortFFIType = block *; using SortList = list *; using SortMap = map *; using SortSet = set *; @@ -347,6 +193,8 @@ void serialize_configuration_to_proof_trace( FILE *file, block *subject, uint32_t sort); void serialize_term_to_proof_trace( FILE *file, void *subject, uint64_t block_header, uint64_t bits); +string *serialize_term_to_string_v2(block *subject, uint32_t sort); +block *deserialize_term_v2(char *, size_t); // The following functions are called by the generated code and runtime code to // ouput the proof trace data. @@ -421,16 +269,16 @@ using visitor = struct { }; using serialize_to_proof_trace_visitor = struct { - void (*visit_config)(FILE *, block *, uint32_t, bool); - void (*visit_map)(FILE *, map *, uint32_t, uint32_t, uint32_t); - void (*visit_list)(FILE *, list *, uint32_t, uint32_t, uint32_t); - void (*visit_set)(FILE *, set *, uint32_t, uint32_t, uint32_t); - void (*visit_int)(FILE *, mpz_t, uint32_t); - void (*visit_float)(FILE *, floating *, uint32_t); - void (*visit_bool)(FILE *, bool, uint32_t); - void (*visit_string_buffer)(FILE *, stringbuffer *, uint32_t); - void (*visit_m_int)(FILE *, size_t *, size_t, uint32_t); - void (*visit_range_map)(FILE *, rangemap *, uint32_t, uint32_t, uint32_t); + void (*visit_config)(writer *, block *, uint32_t, bool); + void (*visit_map)(writer *, map *, uint32_t, uint32_t, uint32_t); + void (*visit_list)(writer *, list *, uint32_t, uint32_t, uint32_t); + void (*visit_set)(writer *, set *, uint32_t, uint32_t, uint32_t); + void (*visit_int)(writer *, mpz_t, uint32_t); + void (*visit_float)(writer *, floating *, uint32_t); + void (*visit_bool)(writer *, bool, uint32_t); + void (*visit_string_buffer)(writer *, stringbuffer *, uint32_t); + void (*visit_m_int)(writer *, size_t *, size_t, uint32_t); + void (*visit_range_map)(writer *, rangemap *, uint32_t, uint32_t, uint32_t); }; void print_map( @@ -444,7 +292,7 @@ void print_list( void visit_children( block *subject, writer *file, visitor *printer, void *state); void visit_children_for_serialize_to_proof_trace( - block *subject, FILE *file, serialize_to_proof_trace_visitor *printer); + block *subject, writer *file, serialize_to_proof_trace_visitor *printer); stringbuffer *hook_BUFFER_empty(void); stringbuffer *hook_BUFFER_concat(stringbuffer *buf, string *s); diff --git a/include/runtime/types.h b/include/runtime/types.h new file mode 100644 index 000000000..fe230c6b2 --- /dev/null +++ b/include/runtime/types.h @@ -0,0 +1,163 @@ +#ifndef RUNTIME_TYPES_H +#define RUNTIME_TYPES_H + +#include +#include + +#include "config/macros.h" +#include "runtime/alloc.h" + +extern "C" { +// llvm: blockheader = type { i64 } +using blockheader = struct blockheader { + uint64_t hdr; +}; + +// A value b of type block* is either a constant or a block. +// if (((uintptr_t)b) & 3) == 3, then it is a bound variable and +// ((uintptr_t)b) >> 32 is the debruijn index. If ((uintptr_t)b) & 3 == 1) +// then it is a symbol with 0 arguments and ((uintptr_t)b) >> 32 is the tag +// of the symbol. Otherwise, if ((uintptr_t)b) & 1 == 0 then it is a pointer to +// a block. +// llvm: block = type { %blockheader, [0 x i64 *] } +using block = struct block { + blockheader h; + uint64_t *children[]; +}; + +// llvm: string = type { %blockheader, [0 x i8] } +using string = struct string { + blockheader h; + char data[]; +}; + +// llvm: stringbuffer = type { i64, i64, %string* } +using stringbuffer = struct stringbuffer { + blockheader h; + uint64_t strlen; + string *contents; +}; + +using mpz_hdr = struct mpz_hdr { + blockheader h; + mpz_t i; +}; + +using floating = struct floating { + uint64_t exp; // number of bits in exponent range + mpfr_t f; +}; + +using floating_hdr = struct floating_hdr { + blockheader h; + floating f; +}; + +using layoutitem = struct layoutitem { + uint64_t offset; + uint16_t cat; +}; + +using layout = struct layout { + uint8_t nargs; + layoutitem *args; +}; + +using writer = struct { + FILE *file; + stringbuffer *buffer; +}; + +using SortFloat = floating *; +using SortInt = mpz_ptr; +using SortString = string *; +using SortBytes = string *; +using SortStringBuffer = stringbuffer *; +using SortK = block *; +using SortKItem = block *; +using SortIOInt = block *; +using SortIOFile = block *; +using SortIOString = block *; +using SortJSON = block *; +using SortEndianness = block *; +using SortSignedness = block *; +using SortFFIType = block *; +} + +__attribute__((always_inline)) constexpr uint64_t len_hdr(uint64_t hdr) { + return hdr & LENGTH_MASK; +} + +template +__attribute__((always_inline)) constexpr uint64_t len(T const *s) { + return len_hdr(s->h.hdr); +} + +template +__attribute__((always_inline)) constexpr void init_with_len(T *s, uint64_t l) { + s->h.hdr = l | (l > BLOCK_SIZE - sizeof(char *) ? NOT_YOUNG_OBJECT_BIT : 0); +} + +__attribute__((always_inline)) constexpr uint64_t size_hdr(uint64_t hdr) { + return ((hdr >> 32) & 0xff) * 8; +} + +__attribute__((always_inline)) constexpr uint64_t layout_hdr(uint64_t hdr) { + return hdr >> LAYOUT_OFFSET; +} + +template +__attribute__((always_inline)) constexpr uint64_t get_layout(T const *s) { + return layout_hdr((s)->h.hdr); +} + +__attribute__((always_inline)) constexpr uint64_t tag_hdr(uint64_t hdr) { + return hdr & TAG_MASK; +} + +template +__attribute__((always_inline)) constexpr uint64_t tag(T const *s) { + return tag_hdr(s->h.hdr); +} + +__attribute__((always_inline)) constexpr bool +is_in_young_gen_hdr(uint64_t hdr) { + return !(hdr & NOT_YOUNG_OBJECT_BIT); +} + +__attribute__((always_inline)) constexpr bool is_in_old_gen_hdr(uint64_t hdr) { + return (hdr & NOT_YOUNG_OBJECT_BIT) && (hdr & AGE_MASK); +} + +template +__attribute__((always_inline)) constexpr void reset_gc(T *s) { + constexpr auto all_gc_mask = NOT_YOUNG_OBJECT_BIT | AGE_MASK | FWD_PTR_BIT; + s->h.hdr = s->h.hdr & ~all_gc_mask; +} + +__attribute__((always_inline)) inline block *leaf_block(uint64_t tag) { + auto value = uintptr_t{(tag << 32) | 1}; + return reinterpret_cast(value); +} + +__attribute__((always_inline)) inline block *variable_block(uint64_t tag) { + auto value = uintptr_t{(tag << 32) | 3}; + return reinterpret_cast(value); +} + +template +__attribute__((always_inline)) inline bool is_leaf_block(T const *b) { + return reinterpret_cast(b) & 1; +} + +template +__attribute__((always_inline)) inline bool is_variable_block(T const *b) { + return (reinterpret_cast(b) & 3) == 3; +} + +template +__attribute__((always_inline)) constexpr bool is_heap_block(T const *s) { + return is_in_young_gen_hdr(s->h.hdr) || is_in_old_gen_hdr(s->h.hdr); +} + +#endif diff --git a/lib/codegen/EmitConfigParser.cpp b/lib/codegen/EmitConfigParser.cpp index 5e682f16c..da11ac234 100644 --- a/lib/codegen/EmitConfigParser.cpp +++ b/lib/codegen/EmitConfigParser.cpp @@ -635,8 +635,8 @@ static void emit_get_token(kore_definition *definition, llvm::Module *module) { = allocate_term(string_type, len, current_block, "kore_alloc_token"); auto *hdr_ptr = llvm::GetElementPtrInst::CreateInBounds( string_type, block, {zero, zero32, zero32}, "", current_block); - auto *block_size - = module->getOrInsertGlobal("BLOCK_SIZE", llvm::Type::getInt64Ty(ctx)); + auto *block_size = module->getOrInsertGlobal( + "VAR_BLOCK_SIZE", llvm::Type::getInt64Ty(ctx)); auto *block_size_val = new llvm::LoadInst( llvm::Type::getInt64Ty(ctx), block_size, "", current_block); auto *block_alloc_size = llvm::BinaryOperator::Create( diff --git a/runtime/alloc/arena.cpp b/runtime/alloc/arena.cpp index 2041a4247..dd0f6b2e6 100644 --- a/runtime/alloc/arena.cpp +++ b/runtime/alloc/arena.cpp @@ -8,7 +8,7 @@ #include "runtime/arena.h" #include "runtime/header.h" -size_t const BLOCK_SIZE = 1024 * 1024; +extern size_t const VAR_BLOCK_SIZE = BLOCK_SIZE; __attribute__((always_inline)) memory_block_header * mem_block_header(void *ptr) { diff --git a/runtime/util/ConfigurationParser.cpp b/runtime/util/ConfigurationParser.cpp index 3dc431f70..8bb34f5a9 100644 --- a/runtime/util/ConfigurationParser.cpp +++ b/runtime/util/ConfigurationParser.cpp @@ -297,3 +297,16 @@ block *deserialize_configuration(char *data, size_t size) { return static_cast( deserialize_initial_configuration(ptr, end, version)); } + +extern char kompiled_directory; + +block *deserialize_term_v2(char *data, size_t size) { + auto header = kllvm::kore_header::create( + &kompiled_directory + std::string("/header.bin")); + auto buffer = kllvm::proof_trace_memory_buffer(data, data + size); + uint64_t len{}; + auto pat = kllvm::detail::read_v2(buffer, *header, len); + auto *b = (block *)construct_initial_configuration(pat.get()); + deallocate_s_ptr_kore_pattern(std::move(pat)); + return b; +} diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 105db50a3..ac5af3e23 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -58,7 +58,7 @@ static std::string drop_back(std::string const &s, int n) { void serialize_configuration_internal( writer *file, block *subject, char const *sort, bool is_var, void *state); void serialize_configuration_to_proof_trace_internal( - FILE *file, block *subject, uint32_t sort, bool is_var); + writer *file, block *subject, uint32_t sort, bool is_var); /** * Emit a symbol of the form ctor{...}(...); this should be preceded by the @@ -79,9 +79,9 @@ const uint8_t COMPOSITE = 0x01; const uint8_t STRING = 0x00; const uint8_t NULL_BYTE = 0x00; -static void emit_symbol_to_proof_trace(FILE *file, int32_t tag) { - fwrite(&COMPOSITE, sizeof(COMPOSITE), 1, file); - fwrite(&tag, sizeof(tag), 1, file); +static void emit_symbol_to_proof_trace(writer *file, int32_t tag) { + sfwrite(&COMPOSITE, sizeof(COMPOSITE), 1, file); + sfwrite(&tag, sizeof(tag), 1, file); } /** @@ -121,13 +121,13 @@ static void emit_token( } static void emit_token_to_proof_trace( - FILE *file, uint32_t sort, char const *str, size_t len) { + writer *file, uint32_t sort, char const *str, size_t len) { emit_symbol_to_proof_trace(file, sort); - fwrite(&STRING, sizeof(STRING), 1, file); - fwrite(&len, sizeof(len), 1, file); - fwrite(str, 1, len, file); - fwrite(&NULL_BYTE, sizeof(NULL_BYTE), 1, file); + sfwrite(&STRING, sizeof(STRING), 1, file); + sfwrite(&len, sizeof(len), 1, file); + sfwrite(str, 1, len, file); + sfwrite(&NULL_BYTE, sizeof(NULL_BYTE), 1, file); } void serialize_map( @@ -158,7 +158,7 @@ void serialize_map( } void serialize_map_to_proof_trace( - FILE *file, map *map, uint32_t unit, uint32_t element, uint32_t concat) { + writer *file, map *map, uint32_t unit, uint32_t element, uint32_t concat) { size_t size = map->size(); if (size == 0) { emit_symbol_to_proof_trace(file, unit); @@ -216,7 +216,7 @@ void serialize_range_map( } void serialize_range_map_to_proof_trace( - FILE *file, rangemap *map, uint32_t unit, uint32_t element, + writer *file, rangemap *map, uint32_t unit, uint32_t element, uint32_t concat) { size_t size = map->size(); if (size == 0) { @@ -273,7 +273,8 @@ void serialize_list( } void serialize_list_to_proof_trace( - FILE *file, list *list, uint32_t unit, uint32_t element, uint32_t concat) { + writer *file, list *list, uint32_t unit, uint32_t element, + uint32_t concat) { size_t size = list->size(); if (size == 0) { emit_symbol_to_proof_trace(file, unit); @@ -319,7 +320,7 @@ void serialize_set( } void serialize_set_to_proof_trace( - FILE *file, set *set, uint32_t unit, uint32_t element, uint32_t concat) { + writer *file, set *set, uint32_t unit, uint32_t element, uint32_t concat) { size_t size = set->size(); if (size == 0) { emit_symbol_to_proof_trace(file, unit); @@ -347,7 +348,7 @@ void serialize_int(writer *file, mpz_t i, char const *sort, void *state) { emit_token(instance, sort, str.c_str()); } -void serialize_int_to_proof_trace(FILE *file, mpz_t i, uint32_t sort) { +void serialize_int_to_proof_trace(writer *file, mpz_t i, uint32_t sort) { auto str = int_to_string(i); emit_token_to_proof_trace(file, sort, str.data(), str.length()); } @@ -359,7 +360,7 @@ void serialize_float(writer *file, floating *f, char const *sort, void *state) { emit_token(instance, sort, str.c_str()); } -void serialize_float_to_proof_trace(FILE *file, floating *f, uint32_t sort) { +void serialize_float_to_proof_trace(writer *file, floating *f, uint32_t sort) { auto str = float_to_string(f); emit_token_to_proof_trace(file, sort, str.data(), str.length()); } @@ -371,7 +372,7 @@ void serialize_bool(writer *file, bool b, char const *sort, void *state) { emit_token(instance, sort, str); } -void serialize_bool_to_proof_trace(FILE *file, bool b, uint32_t sort) { +void serialize_bool_to_proof_trace(writer *file, bool b, uint32_t sort) { std::string str = b ? "true" : "false"; emit_token_to_proof_trace(file, sort, str.data(), str.length()); } @@ -384,7 +385,7 @@ void serialize_string_buffer( } void serialize_string_buffer_to_proof_trace( - FILE *file, stringbuffer *b, uint32_t sort) { + writer *file, stringbuffer *b, uint32_t sort) { emit_token_to_proof_trace(file, sort, b->contents->data, b->strlen); } @@ -400,7 +401,7 @@ void serialize_m_int( } void serialize_m_int_to_proof_trace( - FILE *file, size_t *i, size_t bits, uint32_t sort) { + writer *file, size_t *i, size_t bits, uint32_t sort) { auto str = (i == nullptr) ? std::string("0") : int_to_string(hook_MINT_import(i, bits, false)); @@ -531,7 +532,7 @@ void serialize_configuration_internal( } void serialize_configuration_to_proof_trace_internal( - FILE *file, block *subject, uint32_t sort, bool is_var) { + writer *file, block *subject, uint32_t sort, bool is_var) { if (is_var) { throw std::invalid_argument("does not support bound variables yet"); } @@ -637,7 +638,16 @@ void serialize_configuration( void serialize_configuration_to_proof_trace( FILE *file, block *subject, uint32_t sort) { fputs("\x7FKR2", file); - serialize_configuration_to_proof_trace_internal(file, subject, sort, false); + writer w{}; + w.file = file; + serialize_configuration_to_proof_trace_internal(&w, subject, sort, false); +} + +string *serialize_term_to_string_v2(block *subject, uint32_t sort) { + writer w{}; + w.buffer = hook_BUFFER_empty(); + serialize_configuration_to_proof_trace_internal(&w, subject, sort, false); + return hook_BUFFER_toString(w.buffer); } void write_hook_event_pre_to_proof_trace( @@ -748,6 +758,8 @@ void serialize_term_to_proof_trace( term->h = header_val; store_symbol_children(term, &arg); fputs("\x7FKR2", file); + writer w{}; + w.file = file; serialize_to_proof_trace_visitor callbacks = {serialize_configuration_to_proof_trace_internal, @@ -761,7 +773,7 @@ void serialize_term_to_proof_trace( serialize_m_int_to_proof_trace, serialize_range_map_to_proof_trace}; - visit_children_for_serialize_to_proof_trace(term, file, &callbacks); + visit_children_for_serialize_to_proof_trace(term, &w, &callbacks); } void serialize_raw_term_to_file( diff --git a/unittests/runtime-arithmetic/inttest.cpp b/unittests/runtime-arithmetic/inttest.cpp index fc9022fa3..209ce9c39 100644 --- a/unittests/runtime-arithmetic/inttest.cpp +++ b/unittests/runtime-arithmetic/inttest.cpp @@ -8,7 +8,6 @@ extern "C" { void *kore_alloc_token(size_t requested) { return malloc(requested); } -size_t const BLOCK_SIZE = -1; mpz_ptr hook_INT_tmod(mpz_t, mpz_t); mpz_ptr hook_INT_emod(mpz_t, mpz_t); diff --git a/unittests/runtime-collections/lists.cpp b/unittests/runtime-collections/lists.cpp index 381b7d90e..d4d2a20d9 100644 --- a/unittests/runtime-collections/lists.cpp +++ b/unittests/runtime-collections/lists.cpp @@ -31,7 +31,6 @@ bool during_gc() { void *kore_alloc_token(size_t requested) { return malloc(requested); } -size_t const BLOCK_SIZE = -1; char const **get_argument_sorts_for_tag(uint32_t tag) { return nullptr; diff --git a/unittests/runtime-strings/CMakeLists.txt b/unittests/runtime-strings/CMakeLists.txt index a7b99cbca..53ee2975b 100644 --- a/unittests/runtime-strings/CMakeLists.txt +++ b/unittests/runtime-strings/CMakeLists.txt @@ -8,8 +8,8 @@ target_link_libraries(runtime-strings-tests PUBLIC strings arithmetic - alloc lto-static + alloc gmp mpfr ${Boost_UNIT_TEST_FRAMEWORK_LIBRARIES}