search

runtimeverification / llvm-backend

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

--hidden-visibility flag to llvm-kompile #1060

Closed dwightguth closed 1 month ago

dwightguth commented 1 month ago

This flag is used to assist with the process of building an application that links against more than one llvm backend semantics.

It can be used in roughly the following way:

  1. Compile the llvm backend with the clang++ flag -fvisibility=hidden.
  2. Run llvm-kompile definition.kore dt library --hidden-visibility -- -shared entry.cpp -o definition.so in the kompiled directory.
  3. Link definition.so into your application. It will have all the symbols of entry.cpp and entry.cpp will be able to access any symbol in the semantics, but those internal symbols will not be visible to the application.

The application can do this with multiple semantics and there will be no linker issue. I have tested some basic examples that show that each semantics can separately apply its own rewrite rules. There is no test in this PR because the test harness does not allow us to rebuild the llvm backend with a particular set of build flags just for one test, and it didn't seem worth it to put all that effort in just for one test. When we create downstream projects that use this feature, we will be sure to include tests for this feature in those repositories.

dwightguth commented 1 month ago

Something seems broken on ARM. I may have to investigate this.