Construcción formal del gráfico de flujo de control

Question

Escribo un compilador para el proyecto de la universidad y me gustaría transformar mi árbol de sintaxis abstracta en un gráfico de flujo de control (CFG).

Estoy pensando que los nodos (V) en el CFG deberían ser nodos del AST. Sé algorítmicamente la forma de construir el conjunto de borde (G=(V,E)), pero estoy teniendo dificultades para escribir el proceso un poco más formalmente

He creado este patrón de estilo de juego Scala (Pseudo):

def edges(n:Node)(nestedin_next: Node) : List[(Node,Node)] = 
    n match { 
     case (c_1 :: c_2::tl) => (c1,c2) :: edges(c2::tl)(nestedin_next)++ 
            edges(c_1)(c_2)//recurse 
     case c_1 :: Nil => (c_1,nestedin_next)::Nil 
     case i@ IF(_,c1,c2) => (i,c1)::(i,c2)::edges(c1)(nestedin_next)++ 
           edges(c2)(nestedin_next) 
     case _ => Nil 
    } 

Qué debe coincidir con una estructura como la AST:

(IF(1, 
     ASSIGN(x,1), // ia1 
     ASSIGN(x,2) // ia2 
    ) :: // i1 
    ASSIGN(y,2) :: // a1 
    ASSIGN(z,ADD(x,y)) :: //a2 
    IF(z, 
     RET(z), //i2r1 
     assign(z,0):: // i2a1 
     ret(z) // i2r2 
) :://i2 
    Nil 
) 

y proporcionar una edgeset como:

{ i1 -> ia1, 
    i1 -> ia2, 
    ia1 -> a1, 
    ia2 -> a1, 
    a1 -> a2, 
    a2 -> i2, 
    i2 -> i2r1 
    i2-> i2a1 
    i2a1 -> i2r2 
    i2r2 -> _|_ 
    i2r1 -> _|_ 
} 

DotSrc

Alguien tiene alguna pista sobre cómo hacer esto un poco más formal que Scala "pseudocódigo"?

Im pensando algo inductiva como:

e[[ IF(_,b1,b2) ]] = (if -> b1) + (if -> b2) \cup e[[ b1 ]] \cup e[[ b2 ]] 
e[[ b1, b2 ]] = e[[b1]] \cup e[[b2]] 

(la que sólo dan un árbol y no un gráfico, aunque n borde de la orilla del entonces rama en la próxima declaración de ejemplo anterior.)

EDITAR :

He estado leyendo en kiama and dataflows para scala, y me gusta el enfoque "succ" y "following" que usan. Sin embargo, me está costando mucho reducirlo a una descripción más formal, principalmente debido a la ingeniosa childAttr, s.next que oculta algunos de los detalles que se vuelven feos cuando intento especificarlo formalmente.

Edit2:

He pasado por el libro del dragón y "Compilador moderna implementación en ML", así como algunos de los otros materiales de Learning to write a compiler y algunos/menciona más flujo de datos y flujo de control, pero nunca toca mucho sobre CÓMO crear el CFG de forma formal.

Edit3:

Via Kiama autor, Associate Professor Dr. Tony Sloane he recibido alguna additional book references to look up.

Por lo que puedo ver, la "forma de hacerlo" según esos libros se basa en una "declaración" del programa más que en AST y se basa en los bloques básicos. ¡Gran entrada sin embargo!

Answer 1

Si su intención es simplemente crear algo que parezca un poco más formal, entonces podría expresar estas operaciones de coincidencia como reglas de inferencia usando el standard notation. Debe expresarlo en términos de un solo paso de reducción, en lugar de recursivamente, porque entonces es suficiente simplemente seguir aplicando estas reglas hasta que no se pueda aplicar más.

Dicho esto, esta definición esencialmente va a decir exactamente lo mismo que su código scala.Si realmente quiere hacer nada "formal" las propiedades que necesita para probar son:

• Su algoritmo de traducción CFG siempre termina
• Ya sea que su CFG es mínima con respecto a una entrada de AST dado
• Si hay es un derivado único de CFG por su algoritmo para una entrada determinada de AST (es decir, no es determinista qué CFG produce).

No creo que su enfoque de bloques básicos (en lugar de un enfoque por enunciado) sea necesariamente una mala idea, tampoco. Parece perfectamente razonable que si puede hacer coincidir un bloque básico, puede escribir una regla que haga afirmaciones sobre la membresía establecida en función de la presencia de esta coincidencia. Parece que la definición inductiva que comenzaste a dibujar podría funcionar bien.

Algo más interesante podría ser intentar relacionar (formalmente) structured operational semantics y su construcción de CFG. Puede que ya haya trabajo en esta área, pero solo realicé una búsqueda rápida en Google y no encontré ninguna relación clara entre los dos, pero intuitivamente parece que uno debería existir.

Answer 2

Google's Closure Compiler implementa un Control-Flow Analysis que transforma un AST para JavaScript en un gráfico de control-flujo. Las ideas para esta implementación están inspiradas en el documento: Declarative Intraprocedural Flow Analysis of Java Source Code.