diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp index 44f4ab861..277dbacdc 100644 --- a/bindings/python/ast.cpp +++ b/bindings/python/ast.cpp @@ -218,6 +218,8 @@ void bind_ast(py::module_ &m) { std::shared_ptr 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(); }); diff --git a/include/kllvm/ast/AST.h b/include/kllvm/ast/AST.h index 492a0ad48..091721dab 100644 --- a/include/kllvm/ast/AST.h +++ b/include/kllvm/ast/AST.h @@ -1023,9 +1023,9 @@ class kore_definition { [[nodiscard]] std::list 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_; diff --git a/include/kllvm/ast/attribute_set.h b/include/kllvm/ast/attribute_set.h index 91515efca..893182b7d 100644 --- a/include/kllvm/ast/attribute_set.h +++ b/include/kllvm/ast/attribute_set.h @@ -58,6 +58,7 @@ class attribute_set { MacroRec, Nat, NonExecutable, + Ordinal, Priorities, Priority, Right, diff --git a/include/kllvm/codegen/ProofEvent.h b/include/kllvm/codegen/ProofEvent.h index 00ef243c0..d6dc8675a 100644 --- a/include/kllvm/codegen/ProofEvent.h +++ b/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 vars, llvm::StringMap 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 const &args, - llvm::BasicBlock *current_block); + kore_axiom_declaration const &axiom, + std::vector 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) diff --git a/lib/ast/attribute_set.cpp b/lib/ast/attribute_set.cpp index 658a18395..17a23e817 100644 --- a/lib/ast/attribute_set.cpp +++ b/lib/ast/attribute_set.cpp @@ -35,6 +35,7 @@ std::unordered_map 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"}, diff --git a/lib/ast/definition.cpp b/lib/ast/definition.cpp index 60ec43029..fefcdb5c3 100644 --- a/lib/ast/definition.cpp +++ b/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(); diff --git a/lib/codegen/Decision.cpp b/lib/codegen/Decision.cpp index 4c2b53dc1..b019da8dd 100644 --- a/lib/codegen/Decision.cpp +++ b/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 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{}; - 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{}; auto i = 0; diff --git a/lib/codegen/ProofEvent.cpp b/lib/codegen/ProofEvent.cpp index dd16d7b76..1013ad868 100644 --- a/lib/codegen/ProofEvent.cpp +++ b/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 vars, llvm::StringMap 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 const &args, + kore_axiom_declaration const &axiom, std::vector 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 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); diff --git a/test/python/test_proof_trace.py b/test/python/test_proof_trace.py index dfe2997b4..ce527e7e1 100644 --- a/test/python/test_proof_trace.py +++ b/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()) diff --git a/test/python/test_proof_trace_slow.py b/test/python/test_proof_trace_slow.py index ce0368682..5e9f3b74f 100644 --- a/test/python/test_proof_trace_slow.py +++ b/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())