GaloisInc / crucible

Crucible is a library for symbolic simulation of imperative programs
683 stars 44 forks source link

Expand C lib support using `musl` implementations #486

Open robdockins opened 4 years ago

robdockins commented 4 years ago

MUSL is a smallish libc implementation for linux-based systems. We could probably make pretty good progress on expanding the amount of libc coverage we support by simply grabbing implementations piecemeal and linking them into bitcode files, similar to the way we link in support for libcxx. Obviously, anything that boils down into actually syscalls wouldn't work, but there are a lot of utility operations that simply invoke other primitives or can be directly implemented.

MUSL is nice for this purpose because it is released under an MIT license, which is highly compatible with our own ecosystem.

langston-barrett commented 3 years ago

As @travitch mentions on #911, another approach would be to write our own versions in C (or do so in cases where MUSL's implementations are unsuitable for whatever reason).

I think this certainly sounds like a good way to get more coverage, though there might be a complexity trade-off in that we'd have to worry about things like:

Some of these questions might have already been answered in the context of the libcxx bitcode.

langston-barrett commented 1 year ago

Yet another possible approach would be to write overrides in the Crucible-LLVM S-expression syntax, which avoids many of the downsides mentioned in my last comment.