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
This commit is contained in:
Henrik Böving
GitHub
parent
c27474341e
commit
06f73d621b
3 changed files with 79 additions and 38 deletions
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue