Add flag --emit-json-spec to kprovex

k-distribution/tests/pyk/Makefile

@@ -11,19 +11,20 @@ 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
 
 .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
 
 clean:
-	rm -rf $(llvm_dir) $(haskell_dir)
+	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
@@ -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 $<

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('<generatedTop>', [KVariable('CONFIG'), KVariable('_')]), KVariable('CONFIG')
+    return rewriteAnywhereWith(rule, term)

k-distribution/tests/pyk/emit-json-spec-tests/looping-spec.k

@@ -0,0 +1,18 @@
+requires "verification.k"
+
+module LOOPING-SPEC
+    imports VERIFICATION
+
+    claim <k> while ( 1 <= $n ) {
+                $s = $s + $n ;
+                $n = $n + -1 ;
+              }
+           => . ... </k>
+          <state> $s |-> (S:Int => S +Int ((N +Int 1) *Int N /Int 2))
+                  $n |-> (N:Int => 0)
+          </state>
+      requires N >=Int 0
+       andBool S >=Int 0
+
+endmodule
+

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
+

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() {

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;
 }

kernel/src/main/java/org/kframework/kprovex/KProve.java

@@ -20,6 +20,7 @@
 import org.kframework.utils.file.FileUtil;
 import scala.Tuple2;
 
+import java.io.File;
 import java.io.UnsupportedEncodingException;
 import java.util.function.Function;
 
@@ -85,6 +86,10 @@ public int run() {
             }
         }
 
+        if (kproveOptions.emitJsonSpec != null) {
+            files.saveToWorkingDirectory(kproveOptions.emitJsonSpec, ToJson.apply(specModule));
+        }
+
         RewriterResult results = rewriter.prove(specModule, boundaryPattern, true);
         sw.printIntermediate("Backend");
         kprint.prettyPrint(compiled._1(), compiled._1().getModule("LANGUAGE-PARSING").get(), kprint::outputFile,

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"

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();
 
@@ -143,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());