From c6c0a6fdeb0a7af1f576cc6264184b9a986dcfee Mon Sep 17 00:00:00 2001 From: Radu Mereuta Date: Tue, 28 Nov 2023 00:42:29 +0200 Subject: [PATCH] Claim infer cell2 (#3812) Fixes: #3656 Changes: - add the `` cell only when a fresh variable is found or it has cells. - don't do configuration concretization on claims unless it has cells. - added an option to disable the check for functional claims. `--allow-func-claims`. I thought about disabling the check when `--dry-run` but I think that would be confusing. This option makes it explicit and obvious. --------- Co-authored-by: rv-jenkins --- .../backend/haskell/HaskellRewriter.java | 7 +++- .../a4-spec.k | 2 +- .../a5-spec.k | 2 +- .../kframework/backend/kore/ModuleToKORE.java | 34 ++++++++++++------- .../compile/AddImplicitComputationCell.java | 2 +- .../compile/AddImplicitCounterCell.java | 15 ++++++++ .../kframework/compile/ConcretizeCells.java | 23 +++++++++++++ .../compile/ResolveFreshConstants.java | 6 +++- .../org/kframework/kprove/KProveOptions.java | 6 ++++ 9 files changed, 80 insertions(+), 17 deletions(-) diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java index 43760f0ec54..7cbca201265 100644 --- a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java +++ b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java @@ -380,7 +380,12 @@ private RewriterResult executeKoreCommands( public RewriterResult prove(Module rules, Boolean reuseDef) { Module kompiledModule = KoreBackend.getKompiledModule(module, true); ModuleToKORE converter = - new ModuleToKORE(kompiledModule, def.topCellInitializer, kompileOptions, kem); + new ModuleToKORE( + kompiledModule, + def.topCellInitializer, + kompileOptions, + kem, + kProveOptions.allowFuncClaims); String defPath = reuseDef ? files.resolveKompiled("definition.kore").getAbsolutePath() diff --git a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k index caff438f238..a4dd3ba8c71 100644 --- a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k +++ b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a4-spec.k @@ -6,7 +6,7 @@ module A4-SPEC import TEST imports ML-SYNTAX - claim c => 2 #And {3 #Equals n} + claim c => 2 #And {3 #Equals n} rule {n #Equals 3} => #Top [simplification, comm] // the comm attribute is stripped because it has a different meaning in the backend // rule {3 #Equals n} => #Top [simplification] // should be generated by the above endmodule diff --git a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k index 9c2ce5e8591..eb594a38981 100644 --- a/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k +++ b/k-distribution/tests/regression-new/issue-2287-simpl-rules-in-kprovex/a5-spec.k @@ -6,7 +6,7 @@ module A5-SPEC import TEST imports ML-SYNTAX - claim c => 2 #And n +Int n + claim c => 2 #And n +Int n rule n +Int n => #Top [simplification, comm] // the comm attribute is stripped because it has a different meaning in the backend // even if comm, the body is identical so we don't generate anything extra diff --git a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java index 18dfb377c0b..bf649f679c6 100644 --- a/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java +++ b/kernel/src/main/java/org/kframework/backend/kore/ModuleToKORE.java @@ -117,15 +117,22 @@ public enum SentenceType { private final Set mlBinders = new HashSet<>(); private final KompileOptions options; + // for now these two variables are coupled to enable the functional claim check private final KExceptionManager kem; + private final boolean allowFuncClaims; public ModuleToKORE(Module module, KLabel topCellInitializer, KompileOptions options) { - this(module, topCellInitializer, options, null); + this(module, topCellInitializer, options, null, false); } public ModuleToKORE( - Module module, KLabel topCellInitializer, KompileOptions options, KExceptionManager kem) { + Module module, + KLabel topCellInitializer, + KompileOptions options, + KExceptionManager kem, + boolean allowFuncClaims) { this.kem = kem; + this.allowFuncClaims = allowFuncClaims; this.module = module; this.addSortInjections = new AddSortInjections(module); this.topCellInitializer = topCellInitializer; @@ -1057,6 +1064,9 @@ private RuleInfo getRuleInfo(RuleOrClaim rule, boolean heatCoolEq, String topCel productionSortStr = topCellSortStr; } owise = rule.att().contains(Att.OWISE()); + } else if (leftPattern instanceof KToken kt) { + productionSort = kt.sort(); + productionSortStr = getSortStr(productionSort); } return new RuleInfo( @@ -1107,7 +1117,7 @@ private void convertRule( assertNoExistentials(rule, existentials); if (rule instanceof Claim) { sb.append(" claim{R"); - if (kem != null) // TODO: remove once + if (!allowFuncClaims) // TODO: remove once // https://github.com/runtimeverification/haskell-backend/issues/3010 is // implemented kem.registerCompilerWarning( @@ -1348,9 +1358,9 @@ private void convertRule( } else { // LHS for claims sb.append(" claim{} "); - sb.append(String.format("\\implies{%s} (\n ", topCellSortStr)); - sb.append(String.format(" \\and{%s} (\n ", topCellSortStr)); - convertSideCondition(requires, topCellSortStr, sb); + sb.append(String.format("\\implies{%s} (\n ", ruleInfo.productionSortStr)); + sb.append(String.format(" \\and{%s} (\n ", ruleInfo.productionSortStr)); + convertSideCondition(requires, ruleInfo.productionSortStr, sb); sb.append(", "); convert(left, sb); sb.append("), "); @@ -1358,28 +1368,28 @@ private void convertRule( // generate rule RHS if (sentenceType == SentenceType.ALL_PATH) { - sb.append(String.format("%s{%s} (\n ", ALL_PATH_OP, topCellSortStr)); + sb.append(String.format("%s{%s} (\n ", ALL_PATH_OP, ruleInfo.productionSortStr)); } else if (sentenceType == SentenceType.ONE_PATH) { - sb.append(String.format("%s{%s} (\n ", ONE_PATH_OP, topCellSortStr)); + sb.append(String.format("%s{%s} (\n ", ONE_PATH_OP, ruleInfo.productionSortStr)); } if (!existentials.isEmpty()) { for (KVariable exists : existentials) { - sb.append(String.format(" \\exists{%s} (", topCellSortStr)); + sb.append(String.format(" \\exists{%s} (", ruleInfo.productionSortStr)); convert((K) exists, sb); sb.append(", "); } sb.append("\n "); } - sb.append(String.format("\\and{%s} (\n ", topCellSortStr)); + sb.append(String.format("\\and{%s} (\n ", ruleInfo.productionSortStr)); if (options.enableKoreAntileft) { - convertSideCondition(ensures, topCellSortStr, sb); + convertSideCondition(ensures, ruleInfo.productionSortStr, sb); sb.append(", "); convert(right, sb); } else { convert(right, sb); sb.append(", "); - convertSideCondition(ensures, topCellSortStr, sb); + convertSideCondition(ensures, ruleInfo.productionSortStr, sb); } sb.append(')'); diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java index a7bc3873216..475db877f8b 100644 --- a/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java +++ b/kernel/src/main/java/org/kframework/compile/AddImplicitComputationCell.java @@ -66,7 +66,7 @@ private boolean skipSentence(Sentence s) { // cell mentioned is the automatically-added cell. private boolean shouldConsider(List items, boolean isClaim) { if (items.size() == 1) { - return true; + return !isClaim; } else if (items.size() == 2 && isClaim) { K second = items.get(1); if (second instanceof KApply app) { diff --git a/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java b/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java index e644e9e305e..8862f4bb7cb 100644 --- a/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java +++ b/kernel/src/main/java/org/kframework/compile/AddImplicitCounterCell.java @@ -21,6 +21,21 @@ public AddImplicitCounterCell() {} public Sentence apply(Module m, Sentence s) { if (s instanceof Claim claim) { + Set freshVars = new HashSet<>(); + VisitK visitor = + new VisitK() { + @Override + public void apply(KVariable var) { + if (ResolveFreshConstants.isFreshVar(var)) freshVars.add(var); + } + }; + visitor.apply(claim.body()); + visitor.apply(claim.requires()); + visitor.apply(claim.ensures()); + // do not add if the claim doesn't contain cells or fresh vars + if (!ConcretizeCells.hasCells(claim.body()) && freshVars.isEmpty()) { + return s; + } return claim.newInstance( apply(claim.body(), m), claim.requires(), claim.ensures(), claim.att()); } diff --git a/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java b/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java index a38dc4027c4..279b840efff 100644 --- a/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java +++ b/kernel/src/main/java/org/kframework/compile/ConcretizeCells.java @@ -1,8 +1,12 @@ // Copyright (c) K Team. All Rights Reserved. package org.kframework.compile; +import java.util.stream.Stream; +import org.kframework.attributes.Att; import org.kframework.definition.*; import org.kframework.definition.Module; +import org.kframework.kore.K; +import org.kframework.kore.KRewrite; /** * Apply the configuration concretization process. The implicit {@code } cell is added by another @@ -60,6 +64,9 @@ public ConcretizeCells( } public Sentence concretize(Module m, Sentence s) { + if (s instanceof Claim c && !hasCells(c.body())) { + return s; + } s = addRootCell.addImplicitCells(s, m); s = addParentCells.concretize(s); s = closeCells.close(s); @@ -69,4 +76,20 @@ public Sentence concretize(Module m, Sentence s) { s = sortCells.postprocess(s); return s; } + + public static boolean hasCells(K item) { + if (IncompleteCellUtils.flattenCells(item).stream() + .anyMatch(k -> k.att().get(Production.class).att().contains(Att.CELL()))) { + return true; + } + + if (item instanceof KRewrite rew) { + return Stream.concat( + IncompleteCellUtils.flattenCells(rew.left()).stream(), + IncompleteCellUtils.flattenCells(rew.right()).stream()) + .anyMatch(ConcretizeCells::hasCells); + } + + return false; + } } diff --git a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java b/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java index 80e50245e7a..8fe9a6000f7 100644 --- a/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java +++ b/kernel/src/main/java/org/kframework/compile/ResolveFreshConstants.java @@ -102,11 +102,15 @@ private Rule resolve(Rule rule) { return withFresh; } + public static boolean isFreshVar(KVariable kvar) { + return kvar.name().startsWith("!"); + } + private void analyze(K term) { new VisitK() { @Override public void apply(KVariable k) { - if (k.name().startsWith("!")) { + if (isFreshVar(k)) { freshVars.add(k); } super.apply(k); diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java index 57921f54583..c548827d4a9 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java +++ b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java @@ -109,4 +109,10 @@ public synchronized File specFile(FileUtil files) { descriptionKey = "file", description = "If set, emit the JSON serialization of the spec module to the specified file.") public String emitJsonSpec = null; + + @Parameter( + names = "--allow-func-claims", + description = "Allow functional claims to be printed in kore format. Use with --dry-run.", + hidden = true) + public boolean allowFuncClaims = false; }