Abstract proof trace writer at event level

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

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

include/kllvm/codegen/ProofEvent.h

@@ -44,52 +44,103 @@ 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::CallInst *emit_serialize_term(
-      kore_composite_sort &sort, llvm::Value *proof_writer, llvm::Value *term,
+  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_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);
+
+  /*
+   * 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(

include/runtime/header.h

@@ -22,7 +22,6 @@
 #include <immer/map.hpp>
 #include <immer/set.hpp>
 #include <kllvm/ast/AST.h>
-#include <kllvm/binary/serializer.h>
 #include <runtime/collections/rangemap.h>
 #include <unordered_set>
 
@@ -344,18 +343,38 @@ 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_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
 // and linked with the interpreter.
@@ -400,16 +419,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(
@@ -423,8 +442,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);