From 7d9951104a1225cc34aa250962fa8e3dad6f009f Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 21 Mar 2024 14:27:13 -0500 Subject: [PATCH] Add total attribute to projection functions for named nonterminals which are total (#4118) As part of https://github.com/runtimeverification/evm-semantics/pull/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. --- .../tests/regression-new/total-proj/1.test | 1 + .../regression-new/total-proj/1.test.out | 3 +++ .../tests/regression-new/total-proj/Makefile | 6 +++++ .../tests/regression-new/total-proj/test.k | 15 ++++++++++++ .../kframework/backend/kore/KoreBackend.java | 16 +++++++++---- .../compile/GenerateSortProjections.java | 24 +++++++++++++++++-- 6 files changed, 58 insertions(+), 7 deletions(-) create mode 100644 k-distribution/tests/regression-new/total-proj/1.test create mode 100644 k-distribution/tests/regression-new/total-proj/1.test.out create mode 100644 k-distribution/tests/regression-new/total-proj/Makefile create mode 100644 k-distribution/tests/regression-new/total-proj/test.k diff --git a/k-distribution/tests/regression-new/total-proj/1.test b/k-distribution/tests/regression-new/total-proj/1.test new file mode 100644 index 00000000000..eb28ef4401b --- /dev/null +++ b/k-distribution/tests/regression-new/total-proj/1.test @@ -0,0 +1 @@ +foo() diff --git a/k-distribution/tests/regression-new/total-proj/1.test.out b/k-distribution/tests/regression-new/total-proj/1.test.out new file mode 100644 index 00000000000..4c3c1457eeb --- /dev/null +++ b/k-distribution/tests/regression-new/total-proj/1.test.out @@ -0,0 +1,3 @@ + + false ~> .K + diff --git a/k-distribution/tests/regression-new/total-proj/Makefile b/k-distribution/tests/regression-new/total-proj/Makefile new file mode 100644 index 00000000000..7cef438d1d0 --- /dev/null +++ b/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 diff --git a/k-distribution/tests/regression-new/total-proj/test.k b/k-distribution/tests/regression-new/total-proj/test.k new file mode 100644 index 00000000000..5fb930703dd --- /dev/null +++ b/k-distribution/tests/regression-new/total-proj/test.k @@ -0,0 +1,15 @@ +module TEST + imports INT + imports BOOL + imports LIST + + configuration $PGM:Pgm + + syntax Pgm ::= foo() | Pgm2 + syntax Pgm2 ::= bar(baz: Int) + + rule foo() => ?X:Pgm2 + rule X:Pgm2 => baz(X) + rule I:Int => false + +endmodule diff --git a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java index 68d54e21e93..671b6f06db8 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java +++ b/kernel/src/main/java/org/kframework/backend/kore/KoreBackend.java @@ -154,9 +154,12 @@ public Function 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 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 addCoolLikeAtt = @@ -377,8 +380,11 @@ public Function 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 generateSortProjections = + m -> + ModuleTransformer.from( + new GenerateSortProjections(false, m)::gen, "adding sort projections") + .apply(m); return m -> resolveComm diff --git a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java b/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java index 5bc24ff704d..f4c18ad293e 100644 --- a/kernel/src/main/java/org/kframework/compile/GenerateSortProjections.java +++ b/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,6 +136,19 @@ public Stream gen(Production prod) { if (!hasName) { return Stream.empty(); } + boolean total = false; + if (mainMod != null) { + if (stream( + mainMod + .productionsForSort() + .get(prod.sort().head()) + .getOrElse(() -> Collections.Set())) + .filter(p -> !p.att().contains(Att.FUNCTION())) + .count() + == 1) { + total = true; + } + } i = 0; for (NonTerminal nt : iterable(prod.nonterminals())) { if (nt.name().isDefined()) { @@ -140,6 +156,10 @@ public Stream gen(Production prod) { 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 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)),