y553546436/jpf-core

Computer hardware is susceptible to errors. For example, radiation may induce error to the hardware and some bit might be flipped. It is important to improve the resiliency of software against hardware errors. One way to evaluate the resiliency of software against hardware errors is by fault injection. The project uses Java PathFinder to systematically inject and explore bit-flip faults in the user specified variables in Java programs.

Java Pathfinder (JPF)

An extensible software model checking framework for Java bytecode programs

General Information about JPF

All the latest developments, changes, documentation can be found on our wiki page.

Building and Installing

If you are having problems installing and running JPF, please look at the How to install JPF guide.

We have documented on the wiki a lot of common problems that might occur during the installation and build processes as reported by the users. If you are facing any issue, please, make sure that we have not addressed it in documentation. Otherwise, feel free to contact us at [email protected] or open an issue on the Issue Tracker.

Documentation

There is a constant effort to update and add JPF documentation on the wiki. If you would like to contribute in that, please, contact us at [email protected].

Contributions are welcome and we encourage you to get involved with the community.

Happy Verification -- the Java PathFinder team

jpf-core's Issues

Finer-grained support for command line specified bit flips

Now we support to let command line arguments specify fields, parameters and local variables to flip, but the following features could be added for finer-grained command line control:

1. For fields and local variables, we can inject bit flips only in a specific write instruction (instead of all write instructions) by passing in a source location.
2. For parameters, we can inject bit flips only in a specific invoke instruction (instead of all invoke instructions) by passing in a source location.

The BitFlip annotation now does not work as local variables and fields annotations

Need to add this feature.

Support for command line argument to trigger the bit flips

If one can use command line argument for JPF to trigger the bit flips and specify the fields/variables/parameters to flip, then the source code need not be changed.

cannot handle multiple annotated parameters in one method

Now, the BitFlipListener reads the parameter annotations in a loop, breaks the loop if seeing a parameter annotated with @bitflip, and then inject bit flips to the parameter. However, in this way, it cannot properly handle multiple annotated parameters in one method such as:

public int foo (@BitFlip int a, @BitFlip int b) {
  return a+b;
}

The current BitFlipTest does not check that each bit is flipped exactly once

In the current BitFlipTest.java, the test checks that all the bits get flipped at least once but not that each bit is flipped exactly once.

Should add more tests

We should add more test cases:
1 and 2: what happens if we combine annotations and
command line options (in a redundant way or as to enable bit flips in two
values)?
3 and 4: what happens if we have bit flips for two values (two
annotations or two command line options)?
5: add a test for flip two bits of one value

JPF seems unable to handle local variable annotations

I added the logic to print local variable annotation information in the JPF listener and tried to run something like this in JPF:

public static void main(String[] args) {
  @BitFlip int a;
  int a=0;
}

The result shows that there is no AnnotationInfo for this local variable a. Therefore, our @bitflip annotation cannot work with local variables now.

Invoking getInt__II__I repeatedly always gets the same value

In method getBitFlip__JII__ (09c76f7#diff-33d0110f5af3cb68d26e778e457f72ff77d1f7b2707cdb0ea453d1574f46ca1bR437), I tried to generate nBit positions to flip by generating them one by one. However, it seems that if this method invokes getInt__II__I more than once, multiple invocations return the same result. When nBit=2, the return value of getBitFlip__JII__ is always 0, because the two flipping positions returned from getInt__II__I are the same and two flips of the same bit cancel out. I wonder what the mechanism is behind this and how to work around it so that I can use getInt__II__I multiple times in a getBitFlip__JII__ method.

If it is not easy to use getInt__II__I multiple times in a getBitFlip__JII__ method, I guess we can work around by invoking getInt__II__I only once to get a big number encoding a selection set of positions, and then decoding the number to get the actual positions to flip.