Merge branch 'master' into patterns

bindings/python/ast.cpp

@@ -1,4 +1,5 @@
 #include <kllvm/ast/AST.h>
+#include <kllvm/binary/ProofTraceParser.h>
 #include <kllvm/binary/deserializer.h>
 #include <kllvm/binary/serializer.h>
 #include <kllvm/parser/KOREParser.h>
@@ -347,7 +348,70 @@ void bind_parser(py::module_ &mod) {
       });
 }
 
+void bind_proof_trace(py::module_ &m) {
+  auto proof_trace = m.def_submodule("prooftrace", "K LLVM backend KORE AST");
+
+  auto llvm_step_event
+      = py::class_<LLVMStepEvent, std::shared_ptr<LLVMStepEvent>>(
+            proof_trace, "LLVMStepEvent")
+            .def("__repr__", print_repr_adapter<LLVMStepEvent>());
+
+  auto llvm_rewrite_event
+      = py::class_<LLVMRewriteEvent, std::shared_ptr<LLVMRewriteEvent>>(
+            proof_trace, "LLVMREwriteEvent", llvm_step_event)
+            .def_property_readonly(
+                "rule_ordinal", &LLVMRewriteEvent::getRuleOrdinal)
+            .def_property_readonly(
+                "substitution", &LLVMRewriteEvent::getSubstitution);
+
+  py::class_<LLVMRuleEvent, std::shared_ptr<LLVMRuleEvent>>(
+      proof_trace, "LLVMRuleEvent", llvm_rewrite_event);
+
+  py::class_<LLVMSideConditionEvent, std::shared_ptr<LLVMSideConditionEvent>>(
+      proof_trace, "LLVMSideConditionEvent", llvm_rewrite_event);
+
+  py::class_<LLVMFunctionEvent, std::shared_ptr<LLVMFunctionEvent>>(
+      proof_trace, "LLVMFunctionEvent", llvm_step_event)
+      .def_property_readonly("name", &LLVMFunctionEvent::getName)
+      .def_property_readonly(
+          "relative_position", &LLVMFunctionEvent::getRelativePosition)
+      .def_property_readonly("args", &LLVMFunctionEvent::getArguments);
+
+  py::class_<LLVMHookEvent, std::shared_ptr<LLVMHookEvent>>(
+      proof_trace, "LLVMHookEvent", llvm_step_event)
+      .def_property_readonly("name", &LLVMHookEvent::getName)
+      .def_property_readonly(
+          "relative_position", &LLVMHookEvent::getRelativePosition)
+      .def_property_readonly("args", &LLVMHookEvent::getArguments)
+      .def_property_readonly("result", &LLVMHookEvent::getKOREPattern);
+
+  py::class_<LLVMEvent, std::shared_ptr<LLVMEvent>>(proof_trace, "Argument")
+      .def("__repr__", print_repr_adapter<LLVMEvent>(true))
+      .def_property_readonly("step_event", &LLVMEvent::getStepEvent)
+      .def_property_readonly("kore_pattern", &LLVMEvent::getKOREPattern)
+      .def("is_step_event", &LLVMEvent::isStep)
+      .def("is_kore_pattern", &LLVMEvent::isPattern);
+
+  py::class_<LLVMRewriteTrace, std::shared_ptr<LLVMRewriteTrace>>(
+      proof_trace, "LLVMRewriteTrace")
+      .def("__repr__", print_repr_adapter<LLVMRewriteTrace>())
+      .def_property_readonly("version", &LLVMRewriteTrace::getVersion)
+      .def_property_readonly("pre_trace", &LLVMRewriteTrace::getPreTrace)
+      .def_property_readonly(
+          "initial_config", &LLVMRewriteTrace::getInitialConfig)
+      .def_property_readonly("trace", &LLVMRewriteTrace::getTrace)
+      .def_static(
+          "parse",
+          [](py::bytes const &bytes) {
+            ProofTraceParser Parser(false);
+            auto str = std::string(bytes);
+            return Parser.parse_proof_trace(str);
+          },
+          py::arg("bytes"));
+}
+
 PYBIND11_MODULE(_kllvm, m) {
   bind_ast(m);
   bind_parser(m);
+  bind_proof_trace(m);
 }

include/kllvm/binary/ProofTraceParser.h

@@ -117,7 +117,7 @@ class LLVMFunctionEvent : public LLVMStepEvent {
 
   std::string const &getName() const { return name; }
   std::string const &getRelativePosition() const { return relativePosition; }
-  std::vector<LLVMEvent> const &getArguemnts() const { return arguments; }
+  std::vector<LLVMEvent> const &getArguments() const { return arguments; }
 
   void addArgument(LLVMEvent const &argument) { arguments.push_back(argument); }
 
@@ -147,7 +147,7 @@ class LLVMHookEvent : public LLVMStepEvent {
 
   std::string const &getName() const { return name; }
   std::string const &getRelativePosition() const { return relativePosition; }
-  std::vector<LLVMEvent> const &getArguemnts() const { return arguments; }
+  std::vector<LLVMEvent> const &getArguments() const { return arguments; }
   sptr<KOREPattern> getKOREPattern() const { return korePattern; }
   uint64_t getPatternLength() const { return patternLength; }
   void setKOREPattern(sptr<KOREPattern> _korePattern, uint64_t _patternLength) {
@@ -185,20 +185,35 @@ class LLVMEvent {
   void print(std::ostream &Out, bool isArg, unsigned indent = 0u) const;
 };
 
-struct LLVMRewriteTrace {
+class LLVMRewriteTrace {
+private:
   uint32_t version;
   std::vector<LLVMEvent> preTrace;
   LLVMEvent initialConfig;
   std::vector<LLVMEvent> trace;
 
+public:
+  uint32_t getVersion() const { return version; }
+  std::vector<LLVMEvent> const &getPreTrace() const { return preTrace; }
+  LLVMEvent getInitialConfig() const { return initialConfig; }
+  std::vector<LLVMEvent> const &getTrace() const { return trace; }
+  void setVersion(uint32_t _version) { version = _version; }
+  void setInitialConfig(LLVMEvent _initialConfig) {
+    initialConfig = _initialConfig;
+  }
+
+  void addPreTraceEvent(LLVMEvent const &event) { preTrace.push_back(event); }
+  void addTraceEvent(LLVMEvent const &event) { trace.push_back(event); }
+
   void print(std::ostream &Out, unsigned indent = 0u) const;
 };
 
 class ProofTraceParser {
+public:
+  static constexpr uint32_t expectedVersion = 3u;
 
 private:
   bool verbose;
-  uint32_t expectedVersion;
 
   // Caller needs to check that there are at least 8 bytes remaining in the
   // stream before peeking
@@ -586,14 +601,14 @@ class ProofTraceParser {
     if (!parse_header(ptr, end, version)) {
       return false;
     }
-    trace.version = version;
+    trace.setVersion(version);
 
     while (std::distance(ptr, end) >= 8u && peek_word(ptr) != config_sentinel) {
       LLVMEvent event;
       if (!parse_event(ptr, end, event)) {
         return false;
       }
-      trace.preTrace.push_back(event);
+      trace.addPreTraceEvent(event);
     }
 
     uint64_t pattern_len;
@@ -603,24 +618,25 @@ class ProofTraceParser {
     }
     LLVMEvent config_event;
     config_event.setKOREPattern(config, pattern_len);
-    trace.initialConfig = config_event;
+    trace.setInitialConfig(config_event);
 
     while (ptr != end) {
       LLVMEvent event;
       if (!parse_event(ptr, end, event)) {
         return false;
       }
-      trace.trace.push_back(event);
+      trace.addTraceEvent(event);
     }
 
     return true;
   }
 
 public:
-  ProofTraceParser(bool _verbose, uint32_t _expectedVersion);
+  ProofTraceParser(bool _verbose);
 
   std::optional<LLVMRewriteTrace>
-  parse_proof_trace(std::string const &filename);
+  parse_proof_trace_from_file(std::string const &filename);
+  std::optional<LLVMRewriteTrace> parse_proof_trace(std::string const &data);
 };
 
 } // namespace kllvm

lib/binary/CMakeLists.txt

@@ -8,10 +8,6 @@ target_link_libraries(BinaryKore
   PUBLIC AST fmt::fmt
 )
 
-target_link_libraries(BinaryKore
-  PUBLIC AST
-)
-
 install(
   TARGETS BinaryKore
   ARCHIVE DESTINATION lib/kllvm

lib/binary/ProofTraceParser.cpp

@@ -67,14 +67,11 @@ void LLVMRewriteTrace::print(std::ostream &Out, unsigned indent) const {
   }
 }
 
-ProofTraceParser::ProofTraceParser(bool _verbose, uint32_t _expectedVersion)
-    : verbose(_verbose)
-    , expectedVersion(_expectedVersion) { }
+ProofTraceParser::ProofTraceParser(bool _verbose)
+    : verbose(_verbose) { }
 
 std::optional<LLVMRewriteTrace>
-ProofTraceParser::parse_proof_trace(std::string const &filename) {
-  auto data = file_contents(filename);
-
+ProofTraceParser::parse_proof_trace(std::string const &data) {
   auto ptr = data.begin();
   LLVMRewriteTrace trace;
   bool result = parse_trace(ptr, data.end(), trace);
@@ -90,4 +87,10 @@ ProofTraceParser::parse_proof_trace(std::string const &filename) {
   return trace;
 }
 
+std::optional<LLVMRewriteTrace>
+ProofTraceParser::parse_proof_trace_from_file(std::string const &filename) {
+  auto data = file_contents(filename);
+  return parse_proof_trace(data);
+}
+
 } // namespace kllvm

test/python/Inputs/proof-trace.in

@@ -0,0 +1,9 @@
+LblinitGeneratedTopCell{}
+(
+Lbl'Unds'Map'Unds'{}(
+Lbl'Stop'Map{}()
+, Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\dv{SortKConfigVar{}}(
+"$PGM"
+)),
+inj{SortFoo{}, SortKItem{}}(Lbla'LParRParUnds'TEST-PROOF-TRACE-SYNTAX'Unds'Foo{}())))
+)