Support for LLLVM 15 16 by MartinNowack · Pull Request #1664 · klee/klee

MartinNowack · 2023-10-27T07:14:47Z

This PR adds support for LLVM 15 and 16.

There have been a multitude of required changes that are split into separate commits to simplify the whole process.

In a nutshell, we transitioned to support opaque pointers starting with LLVM 15 explicitly.
All the other commits handle additional moving parts in KLEE that had to be fixed.

Summary:

Checklist:

The PR addresses a single issue. If it can be divided into multiple independent PRs, please do so.
The PR is divided into a logical sequence of commits OR a single commit is sufficient.
There are no unnecessary commits (e.g. commits fixing issues in a previous commit in the same PR).
Each commit has a meaningful message documenting what it does.
All messages added to the codebase, all comments, as well as commit messages are spellchecked.
The code is commented OR not applicable/necessary.
The patch is formatted via clang-format OR not applicable (if explicitly overridden leave unchecked and explain).
There are test cases for the code you added or modified OR no such test cases are required.

scripts/build/p-libcxx.inc

codecov · 2023-10-27T09:15:28Z

Codecov Report

Merging #1664 (5f7d0b2) into master (3ca81c2) will decrease coverage by 0.02%.
The diff coverage is 82.75%.

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #1664      +/-   ##
==========================================
- Coverage   70.20%   70.18%   -0.02%     
==========================================
  Files         161      162       +1     
  Lines       19366    19397      +31     
  Branches     4626     4632       +6     
==========================================
+ Hits        13596    13614      +18     
- Misses       3730     3743      +13     
  Partials     2040     2040

Files	Coverage Δ
include/klee/Expr/Expr.h	`84.76% <100.00%> (+0.05%)`	⬆️
lib/Core/ExternalDispatcher.cpp	`87.31% <ø> (ø)`
lib/Core/GetElementPtrTypeIterator.h	`93.93% <ø> (-1.62%)`	⬇️
lib/Core/SpecialFunctionHandler.cpp	`73.55% <ø> (ø)`
lib/Module/FunctionAlias.cpp	`90.56% <100.00%> (ø)`
lib/Module/IntrinsicCleaner.cpp	`92.97% <ø> (ø)`
lib/Module/KModule.cpp	`86.44% <100.00%> (+0.79%)`	⬆️
lib/Module/LowerSwitch.cpp	`77.77% <100.00%> (-1.39%)`	⬇️
lib/Module/RaiseAsm.cpp	`71.73% <ø> (ø)`
tools/klee/main.cpp	`64.72% <ø> (ø)`
... and 3 more

... and 3 files with indirect coverage changes

ccadar · 2023-10-30T09:47:24Z

@MartinNowack great to see this! I hope we'll see it ready soon!

However, we should first merge #1349 , #1380 and #1663.

jirislaby · 2023-12-14T08:05:40Z

I see (both with llvm 15 and 16 but not with llvm 14 -- even when the patches are applied):

[   35s] Failing Tests (3):
[   35s]     KLEE :: Feature/VarArgByVal.c
[   35s]     KLEE :: Runtime/POSIX/DirConsistency.c
[   35s]     KLEE :: Runtime/POSIX/SymFileConsistency.c

Full log

ccadar

Thanks, @MartinNowack.
Let's merge this as soon as #1380 , #1674 and #1663 are resolved.

ccadar · 2024-01-30T21:33:55Z

@MartinNowack I think this one is next! Do you want to rebase it to double-check that the FreeBSD checks pass, after the latest update? If you do, I spotted two tiny issues: "pointerws" is misspelled in commit message of 561fff8 and LLVM 17 seems to have been introduced prematurely in 5b13c51.

danielschemmel

Thank you very much for all your hard work on this, @MartinNowack!

I have a few comments, most of which are just stylistic (uint64_t is actually called std::uint64_t and for most of the codebase we have an empty line between the includes and the rest of the code), but also one comment about the cmake changes that looks somewhat important.

I hope you can either just one-click apply or ignore the many small suggestions ;).

danielschemmel · 2024-01-31T23:30:40Z

scripts/build/p-libcxx.inc

+     make runtimes - j"$(nproc)" || make cxx || return 1
+   else
+     make cxx - j"$(nproc)" || make cxx || return 1


This looks like the original intent was to run a parallel make followed by a serial make of the same target. This change introduces two problems:

There is a blank between the - and the j that should not be there

it should probably also run make runtimes in the fallback position of the then-case

lib/Core/Executor.cpp

test/regression/2014-07-04-unflushed-error-report.c

test/regression/2015-08-30-empty-constraints.c

test/regression/2015-08-30-sdiv-1.c

test/regression/2017-02-21-pathOS-id.c

test/regression/2017-11-01-test-with-empty-varname.c

lib/Core/Executor.cpp

lib/Module/OptimizeLegacy.cpp

`-DLLVM_ENABLE_PROJECTS` does not include runtimes anymore, instead a `-DLLVM_ENABLE_RUNTIMES` should be used in addition

`libc++` include headers are now split between platform dependent and platform independent code. Before, only include files for the platform independent code were considered. Add support to automatically find platform dependent includes as well. Simplify the detection of libraries and paths. Instead of pointing to the `v1` directory, pointing to the include directory for `-DKLEE_LIBCXX_INCLUDE_PATH` is enough. Update build script to support this as well.

…irectories To support multiple include directories for c++ header files, use `%libcxx_includes`. This string contains the `-I` compiler directive for each include path as well. Update test cases to use new directive.

…er compilers

Newer compilers use `-std=gnu17` as the default when compiling C code. Fix all the test cases that violate this behaviour or explicitly request older standards `-std=c89` where necessary.

Currently, we assume C++11 support being used to by the tested software. This needs to change if newer C++ standards should be supported.

This automatically lifts old-style pointers to opaque pointers. More recent versions use opaque pointers automatically and do not need an explicit enabling.

`Intrinsic::flt_rounds` got removed

Handle like `memalign` for now.

Similar functionality needs to be added using a new pass manager

The optimiser generates different code and calls fwrite directly instead.

The wording changed slightly in newer versions. Update the test case to support this.

They are not supported anymore for newer LLVM versions.

Co-authored-by: Daniel Schemmel <[email protected]> (cherry picked from commit 5d9af02)

Co-authored-by: Daniel Schemmel <[email protected]> (cherry picked from commit 5d61fb6)

Co-authored-by: Daniel Schemmel <[email protected]> (cherry picked from commit 1ea1a75)

MartinNowack · 2024-02-05T17:48:12Z

Thanks @ccadar and @danielschemmel for the review. I addressed most of the comments, I kept the lit's one LLVM 17. We will need it anyway soon 😃 So, this one is ready!

ccadar · 2024-02-08T13:17:16Z

Thanks again, @MartinNowack , for the hard work of adding support for LLVM 15 & 16!

jirislaby · 2024-02-09T07:58:13Z

FWIW, current klee's HEAD -- 9336cd2 -- (still) compiles fine for me with LLVM 16. But I still see #1664 (comment):

[   36s]     KLEE :: Feature/VarArgByVal.c
[   36s]     KLEE :: Runtime/POSIX/DirConsistency.c
[   36s]     KLEE :: Runtime/POSIX/SymFileConsistency.c

ccadar · 2024-02-09T08:28:56Z

Thanks, @jirislaby, I somehow thought that was resolved. Can you please open a new issue with more details? (what platform and configuration you are using, how the tests fail)?

github-advanced-security bot found potential problems Oct 27, 2023

View reviewed changes

scripts/build/p-libcxx.inc Fixed Show fixed Hide fixed

MartinNowack force-pushed the llvm_15_16_support branch from be68584 to bf0ac0a Compare October 30, 2023 15:16

MartinNowack marked this pull request as ready for review October 30, 2023 16:09

ccadar mentioned this pull request Dec 13, 2023

[LLVM15] Module: remove deleted passes #1648

Closed

ccadar requested changes Dec 14, 2023

View reviewed changes

ccadar mentioned this pull request Jan 25, 2024

Drop LLVM 9 and 10 #1686

Merged

8 tasks

danielschemmel reviewed Jan 31, 2024

View reviewed changes

danielschemmel reviewed Feb 2, 2024

View reviewed changes

lib/Core/Executor.cpp Outdated Show resolved Hide resolved

lib/Module/OptimizeLegacy.cpp Outdated Show resolved Hide resolved

lib/Module/OptimizeLegacy.cpp Outdated Show resolved Hide resolved

MartinNowack added 18 commits February 5, 2024 09:36

Add support to build newer LLVM versions

e7d2fec

`-DLLVM_ENABLE_PROJECTS` does not include runtimes anymore, instead a `-DLLVM_ENABLE_RUNTIMES` should be used in addition

MERGE libc++ build system

12f773f

Fix klee-libc/memchr.c compiler warning

d9ead8d

Fix klee_eh_cxx.cpp compiler error

5bda8d1

Refactor invocation of old pass manager into legacy function

e926749

Use KLEE's uClibc v1.4 as default to support the compilation with new…

8435e83

…er compilers

Assume C compiler's default standard is -std=gnu17

36f1eaf

Newer compilers use `-std=gnu17` as the default when compiling C code. Fix all the test cases that violate this behaviour or explicitly request older standards `-std=c89` where necessary.

Explicitly build KLEE's exception handling runtime with C++11

7b27c5e

Currently, we assume C++11 support being used to by the tested software. This needs to change if newer C++ standards should be supported.

Explicitly enable opaque pointer support for LLVM 15

c65892d

This automatically lifts old-style pointers to opaque pointers. More recent versions use opaque pointers automatically and do not need an explicit enabling.

Add support for opaque pointers

4aa2e65

Fix test cases to support opaque pointers

be94ebe

Fix test case: using unsupported CHECK_NEXT instead of CHECK-NEXT

4622b8c

Use APIs of newer LLVM versions instead of unsupported ones

031b33c

Add support for Intrinsic::get_rounding for LLVM 16

bcb6891

`Intrinsic::flt_rounds` got removed

Add support to aligned_alloc generated by LLVM

358386c

Handle like `memalign` for now.

Disable unsupported passes for newer LLVM versions

3e893a2

Similar functionality needs to be added using a new pass manager

MartinNowack and others added 8 commits February 5, 2024 10:30

Disable 2018-10-30-llvm-pr39177.ll for newer LLVM versions.

4a03b4f

The optimiser generates different code and calls fwrite directly instead.

Handle check for thrown libc++ exceptions more general

1ecd32f

The wording changed slightly in newer versions. Update the test case to support this.

Update test case for expressions using udiv, urem, sdiv and srem

097ce3b

They are not supported anymore for newer LLVM versions.

Support newer LLVM versions in lit

0c2812f

Enable CI to test newer LLVM versions

3be7175

Use std:: namespace for uint64_t

cadb905

Co-authored-by: Daniel Schemmel <[email protected]> (cherry picked from commit 5d9af02)

Mention default value in help text for --strip-all and --strip-debug

266cc4b

Co-authored-by: Daniel Schemmel <[email protected]> (cherry picked from commit 5d61fb6)

Add space between include and main function for updated test cases

5f7d0b2

Co-authored-by: Daniel Schemmel <[email protected]> (cherry picked from commit 1ea1a75)

MartinNowack force-pushed the llvm_15_16_support branch from 47219f4 to 5f7d0b2 Compare February 5, 2024 10:34

MartinNowack mentioned this pull request Feb 5, 2024

[BUG]: stucking at 99% during building in NixOS #1690

Closed

ccadar approved these changes Feb 8, 2024

View reviewed changes

ccadar merged commit 9336cd2 into klee:master Feb 8, 2024

MartinNowack deleted the llvm_15_16_support branch February 8, 2024 14:21

jirislaby mentioned this pull request Feb 9, 2024

Tests failures with llvm 15 and 16 #1691

Closed

chenrui333 mentioned this pull request Mar 2, 2024

klee 3.1 Homebrew/homebrew-core#164859

Merged

1 task

milahu mentioned this pull request Apr 14, 2024

klee: llvm llvmPackages_13 -> llvmPackages milahu/nixpkgs#42

Open

emilazy mentioned this pull request Aug 22, 2025

klee: 3.1 -> 3.1-unstable-2025-07-11, bump to LLVM 18 NixOS/nixpkgs#435927

Merged

13 tasks

Conversation

MartinNowack commented Oct 27, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary:

Checklist:

Uh oh!

Uh oh!

codecov bot commented Oct 27, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

ccadar commented Oct 30, 2023

Uh oh!

jirislaby commented Dec 14, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ccadar left a comment

Choose a reason for hiding this comment

Uh oh!

ccadar commented Jan 30, 2024

Uh oh!

danielschemmel left a comment

Choose a reason for hiding this comment

Uh oh!

danielschemmel Jan 31, 2024

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

MartinNowack commented Feb 5, 2024

Uh oh!

ccadar commented Feb 8, 2024

Uh oh!

jirislaby commented Feb 9, 2024

Uh oh!

ccadar commented Feb 9, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

MartinNowack commented Oct 27, 2023 •

edited

Loading

codecov bot commented Oct 27, 2023 •

edited

Loading

jirislaby commented Dec 14, 2023 •

edited

Loading