Acyclic CFA reduction

[mira-alford]

Implements the acyclic cfa reduction transform from some old snippet of nicks thesis. Basically just flattens an acyclic, deterministic procedure in a single block.
Cheats a bit because we already have an SSA transform so we can skip some of the algorithm, yay!

[mira-alford]

Just noticed the tacked on simplify at the end messes it up by inlining things in a way that messes up the guards? Removing the simplify pass for now.

[katrinafyi]

Thanks for this, it's good! There are some small readability comments which are hopefully easy to fix.

Forgive me for my ignorance because I haven't read Nick's thesis, but I also have some questions.

I would really appreciate some module-level documentation about the purpose and idea of this transform. I think it's simple enough that I can guess the ideas, but it would be good to see it written out (at minimum, what is a CFA). Is there any reference you can link to?

Also, using fold_blocks_topo_fwd will amalgamate all of the edges from all blocks in the procedure, and it will not necessarily be in any sensible control-flow order (e.g., by dominators). Is this intentional and it won't cause any problems?

Edit: Ah, I guess it is sufficient to ensure that preds are all defined in the hashtbl before being accessed. However, the accumulation of final_edge is what is unexpected to me.

[katrinafyi]

term is too generic, a longer name like "termination_condition" would be better.

[katrinafyi]

Local open of BasilExpr can avoid some repetition

Suggested change

	List.fold_left
	(fun acc (in_edge, var) ->
	Expr.BasilExpr.ifthenelse
	(Expr.BasilExpr.rvar @@ Hashtbl.find term in_edge)
	(Expr.BasilExpr.rvar var) acc)
	(Expr.BasilExpr.rvar @@ snd hd)
	List.fold_left
	(fun acc (in_edge, var) ->
	let cond = Hashtbl.find term in_edge in
	Expr.BasilExpr.(ifthenelse (rvar cond) (rvar var) acc))
	(Expr.BasilExpr.rvar @@ snd hd)

I also add a local variable because I like to keep things in the local open as small as possible.

[katrinafyi]

There's a subtlety here that the block ID in hd is not used and it's just assumed to be the negation of everything else. Is this worth a comment?

Regardless, pattern matching on (_, hd_var) instead of hd will make this more clear and avoid the snd.

[katrinafyi]

I would prefer to factor out this filter (and avoid the repetition in the later inverse filter) by using a partition.

For example

      let guard_expressions, non_guard_stmts =
        Block.stmts_iter block |> Iter.to_list
        |> List.partition_map_either (function
          | Stmt.Instr_Assume { body; branch = true } -> Left body
          | stmt -> Right stmt)

This will also simplify the final list concats in this function.

[katrinafyi]

Suggested change

	List.empty proc
	[] proc

[katrinafyi]

Generally prefer pattern matching rather than explicit conditions. I've also inlined the preds definition because it's only used here.

Suggested change

	let preds = Procedure.blocks_pred proc id |> Iter.to_list in
	(* Compute reachability of this block. *)
	let reachable =
	(* Always reachable if no predecessors. *)
	if List.is_empty preds then Expr.BasilExpr.boolconst true
	(* Otherwise, reachability is ANY of the predecessors reachability. *)
	else
	Expr.BasilExpr.applyintrin ~op:`OR
	(preds
	|> List.filter_map (fst %> Hashtbl.get term)
	|> List.map Expr.BasilExpr.rvar)
	in
	(* Compute reachability of this block. *)
	let reachable =
	match Procedure.blocks_pred proc id |> Iter.to_list with
	(* Always reachable if no predecessors. *)
	| [] -> Expr.BasilExpr.boolconst true
	(* Otherwise, reachability is ANY of the predecessors reachability. *)
	| preds ->
	Expr.BasilExpr.applyintrin ~op:`OR
	(preds
	|> List.filter_map (fst %> Hashtbl.get term)
	|> List.map Expr.BasilExpr.rvar)
	in

[katrinafyi]

Just shadow proc to avoid accidentally re-using it.

Suggested change

	let out_proc =
	proc |> Procedure.iter_blocks |> Iter.map fst
	|> Iter.fold (fun acc id -> Procedure.remove_block acc id) proc
	in
	let out_proc, id = Procedure.fresh_block out_proc ~stmts:final_edge () in
	(* Make this the entry and return block. *)
	let out_proc = Procedure.set_entry_block out_proc id in
	Procedure.PG.map_graph
	(fun g ->
	Procedure.G.add_edge g (Procedure.Vert.End id) Procedure.Vert.Return)
	out_proc
	let proc =
	proc |> Procedure.iter_blocks |> Iter.map fst
	|> Iter.fold Procedure.remove_block proc
	in
	let proc, id = Procedure.fresh_block proc ~stmts:final_edge () in
	(* Make this the entry and return block. *)
	let proc = Procedure.set_entry_block proc id in
	Procedure.PG.map_graph
	(fun g ->
	Procedure.G.add_edge g (Procedure.Vert.End id) Procedure.Vert.Return)
	proc