Merge branch 'develop' into fix-side-condition-bug

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 *);

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();
 }

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

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

include/runtime/header.h

@@ -6,14 +6,11 @@
 #include <limits>
 #include <vector>
 
-#include <gmp.h>
-#include <mpfr.h>
-
 #include <fmt/printf.h>
 
 #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 <typename T>
-__attribute__((always_inline)) constexpr uint64_t len(T const *s) {
-  return len_hdr(s->h.hdr);
-}
-
-template <typename T>
-__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 <typename T>
-__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 <typename T>
-__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 <typename T>
-__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<block *>(value);
-}
-
-__attribute__((always_inline)) inline block *variable_block(uint64_t tag) {
-  auto value = uintptr_t{(tag << 32) | 3};
-  return reinterpret_cast<block *>(value);
-}
-
-template <typename T>
-__attribute__((always_inline)) inline bool is_leaf_block(T const *b) {
-  return reinterpret_cast<uintptr_t>(b) & 1;
-}
-
-template <typename T>
-__attribute__((always_inline)) inline bool is_variable_block(T const *b) {
-  return (reinterpret_cast<uintptr_t>(b) & 3) == 3;
-}
-
-template <typename T>
-__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);