Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for musl library #483

Closed
wants to merge 4 commits into from
Closed

Conversation

MartinNowack
Copy link
Contributor

Initial support for executing KLEE using musl library.
Similar to uclibc (--libc=uclib), use --libc=musllibc.

To be able to use it, put a link to the musllibc bc file into your Release+Asserts/lib directory.
This will be automated soon.

@mdimjasevic This should get you going. Please try it out.
If you see any issues, let me know.

@@ -1312,6 +1388,8 @@ int main(int argc, char **argv, char **envp) {
case UcLibc:
mainModule = linkWithUclibc(mainModule, LibraryDir);
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Replace the code with: mainModule = linkWithMusllibc(mainModule, LibraryDir); to use musllibc instead of uclibc for testing.

@MartinNowack
Copy link
Contributor Author

Here is the repository for the musl libc: https://github.com/MartinNowack/klee-musl
You find the build instructions here: https://github.com/MartinNowack/klee-musl/blob/klee_support/README.klee.md

By the way, test suite should pass if musl is selected as default library (See code comment).

@ccadar
Copy link
Contributor

ccadar commented Oct 18, 2016

Thanks, @MartinNowack ! @mdimjasevic, is this in line with what you were trying?

@@ -1157,6 +1160,79 @@ static llvm::Module *linkWithUclibc(llvm::Module *mainModule, StringRef libDir)
}
#endif


Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess you should guard it with "#ifndef SUPPORT_KLEE_UCLIBC"

@mdimjasevic
Copy link
Contributor

@ccadar : I believe it's very close, much closer than I managed to get it on my own!

However, I believe there are more changes to be done to KLEE to support Musl. You can see I make changes to more files than @MartinNowack in this pull request: mdimjasevic@367543b

This includes changes to configuration files in KLEE. I believe it's better to have them and not pretend Musl is KLEE-uClibc with a different location on the file system.

That being said, with a manual tweak or two after compiling this, I am able to run KLEE on the hostname utility. I wanted to confirm I can get rid of an earlier false bug due to a missing function implementation in KLEE-uClibc:

$ ~/research/klee-mnowack-support-for-musl/Release+Asserts/bin/klee -libc=musllibc -posix-runtime hostname -A
KLEE: NOTE: Using klee-musllibc : /home/marko/research/klee-mnowack-support-for-musl/Release+Asserts/lib/musllibc.bca
KLEE: NOTE: Using model: /home/marko/research/klee-mnowack-support-for-musl/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory is "/home/marko/research/klee/examples/hostname-3.18/hostname-3.18/klee-out-25"
Using STP solver backend
KLEE: WARNING ONCE: function "qsort" has inline asm
KLEE: WARNING ONCE: function "trinkle" has inline asm
KLEE: WARNING ONCE: function "__init_libc" has inline asm
KLEE: WARNING ONCE: function "cgt_init" has inline asm
KLEE: WARNING ONCE: function "__lockfile" has inline asm
KLEE: WARNING ONCE: function "__unlockfile" has inline asm
KLEE: WARNING ONCE: function "static_init_tls" has inline asm
KLEE: WARNING ONCE: function "__wait" has inline asm
KLEE: WARNING ONCE: function "__lock" has inline asm
KLEE: WARNING ONCE: function "__unlock" has inline asm
KLEE: WARNING ONCE: function "__do_orphaned_stdio_locks" has inline asm
KLEE: WARNING ONCE: function "ftrylockfile" has inline asm
KLEE: WARNING: undefined reference to function: endutent
KLEE: WARNING: undefined reference to function: getutent
KLEE: WARNING: undefined reference to function: klee_posix_prefer_cex
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: realpath
KLEE: WARNING: undefined reference to function: setutent
KLEE: WARNING: undefined reference to function: utmpname
KLEE: WARNING ONCE: calling external: syscall(218, 44423024)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: ERROR: /home/marko/research/klee-musl-mnowack/./arch/x86_64/atomic_arch.h:13: inline assembly is unsupported
KLEE: NOTE: now ignoring this error at this location

KLEE: done: total instructions = 316958
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

Therefore, I can get this running. I guess the particular error reported by KLEE is to say we'd need to do more massaging of KLEE-Musl by @MartinNowack.

@MartinNowack
Copy link
Contributor Author

@mdimjasevic I know, the configuration are still missing. But it is trivial to add. This patch is just a WIP.
You got me wrong with uclibc = musllibc, I wanted to say, it is already working as a drop-in replacement for uclibc if you replace manually the code, you see that the test suite successfully runs.
Another question, did you use the klee_support branch?

@mdimjasevic
Copy link
Contributor

@MartinNowack , yes, I used the klee_support branch.

@ccadar ccadar added the Feature Request New feature that should be implemented in KLEE label Jul 20, 2017
@ccadar ccadar added this to Extension in KLEE Extensions Jun 18, 2020
@ccadar
Copy link
Contributor

ccadar commented Jun 18, 2020

Given the age of the PR, I will close it, but place it in the Extensions project at https://github.com/klee/klee/projects/4, so that others can build up on it if there is interest.

@ccadar ccadar closed this Jun 18, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Feature Request New feature that should be implemented in KLEE
Projects
Development

Successfully merging this pull request may close these issues.

None yet

4 participants