[LLVMdev] vmkit and klee

[Cristian Zamfir]

Hi,

I am trying to evaluate how complex would be to modify KLEE ( http://klee.llvm.org/ 
  ) so that it can run LLVM bitcode compiled from Java code obtained  
with vmjc (from the VMKIT project). Your feedback will be very  
appreciated.

I am familiar with KLEE but I would like to know more about VMKIT, so  
please point me to the right docs/source code if appropriate.

After a quick look over VMKIT, I think that I would need to add  
support in KLEE for synchronization, exceptions, class loading,  
inheritance and maybe some simple garbage collection, since  
performance is not an issue.

Another problem seems to be that the bitcode depends on the core class  
libraries provided by Classpath.
I guess these would need to be compiled to LLVM and loaded by KLEE too  
but that would make the resulting LLVM bitcode huge. Do you have any  
suggestions for that?

Finally, is there a VMKIT tool that runs the *.bc output of vmjc, or  
the only option is to run jnjvm with the jar file? I think such a tool  
would be exactly what I need to take a look at.

Thanks,
Cristi