C Alias

Info

Full Name	C Alias 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{assigment_labels}\)	Pair \((a, \overline{a})\) where label \(a\) represents the assignment operation and \(a_r\) is reverse to it
\(\textit{dereference_labels}\)	Pair \((d, \overline{d})\) where label \(d\) represents pointer dereference relation and \(d_r\) is reverse to it

Grammar Template

\[\begin{split}S \, &\rightarrow \, \overline{d} \, V \, d \, \\ V \, &\rightarrow \, ((S \, \mid \, \varepsilon) \, \overline{a})^{*} \, (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 \(\textit{assigment_labels} = \{(\textit{a}, \textit{a_r})\}\) and \(\textit{dereference_labels} = \{(\textit{d}, \textit{d_r})\}\).

\[\begin{split}S \, \rightarrow \, \textit{d_r} \, V \, d \, \\ V \, \rightarrow \, V_1 \, V_2 \, V_3 \, \\ V_1 \, \rightarrow \, \varepsilon \, \\ V_1 \, \rightarrow \, V_2 \, \textit{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 \, \textit{d_r} \, V \, d \, \\ V \, \rightarrow \, ((S \, \mid \, \varepsilon) \, \textit{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))*