From 037634adf2a44b98026d3339bdbaeac8f8bfdcda Mon Sep 17 00:00:00 2001 From: Theodoros Kasampalis Date: Thu, 15 Aug 2024 16:14:48 -0500 Subject: [PATCH 1/6] removing unused flag --- runtime/main/main.ll | 1 - 1 file changed, 1 deletion(-) diff --git a/runtime/main/main.ll b/runtime/main/main.ll index 43dc6e0bf..c4630c663 100644 --- a/runtime/main/main.ll +++ b/runtime/main/main.ll @@ -19,7 +19,6 @@ declare void @print_proof_hint_header(ptr) @statistics.flag = private constant [13 x i8] c"--statistics\00" @binary_out.flag = private constant [16 x i8] c"--binary-output\00" @proof_out.flag = private constant [15 x i8] c"--proof-output\00" -@use_shm.flag = private constant [20 x i8] c"--use-shared-memory\00" @proof_writer = external global ptr @statistics = external global i1 From 250335af27d2ab8b7933373f686c278155bb2c42 Mon Sep 17 00:00:00 2001 From: Theodoros Kasampalis Date: Wed, 14 Aug 2024 18:25:44 -0500 Subject: [PATCH 2/6] new abstract writer at the event level --- config/llvm_header.inc | 6 +- include/kllvm/codegen/ProofEvent.h | 98 ++++++--- include/runtime/header.h | 31 ++- include/runtime/proof_trace_writer.h | 142 ++++++++++++ lib/codegen/ProofEvent.cpp | 269 +++++++++++++++++------ runtime/util/ConfigurationSerializer.cpp | 79 ++++++- runtime/util/finish_rewriting.cpp | 14 +- runtime/util/util.cpp | 6 +- 8 files changed, 526 insertions(+), 119 deletions(-) create mode 100644 include/runtime/proof_trace_writer.h diff --git a/config/llvm_header.inc b/config/llvm_header.inc index ba3d3d2f4..c8c4c8297 100644 --- a/config/llvm_header.inc +++ b/config/llvm_header.inc @@ -193,8 +193,7 @@ define i1 @string_equal(ptr %str1, ptr %str2, i64 %len1, i64 %len2) { declare tailcc ptr @k_step(ptr) declare tailcc void @step_all(ptr) -declare void @serialize_configuration_to_proof_writer(ptr, ptr) -declare void @write_uint64_to_proof_trace(ptr, i64) +declare void @write_configuration_to_proof_trace(ptr, ptr) @proof_output = external global i1 @proof_writer = external global ptr @@ -237,8 +236,7 @@ define ptr @take_steps(i64 %depth, ptr %subject) { br i1 %proof_output, label %if, label %merge if: %proof_writer = load ptr, ptr @proof_writer - call void @write_uint64_to_proof_trace(ptr %proof_writer, i64 18446744073709551615) - call void @serialize_configuration_to_proof_writer(ptr %proof_writer, ptr %subject) + call void @write_configuration_to_proof_trace(ptr %proof_writer, ptr %subject) br label %merge merge: store i64 %depth, ptr @depth diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h index d4aacc437..80a283b62 100644 --- a/include/kllvm/codegen/ProofEvent.h +++ b/include/kllvm/codegen/ProofEvent.h @@ -44,52 +44,96 @@ class proof_event { event_prelude(std::string const &label, llvm::BasicBlock *insert_at_end); /* - * Emit a call that will serialize `term` to the specified `proof_writer` as - * binary KORE. This function can be called on any term, but the sort of that - * term must be known. + * Emit an instruction that has no effect and will be removed by optimization + * passes. + * + * We need this workaround because some callsites will try to use + * llvm::Instruction::insertAfter on the back of the MergeBlock after a proof + * branch is created. If the MergeBlock has no instructions, this has resulted + * in a segfault when printing the IR. Adding an effective no-op prevents this. + */ + llvm::BinaryOperator *emit_no_op(llvm::BasicBlock *insert_at_end); + + /* + * Emit instructions to get a pointer to the interpreter's proof_trace_writer; + * the data structure that outputs proof trace data. + */ + llvm::LoadInst *emit_get_proof_trace_writer(llvm::BasicBlock *insert_at_end); + + /* + * Get the block header value for the given `sort_name`. + */ + uint64_t get_block_header(std::string const &sort_name); + + /* + * Emit a call to the `hook_event_pre` API of the specified `proof_writer`. */ - llvm::CallInst *emit_serialize_term( - kore_composite_sort &sort, llvm::Value *proof_writer, llvm::Value *term, + llvm::CallInst *emit_write_hook_event_pre( + llvm::Value *proof_writer, std::string const &name, + std::string const &pattern, std::string const &location_stack, llvm::BasicBlock *insert_at_end); /* - * Emit a call that will serialize `value` to the specified `proof_writer`. + * Emit a call to the `hook_event_post` API of the specified `proof_writer`. */ - llvm::CallInst *emit_write_uint64( - llvm::Value *proof_writer, uint64_t value, + llvm::CallInst *emit_write_hook_event_post( + llvm::Value *proof_writer, llvm::Value *val, kore_composite_sort &sort, llvm::BasicBlock *insert_at_end); /* - * Emit a call that will serialize a boolean value to the specified - * `proof_writer`. - */ - llvm::CallInst *emit_write_bool( - llvm::Value *proof_writer, llvm::Value *term, + * Emit a call to the `argument` API of the specified `proof_writer`. + */ + llvm::CallInst *emit_write_argument( + llvm::Value *proof_writer, llvm::Value *val, kore_composite_sort &sort, llvm::BasicBlock *insert_at_end); /* - * Emit a call that will serialize `str` to the specified `proof_writer`. + * Emit a call to the `rewrite_event_pre` API of the specified `proof_writer`. */ - llvm::CallInst *emit_write_string( - llvm::Value *proof_writer, std::string const &str, + llvm::CallInst *emit_write_rewrite_event_pre( + llvm::Value *proof_writer, uint64_t ordinal, uint64_t arity, llvm::BasicBlock *insert_at_end); /* - * Emit an instruction that has no effect and will be removed by optimization - * passes. - * - * We need this workaround because some callsites will try to use - * llvm::Instruction::insertAfter on the back of the MergeBlock after a proof - * branch is created. If the MergeBlock has no instructions, this has resulted - * in a segfault when printing the IR. Adding an effective no-op prevents this. + * Emit a call to the `variable` API of the specified `proof_writer`. */ - llvm::BinaryOperator *emit_no_op(llvm::BasicBlock *insert_at_end); + llvm::CallInst *emit_write_variable( + llvm::Value *proof_writer, std::string const &name, llvm::Value *val, + kore_composite_sort &sort, llvm::BasicBlock *insert_at_end); /* - * Emit instructions to get a pointer to the interpreter's proof_trace_writer; - * the data structure that outputs proof trace data. + * Emit a call to the `rewrite_event_post` API of the specified `proof_writer`. */ - llvm::LoadInst *emit_get_proof_trace_writer(llvm::BasicBlock *insert_at_end); + llvm::CallInst *emit_write_rewrite_event_post( + llvm::Value *proof_writer, llvm::Value *val, kore_composite_sort &sort, + llvm::BasicBlock *insert_at_end); + + /* + * Emit a call to the `function_event_pre` API of the specified `proof_writer`. + */ + llvm::CallInst *emit_write_function_event_pre( + llvm::Value *proof_writer, std::string const &name, + std::string const &location_stack, llvm::BasicBlock *insert_at_end); + + /* + * Emit a call to the `function_event_post` API of the specified `proof_writer`. + */ + llvm::CallInst *emit_write_function_event_post( + llvm::Value *proof_writer, llvm::BasicBlock *insert_at_end); + + /* + * Emit a call to the `side_condition_event_pre` API of the specified `proof_writer`. + */ + llvm::CallInst *emit_write_side_condition_event_pre( + llvm::Value *proof_writer, uint64_t ordinal, uint64_t arity, + llvm::BasicBlock *insert_at_end); + + /* + * Emit a call to the `side_condition_event_post` API of the specified `proof_writer`. + */ + llvm::CallInst *emit_write_side_condition_event_post( + llvm::Value *proof_writer, uint64_t ordinal, llvm::Value *val, + llvm::BasicBlock *insert_at_end); public: [[nodiscard]] llvm::BasicBlock *hook_event_pre( diff --git a/include/runtime/header.h b/include/runtime/header.h index 661fcdb7b..70b047a85 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -344,18 +344,41 @@ void serialize_term_to_file( bool k_item_inj = false); void serialize_raw_term_to_file( FILE *file, void *subject, char const *sort, bool use_intern); +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, bool indirect); // The following functions are called by the generated code and runtime code to // ouput the proof trace data. -void serialize_configuration_to_proof_trace( - void *proof_writer, block *subject, uint32_t sort); void serialize_configuration_to_proof_writer( void *proof_writer, block *subject); void write_uint64_to_proof_trace(void *proof_writer, uint64_t i); void write_bool_to_proof_trace(void *proof_writer, bool b); void write_string_to_proof_trace(void *proof_writer, char const *str); -void serialize_term_to_proof_trace( - void *proof_writer, void *subject, uint64_t, bool); +void write_hook_event_pre_to_proof_trace( + void *proof_writer, char const *name, char const *pattern, + char const *location_stack); +void write_hook_event_post_to_proof_trace( + void *proof_writer, void *hook_result, uint64_t block_header, + bool indirect); +void write_argument_to_proof_trace( + void *proof_writer, void *arg, uint64_t block_header, bool indirect); +void write_rewrite_event_pre_to_proof_trace( + void *proof_writer, uint64_t ordinal, uint64_t arity); +void write_variable_to_proof_trace( + void *proof_writer, char const *name, void *var, uint64_t block_header, + bool indirect); +void write_rewrite_event_post_to_proof_trace( + void *proof_writer, void *config, uint64_t block_header, bool indirect); +void write_function_event_pre_to_proof_trace( + void *proof_writer, char const *name, char const *location_stack); +void write_function_event_post_to_proof_trace(void *proof_writer); +void write_side_condition_event_pre_to_proof_trace( + void *proof_writer, uint64_t ordinal, uint64_t arity); +void write_side_condition_event_post_to_proof_trace( + void *proof_writer, uint64_t ordinal, bool side_cond_result); +void write_configuration_to_proof_trace(void *proof_writer, block *config); // The following functions have to be generated at kompile time // and linked with the interpreter. diff --git a/include/runtime/proof_trace_writer.h b/include/runtime/proof_trace_writer.h new file mode 100644 index 000000000..91568960b --- /dev/null +++ b/include/runtime/proof_trace_writer.h @@ -0,0 +1,142 @@ +#ifndef RUNTIME_PROOF_TRACE_WRITER_H +#define RUNTIME_PROOF_TRACE_WRITER_H + +#include +#include + +#include + +class proof_trace_writer { +public: + virtual ~proof_trace_writer() = default; + + virtual void proof_trace_header(uint32_t version) = 0; + virtual void hook_event_pre( + char const *name, char const *pattern, char const *location_stack) + = 0; + virtual void + hook_event_post(void *hook_result, uint64_t block_header, bool indirect) + = 0; + virtual void argument(void *arg, uint64_t block_header, bool indirect) = 0; + virtual void rewrite_event_pre(uint64_t ordinal, uint64_t arity) = 0; + virtual void + variable(char const *name, void *var, uint64_t block_header, bool indirect) + = 0; + virtual void + rewrite_event_post(void *config, uint64_t block_header, bool indirect) + = 0; + virtual void function_event_pre(char const *name, char const *location_stack) + = 0; + virtual void function_event_post() = 0; + virtual void side_condition_event_pre(uint64_t ordinal, uint64_t arity) = 0; + virtual void + side_condition_event_post(uint64_t ordinal, bool side_cond_result) + = 0; + virtual void configuration(block *config) = 0; + virtual void end_of_trace() = 0; +}; + +class proof_trace_file_writer : public proof_trace_writer { +private: + FILE *file_; + + void write(void const *ptr, size_t len) { fwrite(ptr, len, 1, file_); } + + void write_string(char const *str, size_t len) { fwrite(str, 1, len, file_); } + + // Note: This method will not write a 0 at the end of string. + // The passed string should be 0 terminated. + void write_string(char const *str) { fputs(str, file_); } + + // Note: this method will write a 0 at the end of the string. + // The passed string should be 0 terminated. + void write_null_terminated_string(char const *str) { + write_string(str); + char n = 0; + write(&n, 1); + } + + void write_bool(bool b) { write(&b, sizeof(bool)); } + void write_uint32(uint32_t i) { write(&i, sizeof(uint32_t)); } + void write_uint64(uint64_t i) { write(&i, sizeof(uint64_t)); } + +public: + proof_trace_file_writer(FILE *file) + : file_(file) { } + + void proof_trace_header(uint32_t version) override { + write_string("HINT"); + write_uint32(version); + } + + void hook_event_pre( + char const *name, char const *pattern, + char const *location_stack) override { + write_uint64(kllvm::hook_event_sentinel); + write_null_terminated_string(name); + write_null_terminated_string(pattern); + write_null_terminated_string(location_stack); + } + + void hook_event_post( + void *hook_result, uint64_t block_header, bool indirect) override { + write_uint64(kllvm::hook_result_sentinel); + serialize_term_to_proof_trace(file_, hook_result, block_header, indirect); + } + + void argument(void *arg, uint64_t block_header, bool indirect) override { + serialize_term_to_proof_trace(file_, arg, block_header, indirect); + } + + void rewrite_event_pre(uint64_t ordinal, uint64_t arity) override { + write_uint64(kllvm::rule_event_sentinel); + write_uint64(ordinal); + write_uint64(arity); + } + + void variable( + char const *name, void *var, uint64_t block_header, + bool indirect) override { + write_null_terminated_string(name); + serialize_term_to_proof_trace(file_, var, block_header, indirect); + } + + void rewrite_event_post( + void *config, uint64_t block_header, bool indirect) override { + write_uint64(kllvm::config_sentinel); + serialize_term_to_proof_trace(file_, config, block_header, indirect); + } + + void + function_event_pre(char const *name, char const *location_stack) override { + write_uint64(kllvm::function_event_sentinel); + write_null_terminated_string(name); + write_null_terminated_string(location_stack); + } + + void function_event_post() override { + write_uint64(kllvm::function_end_sentinel); + } + + void side_condition_event_pre(uint64_t ordinal, uint64_t arity) override { + write_uint64(kllvm::side_condition_event_sentinel); + write_uint64(ordinal); + write_uint64(arity); + } + + void + side_condition_event_post(uint64_t ordinal, bool side_cond_result) override { + write_uint64(kllvm::side_condition_end_sentinel); + write_uint64(ordinal); + write_bool(side_cond_result); + } + + void configuration(block *config) override { + write_uint64(kllvm::config_sentinel); + serialize_configuration_to_proof_trace(file_, config, 0); + } + + void end_of_trace() override { } +}; + +#endif // RUNTIME_PROOF_TRACE_WRITER_H diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp index 460f8ecb4..b746f8ad6 100644 --- a/lib/codegen/ProofEvent.cpp +++ b/lib/codegen/ProofEvent.cpp @@ -24,16 +24,13 @@ llvm::Constant *create_global_sort_string_ptr( ast_to_string(sort), fmt::format("{}_str", sort.get_name()), 0, mod); } -} // namespace +bool get_indirect(std::string const &sort_name) { + return sort_name == "SortBool{}" || sort_name.substr(0, 9) == "SortMInt{"; +} -llvm::CallInst *proof_event::emit_serialize_term( - kore_composite_sort &sort, llvm::Value *proof_writer, llvm::Value *term, - llvm::BasicBlock *insert_at_end) { - auto b = llvm::IRBuilder(insert_at_end); +} // namespace - std::string sort_name = ast_to_string(sort); - bool indirect - = sort_name == "SortBool{}" || sort_name.substr(0, 9) == "SortMInt{"; +uint64_t proof_event::get_block_header(std::string const &sort_name) { std::string inj_name; if (sort_name == "SortKItem{}") { inj_name = "rawTerm{}"; @@ -43,8 +40,66 @@ llvm::CallInst *proof_event::emit_serialize_term( inj_name = "inj{" + sort_name + ", SortKItem{}}"; } auto *symbol = definition_->get_all_symbols().at(inj_name); - uint64_t block_header = get_block_header_val( + return get_block_header_val( module_, symbol, get_block_type(module_, definition_, symbol)); +} + +llvm::CallInst *proof_event::emit_write_hook_event_pre( + llvm::Value *proof_writer, std::string const &name, + std::string const &pattern, std::string const &location_stack, + 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 *func_ty = llvm::FunctionType::get( + void_ty, {i8_ptr_ty, i8_ptr_ty, i8_ptr_ty, i8_ptr_ty}, false); + + auto *func = get_or_insert_function( + module_, "write_hook_event_pre_to_proof_trace", func_ty); + + auto *var_name = b.CreateGlobalStringPtr(name, "", 0, module_); + auto *var_pattern = b.CreateGlobalStringPtr(pattern, "", 0, module_); + auto *var_location = b.CreateGlobalStringPtr(location_stack, "", 0, module_); + return b.CreateCall( + func, {proof_writer, var_name, var_pattern, var_location}); +} + +llvm::CallInst *proof_event::emit_write_hook_event_post( + llvm::Value *proof_writer, llvm::Value *val, kore_composite_sort &sort, + llvm::BasicBlock *insert_at_end) { + auto b = llvm::IRBuilder(insert_at_end); + + std::string sort_name = ast_to_string(sort); + bool indirect = get_indirect(sort_name); + uint64_t block_header = get_block_header(sort_name); + + auto *void_ty = llvm::Type::getVoidTy(ctx_); + auto *i8_ptr_ty = llvm::PointerType::getUnqual(ctx_); + auto *i1_ty = llvm::Type::getInt1Ty(ctx_); + auto *i64_ty = llvm::Type::getInt64Ty(ctx_); + + auto *func_ty = llvm::FunctionType::get( + void_ty, {i8_ptr_ty, i8_ptr_ty, i64_ty, i1_ty}, false); + + auto *func = get_or_insert_function( + module_, "write_hook_event_post_to_proof_trace", func_ty); + + auto *var_block_header = llvm::ConstantInt::get(i64_ty, block_header); + auto *var_indirect = llvm::ConstantInt::get(i1_ty, indirect); + return b.CreateCall( + func, {proof_writer, val, var_block_header, var_indirect}); +} + +llvm::CallInst *proof_event::emit_write_argument( + llvm::Value *proof_writer, llvm::Value *val, kore_composite_sort &sort, + llvm::BasicBlock *insert_at_end) { + auto b = llvm::IRBuilder(insert_at_end); + + std::string sort_name = ast_to_string(sort); + bool indirect = get_indirect(sort_name); + uint64_t block_header = get_block_header(sort_name); auto *void_ty = llvm::Type::getVoidTy(ctx_); auto *i8_ptr_ty = llvm::PointerType::getUnqual(ctx_); @@ -54,68 +109,160 @@ llvm::CallInst *proof_event::emit_serialize_term( auto *func_ty = llvm::FunctionType::get( void_ty, {i8_ptr_ty, i8_ptr_ty, i64_ty, i1_ty}, false); - auto *serialize = get_or_insert_function( - module_, "serialize_term_to_proof_trace", func_ty); + auto *func = get_or_insert_function( + module_, "write_argument_to_proof_trace", func_ty); + auto *var_block_header = llvm::ConstantInt::get(i64_ty, block_header); + auto *var_indirect = llvm::ConstantInt::get(i1_ty, indirect); return b.CreateCall( - serialize, - {proof_writer, term, llvm::ConstantInt::get(i64_ty, block_header), - llvm::ConstantInt::get(i1_ty, indirect)}); + func, {proof_writer, val, var_block_header, var_indirect}); } -llvm::CallInst *proof_event::emit_write_uint64( - llvm::Value *proof_writer, uint64_t value, +llvm::CallInst *proof_event::emit_write_rewrite_event_pre( + llvm::Value *proof_writer, uint64_t ordinal, uint64_t arity, 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_ptr_ty = llvm::Type::getInt64Ty(ctx_); + auto *i64_ty = llvm::Type::getInt64Ty(ctx_); auto *func_ty - = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i64_ptr_ty}, false); - auto *func - = get_or_insert_function(module_, "write_uint64_to_proof_trace", func_ty); + = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i64_ty, i64_ty}, false); - auto *i64_value = llvm::ConstantInt::get(i64_ptr_ty, value); + auto *func = get_or_insert_function( + module_, "write_rewrite_event_pre_to_proof_trace", func_ty); - return llvm::CallInst::Create( - func, {proof_writer, i64_value}, "", insert_at_end); + auto *var_ordinal = llvm::ConstantInt::get(i64_ty, ordinal); + auto *var_arity = llvm::ConstantInt::get(i64_ty, arity); + return b.CreateCall(func, {proof_writer, var_ordinal, var_arity}); } -llvm::CallInst *proof_event::emit_write_bool( - llvm::Value *proof_writer, llvm::Value *term, +llvm::CallInst *proof_event::emit_write_variable( + llvm::Value *proof_writer, std::string const &name, llvm::Value *val, + kore_composite_sort &sort, llvm::BasicBlock *insert_at_end) { + auto b = llvm::IRBuilder(insert_at_end); + + std::string sort_name = ast_to_string(sort); + bool indirect = get_indirect(sort_name); + uint64_t block_header = get_block_header(sort_name); + + auto *void_ty = llvm::Type::getVoidTy(ctx_); + auto *i8_ptr_ty = llvm::PointerType::getUnqual(ctx_); + auto *i1_ty = llvm::Type::getInt1Ty(ctx_); + auto *i64_ty = llvm::Type::getInt64Ty(ctx_); + + auto *func_ty = llvm::FunctionType::get( + void_ty, {i8_ptr_ty, i8_ptr_ty, i8_ptr_ty, i64_ty, i1_ty}, false); + + auto *func = get_or_insert_function( + module_, "write_variable_to_proof_trace", func_ty); + + auto *var_name = b.CreateGlobalStringPtr(name, "", 0, module_); + auto *var_block_header = llvm::ConstantInt::get(i64_ty, block_header); + auto *var_indirect = llvm::ConstantInt::get(i1_ty, indirect); + return b.CreateCall( + func, {proof_writer, var_name, val, var_block_header, var_indirect}); +} + +llvm::CallInst *proof_event::emit_write_rewrite_event_post( + llvm::Value *proof_writer, llvm::Value *val, kore_composite_sort &sort, llvm::BasicBlock *insert_at_end) { auto b = llvm::IRBuilder(insert_at_end); + std::string sort_name = ast_to_string(sort); + bool indirect = get_indirect(sort_name); + uint64_t block_header = get_block_header(sort_name); + auto *void_ty = llvm::Type::getVoidTy(ctx_); auto *i8_ptr_ty = llvm::PointerType::getUnqual(ctx_); + auto *i1_ty = llvm::Type::getInt1Ty(ctx_); + auto *i64_ty = llvm::Type::getInt64Ty(ctx_); - term = b.CreateIntToPtr(term, i8_ptr_ty); + auto *func_ty = llvm::FunctionType::get( + void_ty, {i8_ptr_ty, i8_ptr_ty, i64_ty, i1_ty}, false); + + auto *func = get_or_insert_function( + module_, "write_rewrite_event_post_to_proof_trace", func_ty); + + auto *var_block_header = llvm::ConstantInt::get(i64_ty, block_header); + auto *var_indirect = llvm::ConstantInt::get(i1_ty, indirect); + return b.CreateCall( + func, {proof_writer, val, var_block_header, var_indirect}); +} + +llvm::CallInst *proof_event::emit_write_function_event_pre( + llvm::Value *proof_writer, std::string const &name, + std::string const &location_stack, 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 *func_ty = llvm::FunctionType::get( + void_ty, {i8_ptr_ty, i8_ptr_ty, i8_ptr_ty}, false); + + auto *func = get_or_insert_function( + module_, "write_function_event_pre_to_proof_trace", func_ty); + + auto *var_name = b.CreateGlobalStringPtr(name, "", 0, module_); + auto *var_location = b.CreateGlobalStringPtr(location_stack, "", 0, module_); + return b.CreateCall(func, {proof_writer, var_name, var_location}); +} + +llvm::CallInst *proof_event::emit_write_function_event_post( + llvm::Value *proof_writer, 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 *func_ty = llvm::FunctionType::get(void_ty, {i8_ptr_ty}, false); + + auto *func = get_or_insert_function( + module_, "write_function_event_post_to_proof_trace", func_ty); + + return b.CreateCall(func, {proof_writer}); +} + +llvm::CallInst *proof_event::emit_write_side_condition_event_pre( + llvm::Value *proof_writer, uint64_t ordinal, uint64_t arity, + 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 *func_ty - = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i8_ptr_ty}, false); + = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i64_ty, i64_ty}, false); - auto *serialize - = get_or_insert_function(module_, "write_bool_to_proof_trace", func_ty); + auto *func = get_or_insert_function( + module_, "write_side_condition_event_pre_to_proof_trace", func_ty); - return b.CreateCall(serialize, {proof_writer, term}); + auto *var_ordinal = llvm::ConstantInt::get(i64_ty, ordinal); + auto *var_arity = llvm::ConstantInt::get(i64_ty, arity); + return b.CreateCall(func, {proof_writer, var_ordinal, var_arity}); } -llvm::CallInst *proof_event::emit_write_string( - llvm::Value *proof_writer, std::string const &str, +llvm::CallInst *proof_event::emit_write_side_condition_event_post( + llvm::Value *proof_writer, uint64_t ordinal, llvm::Value *val, 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 *i1_ty = llvm::Type::getInt1Ty(ctx_); + auto *i64_ty = llvm::Type::getInt64Ty(ctx_); auto *func_ty - = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i8_ptr_ty}, false); + = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i64_ty, i1_ty}, false); - auto *print - = get_or_insert_function(module_, "write_string_to_proof_trace", func_ty); + auto *func = get_or_insert_function( + module_, "write_side_condition_event_post_to_proof_trace", func_ty); - auto *varname = b.CreateGlobalStringPtr(str, "", 0, module_); - return b.CreateCall(print, {proof_writer, varname}); + auto *var_ordinal = llvm::ConstantInt::get(i64_ty, ordinal); + return b.CreateCall(func, {proof_writer, var_ordinal, val}); } llvm::BinaryOperator *proof_event::emit_no_op(llvm::BasicBlock *insert_at_end) { @@ -177,11 +324,9 @@ llvm::BasicBlock *proof_event::hook_event_pre( auto [true_block, merge_block, proof_writer] = event_prelude("hookpre", current_block); - emit_write_uint64(proof_writer, detail::word(0xAA), true_block); - emit_write_string(proof_writer, name, true_block); - emit_write_string( - proof_writer, ast_to_string(*pattern->get_constructor()), true_block); - emit_write_string(proof_writer, location_stack, true_block); + emit_write_hook_event_pre( + proof_writer, name, ast_to_string(*pattern->get_constructor()), + location_stack, true_block); llvm::BranchInst::Create(merge_block, true_block); return merge_block; @@ -197,9 +342,7 @@ llvm::BasicBlock *proof_event::hook_event_post( auto [true_block, merge_block, proof_writer] = event_prelude("hookpost", current_block); - emit_write_uint64(proof_writer, detail::word(0xBB), true_block); - - emit_serialize_term(*sort, proof_writer, val, true_block); + emit_write_hook_event_post(proof_writer, val, *sort, true_block); llvm::BranchInst::Create(merge_block, true_block); return merge_block; @@ -223,7 +366,7 @@ llvm::BasicBlock *proof_event::argument( auto [true_block, merge_block, proof_writer] = event_prelude("eventarg", current_block); - emit_serialize_term(*sort, proof_writer, val, true_block); + emit_write_argument(proof_writer, val, *sort, true_block); llvm::BranchInst::Create(merge_block, true_block); return merge_block; @@ -245,9 +388,9 @@ llvm::BasicBlock *proof_event::rewrite_event_pre( auto [true_block, merge_block, proof_writer] = event_prelude("rewrite_pre", current_block); - emit_write_uint64(proof_writer, detail::word(0x22), true_block); - emit_write_uint64(proof_writer, axiom.get_ordinal(), true_block); - emit_write_uint64(proof_writer, arity, true_block); + emit_write_rewrite_event_pre( + proof_writer, axiom.get_ordinal(), arity, true_block); + for (auto entry = subst.begin(); entry != subst.end(); ++entry) { auto key = entry->getKey(); auto *val = entry->getValue(); @@ -255,8 +398,7 @@ llvm::BasicBlock *proof_event::rewrite_event_pre( auto sort = std::dynamic_pointer_cast(var->get_sort()); - emit_write_string(proof_writer, key.str(), true_block); - emit_serialize_term(*sort, proof_writer, val, true_block); + emit_write_variable(proof_writer, key.str(), val, *sort, true_block); } llvm::BranchInst::Create(merge_block, true_block); @@ -276,8 +418,8 @@ llvm::BasicBlock *proof_event::rewrite_event_post( auto return_sort = std::dynamic_pointer_cast( axiom->get_right_hand_side()->get_sort()); - emit_write_uint64(proof_writer, detail::word(0xFF), true_block); - emit_serialize_term(*return_sort, proof_writer, return_value, true_block); + emit_write_rewrite_event_post( + proof_writer, return_value, *return_sort, true_block); llvm::BranchInst::Create(merge_block, true_block); return merge_block; @@ -297,10 +439,9 @@ llvm::BasicBlock *proof_event::function_event_pre( auto [true_block, merge_block, proof_writer] = event_prelude("function_pre", current_block); - emit_write_uint64(proof_writer, detail::word(0xDD), true_block); - emit_write_string( - proof_writer, ast_to_string(*pattern->get_constructor()), true_block); - emit_write_string(proof_writer, location_stack, true_block); + emit_write_function_event_pre( + proof_writer, ast_to_string(*pattern->get_constructor()), location_stack, + true_block); llvm::BranchInst::Create(merge_block, true_block); return merge_block; @@ -315,7 +456,7 @@ proof_event::function_event_post(llvm::BasicBlock *current_block) { auto [true_block, merge_block, proof_writer] = event_prelude("function_post", current_block); - emit_write_uint64(proof_writer, detail::word(0x11), true_block); + emit_write_function_event_post(proof_writer, true_block); llvm::BranchInst::Create(merge_block, true_block); @@ -335,9 +476,7 @@ llvm::BasicBlock *proof_event::side_condition_event_pre( size_t ordinal = axiom.get_ordinal(); size_t arity = args.size(); - emit_write_uint64(proof_writer, detail::word(0xEE), true_block); - emit_write_uint64(proof_writer, ordinal, true_block); - emit_write_uint64(proof_writer, arity, true_block); + emit_write_side_condition_event_pre(proof_writer, ordinal, arity, true_block); kore_pattern *pattern = axiom.get_requires(); std::map vars; @@ -351,8 +490,7 @@ llvm::BasicBlock *proof_event::side_condition_event_pre( auto sort = std::dynamic_pointer_cast(var->get_sort()); - emit_write_string(proof_writer, var_name, true_block); - emit_serialize_term(*sort, proof_writer, val, true_block); + emit_write_variable(proof_writer, var_name, val, *sort, true_block); } llvm::BranchInst::Create(merge_block, true_block); @@ -372,9 +510,8 @@ llvm::BasicBlock *proof_event::side_condition_event_post( size_t ordinal = axiom.get_ordinal(); - emit_write_uint64(proof_writer, detail::word(0x33), true_block); - emit_write_uint64(proof_writer, ordinal, true_block); - emit_write_bool(proof_writer, check_result, true_block); + emit_write_side_condition_event_post( + proof_writer, ordinal, check_result, true_block); llvm::BranchInst::Create(merge_block, true_block); diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 3a6253553..139ae0ddf 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -4,6 +4,7 @@ #include #include "runtime/header.h" +#include "runtime/proof_trace_writer.h" #include @@ -624,13 +625,6 @@ void serialize_configuration_to_proof_writer( serialize_configuration_to_proof_trace(proof_writer, subject, 0); } -void serialize_configuration_to_proof_trace( - void *proof_writer, block *subject, uint32_t sort) { - static_cast(proof_writer)->write_string("\x7FKR2"); - serialize_configuration_to_proof_trace_internal( - proof_writer, subject, sort, false); -} - void serialize_configuration( block *subject, char const *sort, char **data_out, size_t *size_out, bool emit_size, bool use_intern) { @@ -665,6 +659,77 @@ void write_string_to_proof_trace(void *proof_writer, char const *str) { ->write_null_terminated_string(str); } +void serialize_configuration_to_proof_trace( + FILE *file, block *subject, uint32_t sort) { + fputs("\x7FKR2", file); + serialize_configuration_to_proof_trace_internal(file, subject, sort, false); +} + +void write_hook_event_pre_to_proof_trace( + void *proof_writer, char const *name, char const *pattern, + char const *location_stack) { + static_cast(proof_writer) + ->hook_event_pre(name, pattern, location_stack); +} + +void write_hook_event_post_to_proof_trace( + void *proof_writer, void *hook_result, uint64_t block_header, + bool indirect) { + static_cast(proof_writer) + ->hook_event_post(hook_result, block_header, indirect); +} + +void write_argument_to_proof_trace( + void *proof_writer, void *arg, uint64_t block_header, bool indirect) { + static_cast(proof_writer) + ->argument(arg, block_header, indirect); +} + +void write_rewrite_event_pre_to_proof_trace( + void *proof_writer, uint64_t ordinal, uint64_t arity) { + static_cast(proof_writer) + ->rewrite_event_pre(ordinal, arity); +} + +void write_variable_to_proof_trace( + void *proof_writer, char const *name, void *var, uint64_t block_header, + bool indirect) { + static_cast(proof_writer) + ->variable(name, var, block_header, indirect); +} + +void write_rewrite_event_post_to_proof_trace( + void *proof_writer, void *config, uint64_t block_header, bool indirect) { + static_cast(proof_writer) + ->rewrite_event_post(config, block_header, indirect); +} + +void write_function_event_pre_to_proof_trace( + void *proof_writer, char const *name, char const *location_stack) { + static_cast(proof_writer) + ->function_event_pre(name, location_stack); +} + +void write_function_event_post_to_proof_trace(void *proof_writer) { + static_cast(proof_writer)->function_event_post(); +} + +void write_side_condition_event_pre_to_proof_trace( + void *proof_writer, uint64_t ordinal, uint64_t arity) { + static_cast(proof_writer) + ->side_condition_event_pre(ordinal, arity); +} + +void write_side_condition_event_post_to_proof_trace( + void *proof_writer, uint64_t ordinal, bool side_cond_result) { + static_cast(proof_writer) + ->side_condition_event_post(ordinal, side_cond_result); +} + +void write_configuration_to_proof_trace(void *proof_writer, block *config) { + static_cast(proof_writer)->configuration(config); +} + void serialize_term_to_file( FILE *file, void *subject, char const *sort, bool use_intern, bool k_item_inj) { diff --git a/runtime/util/finish_rewriting.cpp b/runtime/util/finish_rewriting.cpp index 31d0e02b9..4d155dac2 100644 --- a/runtime/util/finish_rewriting.cpp +++ b/runtime/util/finish_rewriting.cpp @@ -1,6 +1,5 @@ -#include - #include +#include #include #include @@ -25,7 +24,7 @@ int32_t get_exit_code(block *); void init_outputs(char const *output_filename) { output_file = fopen(output_filename, "a"); if (proof_output) { - proof_writer = new kllvm::proof_trace_file_writer(output_file); + proof_writer = new proof_trace_file_writer(output_file); } } @@ -38,8 +37,8 @@ void init_outputs(char const *output_filename) { = std::unique_ptr(output_file, fclose); // Similar for deletinging the proof_output_buffer data structure - auto *w = static_cast(proof_writer); - [[maybe_unused]] auto deleter = std::unique_ptr(w); + auto *w = static_cast(proof_writer); + [[maybe_unused]] auto deleter = std::unique_ptr(w); if (error && safe_partial) { throw std::runtime_error( @@ -62,14 +61,13 @@ void init_outputs(char const *output_filename) { print_configuration(output_file, subject); } } else if (!error && !proof_hint_instrumentation_slow) { - w->write_uint64(0xFFFFFFFFFFFFFFFF); - serialize_configuration_to_proof_writer(proof_writer, subject); + write_configuration_to_proof_trace(proof_writer, subject); } auto exit_code = error ? 113 : get_exit_code(subject); if (proof_output) { - w->write_eof(); + w->end_of_trace(); } std::exit(exit_code); diff --git a/runtime/util/util.cpp b/runtime/util/util.cpp index d94ffda47..8cd9c8e60 100644 --- a/runtime/util/util.cpp +++ b/runtime/util/util.cpp @@ -1,4 +1,5 @@ #include "runtime/header.h" +#include "runtime/proof_trace_writer.h" #include @@ -34,9 +35,8 @@ block *construct_raw_term(void *subject, char const *sort, bool raw_value) { return static_cast(construct_composite_pattern(tag, args)); } -void print_proof_hint_header(kllvm::proof_trace_writer *writer) { +void print_proof_hint_header(proof_trace_writer *writer) { uint32_t version = 11; - writer->write_string("HINT"); - writer->write_uint32(version); + writer->proof_trace_header(version); } } From 1226f160ee1d7d7f5651c4f0c8621dcfec2aa621 Mon Sep 17 00:00:00 2001 From: Theodoros Kasampalis Date: Fri, 16 Aug 2024 16:54:30 -0500 Subject: [PATCH 3/6] removing old proof_trace_writer --- include/kllvm/binary/serializer.h | 40 ------- include/runtime/header.h | 29 ++--- lib/binary/serializer.cpp | 12 --- runtime/util/ConfigurationSerializer.cpp | 129 +++++++++-------------- 4 files changed, 63 insertions(+), 147 deletions(-) diff --git a/include/kllvm/binary/serializer.h b/include/kllvm/binary/serializer.h index 517024c5b..0f0d9eb3e 100644 --- a/include/kllvm/binary/serializer.h +++ b/include/kllvm/binary/serializer.h @@ -141,46 +141,6 @@ void serializer::emit(T val) { void emit_kore_rich_header(std::ostream &os, kore_definition *definition); -class proof_trace_writer { -public: - virtual ~proof_trace_writer() = default; - virtual void write(void const *ptr, size_t len) = 0; - - virtual void write_string(char const *str, size_t len) = 0; - - // Note: This method will not write a 0 at the end of string. - // The passed string should be 0 terminated. - virtual void write_string(char const *str) = 0; - - // Note: this method will write a 0 at the end of the string. - // The passed string should be 0 terminated. - void write_null_terminated_string(char const *str) { - write_string(str); - char n = 0; - write(&n, 1); - } - - virtual void write_eof() = 0; - - void write_bool(bool b) { write(&b, sizeof(bool)); } - void write_uint32(uint32_t i) { write(&i, sizeof(uint32_t)); } - void write_uint64(uint64_t i) { write(&i, sizeof(uint64_t)); } -}; - -class proof_trace_file_writer : public proof_trace_writer { -private: - FILE *file_; - -public: - proof_trace_file_writer(FILE *file) - : file_(file) { } - - void write(void const *ptr, size_t len) override; - void write_string(char const *str, size_t len) override; - void write_string(char const *str) override; - void write_eof() override { } -}; - } // namespace kllvm #endif diff --git a/include/runtime/header.h b/include/runtime/header.h index 70b047a85..70998d4f5 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -22,7 +22,6 @@ #include #include #include -#include #include #include @@ -351,11 +350,6 @@ void serialize_term_to_proof_trace( // The following functions are called by the generated code and runtime code to // ouput the proof trace data. -void serialize_configuration_to_proof_writer( - void *proof_writer, block *subject); -void write_uint64_to_proof_trace(void *proof_writer, uint64_t i); -void write_bool_to_proof_trace(void *proof_writer, bool b); -void write_string_to_proof_trace(void *proof_writer, char const *str); void write_hook_event_pre_to_proof_trace( void *proof_writer, char const *name, char const *pattern, char const *location_stack); @@ -423,16 +417,16 @@ using visitor = struct { }; using serialize_to_proof_trace_visitor = struct { - void (*visit_config)(void *, block *, uint32_t, bool); - void (*visit_map)(void *, map *, uint32_t, uint32_t, uint32_t); - void (*visit_list)(void *, list *, uint32_t, uint32_t, uint32_t); - void (*visit_set)(void *, set *, uint32_t, uint32_t, uint32_t); - void (*visit_int)(void *, mpz_t, uint32_t); - void (*visit_float)(void *, floating *, uint32_t); - void (*visit_bool)(void *, bool, uint32_t); - void (*visit_string_buffer)(void *, stringbuffer *, uint32_t); - void (*visit_m_int)(void *, size_t *, size_t, uint32_t); - void (*visit_range_map)(void *, rangemap *, uint32_t, uint32_t, uint32_t); + 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 print_map( @@ -446,8 +440,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, void *proof_writer, - serialize_to_proof_trace_visitor *printer); + block *subject, FILE *file, serialize_to_proof_trace_visitor *printer); stringbuffer *hook_BUFFER_empty(void); stringbuffer *hook_BUFFER_concat(stringbuffer *buf, string *s); diff --git a/lib/binary/serializer.cpp b/lib/binary/serializer.cpp index 5f30f2658..bef7b72d5 100644 --- a/lib/binary/serializer.cpp +++ b/lib/binary/serializer.cpp @@ -210,16 +210,4 @@ void emit_kore_rich_header(std::ostream &os, kore_definition *definition) { } } -void proof_trace_file_writer::write(void const *ptr, size_t len) { - fwrite(ptr, len, 1, file_); -} - -void proof_trace_file_writer::write_string(char const *str, size_t len) { - fwrite(str, 1, len, file_); -} - -void proof_trace_file_writer::write_string(char const *str) { - fputs(str, file_); -} - } // namespace kllvm diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 139ae0ddf..463d8ba66 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -58,7 +58,7 @@ static std::string drop_back(std::string const &s, int n) { void serialize_configuration_internal( writer *file, block *subject, char const *sort, bool is_var, void *state); void serialize_configuration_to_proof_trace_internal( - void *proof_writer, block *subject, uint32_t sort, bool is_var); + FILE *file, block *subject, uint32_t sort, bool is_var); /** * Emit a symbol of the form ctor{...}(...); this should be preceded by the @@ -79,10 +79,9 @@ const uint8_t COMPOSITE = 0x01; const uint8_t STRING = 0x00; const uint8_t NULL_BYTE = 0x00; -static void emit_symbol_to_proof_trace(void *proof_writer, int32_t tag) { - auto *w = static_cast(proof_writer); - w->write(&COMPOSITE, sizeof(COMPOSITE)); - w->write(&tag, sizeof(tag)); +static void emit_symbol_to_proof_trace(FILE *file, int32_t tag) { + fwrite(&COMPOSITE, sizeof(COMPOSITE), 1, file); + fwrite(&tag, sizeof(tag), 1, file); } /** @@ -122,14 +121,13 @@ static void emit_token( } static void emit_token_to_proof_trace( - void *proof_writer, uint32_t sort, char const *str, size_t len) { - emit_symbol_to_proof_trace(proof_writer, sort); + FILE *file, uint32_t sort, char const *str, size_t len) { + emit_symbol_to_proof_trace(file, sort); - auto *w = static_cast(proof_writer); - w->write(&STRING, sizeof(STRING)); - w->write(&len, sizeof(len)); - w->write_string(str, len); - w->write(&NULL_BYTE, sizeof(NULL_BYTE)); + fwrite(&STRING, sizeof(STRING), 1, file); + fwrite(&len, sizeof(len), 1, file); + fwrite(str, 1, len, file); + fwrite(&NULL_BYTE, sizeof(NULL_BYTE), 1, file); } void serialize_map( @@ -160,11 +158,10 @@ void serialize_map( } void serialize_map_to_proof_trace( - void *proof_writer, map *map, uint32_t unit, uint32_t element, - uint32_t concat) { + FILE *file, map *map, uint32_t unit, uint32_t element, uint32_t concat) { size_t size = map->size(); if (size == 0) { - emit_symbol_to_proof_trace(proof_writer, unit); + emit_symbol_to_proof_trace(file, unit); return; } @@ -172,15 +169,15 @@ void serialize_map_to_proof_trace( = get_argument_sorts_for_tag_with_proof_trace_serialization(element); for (size_t i = 0; i < size - 1; ++i) { - emit_symbol_to_proof_trace(proof_writer, concat); + emit_symbol_to_proof_trace(file, concat); } for (auto iter = map->begin(); iter != map->end(); ++iter) { - emit_symbol_to_proof_trace(proof_writer, element); + emit_symbol_to_proof_trace(file, element); serialize_configuration_to_proof_trace_internal( - proof_writer, iter->first, arg_sorts[0], false); + file, iter->first, arg_sorts[0], false); serialize_configuration_to_proof_trace_internal( - proof_writer, iter->second, arg_sorts[1], false); + file, iter->second, arg_sorts[1], false); } } @@ -219,11 +216,11 @@ void serialize_range_map( } void serialize_range_map_to_proof_trace( - void *proof_writer, rangemap *map, uint32_t unit, uint32_t element, + FILE *file, rangemap *map, uint32_t unit, uint32_t element, uint32_t concat) { size_t size = map->size(); if (size == 0) { - emit_symbol_to_proof_trace(proof_writer, unit); + emit_symbol_to_proof_trace(file, unit); return; } @@ -235,19 +232,19 @@ void serialize_range_map_to_proof_trace( = get_argument_sorts_for_tag_with_proof_trace_serialization(range_tag); for (size_t i = 0; i < size - 1; ++i) { - emit_symbol_to_proof_trace(proof_writer, concat); + emit_symbol_to_proof_trace(file, concat); } for (auto iter = rng_map::ConstRangeMapIterator(*map); iter.has_next(); ++iter) { - emit_symbol_to_proof_trace(proof_writer, element); - emit_symbol_to_proof_trace(proof_writer, range_tag); + emit_symbol_to_proof_trace(file, element); + emit_symbol_to_proof_trace(file, range_tag); serialize_configuration_to_proof_trace_internal( - proof_writer, iter->first.start(), range_sorts[0], false); + file, iter->first.start(), range_sorts[0], false); serialize_configuration_to_proof_trace_internal( - proof_writer, iter->first.end(), range_sorts[1], false); + file, iter->first.end(), range_sorts[1], false); serialize_configuration_to_proof_trace_internal( - proof_writer, iter->second, arg_sorts[1], false); + file, iter->second, arg_sorts[1], false); } } @@ -276,11 +273,10 @@ void serialize_list( } void serialize_list_to_proof_trace( - void *proof_writer, list *list, uint32_t unit, uint32_t element, - uint32_t concat) { + FILE *file, list *list, uint32_t unit, uint32_t element, uint32_t concat) { size_t size = list->size(); if (size == 0) { - emit_symbol_to_proof_trace(proof_writer, unit); + emit_symbol_to_proof_trace(file, unit); return; } @@ -288,13 +284,13 @@ void serialize_list_to_proof_trace( = get_argument_sorts_for_tag_with_proof_trace_serialization(element); for (size_t i = 0; i < size - 1; ++i) { - emit_symbol_to_proof_trace(proof_writer, concat); + emit_symbol_to_proof_trace(file, concat); } for (auto iter = list->begin(); iter != list->end(); ++iter) { - emit_symbol_to_proof_trace(proof_writer, element); + emit_symbol_to_proof_trace(file, element); serialize_configuration_to_proof_trace_internal( - proof_writer, *iter, arg_sorts[0], false); + file, *iter, arg_sorts[0], false); } } @@ -323,11 +319,10 @@ void serialize_set( } void serialize_set_to_proof_trace( - void *proof_writer, set *set, uint32_t unit, uint32_t element, - uint32_t concat) { + FILE *file, set *set, uint32_t unit, uint32_t element, uint32_t concat) { size_t size = set->size(); if (size == 0) { - emit_symbol_to_proof_trace(proof_writer, unit); + emit_symbol_to_proof_trace(file, unit); return; } @@ -335,13 +330,13 @@ void serialize_set_to_proof_trace( = get_argument_sorts_for_tag_with_proof_trace_serialization(element); for (size_t i = 0; i < size - 1; ++i) { - emit_symbol_to_proof_trace(proof_writer, concat); + emit_symbol_to_proof_trace(file, concat); } for (auto iter = set->begin(); iter != set->end(); ++iter) { - emit_symbol_to_proof_trace(proof_writer, element); + emit_symbol_to_proof_trace(file, element); serialize_configuration_to_proof_trace_internal( - proof_writer, *iter, arg_sorts[0], false); + file, *iter, arg_sorts[0], false); } } @@ -352,9 +347,9 @@ void serialize_int(writer *file, mpz_t i, char const *sort, void *state) { emit_token(instance, sort, str.c_str()); } -void serialize_int_to_proof_trace(void *proof_writer, mpz_t i, uint32_t sort) { +void serialize_int_to_proof_trace(FILE *file, mpz_t i, uint32_t sort) { auto str = int_to_string(i); - emit_token_to_proof_trace(proof_writer, sort, str.data(), str.length()); + emit_token_to_proof_trace(file, sort, str.data(), str.length()); } void serialize_float(writer *file, floating *f, char const *sort, void *state) { @@ -364,10 +359,9 @@ void serialize_float(writer *file, floating *f, char const *sort, void *state) { emit_token(instance, sort, str.c_str()); } -void serialize_float_to_proof_trace( - void *proof_writer, floating *f, uint32_t sort) { +void serialize_float_to_proof_trace(FILE *file, floating *f, uint32_t sort) { auto str = float_to_string(f); - emit_token_to_proof_trace(proof_writer, sort, str.data(), str.length()); + emit_token_to_proof_trace(file, sort, str.data(), str.length()); } void serialize_bool(writer *file, bool b, char const *sort, void *state) { @@ -377,9 +371,9 @@ void serialize_bool(writer *file, bool b, char const *sort, void *state) { emit_token(instance, sort, str); } -void serialize_bool_to_proof_trace(void *proof_writer, bool b, uint32_t sort) { +void serialize_bool_to_proof_trace(FILE *file, bool b, uint32_t sort) { std::string str = b ? "true" : "false"; - emit_token_to_proof_trace(proof_writer, sort, str.data(), str.length()); + emit_token_to_proof_trace(file, sort, str.data(), str.length()); } void serialize_string_buffer( @@ -390,8 +384,8 @@ void serialize_string_buffer( } void serialize_string_buffer_to_proof_trace( - void *proof_writer, stringbuffer *b, uint32_t sort) { - emit_token_to_proof_trace(proof_writer, sort, b->contents->data, b->strlen); + FILE *file, stringbuffer *b, uint32_t sort) { + emit_token_to_proof_trace(file, sort, b->contents->data, b->strlen); } void serialize_m_int( @@ -406,12 +400,12 @@ void serialize_m_int( } void serialize_m_int_to_proof_trace( - void *proof_writer, size_t *i, size_t bits, uint32_t sort) { + FILE *file, size_t *i, size_t bits, uint32_t sort) { auto str = (i == nullptr) ? std::string("0") : int_to_string(hook_MINT_import(i, bits, false)); auto buffer = fmt::format("{}p{}", str, bits); - emit_token_to_proof_trace(proof_writer, sort, buffer.data(), buffer.length()); + emit_token_to_proof_trace(file, sort, buffer.data(), buffer.length()); } void serialize_comma(writer *file, void *state) { } @@ -537,7 +531,7 @@ void serialize_configuration_internal( } void serialize_configuration_to_proof_trace_internal( - void *proof_writer, block *subject, uint32_t sort, bool is_var) { + FILE *file, block *subject, uint32_t sort, bool is_var) { if (is_var) { throw std::invalid_argument("does not support bound variables yet"); } @@ -549,19 +543,19 @@ void serialize_configuration_to_proof_trace_internal( throw std::invalid_argument("does not support bound variables yet"); } - emit_symbol_to_proof_trace(proof_writer, tag); + emit_symbol_to_proof_trace(file, tag); return; } uint16_t layout = get_layout(subject); if (!layout) { auto *str = (string *)subject; - emit_token_to_proof_trace(proof_writer, sort, str->data, len(subject)); + emit_token_to_proof_trace(file, sort, str->data, len(subject)); return; } uint32_t tag = tag_hdr(subject->h.hdr); - emit_symbol_to_proof_trace(proof_writer, tag); + emit_symbol_to_proof_trace(file, tag); serialize_to_proof_trace_visitor callbacks = {serialize_configuration_to_proof_trace_internal, @@ -575,8 +569,7 @@ void serialize_configuration_to_proof_trace_internal( serialize_m_int_to_proof_trace, serialize_range_map_to_proof_trace}; - visit_children_for_serialize_to_proof_trace( - subject, proof_writer, &callbacks); + visit_children_for_serialize_to_proof_trace(subject, file, &callbacks); } void serialize_configurations( @@ -620,11 +613,6 @@ void serialize_configuration_to_file( free(data); } -void serialize_configuration_to_proof_writer( - void *proof_writer, block *subject) { - serialize_configuration_to_proof_trace(proof_writer, subject, 0); -} - void serialize_configuration( block *subject, char const *sort, char **data_out, size_t *size_out, bool emit_size, bool use_intern) { @@ -646,19 +634,6 @@ void serialize_configuration( *size_out = size; } -void write_uint64_to_proof_trace(void *proof_writer, uint64_t i) { - static_cast(proof_writer)->write_uint64(i); -} - -void write_bool_to_proof_trace(void *proof_writer, bool b) { - static_cast(proof_writer)->write_bool(b); -} - -void write_string_to_proof_trace(void *proof_writer, char const *str) { - static_cast(proof_writer) - ->write_null_terminated_string(str); -} - void serialize_configuration_to_proof_trace( FILE *file, block *subject, uint32_t sort) { fputs("\x7FKR2", file); @@ -747,7 +722,7 @@ void serialize_term_to_file( } void serialize_term_to_proof_trace( - void *proof_writer, void *subject, uint64_t block_header, bool indirect) { + FILE *file, void *subject, uint64_t block_header, bool indirect) { void *arg = indirect ? (void *)&subject : subject; struct blockheader header_val { block_header @@ -755,7 +730,7 @@ void serialize_term_to_proof_trace( auto *term = (block *)kore_alloc(size_hdr(block_header)); term->h = header_val; store_symbol_children(term, &arg); - static_cast(proof_writer)->write_string("\x7FKR2"); + fputs("\x7FKR2", file); serialize_to_proof_trace_visitor callbacks = {serialize_configuration_to_proof_trace_internal, @@ -769,7 +744,7 @@ void serialize_term_to_proof_trace( serialize_m_int_to_proof_trace, serialize_range_map_to_proof_trace}; - visit_children_for_serialize_to_proof_trace(term, proof_writer, &callbacks); + visit_children_for_serialize_to_proof_trace(term, file, &callbacks); } void serialize_raw_term_to_file( From 1ce3f016e641e642ff65b809902cfdbf65b4ac84 Mon Sep 17 00:00:00 2001 From: Theodoros Kasampalis Date: Mon, 19 Aug 2024 08:38:35 -0500 Subject: [PATCH 4/6] fix bug in writing values of type i1 --- lib/codegen/ProofEvent.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp index b746f8ad6..690985d46 100644 --- a/lib/codegen/ProofEvent.cpp +++ b/lib/codegen/ProofEvent.cpp @@ -252,17 +252,17 @@ llvm::CallInst *proof_event::emit_write_side_condition_event_post( auto *void_ty = llvm::Type::getVoidTy(ctx_); auto *i8_ptr_ty = llvm::PointerType::getUnqual(ctx_); - auto *i1_ty = llvm::Type::getInt1Ty(ctx_); auto *i64_ty = llvm::Type::getInt64Ty(ctx_); auto *func_ty - = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i64_ty, i1_ty}, false); + = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i64_ty, i8_ptr_ty}, false); auto *func = get_or_insert_function( module_, "write_side_condition_event_post_to_proof_trace", func_ty); auto *var_ordinal = llvm::ConstantInt::get(i64_ty, ordinal); - return b.CreateCall(func, {proof_writer, var_ordinal, val}); + auto *var_val = b.CreateIntToPtr(val, i8_ptr_ty); + return b.CreateCall(func, {proof_writer, var_ordinal, var_val}); } llvm::BinaryOperator *proof_event::emit_no_op(llvm::BasicBlock *insert_at_end) { From 650b571e4874fc3de130634356ae38fedbc42879 Mon Sep 17 00:00:00 2001 From: Theodoros Kasampalis Date: Wed, 21 Aug 2024 13:35:43 -0500 Subject: [PATCH 5/6] clearer naming of write methods --- include/runtime/proof_trace_writer.h | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/include/runtime/proof_trace_writer.h b/include/runtime/proof_trace_writer.h index 91568960b..e59dd64d7 100644 --- a/include/runtime/proof_trace_writer.h +++ b/include/runtime/proof_trace_writer.h @@ -40,7 +40,7 @@ class proof_trace_file_writer : public proof_trace_writer { private: FILE *file_; - void write(void const *ptr, size_t len) { fwrite(ptr, len, 1, file_); } + void write_bytes(void const *ptr, size_t len) { fwrite(ptr, len, 1, file_); } void write_string(char const *str, size_t len) { fwrite(str, 1, len, file_); } @@ -52,13 +52,13 @@ class proof_trace_file_writer : public proof_trace_writer { // The passed string should be 0 terminated. void write_null_terminated_string(char const *str) { write_string(str); - char n = 0; - write(&n, 1); + char n = '\0'; + write_bytes(&n, 1); } - void write_bool(bool b) { write(&b, sizeof(bool)); } - void write_uint32(uint32_t i) { write(&i, sizeof(uint32_t)); } - void write_uint64(uint64_t i) { write(&i, sizeof(uint64_t)); } + void write_bool(bool b) { write_bytes(&b, sizeof(bool)); } + void write_uint32(uint32_t i) { write_bytes(&i, sizeof(uint32_t)); } + void write_uint64(uint64_t i) { write_bytes(&i, sizeof(uint64_t)); } public: proof_trace_file_writer(FILE *file) From 36885d55c9c886a087cca950bc0e7825123f4f56 Mon Sep 17 00:00:00 2001 From: Theodoros Kasampalis Date: Wed, 21 Aug 2024 14:03:48 -0500 Subject: [PATCH 6/6] support for new pattern_matching_failure event --- include/kllvm/codegen/ProofEvent.h | 7 +++++++ include/runtime/header.h | 2 ++ include/runtime/proof_trace_writer.h | 6 ++++++ lib/codegen/ProofEvent.cpp | 22 ++++++++++++++++++++-- runtime/util/ConfigurationSerializer.cpp | 6 ++++++ 5 files changed, 41 insertions(+), 2 deletions(-) diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h index d9ac6987d..195af8121 100644 --- a/include/kllvm/codegen/ProofEvent.h +++ b/include/kllvm/codegen/ProofEvent.h @@ -135,6 +135,13 @@ class proof_event { llvm::Value *proof_writer, uint64_t ordinal, llvm::Value *val, llvm::BasicBlock *insert_at_end); + /* + * Emit a call to the `patteern_matching_failure` API of the specified `proof_writer`. + */ + llvm::CallInst *emit_write_pattern_matching_failure( + llvm::Value *proof_writer, std::string const &function_name, + llvm::BasicBlock *insert_at_end); + public: [[nodiscard]] llvm::BasicBlock *hook_event_pre( std::string const &name, kore_composite_pattern *pattern, diff --git a/include/runtime/header.h b/include/runtime/header.h index 70998d4f5..43ec92e3d 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -372,6 +372,8 @@ void write_side_condition_event_pre_to_proof_trace( void *proof_writer, uint64_t ordinal, uint64_t arity); 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_configuration_to_proof_trace(void *proof_writer, block *config); // The following functions have to be generated at kompile time diff --git a/include/runtime/proof_trace_writer.h b/include/runtime/proof_trace_writer.h index e59dd64d7..d69db7a14 100644 --- a/include/runtime/proof_trace_writer.h +++ b/include/runtime/proof_trace_writer.h @@ -32,6 +32,7 @@ class proof_trace_writer { virtual void side_condition_event_post(uint64_t ordinal, bool side_cond_result) = 0; + virtual void pattern_matching_failure(char const *function_name) = 0; virtual void configuration(block *config) = 0; virtual void end_of_trace() = 0; }; @@ -131,6 +132,11 @@ class proof_trace_file_writer : public proof_trace_writer { write_bool(side_cond_result); } + void pattern_matching_failure(char const *function_name) override { + write_uint64(kllvm::pattern_matching_failure_sentinel); + write_null_terminated_string(function_name); + } + void configuration(block *config) override { write_uint64(kllvm::config_sentinel); serialize_configuration_to_proof_trace(file_, config, 0); diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp index a8e7b7e50..294e8b2d7 100644 --- a/lib/codegen/ProofEvent.cpp +++ b/lib/codegen/ProofEvent.cpp @@ -265,6 +265,25 @@ llvm::CallInst *proof_event::emit_write_side_condition_event_post( return b.CreateCall(func, {proof_writer, var_ordinal, var_val}); } +llvm::CallInst *proof_event::emit_write_pattern_matching_failure( + llvm::Value *proof_writer, std::string const &function_name, + 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 *func_ty + = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i8_ptr_ty}, false); + + auto *func = get_or_insert_function( + module_, "write_pattern_matching_failure_to_proof_trace", func_ty); + + auto *var_function_name + = b.CreateGlobalStringPtr(function_name, "", 0, module_); + return b.CreateCall(func, {proof_writer, var_function_name}); +} + llvm::BinaryOperator *proof_event::emit_no_op(llvm::BasicBlock *insert_at_end) { auto *i8_ty = llvm::Type::getInt8Ty(ctx_); auto *zero = llvm::ConstantInt::get(i8_ty, 0); @@ -530,8 +549,7 @@ llvm::BasicBlock *proof_event::pattern_matching_failure( std::string function_name = ast_to_string(*pattern.get_constructor()); - emit_write_uint64(proof_writer, detail::word(0x44), true_block); - emit_write_string(proof_writer, function_name, true_block); + emit_write_pattern_matching_failure(proof_writer, function_name, true_block); llvm::BranchInst::Create(merge_block, true_block); diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index 463d8ba66..b8b9d569f 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -701,6 +701,12 @@ void write_side_condition_event_post_to_proof_trace( ->side_condition_event_post(ordinal, side_cond_result); } +void write_pattern_matching_failure_to_proof_trace( + void *proof_writer, char const *function_name) { + static_cast(proof_writer) + ->pattern_matching_failure(function_name); +} + void write_configuration_to_proof_trace(void *proof_writer, block *config) { static_cast(proof_writer)->configuration(config); }