search

javapathfinder / jpf-core

JPF is an extensible software analysis framework for Java bytecode. jpf-core is the basis for all JPF projects; you always need to install it. It contains the basic VM and model checking infrastructure, and can be used to check for concurrency defects like deadlocks, and unhandled exceptions like NullPointerExceptions and AssertionErrors.
535 stars 337 forks source link

Support java.nio #153

Open jtoman opened 6 years ago

jtoman commented 6 years ago

A lot of modern Java programs use the java.nio for IO operations. At the bare minimum, this means supporting the Paths, ByteChannels, and the bare minimum of the FileSystem functionality.

cyrille-artho commented 6 years ago

There has been work on older versions of net-iocache to support java.nio. Another extension, jpf-nas, takes a different approach for handling I/O. Without any adaptation, I/O operations face the problem that processes outside JPF are not backtracked when JPF backtracks. Is your idea in the context of plain jpf-core, or does it require an extension? How does it work before and after backtracking?

jtoman commented 6 years ago

What I've implemented so far faithfully recreates a read-only filesystem, and requires that processes outside of JPF don't mutate files accessed by the program. I'm surprised to hear about jpf-nas: it's not mentioned on the (cached) Trac page, nor can I seem to find a reference to it in this repo. It's possible my efforts on this are redundant.

cyrille-artho commented 6 years ago

Thanks, having support for a wider set of the read-only I/O API in jpf-core would be great. jpf-nas is on bitbucket: https://bitbucket.org/nastaran/jpf-nas It does not support java.nio, so your work can perhaps even be used together with jpf-nas. A unified version of net-iocache and jpf-nas with java.nio support has long been one of our goals, but we did not have the resources to achieve it so far.