Abstract proof trace writer at event level (#1136)

This PR refactors the proof trace writer to be abstract at the event
generation level, rather than the byte stream level. We do this in order
to be able to use alternative ways of communicating the proof hints that
do not require writing the trace to a file, such as triggering of
callback invocations.

The PR can be reviewed commit by commit:
- the 1st commit removes an unused flag from main.ll
- the 2nd commit adds the new abstract `proof_trace_writer` and a
subclass that writes in a file as before.
- the 3rd commit removes the old `proof_trace_writer` that operated at
the level of writing byte streams.

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