From 7d9951104a1225cc34aa250962fa8e3dad6f009f Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Thu, 21 Mar 2024 14:27:13 -0500 Subject: [PATCH 1/3] 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)), From e3b3186076c7c6f3898863765736fc5423735e9b Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 21 Mar 2024 16:02:35 -0600 Subject: [PATCH 2/3] Update dependency: deps/hs-backend-booster_release (#4120) Co-authored-by: devops --- deps/hs-backend-booster_release | 2 +- flake.lock | 8 ++++---- flake.nix | 2 +- hs-backend-booster/src/main/native/hs-backend-booster | 2 +- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/deps/hs-backend-booster_release b/deps/hs-backend-booster_release index 51ba591510f..104a7967257 100644 --- a/deps/hs-backend-booster_release +++ b/deps/hs-backend-booster_release @@ -1 +1 @@ -36d54e028bd6c5720063ae562758bd7e4848f00d +88ffab54a7266d8c98d5c039ef81143d1d24f3f0 diff --git a/flake.lock b/flake.lock index 5cb0e81c1f0..67c97184865 100644 --- a/flake.lock +++ b/flake.lock @@ -15,17 +15,17 @@ ] }, "locked": { - "lastModified": 1711011750, - "narHash": "sha256-evp8VMrmxZmHiUpq8Cp9sbLuPDwY31eg8MVxxj2AAqo=", + "lastModified": 1711014116, + "narHash": "sha256-/8pHNuBxU1WOcRGRhsGb2gParbcGpP/JdCszS+8u/SU=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "36d54e028bd6c5720063ae562758bd7e4848f00d", + "rev": "88ffab54a7266d8c98d5c039ef81143d1d24f3f0", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "36d54e028bd6c5720063ae562758bd7e4848f00d", + "rev": "88ffab54a7266d8c98d5c039ef81143d1d24f3f0", "type": "github" } }, diff --git a/flake.nix b/flake.nix index 128ee67f4ef..18af207aafd 100644 --- a/flake.nix +++ b/flake.nix @@ -3,7 +3,7 @@ inputs = { haskell-backend.url = "github:runtimeverification/haskell-backend/093af3153a5e07626d9b2e628d7ad4fc77c5a723"; booster-backend = { - url = "github:runtimeverification/hs-backend-booster/36d54e028bd6c5720063ae562758bd7e4848f00d"; + url = "github:runtimeverification/hs-backend-booster/88ffab54a7266d8c98d5c039ef81143d1d24f3f0"; inputs.nixpkgs.follows = "haskell-backend/nixpkgs"; inputs.haskell-backend.follows = "haskell-backend"; inputs.stacklock2nix.follows = "haskell-backend/stacklock2nix"; diff --git a/hs-backend-booster/src/main/native/hs-backend-booster b/hs-backend-booster/src/main/native/hs-backend-booster index 36d54e028bd..88ffab54a72 160000 --- a/hs-backend-booster/src/main/native/hs-backend-booster +++ b/hs-backend-booster/src/main/native/hs-backend-booster @@ -1 +1 @@ -Subproject commit 36d54e028bd6c5720063ae562758bd7e4848f00d +Subproject commit 88ffab54a7266d8c98d5c039ef81143d1d24f3f0 From 9b12fe818b421a74278e7c1c9a116229c79901c8 Mon Sep 17 00:00:00 2001 From: gtrepta <50716988+gtrepta@users.noreply.github.com> Date: Thu, 21 Mar 2024 19:06:56 -0500 Subject: [PATCH 3/3] Add a comment to MinimizeTermConstruction describing what it does (#4124) Fixes #4113 This just adds a small comment to describe what `MinimizeTermConstruction` does as otherwise there's nothing that explains what it's doing. Co-authored-by: rv-jenkins --- .../org/kframework/compile/MinimizeTermConstruction.java | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java b/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java index 8a94e94b415..512e92442f4 100644 --- a/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java +++ b/kernel/src/main/java/org/kframework/compile/MinimizeTermConstruction.java @@ -17,6 +17,14 @@ import org.kframework.definition.Sentence; import org.kframework.kore.*; +/** + * MinimizeTermConstruction. + * + *

Looks for places where #as patterns can be used to reduce the number of constructors in + * rewrites: + * + *

`P1 => P2[P1]` -> `P1 #as X => P2[X]` + */ public class MinimizeTermConstruction { private final Set vars = new HashSet<>();