Exporting kore_symbol in hook_events and exposing symbol entry point in kore_parser (#1064)

This PR introduces the new version of the LLVM Backend Proof Hints:
Version 10.

The major update is in the `llvm_hook_event`, which will have a new
field: `kore_symbol`.
The new format of hook accepted and produced is:

```
symbol_name       ::= string
hook              ::= WORD(0xAA) name symbol_name location arg* WORD(0xBB) kore_term
```
 It also exposes the `symbol` entry point in the `kore_parser`.

This modification will help the Math Proof Team from Pi2 to parse the
`llvm_hook_event->kore_symbol` and `llvm_function_event` using the same
method.

---------

Co-authored-by: Bruce Collie <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 3 people

bindings/python/ast.cpp

@@ -373,9 +373,12 @@ void bind_parser(py::module_ &mod) {
           "pattern",
           [](kore_parser &parser) { return std::shared_ptr(parser.pattern()); })
       .def("sort", [](kore_parser &parser) { return parser.sort(); })
-      .def("definition", [](kore_parser &parser) {
-        return std::shared_ptr(parser.definition());
-      });
+      .def(
+          "definition",
+          [](kore_parser &parser) {
+            return std::shared_ptr(parser.definition());
+          })
+      .def("symbol", &kore_parser::symbol);
 }
 
 void bind_proof_trace(py::module_ &m) {
@@ -421,6 +424,7 @@ void bind_proof_trace(py::module_ &m) {
   py::class_<llvm_hook_event, std::shared_ptr<llvm_hook_event>>(
       proof_trace, "llvm_hook_event", step_event)
       .def_property_readonly("name", &llvm_hook_event::get_name)
+      .def_property_readonly("symbol_name", &llvm_hook_event::get_symbol_name)
       .def_property_readonly(
           "relative_position", &llvm_hook_event::get_relative_position)
       .def_property_readonly("args", &llvm_hook_event::get_arguments)

docs/proof-trace.md

@@ -48,7 +48,8 @@ name              ::= string
 location          ::= string
 function          ::= WORD(0xDD) name location arg* WORD(0x11) // the arg list is ommited in normal mode
 
-hook              ::= WORD(0xAA) name location arg* WORD(0xBB) kore_term
+symbol_name       ::= string
+hook              ::= WORD(0xAA) name symbol_name location arg* WORD(0xBB) kore_term
 
 ordinal           ::= uint64
 arity             ::= uint64

include/kllvm/binary/ProofTraceParser.h

@@ -159,20 +159,27 @@ class llvm_function_event : public llvm_step_event {
 class llvm_hook_event : public llvm_step_event {
 private:
   std::string name_;
+  std::string symbol_name_;
   std::string relative_position_;
   std::vector<llvm_event> arguments_;
   sptr<kore_pattern> kore_pattern_;
   uint64_t pattern_length_{0U};
 
-  llvm_hook_event(std::string name, std::string relative_position);
+  llvm_hook_event(
+      std::string name, std::string symbol_name, std::string relative_position);
 
 public:
-  static sptr<llvm_hook_event>
-  create(std::string const &name, std::string const &relative_position) {
-    return sptr<llvm_hook_event>(new llvm_hook_event(name, relative_position));
+  static sptr<llvm_hook_event> create(
+      std::string const &name, std::string const &symbol_name,
+      std::string const &relative_position) {
+    return sptr<llvm_hook_event>(
+        new llvm_hook_event(name, symbol_name, relative_position));
   }
 
   [[nodiscard]] std::string const &get_name() const { return name_; }
+  [[nodiscard]] std::string const &get_symbol_name() const {
+    return symbol_name_;
+  }
   [[nodiscard]] std::string const &get_relative_position() const {
     return relative_position_;
   }
@@ -260,7 +267,7 @@ class llvm_rewrite_trace {
 
 class proof_trace_parser {
 public:
-  static constexpr uint32_t expected_version = 9U;
+  static constexpr uint32_t expected_version = 10U;
 
 private:
   bool verbose_;
@@ -415,12 +422,17 @@ class proof_trace_parser {
       return nullptr;
     }
 
+    std::string symbol_name;
+    if (!parse_name(ptr, end, symbol_name)) {
+      return nullptr;
+    }
+
     std::string location;
     if (!parse_location(ptr, end, location)) {
       return nullptr;
     }
 
-    auto event = llvm_hook_event::create(name, location);
+    auto event = llvm_hook_event::create(name, symbol_name, location);
 
     while (std::distance(ptr, end) < 8U
            || peek_word(ptr) != hook_result_sentinel) {

include/kllvm/codegen/ProofEvent.h

@@ -92,8 +92,8 @@ class proof_event {
 
 public:
   [[nodiscard]] llvm::BasicBlock *hook_event_pre(
-      std::string const &name, llvm::BasicBlock *current_block,
-      std::string const &location_stack);
+      std::string const &name, kore_composite_pattern *pattern,
+      llvm::BasicBlock *current_block, std::string const &location_stack);
 
   [[nodiscard]] llvm::BasicBlock *hook_event_post(
       llvm::Value *val, kore_composite_sort *sort,

include/kllvm/parser/KOREParser.h

@@ -23,6 +23,7 @@ class kore_parser {
   ptr<kore_definition> definition();
   sptr<kore_pattern> pattern();
   sptr<kore_sort> sort();
+  ptr<kore_symbol> symbol();
   std::vector<ptr<kore_declaration>> declarations();
 
   std::pair<std::string, std::vector<sptr<kore_sort>>> symbol_sort_list();

lib/binary/ProofTraceParser.cpp

@@ -20,8 +20,9 @@ void llvm_function_event::add_argument(llvm_event const &argument) {
 }
 
 llvm_hook_event::llvm_hook_event(
-    std::string name, std::string relative_position)
+    std::string name, std::string symbol_name, std::string relative_position)
     : name_(std::move(name))
+    , symbol_name_(std::move(symbol_name))
     , relative_position_(std::move(relative_position))
     , kore_pattern_(nullptr) { }
 
@@ -81,7 +82,8 @@ void llvm_function_event::print(
 void llvm_hook_event::print(
     std::ostream &out, bool expand_terms, unsigned ind) const {
   std::string indent(ind * indent_size, ' ');
-  out << fmt::format("{}hook: {} ({})\n", indent, name_, relative_position_);
+  out << fmt::format(
+      "{}hook: {} {} ({})\n", indent, name_, symbol_name_, relative_position_);
   for (auto const &arg : arguments_) {
     arg.print(out, expand_terms, true, ind + 1U);
   }

lib/codegen/CreateTerm.cpp

@@ -938,7 +938,8 @@ std::pair<llvm::Value *, bool> create_term::create_allocation(
         std::string name = str_pattern->get_contents();
 
         proof_event p(definition_, module_);
-        current_block_ = p.hook_event_pre(name, current_block_, location_stack);
+        current_block_ = p.hook_event_pre(
+            name, constructor, current_block_, location_stack);
         llvm::Value *val = create_hook(
             symbol_decl->attributes().get(attribute_set::key::Hook).get(),
             constructor, location_stack);

lib/codegen/ProofEvent.cpp

@@ -166,8 +166,8 @@ proof_event::event_prelude(
  */
 
 llvm::BasicBlock *proof_event::hook_event_pre(
-    std::string const &name, llvm::BasicBlock *current_block,
-    std::string const &location_stack) {
+    std::string const &name, kore_composite_pattern *pattern,
+    llvm::BasicBlock *current_block, std::string const &location_stack) {
   if (!proof_hint_instrumentation) {
     return current_block;
   }
@@ -177,6 +177,8 @@ llvm::BasicBlock *proof_event::hook_event_pre(
 
   emit_write_uint64(outputFile, detail::word(0xAA), true_block);
   emit_write_string(outputFile, name, true_block);
+  emit_write_string(
+      outputFile, ast_to_string(*pattern->get_constructor()), true_block);
   emit_write_string(outputFile, location_stack, true_block);
 
   llvm::BranchInst::Create(merge_block, true_block);

lib/parser/KOREParser.cpp

@@ -343,12 +343,7 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
     consume(token::LeftBrace);
     consume(token::RightBrace);
     consume(token::LeftParen);
-    std::string symbol = consume(token::Id);
-    consume(token::LeftBrace);
-    auto pat = kore_composite_pattern::create(symbol);
-    sorts(pat->get_constructor());
-    pat->get_constructor()->init_pattern_arguments();
-    consume(token::RightBrace);
+    auto sym = symbol();
     consume(token::LeftParen);
     std::vector<sptr<kore_pattern>> pats;
     patterns(pats);
@@ -358,7 +353,7 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
       sptr<kore_pattern> accum = pats[0];
       for (auto i = 1U; i < pats.size(); i++) {
         sptr<kore_composite_pattern> new_accum
-            = kore_composite_pattern::create(pat->get_constructor());
+            = kore_composite_pattern::create(sym.get());
         new_accum->add_argument(accum);
         new_accum->add_argument(pats[i]);
         accum = new_accum;
@@ -368,7 +363,7 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
     sptr<kore_pattern> accum = pats[pats.size() - 1];
     for (int i = pats.size() - 2; i >= 0; i--) {
       sptr<kore_composite_pattern> new_accum
-          = kore_composite_pattern::create(pat->get_constructor());
+          = kore_composite_pattern::create(sym.get());
       new_accum->add_argument(pats[i]);
       new_accum->add_argument(accum);
       accum = new_accum;
@@ -402,6 +397,16 @@ sptr<kore_pattern> kore_parser::application_pattern(std::string const &name) {
   return result;
 }
 
+ptr<kore_symbol> kore_parser::symbol() {
+  std::string symbol = consume(token::Id);
+  consume(token::LeftBrace);
+  auto pat = kore_composite_pattern::create(symbol);
+  sorts(pat->get_constructor());
+  pat->get_constructor()->init_pattern_arguments();
+  consume(token::RightBrace);
+  return std::make_unique<kore_symbol>(*pat->get_constructor());
+}
+
 ptr<kore_composite_pattern>
 kore_parser::application_pattern_internal(std::string const &name) {
   consume(token::LeftBrace);

runtime/util/util.cpp

@@ -35,7 +35,7 @@ block *construct_raw_term(void *subject, char const *sort, bool raw_value) {
 }
 
 void print_proof_hint_header(FILE *file) {
-  uint32_t version = 9;
+  uint32_t version = 10;
   fmt::print(file, "HINT");
   fwrite(&version, sizeof(version), 1, file);
 }