Allow kore-proof-trace to display label and location info for i…

…mprove debugging if a kore definition file is given (#1098) Fix: Pi-Squared-Inc/pi2#1562 The Math Proof Team from Pi2 required that rule hints contain more high-level information, such as the `label` attribute, if present, and the k file `location` of a rule, instead of only printing the `ordinal` and `arity`, to help them debug their code. With that in mind, we propose that `kore-proof-trace` could take an extra/optional argument of a kore definition file. When this file is passed in the CLI, the tool will parse and preprocess it so we can extract these high-level info from the definition and print it in the hints human-readable output! If the definition isn't passed to the tool, it keeps this old behavior. The new output looks like this: - If the rule doesn’t have a label or location attr ``` rule: 101 0 [] [] ``` - If the rule has both attributes ``` rule: 97 2 [TEST-PROOF-TRACE.a-to-b] [/home/robertorosmaninho/rv/temp/test-proof-trace.k:7] Var'Unds'DotVar0 = kore[15] Var'Unds'DotVar1 = kore[4] ``` - If the rule doesn’t have a label but has a location attr ``` rule: 98 2 [] [/home/robertorosmaninho/rv/temp/test-proof-trace.k:8] Var'Unds'DotVar0 = kore[15] Var'Unds'DotVar1 = kore[4] ``` We decided to create only one test for this feature, as this is only for debugging, and duplicating every single file test would cause massive and tedious extra work to review not only this simple PR but any other PR that bumps the Hints version.
runtimeverification · Jul 9, 2024 · 67376bc · 67376bc
1 parent 169e15b
commit 67376bc
Show file tree

Hide file tree

Showing 6 changed files with 179 additions and 10 deletions.
diff --git a/include/kllvm/binary/ProofTraceParser.h b/include/kllvm/binary/ProofTraceParser.h
@@ -2,6 +2,7 @@
 #define PROOF_TRACE_PARSER_H
 
 #include <kllvm/ast/AST.h>
+#include <kllvm/ast/util.h>
 #include <kllvm/binary/deserializer.h>
 
 #include <iostream>
@@ -50,6 +51,9 @@ class llvm_rewrite_event : public llvm_step_event {
 private:
   uint64_t rule_ordinal_;
   substitution_t substitution_{};
+  std::string label_;
+  std::string location_;
+  bool debug_{};
 
 protected:
   void print_substitution(
@@ -58,11 +62,20 @@ class llvm_rewrite_event : public llvm_step_event {
 public:
   llvm_rewrite_event(uint64_t rule_ordinal)
       : rule_ordinal_(rule_ordinal) { }
+  llvm_rewrite_event(
+      uint64_t rule_ordinal, std::string label, std::string location)
+      : rule_ordinal_(rule_ordinal)
+      , label_(std::move(label))
+      , location_(std::move(location))
+      , debug_(true) { }
 
+  [[nodiscard]] std::string const &get_label() const { return label_; }
+  [[nodiscard]] std::string const &get_location() const { return location_; }
   [[nodiscard]] uint64_t get_rule_ordinal() const { return rule_ordinal_; }
   [[nodiscard]] substitution_t const &get_substitution() const {
     return substitution_;
   }
+  [[nodiscard]] bool print_debug_info() const { return debug_; }
 
   void add_substitution(
       std::string const &name, sptr<kore_pattern> const &term,
@@ -78,12 +91,22 @@ class llvm_rule_event : public llvm_rewrite_event {
 private:
   llvm_rule_event(uint64_t rule_ordinal)
       : llvm_rewrite_event(rule_ordinal) { }
+  llvm_rule_event(
+      uint64_t rule_ordinal, std::string label, std::string location)
+      : llvm_rewrite_event(
+          rule_ordinal, std::move(label), std::move(location)) { }
 
 public:
   static sptr<llvm_rule_event> create(uint64_t rule_ordinal) {
     return sptr<llvm_rule_event>(new llvm_rule_event(rule_ordinal));
   }
 
+  static sptr<llvm_rule_event>
+  create(uint64_t rule_ordinal, std::string label, std::string location) {
+    return sptr<llvm_rule_event>(new llvm_rule_event(
+        rule_ordinal, std::move(label), std::move(location)));
+  }
+
   void print(std::ostream &out, bool expand_terms, unsigned indent = 0U)
       const override;
 };
@@ -279,6 +302,8 @@ class proof_trace_parser {
   bool verbose_;
   bool expand_terms_;
   [[maybe_unused]] kore_header const &header_;
+  [[maybe_unused]] std::optional<kore_definition> kore_definition_
+      = std::nullopt;
 
   sptr<kore_pattern>
   parse_kore_term(proof_trace_buffer &buffer, uint64_t &pattern_len) {
@@ -439,8 +464,28 @@ class proof_trace_parser {
       return nullptr;
     }
 
-    auto event = llvm_rule_event::create(ordinal);
+    kllvm::sptr<llvm_rule_event> event;
+
+    if (kore_definition_) {
+      auto axiom = kore_definition_->get_axiom_by_ordinal(ordinal);
+      auto axiom_att = axiom.attributes();
+
+      std::string label;
+      if (axiom_att.contains(kllvm::attribute_set::key::Label)) {
+        label = axiom_att.get_string(kllvm::attribute_set::key::Label);
+      }
 
+      std::string location;
+      auto loc = kllvm::get_start_line_location(axiom);
+      if (loc.has_value()) {
+        location = loc.value().first + ":" + std::to_string(loc.value().second);
+      }
+
+      event = llvm_rule_event::create(ordinal, label, location);
+
+    } else {
+      event = llvm_rule_event::create(ordinal);
+    }
     for (auto i = 0; i < arity; i++) {
       if (!parse_variable(buffer, event)) {
         return nullptr;
@@ -648,7 +693,8 @@ class proof_trace_parser {
 
 public:
   proof_trace_parser(
-      bool verbose, bool expand_terms, kore_header const &header);
+      bool verbose, bool expand_terms, kore_header const &header,
+      std::optional<kore_definition> kore_definition = std::nullopt);
 
   std::optional<llvm_rewrite_trace>
   parse_proof_trace_from_file(std::string const &filename);

diff --git a/lib/binary/ProofTraceParser.cpp b/lib/binary/ProofTraceParser.cpp
@@ -48,8 +48,15 @@ void llvm_rewrite_event::print_substitution(
 void llvm_rule_event::print(
     std::ostream &out, bool expand_terms, unsigned ind) const {
   std::string indent(ind * indent_size, ' ');
-  out << fmt::format(
-      "{}rule: {} {}\n", indent, get_rule_ordinal(), get_substitution().size());
+  if (!print_debug_info()) {
+    out << fmt::format(
+        "{}rule: {} {}\n", indent, get_rule_ordinal(),
+        get_substitution().size());
+  } else {
+    out << fmt::format(
+        "{}rule: {} {} [{}] [{}]\n", indent, get_rule_ordinal(),
+        get_substitution().size(), get_label(), get_location());
+  }
   print_substitution(out, expand_terms, ind + 1U);
 }
 
@@ -65,9 +72,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, ' ');
-  out << fmt::format("{}side condition exit: {} ", indent, rule_ordinal_);
-  out << (result_ ? "true" : "false");
-  out << fmt::format("\n");
+  out << fmt::format(
+      "{}side condition exit: {} {}\n", indent, rule_ordinal_,
+      (result_ ? "true" : "false"));
 }
 
 void llvm_function_event::print(
@@ -182,10 +189,12 @@ void llvm_rewrite_trace::print(
 }
 
 proof_trace_parser::proof_trace_parser(
-    bool verbose, bool expand_terms, kore_header const &header)
+    bool verbose, bool expand_terms, kore_header const &header,
+    std::optional<kore_definition> kore_definition)
     : verbose_(verbose)
     , expand_terms_(expand_terms)
-    , header_(header) { }
+    , header_(header)
+    , kore_definition_(std::move(kore_definition)) { }
 
 std::optional<llvm_rewrite_trace>
 proof_trace_parser::parse_proof_trace(std::string const &data) {

diff --git a/test/lit.cfg.py b/test/lit.cfg.py
@@ -168,6 +168,21 @@ def one_line(s):
         fi
     ''')),
 
+    ('%check-proof-debug-out', one_line('''
+        out=%test-dir-out/*.proof.debug.out.diff
+        in=%test-dir-in/`basename $out .proof.debug.out.diff`.in
+        hint=%t.`basename $out .proof.debug.out.diff`.hint
+        rm -f $hint
+        %t.interpreter $in -1 $hint --proof-output
+        %kore-rich-header %s > %t.header.bin
+        %kore-proof-trace --verbose --expand-terms %t.header.bin $hint %s | diff - $out
+        result="$?"
+        if [ "$result" -ne 0 ]; then
+            echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms"
+            exit 1
+        fi
+     ''')),
+
     ('%check-dir-proof-out', one_line('''
         %kore-rich-header %s > %t.header.bin
         for out in %test-dir-out/*.proof.out.diff; do
@@ -207,6 +222,7 @@ def one_line(s):
     ('%test-dir-out', os.path.join('%output-dir', '%test-basename')),
     ('%test-dir-in', os.path.join('%input-dir', '%test-basename')),
     ('%test-proof-diff-out', os.path.join('%output-dir', '%test-basename.proof.out.diff')),
+    ('%test-proof-debug-diff-out', os.path.join('%output-dir', '%test-basename.proof.debug.out.diff')),
     ('%test-basename', '`basename %s .kore`'),
 
     ('%allow-pipefail', 'set +o pipefail'),

diff --git a/test/output/add-rewrite/input.proof.debug.out.diff b/test/output/add-rewrite/input.proof.debug.out.diff
@@ -0,0 +1,81 @@
+version: 11
+hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
+  function: Lbl'UndsPipe'-'-GT-Unds'{} ()
+  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
+  arg: kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+hook: MAP.unit Lbl'Stop'Map{} ()
+  function: Lbl'Stop'Map{} ()
+hook result: kore[Lbl'Stop'Map{}()]
+hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
+  function: Lbl'Unds'Map'Unds'{} ()
+  arg: kore[Lbl'Stop'Map{}()]
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+function: LblinitGeneratedTopCell{} ()
+rule: 111 1 [] []
+  VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+function: LblinitKCell{} (0)
+rule: 112 1 [] []
+  VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+function: Lblproject'Coln'KItem{} (0:0)
+  hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0)
+    function: LblMap'Coln'lookup{} (0:0:0:0)
+    arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+    arg: kore[\dv{SortKConfigVar{}}("$PGM")]
+  hook result: kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+rule: 153 1 [] []
+  VarK = kore[Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+function: LblinitGeneratedCounterCell{} (1)
+rule: 110 0 [] []
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
+rule: 107 5 [ADD-REWRITE.state-next] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:18]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[dotk{}()]
+  Var'Unds'Gen4 = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+  VarM = kore[Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()]
+  VarN = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+rule: 105 4 [ADD-REWRITE.add-succ] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:16]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),dotk{}())]
+  VarM = kore[Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()]
+  VarN = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+rule: 105 4 [ADD-REWRITE.add-succ] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:16]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),dotk{}())]
+  VarM = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+  VarN = kore[Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()]
+rule: 106 3 [ADD-REWRITE.add-zero] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:15]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()),dotk{}())]
+  VarN = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+rule: 103 6 [ADD-REWRITE.state-succ] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:20]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[dotk{}()]
+  Var'Unds'Gen0 = kore[Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()]
+  Var'Unds'Gen4 = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+  VarM = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+  VarN = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+rule: 107 5 [ADD-REWRITE.state-next] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:18]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[dotk{}()]
+  Var'Unds'Gen4 = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())]
+  VarM = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+  VarN = kore[Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()]
+rule: 105 4 [ADD-REWRITE.add-succ] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:16]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}(),Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))),dotk{}())]
+  VarM = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+  VarN = kore[Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()]
+rule: 106 3 [ADD-REWRITE.add-zero] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:15]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}(),Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))),dotk{}())]
+  VarN = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())))]
+rule: 103 6 [ADD-REWRITE.state-succ] [/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k:20]
+  Var'Unds'DotVar0 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  Var'Unds'DotVar1 = kore[dotk{}()]
+  Var'Unds'Gen0 = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+  Var'Unds'Gen4 = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())))]
+  VarM = kore[Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()))]
+  VarN = kore[Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}()]
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblstate'LParUndsCommUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'State'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}(),Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lbls'LParUndsRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat'Unds'Nat{}(Lblz'LParRParUnds'ADD-REWRITE-SYNTAX'Unds'Nat{}())))),dotk{}())),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
diff --git a/test/proof/add-rewrite.kore b/test/proof/add-rewrite.kore
@@ -1,5 +1,6 @@
 // RUN: %proof-interpreter
 // RUN: %check-dir-proof-out
+// RUN: %check-proof-debug-out
 [topCellInitializer{}(LblinitGeneratedTopCell{}()), org'Stop'kframework'Stop'attributes'Stop'Source{}("Source(/home/dwightguth/proof-checker/generation/k-benchmarks/add-rewrite/add-rewrite.k)")]
 
 module BASIC-K

diff --git a/tools/kore-proof-trace/main.cpp b/tools/kore-proof-trace/main.cpp
@@ -1,4 +1,5 @@
 #include <kllvm/binary/ProofTraceParser.h>
+#include <kllvm/parser/KOREParser.h>
 
 #include <llvm/Support/CommandLine.h>
 
@@ -18,6 +19,10 @@ cl::opt<std::string> input_filename(
     cl::Positional, cl::desc("<input file>"), cl::Required,
     cl::cat(kore_proof_trace_cat));
 
+cl::opt<std::string> kore_filename(
+    cl::Positional, cl::desc("[kore definition file]"), cl::Optional,
+    cl::cat(kore_proof_trace_cat));
+
 cl::opt<bool> verbose_output(
     "verbose",
     llvm::cl::desc("Print verbose information about the input proof trace"),
@@ -50,7 +55,18 @@ int main(int argc, char **argv) {
     return 0;
   }
 
-  proof_trace_parser parser(verbose_output, expand_terms_in_output, header);
+  std::optional<kore_definition> kore_def;
+
+  if (!kore_filename.empty()) {
+    std::fstream kore_file(kore_filename);
+    kore_def
+        = std::make_optional(*parser::kore_parser(kore_filename).definition());
+    kore_def->preprocess();
+  }
+
+  proof_trace_parser parser(
+      verbose_output, expand_terms_in_output, header, kore_def);
+
   auto trace = parser.parse_proof_trace_from_file(input_filename);
   if (trace.has_value()) {
     return 0;