Skip to content

Commit 5349a08

Browse files
bolluKha
bollu
and
Kha
authored
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>
1 parent 26edfc3 commit 5349a08

4 files changed

Lines changed: 43 additions & 12 deletions

File tree

‎src/Lean/Compiler/IR/EmitLLVM.lean‎

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1505,9 +1505,12 @@ def optimizeLLVMModule (mod : LLVM.Module ctx) : IO Unit := do
15051505
LLVM.disposePassManager pm
15061506
LLVM.disposePassManagerBuilder pmb
15071507

1508+
/--
1509+
`emitLLVM` is the entrypoint for the lean shell to code generate LLVM.
1510+
-/
15081511
@[export lean_ir_emit_llvm]
1509-
def emitLLVM (env : Environment) (modName : Name) (filepath : String) : IO Unit := do
1510-
LLVM.llvmInitialize
1512+
def emitLLVM (env : Environment) (modName : Name) (filepath : String) (tripleStr? : Option String) : IO Unit := do
1513+
LLVM.llvmInitializeTargetInfo
15111514
let llvmctx ← LLVM.createContext
15121515
let module ← LLVM.createModule llvmctx modName.toString
15131516
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
15201523
LLVM.linkModules (dest := emitLLVMCtx.llvmmodule) (src := modruntime)
15211524
optimizeLLVMModule emitLLVMCtx.llvmmodule
15221525
LLVM.writeBitcodeToFile emitLLVMCtx.llvmmodule filepath
1523-
let tripleStr ← LLVM.getDefaultTargetTriple
1526+
let tripleStr := tripleStr?.getD (← LLVM.getDefaultTargetTriple)
15241527
let target ← LLVM.getTargetFromTriple tripleStr
15251528
let cpu := "generic"
15261529
let features := ""

‎src/Lean/Compiler/IR/LLVMBindings.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -73,8 +73,8 @@ structure Value (ctx : Context) where
7373
private mk :: ptr : USize
7474
instance : Nonempty (Value ctx) := ⟨{ ptr := default }⟩
7575

76-
@[extern "lean_llvm_initialize"]
77-
opaque llvmInitialize : BaseIO (Unit)
76+
@[extern "lean_llvm_initialize_target_info"]
77+
opaque llvmInitializeTargetInfo : BaseIO (Unit)
7878

7979
@[extern "lean_llvm_create_context"]
8080
opaque createContext : BaseIO (Context)

‎src/library/compiler/llvm.cpp‎

Lines changed: 13 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -29,12 +29,14 @@ Lean's IR.
2929
#include "llvm-c/Transforms/PassManagerBuilder.h"
3030
#endif
3131

32-
extern "C" LEAN_EXPORT lean_object* lean_llvm_initialize() {
32+
extern "C" LEAN_EXPORT lean_object* lean_llvm_initialize_target_info() {
3333

3434
#ifdef LEAN_LLVM
35-
LLVMInitializeNativeTarget();
36-
LLVMInitializeNativeAsmParser();
37-
LLVMInitializeNativeAsmPrinter();
35+
LLVMInitializeAllTargetInfos();
36+
LLVMInitializeAllTargets();
37+
LLVMInitializeAllTargetMCs();
38+
LLVMInitializeAllAsmParsers();
39+
LLVMInitializeAllAsmPrinters();
3840
#endif
3941

4042
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,
11171119
char *errmsg = NULL;
11181120
int is_error =
11191121
LLVMGetTargetFromTriple(lean_string_cstr(triple), &t, &errmsg);
1122+
if (is_error) {
1123+
fprintf(stderr, "Unable to find target '%s'. Registered targets:\n", lean_string_cstr(triple));
1124+
for(LLVMTargetRef t = LLVMGetFirstTarget(); t != NULL; t = LLVMGetNextTarget(t)) {
1125+
fprintf(stderr, " %-10s - %s\n", LLVMGetTargetName(t), LLVMGetTargetDescription(t));
1126+
}
1127+
}
1128+
11201129
lean_always_assert(!is_error && "failed to get target from triple");
11211130
return lean_io_result_mk_ok(lean_box_usize(Target_to_lean(t)));
11221131
#endif // LEAN_LLVM
@@ -1156,7 +1165,6 @@ extern "C" LEAN_EXPORT lean_object *lean_llvm_target_machine_emit_to_file(size_t
11561165
lean_to_TargetMachine(target_machine), lean_to_Module(module),
11571166
filepath_c_str, LLVMCodeGenFileType(codegenType), &err_msg);
11581167

1159-
11601168
return lean_io_result_mk_ok(lean_box(0));
11611169
#endif // LEAN_LLVM
11621170
}

‎src/util/shell.cpp‎

Lines changed: 22 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,6 +21,7 @@ Author: Leonardo de Moura
2121
#include "runtime/sstream.h"
2222
#include "runtime/load_dynlib.h"
2323
#include "runtime/array_ref.h"
24+
#include "runtime/object_ref.h"
2425
#include "util/timer.h"
2526
#include "util/macros.h"
2627
#include "util/io.h"
@@ -172,7 +173,7 @@ using namespace lean; // NOLINT
172173
extern "C" void *initialize_Lean_Compiler_IR_EmitLLVM(uint8_t builtin,
173174
lean_object *);
174175
extern "C" object *lean_ir_emit_llvm(object *env, object *mod_name,
175-
object *filepath, object *w);
176+
object *filepath, object *target_triple, object *w);
176177

177178
static void display_header(std::ostream & out) {
178179
out << "Lean (version " << get_version_string() << ", " << LEAN_STR(LEAN_BUILD_TYPE) << ")\n";
@@ -198,6 +199,7 @@ static void display_help(std::ostream & out) {
198199
std::cout << " --i=iname -i create ilean file\n";
199200
std::cout << " --c=fname -c name of the C output file\n";
200201
std::cout << " --bc=fname -b name of the LLVM bitcode file\n";
202+
std::cout << " --target=target target triple of object file produced by LLVM\n";
201203
std::cout << " --stdin take input from stdin\n";
202204
std::cout << " --root=dir set package root directory from which the module name of the input file is calculated\n"
203205
<< " (default: current working directory)\n";
@@ -249,6 +251,7 @@ static struct option g_long_options[] = {
249251
{"timeout", optional_argument, 0, 'T'},
250252
{"c", optional_argument, 0, 'c'},
251253
{"bc", optional_argument, 0, 'b'},
254+
{"target", optional_argument, 0, '3'},
252255
{"features", optional_argument, 0, 'f'},
253256
{"exitOnPanic", no_argument, 0, 'e'},
254257
#if defined(LEAN_MULTI_THREAD)
@@ -486,6 +489,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
486489
std::string native_output;
487490
optional<std::string> c_output;
488491
optional<std::string> llvm_output;
492+
optional<std::string> target_triple;
489493
optional<std::string> root_dir;
490494
buffer<string_ref> forwarded_args;
491495

@@ -523,6 +527,10 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
523527
check_optarg("b");
524528
llvm_output = optarg;
525529
break;
530+
case '3':
531+
check_optarg("target");
532+
target_triple = optarg;
533+
break;
526534
case 's':
527535
lean::lthread::set_thread_stack_size(
528536
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) {
744752
out.close();
745753
}
746754

755+
// target triple is only used by the LLVM backend. Save users
756+
// a great deal of pain by erroring out if they misuse flags.
757+
if (target_triple && !llvm_output) {
758+
std::cerr << "ERROR: '--target' must be used with '--bc' to enable LLVM backend. Quitting code generation.\n";
759+
return 1;
760+
}
761+
747762
if (llvm_output && ok) {
763+
// marshal 'optional<string>' to 'lean_object*'
764+
lean_object* const target_triple_lean =
765+
target_triple ? mk_option_some(lean::string_ref(*target_triple).to_obj_arg()) : mk_option_none();
748766
initialize_Lean_Compiler_IR_EmitLLVM(/*builtin*/ false,
749767
lean_io_mk_world());
750768
time_task _("LLVM code generation", opts);
751769
lean::consume_io_result(lean_ir_emit_llvm(
752770
env.to_obj_arg(), (*main_module_name).to_obj_arg(),
753-
lean::string_ref(*llvm_output).to_obj_arg(), lean_io_mk_world()));
771+
lean::string_ref(*llvm_output).to_obj_arg(),
772+
target_triple_lean,
773+
lean_io_mk_world()));
754774
}
755775

756776
display_cumulative_profiling_times(std::cerr);

0 commit comments

Comments
 (0)