Python bindings for the proof trace API (#939)

This PR adds python bindings for the proof trace parser. The PR also contains two more changes, that became apparent while I was working on the bindings: - The `LLVMRewriteTrace` object becomes a `class` rather than a `struct` and we provide bindings for that class. - The `ProofTraceParser` object does not accept the expected hints version as an argument to its constructor, but rather stores this information in a static constant. This made more sense since the parser currently supports only the latest hints version. In the future, if we want the parser to support older versions we can revisit this.
runtimeverification · Dec 22, 2023 · dbb5820 · dbb5820
1 parent 83a5b30
commit dbb5820
Show file tree

Hide file tree

Showing 10 changed files with 1,579 additions and 31 deletions.
diff --git a/bindings/python/ast.cpp b/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);
 }
diff --git a/include/kllvm/binary/ProofTraceParser.h b/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

diff --git a/lib/binary/CMakeLists.txt b/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

diff --git a/lib/binary/ProofTraceParser.cpp b/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
diff --git a/test/python/Inputs/proof-trace.in b/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{}())))
+)