Skip to content

use cached scanner during kprovex #2421

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
rv-jenkins merged 2 commits into from
Feb 7, 2022
Merged

use cached scanner during kprovex #2421

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
d8a0c3a
use cached scanner during kprovex
Feb 1, 2022
7dcffce
Merge branch 'master' into kprovex_scanner
rv-jenkins Feb 7, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 15 additions & 8 deletions kernel/src/main/java/org/kframework/kompile/DefinitionParsing.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -131,7 +131,7 @@ public DefinitionParsing(
this.sw = sw;
}

public java.util.Set<Module> parseModules(CompiledDefinition definition, String mainModule, String entryPointModule, File definitionFile, java.util.Set<String> excludeModules, boolean readOnlyCache) {
public java.util.Set<Module> parseModules(CompiledDefinition definition, String mainModule, String entryPointModule, File definitionFile, java.util.Set<String> excludeModules, boolean readOnlyCache, boolean useCachedScanner) {
Definition def = parser.loadDefinition(
mainModule,
mutable(definition.getParsedDefinition().modules()),
Expand Down Expand Up @@ -174,7 +174,7 @@ public java.util.Set<Module> parseModules(CompiledDefinition definition, String
throw new AssertionError("should not reach this statement");
}

def = resolveNonConfigBubbles(def, false);
def = resolveNonConfigBubbles(def, false, useCachedScanner);
saveTimings();
if (! readOnlyCache) {
saveCaches();
Expand Down Expand Up @@ -229,7 +229,7 @@ public Definition parseDefinitionAndResolveBubbles(File definitionFile, String m
sw.printIntermediate("Parse configurations [" + parsedBubbles.get() + "/" + (parsedBubbles.get() + cachedBubbles.get()) + " declarations]");
parsedBubbles.set(0);
cachedBubbles.set(0);
Definition afterResolvingAllOtherBubbles = resolveNonConfigBubbles(afterResolvingConfigBubbles, true);
Definition afterResolvingAllOtherBubbles = resolveNonConfigBubbles(afterResolvingConfigBubbles, true, false);
sw.printIntermediate("Parse rules [" + parsedBubbles.get() + "/" + (parsedBubbles.get() + cachedBubbles.get()) + " rules]");
saveTimings();
saveCachesAndReportParsingErrors();
Expand Down Expand Up @@ -370,17 +370,24 @@ private Definition resolveConfigBubbles(Definition def) {
}, "expand configs").apply(defWithParsedConfigs);
}

private Definition resolveNonConfigBubbles(Definition defWithConfig, boolean serializeScanner) {
private Definition resolveNonConfigBubbles(Definition defWithConfig, boolean serializeScanner, boolean deserializeScanner) {
Definition defWithCaches = resolveCachedBubbles(defWithConfig, true);
RuleGrammarGenerator gen = new RuleGrammarGenerator(defWithCaches);
Module ruleParserModule = gen.getRuleGrammar(defWithCaches.mainModule());
ParseCache cache = loadCache(ruleParserModule);
try (ParseInModule parser = RuleGrammarGenerator.getCombinedGrammar(cache.getModule(), true, profileRules, files, true)) {
Scanner scanner = parser.getScanner(globalOptions);
if (serializeScanner) {
scanner.serialize(files.resolveKompiled("scanner"));
Scanner scanner;
if (deserializeScanner) {
scanner = new Scanner(parser, globalOptions, files.resolveKompiled("scanner"));
parser.setScanner(scanner);
} else {
scanner = parser.getScanner(globalOptions);
if (serializeScanner) {
scanner.serialize(files.resolveKompiled("scanner"));
}
}
Map<String, Module> parsed = defWithCaches.parMap(m -> this.resolveNonConfigBubbles(m, parser.getScanner(globalOptions), gen));
final Scanner realScanner = scanner;
Map<String, Module> parsed = defWithCaches.parMap(m -> this.resolveNonConfigBubbles(m, realScanner, gen));
return DefinitionTransformer.from(m -> Module(m.name(), m.imports(), parsed.get(m.name()).localSentences(), m.att()), "parsing rules").apply(defWithConfig);
}
}
Expand Down
4 changes: 2 additions & 2 deletions kernel/src/main/java/org/kframework/kompile/Kompile.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -514,8 +514,8 @@ public Rule compileRule(Definition compiledDef, Rule parsedRule) {
.apply(parsedRule);
}

public Set<Module> parseModules(CompiledDefinition definition, String mainModule, String entryPointModule, File definitionFile, Set<String> excludeModules, boolean readOnlyCache) {
Set<Module> modules = definitionParsing.parseModules(definition, mainModule, entryPointModule, definitionFile, excludeModules, readOnlyCache);
public Set<Module> parseModules(CompiledDefinition definition, String mainModule, String entryPointModule, File definitionFile, Set<String> excludeModules, boolean readOnlyCache, boolean useCachedScanner) {
Set<Module> modules = definitionParsing.parseModules(definition, mainModule, entryPointModule, definitionFile, excludeModules, readOnlyCache, useCachedScanner);
int totalBubbles = definitionParsing.parsedBubbles.get() + definitionParsing.cachedBubbles.get();
sw.printIntermediate("Parse spec modules [" + definitionParsing.parsedBubbles.get() + "/" + totalBubbles + " rules]");
return modules;
Expand Down
2 changes: 1 addition & 1 deletion kernel/src/main/java/org/kframework/kprove/ProofDefinitionBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -70,7 +70,7 @@ public Tuple2<Definition, Module> build(File specFile, String defModuleName, Str
File absSpecFile = files.resolveWorkingDirectory(specFile).getAbsoluteFile();

Set<Module> modules = kompile.parseModules(compiledDefinition, defModuleNameUpdated, specModuleNameUpdated, absSpecFile,
backend.excludedModuleTags(), readOnlyCache);
backend.excludedModuleTags(), readOnlyCache, false);
Map<String, Module> modulesMap = modules.stream().collect(Collectors.toMap(Module::name, m -> m));
Definition parsedDefinition = compiledDefinition.getParsedDefinition();
Module specModule = getModule(specModuleNameUpdated, modulesMap, parsedDefinition);
Expand Down
2 changes: 1 addition & 1 deletion kernel/src/main/java/org/kframework/kprovex/ProofDefinitionBuilder.java
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,7 @@ public Tuple2<Definition, Module> build(File specFile, String specModuleName, bo
File absSpecFile = files.resolveWorkingDirectory(specFile).getAbsoluteFile();

Set<Module> modules = kompile.parseModules(compiledDefinition, defModuleNameUpdated, specModuleNameUpdated, absSpecFile,
backend.excludedModuleTags(), true);
backend.excludedModuleTags(), true, true);
Map<String, Module> modulesMap = modules.stream().collect(Collectors.toMap(Module::name, m -> m));
Definition parsedDefinition = compiledDefinition.getParsedDefinition();
Module specModule = getModule(specModuleNameUpdated, modulesMap, parsedDefinition);
Expand Down