Formally constructing Control Flow Graph

Question

Sto scrivendo un compilatore per progetto universitario e vorrei trasformare il mio Abstract Syntax Tree in un Control Flow Graph (CFG).

Sto pensando che i nodi (V) nel CFG dovrebbero essere nodi dall'AST. So algoritmicamente come costruire il set di bordo (G=(V,E)), ma Im avendo un momento difficile scrivere il processo un po 'più formale

Ho creato questo modello di stile scala di corrispondenza (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 
    } 

Quale deve corrispondere una struttura AST come:

(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 
) 

e fornire un edgeset come:

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

DotSrc

Chiunque ha ottenuto alcun suggerimento su come fare questo un po 'più formale di scala "pseudocodice"?

Im pensando qualcosa induttivo simile:

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

(il sopra sarebbe solo dare un albero e non un grafico anche se nessuno bordo dal bordo di allora-ramo di istruzione successiva, per esempio.)

EDIT :

Ho letto su kiama and dataflows per scala e mi piace l'approccio "succ" e "successivo" che usano. Ciononostante, sto attraversando un periodo difficile per ridurlo a una descrizione più formale, principalmente a causa dell'eccellente childAttr, s.next che nasconde alcuni dei dettagli che diventano brutti quando provo a specificarlo formalmente.

EDIT2:

che ho passato il drago Libro e "moderna Compiler Implementazione in ML", così come alcuni degli altri materiali da Learning to write a compiler e alcuni/più menzioni flusso di dati e del flusso di controllo, ma non tocca mai molto su COME creare il CFG in modo formale.

Edit3:

Via Kiama autore, Associate Professor Dr. Tony Sloane ho ricevuto qualche additional book references to look up.

Per quanto posso vedere, il "modo di farlo" di quei libri si basa su una "dichiarazione per" del programma più che sull'AST e si basa su Basic Block. Ottimo input comunque!

Answer 1

Se l'intenzione è creare semplicemente qualcosa che abbia un aspetto un po 'più formale, è possibile esprimere queste operazioni di corrispondenza come regole di inferenza utilizzando lo standard notation. Dovresti esprimerlo in termini di una singola fase di riduzione, piuttosto che ricorsivamente, perché allora è sufficiente continuare semplicemente ad applicare queste regole fino a quando non sarà più possibile applicarle.

Detto questo, questa definizione sta essenzialmente per dire esattamente la stessa cosa del codice scala.Se si vuole veramente fare qualcosa "formale" le proprietà necessarie per dimostrare sono:

• l'algoritmo di traduzione CFG termina sempre
• Sia che il vostro CFG è minima rispetto ad un dato ingresso AST
• Sull'esistenza è un CFG unico derivabile dal tuo algoritmo per un dato input AST (cioè non è non deterministico quale CFG produce).

Non penso che l'approccio ai blocchi di base (piuttosto che un approccio per-statement) sia necessariamente una cattiva idea. Sembra perfettamente ragionevole che se è possibile abbinare un blocco di base, è possibile scrivere una regola che faccia asserzioni sull'appartenenza ai set in base alla presenza di questa corrispondenza. Sembra che la definizione induttiva che hai iniziato a disegnare possa funzionare bene.

Un'altra cosa interessante potrebbe essere quella di cercare di mettere in relazione (formalmente) structured operational semantics e la vostra costruzione di CFG. Potrebbero esserci già dei lavori in quest'area, ma ho fatto solo una ricerca di Google rapida e non ho trovato alcuna relazione chiaramente stabilita tra i due, ma intuitivamente sembra che dovrebbe esistere.

Answer 2

Google's Closure Compiler implementa un Control-Flow Analysis che trasforma un AST per JavaScript in un grafico di flusso di controllo. Le idee per questa implementazione sono ispirate al documento: Declarative Intraprocedural Flow Analysis of Java Source Code.