vmkit and klee

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

Hi Cristian,

Cristian Zamfir wrote:

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.
  
OK.

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.
  
Why would you need support in klee? Can't you run a .so while executing with klee? You can compile vmkit's jvm to a .so.

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?
  
So yeah, a .bc file generated by vmjc depends on the standard library compiled into a huge .so file (you can generate that .so file by typing make in the tools/vmjc/libvmjc directory). What's possible is to include in the application .bc file all its dependencies with the standard library. That's something vmkit currently does not do, but I don't see a real difficulty in supporting it.
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.

OK, that can be provided easily. Currently, you can generate a .exe file or a .so file. jnjvm first tries to load a .so of the application before looking at the .jar. Adding a .bc file that is jit-generated should not be difficult. I can try to look into that soon if you'd like.

Nicolas