Print print intermediate configurations after some function events in kore-proof-trace (#1139)

This PR introduces a new feature to `kore-proof-trace` to build a
configuration with the contents of a top-level function before its
evaluation.

Due to the new way that function arguments are evaluated and printed in
the trace before the actual function, I talked with Mircea, and we
decided that printing the top-level function with the evaluated
arguments would be better than printing all the nested non-evaluated
functions.

Author: Robertorosmaninho

bindings/python/ast.cpp

@@ -454,7 +454,7 @@ void bind_proof_trace(py::module_ &m) {
           [](py::bytes const &bytes, kore_header const &header) {
             proof_trace_parser parser(false, false, header);
             auto str = std::string(bytes);
-            return parser.parse_proof_trace(str);
+            return parser.parse_proof_trace(str, false);
           },
           py::arg("bytes"), py::arg("header"));
 

include/kllvm/binary/ProofTraceParser.h

@@ -314,7 +314,9 @@ class llvm_rewrite_trace {
   }
   void add_trace_event(llvm_event const &event) { trace_.push_back(event); }
 
-  void print(std::ostream &out, bool expand_terms, unsigned indent = 0U) const;
+  void print(
+      std::ostream &out, bool expand_terms, unsigned indent = 0U,
+      bool intermediate_configs = false) const;
 };
 
 class proof_trace_parser {
@@ -686,9 +688,10 @@ class proof_trace_parser {
       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, bool intermediate_configs);
   std::optional<llvm_rewrite_trace>
-  parse_proof_trace_from_file(std::string const &filename);
-  std::optional<llvm_rewrite_trace> parse_proof_trace(std::string const &data);
+  parse_proof_trace(std::string const &data, bool intermediate_configs);
 
   friend class llvm_rewrite_trace_iterator;
 };
@@ -699,13 +702,16 @@ class llvm_rewrite_trace_iterator {
   std::unique_ptr<proof_trace_buffer> buffer_;
   llvm_event_type type_ = llvm_event_type::PreTrace;
   proof_trace_parser parser_;
+  std::shared_ptr<kore_composite_pattern> current_config_;
 
 public:
   llvm_rewrite_trace_iterator(
       std::unique_ptr<proof_trace_buffer> buffer, kore_header const &header);
   [[nodiscard]] uint32_t get_version() const { return version_; }
   std::optional<annotated_llvm_event> get_next_event();
-  void print(std::ostream &out, bool expand_terms, unsigned indent = 0U);
+  void print(
+      std::ostream &out, bool expand_terms, unsigned indent = 0U,
+      bool intermediate_configs = false);
 };
 
 } // namespace kllvm

include/kllvm/binary/ProofTraceUtils.h

@@ -0,0 +1,22 @@
+#ifndef KLLVM_PROOF_TRACE_UTILS_CPP
+#define KLLVM_PROOF_TRACE_UTILS_CPP
+
+#include <kllvm/ast/AST.h>
+#include <kllvm/binary/ProofTraceParser.h>
+
+namespace kllvm {
+
+/*
+ * This file contains utility functions that are used to pretty print
+ * the Proof Trace and manipulate its data structures.
+*/
+
+std::vector<int> parse_relative_location(std::string location);
+
+llvm_event *build_post_function_event(
+    sptr<kore_composite_pattern> &current_config,
+    sptr<llvm_function_event> &function_event, bool expand_terms);
+
+} // namespace kllvm
+
+#endif // KLLVM_PROOF_TRACE_UTILS_CPP

lib/binary/CMakeLists.txt

@@ -2,6 +2,7 @@ add_library(BinaryKore
   serializer.cpp
   deserializer.cpp
   ProofTraceParser.cpp
+  ProofTraceUtils.cpp
 )
 
 target_link_libraries(BinaryKore

lib/binary/ProofTraceParser.cpp

@@ -1,4 +1,4 @@
-#include <kllvm/binary/ProofTraceParser.h>
+#include <kllvm/binary/ProofTraceUtils.h>
 
 #include <fmt/format.h>
 #include <fstream>
@@ -174,24 +174,74 @@ llvm_rewrite_trace_iterator::get_next_event() {
 }
 
 void llvm_rewrite_trace_iterator::print(
-    std::ostream &out, bool expand_terms, unsigned ind) {
+    std::ostream &out, bool expand_terms, unsigned ind,
+    bool intermediate_configs) {
   std::string indent(ind * indent_size, ' ');
   out << fmt::format("{}version: {}\n", indent, version_);
   while (auto event = get_next_event()) {
     event.value().event.print(out, expand_terms, false, ind);
+    if (intermediate_configs) {
+      if (event.value().type == llvm_event_type::InitialConfig) {
+        current_config_ = std::dynamic_pointer_cast<kore_composite_pattern>(
+            event.value().event.getkore_pattern());
+      } else if (event.value().type == llvm_event_type::Trace) {
+        if (event.value().event.is_pattern()) {
+          current_config_ = std::dynamic_pointer_cast<kore_composite_pattern>(
+              event.value().event.getkore_pattern());
+        } else {
+          if (auto function_event
+              = std::dynamic_pointer_cast<llvm_function_event>(
+                  event.value().event.get_step_event())) {
+            auto *new_config_event = build_post_function_event(
+                current_config_, function_event, expand_terms);
+            if (new_config_event) {
+              current_config_
+                  = std::dynamic_pointer_cast<kore_composite_pattern>(
+                      new_config_event->getkore_pattern());
+              new_config_event->print(out, expand_terms, false, ind);
+            }
+          }
+        }
+      }
+    }
   }
 }
 
 void llvm_rewrite_trace::print(
-    std::ostream &out, bool expand_terms, unsigned ind) const {
+    std::ostream &out, bool expand_terms, unsigned ind,
+    bool intermediate_configs) const {
   std::string indent(ind * indent_size, ' ');
   out << fmt::format("{}version: {}\n", indent, version_);
   for (auto const &pre_trace_event : pre_trace_) {
     pre_trace_event.print(out, expand_terms, false, ind);
   }
   initial_config_.print(out, expand_terms, false, ind);
-  for (auto const &trace_event : trace_) {
-    trace_event.print(out, expand_terms, false, ind);
+  if (intermediate_configs) {
+    auto current_config = std::dynamic_pointer_cast<kore_composite_pattern>(
+        initial_config_.getkore_pattern());
+    for (auto const &trace_event : trace_) {
+      trace_event.print(out, expand_terms, false, ind);
+      if (trace_event.is_pattern()) {
+        current_config = std::dynamic_pointer_cast<kore_composite_pattern>(
+            trace_event.getkore_pattern());
+      } else {
+        if (auto function_event
+            = std::dynamic_pointer_cast<llvm_function_event>(
+                trace_event.get_step_event())) {
+          auto *new_config_event = build_post_function_event(
+              current_config, function_event, expand_terms);
+          if (new_config_event) {
+            current_config = std::dynamic_pointer_cast<kore_composite_pattern>(
+                new_config_event->getkore_pattern());
+            new_config_event->print(out, expand_terms, false, ind);
+          }
+        }
+      }
+    }
+  } else {
+    for (auto const &trace_event : trace_) {
+      trace_event.print(out, expand_terms, false, ind);
+    }
   }
 }
 
@@ -203,8 +253,8 @@ proof_trace_parser::proof_trace_parser(
     , header_(header)
     , kore_definition_(std::move(kore_definition)) { }
 
-std::optional<llvm_rewrite_trace>
-proof_trace_parser::parse_proof_trace(std::string const &data) {
+std::optional<llvm_rewrite_trace> proof_trace_parser::parse_proof_trace(
+    std::string const &data, bool intermediate_configs) {
   proof_trace_memory_buffer buffer(data.data(), data.data() + data.length());
   llvm_rewrite_trace trace;
   bool result = parse_trace(buffer, trace);
@@ -214,14 +264,15 @@ proof_trace_parser::parse_proof_trace(std::string const &data) {
   }
 
   if (verbose_) {
-    trace.print(std::cout, expand_terms_);
+    trace.print(std::cout, expand_terms_, 0U, intermediate_configs);
   }
 
   return trace;
 }
 
 std::optional<llvm_rewrite_trace>
-proof_trace_parser::parse_proof_trace_from_file(std::string const &filename) {
+proof_trace_parser::parse_proof_trace_from_file(
+    std::string const &filename, bool intermediate_configs) {
   std::ifstream file(filename, std::ios_base::binary);
   proof_trace_file_buffer buffer(std::move(file));
   llvm_rewrite_trace trace;
@@ -232,7 +283,7 @@ proof_trace_parser::parse_proof_trace_from_file(std::string const &filename) {
   }
 
   if (verbose_) {
-    trace.print(std::cout, expand_terms_);
+    trace.print(std::cout, expand_terms_, 0U, intermediate_configs);
   }
 
   return trace;

lib/binary/ProofTraceUtils.cpp

@@ -0,0 +1,77 @@
+#include <kllvm/ast/AST.h>
+#include <kllvm/binary/ProofTraceUtils.h>
+
+using namespace kllvm;
+
+std::vector<int> kllvm::parse_relative_location(std::string location) {
+  if (location.empty()) {
+    return {};
+  }
+  std::vector<int> positions;
+  std::string delimiter = ":";
+  size_t pos = 0;
+  std::string token;
+  while ((pos = location.find(delimiter)) != std::string::npos) {
+    token = location.substr(0, pos);
+    positions.push_back(std::stoi(token));
+    location.erase(0, pos + delimiter.length());
+  }
+  positions.push_back(std::stoi(location));
+  return positions;
+}
+
+llvm_event *kllvm::build_post_function_event(
+    sptr<kore_composite_pattern> &current_config,
+    sptr<llvm_function_event> &function_event, bool expand_terms) {
+  sptr<kore_composite_pattern> new_config = nullptr;
+
+  // The name of the function is actually the kore_symbol
+  // corresponding to the function's constructor: function_name{...}
+  // We need to extract only the function name to build the composite pattern
+  auto function_name = function_event->get_name();
+  auto const *delimiter = "{";
+  auto pos = function_name.find(delimiter);
+  if (pos != std::string::npos) {
+    function_name = function_name.substr(0, pos);
+  }
+
+  // Construct the composite pattern for the function
+  auto function = sptr<kore_composite_pattern>(
+      kore_composite_pattern::create(function_name));
+  for (auto const &arg : function_event->get_arguments()) {
+    function->add_argument(arg.getkore_pattern());
+  }
+
+  // Construct location
+  std::string location = function_event->get_relative_position();
+  std::vector<int> positions = kllvm::parse_relative_location(location);
+
+  // We can only replace the argument and build a new configuration if we have a location
+  // And it's a top level function.
+  if (positions.size() == 1) {
+
+    // Create a new configuration, set the ith argument to be replaced by the function or a pattern with it
+    sptr<kore_composite_pattern> new_config
+        = kore_composite_pattern::create(current_config->get_constructor());
+    int index = positions[0];
+
+    // Add the new pattern to the new configuration
+    for (int i = 0; i < current_config->get_arguments().size(); i++) {
+      auto argument
+          = i == index ? function : current_config->get_arguments()[i];
+      new_config->add_argument(argument);
+    }
+
+    // Get new configuration size
+    std::stringstream ss;
+    new_config->print(ss);
+    auto new_config_size = ss.str().size();
+
+    auto *new_config_event = new llvm_event();
+    new_config_event->setkore_pattern(new_config, new_config_size);
+
+    return new_config_event;
+  }
+
+  return nullptr;
+}

test/lit.cfg.py

@@ -212,6 +212,28 @@ def exclude_macos(s):
             fi
         done
     ''')),
+    
+     ('%check-dir-proof-intermediate-out', one_line('''
+        %kore-rich-header %s > %t.header.bin
+        for out in %test-dir-out/*.proof.intermediate.out.diff; do
+            in=%test-dir-in/`basename $out .proof.intermediate.out.diff`.in
+            hint=%t.`basename $out .proof.intermediate.out.diff`.hint
+            rm -f $hint
+            %t.interpreter $in -1 $hint --proof-output
+            %kore-proof-trace --verbose --expand-terms --intermediate-configs %t.header.bin $hint | 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
+            %kore-proof-trace --streaming-parser --verbose --expand-terms --intermediate-configs %t.header.bin $hint | diff - $out
+            result="$?"
+            if [ "$result" -ne 0 ]; then
+                echo "kore-proof-trace error while parsing proof hint trace with expanded kore terms and streaming parser"
+                exit 1
+            fi
+        done
+    ''')),
 
     ('%run-binary-out', 'rm -f %t.out.bin && %t.interpreter %test-input -1 %t.out.bin --binary-output'),
     ('%run-binary', 'rm -f %t.bin && %convert-input && %t.interpreter %t.bin -1 /dev/stdout'),

test/output/builtin-io/read.proof.intermediate.out.diff

@@ -0,0 +1,54 @@
+version: 13
+hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} ()
+  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
+  arg: kore[\dv{SortString{}}("input_file")]
+hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
+hook: MAP.unit Lbl'Stop'Map{} ()
+hook result: kore[Lbl'Stop'Map{}()]
+hook: MAP.concat Lbl'Unds'Map'Unds'{} ()
+  arg: kore[Lbl'Stop'Map{}()]
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
+hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
+function: LblinitGeneratedTopCell{} ()
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
+rule: 2761 1
+  VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
+function: LblinitKCell{} (0)
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
+rule: 2762 1
+  VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
+hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0:0)
+  arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\dv{SortKConfigVar{}}("$PGM"),\dv{SortString{}}("input_file"))]
+  arg: kore[\dv{SortKConfigVar{}}("$PGM")]
+hook result: kore[\dv{SortString{}}("input_file")]
+function: Lblproject'Coln'String{} (0:0:0)
+  arg: kore[kseq{}(\dv{SortString{}}("input_file"),dotk{}())]
+rule: 2841 1
+  VarK = kore[\dv{SortString{}}("input_file")]
+function: LblinitFdCell{} (1)
+rule: 2759 0
+function: LblinitBufferCell{} (2)
+rule: 2758 0
+function: LblinitGeneratedCounterCell{} (3)
+rule: 2760 0
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(LblreadFromFile'LParUndsRParUnds'BUILTIN-IO'Unds'KItem'Unds'String{}(\dv{SortString{}}("input_file")),dotk{}())),Lbl'-LT-'fd'-GT-'{}(\dv{SortInt{}}("-1")),Lbl'-LT-'buffer'-GT-'{}(\dv{SortString{}}("")),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
+rule: 2712 4
+  Var'Unds'Gen0 = kore[Lbl'-LT-'fd'-GT-'{}(\dv{SortInt{}}("-1"))]
+  Var'Unds'Gen1 = kore[Lbl'-LT-'buffer'-GT-'{}(\dv{SortString{}}(""))]
+  Var'Unds'Gen2 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  VarFILE = kore[\dv{SortString{}}("input_file")]
+function: Lbl'Hash'open'LParUndsRParUnds'K-IO'Unds'IOInt'Unds'String{} (0:0:0:0)
+  arg: kore[\dv{SortString{}}("input_file")]
+rule: 2702 1
+  VarS = kore[\dv{SortString{}}("input_file")]
+hook: IO.open Lbl'Hash'open'LParUndsCommUndsRParUnds'K-IO'Unds'IOInt'Unds'String'Unds'String{} ()
+  arg: kore[\dv{SortString{}}("input_file")]
+  arg: kore[\dv{SortString{}}("r+")]
+hook result: kore[Lbl'Hash'ENOENT{}()]
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lblopen'LParUndsRParUnds'BUILTIN-IO'Unds'KItem'Unds'IOInt{}(Lbl'Hash'ENOENT{}()),dotk{}())),Lbl'-LT-'fd'-GT-'{}(\dv{SortInt{}}("-1")),Lbl'-LT-'buffer'-GT-'{}(\dv{SortString{}}("")),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]
+rule: 2710 4
+  Var'Unds'Gen0 = kore[\dv{SortInt{}}("-1")]
+  Var'Unds'Gen1 = kore[Lbl'-LT-'buffer'-GT-'{}(\dv{SortString{}}(""))]
+  Var'Unds'Gen2 = kore[Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0"))]
+  VarE = kore[Lbl'Hash'ENOENT{}()]
+config: kore[Lbl'-LT-'generatedTop'-GT-'{}(Lbl'-LT-'k'-GT-'{}(kseq{}(Lbl'Hash'ENOENT{}(),dotk{}())),Lbl'-LT-'fd'-GT-'{}(\dv{SortInt{}}("-2")),Lbl'-LT-'buffer'-GT-'{}(\dv{SortString{}}("")),Lbl'-LT-'generatedCounter'-GT-'{}(\dv{SortInt{}}("0")))]