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 <sebasti@nullri.ch> * chore: normalize indentation in src/util/shell.cpp * chore: strip trailing whitespace Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
This commit is contained in:
Siddharth
GitHub
parent
26edfc33f5
commit
5349a089e5
4 changed files with 43 additions and 12 deletions
|
|
@ -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 := ""
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue