From 06f73d621b30f42e22c2b2ca8d6d797689430738 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Tue, 13 Feb 2024 11:57:35 +0100 Subject: [PATCH] fix: type mismatches in the LLVM backend (#3225) Debugged and authored in collaboration with @bollu. This PR fixes several performance regressions of the LLVM backend compared to the C backend as described in #3192. We are now at the point where some benchmarks from `tests/bench` achieve consistently equal and sometimes ever so slightly better performance when using LLVM instead of C. However there are still a few testcases where we are lacking behind ever so slightly. The PR contains two changes: 1. Using the same types for `lean.h` runtime functions in the LLVM backend as in `lean.h` it turns out that: a) LLVM does not throw an error if we declare a function with a different type than it actually has. This happened on multiple occasions here, in particular when the function used `unsigned`, as it was wrongfully assumed to be `size_t` sized. b) Refuses to inline a function to the call site if such a type mismatch occurs. This means that we did not inline important functionality such as `lean_ctor_set` and were thus slowed down compared to the C backend which did this correctly. 2. While developing this change we noticed that LLVM does treat the following as invalid: Having a function declared with a certain type but called with integers of a different type. However this will manifest in completely nonsensical errors upon optimizing the bitcode file through `leanc` such as: ``` error: Invalid record (Producer: 'LLVM15.0.7' Reader: 'LLVM 15.0.7') ``` Presumably because the generate .bc file is invalid in the first place. Thus we added a call to `LLVMVerifyModule` before serializing the module into a bitcode file. This ended producing the expected type errors from LLVM an aborting the bitcode file generation as expected. We manually checked each function in `lean.h` that is mentioned in `EmitLLVM.lean` to make sure that all of their types align correctly now. Quick overview of the fast benchmarks as measured on my machine, 2 runs of LLVM and 2 runs of C to get a feeling for how far the averages move: - binarytrees: basically equal performance - binarytrees.st: basically equal performance - const_fold: equal if not slightly better for LLVM - deriv: LLVM has 8% more instructions than C but same wall clock time - liasolver: basically equal performance - qsort: LLVM is slower by 7% instructions, 4% time. We have identified why the generated code is slower (there is a store/load in a hot loop in LLVM that is not in C) but not figured out why that happens/how to address it. - rbmap: LLVM has 3% less instructions and 13% less wall-clock time than C (woop woop) - rbmap_1 and rbmap_10 show similar behavior - rbmap_fbip: LLVM has 2% more instructions but 2% better wall time - rbmap_library: equal if not slightly better for LLVM - unionfind: LLVM has 5% more instructions but 4% better wall time Leaving out benchmarks related to the compiler itself as I was too lazy to keep recompiling it from scratch until we are on a level with C. Summing things up, it appears that LLVM has now caught up or surpassed the C backend in the microbenchmarks for the most part. Next steps from our side are: - trying to win the qsort benchmark - figuring out why/how LLVM runs more instructions for less wall-clock time. My current guesses would be measurement noise and/or better use of micro architecture? - measuring the larger benchmarks as well --- src/Lean/Compiler/IR/EmitLLVM.lean | 89 +++++++++++++++----------- src/Lean/Compiler/IR/LLVMBindings.lean | 10 ++- src/library/compiler/llvm.cpp | 18 ++++++ 3 files changed, 79 insertions(+), 38 deletions(-) diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean index 0a079d3972..dc355a2dd7 100644 --- a/src/Lean/Compiler/IR/EmitLLVM.lean +++ b/src/Lean/Compiler/IR/EmitLLVM.lean @@ -25,9 +25,13 @@ def leanMainFn := "_lean_main" namespace LLVM -- TODO(bollu): instantiate target triple and find out what size_t is. -def size_tType (llvmctx : LLVM.Context) : IO (LLVM.LLVMType llvmctx) := +def size_tType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx) := LLVM.i64Type llvmctx +-- TODO(bollu): instantiate target triple and find out what unsigned is. +def unsignedType (llvmctx : LLVM.Context) : BaseIO (LLVM.LLVMType llvmctx) := + LLVM.i32Type llvmctx + -- Helper to add a function if it does not exist, and to return the function handle if it does. def getOrAddFunction (m : LLVM.Module ctx) (name : String) (type : LLVM.LLVMType ctx) : BaseIO (LLVM.Value ctx) := do match (← LLVM.getNamedFunction m name) with @@ -96,6 +100,15 @@ def getDecl (n : Name) : M llvmctx Decl := do | some d => pure d | none => throw s!"unknown declaration {n}" +def constInt8 (n : Nat) : M llvmctx (LLVM.Value llvmctx) := do + LLVM.constInt8 llvmctx (UInt64.ofNat n) + +def constInt64 (n : Nat) : M llvmctx (LLVM.Value llvmctx) := do + LLVM.constInt64 llvmctx (UInt64.ofNat n) + +def constIntSizeT (n : Nat) : M llvmctx (LLVM.Value llvmctx) := do + LLVM.constIntSizeT llvmctx (UInt64.ofNat n) + def constIntUnsigned (n : Nat) : M llvmctx (LLVM.Value llvmctx) := do LLVM.constIntUnsigned llvmctx (UInt64.ofNat n) @@ -162,14 +175,14 @@ def callLeanUnsignedToNatFn (builder : LLVM.Builder llvmctx) let retty ← LLVM.voidPtrType llvmctx let f ← getOrCreateFunctionPrototype mod retty "lean_unsigned_to_nat" argtys let fnty ← LLVM.functionType retty argtys - let nv ← LLVM.constInt32 llvmctx (UInt64.ofNat n) + let nv ← constIntUnsigned n LLVM.buildCall2 builder fnty f #[nv] name def callLeanMkStringFromBytesFn (builder : LLVM.Builder llvmctx) (strPtr nBytes : LLVM.Value llvmctx) (name : String) : M llvmctx (LLVM.Value llvmctx) := do let fnName := "lean_mk_string_from_bytes" let retty ← LLVM.voidPtrType llvmctx - let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.i64Type llvmctx] + let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys LLVM.buildCall2 builder fnty fn #[strPtr, nBytes] name @@ -218,9 +231,9 @@ def callLeanAllocCtor (builder : LLVM.Builder llvmctx) let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys - let tag ← LLVM.constInt32 llvmctx (UInt64.ofNat tag) - let num_objs ← LLVM.constInt32 llvmctx (UInt64.ofNat num_objs) - let scalar_sz ← LLVM.constInt32 llvmctx (UInt64.ofNat scalar_sz) + let tag ← constIntUnsigned tag + let num_objs ← constIntUnsigned num_objs + let scalar_sz ← constIntUnsigned scalar_sz LLVM.buildCall2 builder fnty fn #[tag, num_objs, scalar_sz] name def callLeanCtorSet (builder : LLVM.Builder llvmctx) @@ -228,7 +241,7 @@ def callLeanCtorSet (builder : LLVM.Builder llvmctx) let fnName := "lean_ctor_set" let retty ← LLVM.voidType llvmctx let voidptr ← LLVM.voidPtrType llvmctx - let unsigned ← LLVM.size_tType llvmctx + let unsigned ← LLVM.unsignedType llvmctx let argtys := #[voidptr, unsigned, voidptr] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys @@ -248,7 +261,7 @@ def callLeanAllocClosureFn (builder : LLVM.Builder llvmctx) (f arity nys : LLVM.Value llvmctx) (retName : String := "") : M llvmctx (LLVM.Value llvmctx) := do let fnName := "lean_alloc_closure" let retty ← LLVM.voidPtrType llvmctx - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.unsignedType llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys LLVM.buildCall2 builder fnty fn #[f, arity, nys] retName @@ -257,7 +270,7 @@ def callLeanClosureSetFn (builder : LLVM.Builder llvmctx) (closure ix arg : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do let fnName := "lean_closure_set" let retty ← LLVM.voidType llvmctx - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.voidPtrType llvmctx] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.voidPtrType llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys let _ ← LLVM.buildCall2 builder fnty fn #[closure, ix, arg] retName @@ -285,7 +298,7 @@ def callLeanCtorRelease (builder : LLVM.Builder llvmctx) (closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do let fnName := "lean_ctor_release" let retty ← LLVM.voidType llvmctx - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys let _ ← LLVM.buildCall2 builder fnty fn #[closure, i] retName @@ -294,7 +307,7 @@ def callLeanCtorSetTag (builder : LLVM.Builder llvmctx) (closure i : LLVM.Value llvmctx) (retName : String := "") : M llvmctx Unit := do let fnName := "lean_ctor_set_tag" let retty ← LLVM.voidType llvmctx - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.i8Type llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys let _ ← LLVM.buildCall2 builder fnty fn #[closure, i] retName @@ -428,7 +441,7 @@ def buildIfThenElse_ (builder : LLVM.Builder llvmctx) (name : String) (brval : -- Recall that lean uses `i8` for booleans, not `i1`, so we need to compare with `true`. def buildLeanBoolTrue? (builder : LLVM.Builder llvmctx) (b : LLVM.Value llvmctx) (name : String := "") : M llvmctx (LLVM.Value llvmctx) := do - LLVM.buildICmp builder LLVM.IntPredicate.NE b (← LLVM.constInt8 llvmctx 0) name + LLVM.buildICmp builder LLVM.IntPredicate.NE b (← constInt8 0) name def emitFnDeclAux (mod : LLVM.Module llvmctx) (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M llvmctx (LLVM.Value llvmctx) := do @@ -514,7 +527,7 @@ def emitArgSlot_ (builder : LLVM.Builder llvmctx) | _ => do let slotty ← LLVM.voidPtrType llvmctx let slot ← LLVM.buildAlloca builder slotty "irrelevant_slot" - let v ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "irrelevant_val" + let v ← callLeanBox builder (← constIntSizeT 0) "irrelevant_val" let _ ← LLVM.buildStore builder v slot return (slotty, slot) @@ -536,7 +549,7 @@ def emitCtorSetArgs (builder : LLVM.Builder llvmctx) ys.size.forM fun i => do let zv ← emitLhsVal builder z let (_yty, yv) ← emitArgVal builder ys[i]! - let iv ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat i) + let iv ← constIntUnsigned i callLeanCtorSet builder zv iv yv emitLhsSlotStore builder z zv pure () @@ -545,7 +558,7 @@ def emitCtor (builder : LLVM.Builder llvmctx) (z : VarId) (c : CtorInfo) (ys : Array Arg) : M llvmctx Unit := do let (_llvmty, slot) ← emitLhsSlot_ z if c.size == 0 && c.usize == 0 && c.ssize == 0 then do - let v ← callLeanBox builder (← constIntUnsigned c.cidx) "lean_box_outv" + let v ← callLeanBox builder (← constIntSizeT c.cidx) "lean_box_outv" let _ ← LLVM.buildStore builder v slot else do let v ← emitAllocCtor builder c @@ -557,7 +570,7 @@ def emitInc (builder : LLVM.Builder llvmctx) let xv ← emitLhsVal builder x if n != 1 then do - let nv ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat n) + let nv ← constIntSizeT n callLeanRefcountFn builder (kind := RefcountKind.inc) (checkRef? := checkRef?) (delta := nv) xv else callLeanRefcountFn builder (kind := RefcountKind.inc) (checkRef? := checkRef?) xv @@ -680,7 +693,7 @@ def emitApp (builder : LLVM.Builder llvmctx) (z : VarId) (f : VarId) (ys : Array let retty ← LLVM.voidPtrType llvmctx let args := #[← emitLhsVal builder f, ← constIntUnsigned ys.size, aargs] -- '1 + ...'. '1' for the fn and 'args' for the arguments - let argtys := #[← LLVM.voidPtrType llvmctx] + let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.voidPtrType llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys let zv ← LLVM.buildCall2 builder fnty fn args @@ -727,13 +740,13 @@ def emitLit (builder : LLVM.Builder llvmctx) let zv ← match v with | LitVal.num v => emitNumLit builder t v | LitVal.str v => - let zero ← LLVM.constIntUnsigned llvmctx 0 + let zero ← constIntUnsigned 0 let str_global ← LLVM.buildGlobalString builder v -- access through the global, into the 0th index of the array let strPtr ← LLVM.buildInBoundsGEP2 builder (← LLVM.opaquePointerTypeInContext llvmctx) str_global #[zero] "" - let nbytes ← LLVM.constIntUnsigned llvmctx (UInt64.ofNat (v.utf8ByteSize)) + let nbytes ← constIntSizeT v.utf8ByteSize callLeanMkStringFromBytesFn builder strPtr nbytes "" LLVM.buildStore builder zv zslot return zslot @@ -757,7 +770,7 @@ def callLeanCtorGetUsize (builder : LLVM.Builder llvmctx) (x i : LLVM.Value llvmctx) (retName : String) : M llvmctx (LLVM.Value llvmctx) := do let fnName := "lean_ctor_get_usize" let retty ← LLVM.size_tType llvmctx - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx] let fnty ← LLVM.functionType retty argtys let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys LLVM.buildCall2 builder fnty fn #[x, i] retName @@ -784,7 +797,7 @@ def emitSProj (builder : LLVM.Builder llvmctx) | IRType.uint32 => pure ("lean_ctor_get_uint32", ← LLVM.i32Type llvmctx) | IRType.uint64 => pure ("lean_ctor_get_uint64", ← LLVM.i64Type llvmctx) | _ => throw s!"Invalid type for lean_ctor_get: '{t}'" - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let xval ← emitLhsVal builder x let offset ← emitOffset builder n offset @@ -891,7 +904,7 @@ def emitReset (builder : LLVM.Builder llvmctx) (z : VarId) (n : Nat) (x : VarId) (fun builder => do let xv ← emitLhsVal builder x callLeanDecRef builder xv - let box0 ← callLeanBox builder (← constIntUnsigned 0) "box0" + let box0 ← callLeanBox builder (← constIntSizeT 0) "box0" emitLhsSlotStore builder z box0 return ShouldForwardControlFlow.yes ) @@ -912,7 +925,7 @@ def emitReuse (builder : LLVM.Builder llvmctx) emitLhsSlotStore builder z xv if updtHeader then let zv ← emitLhsVal builder z - callLeanCtorSetTag builder zv (← constIntUnsigned c.cidx) + callLeanCtorSetTag builder zv (← constInt8 c.cidx) return ShouldForwardControlFlow.yes ) emitCtorSetArgs builder z ys @@ -961,7 +974,7 @@ def emitTag (builder : LLVM.Builder llvmctx) (x : VarId) (xType : IRType) : M ll def emitSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M llvmctx Unit := do let fnName := "lean_ctor_set" let retty ← LLVM.voidType llvmctx - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.voidPtrType llvmctx] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx , ← LLVM.voidPtrType llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys let _ ← LLVM.buildCall2 builder fnty fn #[← emitLhsVal builder x, ← constIntUnsigned i, (← emitArgVal builder y).2] @@ -969,7 +982,7 @@ def emitSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : Arg) : M def emitUSet (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) (y : VarId) : M llvmctx Unit := do let fnName := "lean_ctor_set_usize" let retty ← LLVM.voidType llvmctx - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, ← LLVM.size_tType llvmctx] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, ← LLVM.size_tType llvmctx] let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let fnty ← LLVM.functionType retty argtys let _ ← LLVM.buildCall2 builder fnty fn #[← emitLhsVal builder x, ← constIntUnsigned i, (← emitLhsVal builder y)] @@ -1008,7 +1021,7 @@ def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Na | IRType.uint32 => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx) | IRType.uint64 => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx) | _ => throw s!"invalid type for 'lean_ctor_set': '{t}'" - let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx, setty] + let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, setty] let retty ← LLVM.voidType llvmctx let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys let xv ← emitLhsVal builder x @@ -1026,12 +1039,12 @@ def emitDel (builder : LLVM.Builder llvmctx) (x : VarId) : M llvmctx Unit := do let _ ← LLVM.buildCall2 builder fnty fn #[xv] def emitSetTag (builder : LLVM.Builder llvmctx) (x : VarId) (i : Nat) : M llvmctx Unit := do - let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx] + let argtys := #[← LLVM.voidPtrType llvmctx, ← LLVM.i8Type llvmctx] let retty ← LLVM.voidType llvmctx let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty "lean_ctor_set_tag" argtys let xv ← emitLhsVal builder x let fnty ← LLVM.functionType retty argtys - let _ ← LLVM.buildCall2 builder fnty fn #[xv, ← constIntUnsigned i] + let _ ← LLVM.buildCall2 builder fnty fn #[xv, ← constInt8 i] def ensureHasDefault' (alts : Array Alt) : Array Alt := if alts.any Alt.isDefault then alts @@ -1057,7 +1070,7 @@ partial def emitCase (builder : LLVM.Builder llvmctx) match alt with | Alt.ctor c b => let destbb ← builderAppendBasicBlock builder s!"case_{xType}_{c.name}_{c.cidx}" - LLVM.addCase switch (← constIntUnsigned c.cidx) destbb + LLVM.addCase switch (← constIntSizeT c.cidx) destbb LLVM.positionBuilderAtEnd builder destbb emitFnBody builder b | Alt.default b => @@ -1300,7 +1313,7 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M let ginit?v ← LLVM.buildLoad2 builder ginit?ty ginit?slot "init_v" buildIfThen_ builder "isGInitialized" ginit?v (fun builder => do - let box0 ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "box0" + let box0 ← callLeanBox builder (← constIntSizeT 0) "box0" let out ← callLeanIOResultMKOk builder box0 "retval" let _ ← LLVM.buildRet builder out pure ShouldForwardControlFlow.no) @@ -1318,7 +1331,7 @@ def emitInitFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M callLeanDecRef builder res let decls := getDecls env decls.reverse.forM (emitDeclInit builder initFn) - let box0 ← callLeanBox builder (← LLVM.constIntUnsigned llvmctx 0) "box0" + let box0 ← callLeanBox builder (← constIntSizeT 0) "box0" let out ← callLeanIOResultMKOk builder box0 "retval" let _ ← LLVM.buildRet builder out @@ -1440,7 +1453,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M See issue #534. We can remove this workaround after we implement issue #467. -/ callLeanSetPanicMessages builder (← LLVM.constFalse llvmctx) let world ← callLeanIOMkWorld builder - let resv ← callModInitFn builder (← getModName) (← LLVM.constInt8 llvmctx 1) world ((← getModName).toString ++ "_init_out") + let resv ← callModInitFn builder (← getModName) (← constInt8 1) world ((← getModName).toString ++ "_init_out") let _ ← LLVM.buildStore builder resv res callLeanSetPanicMessages builder (← LLVM.constTrue llvmctx) @@ -1453,7 +1466,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M callLeanDecRef builder resv callLeanInitTaskManager builder if xs.size == 2 then - let inv ← callLeanBox builder (← LLVM.constInt (← LLVM.size_tType llvmctx) 0) "inv" + let inv ← callLeanBox builder (← constIntSizeT 0) "inv" let _ ← LLVM.buildStore builder inv inslot let ity ← LLVM.size_tType llvmctx let islot ← LLVM.buildAlloca builder ity "islot" @@ -1463,11 +1476,11 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M buildWhile_ builder "argv" (condcodegen := fun builder => do let iv ← LLVM.buildLoad2 builder ity islot "iv" - let i_gt_1 ← LLVM.buildICmp builder LLVM.IntPredicate.UGT iv (← constIntUnsigned 1) "i_gt_1" + let i_gt_1 ← LLVM.buildICmp builder LLVM.IntPredicate.UGT iv (← constIntSizeT 1) "i_gt_1" return i_gt_1) (bodycodegen := fun builder => do let iv ← LLVM.buildLoad2 builder ity islot "iv" - let iv_next ← LLVM.buildSub builder iv (← constIntUnsigned 1) "iv.next" + let iv_next ← LLVM.buildSub builder iv (← constIntSizeT 1) "iv.next" LLVM.buildStore builder iv_next islot let nv ← callLeanAllocCtor builder 1 2 0 "nv" let argv_i_next_slot ← LLVM.buildGEP2 builder (← LLVM.voidPtrType llvmctx) argvval #[iv_next] "argv.i.next.slot" @@ -1509,7 +1522,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M pure ShouldForwardControlFlow.no else do callLeanDecRef builder resv - let _ ← LLVM.buildRet builder (← LLVM.constInt64 llvmctx 0) + let _ ← LLVM.buildRet builder (← constInt64 0) pure ShouldForwardControlFlow.no ) @@ -1517,7 +1530,7 @@ def emitMainFn (mod : LLVM.Module llvmctx) (builder : LLVM.Builder llvmctx) : M let resv ← LLVM.buildLoad2 builder resty res "resv" callLeanIOResultShowError builder resv callLeanDecRef builder resv - let _ ← LLVM.buildRet builder (← LLVM.constInt64 llvmctx 1) + let _ ← LLVM.buildRet builder (← constInt64 1) pure ShouldForwardControlFlow.no) -- at the merge let _ ← LLVM.buildUnreachable builder @@ -1592,6 +1605,8 @@ def emitLLVM (env : Environment) (modName : Name) (filepath : String) : IO Unit let some fn ← LLVM.getNamedFunction emitLLVMCtx.llvmmodule name | throw <| IO.Error.userError s!"ERROR: linked module must have function from runtime module: '{name}'" LLVM.setLinkage fn LLVM.Linkage.internal + if let some err ← LLVM.verifyModule emitLLVMCtx.llvmmodule then + throw <| .userError err LLVM.writeBitcodeToFile emitLLVMCtx.llvmmodule filepath LLVM.disposeModule emitLLVMCtx.llvmmodule | .error err => throw (IO.Error.userError err) diff --git a/src/Lean/Compiler/IR/LLVMBindings.lean b/src/Lean/Compiler/IR/LLVMBindings.lean index e60a49abca..3098314c4b 100644 --- a/src/Lean/Compiler/IR/LLVMBindings.lean +++ b/src/Lean/Compiler/IR/LLVMBindings.lean @@ -326,6 +326,9 @@ opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit @[extern "lean_llvm_dispose_module"] opaque disposeModule (m : Module ctx) : BaseIO Unit +@[extern "lean_llvm_verify_module"] +opaque verifyModule (m : Module ctx) : BaseIO (Option String) + @[extern "lean_llvm_create_string_attribute"] opaque createStringAttribute (key : String) (value : String) : BaseIO (Attribute ctx) @@ -439,6 +442,11 @@ def constInt32 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : B def constInt64 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) := constInt' ctx 64 value signExtend -def constIntUnsigned (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) := +def constIntSizeT (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) := + -- TODO: make this stick to the actual size_t of the target machine constInt' ctx 64 value signExtend + +def constIntUnsigned (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) := + -- TODO: make this stick to the actual unsigned of the target machine + constInt' ctx 32 value signExtend end LLVM diff --git a/src/library/compiler/llvm.cpp b/src/library/compiler/llvm.cpp index 2b15190a06..efc08a6c8b 100644 --- a/src/library/compiler/llvm.cpp +++ b/src/library/compiler/llvm.cpp @@ -18,6 +18,7 @@ Lean's IR. #include "runtime/string_ref.h" #ifdef LEAN_LLVM +#include "llvm-c/Analysis.h" #include "llvm-c/BitReader.h" #include "llvm-c/BitWriter.h" #include "llvm-c/Core.h" @@ -1424,3 +1425,20 @@ extern "C" LEAN_EXPORT lean_object *llvm_is_declaration(size_t ctx, size_t globa return lean_io_result_mk_ok(lean_box(is_bool)); #endif // LEAN_LLVM } + +extern "C" LEAN_EXPORT lean_object *lean_llvm_verify_module(size_t ctx, size_t mod, + lean_object * /* w */) { +#ifndef LEAN_LLVM + lean_always_assert( + false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " + "the LLVM backend function.")); +#else + char* msg = NULL; + LLVMBool broken = LLVMVerifyModule(lean_to_Module(mod), LLVMReturnStatusAction, &msg); + if (broken) { + return lean_io_result_mk_ok(lean::mk_option_some(lean_mk_string(msg))); + } else { + return lean_io_result_mk_ok(lean::mk_option_none()); + } +#endif // LEAN_LLVM +}