Skip to content

Commit

Permalink
Remove injections from output files of proof hint tests (#1048)
Browse files Browse the repository at this point in the history
Since the Pi2 team that consumes the proof hint is discarding the
injections, and we have a minor issue in our upcoming serialization PR
that does not quite deserialize injections correctly, I figured the
expedient thing to do would be to test whether or not the updated
serialization format provides the same output modulo the injections in
the provided terms. We implement this by simply recursively visiting
each term as it is printed by `kore-proof-trace` and stripping out the
injections prior to printing it.

This will be used to show that the deserialized output does not change
modulo the injections in a follow-up PR.

---------

Co-authored-by: rv-jenkins <[email protected]>
  • Loading branch information
Dwight Guth and rv-jenkins authored May 9, 2024
1 parent 336e4e4 commit 26902b1
Show file tree
Hide file tree
Showing 7 changed files with 67,142 additions and 67,125 deletions.
4 changes: 4 additions & 0 deletions include/kllvm/ast/AST.h
Original file line number Diff line number Diff line change
Expand Up @@ -420,6 +420,7 @@ class kore_pattern : public std::enable_shared_from_this<kore_pattern> {
SubsortMap const &subsorts, SymbolMap const &overloads,
std::vector<ptr<kore_declaration>> const &axioms, bool reverse);
virtual sptr<kore_pattern> unflatten_and_or() = 0;
virtual sptr<kore_pattern> strip_injections() = 0;

/*
* Recursively expands productions of the form:
Expand Down Expand Up @@ -506,6 +507,7 @@ class kore_variable_pattern : public kore_pattern {
}

sptr<kore_pattern> unflatten_and_or() override { return shared_from_this(); }
sptr<kore_pattern> strip_injections() override { return shared_from_this(); }

bool matches(
substitution &subst, SubsortMap const &, SymbolMap const &,
Expand Down Expand Up @@ -585,6 +587,7 @@ class kore_composite_pattern : public kore_pattern {
std::map<std::string, int> gather_var_counts() override;
sptr<kore_pattern> desugar_associative() override;
sptr<kore_pattern> unflatten_and_or() override;
sptr<kore_pattern> strip_injections() override;
sptr<kore_pattern> filter_substitution(
pretty_print_data const &data,
std::set<std::string> const &vars) override;
Expand Down Expand Up @@ -648,6 +651,7 @@ class kore_string_pattern : public kore_pattern {
}

sptr<kore_pattern> unflatten_and_or() override { return shared_from_this(); }
sptr<kore_pattern> strip_injections() override { return shared_from_this(); }

sptr<kore_pattern> filter_substitution(
pretty_print_data const &data,
Expand Down
13 changes: 13 additions & 0 deletions lib/ast/AST.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1122,6 +1122,19 @@ sptr<kore_pattern> kore_composite_pattern::unflatten_and_or() {
return result;
}

sptr<kore_pattern> kore_composite_pattern::strip_injections() {
if (constructor_->get_name() == "inj" && arguments_.size() == 1) {
return arguments_[0]->strip_injections();
}
auto result = kore_composite_pattern::create(constructor_.get());

for (auto &arg : arguments_) {
result->add_argument(arg->strip_injections());
}

return result;
}

sptr<kore_pattern> kore_composite_pattern::expand_macros(
SubsortMap const &subsorts, SymbolMap const &overloads,
std::vector<ptr<kore_declaration>> const &macros, bool reverse,
Expand Down
6 changes: 3 additions & 3 deletions lib/binary/ProofTraceParser.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -35,7 +35,7 @@ void llvm_rewrite_event::print_substitution(
for (auto const &p : substitution_) {
if (expand_terms) {
out << fmt::format("{}{} = kore[", indent, p.first);
p.second.first->print(out);
p.second.first->strip_injections()->print(out);
out << fmt::format("]\n");
} else {
out << fmt::format("{}{} = kore[{}]\n", indent, p.first, p.second.second);
Expand Down Expand Up @@ -87,7 +87,7 @@ void llvm_hook_event::print(
}
if (expand_terms) {
out << fmt::format("{}hook result: kore[", indent);
kore_pattern_->print(out);
kore_pattern_->strip_injections()->print(out);
out << fmt::format("]\n");
} else {
out << fmt::format("{}hook result: kore[{}]\n", indent, pattern_length_);
Expand All @@ -102,7 +102,7 @@ void llvm_event::print(
std::string indent(ind * indent_size, ' ');
if (expand_terms) {
out << fmt::format("{}{}: kore[", indent, is_arg ? "arg" : "config");
kore_pattern_->print(out);
kore_pattern_->strip_injections()->print(out);
out << fmt::format("]\n");
} else {
out << fmt::format(
Expand Down
9,224 changes: 4,612 additions & 4,612 deletions test/output/imp-sum-slow.proof.out.diff

Large diffs are not rendered by default.

7,454 changes: 3,727 additions & 3,727 deletions test/output/imp-sum.proof.out.diff

Large diffs are not rendered by default.

96,412 changes: 48,206 additions & 48,206 deletions test/output/imp.proof.out.diff

Large diffs are not rendered by default.

21,154 changes: 10,577 additions & 10,577 deletions test/output/kool-static.proof.out.diff

Large diffs are not rendered by default.

0 comments on commit 26902b1

Please sign in to comment.