diff --git a/frontend/src/main/java/org/kframework/ProofResult.java b/frontend/src/main/java/org/kframework/ProofResult.java new file mode 100644 index 0000000000..15ac2b7a5e --- /dev/null +++ b/frontend/src/main/java/org/kframework/ProofResult.java @@ -0,0 +1,28 @@ +package org.kframework; + +import org.kframework.frontend.K; + +import java.util.List; + +public class ProofResult { + private List results; + + private Status status; + + public enum Status { + PROVED, NOT_PROVED, EMPTY_SPEC + } + + public ProofResult(List results, Status status) { + this.results = results; + this.status = status; + } + + public List getResults() { + return results; + } + + public Status getStatus() { + return status; + } +} diff --git a/frontend/src/main/scala/org/kframework/definition/outer.scala b/frontend/src/main/scala/org/kframework/definition/outer.scala index 8aff24bf8f..6f527da5b6 100644 --- a/frontend/src/main/scala/org/kframework/definition/outer.scala +++ b/frontend/src/main/scala/org/kframework/definition/outer.scala @@ -255,6 +255,12 @@ case class Module(val name: String, val imports: Set[Module], unresolvedLocalSen lazy val rules: Set[Rule] = sentences collect { case r: Rule => r } + private val locationKey: String = "org.kframework.attributes.Source" + + lazy val claims: Set[Rule] = rules.filter(r => { + r.att.contains("claim") || (r.att.attMap.contains(locationKey) && r.att.attMap.get(locationKey).toString.contains("spec.k")) + }) + lazy val localRules: Set[Rule] = localSentences collect { case r: Rule => r } // Check that productions with the same klabel have identical attributes diff --git a/frontend/src/main/scala/org/kframework/rewriter/Rewriter.scala b/frontend/src/main/scala/org/kframework/rewriter/Rewriter.scala index 49e8c946a3..720d7d7e5e 100644 --- a/frontend/src/main/scala/org/kframework/rewriter/Rewriter.scala +++ b/frontend/src/main/scala/org/kframework/rewriter/Rewriter.scala @@ -3,7 +3,7 @@ package org.kframework.rewriter import java.util.Optional import org.kframework.definition.{Module, Rule} -import org.kframework.{RewriterResult, frontend} +import org.kframework.{ProofResult, RewriterResult, frontend} trait RewriterConstructor extends (Module => Rewriter) @@ -38,5 +38,6 @@ trait Rewriter { def executeAndMatch(k: frontend.K, depth: Optional[Integer], rule: Rule): Tuple2[RewriterResult, frontend.K] - def prove(rules: java.util.List[Rule]): java.util.List[frontend.K] +// def prove(rules: java.util.List[Rule]): java.util.List[frontend.K] + def prove(rules: java.util.List[Rule]): ProofResult } diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/InitializeRewriter.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/InitializeRewriter.java index 9dc5af4f9d..59f44ea5e5 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/InitializeRewriter.java +++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/InitializeRewriter.java @@ -3,6 +3,7 @@ import org.apache.commons.lang3.tuple.Pair; import org.kframework.KapiGlobal; +import org.kframework.ProofResult; import org.kframework.RewriterResult; import org.kframework.backend.java.MiniKoreUtils; import org.kframework.backend.java.compile.KOREtoBackendKIL; @@ -172,7 +173,7 @@ public Tuple2 executeAndMatch(K k, Optional depth, R } @Override - public List prove(List rules) { + public ProofResult prove(List rules) { TermContext termContext = TermContext.builder(rewritingContext).freshCounter(initCounterValue).build(); KOREtoBackendKIL converter = new KOREtoBackendKIL(module, definition, termContext.global(), false); termContext.setKOREtoBackendKILConverter(converter); @@ -212,10 +213,15 @@ public List prove(List rules) { .flatMap(List::stream) .collect(Collectors.toList()); - return proofResults.stream() - .map(ConstrainedTerm::term) - .map(t -> (KItem) t) - .collect(Collectors.toList()); + List filteredResults = proofResults.stream() + .map(ConstrainedTerm::term) + .map(t -> (KItem) t) + .collect(Collectors.toList()); + + if (filteredResults.isEmpty()) { + return new ProofResult(filteredResults, ProofResult.Status.PROVED); + } + return new ProofResult(filteredResults, ProofResult.Status.NOT_PROVED); } } diff --git a/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java b/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java index c0c969b5e5..9e5378e1a4 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java +++ b/java-backend/src/main/java/org/kframework/backend/java/symbolic/ProofExecutionMode.java @@ -1,6 +1,7 @@ // Copyright (c) 2015-2016 K Team. All Rights Reserved. package org.kframework.backend.java.symbolic; +import org.kframework.ProofResult; import org.kframework.attributes.Att; import org.kframework.backend.java.frontend.compile.ExpandMacros; import org.kframework.compile.NormalizeKSeq; @@ -29,11 +30,14 @@ import org.kframework.krun.modes.ExecutionMode; import org.kframework.main.GlobalOptions; import org.kframework.utils.Stopwatch; +import org.kframework.utils.errorsystem.KEMException; import org.kframework.utils.errorsystem.KExceptionManager; import org.kframework.utils.file.FileUtil; import scala.Function1; +import scala.collection.JavaConverters; import scala.collection.Set; +import java.util.ArrayList; import java.util.Collection; import java.util.Collections; import java.util.List; @@ -49,7 +53,7 @@ /** * Class that implements the "--prove" option. */ -public class ProofExecutionMode implements ExecutionMode> { +public class ProofExecutionMode implements ExecutionMode { private final KExceptionManager kem; private final KRunOptions options; @@ -66,7 +70,7 @@ public ProofExecutionMode(KExceptionManager kem, KRunOptions options, Stopwatch } @Override - public List execute(K k, Rewriter rewriter, CompiledDefinition compiledDefinition) { + public ProofResult execute(K k, Rewriter rewriter, CompiledDefinition compiledDefinition) { String proofFile = options.experimental.prove; Kompile kompile = new Kompile(compiledDefinition.kompileOptions, globalOptions, files, kem, sw, false); Module mod = kompile.parseModule(compiledDefinition, files.resolveWorkingDirectory(proofFile).getAbsoluteFile()); @@ -145,20 +149,25 @@ public K apply(KVariable k) { ExpandMacros macroExpander = new ExpandMacros(compiledDefinition.kompiledDefinition.mainModule(), kem, files, globalOptions, compiledDefinition.kompileOptions.transition, compiledDefinition.kompileOptions.experimental.smt); - List rules = stream(mod.localRules()) - .filter(r -> r.toString().contains("spec.k")) - .map(r -> new Rule( - cellPlaceholderSubstitutionApplication.apply(r.body()), - cellPlaceholderSubstitutionApplication.apply(r.requires()), - cellPlaceholderSubstitutionApplication.apply(r.ensures()), - r.att())) - .map(r -> (Rule) macroExpander.expand(r)) - .map(r -> transformFunction(JavaBackend::ADTKVariableToSortedVariable, r)) - .map(r -> transformFunction(Kompile::convertKSeqToKApply, r)) - .map(r -> transform(NormalizeKSeq.self(), r)) - //.map(r -> kompile.compileRule(compiledDefinition, r)) - .collect(Collectors.toList()); - return rewriter.prove(rules); + List rules = JavaConverters.seqAsJavaList(mod.claims().toSeq()); + + if(rules.isEmpty()) { + return new ProofResult(new ArrayList(), ProofResult.Status.EMPTY_SPEC); + } + else { + rules = rules.stream() + .map(r -> new Rule( + cellPlaceholderSubstitutionApplication.apply(r.body()), + cellPlaceholderSubstitutionApplication.apply(r.requires()), + cellPlaceholderSubstitutionApplication.apply(r.ensures()), + r.att())) + .map(r -> (Rule) macroExpander.expand(r)) + .map(r -> transformFunction(JavaBackend::ADTKVariableToSortedVariable, r)) + .map(r -> transformFunction(Kompile::convertKSeqToKApply, r)) + .map(r -> transform(NormalizeKSeq.self(), r)) + .collect(Collectors.toList()); + return rewriter.prove(rules); + } } public static Rule transformFunction(Function f, Rule r) { diff --git a/k-distribution/tests/config.xml b/k-distribution/tests/config.xml index 870bdb58af..54a62d4420 100644 --- a/k-distribution/tests/config.xml +++ b/k-distribution/tests/config.xml @@ -32,5 +32,8 @@ - + + + + diff --git a/k-distribution/tests/prover/prover-io/config.xml b/k-distribution/tests/prover/prover-io/config.xml new file mode 100644 index 0000000000..2ce77f97a7 --- /dev/null +++ b/k-distribution/tests/prover/prover-io/config.xml @@ -0,0 +1,25 @@ + + + + + + + + + + + + + + + + + + + + diff --git a/k-distribution/tests/prover/prover-io/iotest.k b/k-distribution/tests/prover/prover-io/iotest.k new file mode 100644 index 0000000000..fa9b0d5764 --- /dev/null +++ b/k-distribution/tests/prover/prover-io/iotest.k @@ -0,0 +1,16 @@ +require "domains.k" + +module IOTEST-SYNTAX + syntax Tok ::= "a" | "b" | "c" +endmodule + +module IOTEST + imports IOTEST-SYNTAX + + configuration $PGM:Tok + + rule a => b + + rule b => c +endmodule + diff --git a/k-distribution/tests/prover/prover-io/p1.iotest b/k-distribution/tests/prover/prover-io/p1.iotest new file mode 100644 index 0000000000..7898192261 --- /dev/null +++ b/k-distribution/tests/prover/prover-io/p1.iotest @@ -0,0 +1 @@ +a diff --git a/k-distribution/tests/prover/prover-io/p1.iotest.out b/k-distribution/tests/prover/prover-io/p1.iotest.out new file mode 100644 index 0000000000..27ba77ddaf --- /dev/null +++ b/k-distribution/tests/prover/prover-io/p1.iotest.out @@ -0,0 +1 @@ +true diff --git a/k-distribution/tests/prover/prover-io/p1_without_attribute.iotest b/k-distribution/tests/prover/prover-io/p1_without_attribute.iotest new file mode 100644 index 0000000000..7898192261 --- /dev/null +++ b/k-distribution/tests/prover/prover-io/p1_without_attribute.iotest @@ -0,0 +1 @@ +a diff --git a/k-distribution/tests/prover/prover-io/p1_without_attribute.iotest.out b/k-distribution/tests/prover/prover-io/p1_without_attribute.iotest.out new file mode 100644 index 0000000000..4d706fa291 --- /dev/null +++ b/k-distribution/tests/prover/prover-io/p1_without_attribute.iotest.out @@ -0,0 +1,2 @@ +No Rules with attribute "claim" found + diff --git a/k-distribution/tests/prover/prover-io/proof1.k b/k-distribution/tests/prover/prover-io/proof1.k new file mode 100644 index 0000000000..ca2991fb1d --- /dev/null +++ b/k-distribution/tests/prover/prover-io/proof1.k @@ -0,0 +1,4 @@ +module PROOFTEST + imports IOTEST + rule a => c [claim] +endmodule diff --git a/k-distribution/tests/prover/prover-io/proof1_without_attribute.k b/k-distribution/tests/prover/prover-io/proof1_without_attribute.k new file mode 100644 index 0000000000..24c76fdc5b --- /dev/null +++ b/k-distribution/tests/prover/prover-io/proof1_without_attribute.k @@ -0,0 +1,4 @@ +module PROOFTEST + imports IOTEST + rule a => c +endmodule diff --git a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala index c194e5ac5b..31139b7713 100644 --- a/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala +++ b/kale-backend/src/main/scala/org/kframework/kale/KaleRewriter.scala @@ -8,7 +8,7 @@ import org.kframework.definition._ import org.kframework.frontend.Unapply.KRewrite import org.kframework.frontend._ import org.kframework.rewriter.SearchType -import org.kframework.{RewriterResult, frontend} +import org.kframework.{ProofResult, RewriterResult, frontend} import scala.collection._ @@ -206,5 +206,5 @@ class KaleRewriter(m: Module) extends org.kframework.rewriter.Rewriter { override def executeAndMatch(k: K, depth: Optional[Integer], rule: Rule): (RewriterResult, K) = ??? - override def prove(rules: util.List[Rule]): util.List[K] = ??? + override def prove(rules: util.List[Rule]): ProofResult = ??? } diff --git a/kernel/src/main/java/org/kframework/krun/KRun.java b/kernel/src/main/java/org/kframework/krun/KRun.java index f58f8e1244..ad07d4f703 100644 --- a/kernel/src/main/java/org/kframework/krun/KRun.java +++ b/kernel/src/main/java/org/kframework/krun/KRun.java @@ -3,6 +3,7 @@ import org.apache.commons.io.output.ByteArrayOutputStream; import org.apache.commons.lang3.tuple.Pair; +import org.kframework.ProofResult; import org.kframework.RewriterResult; import org.kframework.attributes.Source; import org.kframework.builtin.KLabels; @@ -123,9 +124,18 @@ public int run(KompileMetaInfo kompileMetaInfo, CompiledDefinition compiledDef, return (Integer) tuple._2(); } } else if (options.experimental.prove != null) { - if (((List) result).isEmpty()) { + ProofResult proofResult = (ProofResult) result; + switch (proofResult.getStatus()) { + case PROVED: System.out.println("true"); + break; + case NOT_PROVED: + System.out.println("Claim(s) Couldn't Be Proven!"); + break; + case EMPTY_SPEC: + System.out.println("No Rules with attribute \"claim\" found"); } + } else if (result instanceof Integer) { return (Integer) result; }