search

runtimeverification / llvm-backend

KORE to llvm translation
BSD 3-Clause "New" or "Revised" License
34 stars 19 forks source link

Disable LTO when building Debian packages #1084

Closed Baltoli closed 1 month ago

Baltoli commented 1 month ago

This PR explicitly disables LTO via the backend's own option when building Debian packages, rather than relying on the Debian Makefile infrastructure to propagate the appropriate flags down through CMake. We already do the same thing when building via Nix.

The issue here manifests strangely (https://github.com/runtimeverification/llvm-backend/issues/1038). In this case, what's happening is that LTO being enabled causes the runtime's static libraries to get built as archives of .bc files rather than actual objects. These bitcode files then contain inline assembly directives based on the C++ code's directives, which contain absolute paths referencing the build system rather than the runtime system. We therefore need to disable LTO so that the assembly directives are resolved fully when the Debian package is built, rather than when it's shipped.

Fixes https://github.com/runtimeverification/llvm-backend/issues/1038

Baltoli commented 1 month ago

Note that the specific issue in #1038 isn't testable here because it's an interaction with the K frontend; that interaction will get tested properly when we finish the K CI refactoring process.

I have verified locally that the issue no longer reproduces in the original context that it appeared in.