From 4d47c8abc6cea2a4d54bb179fb1fd1bda1844707 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Mon, 21 Nov 2022 00:50:01 -0800 Subject: [PATCH] feat: add LLVM C API bindings (#1497) Co-authored-by: Sebastian Ullrich Co-authored-by: Gabriel Ebner --- nix/bootstrap.nix | 8 +- nix/packages.nix | 2 +- script/prepare-llvm-linux.sh | 1 + script/prepare-llvm-macos.sh | 1 + script/prepare-llvm-mingw.sh | 1 + src/CMakeLists.txt | 69 +- src/Lean/Compiler/IR.lean | 1 + src/Lean/Compiler/IR/EmitLLVM.lean | 0 src/Lean/Compiler/IR/LLVMBindings.lean | 350 +++++++ src/library/compiler/CMakeLists.txt | 2 +- src/library/compiler/llvm.cpp | 1301 ++++++++++++++++++++++++ 11 files changed, 1718 insertions(+), 18 deletions(-) create mode 100644 src/Lean/Compiler/IR/EmitLLVM.lean create mode 100644 src/Lean/Compiler/IR/LLVMBindings.lean create mode 100644 src/library/compiler/llvm.cpp diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 8a29666748..6d3a7836bf 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -1,12 +1,12 @@ { debug ? false, stage0debug ? false, extraCMakeFlags ? [], - stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, + stdenv, lib, cmake, gmp, gnumake, bash, buildLeanPackage, writeShellScriptBin, runCommand, symlinkJoin, lndir, perl, gnused, darwin, llvmPackages, ... } @ args: with builtins; rec { inherit stdenv; buildCMake = args: stdenv.mkDerivation ({ nativeBuildInputs = [ cmake ]; - buildInputs = [ gmp ]; + buildInputs = [ gmp llvmPackages.llvm ]; # https://github.com/NixOS/nixpkgs/issues/60919 hardeningDisable = [ "all" ]; dontStrip = (args.debug or debug); @@ -16,7 +16,7 @@ rec { ''; } // args // { src = args.realSrc or (lib.sourceByRegex args.src [ "[a-z].*" "CMakeLists\.txt" ]); - cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ]; + cmakeFlags = (args.cmakeFlags or [ "-DSTAGE=1" "-DLLVM=ON" "-DPREV_STAGE=./faux-prev-stage" "-DUSE_GITHASH=OFF" ]) ++ (args.extraCMakeFlags or extraCMakeFlags) ++ lib.optional (args.debug or debug) [ "-DCMAKE_BUILD_TYPE=Debug" ]; preConfigure = args.preConfigure or "" + '' # ignore absence of submodule sed -i 's!lake/Lake.lean!!' CMakeLists.txt @@ -114,6 +114,7 @@ rec { LEAN_CC=${stdenv.cc}/bin/cc ${lean-bin-tools-unwrapped}/bin/leanc -shared ${lib.optionalString stdenv.isLinux "-Bsymbolic"} \ ${if stdenv.isDarwin then "-Wl,-force_load,${Init.staticLib}/libInit.a -Wl,-force_load,${Lean.staticLib}/libLean.a -Wl,-force_load,${leancpp}/lib/lean/libleancpp.a ${leancpp}/lib/libleanrt_initial-exec.a -lc++" else "-Wl,--whole-archive -lInit -lLean -lleancpp ${leancpp}/lib/libleanrt_initial-exec.a -Wl,--no-whole-archive -lstdc++"} -lm ${stdlibLinkFlags} \ + $(${llvmPackages.libllvm.dev}/bin/llvm-config --ldflags --libs) \ -o $out/$libName ''; mods = Init.mods // Lean.mods; @@ -143,6 +144,7 @@ rec { preConfigure = '' cd src ''; + extraCMakeFlags = [ "-DLLVM=OFF" ]; postConfigure = '' patchShebangs ../../tests rm -r bin lib include share diff --git a/nix/packages.nix b/nix/packages.nix index d97021829f..74aa580fef 100644 --- a/nix/packages.nix +++ b/nix/packages.nix @@ -29,7 +29,7 @@ let stdenv' = if stdenv.isLinux then useGoldLinker stdenv else stdenv; lean = callPackage (import ./bootstrap.nix) (args // { stdenv = overrideCC stdenv' cc; - inherit buildLeanPackage; + inherit buildLeanPackage llvmPackages; }); makeOverridableLeanPackage = f: let newF = origArgs: f origArgs // { diff --git a/script/prepare-llvm-linux.sh b/script/prepare-llvm-linux.sh index c4f9b3f278..b896636ab4 100755 --- a/script/prepare-llvm-linux.sh +++ b/script/prepare-llvm-linux.sh @@ -45,6 +45,7 @@ $CP -r llvm/include/*-*-* llvm-host/include/ $CP $GLIBC/lib/libc_nonshared.a stage1/lib/glibc for f in $GLIBC/lib/lib{c,dl,m,rt,pthread}-*; do b=$(basename $f); cp $f stage1/lib/glibc/${b%-*}.so; done OPTIONS=() +echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm-host/bin/llvm-config" # manually point to `llvm-config` location echo -n " -DLEAN_STANDALONE=ON" echo -n " -DCMAKE_CXX_COMPILER=$PWD/llvm-host/bin/clang++ -DLEAN_CXX_STDLIB='-Wl,-Bstatic -lc++ -lc++abi -Wl,-Bdynamic'" echo -n " -DLEAN_EXTRA_CXX_FLAGS='--sysroot $PWD/llvm -idirafter $GLIBC_DEV/include ${EXTRA_FLAGS:-}'" diff --git a/script/prepare-llvm-macos.sh b/script/prepare-llvm-macos.sh index 10f7cdba09..6e1a0fc293 100755 --- a/script/prepare-llvm-macos.sh +++ b/script/prepare-llvm-macos.sh @@ -36,6 +36,7 @@ $CP llvm/lib/clang/*/include/{std*,__std*,limits}.h stage1/include/clang cp $SDK/usr/lib/libSystem.tbd stage1/lib/libc # use for linking, use system libs for running gcp llvm/lib/lib{c++,c++abi,unwind}.dylib stage1/lib/libc +echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm-host/bin/llvm-config" # manually point to `llvm-config` location echo -n " -DLEAN_STANDALONE=ON" # do not change C++ compiler; libc++ etc. being system libraries means there's no danger of conflicts, # and the custom clang++ outputs a myriad of warnings when consuming the SDK diff --git a/script/prepare-llvm-mingw.sh b/script/prepare-llvm-mingw.sh index b30bcd6488..7a96588971 100644 --- a/script/prepare-llvm-mingw.sh +++ b/script/prepare-llvm-mingw.sh @@ -32,6 +32,7 @@ cp /clang64/lib/{crtbegin,crtend,crt2,dllcrt2}.o stage1/lib/ (cd llvm; cp --parents lib/clang/*/lib/*/libclang_rt.builtins* ../stage1) # further dependencies cp /clang64/lib/lib{m,bcrypt,mingw32,moldname,mingwex,msvcrt,pthread,advapi32,shell32,user32,kernel32,ucrtbase}.* /clang64/lib/libgmp.a llvm/lib/lib{c++,c++abi,unwind}.a stage1/lib/ +echo -n " -DLLVM=ON -DLLVM_CONFIG=$PWD/llvm/bin/llvm-config" # manually point to `llvm-config` location echo -n " -DLEAN_STANDALONE=ON" echo -n " -DCMAKE_C_COMPILER=$PWD/stage1/bin/clang.exe -DCMAKE_C_COMPILER_WORKS=1 -DCMAKE_CXX_COMPILER=$PWD/llvm/bin/clang++.exe -DCMAKE_CXX_COMPILER_WORKS=1 -DLEAN_CXX_STDLIB='-lc++ -lc++abi'" echo -n " -DSTAGE0_CMAKE_C_COMPILER=clang -DSTAGE0_CMAKE_CXX_COMPILER=clang++" diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 215d0c014b..36bdc9ab0b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -157,19 +157,6 @@ if(AUTO_THREAD_FINALIZATION AND NOT MSVC) string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_AUTO_THREAD_FINALIZATION") endif() -if(LLVM) - if(NOT (CMAKE_CXX_COMPILER_ID STREQUAL "Clang" AND CMAKE_C_COMPILER_ID STREQUAL "Clang")) - message(FATAL_ERROR "LLVM=ON must be used with clang. Set `CMAKE_CXX_COMPILER` and `CMAKE_C_COMPILER` accordingly.") - endif() - message(STATUS "Found LLVM ${LLVM_PACKAGE_VERSION}") - message(STATUS "Using LLVMConfig.cmake in: ${LLVM_DIR}") - - include_directories(${LLVM_INCLUDE_DIRS}) - string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_LLVM") -else() - #message(WARNING "Disabling LLVM support. JIT compilation will not be available") -endif() - # Set Module Path set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${CMAKE_SOURCE_DIR}/cmake/Modules") @@ -263,9 +250,44 @@ find_package(PythonInterp) include_directories(${CMAKE_BINARY_DIR}/include) +# Pick up `llvm-config` to setup LLVM flags. +if(LLVM) + if(NOT LLVM_CONFIG) # look for `llvm-config` if not supplied + message(STATUS "'-DLLVM_CONFIG=' not passed as CMake flag, finding `llvm-config` via CMake...") + find_program(LLVM_CONFIG "llvm-config") + if(NOT LLVM_CONFIG) # check that it was found + message(FATAL_ERROR "Unable to find 'llvm-config'") + endif() + endif() + # check that we have 'llvm-config' version. + message(STATUS "Executing 'llvm-config --version' at '${LLVM_CONFIG}' to check configuration.") + execute_process(COMMAND ${LLVM_CONFIG} --version COMMAND_ERROR_IS_FATAL ANY) + message(STATUS "Found 'llvm-config' as ${LLVM_CONFIG}") + # -DLEAN_LLVM is used to conditionally compile Lean features that depend on LLVM + string(APPEND LEAN_EXTRA_CXX_FLAGS " -D LEAN_LLVM") + + execute_process(COMMAND ${LLVM_CONFIG} --ldflags OUTPUT_VARIABLE LLVM_CONFIG_LDFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE) + execute_process(COMMAND ${LLVM_CONFIG} --libs OUTPUT_VARIABLE LLVM_CONFIG_LIBS OUTPUT_STRIP_TRAILING_WHITESPACE) + execute_process(COMMAND ${LLVM_CONFIG} --libdir OUTPUT_VARIABLE LLVM_CONFIG_LIBDIR OUTPUT_STRIP_TRAILING_WHITESPACE) + execute_process(COMMAND ${LLVM_CONFIG} --includedir OUTPUT_VARIABLE LLVM_CONFIG_INCLUDEDIR OUTPUT_STRIP_TRAILING_WHITESPACE) + execute_process(COMMAND ${LLVM_CONFIG} --cxxflags OUTPUT_VARIABLE LLVM_CONFIG_CXXFLAGS OUTPUT_STRIP_TRAILING_WHITESPACE) + execute_process(COMMAND ${LLVM_CONFIG} --system-libs OUTPUT_VARIABLE LLVM_CONFIG_SYSTEM_LIBS OUTPUT_STRIP_TRAILING_WHITESPACE) + message(STATUS "llvm-config: libdir '${LLVM_CONFIG_LIBDIR}' | ldflags '${LLVM_CONFIG_LDFLAGS}' | libs '${LLVM_CONFIG_LIBS}' | system libs '${LLVM_CONFIG_SYSTEM_LIBS}' | cxxflags: ${LLVM_CONFIG_CXXFLAGS} | includedir: ${LLVM_CONFIG_INCLUDEDIR}") +else() + message(WARNING "Disabling LLVM support") +endif() + # libleancpp/Lean as well as libleanrt/Init are cyclically dependent. This works by default on macOS, which also doesn't like # the linker flags necessary on other platforms. +# Furthermore, add LLVM flags into the list of flags we need when linking. +# when using shared libraries, set the `rpath` to help the dynamic loader if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") + if(LLVM) # link to Zlib because LLVM depends on it. + find_package(ZLIB REQUIRED) + message(STATUS "ZLIB_LIBRARY: ${ZLIB_LIBRARY}") + cmake_path(GET ZLIB_LIBRARY PARENT_PATH ZLIB_LIBRARY_PARENT_PATH) + string(APPEND LEAN_EXTRA_LINKER_FLAGS " -L ${ZLIB_LIBRARY_PARENT_PATH}") + endif() string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lleanrt") elseif(${CMAKE_SYSTEM_NAME} MATCHES "Emscripten") string(APPEND LEANC_STATIC_LINKER_FLAGS " -lleancpp -lInit -lLean -lnodefs.js -lleanrt") @@ -282,6 +304,27 @@ endif() string(APPEND LEANC_STATIC_LINKER_FLAGS " ${LEAN_CXX_STDLIB}") string(APPEND LEANSHARED_LINKER_FLAGS " ${LEAN_CXX_STDLIB}") +if(LLVM) + # Here, we perform a replacement of `llvm-host` with `llvm`. This is necessary for our cross-compile + # builds in `script/prepare-llvm-*.sh`. + # - Recall that the host's copy of LLVM binaries and libraries is at + # `llvm-host`, and the target's copy of LLVM binaries and libraries is at + # `llvm`. + # - In an ideal world, we would run the target's `llvm/bin/llvm-config` and get the corrct link options for the target + # (e.g. `-Lllvm/lib/libLLVM`.) + # - However, the target's `llvm/bin/llvm-config` has a different target + # triple from the host, and thus cannot be run on the host. + # - So, we run the host `llvm-host/bin/llvm-config` from which we pick up + # compiler options, and change the output of the host to point to the target. + # - In particular, `host/bin/llvm-config` produces flags like `-Lllvm-host/lib/libLLVM`, while + # we need the path to be `-Lllvm/lib/libLLVM`. Thus, we perform this replacement here. + string(APPEND LEANSHARED_LINKER_FLAGS " -L${LLVM_CONFIG_LIBDIR} ${LLVM_CONFIG_LDFLAGS} ${LLVM_CONFIG_LIBS} ${LLVM_CONFIG_SYSTEM_LIBS}") + string(REPLACE "llvm-host" "llvm" LEANSHARED_LINKER_FLAGS ${LEANSHARED_LINKER_FLAGS}) + set(APPEND LEAN_EXTRA_CXX_FLAGS " -I${LLVM_CONFIG_INCLUDEDIR}") + string(REPLACE "llvm-host" "llvm" LEAN_EXTRA_CXX_FLAGS ${LEAN_EXTRA_CXX_FLAGS}) + message(VERBOSE "leanshared linker flags: '${LEANSHARED_LINKER_FLAGS}' | lean extra cxx flags '${LEAN_EXTR_CXX_FLAGS}'") +endif() + # get rid of unused parts of C++ stdlib if(${CMAKE_SYSTEM_NAME} MATCHES "Darwin") string(APPEND LEANSHARED_LINKER_FLAGS " -Wl,-dead_strip") diff --git a/src/Lean/Compiler/IR.lean b/src/Lean/Compiler/IR.lean index 9fa9939315..8bb7108c53 100644 --- a/src/Lean/Compiler/IR.lean +++ b/src/Lean/Compiler/IR.lean @@ -19,6 +19,7 @@ import Lean.Compiler.IR.ExpandResetReuse import Lean.Compiler.IR.UnboxResult import Lean.Compiler.IR.ElimDeadBranches import Lean.Compiler.IR.EmitC +import Lean.Compiler.IR.EmitLLVM import Lean.Compiler.IR.CtorLayout import Lean.Compiler.IR.Sorry diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean new file mode 100644 index 0000000000..e69de29bb2 diff --git a/src/Lean/Compiler/IR/LLVMBindings.lean b/src/Lean/Compiler/IR/LLVMBindings.lean new file mode 100644 index 0000000000..dec031c798 --- /dev/null +++ b/src/Lean/Compiler/IR/LLVMBindings.lean @@ -0,0 +1,350 @@ +/- +Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Siddharth Bhat +-/ + +namespace LLVM +/-! +This file defines bindings for LLVM. The main mechanisms +are to: +- Mirror the values of C enumerations. +- Create opaque values for LLVM's pointer based API +- Write bindings that are `IO` based, which mutate the underlying in-memory + data structures to build IR. +-/ + +-- https://github.com/llvm/llvm-project/blob/c3e073bcbdc523b0f758d44a89a6333e38bff863/llvm/include/llvm-c/TargetMachine.h#L64 +structure CodegenFileType where + private mk :: val : UInt64 + +def CodegenFileType.AssemblyFile : CodegenFileType := { val := 0 } +def CodegenFileType.ObjectFile : CodegenFileType := { val := 1 } + +-- https://github.com/llvm/llvm-project/blob/c3e073bcbdc523b0f758d44a89a6333e38bff863/llvm/include/llvm-c/Core.h#L290 +structure IntPredicate where + private mk :: val : UInt64 + +def IntPredicate.EQ : IntPredicate := { val := 32 } +def IntPredicate.NE : IntPredicate := { val := IntPredicate.EQ.val + 1 } +def IntPredicate.UGT : IntPredicate := { val := IntPredicate.NE.val + 1 } + +structure BasicBlock (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (BasicBlock ctx) := ⟨{ ptr := default }⟩ + +structure Builder (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (Builder ctx) := ⟨{ ptr := default }⟩ + +structure Context where + private mk :: ptr : USize +instance : Nonempty Context := ⟨{ ptr := default }⟩ + +structure LLVMType (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (LLVMType ctx) := ⟨{ ptr := default }⟩ + +structure MemoryBuffer (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (MemoryBuffer ctx) := ⟨{ ptr := default }⟩ + +structure Module (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (Module ctx) := ⟨{ ptr := default }⟩ + +structure PassManager (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (PassManager ctx) := ⟨{ ptr := default }⟩ + +structure PassManagerBuilder (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (PassManagerBuilder ctx) := ⟨{ ptr := default }⟩ + +structure Target (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (Target ctx) := ⟨{ ptr := default }⟩ + +structure TargetMachine (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (TargetMachine ctx) := ⟨{ ptr := default }⟩ + +structure Value (ctx : Context) where + private mk :: ptr : USize +instance : Nonempty (Value ctx) := ⟨{ ptr := default }⟩ + +@[extern "lean_llvm_create_context"] +opaque createContext : BaseIO (Context) + +@[extern "lean_llvm_create_module"] +opaque createModule (ctx : Context) (name : @&String) : BaseIO (Module ctx) + +@[extern "lean_llvm_module_to_string"] +opaque moduleToString (m : Module ctx) : BaseIO String + +@[extern "lean_llvm_write_bitcode_to_file"] +opaque writeBitcodeToFile (m : Module ctx) (path : @&String) : BaseIO Unit + +@[extern "lean_llvm_add_function"] +opaque addFunction (m : Module ctx) (name : @&String) (type : LLVMType ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_get_named_function"] +opaque getNamedFunction (m : Module ctx) (name : @&String) : BaseIO (Option (Value ctx)) + +@[extern "lean_llvm_add_global"] +opaque addGlobal (m : Module ctx) (name : @&String) (type : LLVMType ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_get_named_global"] +opaque getNamedGlobal (m : Module ctx) (name : @&String) : BaseIO (Option (Value ctx)) + +@[extern "lean_llvm_build_global_string"] +opaque buildGlobalString (builder : Builder ctx) (value : @&String) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_set_initializer"] +opaque setInitializer (glbl : Value ctx) (val : Value ctx) : BaseIO Unit + +@[extern "lean_llvm_function_type"] +opaque functionType (retty : LLVMType ctx) (args : @&Array (LLVMType ctx)) (isVarArg : Bool := false) : BaseIO (LLVMType ctx) + +@[extern "lean_llvm_void_type_in_context"] +opaque voidType (ctx : Context) : BaseIO (LLVMType ctx) + +@[extern "lean_llvm_int_type_in_context"] +opaque intTypeInContext (ctx : Context) (width : UInt64) : BaseIO (LLVMType ctx) + +@[extern "lean_llvm_float_type_in_context"] +opaque floatTypeInContext (ctx : Context) : BaseIO (LLVMType ctx) + +@[extern "lean_llvm_double_type_in_context"] +opaque doubleTypeInContext (ctx : Context) : BaseIO (LLVMType ctx) + +@[extern "lean_llvm_pointer_type"] +opaque pointerType (elemty : LLVMType ctx) : BaseIO (LLVMType ctx) + +@[extern "lean_llvm_array_type"] +opaque arrayType (elemty : LLVMType ctx) (nelem : UInt64) : BaseIO (LLVMType ctx) + +@[extern "lean_llvm_const_array"] +opaque constArray (elemty : LLVMType ctx) (vals : @&Array (Value ctx)) : BaseIO (LLVMType ctx) + +-- `constString` provides a `String` as a constant array of element type `i8` +@[extern "lean_llvm_const_string"] +opaque constString (ctx : Context) (str : @&String) : BaseIO (Value ctx) + +@[extern "lean_llvm_const_pointer_null"] +opaque constPointerNull (elemty : LLVMType ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_get_undef"] +opaque getUndef (elemty : LLVMType ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_create_builder_in_context"] +opaque createBuilderInContext (ctx : Context) : BaseIO (Builder ctx) + +@[extern "lean_llvm_append_basic_block_in_context"] +opaque appendBasicBlockInContext (ctx : Context) (fn : Value ctx) (name : @&String) : BaseIO (BasicBlock ctx) + +@[extern "lean_llvm_position_builder_at_end"] +opaque positionBuilderAtEnd (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO Unit + +@[extern "lean_llvm_build_call"] +opaque buildCall (builder : Builder ctx) (fn : Value ctx) (args : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_set_tail_call"] +opaque setTailCall (fn : Value ctx) (istail : Bool) : BaseIO Unit + +@[extern "lean_llvm_build_cond_br"] +opaque buildCondBr (builder : Builder ctx) (if_ : Value ctx) (thenbb : BasicBlock ctx) (elsebb : BasicBlock ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_build_br"] +opaque buildBr (builder : Builder ctx) (bb : BasicBlock ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_build_alloca"] +opaque buildAlloca (builder : Builder ctx) (ty : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_load"] +opaque buildLoad (builder : Builder ctx) (val : Value ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_store"] +opaque buildStore (builder : Builder ctx) (val : Value ctx) (store_loc_ptr : Value ctx) : BaseIO Unit + +@[extern "lean_llvm_build_ret"] +opaque buildRet (builder : Builder ctx) (val : Value ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_build_unreachable"] +opaque buildUnreachable (builder : Builder ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_build_gep"] +opaque buildGEP (builder : Builder ctx) (base : Value ctx) (ixs : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_inbounds_gep"] +opaque buildInBoundsGEP (builder : Builder ctx) (base : Value ctx) (ixs : @&Array (Value ctx)) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_pointer_cast"] +opaque buildPointerCast (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_sext"] +opaque buildSext (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_zext"] +opaque buildZext (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_sext_or_trunc"] +opaque buildSextOrTrunc (builder : Builder ctx) (val : Value ctx) (destTy : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_switch"] +opaque buildSwitch (builder : Builder ctx) (val : Value ctx) (elseBB : BasicBlock ctx) (numCasesHint : UInt64) : BaseIO (Value ctx) + +@[extern "lean_llvm_build_ptr_to_int"] +opaque buildPtrToInt (builder : Builder ctx) (ptr : Value ctx) (destTy : LLVMType ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_mul"] +opaque buildMul (builder : Builder ctx) (x y : Value ctx) (name : @&String) : BaseIO (Value ctx) + +@[extern "lean_llvm_build_add"] +opaque buildAdd (builder : Builder ctx) (x y : Value ctx) (name : @&String) : BaseIO (Value ctx) + +@[extern "lean_llvm_build_sub"] +opaque buildSub (builder : Builder ctx) (x y : Value ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_not"] +opaque buildNot (builder : Builder ctx) (x : Value ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_build_icmp"] +opaque buildICmp (builder : Builder ctx) (predicate : IntPredicate) (x y : Value ctx) (name : @&String := "") : BaseIO (Value ctx) + +@[extern "lean_llvm_add_case"] +opaque addCase (switch onVal : Value ctx) (destBB : BasicBlock ctx) : BaseIO Unit + +@[extern "lean_llvm_get_insert_block"] +opaque getInsertBlock (builder : Builder ctx) : BaseIO (BasicBlock ctx) + +@[extern "lean_llvm_clear_insertion_position"] +opaque clearInsertionPosition (builder : Builder ctx) : BaseIO Unit + +@[extern "lean_llvm_get_basic_block_parent"] +opaque getBasicBlockParent (bb : BasicBlock ctx) : BaseIO (Value ctx) + +@[extern "lean_llvm_type_of"] +opaque typeOf (val : Value ctx) : BaseIO (LLVMType ctx) + +@[extern "lean_llvm_const_int"] +opaque constInt (intty : LLVMType ctx) (value : UInt64) (signExtend : @Bool := false) : BaseIO (Value ctx) + +@[extern "lean_llvm_print_module_to_string"] +opaque printModuletoString (mod : Module ctx) : BaseIO (String) + +@[extern "lean_llvm_print_module_to_file"] +opaque printModuletoFile (mod : Module ctx) (file : @&String) : BaseIO Unit + +@[extern "llvm_count_params"] +opaque countParams (fn : Value ctx) : UInt64 + +@[extern "llvm_get_param"] +opaque getParam (fn : Value ctx) (ix : UInt64) : BaseIO (Value ctx) + +@[extern "lean_llvm_create_memory_buffer_with_contents_of_file"] +opaque createMemoryBufferWithContentsOfFile (path : @&String) : BaseIO (MemoryBuffer ctx) + +@[extern "lean_llvm_parse_bitcode"] +opaque parseBitcode (ctx : Context) (membuf : MemoryBuffer ctx) : BaseIO (Module ctx) + +@[extern "lean_llvm_link_modules"] +opaque linkModules (dest : Module ctx) (src : Module ctx) : BaseIO Unit + +@[extern "lean_llvm_get_default_target_triple"] +opaque getDefaultTargetTriple : BaseIO String + +@[extern "lean_llvm_get_target_from_triple"] +opaque getTargetFromTriple (triple : @&String) : BaseIO (Target ctx) + +@[extern "lean_llvm_create_target_machine"] +opaque createTargetMachine (target : Target ctx) (tripleStr : @&String) (cpu : @&String) (features : @&String) : BaseIO (TargetMachine ctx) + +@[extern "lean_llvm_target_machine_emit_to_file"] +opaque targetMachineEmitToFile (targetMachine : TargetMachine ctx) (module : Module ctx) (filepath : @&String) (codegenType : LLVM.CodegenFileType) : BaseIO Unit + +@[extern "lean_llvm_create_pass_manager"] +opaque createPassManager : BaseIO (PassManager ctx) + +@[extern "lean_llvm_dispose_pass_manager"] +opaque disposePassManager (pm : PassManager ctx) : BaseIO Unit + +@[extern "lean_llvm_run_pass_manager"] +opaque runPassManager (pm : PassManager ctx) (mod : Module ctx): BaseIO Unit + +@[extern "lean_llvm_create_pass_manager_builder"] +opaque createPassManagerBuilder : BaseIO (PassManagerBuilder ctx) + +@[extern "lean_llvm_dispose_pass_manager_builder"] +opaque disposePassManagerBuilder (pmb : PassManagerBuilder ctx) : BaseIO Unit + +@[extern "lean_llvm_pass_manager_builder_set_opt_level"] +opaque PassManagerBuilder.setOptLevel (pmb : PassManagerBuilder ctx) (optLevel : unsigned) : BaseIO Unit + +@[extern "lean_llvm_pass_manager_builder_populate_module_pass_manager"] +opaque PassManagerBuilder.populateModulePassManager (pmb : PassManagerBuilder ctx) (pm : PassManager ctx): BaseIO Unit + +@[extern "lean_llvm_dispose_target_machine"] +opaque disposeTargetMachine (tm : TargetMachine ctx) : BaseIO Unit + +@[extern "lean_llvm_dispose_module"] +opaque disposeModule (m : Module ctx) : BaseIO Unit + + +-- Helper to add a function if it does not exist, and to return the function handle if it does. +def getOrAddFunction(m : Module ctx) (name : String) (type : LLVMType ctx) : BaseIO (Value ctx) := do + match (← getNamedFunction m name) with + | .some fn => return fn + | .none => addFunction m name type + +def getOrAddGlobal(m : Module ctx) (name : String) (type : LLVMType ctx) : BaseIO (Value ctx) := do + match (← getNamedGlobal m name) with + | .some fn => return fn + | .none => addGlobal m name type + + +def i1Type (ctx : LLVM.Context) : BaseIO (LLVM.LLVMType ctx) := + LLVM.intTypeInContext ctx 1 + +def i8Type (ctx : LLVM.Context) : BaseIO (LLVM.LLVMType ctx) := + LLVM.intTypeInContext ctx 8 + +def i16Type (ctx : LLVM.Context) : BaseIO (LLVM.LLVMType ctx) := + LLVM.intTypeInContext ctx 16 + +def i32Type (ctx : LLVM.Context) : BaseIO (LLVM.LLVMType ctx) := + LLVM.intTypeInContext ctx 32 + +def i64Type (ctx : LLVM.Context) : BaseIO (LLVM.LLVMType ctx) := + LLVM.intTypeInContext ctx 64 + +def voidPtrType (ctx : LLVM.Context) : BaseIO (LLVM.LLVMType ctx) := + do LLVM.pointerType (← LLVM.intTypeInContext ctx 8) + +def i8PtrType (ctx : LLVM.Context) : BaseIO (LLVM.LLVMType ctx) := + voidPtrType ctx + +def constTrue (ctx : Context) : BaseIO (Value ctx) := + do constInt (← i1Type ctx) 1 (signExtend := false) + +def constFalse (ctx : Context) : BaseIO (Value ctx) := + do constInt (← i1Type ctx) 0 (signExtend := false) + +def constInt' (ctx : Context) (width : UInt64) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) := + do constInt (← LLVM.intTypeInContext ctx width) value signExtend + +def constInt1 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) := + constInt' ctx 1 value signExtend + +def constInt8 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) := + constInt' ctx 8 value signExtend + +def constInt32 (ctx : Context) (value : UInt64) (signExtend : Bool := false) : BaseIO (Value ctx) := + constInt' ctx 32 value signExtend + +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) := + constInt' ctx 64 value signExtend +end LLVM diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index 11912b9749..cc8c6f4639 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -6,4 +6,4 @@ add_library(compiler OBJECT init_module.cpp ## New export_attribute.cpp extern_attribute.cpp borrowed_annotation.cpp init_attribute.cpp eager_lambda_lifting.cpp struct_cases_on.cpp find_jp.cpp ir.cpp implemented_by_attribute.cpp - ir_interpreter.cpp) + ir_interpreter.cpp llvm.cpp) diff --git a/src/library/compiler/llvm.cpp b/src/library/compiler/llvm.cpp new file mode 100644 index 0000000000..d6431d60aa --- /dev/null +++ b/src/library/compiler/llvm.cpp @@ -0,0 +1,1301 @@ +/* +Copyright (c) 2022 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Siddharth Bhat + +This file contains bare bones bindings to the LLVM C FFI. This enables +`src/Lean/Compiler/IR/EmitLLVM.lean` to produce LLVM bitcode from +Lean's IR. +*/ + +#include + +#include + +#include "runtime/array_ref.h" +#include "runtime/debug.h" +#include "runtime/string_ref.h" + +#ifdef LEAN_LLVM +#include +#include +#include +#include +#include +#include +#include +#include +#include + +// == LLVM <-> Lean: Target == +static inline size_t Target_to_lean(LLVMTargetRef s) { + return reinterpret_cast(s); +} + +static inline LLVMTargetRef lean_to_Target(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: TargetMachine == + +static inline size_t TargetMachine_to_lean(LLVMTargetMachineRef s) { + return reinterpret_cast(s); +} + +static inline LLVMTargetMachineRef lean_to_TargetMachine(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: MemoryBuffer == + +static inline size_t MemoryBuffer_to_lean(LLVMMemoryBufferRef s) { + return reinterpret_cast(s); +} + +static inline LLVMMemoryBufferRef lean_to_MemoryBuffer(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: ModuleRef == + +static inline size_t Module_to_lean(LLVMModuleRef s) { + return reinterpret_cast(s); +} + +static inline LLVMModuleRef lean_to_Module(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: ContextRef == +static inline size_t Context_to_lean(LLVMContextRef s) { + return reinterpret_cast(s); +} + +static inline LLVMContextRef lean_to_Context(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: TypeRef == +static inline size_t Type_to_lean(LLVMTypeRef s) { + return reinterpret_cast(s); +} + +static inline LLVMTypeRef lean_to_Type(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: ValueRef == +static inline size_t Value_to_lean(LLVMValueRef s) { + return reinterpret_cast(s); +} + +static inline LLVMValueRef lean_to_Value(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: BuilderRef == +static inline size_t Builder_to_lean(LLVMBuilderRef s) { + return reinterpret_cast(s); +} + +static inline LLVMBuilderRef lean_to_Builder(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: BasicBlockRef == +static inline size_t BasicBlock_to_lean(LLVMBasicBlockRef s) { + return reinterpret_cast(s); +} + +static inline LLVMBasicBlockRef lean_to_BasicBlock(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: PassManagerRef == +static inline size_t PassManager_to_lean(LLVMPassManagerRef s) { + return reinterpret_cast(s); +} + +static inline LLVMPassManagerRef lean_to_PassManager(size_t s) { + return reinterpret_cast(s); +} + +// == LLVM <-> Lean: PassManagerRef == +static inline size_t PassManagerBuilder_to_lean(LLVMPassManagerBuilderRef s) { + return reinterpret_cast(s); +} + +static inline LLVMPassManagerBuilderRef lean_to_PassManagerBuilder(size_t s) { + return reinterpret_cast(s); +} +#else +typedef int LLVMBasicBlockRef; +typedef int LLVMContextRef; +typedef int LLVMBuilderRef; +typedef int LLVMTargetRef; +typedef int LLVMTargetMachineRef; +typedef int LLVMTypeRef; +typedef int LLVMValueRef; +typedef int LLVMModuleRef; +typedef int LLVMPassManagerRef; +typedef int LLVMPassManagerBuilderRef; +#endif // LEAN_LLVM + +// == Array Type <-> C array of types == + +// There is redundancy here, but I am loath to clean it up with templates, +// because we will somehow dispatch to the correct `lean_to_*` function. I can't +// think of an immediate, clean way to achieve this (plenty of unclean ways. eg: +// create a templated function that we partial template specialize that tells us +// what the correct `lean_to_*` is. +// Concretely: +// leanToFn = lean_to_LLVMType; +// leanToFn = lean_to_LLVMValue). +LLVMTypeRef *array_ref_to_ArrayLLVMType( + const lean::array_ref &arr) { +#ifndef LEAN_LLVM + lean_always_assert( + false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " + "the LLVM backend function.")); +#else + const int nargs = arr.size(); // lean::array_size(args); + // bollu: ouch, this is expensive! There must be a cheaper way? + LLVMTypeRef *tys = (LLVMTypeRef *)malloc(sizeof(LLVMTypeRef) * nargs); + for (int i = 0; i < nargs; ++i) { + tys[i] = lean_to_Type(lean_unbox_usize(arr[i])); + } + return tys; +#endif // LEAN_LLVM +} + +// TODO: Is there a nicer way to do this? +LLVMValueRef *array_ref_to_ArrayLLVMValue( + const lean::array_ref &arr) { +#ifndef LEAN_LLVM + lean_always_assert( + false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " + "the LLVM backend function.")); +#else + const int nargs = arr.size(); // lean::array_size(args); + // bollu: ouch, this is expensive! There must be a cheaper way? + LLVMValueRef *vals = (LLVMValueRef *)malloc(sizeof(LLVMValueRef) * nargs); + lean_always_assert(vals && "unable to allocate array"); + for (int i = 0; i < nargs; ++i) { + lean_inc(arr[i]); // TODO: do I need this? + vals[i] = lean_to_Value(lean_unbox_usize(arr[i])); + } + return vals; +#endif // LEAN_LLVM +} + +// == FFI == +extern "C" LEAN_EXPORT lean_object *lean_llvm_create_context( + 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 + LLVMContextRef ctx = LLVMContextCreate(); + return lean_io_result_mk_ok(lean_box_usize(Context_to_lean(ctx))); +#endif // LEAN_LLVM +}; + +extern "C" LEAN_EXPORT lean_object *lean_llvm_create_module( + size_t ctx, lean_object *str, 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 + LLVMModuleRef mod = LLVMModuleCreateWithNameInContext(lean_string_cstr(str), + lean_to_Context(ctx)); + return lean_io_result_mk_ok(lean_box_usize(Module_to_lean(mod))); +#endif // LEAN_LLVM +}; + +extern "C" LEAN_EXPORT lean_object *lean_llvm_write_bitcode_to_file( + size_t ctx, size_t mod, lean_object *filepath, 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 + const int err = + LLVMWriteBitcodeToFile(lean_to_Module(mod), lean_string_cstr(filepath)); + lean_always_assert(!err && "unable to write bitcode"); + return lean_io_result_mk_ok(lean_box(0)); // IO Unit +#endif // LEAN_LLVM +}; + +extern "C" LEAN_EXPORT lean_object *lean_llvm_module_to_string( + 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 + return lean_io_result_mk_ok( + lean_mk_string(LLVMPrintModuleToString(lean_to_Module(mod)))); +#endif // LEAN_LLVM +}; + +extern "C" LEAN_EXPORT lean_object *lean_llvm_add_function( + size_t ctx, size_t mod, lean_object *name, size_t type, + 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 + LLVMValueRef out = LLVMAddFunction( + lean_to_Module(mod), lean_string_cstr(name), lean_to_Type(type)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_get_named_function( + size_t ctx, size_t mod, lean_object *name, 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 + LLVMValueRef f = + LLVMGetNamedFunction(lean_to_Module(mod), lean_string_cstr(name)); + return lean_io_result_mk_ok( + f ? lean::mk_option_some(lean_box_usize(Value_to_lean(f))) + : lean::mk_option_none()); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_add_global( + size_t ctx, size_t mod, lean_object *name, size_t type, + 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 + LLVMValueRef out = LLVMAddGlobal(lean_to_Module(mod), lean_to_Type(type), + lean_string_cstr(name)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_get_named_global( + size_t ctx, size_t mod, lean_object *name, 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 + LLVMValueRef g = + LLVMGetNamedGlobal(lean_to_Module(mod), lean_string_cstr(name)); + return lean_io_result_mk_ok( + g ? lean::mk_option_some(lean_box_usize(Value_to_lean(g))) + : lean::mk_option_none()); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_global_string( + size_t ctx, size_t builder, lean_object *str, lean_object *name, + 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 + lean::string_ref sref = lean::string_ref(str, true); + lean::string_ref nameref = lean::string_ref(name, true); + if ( LLVMValueRef out = LLVMBuildGlobalString(lean_to_Builder(builder), + sref.data(), nameref.data()); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} +extern "C" LEAN_EXPORT lean_object *lean_llvm_get_undef(size_t ctx, size_t ty, + 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 + LLVMValueRef out = LLVMGetUndef(lean_to_Type(ty)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_set_initializer( + size_t ctx, size_t global, size_t initializer, 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 + LLVMSetInitializer(lean_to_Value(global), lean_to_Value(initializer)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_function_type( + size_t ctx, size_t retty, lean_object *argtys, uint8_t isvararg, + 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 + lean::array_ref arr(argtys, true); + // TODO, this is expensive! Is there a cheaper way? + LLVMTypeRef *tys = array_ref_to_ArrayLLVMType(arr); + LLVMTypeRef out = + LLVMFunctionType(lean_to_Type(retty), tys, arr.size(), isvararg); + free(tys); + return lean_io_result_mk_ok(lean_box_usize(Type_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_int_type_in_context( + size_t ctx, uint64_t width, 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 + return lean_io_result_mk_ok(lean_box_usize( + Type_to_lean(LLVMIntTypeInContext(lean_to_Context(ctx), width)))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_float_type_in_context( + size_t ctx, 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 + return lean_io_result_mk_ok(lean_box_usize( + Type_to_lean(LLVMFloatTypeInContext(lean_to_Context(ctx))))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_void_type_in_context( + size_t ctx, 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 + return lean_io_result_mk_ok(lean_box_usize( + Type_to_lean(LLVMVoidTypeInContext(lean_to_Context(ctx))))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_double_type_in_context( + size_t ctx, 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 + return lean_io_result_mk_ok(lean_box_usize( + Type_to_lean(LLVMDoubleTypeInContext(lean_to_Context(ctx))))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_pointer_type( + size_t ctx, size_t base, 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 + LLVMTypeRef out = LLVMPointerType(lean_to_Type(base), /*addrspace=*/0); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintTypeToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Type_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_array_type( + size_t ctx, size_t base, uint64_t nelem, 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 + LLVMTypeRef out = LLVMArrayType(lean_to_Type(base), /*nelem=*/nelem); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintTypeToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Type_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_create_builder_in_context( + size_t ctx, 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 + return lean_io_result_mk_ok(lean_box_usize( + Builder_to_lean(LLVMCreateBuilderInContext(lean_to_Context(ctx))))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_append_basic_block_in_context( + size_t ctx, size_t fn, lean_object *name, 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 + LLVMBasicBlockRef bb = LLVMAppendBasicBlockInContext( + lean_to_Context(ctx), lean_to_Value(fn), lean_string_cstr(name)); + return lean_io_result_mk_ok(lean_box_usize(BasicBlock_to_lean(bb))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_position_builder_at_end( + size_t ctx, size_t builder, size_t bb, 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 + LLVMPositionBuilderAtEnd(lean_to_Builder(builder), lean_to_BasicBlock(bb)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_clear_insertion_position( + size_t ctx, size_t builder, 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 + LLVMClearInsertionPosition(lean_to_Builder(builder)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_call2( + size_t ctx, size_t builder, size_t fnty, size_t fnval, lean_object *args, + lean_object *name, 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 + lean::array_ref arr(args, true); + LLVMValueRef *arrArgVals = array_ref_to_ArrayLLVMValue(arr); + LLVMValueRef out = LLVMBuildCall2( + lean_to_Builder(builder), lean_to_Type(fnty), lean_to_Value(fnval), + arrArgVals, arr.size(), lean_string_cstr(name)); + free(arrArgVals); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_call( + size_t ctc, size_t builder, size_t fnval, lean_object *args, + lean_object *name, 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 + lean::array_ref arr(args, true); + LLVMValueRef *arrArgVals = array_ref_to_ArrayLLVMValue(arr); + LLVMValueRef out = + LLVMBuildCall(lean_to_Builder(builder), lean_to_Value(fnval), arrArgVals, + arr.size(), lean_string_cstr(name)); + free(arrArgVals); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_cond_br( + size_t ctx, size_t builder, size_t if_, size_t thenbb, size_t elsebb, + 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 + LLVMValueRef out = + LLVMBuildCondBr(lean_to_Builder(builder), lean_to_Value(if_), + lean_to_BasicBlock(thenbb), lean_to_BasicBlock(elsebb)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_br(size_t ctx, + size_t builder, + size_t bb, + 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 + LLVMValueRef out = + LLVMBuildBr(lean_to_Builder(builder), lean_to_BasicBlock(bb)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_store( + size_t ctx, size_t builder, size_t v, size_t slot, 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 + LLVMValueRef out = LLVMBuildStore(lean_to_Builder(builder), lean_to_Value(v), + lean_to_Value(slot)); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_load( + size_t ctx, size_t builder, size_t slot, lean_object *name, + 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 + LLVMValueRef out = LLVMBuildLoad(lean_to_Builder(builder), + lean_to_Value(slot), lean_string_cstr(name)); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_alloca( + size_t ctx, size_t builder, size_t type, lean_object *name, + 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 + LLVMValueRef out = LLVMBuildAlloca( + lean_to_Builder(builder), lean_to_Type(type), lean_string_cstr(name)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_ret(size_t ctx, + size_t builder, + size_t v, + 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 + LLVMValueRef out = LLVMBuildRet(lean_to_Builder(builder), lean_to_Value(v)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_ret_void( + size_t builder, 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 + LLVMValueRef out = LLVMBuildRetVoid(lean_to_Builder(builder)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_unreachable( + size_t ctx, size_t builder, 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 + LLVMValueRef out = LLVMBuildUnreachable(lean_to_Builder(builder)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_inbounds_gep( + size_t ctx, size_t builder, size_t pointer, lean_object *indices, + lean_object *name, 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 + lean::array_ref indices_array_ref(indices, true); + LLVMValueRef *indices_carr = array_ref_to_ArrayLLVMValue(indices_array_ref); + lean::string_ref name_ref(name, true); + + LLVMValueRef out = LLVMBuildInBoundsGEP( + lean_to_Builder(builder), lean_to_Value(pointer), indices_carr, + indices_array_ref.size(), name_ref.data()); + free(indices_carr); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_gep( + size_t ctx, size_t builder, size_t pointer, lean_object *indices, + lean_object *name, 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 + lean::array_ref indices_array_ref(indices, true); + LLVMValueRef *indices_carr = array_ref_to_ArrayLLVMValue(indices_array_ref); + lean::string_ref name_ref(name, true); + + LLVMValueRef out = + LLVMBuildGEP(lean_to_Builder(builder), lean_to_Value(pointer), + indices_carr, indices_array_ref.size(), name_ref.data()); + free(indices_carr); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_pointer_cast( + size_t ctx, size_t builder, size_t val, size_t destty, lean_object *name, + 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 + LLVMValueRef out = + LLVMBuildPointerCast(lean_to_Builder(builder), lean_to_Value(val), + lean_to_Type(destty), lean_string_cstr(name)); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_sext( + size_t ctx, size_t builder, size_t val, size_t destty, lean_object *name, + 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 + LLVMValueRef out = + LLVMBuildSExt(lean_to_Builder(builder), lean_to_Value(val), + lean_to_Type(destty), lean_string_cstr(name)); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_zext( + size_t ctx, size_t builder, size_t val, size_t destty, lean_object *name, + 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 + LLVMValueRef out = + LLVMBuildZExt(lean_to_Builder(builder), lean_to_Value(val), + lean_to_Type(destty), lean_string_cstr(name)); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_sext_or_trunc( + size_t ctx, size_t builder, size_t val, size_t destty, lean_object *name, + 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 + LLVMTypeRef valType = LLVMTypeOf(lean_to_Value(val)); + LLVMValueRef out; + if (LLVMGetIntTypeWidth(valType) == + LLVMGetIntTypeWidth(lean_to_Type(destty))) { + out = lean_to_Value(val); + } else if (LLVMGetIntTypeWidth(valType) < + LLVMGetIntTypeWidth(lean_to_Type(destty))) { + out = LLVMBuildSExt(lean_to_Builder(builder), lean_to_Value(val), + lean_to_Type(destty), lean_string_cstr(name)); + } else { + out = LLVMBuildTrunc(lean_to_Builder(builder), lean_to_Value(val), + lean_to_Type(destty), lean_string_cstr(name)); + } + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_switch( + size_t ctx, size_t builder, size_t val, size_t elsebb, uint64_t numCases, + 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 + LLVMValueRef out = + LLVMBuildSwitch(lean_to_Builder(builder), lean_to_Value(val), + lean_to_BasicBlock(elsebb), numCases); + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_ptr_to_int( + size_t ctx, size_t builder, size_t ptr, size_t destty, lean_object *name, + 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 + LLVMValueRef out = + LLVMBuildPtrToInt(lean_to_Builder(builder), lean_to_Value(ptr), + lean_to_Type(destty), lean_string_cstr(name)); + + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_mul(size_t ctx, + size_t builder, + size_t lhs, size_t rhs, + lean_object *name, + 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 + LLVMValueRef out = LLVMBuildMul(lean_to_Builder(builder), lean_to_Value(lhs), + lean_to_Value(rhs), lean_string_cstr(name)); + + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_add(size_t ctx, + size_t builder, + size_t lhs, size_t rhs, + lean_object *name, + 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 + LLVMValueRef out = LLVMBuildAdd(lean_to_Builder(builder), lean_to_Value(lhs), + lean_to_Value(rhs), lean_string_cstr(name)); + + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_sub(size_t ctx, + size_t builder, + size_t lhs, size_t rhs, + lean_object *name, + 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 + LLVMValueRef out = LLVMBuildSub(lean_to_Builder(builder), lean_to_Value(lhs), + lean_to_Value(rhs), lean_string_cstr(name)); + + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_not(size_t ctx, + size_t builder, + size_t v, + lean_object *name, + 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 + LLVMValueRef out = LLVMBuildNot(lean_to_Builder(builder), lean_to_Value(v), + lean_string_cstr(name)); + + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_build_icmp( + size_t ctx, size_t builder, uint64_t predicate, size_t x, size_t y, + lean_object *name, 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 + LLVMValueRef out = + LLVMBuildICmp(lean_to_Builder(builder), LLVMIntPredicate(predicate), + lean_to_Value(x), lean_to_Value(y), lean_string_cstr(name)); + + fprintf(stderr, "...%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_add_case(size_t ctx, + size_t switch_, + size_t onVal, + size_t destbb, + 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 + LLVMAddCase(lean_to_Value(switch_), lean_to_Value(onVal), + lean_to_BasicBlock(destbb)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_get_basic_block_parent( + size_t ctx, size_t bb, 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 + LLVMValueRef out = LLVMGetBasicBlockParent(lean_to_BasicBlock(bb)); + fprintf(stderr, "...%s ; parent: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_get_insert_block( + size_t ctx, size_t builder, 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 + LLVMBasicBlockRef out = LLVMGetInsertBlock(lean_to_Builder(builder)); + return lean_io_result_mk_ok(lean_box_usize(BasicBlock_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_type_of(size_t ctx, size_t val, + 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 + LLVMTypeRef ty = LLVMTypeOf(lean_to_Value(val)); + return lean_io_result_mk_ok(lean_box_usize(Type_to_lean(ty))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_print_module_to_string( + 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 + const char *s = LLVMPrintModuleToString(lean_to_Module(mod)); + return lean_io_result_mk_ok(lean::mk_string(s)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_print_module_to_file( + size_t ctx, size_t mod, lean_object *file, 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 + LLVMPrintModuleToFile(lean_to_Module(mod), lean_string_cstr(file), + /*errorMessage=*/NULL); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_const_int(size_t ctx, size_t ty, + uint64_t val, + uint8_t sext, + 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 + LLVMValueRef out = LLVMConstInt(lean_to_Type(ty), val, sext); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_const_array( + size_t ctx, size_t elemty, lean_object *args, 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 + lean::array_ref args_array_ref(args, true); + LLVMValueRef *args_carr = array_ref_to_ArrayLLVMValue(args_array_ref); + LLVMValueRef out = + LLVMConstArray(lean_to_Type(elemty), args_carr, args_array_ref.size()); + free(args_carr); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_const_string( + size_t ctx, lean_object *s, lean_object * /* w */) { + lean::string_ref sref = lean::string_ref(s, true); +#ifndef LEAN_LLVM + lean_always_assert( + false && ("Please build a version of Lean4 with -DLLVM=ON to invoke " + "the LLVM backend function.")); +#else + + LLVMValueRef out = + LLVMConstStringInContext(lean_to_Context(ctx), sref.data(), sref.length(), + /*DontNullTerminate=*/false); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_const_pointer_null( + size_t ctx, size_t elemty, 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 + + LLVMValueRef out = LLVMConstPointerNull(lean_to_Type(elemty)); + + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *llvm_get_param(size_t ctx, size_t f, + uint64_t ix, + 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 + LLVMValueRef out = LLVMGetParam(lean_to_Value(f), ix); + fprintf(stderr, "%s ; out: %s\n", __PRETTY_FUNCTION__, + LLVMPrintValueToString(out)); + return lean_io_result_mk_ok(lean_box_usize(Value_to_lean(out))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT uint64_t llvm_count_params(size_t ctx, size_t f, + 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 + int n = LLVMCountParams(lean_to_Value(f)); + fprintf(stderr, "%s ; n: %d\n", __PRETTY_FUNCTION__, n); + return n; +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_set_tail_call( + size_t ctx, size_t fnval, uint8_t isTail, 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 + LLVMSetTailCall(lean_to_Value(fnval), isTail); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object * +lean_llvm_create_memory_buffer_with_contents_of_file(size_t ctx, + lean_object *path, + 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 + LLVMMemoryBufferRef membuf; + char *err_str = NULL; + int is_error = LLVMCreateMemoryBufferWithContentsOfFile( + lean_string_cstr(path), &membuf, &err_str); + + lean_always_assert((is_error != 1) && "failed to link modules"); + return lean_io_result_mk_ok(lean_box_usize(MemoryBuffer_to_lean(membuf))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_parse_bitcode( + size_t context, size_t membuf, 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 + LLVMModuleRef out_module; + char *err_str = NULL; + int is_error = LLVMParseBitcodeInContext(lean_to_Context(context), + lean_to_MemoryBuffer(membuf), + &out_module, &err_str); + + lean_always_assert(!is_error && "failed to link modules"); + return lean_io_result_mk_ok(lean_box_usize(Module_to_lean(out_module))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_link_modules( + size_t ctx, size_t dest_module, size_t src_module, 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 + int is_error = + LLVMLinkModules2(lean_to_Module(dest_module), lean_to_Module(src_module)); + + lean_always_assert(!is_error && "failed to link modules"); + return lean_io_result_mk_ok(lean_box(0)); +#endif +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_create_target_machine( + size_t ctx, size_t target, lean_object *tripleStr, lean_object *cpuStr, + lean_object *featuresStr, 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 + // TODO (bollu): expose this option + const LLVMCodeGenOptLevel optLevel = LLVMCodeGenLevelAggressive; + const LLVMRelocMode relocMode = LLVMRelocPIC; + const LLVMCodeModel codeModel = LLVMCodeModelDefault; + LLVMTargetMachineRef tm = LLVMCreateTargetMachine( + lean_to_Target(target), lean_string_cstr(tripleStr), + lean_string_cstr(cpuStr), lean_string_cstr(featuresStr), optLevel, + relocMode, codeModel); + + return lean_io_result_mk_ok(lean_box_usize(TargetMachine_to_lean(tm))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_get_target_from_triple( + size_t ctx, lean_object *triple, 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 + LLVMTargetRef t; + char *errmsg = NULL; + int is_error = LLVMGetTargetFromTriple(lean_string_cstr(triple), &t, &errmsg); + lean_always_assert(!is_error && "failed to get target from triple"); + return lean_io_result_mk_ok(lean_box_usize(Target_to_lean(t))); +#endif // LEAN_LLVM +} + +// opaque getDefaultTargetTriple: IO String +extern "C" LEAN_EXPORT lean_object *lean_llvm_get_default_target_triple( + size_t ctx, 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 *triple = LLVMGetDefaultTargetTriple(); + return lean_io_result_mk_ok(lean::mk_string(triple)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_target_machine_emit_to_file( + size_t ctx, size_t target_machine, size_t module, lean_object *filepath, + uint64_t codegenType, 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 + // TODO (bollu): figure out a story for cross-compilation. + // We currently choose not to invoke LLVMInitializeAllTargetInfos() etc. + // since our build system only enables certain backends. + // LLVMInitializeNativeTargetInfo(); + LLVMInitializeNativeTarget(); + LLVMInitializeNativeAsmParser(); + LLVMInitializeNativeAsmPrinter(); + + char *err_msg = NULL; + char *filepath_c_str = strdup(lean_string_cstr(filepath)); + int is_error = LLVMTargetMachineEmitToFile( + lean_to_TargetMachine(target_machine), lean_to_Module(module), + filepath_c_str, LLVMCodeGenFileType(codegenType), &err_msg); + + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager( + size_t ctx, 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 + return lean_io_result_mk_ok( + lean_box_usize(PassManager_to_lean(LLVMCreatePassManager()))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_run_pass_manager( + size_t ctx, size_t pm, 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 + int is_error = + LLVMRunPassManager(lean_to_PassManager(pm), lean_to_Module(mod)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager( + size_t ctx, size_t pm, 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 + LLVMDisposePassManager(lean_to_PassManager(pm)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_create_pass_manager_builder( + size_t ctx, 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 + return lean_io_result_mk_ok(lean_box_usize( + PassManagerBuilder_to_lean(LLVMPassManagerBuilderCreate()))); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_pass_manager_builder( + size_t ctx, size_t pmb, 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 + LLVMPassManagerBuilderDispose(lean_to_PassManagerBuilder(pmb)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object * +lean_llvm_pass_manager_builder_set_opt_level(size_t ctx, size_t pmb, + unsigned opt_level, + 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 + LLVMPassManagerBuilderSetOptLevel(lean_to_PassManagerBuilder(pmb), opt_level); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object * +lean_llvm_pass_manager_builder_populate_module_pass_manager( + size_t ctx, size_t pmb, size_t pm, 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 + LLVMPassManagerBuilderPopulateModulePassManager( + lean_to_PassManagerBuilder(pmb), lean_to_PassManager(pm)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_target_machine( + size_t ctx, size_t tm, 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 + LLVMDisposeTargetMachine(lean_to_TargetMachine(tm)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +} + +extern "C" LEAN_EXPORT lean_object *lean_llvm_dispose_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 + LLVMDisposeModule(lean_to_Module(mod)); + return lean_io_result_mk_ok(lean_box(0)); +#endif // LEAN_LLVM +}