GoogleSummerOfCode Veritesting Project 2018

[sohah]

Veritesting for Symbolic PathFinder

Veritesting collapses paths of regions of code that could be summarized statically. This allows for less path exploration by dynamic symbolic execution, thus allowing dynamic symbolic execution to be used over larger programs.

Veritesting Design:

This implementation of Veritesting has a unique architecture and design, that is it has the following features:

1. Supproting an intermediate language: "RangerIR", which decompiles a CFG into an AST for later mainpulation by veritesting.
2. Allow different transformations over a veritesting region, which ensures transperency and enables reasoning about correctness and/or equivelance to the original program.
3. Enables high order regions, by de-referencing and inlining methods invocations.
4. Enables summarization of partial regions, allowing dynamic symbolic execution to only explore pieces of code that could not be statically summarized.
5. Supports SSA for fields that allows the summarization of nested fields.

Veritesting Transformations

This veritesting project uses WALA as the static analysis engine to summarize regions of code. Summarization is done through different transformations applied on the initial Control Flow Graph, CFG, obtained by WALA. These transformations are:

1. CFG to AST Transformation: this is done by walking the CFG and creating a corresponding statement in RangerIR, at the end of this transformation a StaticRegion along with all its environment tables, input table, output table, var to slot table and variable type table.
2. Gamma Creation Transformation: this should be considered as a subtransformation of the previous tranformation where at the end of this transformation, phi instructions, are replaced by a Gamma instruction that captures the condition under which assignments of values are taken.
3. Substitution Transformation: in this transformation, constants and inputs are populated into the region, at the end of this transformation a DynamicRegion is generated that represents an instance
4. Field Transformation: in this transformation, an SSA for fields is created to allow summarization of fields. At the end of this transformation, all "get" and "put" instructions should disappear leaving only field variables and assignment statements to them.
5. High Order Regions Transformation: in this transformation, method invocations are resolved and the intended method is inlined with the original region. At the end of this transformation, there should be no invoke instructions, instead, in their position, the method being invoked is inlined at that part.
6. SPFCases Transformations: This is two pass transformation, in the first pass, SPFCase statements are created for insturctions that are are hard to statically summaries and requires SPF exploration. In the second pass of this transformation SPFCases disappears only keeping a record of their predicates, leaving only instructions that could be statically summarized. At the end of this transformation, the Dynamic Region will be populated with the propriate SPFCase predicates, to account for all paths that requires SPF exploration, also all SPFCases statements are removed from the region statement.
7. Uniquness Transformation: in this transformation variable names are made unique to avoid conflicts that could result from hitting the same region again, i.e., inside a loop, but with different instantiated values.
8. Linearilization: in this transformation if-statements collapse by merging the statements of its "then" and the "else" sides. The idea being assignment of different variables are already reflected in the Gamma expressions and therefore if-statements are not longer needed.
9. To Green Expression Transformation: in this transformation, statements in the dynamic region are translated to Green expression and they should be ready to populate SPF accordingly.

This design that have the following benefits:

1. Ensures transperancy of different Veritesting steps/transformations.
2. Allows for checking invariants after each transformation.
3. Increases the oppurtunties over regions where veritesting could be applied.

Veritesting Documentation

For information about Java Documentation of the project please refer to https://sohah.github.io/VeritestingTransformations/.

Getting Started

In order to start using this project, you need to do the following:

1. Install Wala from https://github.com/wala/WALA.
2. Install JPF from https://github.com/javapathfinder/jpf-core .
3. Clone master branch for Veritesting.
4. Run ant for SPF.
5. Create your programs and .jpf files configured to use "VeritestingListener"
6. Run and watch different transformations as they happen, and observe the number of paths with and without VeritestingListener.

Walk-Through Example

Suppose you want to run veritesting over simpleRegion below, which invokes "staticMethod1". Veritesting attempts to summarize the region starting from the if statement, including the invoked method. The methods are as follows:

public static int simpleRegion(int y) {
        int methodCount = 0;
        if (y > 100)
            methodCount = staticMethod1(y);

        assert((y > 100)? (methodCount == 1): (methodCount == 0));
        return methodCount;
    }

public static int staticMethod1(int x) {
        int myCount = 0;
        if (x > 0) {
            myCount = 1;
        } else {
            myCount = 2;
        }
        return myCount;
    }

Veritesting first attempts to construct a RangerIR statement from the cfg, creating the following:

if ((! (<= @w1 100 ) )) {
   6 = invokestatic < Application, LVeritestingPerf, staticMethod1(I)I > 1 @9 exception:5
} else {
   skip; 
}
@w7 := (Gamma !(@w1<=100) @w6 0); 

and

if ((<= @w1 0 )) {
   skip; 
} else {
   skip; 
}
@w6 := (Gamma @w1<=0 2 1); 
return 6

The both regions, go through a number of transformations including populating the environment and inlining the invoked method to obtain:

if ((! (<= y 100 ) )) {
   if ((<= y 0 )) {
      skip; 
   } else {
      skip; 
   }
   @w612 := (Gamma y<=0 2 1); 
   skip; 
   @w62 := @w612; 
} else {
   skip; 
}
@w72 := (Gamma !(y<=100) @w62 0); 

which finally translates a Green expression and placed on SPF path condition.
Note that the above code will actually cause the assertion in simpleRegion to fail, if the assertion is changed to myCount ==2 instead of myCount ==1, then the assertion will pass. This shows that the semantics of the program is maintained at least in this program.

To see the complete output please check out it out here
output.txt

My Contribution

My contribution in this project could be found on github pushes and below as a list of commits. These contributions mainly fall under one of these categories:

1. Created intial version of the RangerIR as well as creation of an initial version of translating the CFG to AST.
2. Implemented Substitution Transformation.
3. Implemented Uniquness Transformation.
4. Implemented SPFCases Transformation.
5. Implemented High Order Region Transformation for static methods, to support dynamic dispatch of methods, requires field transformation , which is currently a work in progress.
6. Built up of the Static Region and the Dynamic Region, and populating their environments, this includes input table, output table, var type table, var slot table and var value table.
7. Participated in the ToGreen transformation, by generating the appropriate Green vars depending on the type.
8. Provide the machinary of checking symbolic regions, and setting up SPF to reflect the summarized region.
9. I managed to get Veritesting running on WBS and passing/failing assertions in correspondence with SPF behavior.

Remaining Work

There are some implementation that I still need to do, these are:

1. Adding choice generators to support SPFCases, test its functionality.
2. Supporting high order regions for dynamic dispatch methods and also test it on depth more than 2.
3. Adding and checking invariants after each transformation.
4. Run performance measurement.

List of Commits

a457f34 - pushing wbs assertion passing
1650368 - pushing javaDoc
2d93e0c - pushing high order region
6222720 - pushing initial version of high order region
62ab4c0 - changing the prefix of wala variables
5d493e2 - removing StackSlotTypeTable
0b75a9e - adding support for checking symbolic region based on the expression
7a4dbef - pushing wbs with .jpf file for update method instead of launch
8dbf778 - adding boundaries to static region computation
07ddc1a - pushing boundary computation for the region tables
a11bea2 - adding back commented GetSubstitutionVisitor
b7a915f - fixing issue #1 and #3
6586c6c - removing stack slot type table and rely only on the VarTypeTable to get the type for vars
2746f0c - Merge remote-tracking branch 'origin/master' into fixingPair
b417bb5 - adding pair class as a veritesting util
7810b89 - allow inputs to be bounded to the region
d01c6c1 - fixing a bug in the uniquness where appending is done in decending order
96152cc - fixing getting number of the WalaExprVar, plus fixing the output table to include only for the bounderies of the region
e65f013 - using type table instead of the slot type table, soon I need to git rid of the slot type table.
55ad32c - fixing exploration of blocks if an exception was raised while attempting to make a region
f39ac59 - fixing ValueSymbolTable to become local to field substitution, because it is really needed for substitution and shouldn't be used later or kept in the DynamicRegion
f2c966f - restructuring and fixing field ref type exploration for getStatic
155e996 - 1. adding static type for vars 2. some file restructuring
f02e62c - fixing type error in new TypeTable
3f9f02e - fixing merging conflicts
3e8be44 - making StaticRegion input, output param/slot tables generic for region and methodRegions
d6cefe5 - fixing merging issues
afe6b1b - allowing SPFCases to generate a new DynamicRegion, fixing typing error for IfThenElse in SPFCases
f6a0462 - fixing invocation of SPFCases
bf076d2 - adding SPFCases first and second passes
96d71e7 - adding pass1 and pass2 to SPFCases
711e38c - baseline 1
840e35c - not veritesting concerte condition and popping of stack when we veritest
16239a2 - not failing when constants are not supported
4e29fb7 - pushing fix to transform a skip to true
0bc8cd2 - pushing minor fixes for exceptional cases
3be17b5 - adding fixes for types, minor fix in the ToGreenVisitor plus the population of the stack slots of the region output
ed5bf40 - Merge branch 'master' of https://github.com/sohah/VeritestingTransformations
0bd66be - setting up path condition
e1a59fb - propagating endIns in dynamic region plus finishing up code for populating vairables and skipping to the next instruction after the region
3d1788e - fixing merging problems
2eaaeed - adding linearlization transformation
502dae8 - fixing substitution for gamma
e6ab4de - adding region input table seperately and allowing the substitution to happen over the input table and wala constants only
2c25492 - pushing fixes for constants finding
5b0d273 - fixing merging problems and intellij problems
86fd710 - Merge branch 'master' of https://github.com/sohah/VeritestingTransformations
962e4c9 - fixing static-dynamic region relation plus finishing up uniqueness of dynamic regions.
6381de9 - pushing prints
6920083 - printing new region statement after uniquness pass
cf05d88 - initial version of region uniquness plus restructuring of the environment tables
7a211e7 - changing order of printing
8210f19 - handling case where SPF cannot recognize the type
3884faa - fixed untracked files
175b95e - printing type table
a572192 - fixing output of the region
c2badbd - fixing var output of a region
97c041a - commenting out region output
3ffafa2 - adding initial version of regionOutput computation
ddeafa5 - merging to master
fbb5b07 - pushing SPFCases and Dynamic region creation
36f0330 - seperating static region and dynamic region, where the later is the substituted version of the the static region with it variable valueTable filled out
e01262f - adding some print out messages
ef2d282 - adding an initial version of SPFCases for handling object creation and throw isntructions
80e2e42 - push some code clean up
6275ac2 - changing phi stack propagation to be more structured
d894d91 - adding protected in prettyPrintVisitor
e4af1ed - Finishing substitution
a2eee91 - adding substitution machinary
1f3f6ba - some merging changes including some clean up and plus extending IfThenElseStmt with the original instruction.
aac2c66 - adding stack slot discovery, plus changing the region to be a class of stmt and a symbol table instead of just stmt
03b4a08 - adding Wala Instruction AST
e124330 - adding comments and handling the case where invoke instructions has no result
74cc3c6 - adding gitignore
3924474 - removing classes
6294eb7 - fixing the call of transform for IfThenElse case to stop at the ipdm
b8c28f1 - removing build folder
c067838 - changing translation of invoke instruction
46d79ac - fixing initial run plus adding emptyVars for initial transformation where variables are not yet defined
3ae785f - adding skip for empty blocks and exit block
6a33aeb - adding finished but untested AST Transformation
e56b98d - adding statement visitor and some renaming
e9378e4 - adding partial cfg to ast transformation
836c75e - adding instruction to VeritestingExpression translation
163b606 - adding VeritestingAST
9d162c3 - Merge branch 'master' of https://github.com/vaibhavbsharma/jpf-symbc-veritesting
7ea10d8 - Merge branch 'master' of https://github.com/vaibhavbsharma/jpf-symbc-veritesting