Add extra options for kompiling to haskell (#2652)

* Add extra options for kompiling to haskell --haskell-backend-command --no-haskell-binary * Fix installation Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · Jun 11, 2022 · 84dcd0c · 84dcd0c
1 parent 0bacf0a
commit 84dcd0c
Show file tree

Hide file tree

Showing 7 changed files with 52 additions and 15 deletions.
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackend.java
@@ -5,7 +5,6 @@
 import org.kframework.attributes.Att;
 import org.kframework.backend.kore.KoreBackend;
 import org.kframework.compile.Backend;
-import org.kframework.kompile.CompiledDefinition;
 import org.kframework.kompile.KompileOptions;
 import org.kframework.main.Tool;
 import org.kframework.utils.errorsystem.KExceptionManager;
@@ -26,15 +25,18 @@ public class HaskellBackend extends KoreBackend {
 
     private final KompileOptions kompileOptions;
     private final FileUtil files;
+    private final HaskellKompileOptions haskellKompileOptions;
 
     @Inject
     public HaskellBackend(
             KompileOptions kompileOptions,
+            HaskellKompileOptions haskellKompileOptions,
             FileUtil files,
             KExceptionManager kem,
             Tool tool) {
         super(kompileOptions, files, kem, EnumSet.of(HEAT_RESULT, COOL_RESULT_CONDITION), false, tool);
         this.files = files;
+        this.haskellKompileOptions = haskellKompileOptions;
         this.kompileOptions = kompileOptions;
     }
 
@@ -46,13 +48,19 @@ public void accept(Backend.Holder h) {
         files.saveToKompiled("definition.kore", kore);
         ProcessBuilder pb = files.getProcessBuilder();
         List<String> args = new ArrayList<>();
-        args.add("kore-exec");
-        args.add("definition.kore");
-        args.add("--module");
-        args.add(kompileOptions.mainModule(files));
-        args.add("--output");
-        args.add("haskellDefinition.bin");
-        args.add("--serialize");
+        if (haskellKompileOptions.noHaskellBinary) {
+            args.add("kore-parser");
+            args.add("--no-print-definition");
+            args.add("definition.kore");
+        } else {
+            args.add(haskellKompileOptions.haskellBackendCommand);
+            args.add("definition.kore");
+            args.add("--module");
+            args.add(kompileOptions.mainModule(files));
+            args.add("--output");
+            args.add("haskellDefinition.bin");
+            args.add("--serialize");
+        }
         try {
           Process p = pb.command(args).directory(files.resolveKompiled(".")).inheritIO().start();
           int exit = p.waitFor();

diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellBackendKModule.java
@@ -26,6 +26,7 @@ public List<Module> getKompileModules() {
         mods.add(new AbstractModule() {
             @Override
             protected void configure() {
+                bindOptions(HaskellBackendKModule.this::kompileOptions, binder());
                 installHaskellBackend(binder());
             }
         });
@@ -43,6 +44,11 @@ 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() {

diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellKompileOptions.java
@@ -0,0 +1,15 @@
+// Copyright (c) 2014-2019 K Team. All Rights Reserved.
+package org.kframework.backend.haskell;
+
+import com.beust.jcommander.Parameter;
+import org.kframework.utils.inject.RequestScoped;
+
+@RequestScoped
+public class HaskellKompileOptions {
+
+    @Parameter(names="--haskell-backend-command", description="Command to run the Haskell backend execution engine.")
+    public String haskellBackendCommand = "kore-exec";
+
+    @Parameter(names="--no-haskell-binary", description="Do not force the haskell backend to use the binary format. Use the textual format instead. This is a development option. Sometime the binary format can cause issues.")
+    public boolean noHaskellBinary = false;
+}
diff --git a/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java b/haskell-backend/src/main/java/org/kframework/backend/haskell/HaskellRewriter.java
@@ -111,7 +111,9 @@ public RewriterResult execute(K k, Optional<Integer> depth) {
                 Module mod = getExecutionModule(module);
                 ModuleToKORE converter = new ModuleToKORE(mod, def.topCellInitializer, kompileOptions);
                 String koreOutput = getKoreString(k, mod, converter);
-                String defPath = files.resolveKompiled("haskellDefinition.bin").getAbsolutePath();
+                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);
@@ -191,7 +193,9 @@ public K search(K initialConfiguration, Optional<Integer> depth, Optional<Intege
                         + patternTermKore
                         + ", " + patternConditionKore
                         + ")";
-                String defPath = files.resolveKompiled("haskellDefinition.bin").getAbsolutePath();
+                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);

diff --git a/k-distribution/src/main/scripts/bin/krun b/k-distribution/src/main/scripts/bin/krun
@@ -566,6 +566,11 @@ elif [ "$backendName" = "haskell" ] ; then
   # Haskell backend
   koreExecFlags=
   depthFlags=
+  defFile="definition.kore"
+  if [ -f "$kompiledDir/haskellDefinition.bin" ]; then
+    defFile="haskellDefinition.bin"
+  fi
+
   if [ -n "$depth" ]; then
     depthFlags="--depth $depth"
   fi
@@ -589,7 +594,7 @@ elif [ "$backendName" = "haskell" ] ; then
       tempFiles+=("$final_input")
       keepTempsIfDryRun "$tempDir" "$final_input" "$expanded_input_file" "$kore_output"
       set +e
-      execute $cmdprefix "$haskellCmd" "$kompiledDir/haskellDefinition.bin" --module "$mainModuleName" --pattern "$expanded_input_file" --output "$final_input" $koreExecFlags
+      execute $cmdprefix "$haskellCmd" "$kompiledDir/$defFile" --module "$mainModuleName" --pattern "$expanded_input_file" --output "$final_input" $koreExecFlags
       set -e
       depthFlags="--depth 0"
     else
@@ -601,13 +606,13 @@ elif [ "$backendName" = "haskell" ] ; then
     fi
     keepTempsIfDryRun "$tempDir" "$final_input" "$patternFile" "$kore_output"
     set +e
-    execute $cmdprefix "$haskellCmd" "$kompiledDir/haskellDefinition.bin" --module "$mainModuleName" --pattern "$final_input" --output "$kore_output" --searchType "$searchType" --search "$patternFile" $koreExecFlags $depthFlags
+    execute $cmdprefix "$haskellCmd" "$kompiledDir/$defFile" --module "$mainModuleName" --pattern "$final_input" --output "$kore_output" --searchType "$searchType" --search "$patternFile" $koreExecFlags $depthFlags
     result=$?
     set -e
   else
     keepTempsIfDryRun "$tempDir" "$expanded_input_file" "$kore_output"
     set +e
-    execute $cmdprefix "$haskellCmd" "$kompiledDir/haskellDefinition.bin" --module "$mainModuleName" --pattern "$expanded_input_file" --output "$kore_output" $koreExecFlags $depthFlags
+    execute $cmdprefix "$haskellCmd" "$kompiledDir/$defFile" --module "$mainModuleName" --pattern "$expanded_input_file" --output "$kore_output" $koreExecFlags $depthFlags
     result=$?
     set -e
   fi

diff --git a/k-distribution/tests/regression-new/imp-haskell/Makefile b/k-distribution/tests/regression-new/imp-haskell/Makefile
@@ -2,6 +2,7 @@ DEF=imp
 EXT=imp
 TESTDIR=.
 KOMPILE_BACKEND=haskell
+KOMPILE_FLAGS=--no-haskell-binary
 KPROVE_FLAGS=--def-module VERIFICATION
 export KOMPILE_BACKEND
 export KPROVE_FLAGS

diff --git a/kernel/src/main/java/org/kframework/kompile/KompileOptions.java b/kernel/src/main/java/org/kframework/kompile/KompileOptions.java
@@ -50,8 +50,6 @@ GlobalOptions getGlobalOptions_UseOnlyInGuiceProvider() {
     @Parameter(names="--backend", description="Choose a backend. <backend> is one of [llvm|haskell|kore|java]. Each creates the kompiled K definition.")
     public String backend = Backends.LLVM;
 
-    private boolean kore;
-
     @Parameter(names="--main-module", description="Specify main module in which a program starts to execute. This information is used by 'krun'. The default is the name of the given K definition file without the extension (.k).")
     private String mainModule;