rocq/theories/Cfg.v

The control-flow graph (CFG) of a function and its dominators, transcribed from cfg.pl: func_cfg/2, cfg_idoms/2 (Cooper, Harvey and Kennedy, "A Simple, Fast Dominance Algorithm"), dom_children/3, dom_intervals/3 and dominates_by_interval/3. The validator asks "does A dominate B?" for every use of every temporary, and the dominator tree's preorder intervals answer it in constant time, as they do for ir.pl.

Parts

Gallina	cfg.pl
`jump_succs`	`jump_succs/2`
`cfg`, `func_cfg`	`func_cfg/2`, `reverse_postorder/6`
`cfg_idoms`	`cfg_idoms/2`, `label_idoms/5`, `common_dominator/5`
`dom_children`, `dom_intervals`	the same, `subtree_intervals/6`
`dominates_by_interval`	the same

Orders

cfg.pl keeps a block's successors and predecessors as ordsets, sorted in the standard order of terms. The model keeps a jump's own order and does not sort. That changes the reverse postorder, the order of the sweeps and the preorder numbers, but not the immediate dominators, which are unique, nor the relation dominates_by_interval states, which is all ir.pl reads from them.

Fuel

The Prolog recursions end because each visits a block at most once or walks up a finite tree; the Gallina ones carry fuel that bounds the same walk, and give no answer if it runs out, which a correct bound never lets happen. The bounds are noted at each.

From Stdlib Require Import String ZArith List Bool

From Nanofil Require Import Term Syntax Maps

Import ListNotations

Open Scope Z_scope

Option binding: let* x ≔ e in b is b with x the value of e, or none if e has none.

44Notation 'let*' x ':=' e 'in' b ≔ match e with Somex ⇒ b | None ⇒ None end (at level 200 , x name , e at level 100 , b at level 200)

The graph

As jump_succs(Jump, Succs): the labels the jump j can go to, in its own order, a poll edgepoll Fil-CA safepoint is a point where the thread may run signal handlers and answer the collector. The collector frees nothing the program can name there, but a handler the program installed may free an object under the rest of the program. A pollcheck is a safepoint on an edge: a jump target poll(L), a poll edge, runs one before going to L. Calls, allocations and some helpers are safepoints too (ir:evidence_preserving/1, ir:polls_every_cycle/1).'s included.

52Definition jump_succsj : jump : listname ≔

match j with

JGotot

⇒

edge_labelt

JBranch_ t₁ t₂

⇒

edge_labelt₁; edge_labelt₂

⇒

[ ]

As cfg(Entry, Rpo, Succs, Preds): a function's control-flow graph, over its block labels.

61Record cfg: Type ≔ mkCfg

cfg_entry	: name	the entry block's label
cfg_rpo	: listname	the labels reachable from the entry, in reverse postorder
cfg_succs	: nmaplistname	each block's successors
cfg_preds	: nmaplistname	each block's predecessors, unreachable ones included

As reverse_postorder(Ns, Succs, Seen0, Seen, Post0, Post): depth first from each of Ns in turn, a label's successors before the labels after it; Post has the reverse postorder in front of Post0. Along any chain of nested calls, each call but the last takes one element of some list the walk has met (the entry or a block's successors), and the last is on an empty list, so the fuel is two more than the number of edges.

75Fixpoint reverse_postorderfuel : nat ns : listname succs : nmaplistname seen : nmapunit post : listname : optionnmapunit × listname ≔

match fuel with

⇒

None

Sfuel′

⇒

match ns with

[ ]

⇒

Someseen, post

l :: ls

⇒

nm_meml seen

→

reverse_postorderfuel′ ls succs seen post

else

let* ss ≔ nm_findl succs in

let* r ≔ reverse_postorderfuel′ ss succs nm_addl tt seen post in

let seen₂, post₁ ≔ r in

reverse_postorderfuel′ ls succs seen₂ l :: post₁

As func_cfg(Blocks, Cfg): the graph of the blocks bs, whose entry is the first block; each block's predecessors include unreachable ones. No graph when an edge targets a label that is no block's, where label_preds/3 fails.

96Definition func_cfgbs : listblock : optioncfg ≔

match bs with

[ ]

⇒

None

entry :: _

⇒

let succs ≔ nm_of_listmapλb ⇒ b_labelb, jump_succsb_jumpb bs in

let edges ≔ flat_mapλb ⇒ mapλs ⇒ s, b_labelb jump_succsb_jumpb bs in

negbforallbλe ⇒ nm_memfste succs edges

→

None

else

let preds ≔

fold_left

λ m e ⇒

let ps ≔

match nm_findfste m with

Someps

⇒

None

⇒

[ ]

nm_addfste snde :: ps m

edges

nm_of_listmapλb ⇒ b_labelb, [ ] bs

let* r ≔ reverse_postorderSSlengthedges b_labelentry succs nm_empty [ ] in

SomemkCfgb_labelentry sndr succs preds

Immediate dominators

As labels_numbered(Labels, 0, Pairs): each label of ls with its position in the list, from 0.

115Definition labels_numberedls : listname : nmapZ ≔

sndfold_leftλacc l ⇒ fstacc + 1, nm_addl fstacc sndacc ls 0, nm_empty

As common_dominator(Num, Idom, A, B, Common): the nearest common dominator of the labels a and b in the tree of immediate dominators idom found so far, num being reverse postorder numbers. Walk up from the later of a and b until they meet. Each step moves one of them to its immediate dominator (idom), earlier in reverse postorder, so twice the number of labels is enough fuel.

124Fixpoint common_dominatorfuel : nat num : nmapZ idom : nmapname a b : name : optionname ≔

match fuel with

⇒

None

Sfuel′

⇒

name_eqba b

→

Somea

else

let* na ≔ nm_finda num in

let* nb ≔ nm_findb num in

nb <? na

→

let* a₁ ≔ nm_finda idom in

common_dominatorfuel′ num idom a₁ b

else

let* b₁ ≔ nm_findb idom in

common_dominatorfuel′ num idom a b₁

As label_idoms(Preds, Num, B, Idom0-Changed0, Idom-Changed): one step of a sweep, at the label b. Its immediate dominator becomes the common_dominator of its predecessors that have one so far, and the flag records whether it changed.

140Definition label_idomspreds : nmaplistname num : nmapZ fuel : nat st : optionnmapname × bool b : name : optionnmapname × bool ≔

let* st′ ≔ st in

let idom, changed ≔ st′ in

let* ps ≔ nm_findb preds in

match filterλp ⇒ nm_memp idom ps with

[ ]

⇒

None

first :: others

⇒

let* nw ≔

fold_left

λ acc p ⇒

let* c ≔ acc in

common_dominatorfuel num idom p c

others

Somefirst

match nm_findb idom with

Someold

⇒

name_eqbold nw

→

Someidom, changed

else

Somenm_addb nw idom, true

None

⇒

Somenm_addb nw idom, true

As idom_fixpoint(Labels, Preds, Num, Idom0, Idom): sweeps of label_idoms over the labels ls in reverse postorder until one changes nothing. A sweep changes an idom only to a label earlier in reverse postorder, and the sweeps settle within the graph's loop nesting depth plus two (Cooper, Harvey and Kennedy), so one more sweep than labels is enough fuel.

162Fixpoint idom_fixpointfuel : nat ls : listname preds : nmaplistname num : nmapZ cfuel : nat idom : nmapname : optionnmapname ≔

match fuel with

⇒

None

Sfuel′

⇒

let* r ≔ fold_leftlabel_idomspreds num cfuel ls Someidom, false in

let idom₁, changed ≔ r in

changed

→

idom_fixpointfuel′ ls preds num cfuel idom₁

else

Someidom₁

As cfg_idoms(Cfg, Idom): each reachable label of the graph g but the entry, with its immediate dominator, the nearest block every path from the entry to it passes through.

175Definition cfg_idomsg : cfg : optionnmapname ≔

match cfg_rpog with

[ ]

⇒

None

_ :: rest

⇒

let n ≔ lengthcfg_rpog in

let num ≔ labels_numberedcfg_rpog in

let* idom ≔ idom_fixpointSSn rest cfg_predsg num S2 × n nm_addcfg_entryg cfg_entryg nm_empty in

Somenm_removecfg_entryg idom

del_assoc(Entry, ...): the entry is its own idom only during the sweeps.

The dominator tree's intervals

As dom_children(Cfg, Idom, Kids): each reachable label's children in the dominator tree, the labels it is the immediate dominator of, in reverse postorder.

193Definition dom_childreng : cfg idom : nmapname : optionnmaplistname ≔

fold_left

λ acc l ⇒

let* kids ≔ acc in

match nm_findl idom with

Someparent

⇒

let* cs ≔ nm_findparent kids in

Somenm_addparent l :: cs kids

None

⇒

Somekids

revcfg_rpog

Somenm_of_listmapλl ⇒ l, [ ] cfg_rpog

As subtree_intervals(L, Kids, N0, N, Intervals0, Intervals): number the subtree at the label l in preorder from n0, giving each label its number and the last number of its subtree, and return the next free number. The tree's depth is at most the number of labels, the fuel.

208Fixpoint subtree_intervalsfuel : nat kids : nmaplistname l : name n₀ : Z ivs : nmapZ × Z : optionZ × nmapZ × Z ≔

match fuel with

⇒

None

Sfuel′

⇒

let* ks ≔ nm_findl kids in

let* r ≔

fold_left

λ acc k ⇒

let* a ≔ acc in

subtree_intervalsfuel′ kids k fsta snda

Somen₀ + 1, ivs

let n, ivs₁ ≔ r in

Somen, nm_addl n₀, n − 1 ivs₁

As dom_intervals(Cfg, Idom, Intervals): each reachable label's preorder number in the dominator tree and the last one of its subtree, its dominator interval.

224Definition dom_intervalsg : cfg idom : nmapname : optionnmapZ × Z ≔

let* kids ≔ dom_childreng idom in

let* r ≔ subtree_intervalsSlengthcfg_rpog kids cfg_entryg 0 nm_empty in

Somesndr

As dominates_by_interval(Intervals, A, B): the label a dominates b, both reachable: every path from the entry to b passes through a, which holds when b's preorder number lies in a's interval. A label dominates itself.

233Definition dominates_by_intervalivs : nmapZ × Z a b : name : bool ≔

match nm_finda ivs, nm_findb ivs with

Somepa, la, Somepb, _

⇒

pa ≤? pb && pb ≤? la

_, _

⇒

false

The dominator intervals of a function's blocks bs: func_cfg, cfg_idoms and dom_intervals in turn, as definitions_dominate/3 and stage_sources/4 compute them.

242Definition block_intervalsbs : listblock : optionnmapZ × Z ≔

let* g ≔ func_cfgbs in

let* idom ≔ cfg_idomsg in

dom_intervalsg idom