asil-1.2: src/CFGAst.ag
-- Control flow graphs of a program
--
-- Each graph has its unique id for association of meta-info
--
-- To find back-edges: Bread-first numbering: if already numbered the
-- node, then it's a backedge when that node's number is smaller than
-- that of the current node.
--
-- Also, try to sequentialize the CFG when generating code, such that
-- all branching instructions are of the Jump 0 kind.
--
TYPE Programs = [Program]
DATA Program | Program
graphs : CFGs
TYPE CFGs = [CFG]
DATA CFG | CFG -- control-flow graph of a method
id : Int -- unique identification
segs : Segments -- linear sequence of instrumentions + outgoing edges
TYPE Segments = [Segment]
DATA Segment | Segment
id : Int -- unique identification
nodes : Nodes -- linear sequence of instructions
branch : Code -- outgoing edges
TYPE Nodes = [Node]
DATA Node
| Pseudo -- pseudo nodes may contain additional code
id : Int -- unique identification
info : Pseudo -- match information
body : Codes -- inserted instrumentations
| Opaque -- an opaque instruction; implementation hidden
instr : Instruction
-- Information about pseudo-nodes in the control-flow-graph
DATA Pseudo
| Nop -- pseudo node without any specific meaning
| EnterBlock
| LeaveBlock
| FailBlock
| EnterFun
| LeaveFun
| FailFun
| BeginCall
| DoneCall
| FailedCall
| BeginCoerce
| DoneCoerce
| FailedCoerce
-- Abstract Machine Instructions
TYPE Codes = [Code]
DATA Code
| Nop -- no code
| Label id : Int -- jump destination
| Jump target : Int -- various forms of jumps
cond : JumpCond
| Switch default : Int -- default target
targets : {[Int]} -- jump targets
-- Jump conditions
DATA JumpCond
| None
| IfEq
| IfFalse
| IfGe
| IfGt
| IfLe
| IfLt
| IfNGe
| IfNGt
| IfNLe
| IfNLt
| IfNe
| IfStrictEq
| IfStrictNe
| IfTrue
| Jump