Hi Cristian, I did not look into this in depth so I don't have any useful insights besides the ones you have already mentioned. At this point I think you have researched this more than I have.
thanks, Andreas On Tue, Mar 2, 2010 at 5:09 PM, Cristian Zamfir <cristian.zamfir at epfl.ch>wrote: > 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 > >> > > > > > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100307/d96f4b57/attachment.html
