Stack Graphs via CFL Reachability

stack-graph-cfl-reachability.dl

// resolve names in stack graph by CFL reachability

.decl Node(x:symbol, id:symbol, act:symbol)
.decl Edge(id1:symbol, id2:symbol)

.decl Push(id1:symbol,id2:symbol,sym:symbol)
.output Push(IO=stdout,delimiter=",")

.decl Pop(id1:symbol, id2:symbol, sym:symbol)
.output Pop(IO=stdout,delimiter=",")

.decl Nop(id1:symbol, id2:symbol)
.output Nop(IO=stdout,delimiter=",")

.decl Out(id1:symbol, id2:symbol)
.output Out(IO=stdout,delimiter=",")

.decl S(id1:symbol, id2:symbol)
.output S(IO=stdout,delimiter=",")

.decl L(id1:symbol, x:symbol, id2:symbol)
.output L(IO=stdout,delimiter=",")

.decl R(id1:symbol, x:symbol, id2:symbol)
.output R(IO=stdout,delimiter=",")

.decl N(id1:symbol, id2:symbol)
.output N(IO=stdout,delimiter=",")

Out(ID1,ID2) :-
    S(ID1,ID2), Node(_,ID1,ACT1), Node(_,ID2,ACT2),
    contains("PUSH",ACT1), contains("POP",ACT2).

S(ID,ID) :- Node(_, ID, _).
S(ID1,ID4) :- L(ID1,X,ID2), S(ID2,ID3), R(ID3,X,ID4).
S(ID1,ID3) :- S(ID1,ID2), S(ID2,ID3).

L(ID1,X,ID4) :- N(ID1,ID2), Push(ID2,ID3,X), N(ID3,ID4).

R(ID1,X,ID4) :- N(ID1,ID2), Pop(ID2,ID3,X), N(ID3,ID4).

N(ID,ID) :- Node(_,ID,_).
N(ID1,ID2) :- Nop(ID1,ID2).
N(ID1,ID3) :- N(ID1,ID2), N(ID2,ID3).

Push(ID1,ID2,X1) :-
    Node(X1,ID1,ACT1), Node(_,ID2,ACT2), Edge(ID1,ID2),
    contains("PUSH",ACT1), !contains("POP",ACT2).

Pop(ID1,ID2,X2) :-
    Node(_,ID1,ACT1), Node(X2,ID2,ACT2), Edge(ID1,ID2),
    !contains("PUSH",ACT1), contains("POP",ACT2).

Nop(ID1,ID2) :-
    Node(_,ID1,_), Node(_,ID2,_), Edge(ID1,ID2),
    !Push(ID1,ID2,_), !Pop(ID1,ID2,_).


// Figure 3 from the Stack Graphs paper
Node("x","x11","PUSH").
Node("$DOT","$DOT100","PUSH").
Node("$CALL","$CALL200","PUSH").
Node("B","B10","PUSH").
Node("x","x9","PUSH").
Node("$DOT","$DOT101","PUSH").
Node("B","B8","PUSH").
Node("$SCOPE","$SCOPE33","NOP").
Node("$SCOPE","$SCOPE32","NOP").
Node("$SCOPE","$SCOPE31","NOP").
Node("B","B6","POP").
Node("$CALL","$CALL201","POP").
Node("$DOT","$DOT103","POP").
Node("$SCOPE","$SCOPE41","NOP").
Node("$DOT","$DOT104","POP").
Node("$SCOPE","$SCOPE40","NOP").
Node("$DOT","$DOT105","PUSH").
Node("$DOT","$DOT106","PUSH").
Node("$CALL","$CALL202","PUSH").
Node("A","A7","PUSH").
Node("$SCOPE","$SCOPE30","NOP").
Node("$DOT","$DOT102","PUSH").
Node("a","a5","PUSH").
Node("b","b4","POP").
Node("$DOT","$DOT110","POP").
Node("$ROOT","$ROOT_a","ROOT").
Node("$ROOT","$ROOT_b1","ROOT").
Node("$ROOT","$ROOT_b2","ROOT").
Node("a","a1","POP").
Node("$DOT","$DOT107","POP").
Node("$SCOPE","$SCOPE10","NOP").
Node("A","A2","POP").
Node("$CALL","$CALL203","POP").
Node("$DOT","$DOT108","POP").
Node("$SCOPE","$SCOPE21","NOP").
Node("$DOT","$DOT109","POP").
Node("$SCOPE","$SCOPE20","NOP").
Node("x","x3","POP").

Edge("x11","$DOT100").
Edge("$DOT100","$CALL200").
Edge("$CALL200","B10").
Edge("B10","$SCOPE33").
Edge("$SCOPE33","$SCOPE32").
Edge("x9","$DOT101").
Edge("$DOT101","B8").
Edge("B8","$SCOPE32").
Edge("$SCOPE32","$SCOPE31").
Edge("$SCOPE31","$SCOPE30").
Edge("$SCOPE31","B6").
Edge("B6","$CALL201").
Edge("$CALL201","$DOT103").
Edge("$DOT103","$SCOPE41").
Edge("$SCOPE41","$SCOPE40").
Edge("B6","$DOT104").
Edge("$DOT104","$SCOPE40").
Edge("$SCOPE41","$DOT106").
Edge("$DOT106","$CALL202").
Edge("$CALL202","A7").
Edge("$SCOPE40","$DOT105").
Edge("$DOT105","A7").
Edge("A7","$SCOPE30").
Edge("$SCOPE30","$DOT102").
Edge("$DOT102","a5").
Edge("a5","$ROOT_b1").
Edge("$ROOT_b1","$ROOT_a").
Edge("$ROOT_b2","b4").
Edge("b4","$DOT110").
Edge("$DOT110","$SCOPE33").
Edge("$ROOT_a","a1").
Edge("a1","$DOT107").
Edge("$DOT107","$SCOPE10").
Edge("$SCOPE10","A2").
Edge("A2","$DOT109").
Edge("$DOT109","$SCOPE20").
Edge("A2","$CALL203").
Edge("$CALL203","$DOT108").
Edge("$DOT108","$SCOPE21").
Edge("$SCOPE21","$SCOPE20").
Edge("$SCOPE20","x3").