From fdb31c80963c5f4d61ee3258e86dc11a561002e0 Mon Sep 17 00:00:00 2001 From: Theodoros Kasampalis Date: Fri, 27 Sep 2024 13:18:27 -0500 Subject: [PATCH] fix for passing MInts to emit-to-proof-trace functions --- include/kllvm/codegen/ProofEvent.h | 7 +++ include/runtime/header.h | 10 ++-- include/runtime/proof_trace_writer.h | 48 ++++++++--------- lib/codegen/ProofEvent.cpp | 66 ++++++++++++++++-------- runtime/util/ConfigurationSerializer.cpp | 25 +++++---- 5 files changed, 95 insertions(+), 61 deletions(-) diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h index 36dcca9d1..cf66b4cf4 100644 --- a/include/kllvm/codegen/ProofEvent.h +++ b/include/kllvm/codegen/ProofEvent.h @@ -83,6 +83,13 @@ class proof_event { */ llvm::LoadInst *emit_get_proof_chunk_size(llvm::BasicBlock *insert_at_end); + /* + * Check if a value of the given `sort` corresponds to an llvm scalar and + * return the size in bits of that scalar. Returns 0 if the given `sort` does + * not correspond to an llvm scalar. + */ + uint64_t get_llvm_scalar_bits(kore_composite_sort &sort); + /* * Get the block header value for the given `sort_name`. */ diff --git a/include/runtime/header.h b/include/runtime/header.h index 619395917..366afa414 100644 --- a/include/runtime/header.h +++ b/include/runtime/header.h @@ -346,7 +346,7 @@ void serialize_raw_term_to_file( 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); + FILE *file, void *subject, uint64_t block_header, uint64_t bits); // The following functions are called by the generated code and runtime code to // ouput the proof trace data. @@ -355,16 +355,16 @@ void write_hook_event_pre_to_proof_trace( char const *location_stack); void write_hook_event_post_to_proof_trace( void *proof_writer, void *hook_result, uint64_t block_header, - bool indirect); + uint64_t bits); void write_argument_to_proof_trace( - void *proof_writer, void *arg, uint64_t block_header, bool indirect); + void *proof_writer, void *arg, uint64_t block_header, uint64_t bits); 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); + uint64_t bits); void write_rewrite_event_post_to_proof_trace( - void *proof_writer, void *config, uint64_t block_header, bool indirect); + void *proof_writer, void *config, uint64_t block_header, uint64_t bits); 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); diff --git a/include/runtime/proof_trace_writer.h b/include/runtime/proof_trace_writer.h index 8f08cbd0e..55c07c589 100644 --- a/include/runtime/proof_trace_writer.h +++ b/include/runtime/proof_trace_writer.h @@ -15,15 +15,15 @@ class proof_trace_writer { 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) + hook_event_post(void *hook_result, uint64_t block_header, uint64_t bits) = 0; - virtual void argument(void *arg, uint64_t block_header, bool indirect) = 0; + virtual void argument(void *arg, uint64_t block_header, uint64_t bits) = 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) + variable(char const *name, void *var, uint64_t block_header, uint64_t bits) = 0; virtual void - rewrite_event_post(void *config, uint64_t block_header, bool indirect) + rewrite_event_post(void *config, uint64_t block_header, uint64_t bits) = 0; virtual void function_event_pre(char const *name, char const *location_stack) = 0; @@ -106,13 +106,13 @@ class proof_trace_file_writer : public proof_trace_writer { } void hook_event_post( - void *hook_result, uint64_t block_header, bool indirect) override { + void *hook_result, uint64_t block_header, uint64_t bits) override { write_uint64(kllvm::hook_result_sentinel); - serialize_term_to_proof_trace(file_, hook_result, block_header, indirect); + serialize_term_to_proof_trace(file_, hook_result, block_header, bits); } - void argument(void *arg, uint64_t block_header, bool indirect) override { - serialize_term_to_proof_trace(file_, arg, block_header, indirect); + void argument(void *arg, uint64_t block_header, uint64_t bits) override { + serialize_term_to_proof_trace(file_, arg, block_header, bits); } void rewrite_event_pre(uint64_t ordinal, uint64_t arity) override { @@ -123,15 +123,15 @@ class proof_trace_file_writer : public proof_trace_writer { void variable( char const *name, void *var, uint64_t block_header, - bool indirect) override { + uint64_t bits) override { write_null_terminated_string(name); - serialize_term_to_proof_trace(file_, var, block_header, indirect); + serialize_term_to_proof_trace(file_, var, block_header, bits); } void rewrite_event_post( - void *config, uint64_t block_header, bool indirect) override { + void *config, uint64_t block_header, uint64_t bits) override { write_uint64(kllvm::config_sentinel); - serialize_term_to_proof_trace(file_, config, block_header, indirect); + serialize_term_to_proof_trace(file_, config, block_header, bits); } void @@ -191,17 +191,17 @@ class proof_trace_callback_writer : public proof_trace_writer { struct kore_term_construction { void *subject; uint64_t block_header; - bool indirect; + uint64_t bits; kore_term_construction() : subject(nullptr) , block_header(0) - , indirect(false) { } + , bits(0) { } - kore_term_construction(void *subject, uint64_t block_header, bool indirect) + kore_term_construction(void *subject, uint64_t block_header, uint64_t bits) : subject(subject) , block_header(block_header) - , indirect(indirect) { } + , bits(bits) { } }; struct kore_configuration_construction { @@ -301,13 +301,13 @@ class proof_trace_callback_writer : public proof_trace_writer { } void hook_event_post( - void *hook_result, uint64_t block_header, bool indirect) override { - current_call_event_->result.emplace(hook_result, block_header, indirect); + void *hook_result, uint64_t block_header, uint64_t bits) override { + current_call_event_->result.emplace(hook_result, block_header, bits); hook_event_callback(current_call_event_.value()); } - void argument(void *arg, uint64_t block_header, bool indirect) override { - current_call_event_->arguments.emplace_back(arg, block_header, indirect); + void argument(void *arg, uint64_t block_header, uint64_t bits) override { + current_call_event_->arguments.emplace_back(arg, block_header, bits); } void rewrite_event_pre(uint64_t ordinal, uint64_t arity) override { @@ -320,12 +320,12 @@ class proof_trace_callback_writer : public proof_trace_writer { void variable( char const *name, void *var, uint64_t block_header, - bool indirect) override { + uint64_t bits) override { auto &p = current_rewrite_event_->substitution[current_rewrite_event_->pos]; p.first = name; p.second.subject = var; p.second.block_header = block_header; - p.second.indirect = indirect; + p.second.bits = bits; size_t new_pos = ++current_rewrite_event_->pos; if (new_pos == current_rewrite_event_->arity) { rewrite_event_callback(current_rewrite_event_.value()); @@ -333,8 +333,8 @@ class proof_trace_callback_writer : public proof_trace_writer { } void rewrite_event_post( - void *config, uint64_t block_header, bool indirect) override { - kore_term_construction configuration(config, block_header, indirect); + void *config, uint64_t block_header, uint64_t bits) override { + kore_term_construction configuration(config, block_header, bits); configuration_term_event_callback(configuration); } diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp index 16b3343db..b8dc9dfe7 100644 --- a/lib/codegen/ProofEvent.cpp +++ b/lib/codegen/ProofEvent.cpp @@ -24,12 +24,34 @@ llvm::Constant *create_global_sort_string_ptr( ast_to_string(sort), fmt::format("{}_str", sort.get_name()), 0, mod); } -bool get_indirect(std::string const &sort_name) { - return sort_name == "SortBool{}" || sort_name.substr(0, 9) == "SortMInt{"; +template +llvm::Value *get_llvm_value_for_kore_term(llvm::Value *val, uint64_t bits, IRBuilder &b, llvm::Module *mod) { + if (bits <= 64) { + return val; + } + + // If the llvm value is larger than 64 bits, we need to pass its address to + // the runtime functions that emit proof trace events. + auto *int_ty = llvm::IntegerType::get(mod->getContext(), bits); + auto *ptr_val = b.CreateAlloca(int_ty); + b.CreateStore(val, ptr_val); + return ptr_val; } } // namespace +uint64_t proof_event::get_llvm_scalar_bits(kore_composite_sort &sort) { + value_type sort_category = sort.get_category(definition_); + switch (sort_category.cat) { + case sort_category::Bool: + return 1; + case sort_category::MInt: + return sort_category.bits; + default: + return 0; + } +} + uint64_t proof_event::get_block_header(std::string const &sort_name) { std::string inj_name; if (sort_name == "SortKItem{}") { @@ -71,25 +93,25 @@ llvm::CallInst *proof_event::emit_write_hook_event_post( llvm::BasicBlock *insert_at_end) { auto b = llvm::IRBuilder(insert_at_end); + uint64_t bits = get_llvm_scalar_bits(sort); 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); + void_ty, {i8_ptr_ty, i8_ptr_ty, i64_ty, i64_ty}, false); auto *func = get_or_insert_function( module_, "write_hook_event_post_to_proof_trace", func_ty); + auto *var_val = get_llvm_value_for_kore_term(val, bits, b, module_); auto *var_block_header = llvm::ConstantInt::get(i64_ty, block_header); - auto *var_indirect = llvm::ConstantInt::get(i1_ty, indirect); + auto *var_bits = llvm::ConstantInt::get(i64_ty, bits); return b.CreateCall( - func, {proof_writer, val, var_block_header, var_indirect}); + func, {proof_writer, var_val, var_block_header, var_bits}); } llvm::CallInst *proof_event::emit_write_argument( @@ -97,25 +119,25 @@ llvm::CallInst *proof_event::emit_write_argument( llvm::BasicBlock *insert_at_end) { auto b = llvm::IRBuilder(insert_at_end); + uint64_t bits = get_llvm_scalar_bits(sort); 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); + void_ty, {i8_ptr_ty, i8_ptr_ty, i64_ty, i64_ty}, false); auto *func = get_or_insert_function( module_, "write_argument_to_proof_trace", func_ty); + auto *var_val = get_llvm_value_for_kore_term(val, bits, b, module_); auto *var_block_header = llvm::ConstantInt::get(i64_ty, block_header); - auto *var_indirect = llvm::ConstantInt::get(i1_ty, indirect); + auto *var_bits = llvm::ConstantInt::get(i64_ty, bits); return b.CreateCall( - func, {proof_writer, val, var_block_header, var_indirect}); + func, {proof_writer, var_val, var_block_header, var_bits}); } llvm::CallInst *proof_event::emit_write_rewrite_event_pre( @@ -143,26 +165,26 @@ llvm::CallInst *proof_event::emit_write_variable( kore_composite_sort &sort, llvm::BasicBlock *insert_at_end) { auto b = llvm::IRBuilder(insert_at_end); + uint64_t bits = get_llvm_scalar_bits(sort); 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); + void_ty, {i8_ptr_ty, i8_ptr_ty, i8_ptr_ty, i64_ty, i64_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_val = get_llvm_value_for_kore_term(val, bits, b, module_); auto *var_block_header = llvm::ConstantInt::get(i64_ty, block_header); - auto *var_indirect = llvm::ConstantInt::get(i1_ty, indirect); + auto *var_bits = llvm::ConstantInt::get(i64_ty, bits); return b.CreateCall( - func, {proof_writer, var_name, val, var_block_header, var_indirect}); + func, {proof_writer, var_name, var_val, var_block_header, var_bits}); } llvm::CallInst *proof_event::emit_write_rewrite_event_post( @@ -170,25 +192,25 @@ llvm::CallInst *proof_event::emit_write_rewrite_event_post( llvm::BasicBlock *insert_at_end) { auto b = llvm::IRBuilder(insert_at_end); + uint64_t bits = get_llvm_scalar_bits(sort); 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); + void_ty, {i8_ptr_ty, i8_ptr_ty, i64_ty, i64_ty}, false); auto *func = get_or_insert_function( module_, "write_rewrite_event_post_to_proof_trace", func_ty); + auto *var_val = get_llvm_value_for_kore_term(val, bits, b, module_); auto *var_block_header = llvm::ConstantInt::get(i64_ty, block_header); - auto *var_indirect = llvm::ConstantInt::get(i1_ty, indirect); + auto *var_bits = llvm::ConstantInt::get(i64_ty, bits); return b.CreateCall( - func, {proof_writer, val, var_block_header, var_indirect}); + func, {proof_writer, var_val, var_block_header, var_bits}); } llvm::CallInst *proof_event::emit_write_function_event_pre( diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp index a8770d381..105db50a3 100644 --- a/runtime/util/ConfigurationSerializer.cpp +++ b/runtime/util/ConfigurationSerializer.cpp @@ -649,15 +649,15 @@ void write_hook_event_pre_to_proof_trace( void write_hook_event_post_to_proof_trace( void *proof_writer, void *hook_result, uint64_t block_header, - bool indirect) { + uint64_t bits) { static_cast(proof_writer) - ->hook_event_post(hook_result, block_header, indirect); + ->hook_event_post(hook_result, block_header, bits); } void write_argument_to_proof_trace( - void *proof_writer, void *arg, uint64_t block_header, bool indirect) { + void *proof_writer, void *arg, uint64_t block_header, uint64_t bits) { static_cast(proof_writer) - ->argument(arg, block_header, indirect); + ->argument(arg, block_header, bits); } void write_rewrite_event_pre_to_proof_trace( @@ -668,15 +668,15 @@ void write_rewrite_event_pre_to_proof_trace( void write_variable_to_proof_trace( void *proof_writer, char const *name, void *var, uint64_t block_header, - bool indirect) { + uint64_t bits) { static_cast(proof_writer) - ->variable(name, var, block_header, indirect); + ->variable(name, var, block_header, bits); } void write_rewrite_event_post_to_proof_trace( - void *proof_writer, void *config, uint64_t block_header, bool indirect) { + void *proof_writer, void *config, uint64_t block_header, uint64_t bits) { static_cast(proof_writer) - ->rewrite_event_post(config, block_header, indirect); + ->rewrite_event_post(config, block_header, bits); } void write_function_event_pre_to_proof_trace( @@ -734,8 +734,13 @@ void serialize_term_to_file( } void serialize_term_to_proof_trace( - FILE *file, void *subject, uint64_t block_header, bool indirect) { - void *arg = indirect ? (void *)&subject : subject; + FILE *file, void *subject, uint64_t block_header, uint64_t bits) { + void *arg = nullptr; + if (bits == 0 || bits > 64) { + arg = subject; + } else { + arg = (void *)&subject; + } struct blockheader header_val { block_header };