From dfb5548cab54dfcf37cba5ec8c4e25fa305215e0 Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Tue, 22 Nov 2022 01:27:41 +0000 Subject: [PATCH] fix: update libleanrt.bc, rename to lean.h.bc This adds `lean.h.bc`, a LLVM bitcode file of the Lean runtime that is to be inlined. This is programatically generated. 1. This differs from the previous `libleanrt.ll`, since it produces an LLVM bitcode file, versus a textual IR file. The bitcode file is faster to parse and build an in-memory LLVM module from. 2. We build `lean.h.bc` by adding it as a target to `shell`, which ensures that it is always built. 3. We eschew the need for: ```cpp ``` which causes breakage in the build, since changing the meaning of `static` messes with definitions in the C++ headers. Instead, we build `lean.h.bc` by copying everything in `src/include/lean/lean.h`, renaming `inline` to `__attribute__(alwaysinline)` [which forces LLVM to generate `alwaysinline` annotations], then running the `-O3` pass pipeline to get reasonably optimised IR, and will be perfectly inlined when linked into the generated LLVM code by `src/Lean/Compiler/IR/EmitLLVM.lean`. Co-authored-by: Sebastian Ullrich --- nix/bootstrap.nix | 4 ++-- src/runtime/CMakeLists.txt | 16 +++++++++++----- src/runtime/lean_inlines.c | 3 --- src/shell/CMakeLists.txt | 7 +++++++ 4 files changed, 20 insertions(+), 10 deletions(-) delete mode 100644 src/runtime/lean_inlines.c diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix index 6d3a7836bf..359886cd23 100644 --- a/nix/bootstrap.nix +++ b/nix/bootstrap.nix @@ -44,12 +44,12 @@ rec { leancpp = buildCMake { name = "leancpp"; src = ../src; - buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" ]; + buildFlags = [ "leancpp" "leanrt" "leanrt_initial-exec" "shell" "runtime_bc" ]; installPhase = '' mkdir -p $out mv lib/ $out/ mv shell/CMakeFiles/shell.dir/lean.cpp.o $out/lib - mv runtime/libleanrt_initial-exec.a $out/lib + mv runtime/libleanrt_initial-exec.a runtime/lean.h.bc $out/lib ''; }; # rename derivation so `nix run` uses the right executable name but we still see the stage in the build log diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt index 37c4e42bbd..5de8dac4e9 100644 --- a/src/runtime/CMakeLists.txt +++ b/src/runtime/CMakeLists.txt @@ -18,11 +18,17 @@ target_compile_options(leanrt PRIVATE -ftls-model=local-exec) endif() if(LLVM) + if (NOT (CMAKE_CXX_COMPILER_ID MATCHES "Clang")) + message(FATAL_ERROR "building 'lean.h.bc', need CMAKE_CXX_COMPILER_ID to match Clang to build LLVM bitcode file of Lean runtime.") + endif() + FILE(READ "${CMAKE_CURRENT_SOURCE_DIR}/../include/lean/lean.h" LEAN_H) + # generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend + string(REPLACE "static inline" "__attribute__((always_inline))" LEAN_H "${LEAN_H}") + file(WRITE "${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c" "${LEAN_H}") add_custom_command( - OUTPUT libleanrt.bc - DEPENDS ${RUNTIME_OBJS} lean_inlines.c - # compile each runtime file with the original compile flags plus `-emit-llvm`, then `llvm-link` them together - COMMAND bash -ec "rm -rf runtmp || true; mkdir runtmp; for f in ${RUNTIME_OBJS_STR} lean_inlines.c; do ${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER} ${CMAKE_CXX_FLAGS} ${LEANC_OPTS} -I$, -I> $([[ $f = \*.cpp ]] || echo \"-x c\") \"${CMAKE_CURRENT_SOURCE_DIR}/$f\" -S -emit-llvm -o runtmp/$f.ll; done; llvm-link runtmp/*.ll -o libleanrt.bc" + OUTPUT lean.h.bc + DEPENDS ${RUNTIME_OBJS} ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c + COMMAND bash -ec "${CMAKE_BINARY_DIR}/leanc.sh ${LEANC_OPTS} -I$, -I> -c ${CMAKE_CURRENT_BINARY_DIR}/lean_inlines.c -emit-llvm -o ${CMAKE_CURRENT_BINARY_DIR}/lean.h.bc" VERBATIM) - add_custom_target(runtime_bc DEPENDS libleanrt.bc) + add_custom_target(runtime_bc DEPENDS lean.h.bc) endif() diff --git a/src/runtime/lean_inlines.c b/src/runtime/lean_inlines.c deleted file mode 100644 index bb2705e83a..0000000000 --- a/src/runtime/lean_inlines.c +++ /dev/null @@ -1,3 +0,0 @@ -// generate LLVM IR for `static inline` definitions in lean.h for the LLVM backend -#define static extern // work around clang not emitting code for unused `static` definitions -#include diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index f29a9b4a8d..a95af64265 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -32,6 +32,13 @@ add_custom_target(lean ALL COMMAND $(MAKE) -f ${CMAKE_BINARY_DIR}/stdlib.make lean LEAN_SHELL="$" COMMAND_EXPAND_LISTS) +# if we have LLVM enabled, then build `libruntime.bc` which has the LLVM bitcode +# of Lean runtime to be built. +if (LLVM) + add_dependencies(lean runtime_bc) +endif() + + # use executable of current stage for tests string(REGEX REPLACE "^([a-zA-Z]):" "/\\1" LEAN_BIN "${CMAKE_BINARY_DIR}/bin")