feat: add --target flag for LLVM backend to build objects of a differ…

…ent architecture (#2034)

* feat: add --target flag for LLVM backend to build objects of a different architecture

* chore: remove dead comment

* Update src/Lean/Compiler/IR/EmitLLVM.lean

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* chore: normalize indentation in src/util/shell.cpp

* chore: strip trailing whitespace

Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -1505,9 +1505,12 @@ def optimizeLLVMModule (mod : LLVM.Module ctx) : IO Unit := do
   LLVM.disposePassManager pm
   LLVM.disposePassManagerBuilder pmb
 
+/--
+`emitLLVM` is the entrypoint for the lean shell to code generate LLVM.
+-/
 @[export lean_ir_emit_llvm]
-def emitLLVM (env : Environment) (modName : Name) (filepath : String) : IO Unit := do
-  LLVM.llvmInitialize
+def emitLLVM (env : Environment) (modName : Name) (filepath : String) (tripleStr? : Option String) : IO Unit := do
+  LLVM.llvmInitializeTargetInfo
   let llvmctx ← LLVM.createContext
   let module ← LLVM.createModule llvmctx modName.toString
   let emitLLVMCtx : EmitLLVM.Context llvmctx := {env := env, modName := modName, llvmmodule := module}
@@ -1520,7 +1523,7 @@ def emitLLVM (env : Environment) (modName : Name) (filepath : String) : IO Unit
          LLVM.linkModules (dest := emitLLVMCtx.llvmmodule) (src := modruntime)
          optimizeLLVMModule emitLLVMCtx.llvmmodule
          LLVM.writeBitcodeToFile emitLLVMCtx.llvmmodule filepath
-         let tripleStr ← LLVM.getDefaultTargetTriple
+         let tripleStr := tripleStr?.getD (← LLVM.getDefaultTargetTriple)
          let target ← LLVM.getTargetFromTriple tripleStr
          let cpu := "generic"
          let features := ""

src/Lean/Compiler/IR/LLVMBindings.lean

@@ -73,8 +73,8 @@ structure Value (ctx : Context) where
   private mk :: ptr : USize
 instance : Nonempty (Value ctx) := ⟨{ ptr := default }⟩
 
-@[extern "lean_llvm_initialize"]
-opaque llvmInitialize : BaseIO (Unit)
+@[extern "lean_llvm_initialize_target_info"]
+opaque llvmInitializeTargetInfo : BaseIO (Unit)
 
 @[extern "lean_llvm_create_context"]
 opaque createContext : BaseIO (Context)

src/library/compiler/llvm.cpp

@@ -29,12 +29,14 @@ Lean's IR.
 #include "llvm-c/Transforms/PassManagerBuilder.h"
 #endif
 
-extern "C" LEAN_EXPORT lean_object* lean_llvm_initialize() {
+extern "C" LEAN_EXPORT lean_object* lean_llvm_initialize_target_info() {
 
 #ifdef LEAN_LLVM
-    LLVMInitializeNativeTarget();
-    LLVMInitializeNativeAsmParser();
-    LLVMInitializeNativeAsmPrinter();
+    LLVMInitializeAllTargetInfos();
+    LLVMInitializeAllTargets();
+    LLVMInitializeAllTargetMCs();
+    LLVMInitializeAllAsmParsers();
+    LLVMInitializeAllAsmPrinters();
 #endif
 
     return lean_io_result_mk_ok(lean_box(0));
@@ -1117,6 +1119,13 @@ extern "C" LEAN_EXPORT lean_object *lean_llvm_get_target_from_triple(size_t ctx,
     char *errmsg = NULL;
     int is_error =
         LLVMGetTargetFromTriple(lean_string_cstr(triple), &t, &errmsg);
+    if (is_error) {
+        fprintf(stderr, "Unable to find target '%s'. Registered targets:\n", lean_string_cstr(triple));
+        for(LLVMTargetRef t = LLVMGetFirstTarget();  t != NULL; t = LLVMGetNextTarget(t)) {
+            fprintf(stderr, "    %-10s - %s\n", LLVMGetTargetName(t), LLVMGetTargetDescription(t));
+        }
+    }
+
     lean_always_assert(!is_error && "failed to get target from triple");
     return lean_io_result_mk_ok(lean_box_usize(Target_to_lean(t)));
 #endif  // LEAN_LLVM
@@ -1156,7 +1165,6 @@ extern "C" LEAN_EXPORT lean_object *lean_llvm_target_machine_emit_to_file(size_t
         lean_to_TargetMachine(target_machine), lean_to_Module(module),
         filepath_c_str, LLVMCodeGenFileType(codegenType), &err_msg);
 
-
     return lean_io_result_mk_ok(lean_box(0));
 #endif  // LEAN_LLVM
 }

src/util/shell.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "runtime/sstream.h"
 #include "runtime/load_dynlib.h"
 #include "runtime/array_ref.h"
+#include "runtime/object_ref.h"
 #include "util/timer.h"
 #include "util/macros.h"
 #include "util/io.h"
@@ -172,7 +173,7 @@ using namespace lean; // NOLINT
 extern "C" void *initialize_Lean_Compiler_IR_EmitLLVM(uint8_t builtin,
                                                       lean_object *);
 extern "C" object *lean_ir_emit_llvm(object *env, object *mod_name,
-                                     object *filepath, object *w);
+                                     object *filepath, object *target_triple, object *w);
 
 static void display_header(std::ostream & out) {
     out << "Lean (version " << get_version_string() << ", " << LEAN_STR(LEAN_BUILD_TYPE) << ")\n";
@@ -198,6 +199,7 @@ static void display_help(std::ostream & out) {
     std::cout << "  --i=iname -i       create ilean file\n";
     std::cout << "  --c=fname -c       name of the C output file\n";
     std::cout << "  --bc=fname -b      name of the LLVM bitcode file\n";
+    std::cout << "  --target=target    target triple of object file produced by LLVM\n";
     std::cout << "  --stdin            take input from stdin\n";
     std::cout << "  --root=dir         set package root directory from which the module name of the input file is calculated\n"
               << "                     (default: current working directory)\n";
@@ -249,6 +251,7 @@ static struct option g_long_options[] = {
     {"timeout",      optional_argument, 0, 'T'},
     {"c",            optional_argument, 0, 'c'},
     {"bc",           optional_argument, 0, 'b'},
+    {"target",       optional_argument, 0, '3'},
     {"features",     optional_argument, 0, 'f'},
     {"exitOnPanic",  no_argument,       0, 'e'},
 #if defined(LEAN_MULTI_THREAD)
@@ -486,6 +489,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
     std::string native_output;
     optional<std::string> c_output;
     optional<std::string> llvm_output;
+    optional<std::string> target_triple;
     optional<std::string> root_dir;
     buffer<string_ref> forwarded_args;
 
@@ -523,6 +527,10 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
                 check_optarg("b");
                 llvm_output = optarg;
                 break;
+            case '3':
+                check_optarg("target");
+                target_triple = optarg;
+                break;
             case 's':
                 lean::lthread::set_thread_stack_size(
                         static_cast<size_t>((atoi(optarg) / 4) * 4) * static_cast<size_t>(1024));
@@ -744,13 +752,25 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
             out.close();
         }
 
+        // target triple is only used by the LLVM backend. Save users
+        // a great deal of pain by erroring out if they misuse flags.
+        if (target_triple && !llvm_output) {
+            std::cerr << "ERROR: '--target' must be used with '--bc' to enable LLVM backend. Quitting code generation.\n";
+            return 1;
+        }
+
         if (llvm_output && ok) {
+	        // marshal 'optional<string>' to 'lean_object*'
+            lean_object* const target_triple_lean =
+                target_triple ? mk_option_some(lean::string_ref(*target_triple).to_obj_arg()) : mk_option_none();
             initialize_Lean_Compiler_IR_EmitLLVM(/*builtin*/ false,
                     lean_io_mk_world());
             time_task _("LLVM code generation", opts);
             lean::consume_io_result(lean_ir_emit_llvm(
                         env.to_obj_arg(), (*main_module_name).to_obj_arg(),
-                        lean::string_ref(*llvm_output).to_obj_arg(), lean_io_mk_world()));
+                        lean::string_ref(*llvm_output).to_obj_arg(),
+                        target_triple_lean,
+                        lean_io_mk_world()));
         }
 
         display_cumulative_profiling_times(std::cerr);