Allow calling `llvm-kompile` in `library` mode through `kompile` frontend

[ehildenb]

Firefly currently uses a separate invocation to kompile --no-llvm-kompile and llvm-kompile, because it needs to call llvm-kompile in library mode.

I suggest making library and main a boolean toggle, and search and execution a boolean toggle.

Also, if the -o SOME_FILE directory doesn't exist, llvm-kompile does not automatically create it. Can it?

[ehildenb]

The relevant code is here: https://github.com/kframework/k/blob/master/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java#L69

[ehildenb]

I have applied the following patch locally to try and make it work with Firefly:

diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
index 4bccf6a09..f219031de 100644
--- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
+++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
@@ -66,7 +66,7 @@ public class LLVMBackend extends KoreBackend {
         if (options.noLLVMKompile) {
             return;
         }
-        llvmKompile("main", "interpreter");
+        llvmKompile("library", "interpreter");
         if (options.enableSearch) {
           llvmKompile("search", "search");
         }

[ehildenb]

Also, it would be nice to have control over -o from the kompile command-line.

[ehildenb]

This is the final diff I had to use to make Firefly bulid-able with just kompile (instead of kompile --no-llvm-kompile followed by llvm-kompile).

diff --git a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
index 4bccf6a09..66f535278 100644
--- a/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
+++ b/llvm-backend/src/main/java/org/kframework/backend/llvm/LLVMBackend.java
@@ -66,7 +66,7 @@ public class LLVMBackend extends KoreBackend {
         if (options.noLLVMKompile) {
             return;
         }
-        llvmKompile("main", "interpreter");
+        llvmKompile("library", "interpreter");
         if (options.enableSearch) {
           llvmKompile("search", "search");
         }
@@ -79,8 +79,6 @@ public class LLVMBackend extends KoreBackend {
         args.add("definition.kore");
         args.add("dt");
         args.add(type);
-        args.add("-o");
-        args.add(executable);
         if (kompileOptions.optimize1) args.add("-O1");
         if (kompileOptions.optimize2) args.add("-O2");
         if (kompileOptions.optimize3) args.add("-O2"); // clang -O3 does not make the llvm backend any faster

I had to disable -o, so I could pass it manually. Note that I had to pass -o relative to the *-kompiled directory, which is not very ergonomic. It would be better to pass it relative to the working directory. I wanted to say (in the Firefly Makefile) -ccopt -o -ccopt $@, but I had to say -ccopt -o -ccopt $(notdir $@).

Also note that I'm changing the build to library manually, because there isn't a way to make this switch from the kompile ... interface.

[ehildenb]

Maybe we can autogenerate the cmake file so that I can still do kompile --no-llvm-kompile, but then do k-generate-cmake ALL_THE_ARGUMENTS_I_WOULD_PASS_TO_LLVM_KOMPILE? Then llvm-kompile.