Real freestanding runtime

[mrexodia]

Summary:

Currently the 'freestanding' runtime is not actually freestanding, since it depends on system headers that might not be available. This PR addresses this issue by only using headers like stddef.h and stdint.h, which are part of the compiler headers and therefore always available.

Previously the runtime was using errno.h, which might be defined differently depending on the platform you compile KLEE on. For now I added an extern int errno; but that might not be the right approach.

My compilation settings (macos M1 pro with AppleClang):

    "-DENABLE_TCMALLOC:STRING=OFF"
    "-DENABLE_UNIT_TESTS:STRING=OFF"
    "-DENABLE_SYSTEM_TESTS:STRING=OFF"
    "-DENABLE_POSIX_RUNTIME:STRING=OFF"

I used LLVM 17, which appears to compile fine except for llvm/ADT/Triple.h which was moved. If really necessary I can move that change to a separate PR, but it's an extremely small change.

Checklist:

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

[mrexodia]

Any chance for a review on this? The CI appears to be failing for unrelated reasons...

[ccadar]

@mrexodia thank you for your contribution. We are currently short on reviewing time, sorry for the delay.

On what platform have you seen the need for these changes?

This being said, the PR looks useful and fine overall. However, to simplify reviewing, it would be useful to split the single commit into multiple ones with a short explanation of what each set of changes does. I would also split this into 3 PRs: one for the small LLVM 17 change (for which we also need to add a CI target), one for the smaller changes involving headers and definitions, and one for the errno changes, which might require some more discussion. Thanks again.

[mrexodia]

These changes were necessary on macos (M1) and they would also be necessary for Windows (would have to try). Generally LLVM in freestanding mode does not have access to any system headers (even stdint.h is not working properly on Linux), unless you install the cross-compilation toolchains for the platform you're targeting. I will split the pull requests and get back to you!

[arrowd]

Why introduce errno.h in freestanding? Aren't error codes platform-dependent?

[mrexodia]

Yes, errno is platform-dependent but the functions assign to it so I had to do something 🤷‍♂️ The specific values don’t matter in this context either, it’s just to make things compile without #ifdef all over the place.

[arrowd]

I don't see any functions touching errno in runtime/Freestanding. I'm probably missing something?

[mrexodia]

Yeah the references are in runtime/klee-libc. I just rebased on the latest master, so hopefully the CI will pass now.

[arrowd]

Yes, putting that into klee-libc now makes more sense, thank you.

On other hand, this might pose a problem with FreeBSD - the error codes we have might not match ones used by klee-libc and we also don't have uclibc. Maybe klee-libc should still take errno.h from the host system?

[mrexodia]

I don’t think we should take anything from the host system. For example on Windows I do not have errno.h at all, which is the whole point of this PR. I checked and there are only two occurrences of errno in the klee-libc runtime, perhaps we could pass the defines manually or something?

[mrexodia]

Also the CI failure related to rlimit64 happens because the host does not have struct rlimit64 defined at all. Kind of confusing why it succeeds in master, but it’s a similar issue to the errno in my opinion (the host you compile on does not match the POSIX library implementation stubs)

[arrowd]

For example on Windows I do not have errno.h at all

errno.h on Windows is shipped with ucrt.

perhaps we could pass the defines manually or something?

Well, the user will define them to host values in 99% of cases, I believe,

[mrexodia]

Alright, I will try to extract the 2 error codes used from the host at configure-time and put them in a generated errno.h. The issue I ran into is that the host headers are not available at all, because clang doesn’t have a sysroot for them.

[codecov[bot]]

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 70.18%. Comparing base (7cc669b) to head (acafcc9). Report is 35 commits behind head on master.

Additional details and impacted files

@@            Coverage Diff             @@
##           master    #1739      +/-   ##
==========================================
+ Coverage   68.98%   70.18%   +1.20%     
==========================================
  Files         162      162              
  Lines       19446    19443       -3     
  Branches     4643     4638       -5     
==========================================
+ Hits        13414    13646     +232     
+ Misses       3999     3756     -243     
- Partials     2033     2041       +8     

Files with missing lines	Coverage Δ
runtime/POSIX/klee_init_env.c	59.39% <ø> (ø)

... and 9 files with indirect coverage changes

[mrexodia]

Alright, I rebased on the latest master and put everything in separate commits for review.

@arrowd

errno.h on Windows is shipped with ucrt.

Unless you pass the appropriate -isysroot to clang, the only headers guaranteed to be available will be the ones in <clang prefix>/lib/clang/<version>/include. On Linux I believe /usr/include is always added (at least when building for the host triplet), so things 'work' there out of the box.

@ccadar I think this is now ready for another review. Once this is merged I plan to add freestanding Windows support (which should be fairly straightforward with these changes).

[arrowd]

The PR looks good to me overall, but I'm not a KLEE developer and can not approve.

[mrexodia]

Done!

[ccadar]

Thanks, @mrexodia .

I see a test is failing now with ASan, can you take a look?

[mrexodia]

Thanks, @mrexodia .

I see a test is failing now with ASan, can you take a look?

The failing tests appear to be VectorInstructions/oob-read.c and kleaver/Evaluate2.kquery, which do not use any of the freestanding runtime I changed? (they do not use the runtime at all)

[ccadar]

I think it was Feature/const_array_opt1.c, which is a time-sensitive test.
So indeed the failure seems unrelated to your changes and due to a timing issue. I assume the last force-push did not change anything?

[mrexodia]

Yeah the last force push was just to rebase on master, nothing else was changed.

[ccadar]

Glad to see this merged! Thanks again, @mrexodia, and also @arrowd.

[mrexodia]

🥳