Formally constructing Control Flow Graph

Question

Im writing a compiler for university project, and I would like to transform my Abstract Syntax Tree into a Control Flow Graph(CFG).

Im thinking that the nodes(V) in the CFG should be nodes from the AST. I know algorithmically how to construct the edge set (G=(V,E)) but Im having a hard time writing the process a bit more formally

I've created this scala style pattern matching (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
     }

Which should match an AST structure like:

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

and provide an edgeset like:

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

DotSrc

Anyone got any hints on how to do this a bit more formally than scala "pseudocode"?

Im thinking something inductive like:

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

(the above would only give a tree and not a graph though. No edge from edge of then-branch to next statement for example)

EDIT:

I've been reading up on kiama and dataflows for scala, and I like the "succ" and "following" approach they use. Nevertheless, I'm having a hard time boiling that down into a more formal description, mostly because of the nifty childAttr, s.next which hides some of the details that turns ugly when I try to specify it formally.

EDIT2:

I've been through the Dragon Book and "Modern Compiler Implementation in ML" as well as some of the other material from Learning to write a compiler and some/most mentions data flow and control flow, but never touches much upon HOW to create the CFG in any formal way.

EDIT3:

Via Kiama author, Associate Professor Dr. Tony Sloane I recieved some additional book references to look up.

As far as I can see the "way to do it" as per those books is based on a "per statement" of the program more than over the AST and is based on Basic Blocks. Great input nevertheless!

Answer 1

If your intention is to simply create something that looks a bit more formal, then you could express these matching operations as inference rules using the standard notation. You should express it in terms of a single step of reduction, rather than recursively, because then it is sufficient to simply keep applying these rules until no more can be applied.

That said, this definition is essentially going to say exactly the same thing as your scala code. If you really want to do anything "formal" the properties you need to prove are:

• Your CFG translation algorithm always terminates
• Whether your CFG is minimal with respect to a given AST input
• Whether there is a unique CFG derivable by your algorithm for a given AST input (i.e. it's not non-deterministic which CFG it produces).

I don't think your basic blocks approach (rather than a per-statement approach) is necessarily a bad idea, either. It seems perfectly reasonable that if you can match a basic block, you can write a rule that makes assertions about set membership based upon the presence of this match. It seems like the inductive definition you started sketching could work just fine.

Something else interesting might be to try to relate (formally) structured operational semantics and your construction of CFGs. There might already be work in this area, but I only did a cursory google search and didn't find any clearly stated relationship between the two, but intuitively it seems like one should exist.