From b6e638de1c92888f1ac8f94b223fa3eb408adbd9 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Mon, 9 Sep 2024 15:25:10 -0600 Subject: [PATCH 1/4] Minimize substitutions by default (#4635) Substitutions in actual proofs are really quite large, so this addresses two problems: - When printing multiline substitutions, we had some whitespace/newline errors. - Substitutions shouldn't be printed unless non-minimization is turned on. --- pyk/src/pyk/kcfg/show.py | 20 +++++++++----- pyk/src/tests/unit/test_kcfg.py | 48 +++++++++++---------------------- 2 files changed, 29 insertions(+), 39 deletions(-) diff --git a/pyk/src/pyk/kcfg/show.py b/pyk/src/pyk/kcfg/show.py index 83eb51b4dd..17cf07b6d2 100644 --- 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/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index cfa5207d35..de40de7e67 100644 --- a/pyk/src/tests/unit/test_kcfg.py +++ b/pyk/src/tests/unit/test_kcfg.py @@ -592,8 +592,7 @@ def test_pretty_print() -> None: '├─ 14 (split, @bar, @foo)\n' '┃\n' '┃ (branch)\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V15\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 15 )\n' '┃ │\n' @@ -606,23 +605,20 @@ def test_pretty_print() -> None: '┃ └─ 13\n' '┃ (looped back)\n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V16\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 16 )\n' '┃ │\n' '┃ └─ 16\n' '┃ (continues as previously)\n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V17\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 17 )\n' '┃ │\n' '┃ └─ 17 (vacuous, leaf)\n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V18\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 18 )\n' '┃ │\n' @@ -631,8 +627,7 @@ def test_pretty_print() -> None: '┃ │ (1 step)\n' '┃ └─ 17 (vacuous, leaf)\n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V20\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 20 )\n' '┃ │\n' @@ -647,15 +642,13 @@ def test_pretty_print() -> None: '┃ │\n' '┃ └─ 25 (leaf)\n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V23\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 23 )\n' '┃ │\n' '┃ └─ 23 (stuck, leaf)\n' '┃\n' - '┗━━┓ subst:\n' - ' ┃ V14 <- V22\n' + '┗━━┓ subst: ...\n' ' ┃ constraint:\n' ' ┃ _==K_ ( X , 22 )\n' ' │\n' @@ -665,8 +658,7 @@ def test_pretty_print() -> None: ' ├─ 19\n' ' │\n' ' ┊ constraint: true\n' - ' ┊ subst:\n' - ' ┊ V22 <- V19\n' + ' ┊ subst: ...\n' ' └─ 22\n' ' (looped back)\n' '\n' @@ -702,8 +694,7 @@ def test_pretty_print() -> None: '│ \n' '┃\n' '┃ (branch)\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V15\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 15 )\n' '┃ │\n' @@ -725,8 +716,7 @@ def test_pretty_print() -> None: '┃ \n' '┃ (looped back)\n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V16\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 16 )\n' '┃ │\n' @@ -736,8 +726,7 @@ def test_pretty_print() -> None: '┃ \n' '┃ (continues as previously)\n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V17\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 17 )\n' '┃ │\n' @@ -746,8 +735,7 @@ def test_pretty_print() -> None: '┃ V17\n' '┃ \n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V18\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 18 )\n' '┃ │\n' @@ -762,8 +750,7 @@ def test_pretty_print() -> None: '┃ V17\n' '┃ \n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V20\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 20 )\n' '┃ │\n' @@ -788,8 +775,7 @@ def test_pretty_print() -> None: '┃ \n' '┃ #And #Equals ( X , 25 )\n' '┃\n' - '┣━━┓ subst:\n' - '┃ ┃ V14 <- V23\n' + '┣━━┓ subst: ...\n' '┃ ┃ constraint:\n' '┃ ┃ _==K_ ( X , 23 )\n' '┃ │\n' @@ -798,8 +784,7 @@ def test_pretty_print() -> None: '┃ V23\n' '┃ \n' '┃\n' - '┗━━┓ subst:\n' - ' ┃ V14 <- V22\n' + '┗━━┓ subst: ...\n' ' ┃ constraint:\n' ' ┃ _==K_ ( X , 22 )\n' ' │\n' @@ -815,8 +800,7 @@ def test_pretty_print() -> None: ' │ \n' ' │\n' ' ┊ constraint: true\n' - ' ┊ subst:\n' - ' ┊ V22 <- V19\n' + ' ┊ subst: ...\n' ' └─ 22\n' ' \n' ' V22\n' From b74cee01cf4597a465c20b693ff5f1722e602930 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Wed, 11 Sep 2024 12:19:54 +0200 Subject: [PATCH 2/4] More readable and informative status bar (#4636) This PR adjusts the proof info shown in the status bar. In particular, it: - removes the `branches` info, since this number refers to all of the internal branchings of the proof, it differs from the number of leaves, and it is not clear how it is useful to the end-user; - removes the `terminal` info, since this can be computed from the other information; it could also be confusing to end-users as to why there are always two terminal nodes to begin with (final node of `setUp` and `target`); - reduces horizontal space so that there is a greater chance that full status does not overflow and more info can be seen when test name is large. --- pyk/src/pyk/proof/reachability.py | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 62f5956f91..98b96f5a33 100644 --- 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: From c17a0ee903adcf09aa32eadc4c146533abbcccc2 Mon Sep 17 00:00:00 2001 From: Dwight Guth Date: Wed, 11 Sep 2024 14:22:32 -0500 Subject: [PATCH 3/4] 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 670f960b28..2ed1e40787 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 fe77e3010d..4d758313e5 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 e81750f169..040ebcc626 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 = From b4cc05571e41cbed765d7eefd8f3dd2ab2fa33c1 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 12 Sep 2024 13:43:15 -0600 Subject: [PATCH 4/4] Update dependency: deps/llvm-backend_release (#4624) Co-authored-by: devops Co-authored-by: Theodoros Kasampalis --- deps/llvm-backend_release | 2 +- flake.lock | 26 ++-- flake.nix | 2 +- .../input.test.out | Bin 1521 -> 1197 bytes .../proof-instrumentation/input.test.out | Bin 1246 -> 1087 bytes llvm-backend/src/main/native/llvm-backend | 2 +- .../integration/kllvm/test_prooftrace.py | 122 +++++++++--------- .../integration/test_krun_proof_hints.py | 18 +-- 8 files changed, 85 insertions(+), 87 deletions(-) diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 2d6e50c6da..6667b8e5fa 100644 --- 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 index c13a7aab56..28da80a2cb 100644 --- a/flake.lock +++ b/flake.lock @@ -21,11 +21,11 @@ "systems": "systems_2" }, "locked": { - "lastModified": 1694529238, - "narHash": "sha256-zsNZZGTGnMOf9YpHKJqMSsa0dXbfmxeoJ7xHlrt+xmY=", + "lastModified": 1710146030, + "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=", "owner": "numtide", "repo": "flake-utils", - "rev": "ff7b65b44d01cf9ba6a71320833626af21126384", + "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a", "type": "github" }, "original": { @@ -112,16 +112,16 @@ "utils": "utils" }, "locked": { - "lastModified": 1724355360, - "narHash": "sha256-wy+g2rVUn2dYoZ/JSA8x0cWNWYDxnxLpAzaucjUBciQ=", + "lastModified": 1726098480, + "narHash": "sha256-BOCKGOKzJLlYHSOCd2QOERS/sE038domlBc1h6nvM5s=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "b9d2a6da360e2b14a60a22928d625f43fb71ae02", + "rev": "344d1335c0fb8d146b0fa2954b0194afbe11dae6", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.84", + "ref": "v0.1.88", "repo": "llvm-backend", "type": "github" } @@ -134,11 +134,11 @@ ] }, "locked": { - "lastModified": 1693660503, - "narHash": "sha256-B/g2V4v6gjirFmy+I5mwB2bCYc0l3j5scVfwgl6WOl8=", + "lastModified": 1703863825, + "narHash": "sha256-rXwqjtwiGKJheXB43ybM8NwWB8rO2dSRrEqes0S7F5Y=", "owner": "nix-community", "repo": "nix-github-actions", - "rev": "bd5bdbb52350e145c526108f4ef192eb8e554fa0", + "rev": "5163432afc817cf8bd1f031418d1869e4c9d5547", "type": "github" }, "original": { @@ -327,11 +327,11 @@ ] }, "locked": { - "lastModified": 1697388351, - "narHash": "sha256-63N2eBpKaziIy4R44vjpUu8Nz5fCJY7okKrkixvDQmY=", + "lastModified": 1719749022, + "narHash": "sha256-ddPKHcqaKCIFSFc/cvxS14goUhCOAwsM1PbMr0ZtHMg=", "owner": "numtide", "repo": "treefmt-nix", - "rev": "aae39f64f5ecbe89792d05eacea5cb241891292a", + "rev": "8df5ff62195d4e67e2264df0b7f5e8c9995fd0bd", "type": "github" }, "original": { diff --git a/flake.nix b/flake.nix index 4b00526f6a..d3773a100d 100644 --- 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.76"; 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 index b65e2481acf76e1e7a176f9455b353b00e5f681f..e37a8e44649c1c7f09ee16b58057bf7dcf951483 100644 GIT binary patch delta 71 zcmV-N0J#703#|zSNJ&mq4Uq*ikz6W~xKxuY0Xma}0W^`gGm~Ef3zOOe4YNN2AOVr< d43m!oB$L`H`E|!_zN>XCkXH$6Y9xDC5Q<2nCa0G098}Nm78x`6T722bbg*sQV@sRM#>v zz|>9LW`)py%WJX?6UW96^BE_1GjmT?XO^7Y&tw3XpS*}E1z~|8lQz&2qscOt7XOTBlH(Zu-@6C08yGcj6mfVhmT3=EU&nRGT!V-#hae4fc* aas!k0XCkXH$6Y9xC?mrm2n7=@>J(t&K1n(1!6o?x>b{8u)wK)^a5dYk z)R5JL=A{&a)To0Q$SOB}@MN5PmXUk%MJCC~mP`h4D<}If$-?cN%*UiXc?y%!=2uLi Fi~w)1Jcj@P diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index b9d2a6da36..344d1335c0 160000 --- a/llvm-backend/src/main/native/llvm-backend +++ b/llvm-backend/src/main/native/llvm-backend @@ -1 +1 @@ -Subproject commit b9d2a6da360e2b14a60a22928d625f43fb71ae02 +Subproject commit 344d1335c0fb8d146b0fa2954b0194afbe11dae6 diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index 0b9982c0ea..0883ca5447 100644 --- a/pyk/src/tests/integration/kllvm/test_prooftrace.py +++ b/pyk/src/tests/integration/kllvm/test_prooftrace.py @@ -97,13 +97,13 @@ def test_proof_trace(self, hints: bytes, header: prooftrace.KoreHeader, definiti def test_streaming_parser_iter(self, header: prooftrace.KoreHeader, hints_file: Path) -> None: # read the hints file and get the iterator for the proof trace it = prooftrace.LLVMRewriteTraceIterator.from_file(hints_file, header) - assert it.version == 12 + assert it.version == 13 # Test that the __iter__ is working list_of_events = list(it) # Test length of the list - assert len(list_of_events) == 13 + assert len(list_of_events) == 14 # Test the type of the events for event in list_of_events: @@ -126,7 +126,7 @@ def test_streaming_parser_next(self, header: prooftrace.KoreHeader, hints_file: # read the hints file and get the iterator for the proof trace it = prooftrace.LLVMRewriteTraceIterator.from_file(hints_file, header) - assert it.version == 12 + assert it.version == 13 # skip pre-trace events while True: @@ -189,8 +189,8 @@ def test_parse_proof_hint_single_rewrite( pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization event - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 2 post-initial-configuration events assert len(pt.trace) == 2 @@ -259,8 +259,8 @@ def test_parse_proof_hint_reverse_no_ints( pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 9 post-initial-configuration events assert len(pt.trace) == 9 @@ -384,11 +384,11 @@ def test_parse_proof_hint_non_rec_function( pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 - # 4 post-initial-configuration events - assert len(pt.trace) == 4 + # 6 post-initial-configuration events + assert len(pt.trace) == 6 # Contents of the k cell in the initial configuration kore_pattern = llvm_to_pattern(pt.initial_config.kore_pattern) @@ -407,18 +407,23 @@ def test_parse_proof_hint_non_rec_function( assert len(rule_event.substitution) == 3 # Functional event - fun_event = pt.trace[1].step_event + inner_fun_event = pt.trace[1].step_event + assert isinstance(inner_fun_event, prooftrace.LLVMFunctionEvent) + assert inner_fun_event.relative_position == '0:0:0:0' + + # Simplification rule + inner_rule_event = pt.trace[2].step_event + assert isinstance(inner_rule_event, prooftrace.LLVMRuleEvent) + + # Functional event + fun_event = pt.trace[3].step_event assert isinstance(fun_event, prooftrace.LLVMFunctionEvent) assert fun_event.name == "Lblid'LParUndsRParUnds'NON-REC-FUNCTION-SYNTAX'Unds'Foo'Unds'Foo{}" assert fun_event.relative_position == '0:0:0' - assert len(fun_event.args) == 2 - # Check that arguments are a functional event and simplification rule - assert isinstance(fun_event.args[0].step_event, prooftrace.LLVMFunctionEvent) - assert fun_event.args[0].step_event.relative_position == '0:0:0:0' - assert isinstance(fun_event.args[1].step_event, prooftrace.LLVMRuleEvent) + assert len(fun_event.args) == 0 # Then rule - rule_event = pt.trace[2].step_event + rule_event = pt.trace[4].step_event assert isinstance(rule_event, prooftrace.LLVMRuleEvent) axiom = repr(definition.get_axiom_by_ordinal(rule_event.rule_ordinal)) axiom_expected = get_pattern_from_ordinal(definition_text, rule_event.rule_ordinal) @@ -426,8 +431,8 @@ def test_parse_proof_hint_non_rec_function( assert len(rule_event.substitution) == 1 # Then pattern - assert pt.trace[3].is_kore_pattern() - kore_pattern = llvm_to_pattern(pt.trace[3].kore_pattern) + assert pt.trace[5].is_kore_pattern() + kore_pattern = llvm_to_pattern(pt.trace[5].kore_pattern) k_cell = kore_pattern.patterns[0].dict['args'][0] assert k_cell['name'] == 'kseq' assert ( @@ -462,8 +467,8 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader, pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 3 post-initial-configuration events assert len(pt.trace) == 3 @@ -490,18 +495,12 @@ def test_parse_proof_hint_dv(self, hints: bytes, header: prooftrace.KoreHeader, assert isinstance(hook_event, prooftrace.LLVMHookEvent) assert hook_event.name == 'INT.add' assert hook_event.relative_position == '0:0:0:0' - assert len(hook_event.args) == 3 - - fun_event = hook_event.args[0].step_event - assert isinstance(fun_event, prooftrace.LLVMFunctionEvent) - assert fun_event.name == "Lbl'UndsPlus'Int'Unds'{}" - assert fun_event.relative_position == '0:0:0:0' - assert len(fun_event.args) == 0 + assert len(hook_event.args) == 2 - arg1 = hook_event.args[1] + arg1 = hook_event.args[0] assert arg1.is_kore_pattern() - arg2 = hook_event.args[2] + arg2 = hook_event.args[1] assert arg2.is_kore_pattern() # Then pattern @@ -549,8 +548,8 @@ def test_parse_concurrent_counters(self, hints: bytes, header: prooftrace.KoreHe pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 37 post-initial-configuration events assert len(pt.trace) == 37 @@ -709,8 +708,8 @@ def test_parse_proof_hint_0_decrement(self, hints: bytes, header: prooftrace.Kor pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 1 post-initial-configuration event assert len(pt.trace) == 1 @@ -738,8 +737,8 @@ def test_parse_proof_hint_1_decrement(self, hints: bytes, header: prooftrace.Kor pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 2 post-initial-configuration events assert len(pt.trace) == 2 @@ -767,8 +766,8 @@ def test_parse_proof_hint_2_decrement(self, hints: bytes, header: prooftrace.Kor pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 3 post-initial-configuration events assert len(pt.trace) == 3 @@ -806,11 +805,11 @@ def test_parse_proof_hint_peano(self, hints: bytes, header: prooftrace.KoreHeade pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 404 post-initial-configuration events - assert len(pt.trace) == 419 + assert len(pt.trace) == 776 class TestIMP5(ProofTraceTest): @@ -910,8 +909,8 @@ def test_parse_proof_hint_imp5(self, hints: bytes, header: prooftrace.KoreHeader pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 15 initialization events - assert len(pt.pre_trace) == 15 + # 16 initialization events + assert len(pt.pre_trace) == 16 # 2 post-initial-configuration events assert len(pt.trace) == 2 @@ -949,11 +948,11 @@ def test_parse_proof_hint_builtin_hook_events( pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 - # 3 post-initial-configuration events - assert len(pt.trace) == 3 + # 4 post-initial-configuration events + assert len(pt.trace) == 4 # Contents of the k cell in the initial configuration kore_pattern = llvm_to_pattern(pt.initial_config.kore_pattern) @@ -971,19 +970,22 @@ def test_parse_proof_hint_builtin_hook_events( repr(definition.get_axiom_by_ordinal(rule_ordinal)) get_pattern_from_ordinal(definition_text, rule_ordinal) - # Hook event with a nested event + # Hook event (first argument of next hook event) assert isinstance(pt.trace[1].step_event, prooftrace.LLVMHookEvent) assert pt.trace[1].step_event.name == 'BOOL.not' - assert pt.trace[1].step_event.relative_position == '0:0:0' - assert len(pt.trace[1].step_event.args) == 2 - arg1 = pt.trace[1].step_event.args[0].step_event - arg2 = pt.trace[1].step_event.args[1] - assert isinstance(arg1, prooftrace.LLVMHookEvent) - assert arg1.name == 'BOOL.not' - assert arg1.relative_position == '0:0:0:0' - assert len(arg1.args) == 1 - assert arg1.args[0].is_kore_pattern() - assert arg2.is_kore_pattern() + assert pt.trace[1].step_event.relative_position == '0:0:0:0' + assert len(pt.trace[1].step_event.args) == 1 + assert pt.trace[1].step_event.args[0].is_kore_pattern() + result = llvm_to_pattern(pt.trace[1].step_event.result) + + # Hook event + assert isinstance(pt.trace[2].step_event, prooftrace.LLVMHookEvent) + assert pt.trace[2].step_event.name == 'BOOL.not' + assert pt.trace[2].step_event.relative_position == '0:0:0' + assert len(pt.trace[2].step_event.args) == 1 + assert pt.trace[2].step_event.args[0].is_kore_pattern() + arg = llvm_to_pattern(pt.trace[2].step_event.args[0].kore_pattern) + assert arg.json == result.json # Final configuration - assert pt.trace[2].is_kore_pattern() + assert pt.trace[3].is_kore_pattern() diff --git a/pyk/src/tests/integration/test_krun_proof_hints.py b/pyk/src/tests/integration/test_krun_proof_hints.py index 239642f3d9..5650a12697 100644 --- a/pyk/src/tests/integration/test_krun_proof_hints.py +++ b/pyk/src/tests/integration/test_krun_proof_hints.py @@ -30,17 +30,14 @@ class Test0Decrement(KRunTest, ProofTraceTest): LblinitGeneratedTopCell{}(Lbl'Unds'Map'Unds'{}(Lbl'Stop'Map{}(),Lbl'UndsPipe'-'-GT-Unds'{}(inj{SortKConfigVar{}, SortKItem{}}(\\dv{SortKConfigVar{}}("$PGM")),inj{SortNat{}, SortKItem{}}(Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())))) """ - HINTS_OUTPUT = """version: 12 + HINTS_OUTPUT = """version: 13 hook: MAP.element Lbl'UndsPipe'-'-GT-Unds'{} () - function: Lbl'UndsPipe'-'-GT-Unds'{} () arg: kore[\\dv{SortKConfigVar{}}("$PGM")] arg: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()] hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())] hook: MAP.unit Lbl'Stop'Map{} () - function: Lbl'Stop'Map{} () hook result: kore[Lbl'Stop'Map{}()] hook: MAP.concat Lbl'Unds'Map'Unds'{} () - function: Lbl'Unds'Map'Unds'{} () arg: kore[Lbl'Stop'Map{}()] arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())] hook result: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())] @@ -50,12 +47,11 @@ class Test0Decrement(KRunTest, ProofTraceTest): function: LblinitKCell{} (0) rule: 100 1 VarInit = kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())] +hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0) + arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())] + arg: kore[\\dv{SortKConfigVar{}}("$PGM")] +hook result: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()] function: Lblproject'Coln'KItem{} (0:0) - hook: MAP.lookup LblMap'Coln'lookup{} (0:0:0:0) - function: LblMap'Coln'lookup{} (0:0:0:0) - arg: kore[Lbl'UndsPipe'-'-GT-Unds'{}(\\dv{SortKConfigVar{}}("$PGM"),Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}())] - arg: kore[\\dv{SortKConfigVar{}}("$PGM")] - hook result: kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()] rule: 139 1 VarK = kore[Lbl0'Unds'DECREMENT-SYNTAX'Unds'Nat{}()] function: LblinitGeneratedCounterCell{} (1) @@ -77,8 +73,8 @@ def test_parse_proof_hint_0_decrement(self, krun: KRun, header: prooftrace.KoreH pt = prooftrace.LLVMRewriteTrace.parse(hints, header) assert pt is not None - # 11 initialization events - assert len(pt.pre_trace) == 11 + # 12 initialization events + assert len(pt.pre_trace) == 12 # 1 post-initial-configuration event assert len(pt.trace) == 1