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 <[email protected]>
runtimeverification · Sep 11, 2024 · c17a0ee · c17a0ee
1 parent b74cee0
commit c17a0ee
Show file tree

Hide file tree

Showing 3 changed files with 52 additions and 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
@@ -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<String> impureFunctions = new HashSet<>();
   private final AddSortInjections addSortInjections;
   private final KLabel topCellInitializer;
   private final Set<String> mlBinders = new HashSet<>();
@@ -232,6 +234,14 @@ public void convert(
         }
       }
     }
+    ComputeTransitiveFunctionDependencies deps = new ComputeTransitiveFunctionDependencies(module);
+    Set<KLabel> 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<Production> 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, scala.collection.immutable.List<Production>> 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<Att.Key, Boolean> attributes,
       SetMultimap<KLabel, Rule> functionRules,
+      Set<KLabel> impurities,
       Set<Production> 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<Att.Key, Boolean> attributes,
       SetMultimap<KLabel, Rule> functionRules,
+      Set<KLabel> impurities,
       Set<Production> 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<Tuple2<Production, Production>> noConfusion,
       SetMultimap<KLabel, Rule> functionRulesMap,
+      Set<KLabel> 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<KLabel> maybeKLabel, boolean hasR, StringBuild
     sb.append("}");
   }
 
-  private boolean isConstructor(Production prod, SetMultimap<KLabel, Rule> functionRules) {
-    Att att = semanticAttributes(prod, functionRules, java.util.Collections.emptySet());
+  private boolean isConstructor(
+      Production prod, SetMultimap<KLabel, Rule> functionRules, Set<KLabel> 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<KLabel, Rule> functionRules,
+      Set<KLabel> impurities,
       Set<Production> overloads,
       boolean withSyntaxAtts) {
     Att att = prod.att();
@@ -1669,15 +1695,18 @@ 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));
     }
     return att;
   }
 
   private Att semanticAttributes(
-      Production prod, SetMultimap<KLabel, Rule> functionRules, Set<Production> overloads) {
+      Production prod,
+      SetMultimap<KLabel, Rule> functionRules,
+      Set<KLabel> impurities,
+      Set<Production> 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
@@ -88,10 +88,12 @@ private static <V> Set<V> ancestors(
     while (!queue.isEmpty()) {
       V v = queue.poll();
       Collection<V> 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
@@ -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 =