[klee-dev] Inline assembly, concurrency

[Andrew Santosa]

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ć<marko at cs.utah.edu> 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ć <marko at cs.utah.edu> .  University of Utah
https://dimjasevic.net/marko         . PGP key ID: 1503F0AA
Learn email self-defense!  https://emailselfdefense.fsf.org_______________________________________________
klee-dev mailing list
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev  
-------------- next part --------------
HTML attachment scrubbed and removed