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/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(

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.

include/runtime/proof_trace_writer.h

@@ -0,0 +1,142 @@
+#ifndef RUNTIME_PROOF_TRACE_WRITER_H
+#define RUNTIME_PROOF_TRACE_WRITER_H
+
+#include <kllvm/binary/ProofTraceParser.h>
+#include <runtime/header.h>
+
+#include <cstdio>
+
+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