Emit json definitions when kompiling

k-distribution/src/main/scripts/lib/pyk/__init__.py

@@ -44,13 +44,13 @@ def kprove(definition, inputFile, kproveArgs = [], teeOutput = True, kRelease =
 
 def kastJSON(definition, inputJSON, kastArgs = [], teeOutput = True, kRelease = None):
     with tempfile.NamedTemporaryFile(mode = 'w') as tempf:
-        json.dump(inputJSON, tempf)
+        tempf.write(json.dumps(inputJSON))
         tempf.flush()
         return kast(definition, tempf.name, kastArgs = kastArgs, teeOutput = teeOutput, kRelease = kRelease)
 
 def krunJSON(definition, inputJSON, krunArgs = [], teeOutput = True, kRelease = None):
     with tempfile.NamedTemporaryFile(mode = 'w') as tempf:
-        json.dump(inputJSON, tempf)
+        tempf.write(json.dumps(inputJSON))
         tempf.flush()
         (rC, out, err) = krun(definition, tempf.name, krunArgs = krunArgs + ['--output', 'json', '--parser', 'cat'], teeOutput = teeOutput, kRelease = kRelease)
         out = None if out == '' else json.loads(out)['term']

k-distribution/src/main/scripts/lib/pyk/kastManip.py

@@ -120,6 +120,19 @@ def flattenLabel(label, kast):
         return [ c for cs in constraints for c in cs ]
     return [kast]
 
+def splitConfigFrom(configuration):
+    initial_substitution = {}
+    _mkCellVar = lambda label: label.replace('-', '_').replace('<', '').replace('>', '').upper() + '_CELL'
+    def _replaceWithVar(k):
+        if pyk.isKApply(k) and pyk.isCellKLabel(k['label']):
+            if len(k['args']) == 1 and not (pyk.isKApply(k['args'][0]) and pyk.isCellKLabel(k['args'][0]['label'])):
+                config_var = _mkCellVar(k['label'])
+                initial_substitution[config_var] = k['args'][0]
+                return KApply(k['label'], [KVariable(config_var)])
+        return k
+    symbolic_config = pyk.traverseBottomUp(configuration, _replaceWithVar)
+    return (symbolic_config, initial_substitution)
+
 def collapseDots(kast):
     def _collapseDots(_kast):
         if isKApply(_kast):

k-distribution/tests/regression-new/imp-json/Makefile

@@ -0,0 +1,7 @@
+DEF=imp
+EXT=imp
+TESTDIR=.
+KOMPILE_BACKEND?=llvm
+KOMPILE_FLAGS=--emit-json
+
+include ../../../include/ktest.mak

k-distribution/tests/regression-new/imp-json/imp.k

@@ -0,0 +1,68 @@
+// Copyright (c) 2014-2019 K Team. All Rights Reserved.
+
+module IMP-SYNTAX
+  imports DOMAINS-SYNTAX
+
+  syntax AExp  ::= Int | Id
+                 | "-" Int                    [format(%1%2)]
+                 | AExp "/" AExp              [left, strict, color(pink)]
+                 > AExp "+" AExp              [left, strict, color(pink)]
+                 | "(" AExp ")"               [bracket]
+  syntax BExp  ::= Bool
+                 | AExp "<=" AExp             [seqstrict, latex({#1}\leq{#2}), color(pink)]
+                 | "!" BExp                   [strict, color(pink)]
+                 > BExp "&&" BExp             [left, strict(1), color(pink)]
+                 | "(" BExp ")"               [bracket]
+  syntax Block ::= "{" "}"
+                 | "{" Stmt "}"               [format(%1%i%n%2%d%n%3)]
+  syntax Stmt  ::= Block
+                 | Id "=" AExp ";"            [strict(2), color(pink), format(%1 %2 %3%4)]
+                 | "if" "(" BExp ")"
+                   Block "else" Block         [strict(1), colors(yellow, white, white, yellow), format(%1 %2%3%4 %5 %6 %7)]
+                 | "while" "(" BExp ")" Block [colors(yellow,white,white), format(%1 %2%3%4 %5)]
+                 > Stmt Stmt                  [left, format(%1%n%2)]
+
+  syntax Pgm ::= "int" Ids ";" Stmt           [format(%1 %2%3%n%4), colors(yellow,pink)]
+  syntax Ids ::= List{Id,","} [format(%1%2 %3)]
+endmodule
+
+module IMP
+  imports IMP-SYNTAX
+  imports INT
+  imports BOOL
+  imports MAP
+
+  syntax KResult ::= Int | Bool
+
+  configuration <T color="yellow">
+                  <k color="green"> $PGM:Pgm </k>
+                  <state color="red"> .Map </state>
+                </T>
+
+  rule <k> X:Id => I ...</k> <state>... X |-> I ...</state>
+
+  rule I1 / I2 => I1 /Int I2  requires I2 =/=Int 0
+  rule I1 + I2 => I1 +Int I2
+  rule - I1 => 0 -Int I1
+
+  rule I1 <= I2 => I1 <=Int I2
+  rule ! T => notBool T
+  rule true && B => B
+  rule false && _ => false
+
+  rule {} => .   [structural]
+  rule {S} => S  [structural]
+
+  rule <k> X = I:Int; => . ...</k> <state>... X |-> (_ => I) ...</state>
+
+  rule S1:Stmt S2:Stmt => S1 ~> S2  [structural]
+
+  rule if (true)  S else _ => S
+  rule if (false) _ else S => S
+
+  rule while (B) S => if (B) {S while (B) S} else {}  [structural]
+
+  rule <k> int (X,Xs => Xs);_ </k> <state> Rho:Map (.Map => X|->0) </state>
+    requires notBool (X in keys(Rho))
+  rule int .Ids; S => S  [structural]
+endmodule

kernel/src/main/java/org/kframework/kompile/Kompile.java

@@ -23,6 +23,7 @@
 import org.kframework.kore.Sort;
 import org.kframework.parser.concrete2kore.ParserUtils;
 import org.kframework.parser.concrete2kore.generator.RuleGrammarGenerator;
+import org.kframework.unparser.ToJson;
 import org.kframework.utils.Stopwatch;
 import org.kframework.utils.errorsystem.KEMException;
 import org.kframework.utils.errorsystem.KExceptionManager;
@@ -31,6 +32,7 @@
 import scala.Function1;
 
 import java.io.File;
+import java.io.UnsupportedEncodingException;
 import java.util.Collections;
 import java.util.EnumSet;
 import java.util.HashSet;
@@ -126,6 +128,15 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String
         files.saveToKompiled("compiled.txt", kompiledDefinition.toString());
         sw.printIntermediate("Apply compile pipeline");
 
+        if (kompileOptions.experimental.emitJson) {
+            try {
+                files.saveToKompiled("parsed.json",   new String(ToJson.apply(parsedDef),          "UTF-8"));
+                files.saveToKompiled("compiled.json", new String(ToJson.apply(kompiledDefinition), "UTF-8"));
+            } catch (UnsupportedEncodingException e) {
+                throw KEMException.criticalError("Unsupported encoding `UTF-8` when saving JSON definition.");
+            }
+        }
+
         ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(kompiledDefinition.mainModule());
 
         return new CompiledDefinition(kompileOptions, parsedDef, kompiledDefinition, files, kem, configInfo.getDefaultCell(configInfo.getRootCell()).klabel());

kernel/src/main/java/org/kframework/kompile/KompileOptions.java

@@ -4,12 +4,15 @@
 import com.beust.jcommander.Parameter;
 import com.beust.jcommander.ParametersDelegate;
 import org.apache.commons.io.FilenameUtils;
+
 import org.kframework.backend.Backends;
 import org.kframework.main.GlobalOptions;
+import org.kframework.unparser.OutputModes;
 import org.kframework.utils.file.FileUtil;
 import org.kframework.utils.inject.RequestScoped;
 import org.kframework.utils.options.OuterParsingOptions;
 import org.kframework.utils.options.SMTOptions;
+import org.kframework.utils.options.BaseEnumConverter;
 import org.kframework.utils.options.StringListConverter;
 
 import java.io.Serializable;
@@ -83,6 +86,18 @@ public boolean isKore() {
         return backend.equals("kore") || backend.equals("haskell") || backend.equals("llvm");
     }
 
+    public static class OutputModeConverter extends BaseEnumConverter<OutputModes> {
+
+        public OutputModeConverter(String optionName) {
+            super(optionName);
+        }
+
+        @Override
+        public Class<OutputModes> enumClass() {
+            return OutputModes.class;
+        }
+    }
+
     public static final class Experimental implements Serializable {
 
         // Experimental options
@@ -112,5 +127,8 @@ public static final class Experimental implements Serializable {
 
         @Parameter(names="--cache-file", description="Location of parse cache file. Default is $KOMPILED_DIR/cache.bin.")
         public String cacheFile;
+
+        @Parameter(names="--emit-json", description="Emit JSON serialized version of parsed and kompiled definitions.")
+        public boolean emitJson = false;
     }
 }