From 5349a089e5bb6905eaca1a09e2b587488f8e4715 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Sun, 15 Jan 2023 20:00:10 +0000 Subject: [PATCH] feat: add --target flag for LLVM backend to build objects of a different 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 * chore: normalize indentation in src/util/shell.cpp * chore: strip trailing whitespace Co-authored-by: Sebastian Ullrich --- src/Lean/Compiler/IR/EmitLLVM.lean | 9 ++++++--- src/Lean/Compiler/IR/LLVMBindings.lean | 4 ++-- src/library/compiler/llvm.cpp | 18 +++++++++++++----- src/util/shell.cpp | 24 ++++++++++++++++++++++-- 4 files changed, 43 insertions(+), 12 deletions(-) diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean index 3a2e87015e..3d2d65c2b6 100644 --- a/src/Lean/Compiler/IR/EmitLLVM.lean +++ b/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 := "" diff --git a/src/Lean/Compiler/IR/LLVMBindings.lean b/src/Lean/Compiler/IR/LLVMBindings.lean index 8e6a2aad53..0d95a5faa7 100644 --- a/src/Lean/Compiler/IR/LLVMBindings.lean +++ b/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) diff --git a/src/library/compiler/llvm.cpp b/src/library/compiler/llvm.cpp index 8d7b8544cf..436def862b 100644 --- a/src/library/compiler/llvm.cpp +++ b/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 } diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 6d5590d413..39c1c84abf 100644 --- a/src/util/shell.cpp +++ b/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 c_output; optional llvm_output; + optional target_triple; optional root_dir; buffer 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((atoi(optarg) / 4) * 4) * static_cast(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' 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);