Add support for multi version bitcode libraries #1250

MartinNowack · 2020-04-06T16:14:56Z

Currently, KLEE only supports one version of the runtime library.
This is a problem if different setups are needed, e.g. 32bit vs. 64bit or different optimisations.

Moreover, an additional external build system is used to handle the generation of one single bitcode library instance.

This PR simplifies and provides a cmake-only based solution that allows arbitrary runtime library configurations, compilation and their setup.
Moreover, it contains several clean-ups and modernisations of the cmake build system.
Last point, worth to mention, this PR sets the requirement for cmake to 3.5 which is still ancient and even supported by Ubuntu 16.04 as default.

kren1 · 2020-04-06T16:40:23Z

200 deleted lines, I like it :D

codecov · 2020-04-06T17:27:03Z

Codecov Report

Merging #1250 into master will increase coverage by 0.00%.
The diff coverage is 85.18%.

@@           Coverage Diff           @@
##           master    #1250   +/-   ##
=======================================
  Coverage   69.18%   69.19%           
=======================================
  Files         154      154           
  Lines       18389    18400   +11     
  Branches     4086     4089    +3     
=======================================
+ Hits        12723    12731    +8     
  Misses       3903     3903           
- Partials     1763     1766    +3

Impacted Files	Coverage Δ
tools/klee/main.cpp	`70.32% <83.33%> (-0.01%)`	⬇️
include/klee/Core/Interpreter.h	`100.00% <100.00%> (ø)`
lib/Core/Executor.cpp	`76.56% <100.00%> (+<0.01%)`	⬆️

jbuening

Great to see this particularly uggly part of the build system gone! I also appreciate bumping the required cmake version at least somewhat. 👍 Besides from a question that I'll post below, I only found some very minor things while taking a look at your changes.

CMakeLists.txt

jbuening · 2020-04-06T18:09:06Z

runtime/CMakeLists.txt

 if (${LLVM_VERSION_MAJOR} GREATER 4)
-	set(O0OPT "${O0OPT} -Xclang -disable-O0-optnone")
+    list(APPEND COMMON_CC_FLAGS "-Xclang" "-disable-O0-optnone")


Did you remove -O0 from COMMON_CC_FLAGS on purpose? If yes, why keep -disable-O0-optnone here?

-O0 should be the default optimisation - -disable-O0-optnone should have no influence if any higher level is selected.
I didn't want to have any optimisation settings as part of the common flags.

runtime/klee-libc/Makefile.cmake.bitcode

runtime/Intrinsic/CMakeLists.txt

runtime/FreeStanding/CMakeLists.txt

jbuening · 2020-04-07T05:51:58Z

@MartinNowack Great work! However, there is one thing that I don't understand: You write that this PR "allows arbitrary runtime library configurations", but somehow I fail to see how I would choose whether to have assertions enabled or which optimization level I want for the runtime libraries? (Not sure if you are ultimately aiming at this, but I think it would be great if it were possible to choose these parameters at runtime in a future version of KLEE)

MartinNowack · 2020-04-07T07:14:28Z

@jbuening Great! Thanks a lot for your review. I'm going to add suggested changes.
To answer your question: https://github.com/klee/klee/pull/1250/files#diff-726b77028646514cca3f1416f7d91237R15 . You add a new name, e.g. "my_super_opt" and specialise the flags:

set(LIB_BC_SUFFIX
        64
        32
        MY_SUPER_OPT
        )

set(LIB_BC_FLAGS_MY_SUPER_OPT
        -O42
        )

And it will automatically generate a set of KLEE runtime libraries with this optimisation and that suffix.
KLEE currently just auto-selects 32bit vs. 64bit but this can be easily extended and generalised.

kren1 · 2020-04-07T09:45:20Z

@MartinNowack that was my concern too. I fail to see how this is used. Maybe just add the above GitHub comment as a code comment somewhere

ccadar · 2020-11-03T13:07:57Z

@MartinNowack This looks nice! There's some useful cleanup and it's great that the runtime libraries are built more similarly to the rest of the code. However, I feel you need to add some documentation; I'm a bit confused about how to use this. I also don't know how this would solve the include in #1337, can you explain?
Would you have time to add a few notes about this at https://klee.github.io/docs/developers-guide/#build-system?

Two other minor points:

Freestanding is a standalone word; not sure why we spell it FreeStanding ;)
Why did you remove the clean_all target? Does everything get cleaned with make clean now?

Thanks!

MartinNowack · 2020-11-03T17:22:39Z

@ccadar Thanks for your review. I added some more detailed documentation. This should solve most of your questions.
If not, let me know such that I can make changes on this PR or the other. The inclusion is solved by referencing the same file in each CMakeLists.txt subdirectories needed.

clean_all used to clean in addition the doxygen and the runtime libraries. Both is now possible as files are tracked now directly by cmake and not externally anymore.
FreeStanding good question how this ended up there - but this can be changed easily.

ccadar · 2020-11-03T19:22:02Z

Thanks, @MartinNowack, that's really excellent documentation!
I guess my only remaining comment is about the new option you added, --library-suffix. I feel suffix refers to an implementation detail, so perhaps we should use something like build? And library sounds more general than it really is, so perhaps --runtime-build? What do you think?

Ubuntu 16.04 supports cmake 3.5.0 as default. Cmake 2.8.12 was the default in 14.04. Use cmake 3 to simplify cmake files.

Every runtime library can be build with multiple configurations. Replace the Makefile-based setup by cmake one. Currently, we generate 32bit and 64bit libraries simultaneously and can link against them.

…to test. Currently, only 32bit vs. 64bit is supported.

ccadar · 2020-11-04T13:53:12Z

@MartinNowack I see you changed the option name to --runtime-build, thanks. I assume that's the only change, right?
If so, let's merge this!

MartinNowack · 2020-11-04T14:33:01Z

@ccadar Yes, I made your recommended changes. The build is finally through. This is ready to go.

ccadar · 2020-11-04T15:14:34Z

Cool, thanks again for the excellent changes!

251 · 2020-11-06T12:41:33Z

@MartinNowack
Maybe I missed the documentation but how do I configure what runtimes to build? Seems I can't override LIB_BC_SUFFIX with -D during configure.

MartinNowack · 2020-11-06T15:01:43Z

It builds all. LIB_BC_SUFFIX just selects the default. You can choose a different one via --library-suffix.

251 · 2020-11-06T15:39:19Z

@MartinNowack

It builds all.

It attempts to build all and fails on my system for I don't want nor need a 32-bit libc on it. This should definitely be configurable.

jbuening suggested changes Apr 7, 2020

View reviewed changes

MartinNowack force-pushed the cmake_bitcode_build branch from d9ba391 to a7b5dfe Compare April 8, 2020 21:50

MartinNowack force-pushed the cmake_bitcode_build branch from a7b5dfe to 3f5af3b Compare October 5, 2020 15:15

MartinNowack force-pushed the cmake_bitcode_build branch 3 times, most recently from 8030783 to fdd120b Compare November 2, 2020 21:25

ccadar mentioned this pull request Nov 3, 2020

Added support for -D_FORTIFY_SOURCE #1337

Merged

8 tasks

MartinNowack mentioned this pull request Nov 3, 2020

Add documentation for runtime libraries for developers klee/klee.github.io#251

Merged

MartinNowack added 9 commits November 3, 2020 20:17

[cmake] Switch to "newer" cmake version 3.5.0

9361e06

Ubuntu 16.04 supports cmake 3.5.0 as default. Cmake 2.8.12 was the default in 14.04. Use cmake 3 to simplify cmake files.

[cmake] Remove several leftovers from old autoconf build system

01d3c40

[cmake] Use clean command to remove generated doxygen files

1302247

[cmake] Remove clean_all target as not needed by any additional target

23753e8

[cmake] Always create KLEE runtime directory even if POSIX is not built

1a0455f

[cmake] Add support to generate arbitrary runtime library configurations

5021dde

Every runtime library can be build with multiple configurations. Replace the Makefile-based setup by cmake one. Currently, we generate 32bit and 64bit libraries simultaneously and can link against them.

Link to the different runtime libraries depending on the application …

f3c876e

…to test. Currently, only 32bit vs. 64bit is supported.

[build] Add multilib package to build 32bit on ubuntu

7f67619

Rename FreeStanding to Freestanding where appropriate

ff5b12e

MartinNowack force-pushed the cmake_bitcode_build branch from fdd120b to ff5b12e Compare November 3, 2020 20:18

ccadar approved these changes Nov 4, 2020

View reviewed changes

ccadar merged commit a4250b2 into klee:master Nov 4, 2020

MartinNowack deleted the cmake_bitcode_build branch November 6, 2020 15:02

ccadar mentioned this pull request Nov 12, 2020

KLEE runtime build system problems #583

Closed

4 tasks

This was referenced Dec 18, 2020

Fix Runtime CFLAGS #1370

Merged

retire some build system legacy #1371

Merged

jbuening mentioned this pull request Apr 10, 2024

Some of the system tests fail #1717

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add support for multi version bitcode libraries #1250

Add support for multi version bitcode libraries #1250

MartinNowack commented Apr 6, 2020

kren1 commented Apr 6, 2020

codecov bot commented Apr 6, 2020 •

edited

Loading

jbuening left a comment

jbuening Apr 6, 2020

MartinNowack Apr 8, 2020

jbuening commented Apr 7, 2020

MartinNowack commented Apr 7, 2020

kren1 commented Apr 7, 2020

ccadar commented Nov 3, 2020

MartinNowack commented Nov 3, 2020

ccadar commented Nov 3, 2020

ccadar commented Nov 4, 2020

MartinNowack commented Nov 4, 2020

ccadar commented Nov 4, 2020

251 commented Nov 6, 2020

MartinNowack commented Nov 6, 2020

251 commented Nov 6, 2020

Add support for multi version bitcode libraries #1250

Add support for multi version bitcode libraries #1250

Conversation

MartinNowack commented Apr 6, 2020

kren1 commented Apr 6, 2020

codecov bot commented Apr 6, 2020 • edited Loading

Codecov Report

jbuening left a comment

Choose a reason for hiding this comment

jbuening Apr 6, 2020

Choose a reason for hiding this comment

MartinNowack Apr 8, 2020

Choose a reason for hiding this comment

jbuening commented Apr 7, 2020

MartinNowack commented Apr 7, 2020

kren1 commented Apr 7, 2020

ccadar commented Nov 3, 2020

MartinNowack commented Nov 3, 2020

ccadar commented Nov 3, 2020

ccadar commented Nov 4, 2020

MartinNowack commented Nov 4, 2020

ccadar commented Nov 4, 2020

251 commented Nov 6, 2020

MartinNowack commented Nov 6, 2020

251 commented Nov 6, 2020

codecov bot commented Apr 6, 2020 •

edited

Loading