Java Points-to

Info

Full Name	Java Points-to Analysis Grammar
Class	Context-Free
Kind	Static Analysis
Version	4.0.0
Example download (.txt + .md)	.tar.gz
Origin	link

Grammar Parameters

Parameter	Description
\(\textit{fields}\)	List of fields \(f\) used in Java program for load/store operations

Grammar Template

\[\begin{split}\textit{PointsTo} \, &\rightarrow \, (\textit{assign} \, \mid \, \textit{load}_f \, \textit{Alias} \, \textit{store}_f)^{*} \, \textit{alloc} \, \\ \textit{Alias} \, &\rightarrow \, \textit{PointsTo} \, \textit{FlowsTo} \, \\ \textit{FlowsTo} \, &\rightarrow \, \overline{\textit{alloc}} \, (\overline{\textit{assign}} \, \mid \, \overline{\textit{store}}_f \, \textit{Alias} \, \overline{\textit{load}}_f)^* \, \\ &\forall \, f \, \in \, \textit{fields} \, \\\end{split}\]

Description

Java points-to analysis grammar generates language for the field-sensitive analysis of Java programs, which tracks the dataflow between heap objects that are stored in and loaded from fields \(f \in \textit{fields}\). Introduced in "Giga-scale exhaustive points-to analysis for Java in under a minute". The dataflow of the program is constructed from object creations, variable assignments, and load/store operations on fields.

Example Grammars

The Java points-to analysis grammar with \(\textit{fields} = [0, 1]\).

Pyformlang CFG:

S -> PTh alloc
PTh -> epsilon
PTh -> assign PTh
PTh -> load_0 Al store_0 PTh
PTh -> load_1 Al store_1 PTh
FT -> alloc_r FTh
FTh -> epsilon
FTh -> assign_r FTh
FTh -> store_0_r Al load_0_r FTh
FTh -> store_1_r Al load_1_r FTh
Al -> S FT

---