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
> Thanks,
> Cristi
>
> _______________________________________________
> LLVM Developers mailing list
> LLVMdev at cs.uiuc.edu http://llvm.cs.uiuc.edu
> http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev
>