Modify side_condition results to be only false or true in Proof…

… Hints (#1023)

This modification was proposed by the LLVM Backend and Math Proof
Generation Teams from Pi2 to optimize the Hints generated by the
`llvm-krun` as constructing and parsing the boolean values of the side
conditions takes some time. Then, we choose to simplify the way we're
generating these hints.

---------

Co-authored-by: Bruce Collie <[email protected]>

bindings/python/ast.cpp

@@ -405,7 +405,7 @@ void bind_proof_trace(py::module_ &m) {
       .def_property_readonly(
           "rule_ordinal", &llvm_side_condition_end_event::get_rule_ordinal)
       .def_property_readonly(
-          "check_result", &llvm_side_condition_end_event::getkore_pattern);
+          "check_result", &llvm_side_condition_end_event::get_result);
 
   py::class_<llvm_function_event, std::shared_ptr<llvm_function_event>>(
       proof_trace, "llvm_function_event", step_event)

docs/proof-trace.md

@@ -45,11 +45,12 @@ hook              ::= WORD(0xAA) name location arg* WORD(0xBB) kore_term
 
 ordinal           ::= uint64
 arity             ::= uint64
+boolean_result    ::= uint8
 variable          ::= name kore_term WORD(0xCC)
 rule              ::= WORD(0x22) ordinal arity variable*
 
 side_cond_entry   ::= WORD(0xEE) ordinal arity variable*
-side_cond_exit    ::= WORD(0x33) ordinal kore_term WORD(0xCC)
+side_cond_exit    ::= WORD(0x33) ordinal boolean_result
 
 config            ::= WORD(0xFF) kore_term WORD(0xCC)
 

include/kllvm/binary/ProofTraceParser.h

@@ -107,29 +107,21 @@ class llvm_side_condition_event : public llvm_rewrite_event {
 class llvm_side_condition_end_event : public llvm_step_event {
 private:
   uint64_t rule_ordinal_;
-  sptr<kore_pattern> kore_pattern_{};
-  uint64_t pattern_length_{0U};
+  bool result_;
 
-  llvm_side_condition_end_event(uint64_t rule_ordinal)
+  llvm_side_condition_end_event(uint64_t rule_ordinal, bool result)
       : rule_ordinal_(rule_ordinal)
-      , kore_pattern_(nullptr) { }
+      , result_(result) { }
 
 public:
-  static sptr<llvm_side_condition_end_event> create(uint64_t rule_ordinal) {
+  static sptr<llvm_side_condition_end_event>
+  create(uint64_t rule_ordinal, bool result) {
     return sptr<llvm_side_condition_end_event>(
-        new llvm_side_condition_end_event(rule_ordinal));
+        new llvm_side_condition_end_event(rule_ordinal, result));
   }
 
   [[nodiscard]] uint64_t get_rule_ordinal() const { return rule_ordinal_; }
-  [[nodiscard]] sptr<kore_pattern> getkore_pattern() const {
-    return kore_pattern_;
-  }
-  [[nodiscard]] uint64_t get_pattern_length() const { return pattern_length_; }
-  void
-  setkore_pattern(sptr<kore_pattern> kore_pattern, uint64_t pattern_length) {
-    kore_pattern_ = std::move(kore_pattern);
-    pattern_length_ = pattern_length;
-  }
+  [[nodiscard]] bool get_result() const { return result_; }
 
   void print(std::ostream &out, bool expand_terms, unsigned indent = 0U)
       const override;
@@ -268,7 +260,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 6U;
+  static constexpr uint32_t expected_version = 7U;
 
 private:
   bool verbose_;
@@ -333,6 +325,16 @@ class proof_trace_parser {
     return read_uint64(ptr, end, arity);
   }
 
+  template <typename It>
+  bool parse_bool(It &ptr, It end, bool &b) {
+    if (std::distance(ptr, end) < 1U) {
+      return false;
+    }
+
+    b = detail::read<bool>(ptr, end);
+    return true;
+  }
+
   template <typename It>
   sptr<kore_pattern> parse_kore_term(It &ptr, It end, uint64_t &pattern_len) {
     if (std::distance(ptr, end) < 11U) {
@@ -571,18 +573,14 @@ class proof_trace_parser {
       return nullptr;
     }
 
-    auto event = llvm_side_condition_end_event::create(ordinal);
-
-    uint64_t pattern_len = 0;
-    auto kore_term = parse_kore_term(ptr, end, pattern_len);
-    if (!kore_term) {
+    bool side_condition_result = false;
+    auto result = parse_bool(ptr, end, side_condition_result);
+    if (!result) {
       return nullptr;
     }
-    event->setkore_pattern(kore_term, pattern_len);
 
-    if (!check_word(ptr, end, kore_end_sentinel)) {
-      return nullptr;
-    }
+    auto event
+        = llvm_side_condition_end_event::create(ordinal, side_condition_result);
 
     return event;
   }

include/kllvm/codegen/ProofEvent.h

@@ -68,14 +68,21 @@ class proof_event {
       llvm::Value *output_file, uint64_t value,
       llvm::BasicBlock *insert_at_end);
 
+  /*
+  * Emit a call that will serialize a boolean value to the specified `output_file`.
+  */
+  llvm::CallInst *emit_bool_term(
+      llvm::Value *output_file, llvm::Value *term,
+      llvm::BasicBlock *insert_at_end);
+
   /*
    * Emit a call that will serialize `str` to the specified `outputFile`.
    */
   llvm::CallInst *emit_write_string(
       llvm::Value *output_file, std::string const &str,
       llvm::BasicBlock *insert_at_end);
 
-  /* 
+  /*
    * Emit an instruction that has no effect and will be removed by optimization
    * passes.
    *

include/runtime/header.h

@@ -334,6 +334,7 @@ void serialize_configuration(
 void serialize_configuration_to_file(
     FILE *file, block *subject, bool emit_size, bool use_intern);
 void write_uint64_to_file(FILE *file, uint64_t i);
+void write_bool_to_file(FILE *file, bool b);
 void serialize_term_to_file(
     FILE *file, block *subject, char const *sort, bool use_intern);
 void serialize_raw_term_to_file(

lib/binary/ProofTraceParser.cpp

@@ -63,16 +63,9 @@ void llvm_side_condition_event::print(
 void llvm_side_condition_end_event::print(
     std::ostream &out, bool expand_terms, unsigned ind) const {
   std::string indent(ind * indent_size, ' ');
-  if (expand_terms) {
-    out << fmt::format(
-        "{}side condition exit: {} kore[", indent, rule_ordinal_);
-    kore_pattern_->print(out);
-    out << fmt::format("]\n");
-  } else {
-    out << fmt::format(
-        "{}side condition exit: {} kore[{}]\n", indent, rule_ordinal_,
-        pattern_length_);
-  }
+  out << fmt::format("{}side condition exit: {} ", indent, rule_ordinal_);
+  out << (result_ ? "true" : "false");
+  out << fmt::format("\n");
 }
 
 void llvm_function_event::print(

lib/codegen/ProofEvent.cpp

@@ -104,6 +104,25 @@ llvm::CallInst *proof_event::emit_write_uint64(
       func, {output_file, i64_value}, "", insert_at_end);
 }
 
+llvm::CallInst *proof_event::emit_bool_term(
+    llvm::Value *output_file, llvm::Value *term,
+    llvm::BasicBlock *insert_at_end) {
+  auto b = llvm::IRBuilder(insert_at_end);
+
+  auto *void_ty = llvm::Type::getVoidTy(ctx_);
+  auto *i8_ptr_ty = llvm::Type::getInt8PtrTy(ctx_);
+
+  term = b.CreateIntToPtr(term, i8_ptr_ty);
+
+  auto *func_ty
+      = llvm::FunctionType::get(void_ty, {i8_ptr_ty, i8_ptr_ty}, false);
+
+  auto *serialize
+      = get_or_insert_function(module_, "write_bool_to_file", func_ty);
+
+  return b.CreateCall(serialize, {output_file, term});
+}
+
 llvm::CallInst *proof_event::emit_write_string(
     llvm::Value *output_file, std::string const &str,
     llvm::BasicBlock *insert_at_end) {
@@ -377,13 +396,9 @@ llvm::BasicBlock *proof_event::side_condition_event_post(
 
   size_t ordinal = axiom->get_ordinal();
 
-  auto check_result_sort = std::dynamic_pointer_cast<kore_composite_sort>(
-      axiom->get_requires()->get_sort());
-
   emit_write_uint64(outputFile, detail::word(0x33), true_block);
   emit_write_uint64(outputFile, ordinal, true_block);
-  emit_serialize_term(*check_result_sort, outputFile, check_result, true_block);
-  emit_write_uint64(outputFile, detail::word(0xCC), true_block);
+  emit_bool_term(outputFile, check_result, true_block);
 
   llvm::BranchInst::Create(merge_block, true_block);
 

runtime/util/ConfigurationSerializer.cpp

@@ -444,6 +444,10 @@ void write_uint64_to_file(FILE *file, uint64_t i) {
   fwrite(&i, 8, 1, file);
 }
 
+void write_bool_to_file(FILE *file, bool b) {
+  fwrite(&b, 1, 1, file);
+}
+
 void serialize_term_to_file(
     FILE *file, block *subject, char const *sort, bool use_intern) {
   char *data = nullptr;

runtime/util/util.cpp

@@ -35,7 +35,7 @@ block *construct_raw_term(void *subject, char const *sort, bool raw_value) {
 }
 
 void print_proof_hint_header(FILE *file) {
-  uint32_t version = 6;
+  uint32_t version = 7;
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
 }