Authors: Peiyi Sun && Dexin Liu
This is a pointer analysis framework for Java, based on Soot analysis framework. Actually, it is the first project for course Software Analysis in Fall 2018.
This work is mostly based on Points-to Analysis for Java Using Annotated Constraints[1], published in 2001 on Oopsula. This is a general-purpose points-to analysis for Java based on Anderson's points-to analysis for C, with constraint-based approach that employs annotated inclusion constraints. It's shown in the paper that it models virtual calls and object fields precisely and efficiently.
In the subsection below, we'll illustrate some basic principles of the whole method.
To solve the problem, we first need annotated set-inclusion constraints of the form
The nodes in the graph can be classified as variables, sources, and sinks. The graph only contains edges of the following forms:
We use annotated constraint graphs based on the inductive form representation. The graphs are represented with adjacency lists
The system is solved by computing the closure of the graph under the following transitive closure rule:
TRANS $$ If \begin{cases} <L,a> \in pred(v) \ <R,b> \in succ(v)\ Match(a,b) \end{cases} $$
The new transitive constraint is created only if the annotations of the two existing constraints “match”—that is, only if Match(a,b) holds.
Match Constraints $$ Match(a, b) = \begin{cases} true&if\ a\ or\ b\ is\ the\ empty\ annotation \ \epsilon \ true&if\ a=b\ false&othervise \end{cases} $$ The annotation of the new constraint is : $$ a○b = \begin{cases} a & if\ b=\epsilon\ b & if\ a=\epsilon\ \epsilon & otherwise \end{cases} $$
We use an example to show how to construct constraints for assignment statements. $$ <l = new\ o_i> \Rightarrow {ref(o_i, v_{o_i}, \overline v_{o_i}) \sub v_l } \ <l = r> \Rightarrow { v_r \sub v_l} \ <l.f = r> \Rightarrow { v_l \sub proj(ref, 3, u), v_r \sub_f u}, u\ fresh \ <l = r.f> \Rightarrow { v_r \sub proj(ref, 2, u), u \sub_r v_l}, u\ fresh $$ Through TRANS operation, we can derivate that $$ ref (o_2,v_{o2},\overline v_{o2})⊆ v_r $$
For every virtual call in the program, our analysis generates a constraint according to the following rule: $$ <l = r_0.m(r_1,...,r_k)>⇒ {v_{r0} ⊆_m lam(\overline 0,\overline {v_{r1}},...,\overline {v_{rk}},v_l)} $$ We use a precomputed lookup table to determine the corresponding run-time target method, based on the class of the receiver object.
For more details about the method, please refer to the paper.
Here we illustrate the code structure of our program.
src
|-- main
|--annotated_anderson_analysis #The handler part
|--constraint_graph_node #Structure of Graph Node
|--BasicConstraintGraphNode.java #Structure
|--ConstraintConstructor.java #Structure
|--ConstraintObjectConstructor.java #Structure
|--ConstraintVariable.java #Structure
|--ConstraintAnnotation.java #Structure for Annotation
|--ConstraintConvertUtility.java #Main part for convertion operation.
|--ConstraintGraph.java #Main part for graph operation.
|--LookUpTable.java #Structure for LookUpTable
In command line or terminal:
java –jar analyzer.jar [src][SomePackage.Main]
-
[src]: root path of project to analysis, including java, class files and rt.jar, jce.jar in Java 1.7 (depended by Soot).
-
[SomePackage.Main]: main class of project, including main function.