From 4ef1d22e1ac26eb4847281b324c6842cb759659e Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 8 Feb 2022 15:58:12 +0000 Subject: [PATCH 01/13] kernel/unparser/ToJson: add apply method which takes a module --- .../java/org/kframework/unparser/ToJson.java | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index a6d88de0f55..660ba3adee2 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -98,6 +98,26 @@ public static byte[] apply(Definition def) { return out.toByteArray(); } + public static byte[] apply(Module mod) { + ByteArrayOutputStream out = new ByteArrayOutputStream(); + try { + DataOutputStream data = new DataOutputStream(out); + JsonWriter jsonWriter = Json.createWriter(data); + + JsonObjectBuilder term = Json.createObjectBuilder(); + term.add("format", "KAST"); + term.add("version", 1); + term.add("term", toJson(mod)); + + jsonWriter.write(term.build()); + jsonWriter.close(); + data.close(); + } catch (IOException e) { + throw KEMException.criticalError("Could not write Module to Json", e); + } + return out.toByteArray(); + } + public static JsonStructure toJson(Definition def) { JsonObjectBuilder jdef = Json.createObjectBuilder(); From 9be9bb2a17769a466cf044bf1618a3f885753eac Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 8 Feb 2022 15:58:54 +0000 Subject: [PATCH 02/13] kernel/{KProveOptions,kprovex/KProve}: add --emit-json-spec option --- .../java/org/kframework/kprove/KProveOptions.java | 3 +++ .../main/java/org/kframework/kprovex/KProve.java | 14 ++++++++++++++ 2 files changed, 17 insertions(+) diff --git a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java index 9ea1e11a186..f0317d8b3f2 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProveOptions.java +++ b/kernel/src/main/java/org/kframework/kprove/KProveOptions.java @@ -94,4 +94,7 @@ public synchronized File specFile(FileUtil files) { @Parameter(names="--emit-json", description="Emit JSON serialized main definition for proving.") public boolean emitJson = false; + + @Parameter(names="--emit-json-spec", description="If set, emit the JSON serialization of the spec module to the specified file.") + public String emitJsonSpec = null; } diff --git a/kernel/src/main/java/org/kframework/kprovex/KProve.java b/kernel/src/main/java/org/kframework/kprovex/KProve.java index b0c2991d559..5789051974f 100644 --- a/kernel/src/main/java/org/kframework/kprovex/KProve.java +++ b/kernel/src/main/java/org/kframework/kprovex/KProve.java @@ -20,6 +20,8 @@ import org.kframework.utils.file.FileUtil; import scala.Tuple2; +import java.io.FileNotFoundException; +import java.io.PrintWriter; import java.io.UnsupportedEncodingException; import java.util.function.Function; @@ -85,6 +87,18 @@ public int run() { } } + if (kproveOptions.emitJsonSpec != null) { + try { + String out = new String(ToJson.apply(specModule)); + PrintWriter fOut = new PrintWriter(kproveOptions.emitJsonSpec); + fOut.println(out); + fOut.close(); + } catch (FileNotFoundException e) { + System.err.println("Could not open node output file: " + kproveOptions.emitJsonSpec); + e.printStackTrace(); + } + } + RewriterResult results = rewriter.prove(specModule, boundaryPattern, true); sw.printIntermediate("Backend"); kprint.prettyPrint(compiled._1(), compiled._1().getModule("LANGUAGE-PARSING").get(), kprint::outputFile, From 062aea971cd37f6e6a2b3207013d57a7d1cca32b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 8 Feb 2022 16:00:12 +0000 Subject: [PATCH 03/13] kernel/kprove/KProve: add check for option not being used on kprove tool --- kernel/src/main/java/org/kframework/kprove/KProve.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kernel/src/main/java/org/kframework/kprove/KProve.java b/kernel/src/main/java/org/kframework/kprove/KProve.java index 0c2778f6f18..e9ef4bba890 100644 --- a/kernel/src/main/java/org/kframework/kprove/KProve.java +++ b/kernel/src/main/java/org/kframework/kprove/KProve.java @@ -61,6 +61,9 @@ public KProve(KExceptionManager kem, FileUtil files, KPrint kprint, KProveOption this.proofDefinitionBuilder = proofDefinitionBuilder; this.rewriterGenerator = rewriterGenerator; this.sw = sw; + if (kproveOptions.emitJsonSpec != null) { + throw KEMException.criticalError("Option `--emit-json-spec` only supported in kprovex tool!"); + } } public int run() { From d709e5405ea36d1471b8f1e77c42243a57cfa800 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Tue, 8 Feb 2022 16:44:17 +0000 Subject: [PATCH 04/13] kernel/{JsonParser,ToJson}: correct emitted nodes for KImport --- kernel/src/main/java/org/kframework/parser/json/JsonParser.java | 1 + kernel/src/main/java/org/kframework/unparser/ToJson.java | 1 + 2 files changed, 2 insertions(+) diff --git a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java index 18825f3e078..1dccd281922 100644 --- a/kernel/src/main/java/org/kframework/parser/json/JsonParser.java +++ b/kernel/src/main/java/org/kframework/parser/json/JsonParser.java @@ -66,6 +66,7 @@ public class JsonParser { , KNONTERMINAL = "KNonTerminal" , KMODULE = "KModule" , KFLATMODULE = "KFlatModule" + , KIMPORT = "KImport" , KPRODUCTION = "KProduction" , KREGEXTERMINAL = "KRegexTerminal" , KREWRITE = "KRewrite" diff --git a/kernel/src/main/java/org/kframework/unparser/ToJson.java b/kernel/src/main/java/org/kframework/unparser/ToJson.java index 660ba3adee2..6b341a59c8c 100644 --- a/kernel/src/main/java/org/kframework/unparser/ToJson.java +++ b/kernel/src/main/java/org/kframework/unparser/ToJson.java @@ -163,6 +163,7 @@ public static JsonStructure toJson(FlatModule mod) { JsonArrayBuilder imports = Json.createArrayBuilder(); stream(mod.imports()).forEach(i -> { JsonObjectBuilder jimp = Json.createObjectBuilder(); + jimp.add("node", JsonParser.KIMPORT); jimp.add("name", i.name()); jimp.add("isPublic", i.isPublic()); imports.add(jimp.build()); From 33f5c0bae8b5ddeb8102a705779fad7c0636d86b Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Wed, 9 Feb 2022 11:19:41 +0100 Subject: [PATCH 05/13] k-distribution/tests/pyk/Makefile: add --no-pager to diff check --- k-distribution/tests/pyk/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/pyk/Makefile b/k-distribution/tests/pyk/Makefile index cfa8c152703..387ddca759b 100644 --- a/k-distribution/tests/pyk/Makefile +++ b/k-distribution/tests/pyk/Makefile @@ -11,7 +11,7 @@ KPYK = $(K_BIN)/kpyk export PATH := $(K_BIN):$(PATH) -CHECK = git diff --no-index -R +CHECK = git --no-pager diff --no-index -R PYTHONPATH := $(K_LIB) export PYTHONPATH From b9ccd438f247022fc396a84c2e8ad4ba6c1f880b Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Wed, 9 Feb 2022 12:59:58 +0100 Subject: [PATCH 06/13] Add test specification for kprovex --emit-json-spec --- k-distribution/tests/pyk/Makefile | 17 +++++++++++++++-- .../pyk/emit-json-spec-tests/looping-spec.k | 18 ++++++++++++++++++ .../pyk/emit-json-spec-tests/verification.k | 12 ++++++++++++ 3 files changed, 45 insertions(+), 2 deletions(-) create mode 100644 k-distribution/tests/pyk/emit-json-spec-tests/looping-spec.k create mode 100644 k-distribution/tests/pyk/emit-json-spec-tests/verification.k diff --git a/k-distribution/tests/pyk/Makefile b/k-distribution/tests/pyk/Makefile index 387ddca759b..09a7d42d8a6 100644 --- a/k-distribution/tests/pyk/Makefile +++ b/k-distribution/tests/pyk/Makefile @@ -18,7 +18,8 @@ export PYTHONPATH .PHONY: all clean update-results pyk \ test test-defn test-defn-kast test-defn-prove \ - test-kpyk test-kpyk-coverage-log test-kpyk-graphviz test-kpyk-minimize-term + test-kpyk test-kpyk-coverage-log test-kpyk-graphviz test-kpyk-minimize-term \ + test-emit-json-spec all: test @@ -49,7 +50,7 @@ kompile: $(llvm_imp_kompiled) $(haskell_imp_kompiled) # Tests -test: test-unit test-defn test-kpyk +test: test-unit test-defn test-kpyk test-emit-json-spec ## Unit Tests @@ -108,3 +109,15 @@ test-kpyk-minimize-term: kpyk-tests/minimize/test.k $(KPYK) kpyk-tests/minimize/test-kompiled prove kpyk-tests/minimize/test.k kpyk-tests/minimize/test.k TEST-SPEC \ | $(KPYK) kpyk-tests/minimize/test-kompiled print /dev/stdin > kpyk-tests/minimize/test.k.out $(CHECK) kpyk-tests/minimize/test.k.out kpyk-tests/minimize/test.k.expected + + +## kprovex --emit-json-spec tests + +emit-json-spec-tests/verification-kompiled/timestamp: emit-json-spec-tests/verification.k imp.k + kompile $< --backend haskell -I . --emit-json + +emit-json-spec-tests/looping-spec.json: emit-json-spec-tests/looping-spec.k emit-json-spec-tests/verification-kompiled/timestamp + kprovex $< --backend haskell -I . --directory $(@D) --emit-json-spec $@ --dry-run + +test-emit-json-spec: emit-json-spec-tests/emit_json_spec_test.py emit-json-spec-tests/looping-spec.json + python3 -m unittest $< diff --git a/k-distribution/tests/pyk/emit-json-spec-tests/looping-spec.k b/k-distribution/tests/pyk/emit-json-spec-tests/looping-spec.k new file mode 100644 index 00000000000..654f07b60fd --- /dev/null +++ b/k-distribution/tests/pyk/emit-json-spec-tests/looping-spec.k @@ -0,0 +1,18 @@ +requires "verification.k" + +module LOOPING-SPEC + imports VERIFICATION + + claim while ( 1 <= $n ) { + $s = $s + $n ; + $n = $n + -1 ; + } + => . ... + $s |-> (S:Int => S +Int ((N +Int 1) *Int N /Int 2)) + $n |-> (N:Int => 0) + + requires N >=Int 0 + andBool S >=Int 0 + +endmodule + diff --git a/k-distribution/tests/pyk/emit-json-spec-tests/verification.k b/k-distribution/tests/pyk/emit-json-spec-tests/verification.k new file mode 100644 index 00000000000..ce3b23c6cc7 --- /dev/null +++ b/k-distribution/tests/pyk/emit-json-spec-tests/verification.k @@ -0,0 +1,12 @@ +requires "imp.k" + +module VERIFICATION-SYNTAX + syntax Id ::= "$s" [token] + | "$n" [token] +endmodule + +module VERIFICATION + imports VERIFICATION-SYNTAX + imports IMP +endmodule + From 802a17b53b6f5555b1c616e520903bc7e1b38a7d Mon Sep 17 00:00:00 2001 From: Tamas Toth Date: Wed, 9 Feb 2022 17:47:02 +0100 Subject: [PATCH 07/13] Add Python unit tests for kprovex --emit-json-spec --- .../emit_json_spec_test.py | 83 +++++++++++++++++++ 1 file changed, 83 insertions(+) create mode 100644 k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py diff --git a/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py b/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py new file mode 100644 index 00000000000..90a7f30a4da --- /dev/null +++ b/k-distribution/tests/pyk/emit-json-spec-tests/emit_json_spec_test.py @@ -0,0 +1,83 @@ +import json +import os +import shutil +import unittest +from pathlib import Path + +from pyk.kast import KApply, KClaim, KDefinition, KRequire, KVariable +from pyk.kastManip import rewriteAnywhereWith +from pyk.ktool import KProve + + +class EmitJsonSpecTest(unittest.TestCase): + TEST_DIR = 'emit-json-spec-tests' + MAIN_FILE = 'verification.k' + USE_DIR = f'{TEST_DIR}/.kprove' + + def setUp(self): + shutil.rmtree(self.USE_DIR, ignore_errors=True) + os.makedirs(self.USE_DIR) + + self.kprove = KProve(f'{self.TEST_DIR}/verification-kompiled', self.MAIN_FILE, self.USE_DIR) + self.kprove.proverArgs += ['-I', '.'] + self._update_symbol_table(self.kprove) + + with open(f'{self.TEST_DIR}/looping-spec.json', 'r') as spec_file: + module = json.load(spec_file)['term'] + + claim = extract_claims(module)[0] + self.claim = KClaim( + body=eliminate_generated_top(claim['body']), + requires=claim['requires'], + ensures=claim['ensures'], + att=None + ) + + module['localSentences'] = [self.claim] + self.module = module + + def tearDown(self): + shutil.rmtree(self.USE_DIR) + + @staticmethod + def _update_symbol_table(kprove): + def paren(f): + def unparse(*args): + return '(' + f(*args) + ')' + return unparse + + kprove.symbolTable['_+Int_'] = paren(kprove.symbolTable['_+Int_']) + + def test_prove_claim(self): + # When + result = self.kprove.proveClaim(self.claim, 'looping-1') + + # Then + self.assertEqual(result['label'], '#Top') + + def test_prove(self): + # Given + spec_name = 'looping-2-spec' + spec_path = Path(f'{self.USE_DIR}/{spec_name}.k') + spec_module_name = spec_name.upper() + + self.module['name'] = spec_module_name + definition = KDefinition(self.module, [self.module], requires=[KRequire(self.MAIN_FILE)]) + + with open(spec_path, 'x') as spec_file: + spec_file.write(self.kprove.prettyPrint(definition)) + + # When + result = self.kprove.prove(spec_path, spec_module_name) + + # Then + self.assertEqual(result['label'], '#Top') + + +def extract_claims(module): + return [claim for claim in module['localSentences'] if claim['node'] == 'KClaim'] + + +def eliminate_generated_top(term): + rule = KApply('', [KVariable('CONFIG'), KVariable('_')]), KVariable('CONFIG') + return rewriteAnywhereWith(rule, term) From b78923e8681e6326ff5e280930df0bc81a4632dc Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 9 Feb 2022 20:49:19 +0000 Subject: [PATCH 08/13] kernel/kprovex/KProve: use existing FileUtil --- .../main/java/org/kframework/kprovex/KProve.java | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/kernel/src/main/java/org/kframework/kprovex/KProve.java b/kernel/src/main/java/org/kframework/kprovex/KProve.java index 5789051974f..e7d570d83e8 100644 --- a/kernel/src/main/java/org/kframework/kprovex/KProve.java +++ b/kernel/src/main/java/org/kframework/kprovex/KProve.java @@ -20,8 +20,7 @@ import org.kframework.utils.file.FileUtil; import scala.Tuple2; -import java.io.FileNotFoundException; -import java.io.PrintWriter; +import java.io.File; import java.io.UnsupportedEncodingException; import java.util.function.Function; @@ -88,15 +87,7 @@ public int run() { } if (kproveOptions.emitJsonSpec != null) { - try { - String out = new String(ToJson.apply(specModule)); - PrintWriter fOut = new PrintWriter(kproveOptions.emitJsonSpec); - fOut.println(out); - fOut.close(); - } catch (FileNotFoundException e) { - System.err.println("Could not open node output file: " + kproveOptions.emitJsonSpec); - e.printStackTrace(); - } + FileUtil.save(new File(kproveOptions.emitJsonSpec), ToJson.apply(specModule)); } RewriterResult results = rewriter.prove(specModule, boundaryPattern, true); From 16e707219556501ece4372de339e13a8665ff153 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 9 Feb 2022 20:49:40 +0000 Subject: [PATCH 09/13] java-backend/StateLog: use existing FileUtil --- .../org/kframework/backend/java/util/StateLog.java | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/java-backend/src/main/java/org/kframework/backend/java/util/StateLog.java b/java-backend/src/main/java/org/kframework/backend/java/util/StateLog.java index 7873fccc0ba..3e33faa44ce 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/util/StateLog.java +++ b/java-backend/src/main/java/org/kframework/backend/java/util/StateLog.java @@ -132,16 +132,7 @@ private String writeNode(K contents) { String fileCode = hash(contents); File outputFile = new File(this.blobsDir, fileCode + "." + OutputModes.JSON.ext()); if (! outputFile.exists()) { - try { - String out = new String(this.prettyPrinter.prettyPrintBytes(contents), StandardCharsets.UTF_8); - PrintWriter fOut = new PrintWriter(outputFile); - fOut.println(out); - fOut.close(); - writtenHashes.put(objectHash,fileCode); - } catch (FileNotFoundException e) { - System.err.println("Could not open node output file: " + outputFile.getAbsolutePath()); - e.printStackTrace(); - } + FileUtil.save(outputFile, this.prettyPrinter.prettyPrintBytes(contents)); } return fileCode; } From e15489f540e6c86470a0ba3257a8ed9d3c4df5fe Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 9 Feb 2022 21:35:19 +0000 Subject: [PATCH 10/13] k-distribution/tests/pyk/Makefile: formatting, better clean target --- k-distribution/tests/pyk/Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/tests/pyk/Makefile b/k-distribution/tests/pyk/Makefile index 09a7d42d8a6..63c7c0d2097 100644 --- a/k-distribution/tests/pyk/Makefile +++ b/k-distribution/tests/pyk/Makefile @@ -19,12 +19,12 @@ export PYTHONPATH .PHONY: all clean update-results pyk \ test test-defn test-defn-kast test-defn-prove \ test-kpyk test-kpyk-coverage-log test-kpyk-graphviz test-kpyk-minimize-term \ - test-emit-json-spec + test-emit-json-spec all: test clean: - rm -rf $(llvm_dir) $(haskell_dir) + rm -rf $(llvm_dir) $(haskell_dir) emit-json-spec-tests/verification-kompiled/timestamp emit-json-spec-tests/looping-spec.json llvm_dir := llvm llvm_imp := $(llvm_dir)/imp.k From 2e800de24949861e25b035b94c251be50a1a26e0 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 9 Feb 2022 21:38:05 +0000 Subject: [PATCH 11/13] k-distribution/tests/pyk/Makefile: correct subtarget name for celan --- k-distribution/tests/pyk/Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/tests/pyk/Makefile b/k-distribution/tests/pyk/Makefile index 63c7c0d2097..d392cc465f6 100644 --- a/k-distribution/tests/pyk/Makefile +++ b/k-distribution/tests/pyk/Makefile @@ -24,7 +24,7 @@ export PYTHONPATH all: test clean: - rm -rf $(llvm_dir) $(haskell_dir) emit-json-spec-tests/verification-kompiled/timestamp emit-json-spec-tests/looping-spec.json + rm -rf $(llvm_dir) $(haskell_dir) emit-json-spec-tests/verification-kompiled emit-json-spec-tests/looping-spec.json llvm_dir := llvm llvm_imp := $(llvm_dir)/imp.k From 45b43b37021c9334d870d31213152d523d34b38b Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 10 Feb 2022 00:24:54 +0000 Subject: [PATCH 12/13] kernel/kprovex/KProve: use saveToWorkingDirectory --- kernel/src/main/java/org/kframework/kprovex/KProve.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/src/main/java/org/kframework/kprovex/KProve.java b/kernel/src/main/java/org/kframework/kprovex/KProve.java index e7d570d83e8..49450660d21 100644 --- a/kernel/src/main/java/org/kframework/kprovex/KProve.java +++ b/kernel/src/main/java/org/kframework/kprovex/KProve.java @@ -87,7 +87,7 @@ public int run() { } if (kproveOptions.emitJsonSpec != null) { - FileUtil.save(new File(kproveOptions.emitJsonSpec), ToJson.apply(specModule)); + files.saveToWorkingDirectory(kproveOptions.emitJsonSpec, ToJson.apply(specModule)); } RewriterResult results = rewriter.prove(specModule, boundaryPattern, true); From 452b5d28e3f2d29c327538c840e571a4238c0c7c Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 11 Feb 2022 00:01:45 +0000 Subject: [PATCH 13/13] Revert "java-backend/StateLog: use existing FileUtil" This reverts commit 16e707219556501ece4372de339e13a8665ff153. --- .../org/kframework/backend/java/util/StateLog.java | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/java-backend/src/main/java/org/kframework/backend/java/util/StateLog.java b/java-backend/src/main/java/org/kframework/backend/java/util/StateLog.java index 3e33faa44ce..7873fccc0ba 100644 --- a/java-backend/src/main/java/org/kframework/backend/java/util/StateLog.java +++ b/java-backend/src/main/java/org/kframework/backend/java/util/StateLog.java @@ -132,7 +132,16 @@ private String writeNode(K contents) { String fileCode = hash(contents); File outputFile = new File(this.blobsDir, fileCode + "." + OutputModes.JSON.ext()); if (! outputFile.exists()) { - FileUtil.save(outputFile, this.prettyPrinter.prettyPrintBytes(contents)); + try { + String out = new String(this.prettyPrinter.prettyPrintBytes(contents), StandardCharsets.UTF_8); + PrintWriter fOut = new PrintWriter(outputFile); + fOut.println(out); + fOut.close(); + writtenHashes.put(objectHash,fileCode); + } catch (FileNotFoundException e) { + System.err.println("Could not open node output file: " + outputFile.getAbsolutePath()); + e.printStackTrace(); + } } return fileCode; }