Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
excluding side condition functions and replacing function names with …
Browse files Browse the repository at this point in the history
…rule ordinals in function exit events
theo25 committed Dec 11, 2024
1 parent bdfceba commit 6198a23
Showing 10 changed files with 64 additions and 36 deletions.
2 changes: 1 addition & 1 deletion bindings/python/ast.cpp
Original file line number Diff line number Diff line change
@@ -430,7 +430,7 @@ void bind_proof_trace(py::module_ &m) {
llvm_tail_call_info_event, std::shared_ptr<llvm_tail_call_info_event>>(
proof_trace, "llvm_tail_call_info_event", step_event)
.def_property_readonly(
"callern_name", &llvm_tail_call_info_event::get_caller_name)
"rule_ordinal", &llvm_tail_call_info_event::get_rule_ordinal)
.def_property_readonly("is_tail", &llvm_tail_call_info_event::is_tail);

py::class_<llvm_function_event, std::shared_ptr<llvm_function_event>>(
2 changes: 1 addition & 1 deletion docs/proof-trace.md
Original file line number Diff line number Diff line change
@@ -61,7 +61,7 @@ rule ::= WORD(0x22) ordinal arity variable*
side_cond_entry ::= WORD(0xEE) ordinal arity variable*
side_cond_exit ::= WORD(0x33) ordinal boolean_result
tail_call_info ::= WORD(0x55) function_name boolean_result
tail_call_info ::= WORD(0x55) ordinal boolean_result
config ::= WORD(0xFF) kore_term
20 changes: 9 additions & 11 deletions include/kllvm/binary/ProofTraceParser.h
Original file line number Diff line number Diff line change
@@ -175,23 +175,21 @@ class llvm_pattern_matching_failure_event : public llvm_step_event {

class llvm_tail_call_info_event : public llvm_step_event {
private:
std::string caller_name_;
uint64_t rule_ordinal_;
bool is_tail_;

llvm_tail_call_info_event(std::string caller_name, bool is_tail)
: caller_name_(std::move(caller_name))
llvm_tail_call_info_event(uint64_t rule_ordinal, bool is_tail)
: rule_ordinal_(rule_ordinal)
, is_tail_(is_tail) { }

public:
static sptr<llvm_tail_call_info_event>
create(std::string caller_name, bool is_tail) {
create(uint64_t rule_ordinal, bool is_tail) {
return sptr<llvm_tail_call_info_event>(
new llvm_tail_call_info_event(std::move(caller_name), is_tail));
new llvm_tail_call_info_event(rule_ordinal, is_tail));
}

[[nodiscard]] std::string const &get_caller_name() const {
return caller_name_;
}
[[nodiscard]] uint64_t get_rule_ordinal() const { return rule_ordinal_; }
[[nodiscard]] bool is_tail() const { return is_tail_; }

void print(std::ostream &out, bool expand_terms, unsigned indent = 0U)
@@ -631,8 +629,8 @@ class proof_trace_parser {
return nullptr;
}

std::string caller_name;
if (!buffer.read_string(caller_name)) {
uint64_t ordinal = 0;
if (!buffer.read_uint64(ordinal)) {
return nullptr;
}

@@ -641,7 +639,7 @@ class proof_trace_parser {
return nullptr;
}

auto event = llvm_tail_call_info_event::create(caller_name, is_tail);
auto event = llvm_tail_call_info_event::create(ordinal, is_tail);

return event;
}
6 changes: 3 additions & 3 deletions include/kllvm/codegen/ProofEvent.h
Original file line number Diff line number Diff line change
@@ -180,7 +180,7 @@ class proof_event {
* Emit a call to the `tail_call_info` API of the specified `proof_writer`.
*/
llvm::CallInst *emit_write_tail_call_info(
llvm::Value *proof_writer, std::string const &caller_name, bool is_tail,
llvm::Value *proof_writer, uint64_t ordinal, bool is_tail,
llvm::BasicBlock *insert_at_end);

/*
@@ -240,8 +240,8 @@ class proof_event {
kore_composite_pattern const &pattern, llvm::BasicBlock *current_block);

[[nodiscard]] llvm::BasicBlock *tail_call_info(
std::string const &caller_name, bool is_tail,
llvm::Instruction *insert_before, llvm::BasicBlock *current_block);
uint64_t ordinal, bool is_tail, llvm::Instruction *insert_before,
llvm::BasicBlock *current_block);

proof_event(kore_definition *definition, llvm::Module *module)
: definition_(definition)
2 changes: 1 addition & 1 deletion include/runtime/header.h
Original file line number Diff line number Diff line change
@@ -232,7 +232,7 @@ void write_side_condition_event_post_to_proof_trace(
void write_pattern_matching_failure_to_proof_trace(
void *proof_writer, char const *function_name);
void write_tail_call_info_to_proof_trace(
void *proof_writer, char const *caller_name, bool is_tail);
void *proof_writer, uint64_t ordinal, bool is_tail);
void write_configuration_to_proof_trace(
void *proof_writer, block *config, bool is_initial);
void start_new_chunk_in_proof_trace(void *proof_writer);
22 changes: 19 additions & 3 deletions include/runtime/proof_trace_writer.h
Original file line number Diff line number Diff line change
@@ -33,7 +33,7 @@ class proof_trace_writer {
side_condition_event_post(uint64_t ordinal, bool side_cond_result)
= 0;
virtual void pattern_matching_failure(char const *function_name) = 0;
virtual void tail_call_info(char const *caller_name, bool is_tail) = 0;
virtual void tail_call_info(uint64_t ordinal, bool is_tail) = 0;
virtual void configuration(block *config, bool is_initial) = 0;
virtual void start_new_chunk() = 0;
virtual void end_of_trace() = 0;
@@ -164,9 +164,9 @@ class proof_trace_file_writer : public proof_trace_writer {
write_null_terminated_string(function_name);
}

void tail_call_info(char const *caller_name, bool is_tail) override {
void tail_call_info(uint64_t ordinal, bool is_tail) override {
write_uint64(kllvm::tail_call_info_sentinel);
write_null_terminated_string(caller_name);
write_uint64(ordinal);
write_bool(is_tail);
}

@@ -234,6 +234,15 @@ class proof_trace_callback_writer : public proof_trace_writer {
, result(result) { }
};

struct tail_call_info_construction {
uint64_t ordinal;
bool is_tail;

tail_call_info_construction(uint64_t ordinal, bool is_tail)
: ordinal(ordinal)
, is_tail(is_tail) { }
};

struct call_event_construction {
char const *hook_name;
char const *symbol_name;
@@ -290,6 +299,8 @@ class proof_trace_callback_writer : public proof_trace_writer {
side_condition_result_construction const &event) { }
[[clang::optnone]] void pattern_matching_failure_callback(
pattern_matching_failure_construction const &event) { }
[[clang::optnone]] void
tail_call_info_callback(tail_call_info_construction const &event) { }
[[clang::optnone]] void configuration_event_callback(
kore_configuration_construction const &config, bool is_initial) { }

@@ -375,6 +386,11 @@ class proof_trace_callback_writer : public proof_trace_writer {
pattern_matching_failure_callback(pm_failure);
}

void tail_call_info(uint64_t ordinal, bool is_tail) override {
tail_call_info_construction tail_call_info(ordinal, is_tail);
tail_call_info_callback(tail_call_info);
}

void configuration(block *config, bool is_initial) override {
kore_configuration_construction configuration(config);
configuration_event_callback(configuration, is_initial);
2 changes: 1 addition & 1 deletion lib/binary/ProofTraceParser.cpp
Original file line number Diff line number Diff line change
@@ -88,7 +88,7 @@ void llvm_tail_call_info_event::print(
std::ostream &out, bool expand_terms, unsigned ind) const {
std::string indent(ind * indent_size, ' ');
out << fmt::format(
"{}tail_call_info: {} {}\n", indent, caller_name_,
"{}tail_call_info: {} {}\n", indent, rule_ordinal_,
(is_tail_ ? "tail" : "notail"));
}

25 changes: 19 additions & 6 deletions lib/codegen/CreateTerm.cpp
Original file line number Diff line number Diff line change
@@ -1277,6 +1277,11 @@ bool make_function(
call->setTailCallKind(llvm::CallInst::TCK_MustTail);
retval = call;
} else {
bool is_apply_rule = name.substr(0, 11) == "apply_rule_";
size_t ordinal = 0;
if (is_apply_rule) {
ordinal = std::stoll(name.substr(11));
}
if (auto *call = llvm::dyn_cast<llvm::CallInst>(retval)) {
// check that musttail requirements are met:
// 1. Call is in tail position (guaranteed)
@@ -1287,16 +1292,24 @@ bool make_function(
if (call->getCallingConv() == llvm::CallingConv::Tail
&& can_tail_call(call->getType())) {
call->setTailCallKind(llvm::CallInst::TCK_MustTail);
current_block = proof_event(definition, module)
.tail_call_info(name, true, call, current_block);
if (is_apply_rule) {
current_block
= proof_event(definition, module)
.tail_call_info(ordinal, true, call, current_block);
}
} else {
if (is_apply_rule) {
current_block
= proof_event(definition, module)
.tail_call_info(ordinal, false, nullptr, current_block);
}
}
} else {
if (is_apply_rule) {
current_block
= proof_event(definition, module)
.tail_call_info(name, false, nullptr, current_block);
.tail_call_info(ordinal, false, nullptr, current_block);
}
} else {
current_block = proof_event(definition, module)
.tail_call_info(name, false, nullptr, current_block);
}
}
auto *ret
15 changes: 8 additions & 7 deletions lib/codegen/ProofEvent.cpp
Original file line number Diff line number Diff line change
@@ -305,23 +305,24 @@ llvm::CallInst *proof_event::emit_write_pattern_matching_failure(
}

llvm::CallInst *proof_event::emit_write_tail_call_info(
llvm::Value *proof_writer, std::string const &caller_name, bool is_tail,
llvm::Value *proof_writer, uint64_t ordinal, bool is_tail,
llvm::BasicBlock *insert_at_end) {
auto b = llvm::IRBuilder(insert_at_end);

auto *void_ty = llvm::Type::getVoidTy(ctx_);
auto *i8_ptr_ty = llvm::PointerType::getUnqual(ctx_);
auto *i64_ty = llvm::Type::getInt64Ty(ctx_);
auto *i8_ty = llvm::Type::getInt64Ty(ctx_);

auto *func_ty
= llvm::FunctionType::get(void_ty, {i8_ptr_ty, i8_ptr_ty, i8_ty}, false);
= llvm::FunctionType::get(void_ty, {i8_ptr_ty, i64_ty, i8_ty}, false);

auto *func = get_or_insert_function(
module_, "write_tail_call_info_to_proof_trace", func_ty);

auto *var_caller_name = b.CreateGlobalStringPtr(caller_name, "", 0, module_);
auto *var_ordinal = llvm::ConstantInt::get(i64_ty, ordinal);
auto *var_is_tail = llvm::ConstantInt::get(i8_ty, is_tail);
return b.CreateCall(func, {proof_writer, var_caller_name, var_is_tail});
return b.CreateCall(func, {proof_writer, var_ordinal, var_is_tail});
}

llvm::CallInst *proof_event::emit_start_new_chunk(
@@ -745,8 +746,8 @@ llvm::BasicBlock *proof_event::pattern_matching_failure(
}

llvm::BasicBlock *proof_event::tail_call_info(
std::string const &caller_name, bool is_tail,
llvm::Instruction *insert_before, llvm::BasicBlock *current_block) {
uint64_t ordinal, bool is_tail, llvm::Instruction *insert_before,
llvm::BasicBlock *current_block) {

if (!proof_hint_instrumentation) {
return current_block;
@@ -762,7 +763,7 @@ llvm::BasicBlock *proof_event::tail_call_info(

auto [true_block, merge_block, proof_writer] = prelude;

emit_write_tail_call_info(proof_writer, caller_name, is_tail, true_block);
emit_write_tail_call_info(proof_writer, ordinal, is_tail, true_block);

llvm::BranchInst::Create(merge_block, true_block);

4 changes: 2 additions & 2 deletions runtime/util/ConfigurationSerializer.cpp
Original file line number Diff line number Diff line change
@@ -718,9 +718,9 @@ void write_pattern_matching_failure_to_proof_trace(
}

void write_tail_call_info_to_proof_trace(
void *proof_writer, char const *caller_name, bool is_tail) {
void *proof_writer, uint64_t ordinal, bool is_tail) {
static_cast<proof_trace_writer *>(proof_writer)
->tail_call_info(caller_name, is_tail);
->tail_call_info(ordinal, is_tail);
}

void write_configuration_to_proof_trace(

0 comments on commit 6198a23

Please sign in to comment.