From c17a0ee903adcf09aa32eadc4c146533abbcccc2 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 11 Sep 2024 14:22:32 -0500 Subject: [PATCH] Impure attribute in KORE (#4637) We add back code that was previously removed that was designed to compute which functions in K are impure (i.e., have side effects). We don't do anything special for these functions except emit an attribute, but the llvm backend needs this information because it needs to know these functions cannot be optimized out. --------- Co-authored-by: rv-jenkins --- .../kframework/backend/kore/ModuleToKORE.java | 57 +++++++++++++++---- ...ComputeTransitiveFunctionDependencies.java | 10 ++-- .../scala/org/kframework/attributes/Att.scala | 2 +- 3 files changed, 52 insertions(+), 17 deletions(-) diff --git a/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index 670f960b28a..2ed1e40787d 100644 --- a/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/k-frontend/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -32,6 +32,7 @@ import org.kframework.builtin.KLabels; import org.kframework.builtin.Sorts; import org.kframework.compile.AddSortInjections; +import org.kframework.compile.ComputeTransitiveFunctionDependencies; import org.kframework.compile.ExpandMacros; import org.kframework.compile.RefreshRules; import org.kframework.compile.RewriteToTop; @@ -107,6 +108,7 @@ public enum SentenceType { public static final String ONE_PATH_OP = KLabels.RL_wEF.name(); public static final String ALL_PATH_OP = KLabels.RL_wAF.name(); private final Module module; + private final Set impureFunctions = new HashSet<>(); private final AddSortInjections addSortInjections; private final KLabel topCellInitializer; private final Set mlBinders = new HashSet<>(); @@ -232,6 +234,14 @@ public void convert( } } } + ComputeTransitiveFunctionDependencies deps = new ComputeTransitiveFunctionDependencies(module); + Set impurities = + stream(module.sortedProductions()) + .filter(prod -> prod.klabel().isDefined() && prod.att().contains(Att.IMPURE())) + .filter(prod -> prod.att().contains(Att.IMPURE())) + .map(prod -> prod.klabel().get()) + .collect(Collectors.toSet()); + impurities.addAll(deps.ancestors(impurities)); semantics.append("\n// symbols\n"); Set overloads = new HashSet<>(); @@ -240,8 +250,8 @@ public void convert( } syntax.append(semantics); - translateSymbols(attributes, functionRules, overloads, semantics, false); - translateSymbols(attributes, functionRules, overloads, syntax, true); + translateSymbols(attributes, functionRules, impurities, overloads, semantics, false); + translateSymbols(attributes, functionRules, impurities, overloads, syntax, true); // print syntax definition for (Tuple2> sort : @@ -250,6 +260,7 @@ public void convert( translateSymbol( attributes, functionRules, + impurities, overloads, prod.att().get(Att.BRACKET_LABEL(), KLabel.class), prod, @@ -303,8 +314,8 @@ public void convert( if (isFunctional(prod)) { genFunctionalAxiom(prod, semantics); } - if (isConstructor(prod, functionRules)) { - genNoConfusionAxioms(prod, noConfusion, functionRules, semantics); + if (isConstructor(prod, functionRules, impurities)) { + genNoConfusionAxioms(prod, noConfusion, functionRules, impurities, semantics); } } @@ -439,6 +450,7 @@ private void translateSorts( private void translateSymbols( Map attributes, SetMultimap functionRules, + Set impurities, Set overloads, StringBuilder sb, boolean withSyntaxAtts) { @@ -449,14 +461,25 @@ private void translateSymbols( if (prod.klabel().isEmpty()) { continue; } + if (impurities.contains(prod.klabel().get())) { + impureFunctions.add(prod.klabel().get().name()); + } translateSymbol( - attributes, functionRules, overloads, prod.klabel().get(), prod, sb, withSyntaxAtts); + attributes, + functionRules, + impurities, + overloads, + prod.klabel().get(), + prod, + sb, + withSyntaxAtts); } } private void translateSymbol( Map attributes, SetMultimap functionRules, + Set impurities, Set overloads, KLabel label, Production prod, @@ -480,7 +503,7 @@ private void translateSymbol( sb.append(") : "); convert(prod.sort(), prod, sb); sb.append(" "); - Att koreAtt = koreAttributes(prod, functionRules, overloads, withSyntaxAtts); + Att koreAtt = koreAttributes(prod, functionRules, impurities, overloads, withSyntaxAtts); convert(attributes, koreAtt, sb, null, null); sb.append("\n"); } @@ -714,6 +737,7 @@ private void genNoConfusionAxioms( Production prod, Set> noConfusion, SetMultimap functionRulesMap, + Set impurities, StringBuilder sb) { // c(x1,x2,...) /\ c(y1,y2,...) -> c(x1/\y2,x2/\y2,...) if (prod.arity() > 0) { @@ -753,7 +777,7 @@ private void genNoConfusionAxioms( if (prod2.klabel().isEmpty() || noConfusion.contains(Tuple2.apply(prod, prod2)) || prod.equals(prod2) - || !isConstructor(prod2, functionRulesMap) + || !isConstructor(prod2, functionRulesMap, impurities) || isBuiltinProduction(prod2)) { // TODO (traiansf): add no confusion axioms for constructor vs inj. continue; @@ -1615,8 +1639,9 @@ private void convertParams(Option maybeKLabel, boolean hasR, StringBuild sb.append("}"); } - private boolean isConstructor(Production prod, SetMultimap functionRules) { - Att att = semanticAttributes(prod, functionRules, java.util.Collections.emptySet()); + private boolean isConstructor( + Production prod, SetMultimap functionRules, Set impurities) { + Att att = semanticAttributes(prod, functionRules, impurities, java.util.Collections.emptySet()); return att.contains(Att.CONSTRUCTOR()); } @@ -1652,6 +1677,7 @@ private boolean isGeneratedInKeysOp(Production prod) { private Att koreAttributes( Production prod, SetMultimap functionRules, + Set impurities, Set overloads, boolean withSyntaxAtts) { Att att = prod.att(); @@ -1669,7 +1695,7 @@ private Att koreAttributes( for (Att.Key key : attsToRemove) { att = att.remove(key); } - att = att.addAll(semanticAttributes(prod, functionRules, overloads)); + att = att.addAll(semanticAttributes(prod, functionRules, impurities, overloads)); if (withSyntaxAtts) { att = att.addAll(syntaxAttributes(prod)); } @@ -1677,7 +1703,10 @@ private Att koreAttributes( } private Att semanticAttributes( - Production prod, SetMultimap functionRules, Set overloads) { + Production prod, + SetMultimap functionRules, + Set impurities, + Set overloads) { boolean isConstructor = !isFunction(prod); isConstructor &= !prod.att().contains(Att.ASSOC()); isConstructor &= !prod.att().contains(Att.COMM()); @@ -1692,16 +1721,20 @@ private Att semanticAttributes( boolean isMacro = prod.isMacro(); boolean isAnywhere = overloads.contains(prod); + Att att = Att.empty(); + if (prod.klabel().isDefined()) { for (Rule r : functionRules.get(prod.klabel().get())) { isAnywhere |= r.att().contains(Att.ANYWHERE()); } + if (impurities.contains(prod.klabel().get())) { + att = att.add(Att.IMPURE()); + } } isConstructor &= !isMacro; isConstructor &= !isAnywhere; - Att att = Att.empty(); if (isHook(prod)) { att = att.add(Att.HOOK(), prod.att().get(att.HOOK())); } diff --git a/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java b/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java index fe77e3010db..4d758313e59 100644 --- a/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java +++ b/k-frontend/src/main/java/org/kframework/compile/ComputeTransitiveFunctionDependencies.java @@ -88,10 +88,12 @@ private static Set ancestors( while (!queue.isEmpty()) { V v = queue.poll(); Collection neighbors = graph.getPredecessors(v); - for (V n : neighbors) { - if (!visited.contains(n)) { - queue.offer(n); - visited.add(n); + if (neighbors != null) { + for (V n : neighbors) { + if (!visited.contains(n)) { + queue.offer(n); + visited.add(n); + } } } } diff --git a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala index e81750f1694..040ebcc6265 100644 --- a/k-frontend/src/main/scala/org/kframework/attributes/Att.scala +++ b/k-frontend/src/main/scala/org/kframework/attributes/Att.scala @@ -289,7 +289,7 @@ object Att { final val IDEM = Key.builtin("idem", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) final val IMPURE = - Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production], KeyRange.FrontendOnly) + Key.builtin("impure", KeyParameter.Forbidden, onlyon[Production], KeyRange.WholePipeline) final val INDEX = Key.builtin("index", KeyParameter.Required, onlyon[Production], KeyRange.FrontendOnly) final val INITIAL =