Algorithm 11.1 Tabulation Algorithm

Input: Exploded supergraph $G^{\sharp}$ of a program.

Output: Solution to the realizable-path reachability problem.

1:declare PathEdge, WorkList, SummaryEdge: global edge set

2:Let $(N^{\sharp}, E^{\sharp}) = G^{\sharp}$

3:PathEdge := $\{(s_{main}, 0) \to (s_{main}, 0)\}$

4:WorkList := $\{(s_{main}, 0) \to (s_{main}, 0)\}$

5:SummaryEdge := $\emptyset$

6:ForwardTabulateSLRPs()

7:for each $n \in N^{*}$ do

8: $X_n$ := $\{d_2 \in D | \exists d_1 \in (D \cup \{0\})$ such that $(s_{procOf(n)}, d_1) \to (n, d_2) \in PathEdge\}$

9: // $procOf$ maps a node to the name of its enclosing procedure.

10:end for

11:

12:procedure Propagate( $e$ )

13:if $e \notin$ PathEdge then

14:Insert $e$ into PathEdge.

15:Insert $e$ into WorkList.

16:end if

17:end procedure

18:

19:procedure ForwardTabulateSLRPs()

20:while WorkList $\ne \emptyset$ do

21:Select and remove an edge $(s_p, d_1) \to (n, d_2)$ from WorkList.

22:if $n \in Call_p$ then

23:for each $d_3$ such that $(n, d_2) \to (s_{calledProc(n)}, d_3) \in E^{\sharp}$ do

24:Propagate( $(s_{calledProc(n)}, d_3) \to (s_{calledProc(n)}, d_3)$ )

25: // $calledProc$ maps a call node to the name of the called procedure.

26:end for

27:for each $d_3$ such that $(n, d_2) \to (returnSite(n), d_3) \in (E^{\sharp} \cup SummaryEdge)$ do

28:Propagate( $(s_p, d_1) \to (returnSite(n), d_3)$ )

29: // $returnSite$ maps a call node to its corresponding return-site node.

30:end for

31:else if $n = e_p$ then

32:for each $c \in callers(p)$ do

33: // $callers$ maps a procedure name to the set of call nodes that represents calls to that procedure.

34:for each $d_4, d_5$ such that $(c, d_4)\to (d_p, d_1) \in E^{\sharp}$ and $(e_p, d_2)\to(returnSite(c), d_5)\in E^{\sharp}$ do

35:if $(c, d_4) \to (returnSite(c), d_5) \notin$ SummaryEdge then

36:Insert $(c, d_4) \to (returnSite(c), d_5)$ into SummaryEdge.

37:for each $d_3$ such that $(s_{procOf(c)}, d_3) \to (c, d_4) \in$ PathEdge do

38:Propagate( $(s_{procOf(c)}, d_3) \to (returnSite(c), d_5)$ )

39:end for

40:end if

41:end for

42:end for

43:else if $n \in (N_p - Call_p - \{e_p\})$ then

44:for each $(m, d_3)$ such that $(n, d_2)\to (m, d_3) \in E^{\sharp}$ do

45:Propagate( $(s_p, d_1) \to (m, d_3)$ )

46:end for

47:end if

48:end while

49:end procedure