Skip to content
This repository was archived by the owner on Feb 1, 2020. It is now read-only.

Commit 5987478

Browse files
daejunparkdaejunpark
committed
Merge remote-tracking branch 'origin/equiv' into no-dep-inj
2 parents 1abc6a5 + 7f56a32 commit 5987478

File tree

14 files changed

+349
-17
lines changed

14 files changed

+349
-17
lines changed

‎.idea/codeStyleSettings.xml

+2-1
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎API/pom.xml

+19
Original file line numberDiff line numberDiff line change
@@ -30,4 +30,23 @@
3030
<version>${project.version}</version>
3131
</dependency>
3232
</dependencies>
33+
34+
<!-- from java-backend/pom.xml
35+
<build>
36+
<plugins>
37+
<plugin>
38+
<artifactId>maven-surefire-plugin</artifactId>
39+
<version>2.17</version>
40+
<configuration>
41+
<environmentVariables>
42+
<LD_LIBRARY_PATH>${env.LD_LIBRARY_PATH}${path.separator}${project.build.directory}/lib/native</LD_LIBRARY_PATH>
43+
<DYLD_LIBRARY_PATH>${env.DYLD_LIBRARY_PATH}${path.separator}${project.build.directory}/lib/native</DYLD_LIBRARY_PATH>
44+
<PATH>${env.PATH}${path.separator}${project.build.directory}/lib/native</PATH>
45+
</environmentVariables>
46+
</configuration>
47+
</plugin>
48+
</plugins>
49+
</build>
50+
-->
51+
3352
</project>

‎API/run.sh

+3
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#!/bin/bash -x
2+
3+
java -Djava.awt.headless=true -Xms64m -Xmx4096m -ea -cp "$(dirname "$0")/target/*:$(dirname "$0")/../k-distribution/target/release/k/lib/java/*" org.kframework.KRunAPI "$@"

‎API/src/main/java/org/kframework/HookProvider.java

+86
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
// Copyright (c) 2016 K Team. All Rights Reserved.
2+
package org.kframework;
3+
4+
import com.google.inject.Provider;
5+
import org.kframework.utils.errorsystem.KEMException;
6+
import org.kframework.utils.errorsystem.KExceptionManager;
7+
8+
import java.io.IOException;
9+
import java.io.InputStream;
10+
import java.lang.invoke.MethodHandle;
11+
import java.lang.invoke.MethodHandles;
12+
import java.lang.reflect.Method;
13+
import java.util.HashMap;
14+
import java.util.Map;
15+
import java.util.Properties;
16+
17+
/**
18+
* HookProvider
19+
*
20+
* Copied from org.kframework.backend.java.symbolic.JavaSymbolicCommonModule
21+
*/
22+
public class HookProvider {
23+
24+
private static final String HOOK_PROPERTIES_FILE_NAME = "/org/kframework/backend/java/symbolic/hooks.properties";
25+
26+
private static Map<String, String> getHookDeclarations() {
27+
Properties properties = new Properties();
28+
try {
29+
InputStream inStream = KRunAPI.class.getResourceAsStream(HOOK_PROPERTIES_FILE_NAME);
30+
if (inStream == null) {
31+
throw new IOException("Could not find resource " + HOOK_PROPERTIES_FILE_NAME);
32+
}
33+
properties.load(inStream);
34+
} catch (IOException e) {
35+
throw KEMException.internalError("Could not read from resource " + HOOK_PROPERTIES_FILE_NAME, e);
36+
}
37+
Map<String, String> builtinMethods = new HashMap<>();
38+
for (Object o: properties.keySet()) {
39+
String key = (String) o;
40+
builtinMethods.put(key, properties.getProperty(key));
41+
}
42+
return builtinMethods;
43+
}
44+
45+
private static Map<String, Provider<MethodHandle>> getBuiltinTable(Map<String, String> hookDeclarations, KExceptionManager kem) {
46+
Map<String, Provider<MethodHandle>> result = new HashMap<>();
47+
MethodHandles.Lookup lookup = MethodHandles.lookup();
48+
for (String key : hookDeclarations.keySet()) {
49+
String hook = hookDeclarations.get(key);
50+
try {
51+
String className = hook.substring(0, hook.lastIndexOf('.'));
52+
String methodName = hook.substring(hook.lastIndexOf('.') + 1);
53+
Class<?> c = Class.forName(className);
54+
for (Method method : c.getDeclaredMethods()) {
55+
if (method.getName().equals(methodName)) {
56+
MethodHandle handle = lookup.unreflect(method);
57+
result.put(key, () -> {
58+
MethodHandle resultHandle = handle;
59+
/* TODO: support non-static hooks e.g., z3 bindings
60+
if (!Modifier.isStatic(method.getModifiers())) {
61+
try {
62+
resultHandle = MethodHandles.insertArguments(handle, 0 , injector.getInstance(c));
63+
} catch (KEMException e) {
64+
e.exception.addTraceFrame("while constructing implementation for " + hook + " hook.");
65+
throw e;
66+
}
67+
}
68+
*/
69+
return resultHandle;
70+
});
71+
break;
72+
}
73+
}
74+
} catch (ClassNotFoundException | SecurityException | IllegalAccessException e) {
75+
kem.registerCriticalWarning("missing implementation for hook " + key + ":\n" + hook, e);
76+
}
77+
}
78+
return result;
79+
}
80+
81+
public static Map<String, Provider<MethodHandle>> get(KExceptionManager kem) {
82+
Map<String, String> hookDeclarations = getHookDeclarations();
83+
return getBuiltinTable(hookDeclarations, kem);
84+
}
85+
86+
}

‎API/src/main/java/org/kframework/KRunAPI.java

+111
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,111 @@
1+
// Copyright (c) 2016 K Team. All Rights Reserved.
2+
package org.kframework;
3+
4+
import com.google.inject.Provider;
5+
import org.kframework.RewriterResult;
6+
import org.kframework.attributes.Source;
7+
import org.kframework.backend.java.symbolic.InitializeRewriter;
8+
import org.kframework.backend.java.symbolic.JavaExecutionOptions;
9+
import org.kframework.definition.Definition;
10+
import org.kframework.kompile.CompiledDefinition;
11+
import org.kframework.kompile.Kompile;
12+
import org.kframework.kompile.KompileOptions;
13+
import org.kframework.kore.K;
14+
import org.kframework.kore.compile.KTokenVariablesToTrueVariables;
15+
import org.kframework.krun.KRun;
16+
import org.kframework.krun.KRunOptions;
17+
import org.kframework.krun.api.io.FileSystem;
18+
import org.kframework.krun.ioserver.filesystem.portable.PortableFileSystem;
19+
import org.kframework.main.GlobalOptions;
20+
import org.kframework.rewriter.Rewriter;
21+
import org.kframework.utils.errorsystem.KExceptionManager;
22+
import org.kframework.utils.file.FileUtil;
23+
24+
import java.io.File;
25+
import java.lang.invoke.MethodHandle;
26+
import java.util.Map;
27+
import java.util.Optional;
28+
import java.util.function.BiFunction;
29+
30+
import static org.kframework.Collections.*;
31+
import static org.kframework.kore.KORE.*;
32+
33+
/**
34+
* KRunAPI
35+
*/
36+
public class KRunAPI {
37+
38+
public static RewriterResult run(CompiledDefinition compiledDef, String programText, Integer depth) {
39+
40+
GlobalOptions globalOptions = new GlobalOptions();
41+
KompileOptions kompileOptions = new KompileOptions();
42+
KRunOptions krunOptions = new KRunOptions();
43+
JavaExecutionOptions javaExecutionOptions = new JavaExecutionOptions();
44+
45+
KExceptionManager kem = new KExceptionManager(globalOptions);
46+
FileUtil files = FileUtil.testFileUtil();
47+
boolean ttyStdin = false;
48+
49+
FileSystem fs = new PortableFileSystem(kem, files);
50+
Map<String, Provider<MethodHandle>> hookProvider = HookProvider.get(kem); // new HashMap<>();
51+
InitializeRewriter.InitializeDefinition initializeDefinition = new InitializeRewriter.InitializeDefinition();
52+
53+
BiFunction<String, Source, K> programParser = compiledDef.getProgramParser(kem);
54+
K pgm = programParser.apply(programText, Source.apply("generated by api"));
55+
K program = KRun.parseConfigVars(krunOptions, compiledDef, kem, files, ttyStdin, pgm);
56+
57+
/* TODO: figure out if it is needed
58+
program = new KTokenVariablesToTrueVariables()
59+
.apply(compiledDef.kompiledDefinition.getModule(compiledDef.mainSyntaxModuleName()).get(), program);
60+
*/
61+
62+
Rewriter rewriter = (InitializeRewriter.SymbolicRewriterGlue)
63+
new InitializeRewriter(
64+
fs,
65+
javaExecutionOptions,
66+
globalOptions,
67+
kem,
68+
kompileOptions.experimental.smt,
69+
hookProvider,
70+
kompileOptions,
71+
krunOptions,
72+
files,
73+
initializeDefinition)
74+
.apply(compiledDef.executionModule());
75+
76+
RewriterResult result = ((InitializeRewriter.SymbolicRewriterGlue) rewriter).execute(program, Optional.ofNullable(depth), true);
77+
78+
return result;
79+
}
80+
81+
public static void main(String[] args) {
82+
GlobalOptions globalOptions = new GlobalOptions();
83+
KompileOptions kompileOptions = new KompileOptions();
84+
KRunOptions krunOptions = new KRunOptions();
85+
KExceptionManager kem = new KExceptionManager(globalOptions);
86+
FileUtil files = FileUtil.testFileUtil();
87+
88+
if (args.length < 2) {
89+
System.out.println("usage: <def> <main-module> <pgm>");
90+
return;
91+
}
92+
String def = FileUtil.load(new File(args[0])); // "require \"domains.k\" module A syntax KItem ::= \"run\" endmodule"
93+
String pgm = FileUtil.load(new File(args[2])); // "run"
94+
95+
String mainModuleName = args[1]; // "A"
96+
97+
// kompile
98+
Definition d = DefinitionParser.from(def, mainModuleName);
99+
CompiledDefinition compiledDef = Kompile.run(d, kompileOptions, kem);
100+
101+
// krun
102+
RewriterResult result = run(compiledDef, pgm, null);
103+
104+
// print output
105+
// from org.kframework.krun.KRun.run()
106+
KRun.prettyPrint(compiledDef, krunOptions.output, s -> KRun.outputFile(s, krunOptions, files), result.k());
107+
108+
return;
109+
}
110+
111+
}

‎java-backend/src/main/java/org/kframework/backend/java/symbolic/InitializeRewriter.java

+10-1
Original file line numberDiff line numberDiff line change
@@ -128,12 +128,21 @@ public SymbolicRewriterGlue(
128128
this.kem = kem;
129129
}
130130

131+
// org.kframework.main.FrontEnd#main
132+
// org.kframework.krun.KRunFrontEnd#run
133+
// org.kframework.krun.KRun#run
134+
// org.kframework.krun.modes.KRunExecutionMode#execute
131135
@Override
132136
public RewriterResult execute(K k, Optional<Integer> depth) {
137+
return execute(k, depth, false);
138+
}
139+
140+
public RewriterResult execute(K k, Optional<Integer> depth, boolean api) {
133141
TermContext termContext = TermContext.builder(rewritingContext).freshCounter(initCounterValue).build();
134142
KOREtoBackendKIL converter = new KOREtoBackendKIL(module, definition, termContext.global(), false);
135143
Term backendKil = KILtoBackendJavaKILTransformer.expandAndEvaluate(termContext, kem, converter.convert(k));
136-
this.rewriter = new SymbolicRewriter(rewritingContext, kompileOptions, javaOptions, new KRunState.Counter(), converter);
144+
this.rewriter = new SymbolicRewriter(rewritingContext, kompileOptions, javaOptions, new KRunState.Counter(), converter, api);
145+
// org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite()
137146
JavaKRunState result = (JavaKRunState) rewriter.rewrite(new ConstrainedTerm(backendKil, termContext), depth.orElse(-1));
138147
return new RewriterResult(result.getStepsTaken(), result.getJavaKilTerm());
139148
}

‎java-backend/src/main/java/org/kframework/backend/java/symbolic/JavaBackend.java

+1-1
Original file line numberDiff line numberDiff line change
@@ -101,7 +101,7 @@ public K apply(KApply kk) {
101101
}.apply(k);
102102
}, "Module-qualify sort predicates");
103103

104-
return d -> (func((Definition dd) -> kompile.defaultSteps().apply(dd)))
104+
return d -> (func((Definition dd) -> kompile.defaultSteps(kompile.kompileOptions, kompile.kem).apply(dd)))
105105
.andThen(DefinitionTransformer.fromRuleBodyTranformer(RewriteToTop::bubbleRewriteToTopInsideCells, "bubble out rewrites below cells"))
106106
.andThen(DefinitionTransformer.fromSentenceTransformer(new NormalizeAssoc(KORE.c()), "normalize assoc"))
107107
.andThen(DefinitionTransformer.fromHybrid(AddBottomSortForListsWithIdenticalLabels.singleton(), "AddBottomSortForListsWithIdenticalLabels"))

‎java-backend/src/main/java/org/kframework/backend/java/symbolic/SymbolicRewriter.java

+10
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,11 @@ public class SymbolicRewriter {
6161
@Inject
6262
public SymbolicRewriter(GlobalContext global, KompileOptions kompileOptions, JavaExecutionOptions javaOptions,
6363
KRunState.Counter counter, KOREtoBackendKIL constructor) {
64+
this(global, kompileOptions, javaOptions, counter, constructor, false);
65+
}
66+
67+
public SymbolicRewriter(GlobalContext global, KompileOptions kompileOptions, JavaExecutionOptions javaOptions,
68+
KRunState.Counter counter, KOREtoBackendKIL constructor, boolean api) {
6469
this.constructor = constructor;
6570
this.definition = global.getDefinition();
6671
this.allRuleBits = BitSet.apply(definition.ruleTable.size());
@@ -74,6 +79,11 @@ public SymbolicRewriter(GlobalContext global, KompileOptions kompileOptions, Jav
7479
this.transition = true;
7580
}
7681

82+
// org.kframework.main.FrontEnd#main
83+
// org.kframework.krun.KRunFrontEnd#run
84+
// org.kframework.krun.KRun#run
85+
// org.kframework.krun.modes.KRunExecutionMode#execute
86+
// org.kframework.backend.java.symbolic.InitializeRewriter.SymbolicRewriterGlue#execute
7787
public KRunState rewrite(ConstrainedTerm constrainedTerm, int bound) {
7888
stopwatch.start();
7989
int step = 0;

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

+18-6
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ public class Kompile {
6363

6464
public final KompileOptions kompileOptions;
6565
private final FileUtil files;
66-
private final KExceptionManager kem;
66+
public final KExceptionManager kem;
6767
private final ParserUtils parser;
6868
private final Stopwatch sw;
6969
private final DefinitionParsing definitionParsing;
@@ -100,7 +100,7 @@ public Kompile(KompileOptions kompileOptions, GlobalOptions global, FileUtil fil
100100
}
101101

102102
public CompiledDefinition run(File definitionFile, String mainModuleName, String mainProgramsModuleName) {
103-
return run(definitionFile, mainModuleName, mainProgramsModuleName, defaultSteps());
103+
return run(definitionFile, mainModuleName, mainProgramsModuleName, defaultSteps(kompileOptions, kem));
104104
}
105105

106106
/**
@@ -126,15 +126,27 @@ public CompiledDefinition run(File definitionFile, String mainModuleName, String
126126
return new CompiledDefinition(kompileOptions, parsedDef, kompiledDefinition, configInfo.getDefaultCell(configInfo.topCell()).klabel());
127127
}
128128

129+
public static CompiledDefinition run(Definition parsedDef, KompileOptions kompileOptions, KExceptionManager kem) {
130+
/* TODO: enable checking
131+
checkDefinition(parsedDef);
132+
*/
133+
134+
Definition kompiledDefinition = defaultSteps(kompileOptions, kem).apply(parsedDef);
135+
136+
ConfigurationInfoFromModule configInfo = new ConfigurationInfoFromModule(kompiledDefinition.mainModule());
137+
138+
return new CompiledDefinition(kompileOptions, parsedDef, kompiledDefinition, configInfo.getDefaultCell(configInfo.topCell()).klabel());
139+
}
140+
129141
public Definition parseDefinition(File definitionFile, String mainModuleName, String mainProgramsModule) {
130142
return definitionParsing.parseDefinitionAndResolveBubbles(definitionFile, mainModuleName, mainProgramsModule);
131143
}
132144

133-
public Definition resolveIOStreams(Definition d) {
145+
public static Definition resolveIOStreams(Definition d) {
134146
return DefinitionTransformer.fromHybrid(new ResolveIOStreams(d, kem)::resolve, "resolving io streams").apply(d);
135147
}
136148

137-
public Function<Definition, Definition> defaultSteps() {
149+
public static Function<Definition, Definition> defaultSteps(KompileOptions kompileOptions, KExceptionManager kem) {
138150
DefinitionTransformer convertStrictToContexts = DefinitionTransformer.fromHybrid(new ResolveStrict(kompileOptions)::resolve, "resolving strict and seqstrict attributes");
139151
DefinitionTransformer resolveHeatCoolAttribute = DefinitionTransformer.fromSentenceTransformer(new ResolveHeatCoolAttribute(new HashSet<>(kompileOptions.transition))::resolve, "resolving heat and cool attributes");
140152
DefinitionTransformer convertAnonVarsToNamedVars = DefinitionTransformer.fromSentenceTransformer(new ResolveAnonVar()::resolve, "resolving \"_\" vars");
@@ -181,7 +193,7 @@ private void checkDefinition(Definition parsedDef) {
181193
}
182194
}
183195

184-
public Definition addSemanticsModule(Definition d) {
196+
public static Definition addSemanticsModule(Definition d) {
185197
java.util.Set<Sentence> prods = new HashSet<>();
186198
for (Sort srt : iterable(d.mainModule().definedSorts())) {
187199
if (!RuleGrammarGenerator.isParserSort(srt)) {
@@ -201,7 +213,7 @@ public Definition addSemanticsModule(Definition d) {
201213
return Constructors.Definition(withKSeq, immutable(allModules), d.att());
202214
}
203215

204-
public Definition resolveFreshConstants(Definition input) {
216+
public static Definition resolveFreshConstants(Definition input) {
205217
return DefinitionTransformer.fromHybrid(new ResolveFreshConstants(input)::resolve, "resolving !Var variables")
206218
.apply(input);
207219
}

0 commit comments

Comments
 (0)