Add total attribute to projection functions for named nonterminals wh…

…ich are total (#4118)

As part of
runtimeverification/evm-semantics#2349 we are
trying to change how we implement the gas schedule in KEVM in order to
improve performance. In order to do this, we introduce a new sort,
ScheduleTuple, which has a single constructor with many arguments. We
rely on projection functions for named nonterminals in order to extract
those arguments. However, this confuses the booster because it is unable
to determine that these functions are total. In general, they are not
total, however, for the case where the sort they are defined over has a
single constructor, they are total. Thus, we introduce logic into
GenerateSortProjections which tags these productions as total in the
cases where they are in fact total.

This has been tested and shown to fix the performance regression in the
booster introduced by the above change. It should be easy to see why
this change is sound since it applies the `total` attribute only in the
case where the production has a single constructor, and the rule matches
unconditionally on any instance of that constructor.

k-distribution/tests/regression-new/total-proj/1.test

@@ -0,0 +1 @@
+foo()

k-distribution/tests/regression-new/total-proj/1.test.out

@@ -0,0 +1,3 @@
+<k>
+  false ~> .K
+</k>

k-distribution/tests/regression-new/total-proj/Makefile

@@ -0,0 +1,6 @@
+DEF=test
+EXT=test
+TESTDIR=.
+KOMPILE_BACKEND=haskell
+
+include ../../../include/kframework/ktest.mak

k-distribution/tests/regression-new/total-proj/test.k

@@ -0,0 +1,15 @@
+module TEST
+  imports INT
+  imports BOOL
+  imports LIST
+
+  configuration <k> $PGM:Pgm </k>
+
+  syntax Pgm ::= foo() | Pgm2
+  syntax Pgm2 ::= bar(baz: Int)
+
+  rule foo() => ?X:Pgm2
+  rule X:Pgm2 => baz(X)
+  rule I:Int => false
+
+endmodule

kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java

@@ -154,9 +154,12 @@ public Function<Definition, Definition> steps() {
     DefinitionTransformer generateSortPredicateRules =
         DefinitionTransformer.from(
             new GenerateSortPredicateRules()::gen, "adding sort predicate rules");
-    DefinitionTransformer generateSortProjections =
-        DefinitionTransformer.from(
-            new GenerateSortProjections(kompileOptions.coverage)::gen, "adding sort projections");
+    Function1<Definition, Definition> generateSortProjections =
+        d ->
+            DefinitionTransformer.from(
+                    new GenerateSortProjections(kompileOptions.coverage, d.mainModule())::gen,
+                    "adding sort projections")
+                .apply(d);
     DefinitionTransformer subsortKItem =
         DefinitionTransformer.from(Kompile::subsortKItem, "subsort all sorts to KItem");
     Function1<Definition, Definition> addCoolLikeAtt =
@@ -377,8 +380,11 @@ public Function<Module, Module> specificationSteps(Definition def) {
         ModuleTransformer.fromSentenceTransformer(
             new ConcretizeCells(configInfo, labelInfo, sortInfo, mod)::concretize,
             "concretizing configuration");
-    ModuleTransformer generateSortProjections =
-        ModuleTransformer.from(new GenerateSortProjections(false)::gen, "adding sort projections");
+    Function1<Module, Module> generateSortProjections =
+        m ->
+            ModuleTransformer.from(
+                    new GenerateSortProjections(false, m)::gen, "adding sort projections")
+                .apply(m);
 
     return m ->
         resolveComm

kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java

@@ -28,13 +28,16 @@
 public class GenerateSortProjections {
 
   private Module mod;
+  private final Module mainMod;
   private final boolean cover;
 
-  public GenerateSortProjections(boolean cover) {
+  public GenerateSortProjections(boolean cover, Module mainMod) {
+    this.mainMod = mainMod;
     this.cover = cover;
   }
 
   public GenerateSortProjections(Module mod) {
+    this.mainMod = null;
     this.mod = mod;
     this.cover = false;
   }
@@ -133,13 +136,30 @@ public Stream<? extends Sentence> gen(Production prod) {
     if (!hasName) {
       return Stream.empty();
     }
+    boolean total = false;
+    if (mainMod != null) {
+      if (stream(
+                  mainMod
+                      .productionsForSort()
+                      .get(prod.sort().head())
+                      .getOrElse(() -> Collections.<Production>Set()))
+              .filter(p -> !p.att().contains(Att.FUNCTION()))
+              .count()
+          == 1) {
+        total = true;
+      }
+    }
     i = 0;
     for (NonTerminal nt : iterable(prod.nonterminals())) {
       if (nt.name().isDefined()) {
         KLabel lbl = getProjectLbl(prod.klabel().get().name(), nt.name().get());
         if (mod.definedKLabels().contains(lbl)) {
           return Stream.empty();
         }
+        Att att = Att.empty().add(Att.FUNCTION());
+        if (total) {
+          att = att.add(Att.TOTAL());
+        }
         sentences.add(
             Production(
                 lbl,
@@ -149,7 +169,7 @@ public Stream<? extends Sentence> gen(Production prod) {
                     Terminal("("),
                     NonTerminal(prod.sort()),
                     Terminal(")")),
-                Att.empty().add(Att.FUNCTION())));
+                att));
         sentences.add(
             Rule(
                 KRewrite(KApply(lbl, KApply(prod.klabel().get(), KList(vars))), vars.get(i)),