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ć <ma...@cs.utah.edu> . University of Utah https://dimjasevic.net/marko . PGP key ID: 1503F0AA Learn email self-defense! https://emailselfdefense.fsf.org
signature.asc
Description: This is a digitally signed message part
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev