C Alias#

Info#

Full Name

C Alias Analysis Grammar

Class

Context-Free

Kind

Static Analysis

Origin

link

Grammar Parameters#

Parameter

Description

assigment_labels

Pair \((a, a_r)\) where label \(a\) represents the assignment operation and \(a_r\) is reverse to it

dereference_labels

Pair \((d, d_r)\) where label \(d\) represents pointer dereference relation and \(d_r\) is reverse to it

Grammar Template#

\[\begin{split}S \, &\rightarrow \, d_r \, V \, d \, \\ V \, &\rightarrow \, ((S \, \mid \, \varepsilon) \, a_r)^{*} \, (S \, \mid \, \varepsilon) \, (a \, (S \, \mid \, \varepsilon))^{*} \, \\\end{split}\]

Description#

C alias analysis grammar generates language for the flow-insensitive alias analysis of C programs. Introduced in “Demand-driven alias analysis for C”. The alias problem here is formulated as a context-free language (CFL) reachability problem over a graph representation of the assignments \(a\) and pointer dereference relations \(d\) in a program.

Example Grammars#

C Alias grammar with assigment_labels = \(\{(a, a_r)\}\) and dereference_labels = \(\{(d, d_r)\}\).

\[\begin{split}S \, \rightarrow \, d_r \, V \, d \, \\ V \, \rightarrow \, V_1 \, V_2 \, V_3 \, \\ V_1 \, \rightarrow \, \varepsilon \, \\ V_1 \, \rightarrow \, V_2 \, a_r \, V_1 \, \\ V_2 \, \rightarrow \, \varepsilon \, \\ V_2 \, \rightarrow \, S \, \\ V_3 \, \rightarrow \, \varepsilon \, \\ V_3 \, \rightarrow \, a \, V_2 \, V_3 \, \\\end{split}\]

Pyformlang CFG:

S -> d_r V d
V -> V1 V2 V3
V1 -> epsilon
V1 -> V2 a_r V1
V2 -> epsilon
V2 -> S
V3 -> epsilon
V3 -> a V2 V3
\[\begin{split}S \, \rightarrow \, d_r \, V \, d \, \\ V \, \rightarrow \, ((S \, \mid \, \varepsilon) \, a_r)^{*} \, (S \, \mid \, \varepsilon) \, (a \, (S \, \mid \, \varepsilon))^{*} \, \\\end{split}\]

Pyformlang RSA:

S -> d_r V d
V -> ((S | epsilon) a_r)* (S | epsilon) (a (S | epsilon))*

Recursive State Machine#

C Alias RSM 
start: S
[box S]
start: 0
final: 3
0 --d_r--> 1
1 --V--> 2
2 --d--> 3
[box V]
start: 0
final: 0, 1, 2, 3
0 --a--> 2
0 --a_r--> 0
0 --S--> 1
1 --a_r--> 0
1 --a--> 2
2 --a--> 2
2 --S--> 3
3 --a--> 2