Merge remote-tracking branch 'origin/develop'

runtimeverification · Nov 27, 2023 · 25da68c · 25da68c
2 parents f47c26a + c6c0a6f
commit 25da68c
Show file tree

Hide file tree

Showing 9 changed files with 80 additions and 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
@@ -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
@@ -6,7 +6,7 @@ module A4-SPEC
   import TEST
   imports ML-SYNTAX
 
-  claim c => 2 #And {3 #Equals n}
+  claim <k> c => 2 #And {3 #Equals n} </k>
   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
@@ -6,7 +6,7 @@ module A5-SPEC
   import TEST
   imports ML-SYNTAX
 
-  claim c => 2 #And n +Int n
+  claim <k> c => 2 #And n +Int n </k>
   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
@@ -117,15 +117,22 @@ public enum SentenceType {
   private final Set<String> 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,38 +1358,38 @@ 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("), ");
       }
 
       // 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
@@ -66,7 +66,7 @@ private boolean skipSentence(Sentence s) {
   // cell mentioned is the automatically-added <generatedCounter> cell.
   private boolean shouldConsider(List<K> 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
@@ -21,6 +21,21 @@ public AddImplicitCounterCell() {}
 
   public Sentence apply(Module m, Sentence s) {
     if (s instanceof Claim claim) {
+      Set<KVariable> 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 <generatedCounter> 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
@@ -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 <k>} 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
@@ -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
@@ -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;
 }