Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

include/kllvm/ast/AST.h

@@ -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:
@@ -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 &,
@@ -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;
@@ -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,

lib/ast/AST.cpp

@@ -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,

lib/binary/ProofTraceParser.cpp

@@ -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);
@@ -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_);
@@ -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(