Skip to content

Commit

Permalink
Merge branch 'develop' into fix-side-condition-bug
Browse files Browse the repository at this point in the history
  • Loading branch information
Robertorosmaninho authored Oct 17, 2024
2 parents 6c27043 + fc9602c commit 832635b
Show file tree
Hide file tree
Showing 13 changed files with 231 additions and 195 deletions.
2 changes: 2 additions & 0 deletions bindings/c/include/kllvm-c/kllvm-c.h
Original file line number Diff line number Diff line change
Expand Up @@ -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 *);
Expand Down
1 change: 0 additions & 1 deletion bindings/c/lib.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,6 @@ auto managed(kore_symbol *ptr) {
*/

extern "C" {
void init_static_objects();
void free_all_kore_mem();
bool hook_BYTES_mutableBytesEnabled();
}
Expand Down
2 changes: 1 addition & 1 deletion include/runtime/alloc.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions include/runtime/collect.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
180 changes: 14 additions & 166 deletions include/runtime/header.h
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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);
Expand All @@ -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()
Expand Down Expand Up @@ -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 *;
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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(
Expand All @@ -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);
Expand Down
Loading

0 comments on commit 832635b

Please sign in to comment.