fix for passing MInts to emit-to-proof-trace functions

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`.
    */

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);

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,21 +320,21 @@ 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());
     }
   }
 
   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);
   }
 

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 <typename IRBuilder>
+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,51 +93,51 @@ 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(
     llvm::Value *proof_writer, llvm::Value *val, 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, 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,52 +165,52 @@ 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(
     llvm::Value *proof_writer, llvm::Value *val, 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, 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(

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_trace_writer *>(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_trace_writer *>(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_trace_writer *>(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_trace_writer *>(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
   };