Don't emit branch unnecessary check for injection (#1029)

Fix Pi-Squared-Inc/pi2#1323
The llvm backend currently emits a branch each time a new injection is
created to check whether the term that is its child is itself an
injection. We skip over some circumstances where such a check would not
be necessary, but not all.
If the sort being injected has no subsort, then the child cannot be an
injection. This PR adds a condition to check if the current sort has no
subsorts. If that's the case, we also skip the branch/new blocks emit.

---------

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

Author: 3 people

include/kllvm/ast/AST.h

@@ -922,6 +922,9 @@ class kore_definition {
 
   kore_symbol *inj_symbol_{};
 
+  std::optional<SubsortMap> subsorts_;
+  std::optional<SubsortMap> supersorts_;
+
   /*
    * Insert symbols into this definition that have knowable labels, but cannot
    * be directly referenced in user code:

lib/ast/definition.cpp

@@ -105,37 +105,43 @@ void kore_definition::insert_reserved_symbols() {
 }
 
 SubsortMap kore_definition::get_subsorts() {
-  auto subsorts = SubsortMap{};
-
-  for (auto *axiom : axioms_) {
-    if (axiom->attributes().contains(attribute_set::key::Subsort)) {
-      auto const &att = axiom->attributes().get(attribute_set::key::Subsort);
-      auto const &inner_sort
-          = att->get_constructor()->get_formal_arguments()[0];
-      auto const &outer_sort
-          = att->get_constructor()->get_formal_arguments()[1];
-      subsorts[inner_sort.get()].insert(outer_sort.get());
+  if (!subsorts_) {
+    auto subsorts = SubsortMap{};
+
+    for (auto *axiom : axioms_) {
+      if (axiom->attributes().contains(attribute_set::key::Subsort)) {
+        auto const &att = axiom->attributes().get(attribute_set::key::Subsort);
+        auto const &inner_sort
+            = att->get_constructor()->get_formal_arguments()[0];
+        auto const &outer_sort
+            = att->get_constructor()->get_formal_arguments()[1];
+        subsorts[inner_sort.get()].insert(outer_sort.get());
+      }
     }
+    subsorts_ = transitive_closure(subsorts);
   }
 
-  return transitive_closure(subsorts);
+  return *subsorts_;
 }
 
 SubsortMap kore_definition::get_supersorts() {
-  auto supersorts = SubsortMap{};
-
-  for (auto *axiom : axioms_) {
-    if (axiom->attributes().contains(attribute_set::key::Subsort)) {
-      auto const &att = axiom->attributes().get(attribute_set::key::Subsort);
-      auto const &inner_sort
-          = att->get_constructor()->get_formal_arguments()[0];
-      auto const &outer_sort
-          = att->get_constructor()->get_formal_arguments()[1];
-      supersorts[outer_sort.get()].insert(inner_sort.get());
+  if (!supersorts_) {
+    auto supersorts = SubsortMap{};
+
+    for (auto *axiom : axioms_) {
+      if (axiom->attributes().contains(attribute_set::key::Subsort)) {
+        auto const &att = axiom->attributes().get(attribute_set::key::Subsort);
+        auto const &inner_sort
+            = att->get_constructor()->get_formal_arguments()[0];
+        auto const &outer_sort
+            = att->get_constructor()->get_formal_arguments()[1];
+        supersorts[outer_sort.get()].insert(inner_sort.get());
+      }
     }
+    supersorts_ = transitive_closure(supersorts);
   }
 
-  return transitive_closure(supersorts);
+  return *supersorts_;
 }
 
 SymbolMap kore_definition::get_overloads() const {
@@ -160,6 +166,8 @@ SymbolMap kore_definition::get_overloads() const {
 
 // NOLINTNEXTLINE(*-function-cognitive-complexity)
 void kore_definition::preprocess() {
+  get_subsorts();
+  get_supersorts();
   for (auto *axiom : axioms_) {
     axiom->pattern_ = axiom->pattern_->expand_aliases(this);
   }

lib/codegen/CreateTerm.cpp

@@ -952,15 +952,13 @@ std::pair<llvm::Value *, bool> create_term::create_allocation(
               fn_name, constructor, false, true, false, location_stack),
           true);
     }
-    if (auto cat
-        = dynamic_cast<kore_composite_sort *>(symbol->get_arguments()[0].get())
-              ->get_category(definition_)
-              .cat;
+    if (auto *sort
+        = dynamic_cast<kore_composite_sort *>(symbol->get_arguments()[0].get());
         symbol_decl->attributes().contains(attribute_set::key::SortInjection)
-        && (cat == sort_category::Symbol)) {
+        && (sort->get_category(definition_).cat == sort_category::Symbol)) {
       std::pair<llvm::Value *, bool> val = create_allocation(
           constructor->get_arguments()[0].get(), location_stack);
-      if (val.second) {
+      if (val.second && !definition_->get_supersorts()[sort].empty()) {
         llvm::Instruction *tag = llvm::CallInst::Create(
             get_or_insert_function(
                 module_, "get_tag", llvm::Type::getInt32Ty(ctx_),