diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp index 8f23fda70..5129aa10d 100644 --- a/bindings/python/ast.cpp +++ b/bindings/python/ast.cpp @@ -427,11 +427,11 @@ void bind_proof_trace(py::module_ &m) { &llvm_pattern_matching_failure_event::get_function_name); py::class_< - llvm_tail_call_info_event, std::shared_ptr>( - proof_trace, "llvm_tail_call_info_event", step_event) + llvm_function_exit_event, std::shared_ptr>( + proof_trace, "llvm_function_exit_event", step_event) .def_property_readonly( - "rule_ordinal", &llvm_tail_call_info_event::get_rule_ordinal) - .def_property_readonly("is_tail", &llvm_tail_call_info_event::is_tail); + "rule_ordinal", &llvm_function_exit_event::get_rule_ordinal) + .def_property_readonly("is_tail", &llvm_function_exit_event::is_tail); py::class_>( proof_trace, "llvm_function_event", step_event) diff --git a/docs/proof-trace.md b/docs/proof-trace.md index 54282a6a5..4f977a83b 100644 --- a/docs/proof-trace.md +++ b/docs/proof-trace.md @@ -38,7 +38,7 @@ event ::= hook | side_cond_exit | config | pattern_matching_failure - | tail_call_info + | function_exit arg ::= kore_term @@ -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) ordinal boolean_result +function_exit ::= WORD(0x55) ordinal boolean_result config ::= WORD(0xFF) kore_term diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h index c6a08ba6e..0c1b53e31 100644 --- a/include/kllvm/binary/ProofTraceParser.h +++ b/include/kllvm/binary/ProofTraceParser.h @@ -35,7 +35,7 @@ constexpr uint64_t rule_event_sentinel = detail::word(0x22); constexpr uint64_t side_condition_event_sentinel = detail::word(0xEE); constexpr uint64_t side_condition_end_sentinel = detail::word(0x33); constexpr uint64_t pattern_matching_failure_sentinel = detail::word(0x44); -constexpr uint64_t tail_call_info_sentinel = detail::word(0x55); +constexpr uint64_t function_exit_sentinel = detail::word(0x55); class llvm_step_event : public std::enable_shared_from_this { public: @@ -173,20 +173,20 @@ class llvm_pattern_matching_failure_event : public llvm_step_event { const override; }; -class llvm_tail_call_info_event : public llvm_step_event { +class llvm_function_exit_event : public llvm_step_event { private: uint64_t rule_ordinal_; bool is_tail_; - llvm_tail_call_info_event(uint64_t rule_ordinal, bool is_tail) + llvm_function_exit_event(uint64_t rule_ordinal, bool is_tail) : rule_ordinal_(rule_ordinal) , is_tail_(is_tail) { } public: - static sptr + static sptr create(uint64_t rule_ordinal, bool is_tail) { - return sptr( - new llvm_tail_call_info_event(rule_ordinal, is_tail)); + return sptr( + new llvm_function_exit_event(rule_ordinal, is_tail)); } [[nodiscard]] uint64_t get_rule_ordinal() const { return rule_ordinal_; } @@ -623,9 +623,9 @@ class proof_trace_parser { return event; } - sptr static parse_tail_call_info( + sptr static parse_function_exit( proof_trace_buffer &buffer) { - if (!buffer.check_word(tail_call_info_sentinel)) { + if (!buffer.check_word(function_exit_sentinel)) { return nullptr; } @@ -639,7 +639,7 @@ class proof_trace_parser { return nullptr; } - auto event = llvm_tail_call_info_event::create(ordinal, is_tail); + auto event = llvm_function_exit_event::create(ordinal, is_tail); return event; } @@ -679,7 +679,7 @@ class proof_trace_parser { case pattern_matching_failure_sentinel: return parse_pattern_matching_failure(buffer); - case tail_call_info_sentinel: return parse_tail_call_info(buffer); + case function_exit_sentinel: return parse_function_exit(buffer); default: return nullptr; } diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h index 108ba7a5d..d387b4854 100644 --- a/include/kllvm/codegen/ProofEvent.h +++ b/include/kllvm/codegen/ProofEvent.h @@ -177,9 +177,9 @@ class proof_event { llvm::BasicBlock *insert_at_end); /* - * Emit a call to the `tail_call_info` API of the specified `proof_writer`. + * Emit a call to the `function_exit` API of the specified `proof_writer`. */ - llvm::CallInst *emit_write_tail_call_info( + llvm::CallInst *emit_write_function_exit( llvm::Value *proof_writer, uint64_t ordinal, bool is_tail, llvm::BasicBlock *insert_at_end); @@ -239,7 +239,7 @@ class proof_event { [[nodiscard]] llvm::BasicBlock *pattern_matching_failure( kore_composite_pattern const &pattern, llvm::BasicBlock *current_block); - [[nodiscard]] llvm::BasicBlock *tail_call_info( + [[nodiscard]] llvm::BasicBlock *function_exit( uint64_t ordinal, bool is_tail, llvm::Instruction *insert_before, llvm::BasicBlock *current_block); diff --git a/include/runtime/header.h b/include/runtime/header.h index a5bf32bd6..06cbfb46c 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -231,7 +231,7 @@ void write_side_condition_event_post_to_proof_trace( void *proof_writer, uint64_t ordinal, bool side_cond_result); void write_pattern_matching_failure_to_proof_trace( void *proof_writer, char const *function_name); -void write_tail_call_info_to_proof_trace( +void write_function_exit_to_proof_trace( void *proof_writer, uint64_t ordinal, bool is_tail); void write_configuration_to_proof_trace( void *proof_writer, block *config, bool is_initial); diff --git a/include/runtime/proof_trace_writer.h b/include/runtime/proof_trace_writer.h index 447b07e2e..994253515 100644 --- a/include/runtime/proof_trace_writer.h +++ b/include/runtime/proof_trace_writer.h @@ -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(uint64_t ordinal, bool is_tail) = 0; + virtual void function_exit(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,8 +164,8 @@ class proof_trace_file_writer : public proof_trace_writer { write_null_terminated_string(function_name); } - void tail_call_info(uint64_t ordinal, bool is_tail) override { - write_uint64(kllvm::tail_call_info_sentinel); + void function_exit(uint64_t ordinal, bool is_tail) override { + write_uint64(kllvm::function_exit_sentinel); write_uint64(ordinal); write_bool(is_tail); } @@ -234,11 +234,11 @@ class proof_trace_callback_writer : public proof_trace_writer { , result(result) { } }; - struct tail_call_info_construction { + struct function_exit_construction { uint64_t ordinal; bool is_tail; - tail_call_info_construction(uint64_t ordinal, bool is_tail) + function_exit_construction(uint64_t ordinal, bool is_tail) : ordinal(ordinal) , is_tail(is_tail) { } }; @@ -300,7 +300,7 @@ class proof_trace_callback_writer : public proof_trace_writer { [[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) { } + function_exit_callback(function_exit_construction const &event) { } [[clang::optnone]] void configuration_event_callback( kore_configuration_construction const &config, bool is_initial) { } @@ -386,9 +386,9 @@ 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 function_exit(uint64_t ordinal, bool is_tail) override { + function_exit_construction function_exit(ordinal, is_tail); + function_exit_callback(function_exit); } void configuration(block *config, bool is_initial) override { diff --git a/lib/binary/ProofTraceParser.cpp b/lib/binary/ProofTraceParser.cpp index 9c87225b0..4f7a5004b 100644 --- a/lib/binary/ProofTraceParser.cpp +++ b/lib/binary/ProofTraceParser.cpp @@ -84,11 +84,11 @@ void llvm_pattern_matching_failure_event::print( "{}pattern matching failure: {}\n", indent, function_name_); } -void llvm_tail_call_info_event::print( +void llvm_function_exit_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, rule_ordinal_, + "{}function exit: {} {}\n", indent, rule_ordinal_, (is_tail_ ? "tail" : "notail")); } diff --git a/lib/codegen/CreateTerm.cpp b/lib/codegen/CreateTerm.cpp index bbd907048..c1856b5da 100644 --- a/lib/codegen/CreateTerm.cpp +++ b/lib/codegen/CreateTerm.cpp @@ -1295,20 +1295,20 @@ bool make_function( if (is_apply_rule) { current_block = proof_event(definition, module) - .tail_call_info(ordinal, true, call, current_block); + .function_exit(ordinal, true, call, current_block); } } else { if (is_apply_rule) { current_block = proof_event(definition, module) - .tail_call_info(ordinal, false, nullptr, current_block); + .function_exit(ordinal, false, nullptr, current_block); } } } else { if (is_apply_rule) { current_block = proof_event(definition, module) - .tail_call_info(ordinal, false, nullptr, current_block); + .function_exit(ordinal, false, nullptr, current_block); } } } diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp index 3916664a6..3ed817730 100644 --- a/lib/codegen/ProofEvent.cpp +++ b/lib/codegen/ProofEvent.cpp @@ -304,7 +304,7 @@ llvm::CallInst *proof_event::emit_write_pattern_matching_failure( return b.CreateCall(func, {proof_writer, var_function_name}); } -llvm::CallInst *proof_event::emit_write_tail_call_info( +llvm::CallInst *proof_event::emit_write_function_exit( llvm::Value *proof_writer, uint64_t ordinal, bool is_tail, llvm::BasicBlock *insert_at_end) { auto b = llvm::IRBuilder(insert_at_end); @@ -318,7 +318,7 @@ llvm::CallInst *proof_event::emit_write_tail_call_info( = 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); + module_, "write_function_exit_to_proof_trace", func_ty); auto *var_ordinal = llvm::ConstantInt::get(i64_ty, ordinal); auto *var_is_tail = llvm::ConstantInt::get(i8_ty, is_tail); @@ -745,7 +745,7 @@ llvm::BasicBlock *proof_event::pattern_matching_failure( return merge_block; } -llvm::BasicBlock *proof_event::tail_call_info( +llvm::BasicBlock *proof_event::function_exit( uint64_t ordinal, bool is_tail, llvm::Instruction *insert_before, llvm::BasicBlock *current_block) { @@ -756,14 +756,14 @@ llvm::BasicBlock *proof_event::tail_call_info( std::tuple prelude; if (is_tail) { assert(insert_before); - prelude = event_prelude("tail_call_info", insert_before); + prelude = event_prelude("function_exit", insert_before); } else { - prelude = event_prelude("tail_call_info", current_block); + prelude = event_prelude("function_exit", current_block); } auto [true_block, merge_block, proof_writer] = prelude; - emit_write_tail_call_info(proof_writer, ordinal, is_tail, true_block); + emit_write_function_exit(proof_writer, ordinal, is_tail, true_block); llvm::BranchInst::Create(merge_block, true_block); diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index adb1849b8..15c20d6b0 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -717,10 +717,10 @@ void write_pattern_matching_failure_to_proof_trace( ->pattern_matching_failure(function_name); } -void write_tail_call_info_to_proof_trace( +void write_function_exit_to_proof_trace( void *proof_writer, uint64_t ordinal, bool is_tail) { static_cast(proof_writer) - ->tail_call_info(ordinal, is_tail); + ->function_exit(ordinal, is_tail); } void write_configuration_to_proof_trace(