Hi Andras, I think there are a few complicated things, mostly threads, garbage collection and some inline assembly that you will most likely need to emulate in Klee. I did not check how the LLVM bitcode for the jdk libraries looks like, but I expect you will not be able to execute all of it in Klee because some syscalls calls are not yet supported by Klee (including thread related functions). Perhaps you will end up adding various components from vmkit to Klee to get around many of the problems you will encounter.
To be clear, I am not saying running Java programs will be very hard, but my initial estimation was that it will not be easy. Please let me know if you already looked more into it, I would be interested to know more about this. Cristi On Thu, Feb 25, 2010 at 4:57 PM, Andreas Saebjoernsen <andreas at digitalplaywright.com> wrote: > Hi Cristi, > Given you experience it sounds like the design of Klee and/or vmkit makes it > so that this > task is quite prohibitive. I am curious though what in the vmkit bytecode > makes it different from > llvm-gcc bytecode with respect to Klee? > > thanks, > Andreas > > But Nicolas suggests generating a .so with vmkit and analyzing that > > On Tue, Feb 23, 2010 at 12:55 AM, Cristian Zamfir <cristian.zamfir at epfl.ch> > wrote: >> >> Hi Andreas, >> >> As a first step, you can check out this thread where I asked a similar >> thing on the llvm-dev list. >> http://lists.cs.uiuc.edu/pipermail/llvmdev/2009-August/024849.html >> >> My initial thoughts after looking at the llvm bitcode generated by vmkit >> were that you would need to modify Klee quite a bit to be able to analyze >> the llvm bitcode produced by vmkit, but it should be possible. >> >> Cristi >> >> >> On Feb 23, 2010, at 2:40 AM, Andreas Saebjoernsen wrote: >> >> > I am considering using Klee for analyzing Java code and I have a >> > question regarding >> > the feasibility of this. The reason why I am considering this is that it >> > seems like Klee >> > can take any llvm bytecode as input. VMKit is capable of producing llvm >> > bytecode for >> > java, which is what llvm-gcc produce as well, but on the Klee webpage >> > llvm-gcc is >> > listed as the only option for generating bytecode. That it is the only >> > option does not >> > have to mean too much, but at the same time I want to double check to >> > make sure >> > that I am not heading down the wrong path. >> > >> > Is there anything in Klee that makes it so that it can only analyze llvm >> > bytecode from >> > llvm-gcc or can it also be used to analyze the llvm bytecode produced by >> > llvm-vmkit? >> > >> > thanks, >> > Andreas >> > _______________________________________________ >> > klee-dev mailing list >> > klee-dev at keeda.stanford.edu >> > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >> > >
