diff --git a/deps/llvm-backend_release b/deps/llvm-backend_release index 2d6e50c6da4..6667b8e5fa5 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 e096b508833..956368c79cc 100644 --- a/flake.lock +++ b/flake.lock @@ -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" } diff --git a/flake.nix b/flake.nix index 817546b095b..e36936b699d 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.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 index b65e2481acf..e37a8e44649 100644 Binary files a/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out and b/k-distribution/tests/regression-new/proof-instrumentation-debug/input.test.out differ diff --git a/k-distribution/tests/regression-new/proof-instrumentation/input.test.out b/k-distribution/tests/regression-new/proof-instrumentation/input.test.out index 41aaac3a53d..adc5b2451f5 100644 Binary files a/k-distribution/tests/regression-new/proof-instrumentation/input.test.out and b/k-distribution/tests/regression-new/proof-instrumentation/input.test.out differ 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 = diff --git a/llvm-backend/src/main/native/llvm-backend b/llvm-backend/src/main/native/llvm-backend index b9d2a6da360..344d1335c0f 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/pyk/kcfg/show.py b/pyk/src/pyk/kcfg/show.py index 83eb51b4dd9..17cf07b6d28 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/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py index 62f5956f915..98b96f5a334 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: diff --git a/pyk/src/tests/integration/kllvm/test_prooftrace.py b/pyk/src/tests/integration/kllvm/test_prooftrace.py index 0b9982c0ea1..0883ca54471 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 239642f3d9a..5650a12697f 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 diff --git a/pyk/src/tests/unit/test_kcfg.py b/pyk/src/tests/unit/test_kcfg.py index cfa5207d353..de40de7e674 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'