Introducing Ordinal KORE Attribute (#1053)

Closes Pi-Squared-Inc/pi2#1432
This PR introduces a new attribute specific to the LLVM Backend. It
includes the `ordinal` attribute to the KORE definition when
`preprocess` is called after parsing a definition. The content of the
attribute is a `string_sort` with the value of the computed
`axiom_ordinal`.

A new C++ tool is planned to consume this feature instead of reading a
definition with a bash script.
The main intention of this feature is to expose this information to the
Python bindings to be used in Proof Hints integration tests.

bindings/python/ast.cpp

@@ -218,6 +218,8 @@ void bind_ast(py::module_ &m) {
              std::shared_ptr<kore_composite_pattern> const &arg) {
             decl.attributes().add(arg);
           })
+      .def("preprocess", &kore_definition::preprocess)
+      .def("get_axiom_by_ordinal", &kore_definition::get_axiom_by_ordinal)
       .def_property_readonly("attributes", [](kore_definition &decl) {
         return decl.attributes().underlying();
       });

include/kllvm/ast/AST.h

@@ -1023,9 +1023,9 @@ class kore_definition {
   [[nodiscard]] std::list<kore_axiom_declaration *> const &get_axioms() const {
     return axioms_;
   }
-  [[nodiscard]] kore_axiom_declaration *
+  [[nodiscard]] kore_axiom_declaration const &
   get_axiom_by_ordinal(size_t ordinal) const {
-    return ordinals_.at(ordinal);
+    return *ordinals_.at(ordinal);
   }
   [[nodiscard]] kore_symbolStringMapType const &get_fresh_functions() const {
     return fresh_functions_;

include/kllvm/ast/attribute_set.h

@@ -58,6 +58,7 @@ class attribute_set {
     MacroRec,
     Nat,
     NonExecutable,
+    Ordinal,
     Priorities,
     Priority,
     Right,

include/kllvm/codegen/ProofEvent.h

@@ -104,7 +104,7 @@ class proof_event {
       llvm::BasicBlock *current_block);
 
   [[nodiscard]] llvm::BasicBlock *rewrite_event_pre(
-      kore_axiom_declaration *axiom, uint64_t arity,
+      kore_axiom_declaration const &axiom, uint64_t arity,
       std::map<std::string, kore_variable_pattern *> vars,
       llvm::StringMap<llvm::Value *> const &subst,
       llvm::BasicBlock *current_block);
@@ -121,11 +121,11 @@ class proof_event {
   function_event_post(llvm::BasicBlock *current_block);
 
   [[nodiscard]] llvm::BasicBlock *side_condition_event_pre(
-      kore_axiom_declaration *axiom, std::vector<llvm::Value *> const &args,
-      llvm::BasicBlock *current_block);
+      kore_axiom_declaration const &axiom,
+      std::vector<llvm::Value *> const &args, llvm::BasicBlock *current_block);
 
   [[nodiscard]] llvm::BasicBlock *side_condition_event_post(
-      kore_axiom_declaration *axiom, llvm::Value *check_result,
+      kore_axiom_declaration const &axiom, llvm::Value *check_result,
       llvm::BasicBlock *current_block);
 
   proof_event(kore_definition *definition, llvm::Module *module)

lib/ast/attribute_set.cpp

@@ -35,6 +35,7 @@ std::unordered_map<attribute_set::key, std::string> const &attribute_table() {
       {attribute_set::key::MacroRec, "macro-rec"},
       {attribute_set::key::Nat, "nat"},
       {attribute_set::key::NonExecutable, "non-executable"},
+      {attribute_set::key::Ordinal, "ordinal"},
       {attribute_set::key::Priorities, "priorities"},
       {attribute_set::key::Priority, "priority"},
       {attribute_set::key::Right, "right"},

lib/ast/definition.cpp

@@ -190,6 +190,11 @@ void kore_definition::preprocess() {
     } else {
       ++iter;
     }
+    auto ordinal_att = kore_composite_pattern::create("ordinal");
+    auto pattern
+        = kore_string_pattern::create(std::to_string(axiom->get_ordinal()));
+    ordinal_att->add_argument(std::move(pattern));
+    axiom->attributes().add(std::move(ordinal_att));
   }
   for (auto &module : modules_) {
     auto const &declarations = module->get_declarations();

lib/codegen/Decision.cpp

@@ -431,8 +431,7 @@ void function_node::codegen(decision *d) {
   if (is_side_condition) {
     proof_event p(d->definition_, d->module_);
     size_t ordinal = std::stoll(function_.substr(15));
-    kore_axiom_declaration *axiom
-        = d->definition_->get_axiom_by_ordinal(ordinal);
+    auto axiom = d->definition_->get_axiom_by_ordinal(ordinal);
     d->current_block_
         = p.side_condition_event_pre(axiom, args, d->current_block_);
   }
@@ -447,8 +446,7 @@ void function_node::codegen(decision *d) {
   if (is_side_condition) {
     proof_event p(d->definition_, d->module_);
     size_t ordinal = std::stoll(function_.substr(15));
-    kore_axiom_declaration *axiom
-        = d->definition_->get_axiom_by_ordinal(ordinal);
+    auto axiom = d->definition_->get_axiom_by_ordinal(ordinal);
     d->current_block_
         = p.side_condition_event_post(axiom, call, d->current_block_);
   }
@@ -461,11 +459,10 @@ void function_node::codegen(decision *d) {
                    + function_.substr(function_.find_first_of('_', 5) + 1);
     } else if (is_side_condition) {
       size_t ordinal = std::stoll(function_.substr(15));
-      kore_axiom_declaration *axiom
-          = d->definition_->get_axiom_by_ordinal(ordinal);
-      if (axiom->attributes().contains(attribute_set::key::Label)) {
+      auto axiom = d->definition_->get_axiom_by_ordinal(ordinal);
+      if (axiom.attributes().contains(attribute_set::key::Label)) {
         debug_name
-            = axiom->attributes().get_string(attribute_set::key::Label) + ".sc";
+            = axiom.attributes().get_string(attribute_set::key::Label) + ".sc";
       }
     }
     std::vector<llvm::Value *> function_args;
@@ -595,13 +592,13 @@ void leaf_node::codegen(decision *d) {
   // retrieve the corresponding ordinal we drop the apply_rule_ prefix.
   auto ordinal = std::stoll(name_.substr(11));
   auto arity = apply_rule->arg_end() - apply_rule->arg_begin();
-  auto *axiom = d->definition_->get_axiom_by_ordinal(ordinal);
+  auto axiom = d->definition_->get_axiom_by_ordinal(ordinal);
 
   auto vars = std::map<std::string, kore_variable_pattern *>{};
-  for (kore_pattern *lhs : axiom->get_left_hand_side()) {
+  for (kore_pattern *lhs : axiom.get_left_hand_side()) {
     lhs->mark_variables(vars);
   }
-  axiom->get_right_hand_side()->mark_variables(vars);
+  axiom.get_right_hand_side()->mark_variables(vars);
 
   auto subst = llvm::StringMap<llvm::Value *>{};
   auto i = 0;

lib/codegen/ProofEvent.cpp

@@ -230,7 +230,7 @@ llvm::BasicBlock *proof_event::argument(
  */
 
 llvm::BasicBlock *proof_event::rewrite_event_pre(
-    kore_axiom_declaration *axiom, uint64_t arity,
+    kore_axiom_declaration const &axiom, uint64_t arity,
     std::map<std::string, kore_variable_pattern *> vars,
     llvm::StringMap<llvm::Value *> const &subst,
     llvm::BasicBlock *current_block) {
@@ -242,7 +242,7 @@ llvm::BasicBlock *proof_event::rewrite_event_pre(
       = event_prelude("rewrite_pre", current_block);
 
   emit_write_uint64(outputFile, detail::word(0x22), true_block);
-  emit_write_uint64(outputFile, axiom->get_ordinal(), true_block);
+  emit_write_uint64(outputFile, axiom.get_ordinal(), true_block);
   emit_write_uint64(outputFile, arity, true_block);
   for (auto entry = subst.begin(); entry != subst.end(); ++entry) {
     auto key = entry->getKey();
@@ -321,7 +321,7 @@ proof_event::function_event_post(llvm::BasicBlock *current_block) {
 }
 
 llvm::BasicBlock *proof_event::side_condition_event_pre(
-    kore_axiom_declaration *axiom, std::vector<llvm::Value *> const &args,
+    kore_axiom_declaration const &axiom, std::vector<llvm::Value *> const &args,
     llvm::BasicBlock *current_block) {
   if (!proof_hint_instrumentation) {
     return current_block;
@@ -330,14 +330,14 @@ llvm::BasicBlock *proof_event::side_condition_event_pre(
   auto [true_block, merge_block, outputFile]
       = event_prelude("side_condition_pre", current_block);
 
-  size_t ordinal = axiom->get_ordinal();
+  size_t ordinal = axiom.get_ordinal();
   size_t arity = args.size();
 
   emit_write_uint64(outputFile, detail::word(0xEE), true_block);
   emit_write_uint64(outputFile, ordinal, true_block);
   emit_write_uint64(outputFile, arity, true_block);
 
-  kore_pattern *pattern = axiom->get_requires();
+  kore_pattern *pattern = axiom.get_requires();
   std::map<std::string, kore_variable_pattern *> vars;
   pattern->mark_variables(vars);
 
@@ -360,7 +360,7 @@ llvm::BasicBlock *proof_event::side_condition_event_pre(
 }
 
 llvm::BasicBlock *proof_event::side_condition_event_post(
-    kore_axiom_declaration *axiom, llvm::Value *check_result,
+    kore_axiom_declaration const &axiom, llvm::Value *check_result,
     llvm::BasicBlock *current_block) {
   if (!proof_hint_instrumentation) {
     return current_block;
@@ -369,7 +369,7 @@ llvm::BasicBlock *proof_event::side_condition_event_post(
   auto [true_block, merge_block, outputFile]
       = event_prelude("side_condition_post", current_block);
 
-  size_t ordinal = axiom->get_ordinal();
+  size_t ordinal = axiom.get_ordinal();
 
   emit_write_uint64(outputFile, detail::word(0x33), true_block);
   emit_write_uint64(outputFile, ordinal, true_block);

test/python/test_proof_trace.py

@@ -15,6 +15,10 @@
 
 
 class TestParser(unittest.TestCase):
+    def get_pattern_from_ordinal(self, definition_text, ordinal):
+        axiom_ordinal = 'ordinal{}("' + str(ordinal) + '")'
+        line = next((i+1 for i, l in enumerate(definition_text) if axiom_ordinal in l), None)
+        return definition_text[line-1].strip()
 
     def test_file(self):
         binary_proof_trace = os.path.join(
@@ -24,6 +28,18 @@ def test_file(self):
             os.path.dirname(os.path.realpath(__file__)),
             "Output", "test_proof_trace.py.tmp", "header.bin")
         header = kllvm.prooftrace.kore_header(binary_header_path)
+
+        definition_file = os.path.join(
+            os.path.dirname(os.path.realpath(__file__)),
+            "Inputs", "proof-trace.kore")
+
+        with open(definition_file, 'rb') as f:
+            data = f.read()
+            definition = kllvm.parser.Parser.from_string(data).definition()
+
+            definition.preprocess()
+            definition_text = repr(definition).split("\n")
+
         with open(binary_proof_trace, 'rb') as f:
            data = f.read()
            trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data, header)
@@ -37,11 +53,17 @@ def test_file(self):
 
            # check that the first event is the rewrite a() => b()
            self.assertTrue(trace.trace[0].is_step_event())
-           self.assertEqual(trace.trace[0].step_event.rule_ordinal, 95)
+           rule_ordinal = trace.trace[0].step_event.rule_ordinal
+           axiom = repr(definition.get_axiom_by_ordinal(rule_ordinal))
+           axiom_expected = self.get_pattern_from_ordinal(definition_text, rule_ordinal)
+           self.assertEqual(axiom, axiom_expected)
 
            # check that the second event is the rewrite b() => c()
            self.assertTrue(trace.trace[1].is_step_event())
-           self.assertEqual(trace.trace[1].step_event.rule_ordinal, 96)
+           rule_ordinal = trace.trace[1].step_event.rule_ordinal
+           axiom = repr(definition.get_axiom_by_ordinal(rule_ordinal))
+           axiom_expected = self.get_pattern_from_ordinal(definition_text, rule_ordinal)
+           self.assertEqual(axiom, axiom_expected)
 
            # check that the third event is a configuration
            self.assertTrue(trace.trace[2].is_kore_pattern())

test/python/test_proof_trace_slow.py

@@ -15,6 +15,10 @@
 
 
 class TestParser(unittest.TestCase):
+    def get_pattern_from_ordinal(self, definition_text, ordinal):
+        axiom_ordinal = 'ordinal{}("' + str(ordinal) + '")'
+        line = next((i+1 for i, l in enumerate(definition_text) if axiom_ordinal in l), None)
+        return definition_text[line-1].strip()
 
     def test_file(self):
         binary_proof_trace = os.path.join(
@@ -24,6 +28,18 @@ def test_file(self):
             os.path.dirname(os.path.realpath(__file__)),
             "Output", "test_proof_trace_slow.py.tmp", "header.bin")
         header = kllvm.prooftrace.kore_header(binary_header_path)
+
+        definition_file = os.path.join(
+            os.path.dirname(os.path.realpath(__file__)),
+            "Inputs", "proof-trace.kore")
+
+        with open(definition_file, 'rb') as f:
+            data = f.read()
+            definition = kllvm.parser.Parser.from_string(data).definition()
+
+            definition.preprocess()
+            definition_text = repr(definition).split("\n")
+
         with open(binary_proof_trace, 'rb') as f:
            data = f.read()
            trace = kllvm.prooftrace.llvm_rewrite_trace.parse(data, header)
@@ -37,14 +53,20 @@ def test_file(self):
 
            # check that the first event is the rewrite a() => b()
            self.assertTrue(trace.trace[0].is_step_event())
-           self.assertEqual(trace.trace[0].step_event.rule_ordinal, 95)
+           rule_ordinal = trace.trace[0].step_event.rule_ordinal
+           axiom = repr(definition.get_axiom_by_ordinal(rule_ordinal))
+           axiom_expected = self.get_pattern_from_ordinal(definition_text, rule_ordinal)
+           self.assertEqual(axiom, axiom_expected)
 
            # check that the second event is a configuration
            self.assertTrue(trace.trace[1].is_kore_pattern())
 
            # check that the third event is the rewrite b() => c()
            self.assertTrue(trace.trace[2].is_step_event())
-           self.assertEqual(trace.trace[2].step_event.rule_ordinal, 96)
+           rule_ordinal = trace.trace[2].step_event.rule_ordinal
+           axiom = repr(definition.get_axiom_by_ordinal(rule_ordinal))
+           axiom_expected = self.get_pattern_from_ordinal(definition_text, rule_ordinal)
+           self.assertEqual(axiom, axiom_expected)
 
            # check that the fourth event is a configuration
            self.assertTrue(trace.trace[3].is_kore_pattern())