fix: LLVM backend: detect size_t from target triple

[iacore]

I added the binding API to get pointer size from target. I hope I got the lifetime right.

A lot of plumbing need to be done in Lean

@bollu

[github-actions[bot]]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[bollu]

@locriacyber Thanks for the PR!

Ideally, all uses of size_t / platform dependent width should be localized to size_tType. We should change its definition to build an i<targetMachinePointerSize>.

I also believe the tests are failing with:

2023-02-04T18:06:53.6001228Z LEAN ASSERTION VIOLATION
2023-02-04T18:06:53.6004296Z File: D:/a/lean4/lean4/src/library/compiler/llvm.cpp
2023-02-04T18:06:53.6012618Z Line: 1143
2023-02-04T18:06:53.6094243Z !is_error && "failed to get target from triple"
2023-02-04T18:06:53.6096142Z 'unreachable' code was reached
2023-02-04T18:06:53.6097006Z + fail 'Failed to compile append.lean into bitcode file'
2023-02-04T18:06:53.6112910Z + echo Failed to compile append.lean into bitcode file
2023-02-04T18:06:53.6120091Z Failed to compile append.lean into bitcode file
2023-02-04T18:06:53.6127040Z + exit 1

since LLVM.llvmInitializeTargetInfo was deleted.

[iacore]

Should be good to go.

@bollu About your comments on "void*", I assumed that is the target pointer size.

[iacore]

I added comments for fixing #2085.

[bollu]

Heya @iacore , thanks again for the PR! I'm now in a position to review and merge this PR, if you have the bandwidth to rebase this on top of current master.

I'm also happy to create a new PR that's rebased on leanprover/lean4/master (with you as the PR author), if that's easier for you!

[iacore]

rebased.

You can squash this with the issue title as the commit message.

[tydeu]

Following Lean style, the size_t definitions should not have underscores (as they are not theorems or macros). I would suggest renaming, e.g., get_size_t_Type to getUSizeType since USize is the Lean type to which the C size_tcorresponds.

[bollu]

were (@hargoniX and I) are testing the code that's generated by this PR before we greenlight it. In doing so, we've discovered a curious bug:

$  ../../build/stage1/bin/lean --target=i386-uknown-linux-gnu closure_bug7.lean  --bc=closure_bug7.bc
$ opt -S closure_bug7.bc
opt: closure_bug7.bc: error: Invalid record (Producer: 'LLVM15.0.7' Reader: 'LLVM 15.0.7')

I suspect that we are silently building incorrect IR, which gets written into an incorrect bitcode file that cannot be loaded back into the LLVM tools. I'm now building a debug build of LLVM with all of the checks to see if LLVM tells us that we are building incorrect IR. We are building LLVM with the options -DCMAKE_BUILD_Type=Debug -DLLVM_ENABLE_ASSERTIONS=ON -DLLVM_ENABLE_EXPENSIVE_CHECKS=ON, to give us the best shot we have at debugging this.

[bollu]

We do indeed miscompile:

$  ../../build/stage1/bin/lean --target=i386-uknown-linux-gnu closure_bug7.lean  --bc=closure_bug7.bc
...
lean: /home/t-sibhat/projects/lean-llvm/llvm-project/llvm/lib/IR/Instructions.cpp:528: void llvm::CallInst::init(llvm::FunctionType*, llvm::Value*, llvm::ArrayRef<llvm::Value*>, llvm::ArrayRef<llvm::OperandBundleDefT<llvm::Value*> >, const llvm::Twine&): Assertion `(i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && "Calling a function with a bad signature!"' failed.
[1]    309982 IOT instruction  ../../build/stage1/bin/lean --target=i386-uknown-linux-gnu closure_bug7.lean

The interesting portion of the backtrace:

...
#5  0x00007ffff578671b in __assert_fail_base (fmt=0x7ffff593b150 "%s%s%s:%u: %s%sAssertion `%s' failed.\n%n",
    assertion=0x7fffe92d60d0 "(i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && \"Calling a function with a bad signature!\"", file=0x7fffe92d5740 "/home/t-sibhat/projects/lean-llvm/llvm-project/llvm/lib/IR/Instructions.cpp", line=528, function=<optimized out>)
    at ./assert/assert.c:92
#6  0x00007ffff5797e96 in __GI___assert_fail (
    assertion=0x7fffe92d60d0 "(i >= FTy->getNumParams() || FTy->getParamType(i) == Args[i]->getType()) && \"Calling a function with a bad signature!\"", file=0x7fffe92d5740 "/home/t-sibhat/projects/lean-llvm/llvm-project/llvm/lib/IR/Instructions.cpp", line=528,
    function=0x7fffe92d5f38 "void llvm::CallInst::init(llvm::FunctionType*, llvm::Value*, llvm::ArrayRef<llvm::Value*>, llvm::ArrayRef<llvm::OperandBundleDefT<llvm::Value*> >, const llvm::Twine&)") at ./assert/assert.c:101
#7  0x00007fffe8f53389 in llvm::CallInst::init (this=0x55555566eae0, FTy=0x555555662408, Func=0x55555566e9b8, Args=..., Bundles=...,
    NameStr=...) at /home/t-sibhat/projects/lean-llvm/llvm-project/llvm/lib/IR/Instructions.cpp:528
#8  0x00007fffe8d4f984 in llvm::CallInst::CallInst (this=0x55555566eae0, Ty=0x555555662408, Func=0x55555566e9b8, Args=..., Bundles=...,
    NameStr=..., InsertBefore=0x0) at /home/t-sibhat/projects/lean-llvm/llvm-project/llvm/include/llvm/IR/Instructions.h:1728
#9  0x00007fffe8d4f7e1 in llvm::CallInst::Create (Ty=0x555555662408, Func=0x55555566e9b8, Args=..., Bundles=..., NameStr=..., InsertBefore=0x0)
    at /home/t-sibhat/projects/lean-llvm/llvm-project/llvm/include/llvm/IR/Instructions.h:1538
#10 0x00007fffe8d520e0 in llvm::IRBuilderBase::CreateCall (this=0x555555664e50, FTy=0x555555662408, Callee=0x55555566e9b8, Args=..., Name=...,
    FPMathTag=0x0) at /home/t-sibhat/projects/lean-llvm/llvm-project/llvm/include/llvm/IR/IRBuilder.h:2232
#11 0x00007fffe8ddc022 in LLVMBuildCall2 (B=0x555555664e50, Ty=0x555555662408, Fn=0x55555566e9b8, Args=0x55555566e990, NumArgs=1,
    Name=0x7fffe574ebc8 "lean_box_outv") at /home/t-sibhat/projects/lean-llvm/llvm-project/llvm/lib/IR/Core.cpp:3919
#12 0x00007ffff7a25409 in lean_llvm_build_call2 () from /home/t-sibhat/projects/lean-llvm/lean4/build/stage1/bin/../lib/lean/libleanshared.so
#13 0x00007ffff6ca22c3 in l_Lean_IR_EmitLLVM_callLeanBox ()
   from /home/t-sibhat/projects/lean-llvm/lean4/build/stage1/bin/../lib/lean/libleanshared.so
#14 0x00007ffff6c99358 in l_Lean_IR_EmitLLVM_emitCtor ()
   from /home/t-sibhat/projects/lean-llvm/lean4/build/stage1/bin/../lib/lean/libleanshared.so
#15 0x00007ffff6c95897 in l_Lean_IR_EmitLLVM_emitVDecl ()
   from /home/t-sibhat/projects/lean-llvm/lean4/build/stage1/bin/../lib/lean/libleanshared.so
#

[bollu]

I'm now attempting to fix the trail of issues this has unearthed here: https://github.com/bollu/lean4/tree/llvm-size_t

@iacore , I've given you push access to the repo bollu/lean4. Shall we continue developing this patch against that branch? It's much easier to collaborate, as everyone who might be interested in commiting against this PR (@Kha, @hargoniX , @tobiasgrosser , @bollu ) have commit access to that repo. Click on https://github.com/bollu/lean4/invitations to accept the commit bits invite!

[bollu]

We appear to have fixed the prior issue with code generating lean_box, and are now attempting to fix the argument list of lean_ctor_set_arg. Here's the backtrace: https://github.com/bollu/lean4/commit/1f617201f011d3c724d4dadd24bc20c1f667890f

[iacore]

@bollu Thanks for the invite. I don't know anything about what to fix though. What commands I need to run to find tests that miscompile?

[bollu]

@iacore one needs to build LLVM with a debug build.

When compiling LLVM, we run cmake ../ -DLLVM_ENABLE_ASSERTIONS=ON -DCMAKE_BUILD_TYPE=Debug -DLLVM_ENABLE_EXPENSIVE_CHECKS=ON.

Then, we use this version of the LLVM toolchain to build lean. Finally, with the new lean build that's linked against the debug llvm, we go to the folder lean4/tests/compiler/ and we run: /path/to/lean4/build/stage1/bin/lean --target=i386-uknown-linux-gnu closure_bug7.lean --bc=closure_bug7.bc. This will cause LLVM to throw an error when we build invalid LLVM IR.