[klee-dev] Inline assembly, concurrency

[Marko Dimjašević]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20161104/9d614178/attachment.sig>