Skip to content

Commit

Permalink
Revert "Remove dead code HaskellKRunOptions (#3419)" (#3424)
Browse files Browse the repository at this point in the history 
This reverts commit 633caab.
  • Loading branch information
@radumereuta
radumereuta authored May 18, 2023
1 parent 516c606 commit 8d0513c
Show file tree
Hide file tree
Showing 5 changed files with 243 additions and 6 deletions.
15 changes: 15 additions & 0 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,11 +39,26 @@ private void installHaskellBackend(Binder binder) {
mapBinder.addBinding("haskell").to(HaskellBackend.class);
}

@Override
public List<Pair<Class<?>, Boolean>> krunOptions() {
return Collections.singletonList(Pair.of(HaskellKRunOptions.class, true));
}

@Override
public List<Pair<Class<?>, Boolean>> kompileOptions() {
return Collections.singletonList(Pair.of(HaskellKompileOptions.class, true));
}

@Override
public List<Module> getKRunModules() {
return Collections.singletonList(new AbstractModule() {
@Override
protected void configure() {
installHaskellRewriter(binder());
}
});
}

private void installHaskellRewriter(Binder binder) {
bindOptions(HaskellBackendKModule.this::krunOptions, binder);

Expand Down
33 changes: 33 additions & 0 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKRunOptions.java
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
// Copyright (c) Runtime Verification, Inc. All Rights Reserved.
package org.kframework.backend.haskell;

import com.beust.jcommander.Parameter;
import org.kframework.backend.kore.ModuleToKORE;
import org.kframework.utils.inject.RequestScoped;
import org.kframework.utils.options.BaseEnumConverter;

@RequestScoped
public class HaskellKRunOptions {

@Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.")
public String haskellBackendCommand = "kore-exec";

@Parameter(names="--haskell-backend-home", description="Directory where the Haskell backend source installation resides.")
public String haskellBackendHome = System.getenv("KORE_HOME");

@Parameter(names="--default-claim-type", converter = SentenceTypeConverter.class, description="Default type for claims. Values: [all-path|one-path].")
public ModuleToKORE.SentenceType defaultClaimType = ModuleToKORE.SentenceType.ALL_PATH;

public static class SentenceTypeConverter extends BaseEnumConverter<ModuleToKORE.SentenceType> {

public SentenceTypeConverter(String optionName) {
super(optionName);
}

@Override
public Class<ModuleToKORE.SentenceType> enumClass() {
return ModuleToKORE.SentenceType.class;
}
}

}
171 changes: 165 additions & 6 deletions haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,6 +61,7 @@ public class HaskellRewriter implements Function<Definition, Rewriter> {
private final SMTOptions smtOptions;
private final KompileOptions kompileOptions;
private final KProveOptions kProveOptions;
private final HaskellKRunOptions haskellKRunOptions;
private final BackendOptions backendOptions;
private final FileUtil files;
private final CompiledDefinition def;
Expand All @@ -74,6 +75,7 @@ public HaskellRewriter(
SMTOptions smtOptions,
KompileOptions kompileOptions,
KProveOptions kProveOptions,
HaskellKRunOptions haskellKRunOptions,
BackendOptions backendOptions,
FileUtil files,
CompiledDefinition def,
Expand All @@ -82,6 +84,7 @@ public HaskellRewriter(
Tool tool) {
this.globalOptions = globalOptions;
this.smtOptions = smtOptions;
this.haskellKRunOptions = haskellKRunOptions;
this.backendOptions = backendOptions;
this.kompileOptions = kompileOptions;
this.kProveOptions = kProveOptions;
Expand All @@ -98,7 +101,53 @@ public Rewriter apply(Definition definition) {
return new Rewriter() {
@Override
public RewriterResult execute(K k, Optional<Integer> depth) {
throw new RuntimeException("Haskell rewriter not implemented in the Java front end!");
Module mod = getExecutionModule(module);
ModuleToKORE converter = new ModuleToKORE(mod, def.topCellInitializer, kompileOptions);
String koreOutput = getKoreString(k, mod, converter);
String defPath = files.resolveKompiled("haskellDefinition.bin").exists() ?
files.resolveKompiled("haskellDefinition.bin").getAbsolutePath() :
files.resolveKompiled("definition.kore").getAbsolutePath();
String moduleName = mod.name();

files.saveToTemp("execute-initial.kore", koreOutput);
String pgmPath = files.resolveTemp("execute-initial.kore").getAbsolutePath();
String[] koreCommand = haskellKRunOptions.haskellBackendCommand.split("\\s+");
String koreDirectory = haskellKRunOptions.haskellBackendHome;
File koreOutputFile = files.resolveTemp("execute-result.kore");
List<String> args = new ArrayList<String>();
args.addAll(Arrays.asList(koreCommand));
args.addAll(Arrays.asList(
defPath,
"--module", moduleName,
"--pattern", pgmPath,
"--output", koreOutputFile.getAbsolutePath()));
if (depth.isPresent()) {
args.add("--depth");
args.add(Integer.toString(depth.get()));
}
if (smtOptions.smtPrelude != null) {
args.add("--smt-prelude");
args.add(smtOptions.smtPrelude);
}
koreCommand = args.toArray(koreCommand);
if (backendOptions.dryRun) {
System.out.println(String.join(" ", koreCommand));
kprint.options.output = OutputModes.NONE;
return new RewriterResult(Optional.empty(), Optional.empty(), k);
}
try {
File korePath = koreDirectory == null ? null : new File(koreDirectory);
int execStatus = executeCommandBasic(korePath, koreCommand);
checkOutput(koreOutputFile, execStatus);
K outputK = new KoreParser(mod.sortAttributesFor()).parseFile(koreOutputFile);
return new RewriterResult(Optional.empty(), Optional.of(execStatus), outputK);
} catch (IOException e) {
throw KEMException.criticalError("I/O Error while executing", e);
} catch (InterruptedException e) {
throw KEMException.criticalError("Interrupted while executing", e);
} catch (ParseError parseError) {
throw KEMException.criticalError("Error parsing haskell backend output", parseError);
}
}

@Override
Expand All @@ -114,9 +163,117 @@ public Tuple2<RewriterResult, K> executeAndMatch(K k, Optional<Integer> depth, R

@Override
public K search(K initialConfiguration, Optional<Integer> depth, Optional<Integer> bound, Rule pattern, SearchType searchType) {
throw new RuntimeException("Haskell rewriter not implemented in the Java front end!");
Module mod = getExecutionModule(module);
String koreOutput = getKoreString(initialConfiguration, mod, new ModuleToKORE(mod, def.topCellInitializer, kompileOptions));
Sort initializerSort = mod.productionsFor().get(def.topCellInitializer).get().head().sort();
K patternTerm = RewriteToTop.toLeft(pattern.body());
if (patternTerm instanceof KVariable) {
patternTerm = KORE.KVariable(((KVariable) patternTerm).name(), Att.empty().add(Sort.class, initializerSort));
}
K patternCondition = pattern.requires();
String patternTermKore = getKoreString(patternTerm, mod, new ModuleToKORE(mod, def.topCellInitializer, kompileOptions));
String patternConditionKore;
if (patternCondition.equals(TRUE)) {
patternConditionKore = "\\top{Sort" + initializerSort.name() + "{}}()";
} else {
patternConditionKore =
"\\equals{SortBool{},Sort" + initializerSort.name() + "{}}("
+ getKoreString(patternCondition, mod, new ModuleToKORE(mod, def.topCellInitializer, kompileOptions))
+ ", \\dv{SortBool{}}(\"true\")"
+ ")";
}
String korePatternOutput = "\\and{Sort" + initializerSort.name() + "{}}("
+ patternTermKore
+ ", " + patternConditionKore
+ ")";
String defPath = files.resolveKompiled("haskellDefinition.bin").exists() ?
files.resolveKompiled("haskellDefinition.bin").getAbsolutePath() :
files.resolveKompiled("definition.kore").getAbsolutePath();
String moduleName = mod.name();

files.saveToTemp("search-initial.kore", koreOutput);
String pgmPath = files.resolveTemp("search-initial.kore").getAbsolutePath();
files.saveToTemp("search-pattern.kore", korePatternOutput);
String patternPath = files.resolveTemp("search-pattern.kore").getAbsolutePath();
String[] koreCommand = haskellKRunOptions.haskellBackendCommand.split("\\s+");
String koreDirectory = haskellKRunOptions.haskellBackendHome;
File koreOutputFile = files.resolveTemp("search-result.kore");
List<String> args = new ArrayList<String>();
args.addAll(Arrays.asList(koreCommand));
args.addAll(Arrays.asList(
defPath,
"--module", moduleName,
"--pattern", pgmPath,
"--output", koreOutputFile.getAbsolutePath(),
"--searchType", searchType.toString(),
"--search", patternPath
)

);
if (depth.isPresent()) {
args.add("--depth");
args.add(depth.get().toString());
}
if (bound.isPresent()) {
args.add("--bound");
args.add(bound.get().toString());
}
if (smtOptions.smtPrelude != null) {
args.add("--smt-prelude");
args.add(smtOptions.smtPrelude);
}
koreCommand = args.toArray(koreCommand);
if (backendOptions.dryRun) {
System.out.println(String.join(" ", koreCommand));
kprint.options.output = OutputModes.NONE;
return initialConfiguration;
}
try {
File korePath = koreDirectory == null ? null : new File(koreDirectory);
if (executeCommandBasic(korePath, koreCommand) != 0) {
throw KEMException.criticalError("Haskell backend returned non-zero exit code");
}
K outputK = new KoreParser(mod.sortAttributesFor()).parseFile(koreOutputFile);
outputK = addAnonymousAttributes(outputK, pattern);
return outputK;
} catch (IOException e) {
throw KEMException.criticalError("I/O Error while executing", e);
} catch (InterruptedException e) {
throw KEMException.criticalError("Interrupted while executing", e);
} catch (ParseError parseError) {
throw KEMException.criticalError("Error parsing haskell backend output", parseError);
}
}

private K addAnonymousAttributes(K input, Rule pattern) {
Map<KVariable, KVariable> anonVars = new HashMap<>();
VisitK visitor = new VisitK() {
@Override
public void apply(KVariable var) {
anonVars.put(var, var);
}
};
visitor.apply(pattern.body());
visitor.apply(pattern.requires());
visitor.apply(pattern.ensures());
return new TransformK() {
@Override
public K apply(KVariable var) {
return anonVars.getOrDefault(var, var);
}
}.apply(input);
}

private Module getExecutionModule(Module module) {
Module mod = def.executionModule();
if (!module.equals(mod)) {
throw KEMException.criticalError("Invalid module specified for rewriting. Haskell backend only supports rewriting over" +
" the definition's main module.");
}
return mod;
}


private String saveKoreDefinitionToTemp(ModuleToKORE converter) {
String kompiledString = KoreBackend.getKompiledString(converter, files, false, tool);
files.saveToTemp("vdefinition.kore", kompiledString);
Expand All @@ -127,7 +284,7 @@ private String saveKoreDefinitionToTemp(ModuleToKORE converter) {
private String saveKoreSpecToTemp(ModuleToKORE converter, Module rules) {
StringBuilder sb = new StringBuilder();
String koreOutput = converter.convertSpecificationModule(module, rules,
ModuleToKORE.SentenceType.ALL_PATH, sb);
haskellKRunOptions.defaultClaimType, sb);
files.saveToTemp("spec.kore", koreOutput);
String specPath = files.resolveTemp("spec.kore").getAbsolutePath();
return specPath;
Expand All @@ -136,10 +293,12 @@ private String saveKoreSpecToTemp(ModuleToKORE converter, Module rules) {
private List<String> buildCommonProvingCommand(String defPath, String specPath, String outPath,
String defModuleName, String specModuleName){
String[] koreCommand;
if (kProveOptions.debugger) {
if (kProveOptions.debugger && !haskellKRunOptions.haskellBackendCommand.equals("kore-exec")) {
throw KEMException.criticalError("Cannot pass --debugger with --haskell-backend-command.");
} else if (kProveOptions.debugger) {
koreCommand = "kore-repl".split("\\s+");
} else {
koreCommand = "kore-exec".split("\\s+");
koreCommand = haskellKRunOptions.haskellBackendCommand.split("\\s+");
}

List<String> args = new ArrayList<>();
Expand Down Expand Up @@ -195,7 +354,7 @@ public RewriterResult prove(Module rules, Boolean reuseDef) {
String specPath = saveKoreSpecToTemp(converter, rules);
File koreOutputFile = files.resolveTemp("result.kore");

String koreDirectory = System.getenv("KORE_HOME");
String koreDirectory = haskellKRunOptions.haskellBackendHome;

String defModuleName = def.executionModule().name();
String specModuleName = kProveOptions.specModule == null ? rules.name() : kProveOptions.specModule;
Expand Down
27 changes: 27 additions & 0 deletions kernel/src/main/java/org/kframework/main/AbstractKModule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,33 @@ public List<Module> getKastModules() {
return Lists.newArrayList();
}

@Override
public List<Module> getKRunModules() {
return Lists.newArrayList(new AbstractModule() {

@Override
protected void configure() {
bindOptions(AbstractKModule.this::krunOptions, binder());
}
});
}

@Override
public List<Module> getKEqModules(List<Module> definitionSpecificModules) {
return Lists.newArrayList();
}

@Override
public List<Module> getDefinitionSpecificKEqModules() {
return Lists.newArrayList(new AbstractModule() {

@Override
protected void configure() {
//bind backend implementations of tools to their interfaces
}
});
}

@Override
public List<Module> getKProveModules() {
return Lists.newArrayList(new AbstractModule() {
Expand Down
3 changes: 3 additions & 0 deletions kernel/src/main/java/org/kframework/main/KModule.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,5 +9,8 @@ public interface KModule {

List<Module> getKompileModules();
List<Module> getKastModules();
List<Module> getKRunModules();
List<Module> getKEqModules(List<Module> definitionSpecificModules);
List<Module> getDefinitionSpecificKEqModules();
List<Module> getKProveModules();
}

0 comments on commit 8d0513c

Please sign in to comment.