Using equivalence checking to verify correctness of Java Ranger - sohah/VeritestingTransformations GitHub Wiki

We've been implementing a technique called veritesting for the Symbolic Pathfinder symbolic execution engine. We've implemented veritesting by

  1. constructing static summaries of multi-path regions
  2. when SPF runs into a previously-summarized region, it will instantiate and use the region summary instead of executing the multi-path region.

But how can we verify that a summary is equivalent to the multi-path region that it substitutes ? This is an important question because, if a summary contains semantics different from the multi-path region that it substitutes, SPF will symbolically execute a program that is different from the subject program. We attempt to answer this question by checking if the summary is equivalent to the multi-path region.

Description

Test Harness

Our equivalence-checking uses a test harness that looks like this:

    void testHarness(int in0) {
        int outSPF = SPFWrapper(v, in0);
        int outJR = JRWrapper(v, in0);
        checkEquality(v, outSPF, outJR);
    }

The SPFWrapper method attempts to run the multi-path region with veritesting turned off. The JRWRapper method attempts to run the multi-path region with veritesting turned on. Both SPFWrapper and JRWRapper run the multi-path region with input in0 and capture its output. Finally, checkEquality compares the outputs for equality.

How does the test harness give us equivalence-checking ?

The test harness is executed with its input parameter in0 set to be a fresh symbolic variable. The test harness first executes the SPFWrapper method. This causes a single path in the multi-path region to be executed with input in0. Next, on this same path, the test harness executes the JRWrapper method. Execution on this path through JRWrapper is forced to continue through branch(es) that satisfy the path condition created earlier by SPFWrapper. When execution on this path finishes through JRWrapper, the outputs of SPFWrapper and JRWrapper are compared for equality via outSPF and outJR. If the outputs are expressed as functions of their inputs, the outputs become symbolic and are compared for equality using the solver.

We continue running this test harness symbolically for all execution paths through it. If the outputs of SPFWrapper and JRWrapper could not be made unequal on any execution path through the test harness, then we can conclude that the code in JRWrapper is equivalent to the code in SPFWrapper.

SPFWrapper and JRWrapper wrap around the same multi-path region. But SPFWrapper executes the multi-path region with veritesting turned off and JRWrapper executes it with veritesting turned on. Hence, if the outputs of SPFWrapper and JRWrapper could not be made unequal on any execution path through the test harness, we conclude that our multi-path region summary is equivalent to the multi-path region.

How do we avoid veritesting inside the SPFWrapper ?

The SPFWrapper method calls a method named NoVeritest which internally calls a testFunction method that contains the region. The NoVeritest method is specially named, Java Ranger will avoid veritesting inside any method that is a direct or indirect callee of NoVeritest. Java Ranger also doesn't veritest the NoVeritest method.

The JRWrapper method directly calls testFunction (which contains the region).

How can I write a equivalence-check for a region ?

  1. Create a new class which is a subclass of TestRegionBaseClass
  2. Implement the testFunction method to execute your multi-path region. testFunction must pass its inputs to the multi-path region and return the multi-path region's outputs as its return value. For now, the test harness assumes multi-path regions have a single output.
  3. Implement a main function in your class to create an instance of TestVeritesting, and call its runTest method with an instance of your class as an argument
    1. Create a jpf configuration file to run your class. It is easiest to simply copy Simple1.jpf and change the target to your class name on line 1.
    2. Optionally, specify the veritestRegionExpectedCount parameter in the jpf configuration to the number of instantiation of regions you expect in your multi-path region.

Here's a sample that can be run with the aforementioned Simple1.jpf.

class Simple1 extends TestRegionBaseClass {
    int testFunction(int in0, int in1, int in2, int in3, int in4, int in5,
                     boolean b0, boolean b1, boolean b2, boolean b3, boolean b4, boolean b5) {
        return simpleRegion(in0);
    }
    int simpleRegion(int x) {
        int count;
        if (x != 0) {
            count = 3;
        } else {
            count = 4;
        }
        return count;
    }
    public static void main(String[] args) {
        TestVeritesting t = new TestVeritesting();
        Simple1 s = new Simple1();
        t.runTest(s);
    }
}

What is veritestRegionExpectedCount ? How should I set a value for it in my equivalence-check ?

veritestRegionExpectedCount should be set to a integer value in the jpf configuration file. It should be set to the number of region instantiations you expect during the equivalence-check. The number of region instantiations will be the number of execution paths through the multi-path region multiplied by the number of regions in the multi-path region.

Related Work

Our test harness is a simpler implementation of the one presented by Ramos et al. We've assumed that all side-effects of the region can be captured in the return values of the SPFWrapper and JRWrapper functions. This simplification saves us the engineering effort of implementing a snapshot-restore mechanism in our test harness. Simultaneously, it allows us to construct a set of regression test cases that contain simple but useful regions.