Adding a side condition exit event to the proof hint trace (#982)

The new event carries the result of the side condition check. --------- Co-authored-by: rv-jenkins <admin@runtimeverification.com>
runtimeverification · Feb 16, 2024 · c4675e2 · c4675e2
1 parent 8918d3e
commit c4675e2
Show file tree

Hide file tree

Showing 9 changed files with 768 additions and 342 deletions.
diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp
@@ -392,6 +392,14 @@ void bind_proof_trace(py::module_ &m) {
       LLVMSideConditionEvent, std::shared_ptr<LLVMSideConditionEvent>>(
       proof_trace, "LLVMSideConditionEvent", llvm_rewrite_event);
 
+  py::class_<
+      LLVMSideConditionEndEvent, std::shared_ptr<LLVMSideConditionEndEvent>>(
+      proof_trace, "LLVMSideConditionEndEvent", llvm_step_event)
+      .def_property_readonly(
+          "rule_ordinal", &LLVMSideConditionEndEvent::getRuleOrdinal)
+      .def_property_readonly(
+          "check_result", &LLVMSideConditionEndEvent::getKOREPattern);
+
   py::class_<LLVMFunctionEvent, std::shared_ptr<LLVMFunctionEvent>>(
       proof_trace, "LLVMFunctionEvent", llvm_step_event)
       .def_property_readonly("name", &LLVMFunctionEvent::getName)

diff --git a/docs/proof-trace.md b/docs/proof-trace.md
@@ -23,36 +23,38 @@ Here is a BNF styled description of the format:
 ```
 proof_trace ::= header event*
 
-header      ::= "HINT" <4-byte version number>
+header            ::= "HINT" <4-byte version number>
 
-event       ::= hook
-              | function
-              | rule
-              | side_cond
-              | config
+event             ::= hook
+                    | function
+                    | rule
+                    | side_cond_entry
+                    | side_cond_exit
+                    | config
 
-argument    ::= hook
-              | function
-              | rule
-              | kore_term
+argument          ::= hook
+                    | function
+                    | rule
+                    | kore_term
 
-name        ::= string
-location    ::= string
-function    ::= WORD(0xDD) name location arg* WORD(0x11)
+name              ::= string
+location          ::= string
+function          ::= WORD(0xDD) name location arg* WORD(0x11)
 
-hook        ::= WORD(0xAA) name location arg* WORD(0xBB) kore_term
+hook              ::= WORD(0xAA) name location arg* WORD(0xBB) kore_term
 
-ordinal     ::= uint64
-arity       ::= uint64
-variable    ::= name kore_term WORD(0xCC)
-rule        ::= WORD(0x22) ordinal arity variable*
+ordinal           ::= uint64
+arity             ::= uint64
+variable          ::= name kore_term WORD(0xCC)
+rule              ::= WORD(0x22) ordinal arity variable*
 
-side_cond   ::= WORD(0xEE) ordinal arity variable*
+side_cond_entry   ::= WORD(0xEE) ordinal arity variable*
+side_cond_exit    ::= WORD(0x33) ordinal kore_term WORD(0xCC)
 
-config      ::= WORD(0xFF) kore_term WORD(0xCC)
+config            ::= WORD(0xFF) kore_term WORD(0xCC)
 
-string      ::= <c-style null terminated string>
-uint64      ::= <64-bit unsigned little endian integer>
+string            ::= <c-style null terminated string>
+uint64            ::= <64-bit unsigned little endian integer>
 ```
 
 ## Notes

diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h
@@ -32,6 +32,7 @@ constexpr uint64_t hook_event_sentinel = detail::word(0xAA);
 constexpr uint64_t hook_result_sentinel = detail::word(0xBB);
 constexpr uint64_t rule_event_sentinel = detail::word(0x22);
 constexpr uint64_t side_condition_event_sentinel = detail::word(0xEE);
+constexpr uint64_t side_condition_end_sentinel = detail::word(0x33);
 
 class LLVMStepEvent : public std::enable_shared_from_this<LLVMStepEvent> {
 public:
@@ -94,6 +95,34 @@ class LLVMSideConditionEvent : public LLVMRewriteEvent {
   virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
 };
 
+class LLVMSideConditionEndEvent : public LLVMStepEvent {
+private:
+  uint64_t ruleOrdinal;
+  sptr<KOREPattern> korePattern;
+  uint64_t patternLength;
+
+  LLVMSideConditionEndEvent(uint64_t _ruleOrdinal)
+      : ruleOrdinal(_ruleOrdinal)
+      , korePattern(nullptr)
+      , patternLength(0u) { }
+
+public:
+  static sptr<LLVMSideConditionEndEvent> Create(uint64_t _ruleOrdinal) {
+    return sptr<LLVMSideConditionEndEvent>(
+        new LLVMSideConditionEndEvent(_ruleOrdinal));
+  }
+
+  uint64_t getRuleOrdinal() const { return ruleOrdinal; }
+  sptr<KOREPattern> getKOREPattern() const { return korePattern; }
+  uint64_t getPatternLength() const { return patternLength; }
+  void setKOREPattern(sptr<KOREPattern> _korePattern, uint64_t _patternLength) {
+    korePattern = _korePattern;
+    patternLength = _patternLength;
+  }
+
+  virtual void print(std::ostream &Out, unsigned indent = 0u) const override;
+};
+
 class LLVMEvent;
 
 class LLVMFunctionEvent : public LLVMStepEvent {
@@ -210,7 +239,7 @@ class LLVMRewriteTrace {
 
 class ProofTraceParser {
 public:
-  static constexpr uint32_t expectedVersion = 4u;
+  static constexpr uint32_t expectedVersion = 5u;
 
 private:
   bool verbose;
@@ -499,6 +528,33 @@ class ProofTraceParser {
     return event;
   }
 
+  template <typename It>
+  sptr<LLVMSideConditionEndEvent> parse_side_condition_end(It &ptr, It end) {
+    if (!check_word(ptr, end, side_condition_end_sentinel)) {
+      return nullptr;
+    }
+
+    uint64_t ordinal;
+    if (!parse_ordinal(ptr, end, ordinal)) {
+      return nullptr;
+    }
+
+    auto event = LLVMSideConditionEndEvent::Create(ordinal);
+
+    uint64_t pattern_len;
+    auto kore_term = parse_kore_term(ptr, end, pattern_len);
+    if (!kore_term) {
+      return nullptr;
+    }
+    event->setKOREPattern(kore_term, pattern_len);
+
+    if (!check_word(ptr, end, kore_end_sentinel)) {
+      return nullptr;
+    }
+
+    return event;
+  }
+
   template <typename It>
   bool parse_argument(It &ptr, It end, LLVMEvent &event) {
     if (std::distance(ptr, end) >= 1u && detail::peek(ptr) == '\x7F') {
@@ -565,6 +621,8 @@ class ProofTraceParser {
 
     case side_condition_event_sentinel: return parse_side_condition(ptr, end);
 
+    case side_condition_end_sentinel: return parse_side_condition_end(ptr, end);
+
     default: return nullptr;
     }
   }

diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h
@@ -121,10 +121,14 @@ class ProofEvent {
   [[nodiscard]] llvm::BasicBlock *
   functionEvent_post(llvm::BasicBlock *current_block);
 
-  [[nodiscard]] llvm::BasicBlock *sideConditionEvent(
+  [[nodiscard]] llvm::BasicBlock *sideConditionEvent_pre(
       KOREAxiomDeclaration *axiom, std::vector<llvm::Value *> const &args,
       llvm::BasicBlock *current_block);
 
+  [[nodiscard]] llvm::BasicBlock *sideConditionEvent_post(
+      KOREAxiomDeclaration *axiom, llvm::Value *check_result,
+      llvm::BasicBlock *current_block);
+
 public:
   ProofEvent(KOREDefinition *Definition, llvm::Module *Module)
       : Definition(Definition)

diff --git a/lib/binary/ProofTraceParser.cpp b/lib/binary/ProofTraceParser.cpp
@@ -24,10 +24,19 @@ void LLVMRuleEvent::print(std::ostream &Out, unsigned indent) const {
 void LLVMSideConditionEvent::print(std::ostream &Out, unsigned indent) const {
   std::string Indent(indent * indent_size, ' ');
   Out << fmt::format(
-      "{}side condition: {} {}\n", Indent, ruleOrdinal, substitution.size());
+      "{}side condition entry: {} {}\n", Indent, ruleOrdinal,
+      substitution.size());
   printSubstitution(Out, indent + 1U);
 }
 
+void LLVMSideConditionEndEvent::print(
+    std::ostream &Out, unsigned indent) const {
+  std::string Indent(indent * indent_size, ' ');
+  Out << fmt::format(
+      "{}side condition exit: {} kore[{}]\n", Indent, ruleOrdinal,
+      patternLength);
+}
+
 void LLVMFunctionEvent::print(std::ostream &Out, unsigned indent) const {
   std::string Indent(indent * indent_size, ' ');
   Out << fmt::format("{}function: {} ({})\n", Indent, name, relativePosition);

diff --git a/lib/codegen/Decision.cpp b/lib/codegen/Decision.cpp
@@ -429,7 +429,7 @@ void FunctionNode::codegen(Decision *d) {
     ProofEvent p(d->Definition, d->Module);
     size_t ordinal = std::stoll(function.substr(15));
     KOREAxiomDeclaration *axiom = d->Definition->getAxiomByOrdinal(ordinal);
-    d->CurrentBlock = p.sideConditionEvent(axiom, args, d->CurrentBlock);
+    d->CurrentBlock = p.sideConditionEvent_pre(axiom, args, d->CurrentBlock);
   }
 
   CreateTerm creator(
@@ -438,6 +438,14 @@ void FunctionNode::codegen(Decision *d) {
       function, cat, args, function.substr(0, 5) == "hook_", false);
   Call->setName(name.substr(0, max_name_length));
   d->store(std::make_pair(name, type), Call);
+
+  if (isSideCondition) {
+    ProofEvent p(d->Definition, d->Module);
+    size_t ordinal = std::stoll(function.substr(15));
+    KOREAxiomDeclaration *axiom = d->Definition->getAxiomByOrdinal(ordinal);
+    d->CurrentBlock = p.sideConditionEvent_post(axiom, Call, d->CurrentBlock);
+  }
+
   if (d->FailPattern) {
     std::string debugName = function;
     if (function.substr(0, 5) == "hook_") {

diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp
@@ -304,15 +304,15 @@ ProofEvent::functionEvent_post(llvm::BasicBlock *current_block) {
   return merge_block;
 }
 
-llvm::BasicBlock *ProofEvent::sideConditionEvent(
+llvm::BasicBlock *ProofEvent::sideConditionEvent_pre(
     KOREAxiomDeclaration *axiom, std::vector<llvm::Value *> const &args,
     llvm::BasicBlock *current_block) {
   if (!ProofHintInstrumentation) {
     return current_block;
   }
 
   auto [true_block, merge_block, outputFile]
-      = eventPrelude("side_condition", current_block);
+      = eventPrelude("side_condition_pre", current_block);
 
   size_t ordinal = axiom->getOrdinal();
   size_t arity = args.size();
@@ -343,4 +343,29 @@ llvm::BasicBlock *ProofEvent::sideConditionEvent(
   return merge_block;
 }
 
+llvm::BasicBlock *ProofEvent::sideConditionEvent_post(
+    KOREAxiomDeclaration *axiom, llvm::Value *check_result,
+    llvm::BasicBlock *current_block) {
+  if (!ProofHintInstrumentation) {
+    return current_block;
+  }
+
+  auto [true_block, merge_block, outputFile]
+      = eventPrelude("side_condition_post", current_block);
+
+  size_t ordinal = axiom->getOrdinal();
+
+  auto check_result_sort = std::dynamic_pointer_cast<KORECompositeSort>(
+      axiom->getRequires()->getSort());
+
+  emitWriteUInt64(outputFile, detail::word(0x33), true_block);
+  emitWriteUInt64(outputFile, ordinal, true_block);
+  emitSerializeTerm(*check_result_sort, outputFile, check_result, true_block);
+  emitWriteUInt64(outputFile, detail::word(0xCC), true_block);
+
+  llvm::BranchInst::Create(merge_block, true_block);
+
+  return merge_block;
+}
+
 } // namespace kllvm
diff --git a/runtime/util/util.cpp b/runtime/util/util.cpp
@@ -39,7 +39,7 @@ block *constructRawTerm(void *subject, char const *sort, bool raw_value) {
 }
 
 void printProofHintHeader(FILE *file) {
-  uint32_t version = 4;
+  uint32_t version = 5;
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
 }