I think this idea has a merit. If we replaced many library code even with
slightly different (or even slightly wrong) implementation in order to get the
KLEE-executable bc, then KLEE execution can remain symbolic for longer before
switching to concrete, potentially gaining better coverage.
Andrew
On Sat, Nov 5, 2016 at 4:36 AM, Marko Dimjašević<[email protected]> wrote:
Dear KLEE devs,
In an attempt to get KLEE working with a newer implementation of the
standard C library, I've been playing with Musl, which when compiled to
LLVM IR, unfortunately contains inline assembly code. That's a problem
for KLEE as it can't work with that.
In particular, Musl defines this function (in
arch/x86_64/atomic_arch.h):
#define a_cas_p a_cas_p
static inline void *a_cas_p(volatile void *p, void *t, void *s)
{
__asm__( "lock ; cmpxchg %3, %1"
: "=a"(t), "=m"(*(void *volatile *)p)
: "a"(t), "r"(s) : "memory" );
return t;
}
It makes KLEE stop analyzing a program that makes a call to this
function.
Given that KLEE at the moment doesn't support analyzing concurrent code,
and the function implements an atomic compare and swap, I was thinking I
could simply rewrite the a_cas_p function in C. I would lose atomicity,
but my hunch is it doesn't really matter as KLEE can't work on
concurrent code anyway.
Do you see any pitfalls with this idea? Maybe other suggestions on how
to handle situations in which inline assembly code exists?
--
Regards,
Marko Dimjašević <[email protected]> . University of Utah
https://dimjasevic.net/marko . PGP key ID: 1503F0AA
Learn email self-defense!
https://emailselfdefense.fsf.org_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
