lean-llvm
lean-llvm copied to clipboard
GaloisInc
LLVM support for the lean theorem prover
LLVM opcodes use unsigned integer tags to identify them (see [llvm/IR/Instruction.def](https://github.com/llvm/llvm-project/blob/2a69790bad1a081d6b89de65331006c674d8781e/llvm/include/llvm/IR/Instruction.def) in LLVM's source), but unfortunately these can change between LLVM versions. Instead of having lean-llvm rely on these tags...
I am very interested in this project. Is it possible to provide me with some instructions to build the code and try the examples out?
Currently [parseAssembly](https://github.com/GaloisInc/lean-llvm/blob/73314693ea966480d38dd7725e604a637f6ec058/src/llvm_exports.cpp#L1039) uses a hard coded data layout string for expediency. We should probably just take a [data_layout](https://github.com/GaloisInc/lean-llvm/blob/73314693ea966480d38dd7725e604a637f6ec058/src/DataLayout.lean#L62) structure and use it's `toString` instance method or similar (which doesn't yet...
Calling [llvm.ffi.parseBitcodeFile](https://github.com/GaloisInc/lean-llvm/blob/81be84ce767312dbeaf0c8637da0f0883000baf5/src/LLVMFFI.lean#L235) with an invalid file (e.g., an LLVM source assembly file instead of a bitcode file) causes an internal lean assertion to fail, e.g.: ``` ../../bin/../src/runtime/lean.h:634: lean_ctor_num_objs: Assertion `lean_is_ctor(o)'...
This is the change I'm not positive is correct =\ Here is a commit removing various usages of `cnstr_get_scalar` and `cnstr_set_scalar` right before the commit that removed those two template...