Skip to content

Commit fc9602c

Browse files
authored
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
1 parent a8704ec commit fc9602c

File tree

13 files changed

+231
-195
lines changed

13 files changed

+231
-195
lines changed

bindings/c/include/kllvm-c/kllvm-c.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -131,6 +131,8 @@ void kore_simplify_binary(
131131

132132
block *take_steps(int64_t depth, block *term);
133133

134+
void init_static_objects(void);
135+
134136
/* kore_sort */
135137

136138
char *kore_sort_dump(kore_sort const *);

bindings/c/lib.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -67,7 +67,6 @@ auto managed(kore_symbol *ptr) {
6767
*/
6868

6969
extern "C" {
70-
void init_static_objects();
7170
void free_all_kore_mem();
7271
bool hook_BYTES_mutableBytesEnabled();
7372
}

include/runtime/alloc.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ extern "C" {
77

88
// The maximum single allocation size in bytes.
99
// A contiguous area larger than that size cannot be allocated in any arena.
10-
extern size_t const BLOCK_SIZE;
10+
#define BLOCK_SIZE (1024 * 1024)
1111

1212
#define YOUNGSPACE_ID 0
1313
#define OLDSPACE_ID 1

include/runtime/collect.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,7 @@ void migrate_set(void *s);
3939
void migrate_collection_node(void **node_ptr);
4040
void set_kore_memory_functions_for_gmp(void);
4141
void kore_collect(void **, uint8_t, layoutitem *, bool force = false);
42+
void free_all_kore_mem();
4243
}
4344

4445
#ifdef GC_DBG

include/runtime/header.h

Lines changed: 14 additions & 166 deletions
Original file line numberDiff line numberDiff line change
@@ -6,14 +6,11 @@
66
#include <limits>
77
#include <vector>
88

9-
#include <gmp.h>
10-
#include <mpfr.h>
11-
129
#include <fmt/printf.h>
1310

1411
#include "config/macros.h"
15-
#include "runtime/alloc.h"
1612
#include "runtime/fmt_error_handling.h"
13+
#include "runtime/types.h"
1714

1815
#ifndef IMMER_TAGGED_NODE
1916
#define IMMER_TAGGED_NODE 0
@@ -42,68 +39,7 @@ struct match_log {
4239

4340
#define STRUCT_BASE(struct_type, member_name, member_addr) \
4441
((struct_type *)((char *)(member_addr)-offsetof(struct_type, member_name)))
45-
4642
extern "C" {
47-
// llvm: blockheader = type { i64 }
48-
using blockheader = struct blockheader {
49-
uint64_t hdr;
50-
};
51-
52-
// A value b of type block* is either a constant or a block.
53-
// if (((uintptr_t)b) & 3) == 3, then it is a bound variable and
54-
// ((uintptr_t)b) >> 32 is the debruijn index. If ((uintptr_t)b) & 3 == 1)
55-
// then it is a symbol with 0 arguments and ((uintptr_t)b) >> 32 is the tag
56-
// of the symbol. Otherwise, if ((uintptr_t)b) & 1 == 0 then it is a pointer to
57-
// a block.
58-
// llvm: block = type { %blockheader, [0 x i64 *] }
59-
using block = struct block {
60-
blockheader h;
61-
uint64_t *children[];
62-
};
63-
64-
// llvm: string = type { %blockheader, [0 x i8] }
65-
using string = struct string {
66-
blockheader h;
67-
char data[];
68-
};
69-
70-
// llvm: stringbuffer = type { i64, i64, %string* }
71-
using stringbuffer = struct stringbuffer {
72-
blockheader h;
73-
uint64_t strlen;
74-
string *contents;
75-
};
76-
77-
using mpz_hdr = struct mpz_hdr {
78-
blockheader h;
79-
mpz_t i;
80-
};
81-
82-
using floating = struct floating {
83-
uint64_t exp; // number of bits in exponent range
84-
mpfr_t f;
85-
};
86-
87-
using floating_hdr = struct floating_hdr {
88-
blockheader h;
89-
floating f;
90-
};
91-
92-
using layoutitem = struct layoutitem {
93-
uint64_t offset;
94-
uint16_t cat;
95-
};
96-
97-
using layout = struct layout {
98-
uint8_t nargs;
99-
layoutitem *args;
100-
};
101-
102-
using writer = struct {
103-
FILE *file;
104-
stringbuffer *buffer;
105-
};
106-
10743
bool hook_KEQUAL_lt(block *, block *);
10844
bool hook_KEQUAL_eq(block *, block *);
10945
bool during_gc(void);
@@ -115,82 +51,6 @@ void hash_exit(void);
11551
extern bool gc_enabled;
11652
}
11753

118-
__attribute__((always_inline)) constexpr uint64_t len_hdr(uint64_t hdr) {
119-
return hdr & LENGTH_MASK;
120-
}
121-
122-
template <typename T>
123-
__attribute__((always_inline)) constexpr uint64_t len(T const *s) {
124-
return len_hdr(s->h.hdr);
125-
}
126-
127-
template <typename T>
128-
__attribute__((always_inline)) constexpr void init_with_len(T *s, uint64_t l) {
129-
s->h.hdr = l | (l > BLOCK_SIZE - sizeof(char *) ? NOT_YOUNG_OBJECT_BIT : 0);
130-
}
131-
132-
__attribute__((always_inline)) constexpr uint64_t size_hdr(uint64_t hdr) {
133-
return ((hdr >> 32) & 0xff) * 8;
134-
}
135-
136-
__attribute__((always_inline)) constexpr uint64_t layout_hdr(uint64_t hdr) {
137-
return hdr >> LAYOUT_OFFSET;
138-
}
139-
140-
template <typename T>
141-
__attribute__((always_inline)) constexpr uint64_t get_layout(T const *s) {
142-
return layout_hdr((s)->h.hdr);
143-
}
144-
145-
__attribute__((always_inline)) constexpr uint64_t tag_hdr(uint64_t hdr) {
146-
return hdr & TAG_MASK;
147-
}
148-
149-
template <typename T>
150-
__attribute__((always_inline)) constexpr uint64_t tag(T const *s) {
151-
return tag_hdr(s->h.hdr);
152-
}
153-
154-
__attribute__((always_inline)) constexpr bool
155-
is_in_young_gen_hdr(uint64_t hdr) {
156-
return !(hdr & NOT_YOUNG_OBJECT_BIT);
157-
}
158-
159-
__attribute__((always_inline)) constexpr bool is_in_old_gen_hdr(uint64_t hdr) {
160-
return (hdr & NOT_YOUNG_OBJECT_BIT) && (hdr & AGE_MASK);
161-
}
162-
163-
template <typename T>
164-
__attribute__((always_inline)) constexpr void reset_gc(T *s) {
165-
constexpr auto all_gc_mask = NOT_YOUNG_OBJECT_BIT | AGE_MASK | FWD_PTR_BIT;
166-
s->h.hdr = s->h.hdr & ~all_gc_mask;
167-
}
168-
169-
__attribute__((always_inline)) inline block *leaf_block(uint64_t tag) {
170-
auto value = uintptr_t{(tag << 32) | 1};
171-
return reinterpret_cast<block *>(value);
172-
}
173-
174-
__attribute__((always_inline)) inline block *variable_block(uint64_t tag) {
175-
auto value = uintptr_t{(tag << 32) | 3};
176-
return reinterpret_cast<block *>(value);
177-
}
178-
179-
template <typename T>
180-
__attribute__((always_inline)) inline bool is_leaf_block(T const *b) {
181-
return reinterpret_cast<uintptr_t>(b) & 1;
182-
}
183-
184-
template <typename T>
185-
__attribute__((always_inline)) inline bool is_variable_block(T const *b) {
186-
return (reinterpret_cast<uintptr_t>(b) & 3) == 3;
187-
}
188-
189-
template <typename T>
190-
__attribute__((always_inline)) constexpr bool is_heap_block(T const *s) {
191-
return is_in_young_gen_hdr(s->h.hdr) || is_in_old_gen_hdr(s->h.hdr);
192-
}
193-
19454
class k_elem {
19555
public:
19656
k_elem()
@@ -274,20 +134,6 @@ using setiter = struct setiter {
274134
set *set_item{};
275135
};
276136

277-
using SortFloat = floating *;
278-
using SortInt = mpz_ptr;
279-
using SortString = string *;
280-
using SortBytes = string *;
281-
using SortStringBuffer = stringbuffer *;
282-
using SortK = block *;
283-
using SortKItem = block *;
284-
using SortIOInt = block *;
285-
using SortIOFile = block *;
286-
using SortIOString = block *;
287-
using SortJSON = block *;
288-
using SortEndianness = block *;
289-
using SortSignedness = block *;
290-
using SortFFIType = block *;
291137
using SortList = list *;
292138
using SortMap = map *;
293139
using SortSet = set *;
@@ -347,6 +193,8 @@ void serialize_configuration_to_proof_trace(
347193
FILE *file, block *subject, uint32_t sort);
348194
void serialize_term_to_proof_trace(
349195
FILE *file, void *subject, uint64_t block_header, uint64_t bits);
196+
string *serialize_term_to_string_v2(block *subject, uint32_t sort);
197+
block *deserialize_term_v2(char *, size_t);
350198

351199
// The following functions are called by the generated code and runtime code to
352200
// ouput the proof trace data.
@@ -421,16 +269,16 @@ using visitor = struct {
421269
};
422270

423271
using serialize_to_proof_trace_visitor = struct {
424-
void (*visit_config)(FILE *, block *, uint32_t, bool);
425-
void (*visit_map)(FILE *, map *, uint32_t, uint32_t, uint32_t);
426-
void (*visit_list)(FILE *, list *, uint32_t, uint32_t, uint32_t);
427-
void (*visit_set)(FILE *, set *, uint32_t, uint32_t, uint32_t);
428-
void (*visit_int)(FILE *, mpz_t, uint32_t);
429-
void (*visit_float)(FILE *, floating *, uint32_t);
430-
void (*visit_bool)(FILE *, bool, uint32_t);
431-
void (*visit_string_buffer)(FILE *, stringbuffer *, uint32_t);
432-
void (*visit_m_int)(FILE *, size_t *, size_t, uint32_t);
433-
void (*visit_range_map)(FILE *, rangemap *, uint32_t, uint32_t, uint32_t);
272+
void (*visit_config)(writer *, block *, uint32_t, bool);
273+
void (*visit_map)(writer *, map *, uint32_t, uint32_t, uint32_t);
274+
void (*visit_list)(writer *, list *, uint32_t, uint32_t, uint32_t);
275+
void (*visit_set)(writer *, set *, uint32_t, uint32_t, uint32_t);
276+
void (*visit_int)(writer *, mpz_t, uint32_t);
277+
void (*visit_float)(writer *, floating *, uint32_t);
278+
void (*visit_bool)(writer *, bool, uint32_t);
279+
void (*visit_string_buffer)(writer *, stringbuffer *, uint32_t);
280+
void (*visit_m_int)(writer *, size_t *, size_t, uint32_t);
281+
void (*visit_range_map)(writer *, rangemap *, uint32_t, uint32_t, uint32_t);
434282
};
435283

436284
void print_map(
@@ -444,7 +292,7 @@ void print_list(
444292
void visit_children(
445293
block *subject, writer *file, visitor *printer, void *state);
446294
void visit_children_for_serialize_to_proof_trace(
447-
block *subject, FILE *file, serialize_to_proof_trace_visitor *printer);
295+
block *subject, writer *file, serialize_to_proof_trace_visitor *printer);
448296

449297
stringbuffer *hook_BUFFER_empty(void);
450298
stringbuffer *hook_BUFFER_concat(stringbuffer *buf, string *s);

0 commit comments

Comments
 (0)