Merge remote-tracking branch 'origin/develop' into _update-deps/runti…

…meverification/haskell-backend
runtimeverification · Sep 16, 2024 · 8b049af · 8b049af
2 parents e534038 + b4cc055
commit 8b049af
Show file tree

Hide file tree

Showing 14 changed files with 158 additions and 139 deletions.
diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release
@@ -1 +1 @@
-0.1.84
+0.1.88
diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -1,7 +1,7 @@
 {
   description = "K Framework";
   inputs = {
-    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.84";
+    llvm-backend.url = "github:runtimeverification/llvm-backend/v0.1.88";
     haskell-backend = {
       url = "github:runtimeverification/haskell-backend/v0.1.81";
       inputs.rv-utils.follows = "llvm-backend/rv-utils";

diff --git a/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out
diff --git a/k-distribution/tests/regression-new/proof-instrumentation/input.test.out b/k-distribution/tests/regression-new/proof-instrumentation/input.test.out
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 =

diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend
diff --git a/pyk/src/pyk/kcfg/show.py b/pyk/src/pyk/kcfg/show.py
@@ -143,14 +143,22 @@ def _multi_line_print(
             return ret_lines
 
         def _print_csubst(
-            csubst: CSubst, subst_first: bool = False, indent: int = 4, max_width: int | None = None
+            csubst: CSubst, subst_first: bool = False, indent: int = 4, minimize: bool = False
         ) -> list[str]:
+            max_width = 78 if minimize else None
             _constraint_strs = [
                 self.kprint.pretty_print(ml_pred_to_bool(constraint, unsafe=True)) for constraint in csubst.constraints
             ]
             constraint_strs = _multi_line_print('constraint', _constraint_strs, 'true', max_width=max_width)
-            _subst_strs = [f'{k} <- {self.kprint.pretty_print(v)}' for k, v in csubst.subst.minimize().items()]
-            subst_strs = _multi_line_print('subst', _subst_strs, '.Subst', max_width=max_width)
+            if len(csubst.subst.minimize()) > 0 and minimize:
+                subst_strs = ['subst: ...']
+            else:
+                _subst_strs = [
+                    line
+                    for k, v in csubst.subst.minimize().items()
+                    for line in f'{k} <- {self.kprint.pretty_print(v)}'.split('\n')
+                ]
+                subst_strs = _multi_line_print('subst', _subst_strs, '.Subst', max_width=max_width)
             if subst_first:
                 return subst_strs + constraint_strs
             return constraint_strs + subst_strs
@@ -172,12 +180,10 @@ def _print_merged_edge(merged_edge: KCFG.MergedEdge) -> list[str]:
             return [res] if len(res) < 78 else ['(merged edge)']
 
         def _print_cover(cover: KCFG.Cover) -> Iterable[str]:
-            max_width = None if not minimize else 78
-            return _print_csubst(cover.csubst, subst_first=False, indent=4, max_width=max_width)
+            return _print_csubst(cover.csubst, subst_first=False, indent=4, minimize=minimize)
 
         def _print_split_edge(split: KCFG.Split, target_id: int) -> list[str]:
-            max_width = None if not minimize else 78
-            return _print_csubst(split.splits[target_id], subst_first=True, indent=4, max_width=max_width)
+            return _print_csubst(split.splits[target_id], subst_first=True, indent=4, minimize=minimize)
 
         def _print_subgraph(indent: str, curr_node: KCFG.Node, prior_on_trace: list[KCFG.Node]) -> None:
             processed = curr_node in processed_nodes

diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py
@@ -551,17 +551,13 @@ def one_line_summary(self) -> str:
         nodes = len(self.kcfg.nodes)
         pending = len(self.pending)
         failing = len(self.failing)
-        branches = 0
-        for branch in self.kcfg.ndbranches() + self.kcfg.splits():
-            branches += len(branch.targets)
         vacuous = len(self.kcfg.vacuous)
-        terminal = len(self.terminal)
         stuck = len(self.kcfg.stuck)
         passed = len([cover for cover in self.kcfg.covers() if cover.target.id == self.target])
         refuted = len(self.node_refutations)
         return (
             super().one_line_summary
-            + f' --- {nodes} nodes|{branches} branches|{terminal} terminal --- {pending} pending|{passed} passed|{failing} failing|{vacuous} vacuous|{refuted} refuted|{stuck} stuck'
+            + f': {nodes} nodes: {pending} pending|{passed} passed|{failing} failing|{vacuous} vacuous|{refuted} refuted|{stuck} stuck'
         )
 
     def get_refutation_id(self, node_id: int) -> str: