From 0b4751e544e73a5f29ff5a0b76890009a78590bc Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 10:10:49 +1000 Subject: [PATCH 01/39] stmts_of_aslp_block --- lib/transforms/aslp/aslp.ml | 17 +++++++++-------- lib/transforms/aslp/aslp_state.ml | 3 +++ 2 files changed, 12 insertions(+), 8 deletions(-) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index bea9f319..f8f91f32 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -69,10 +69,11 @@ let aarch64_intrin_of_stmt ?(include_failed = false) ?default_address : | _ -> None (** Inverse of {!aarch64_intrin_of_stmt}. *) -let stmt_of_aarch64_intrin : +let stmt_of_aarch64_intrin ?error : Bitvec.t * Bitvec.t * Attrib.attrib_map -> Program.stmt = fun (opcode, address, attrib) -> - let args = List.map Expr.BasilExpr.bvconst [ opcode; address ] in + let attrib = Option.fold (Fun.flip (StringMap.add ".error")) attrib error in + let args = Expr.BasilExpr.[ bvconst opcode; bvconst address ] in Stmt.Instr_IntrinCall { attrib; lhs = []; name = Aarch64Eval; args } (** Extracts the next Aarch64 intrinsic from the given list of statements, @@ -109,8 +110,7 @@ let insert_one_diamond ~proc dia = with_ids |> Diamond.iter_backwards |> Iter.fold (fun proc (id, successors, st) -> - let assume = Aslp_state.assume_of_aslp_block st in - let stmts = Option.to_list assume @ CCVector.to_list st.stmts in + let stmts = Aslp_state.stmts_of_aslp_block st in Procedure.add_block proc id ~stmts ~successors ()) proc and (first, _, _), (last, _, _) = Diamond.(first with_ids, last with_ids) in @@ -154,10 +154,11 @@ let transform_one_stmt (module I : Bincaml_ibi.IBI) ~proc bid = |> Procedure.add_goto ~from:bid ~targets:[ aslp_first ] in Some (proc, aslp_last) - | exception exn -> - let exn = `String (Printexc.to_string exn) in - let attrib = StringMap.add error_attrib_key exn intrin_attrib in - let intrin_stmt = stmt_of_aarch64_intrin (opcode, address, attrib) in + | exception error -> + let error = `String (Printexc.to_string error) in + let intrin_stmt = + stmt_of_aarch64_intrin ~error (opcode, address, intrin_attrib) + in let stmts = Vector.of_list (before @ (intrin_stmt :: after)) in Some (Procedure.modify_block proc bid (fun b -> { b with stmts }), bid) ) diff --git a/lib/transforms/aslp/aslp_state.ml b/lib/transforms/aslp/aslp_state.ml index 7701255c..89d3c689 100644 --- a/lib/transforms/aslp/aslp_state.ml +++ b/lib/transforms/aslp/aslp_state.ml @@ -229,6 +229,9 @@ let assume_of_aslp_block = function | { assume = body; _ } -> Some (Stmt.Instr_Assume { attrib = Attrib.empty; body; branch = false }) +let stmts_of_aslp_block ({ stmts } as st) = + Option.to_list (assume_of_aslp_block st) @ CCVector.to_list stmts + (** {1 Formatters} *) let show_aslp_block = show_aslp_block From 3e80e6a7d2f694b9304eeb3169b9f32259f56926 Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 10:40:50 +1000 Subject: [PATCH 02/39] starting flat_map_block but can't think --- lib/transforms/aslp/aslp_util_internal.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index a8569d07..497d3be2 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -32,3 +32,15 @@ let referenced_vars_of_prog = %> Iter.flat_map (fun (_, b) -> Iter.append (Block.read_vars_iter b) (Block.assigned_vars_iter b))) %> Iter.filter Var.is_global + +(** Maps the given block into a sequence of blocks, sequentially ordered in + control-flow. *) +let flat_map_block ~proc f bid = + let b = Procedure.get_block proc bid |> Option.get_exn_or "block not found" in + let new_blocks : (ID.t * _ Block.t) list = f b in + List.fold_left + (fun proc (bid, b) -> + let ({ attrib; phis; stmts } : _ Block.t) = b in + Procedure.add_block proc bid ~attrib ~phis ~stmts:(Vector.to_list stmts) + ()) + proc new_blocks From 66166bc2e01510cbc82a666eb87e28f25b4fe67e Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 14:31:15 +1000 Subject: [PATCH 03/39] isolate_stmts_of_block plan: - writing isolate function is too hard? - flat_map : stmt -> (proc * id * id | block | stmt) --- lib/transforms/aslp/aslp_util_internal.ml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 497d3be2..2f54e1e4 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -33,8 +33,22 @@ let referenced_vars_of_prog = Iter.append (Block.read_vars_iter b) (Block.assigned_vars_iter b))) %> Iter.filter Var.is_global -(** Maps the given block into a sequence of blocks, sequentially ordered in - control-flow. *) +(** Isolates statements satisfying the given predicate into their own block, + while maintaining sequential control-flow between them. *) +let isolate_stmts_of_block ?(label = "%singleton") ~proc f bid = + let b = Procedure.get_block proc bid |> Option.get_exn_or "block not found" in + let stmts = b.stmts |> CCVector.to_list in + + let block_stmts = + List.group_succ ~eq:(CCFun.compose_binop f Bool.equal) stmts + |> List.flat_map (function + | hd :: _ as xs when f hd -> List.map List.pure xs + | xs -> List.pure xs) + in + 2 + +(** Maps each statement inside the given block ID into a sequence of blocks, + then links those blocks sequentially in control-flow. *) let flat_map_block ~proc f bid = let b = Procedure.get_block proc bid |> Option.get_exn_or "block not found" in let new_blocks : (ID.t * _ Block.t) list = f b in From a065b1c84a20cd57e9a035d11bbe0c81ca4ccfdc Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 15:13:56 +1000 Subject: [PATCH 04/39] isolate_stmts_of_block probably works now --- lib/transforms/aslp/aslp_util_internal.ml | 40 ++++++++++++++++++++--- 1 file changed, 36 insertions(+), 4 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 2f54e1e4..4755b45f 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -36,16 +36,48 @@ let referenced_vars_of_prog = (** Isolates statements satisfying the given predicate into their own block, while maintaining sequential control-flow between them. *) let isolate_stmts_of_block ?(label = "%singleton") ~proc f bid = - let b = Procedure.get_block proc bid |> Option.get_exn_or "block not found" in - let stmts = b.stmts |> CCVector.to_list in + let stmts = + Procedure.get_block proc bid |> Option.get_exn_or "block not found" + |> fun b -> CCVector.to_list b.stmts + in - let block_stmts = + (* Group, then flatten isolated statements into their own list. *) + let (grouped_stmts : _ Stmt.t list list) = List.group_succ ~eq:(CCFun.compose_binop f Bool.equal) stmts |> List.flat_map (function | hd :: _ as xs when f hd -> List.map List.pure xs | xs -> List.pure xs) in - 2 + + (* Insert disconnected blocks for each group, reusing [initial_bid] for the first group. *) + let proc, block_ids = + List.fold_map_i + (fun proc i stmts -> + let proc, bid = + if i = 0 then + ( Procedure.modify_block proc bid (fun b -> + { b with stmts = CCVector.of_list stmts }), + bid ) + else Procedure.fresh_block proc ~name:label ~stmts () + in + (proc, bid)) + proc grouped_stmts + in + + let proc = + match List.last_opt block_ids with + | Some to_ -> Procedure.transplant_outgoing_edges proc ~from:bid ~to_ + | None -> proc + in + + match block_ids with + | [] -> proc + | hd :: tl -> + List.fold_left + (fun (proc, from) next -> + (Procedure.add_goto proc ~from ~targets:[ next ], next)) + (proc, hd) tl + |> fst (** Maps each statement inside the given block ID into a sequence of blocks, then links those blocks sequentially in control-flow. *) From d6c9ce9fb3eeac4148b07f2459d58fdd6dc0b701 Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 17:00:20 +1000 Subject: [PATCH 05/39] touch --- lib/transforms/aslp/aslp_util_internal.ml | 21 +++++++++------------ 1 file changed, 9 insertions(+), 12 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 4755b45f..64ec1102 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -49,19 +49,16 @@ let isolate_stmts_of_block ?(label = "%singleton") ~proc f bid = | xs -> List.pure xs) in - (* Insert disconnected blocks for each group, reusing [initial_bid] for the first group. *) + (* Insert disconnected blocks for each group, reusing [bid] for the first group. *) let proc, block_ids = - List.fold_map_i - (fun proc i stmts -> - let proc, bid = - if i = 0 then - ( Procedure.modify_block proc bid (fun b -> - { b with stmts = CCVector.of_list stmts }), - bid ) - else Procedure.fresh_block proc ~name:label ~stmts () - in - (proc, bid)) - proc grouped_stmts + grouped_stmts + |> List.fold_map_i + (fun proc i stmts -> + if i = 0 then + let stmts = CCVector.of_list stmts in + (Procedure.modify_block proc bid (fun b -> { b with stmts }), bid) + else Procedure.fresh_block proc ~name:label ~stmts ()) + proc in let proc = From 2ae82edfa697f0e9b58b45e00841afbbc6634103 Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 21:57:39 +1000 Subject: [PATCH 06/39] stash --- lib/lang/block.ml | 2 +- lib/transforms/aslp/aslp_util_internal.ml | 84 ++++++++++++++++++++--- 2 files changed, 74 insertions(+), 12 deletions(-) diff --git a/lib/lang/block.ml b/lib/lang/block.ml index 732ce134..0233d0c1 100644 --- a/lib/lang/block.ml +++ b/lib/lang/block.ml @@ -106,7 +106,7 @@ let map ~phi f (b : ('v, 'e) t) : ('vv, 'ee) t = { stmts = Vector.map f b.stmts; phis = phi b.phis; attrib = b.attrib } (** Modify stmt list by creating a mutable copy of the underlying vector *) -let fmap_stmts_copy (f : (('a, 'a, 'b) Stmt.t, 'c) Vector.t -> unit) b = +let fmap_stmts_copy (f : (('a, 'a, 'b) Stmt.t, 'mut) Vector.t -> unit) b = let v = Vector.copy b.stmts in f v; { b with stmts = Vector.freeze v } diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 64ec1102..c41686d6 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -76,14 +76,76 @@ let isolate_stmts_of_block ?(label = "%singleton") ~proc f bid = (proc, hd) tl |> fst -(** Maps each statement inside the given block ID into a sequence of blocks, - then links those blocks sequentially in control-flow. *) -let flat_map_block ~proc f bid = - let b = Procedure.get_block proc bid |> Option.get_exn_or "block not found" in - let new_blocks : (ID.t * _ Block.t) list = f b in - List.fold_left - (fun proc (bid, b) -> - let ({ attrib; phis; stmts } : _ Block.t) = b in - Procedure.add_block proc bid ~attrib ~phis ~stmts:(Vector.to_list stmts) - ()) - proc new_blocks +(** Replaces uses of the old block ID with the new [(first, last)] block IDs. + The incoming edges to [old] will be redirected to [first] and the outgoing + edges of [old] will be rebased to originate from [last]. + + [first] and [last] may be the same. One or both of [first]/[last] may be the + same as [old]. If neither is the same as [old], [old] will be removed from + the procedure. *) +let replace_block ~old ~new_:(new_first, new_last) proc = + proc + |> Procedure.transplant_incoming_edges ~from:old ~to_:new_first + |> Procedure.transplant_outgoing_edges ~from:old ~to_:new_last + |> + if ID.equal old new_first || ID.equal old new_last then Fun.id + else Fun.flip Procedure.remove_block old + +let flat_map_stmts + (f : + proc:_ Procedure.t -> + _ Stmt.t -> + (ID.t * ID.t * _ Procedure.t, _ Stmt.t) Either.t) ~proc bid = + let stmts = + Procedure.get_block proc bid |> Option.get_exn_or "block not found" + |> fun b -> CCVector.to_list b.stmts + in + + let proc = + Procedure.modify_block proc bid (Block.fmap_stmts_copy CCVector.clear) + in + + let proc, block_id_pairs = + stmts + (* Map, while generating block names for bare statements returned by the mapping function. + Collects bare statements into a *mutable* vector for O(n) building. *) + |> List.fold_filter_map + (fun (basic_block, proc) stmt -> + match (basic_block, f ~proc stmt) with + (* emitting diamond with no previous basic block *) + | None, Left (first, last, proc) -> ((None, proc), Some (first, last)) + (* emitting diamond with previous basic block. emit that first. *) + | Some (prev_bid, vec), Left (first, last, proc) -> + ( ( None, + Procedure.modify_block proc prev_bid (fun b -> + { b with stmts = CCVector.freeze vec }) ), + Some (first, last) ) + (* collecting bare statement with no previous basic block. make a block. *) + | None, Right s -> + let proc, bid = Procedure.fresh_block proc ~stmts:[] () in + ((Some (bid, CCVector.return s), proc), Some (bid, bid)) + (* collecting bare statement with previous basic block. *) + | Some (bid, vec), Right s -> + CCVector.push vec s; + ((Some (bid, vec), proc), None (* bid is already emitted *))) + (Some (bid, CCVector.create ()), proc) + |> function + | (Some (prev_bid, vec), proc), mapped -> + ( Procedure.modify_block proc prev_bid (fun b -> + { b with stmts = CCVector.freeze vec }), + mapped ) + | (None, proc), mapped -> (proc, mapped) + in + + + + proc + +let flat_map_blocks + (f : proc:_ Procedure.t -> ID.t -> _ Block.t -> ID.t * ID.t * _ Procedure.t) + proc = + Procedure.fold_blocks_topo_fwd + (fun proc bid block -> + let first, last, proc = f ~proc bid block in + proc |> replace_block ~old:bid ~new_:(first, last)) + proc proc From aee7b60e0fdc407e0fcbca74d22c1e6c1845b571 Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 23:04:02 +1000 Subject: [PATCH 07/39] it compiles --- lib/transforms/aslp/aslp_util_internal.ml | 99 +++++++++++++---------- 1 file changed, 58 insertions(+), 41 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index c41686d6..bb9210af 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -23,6 +23,16 @@ let span_while_some f = in step f [] +let[@tail_mod_cons] group_succ_either = + let[@tail_mod_cons] rec while_left xs = + let xs, rest = span_while_some Either.find_left xs in + Either.Left xs :: while_right rest + and[@tail_mod_cons] while_right xs = + let xs, rest = span_while_some Either.find_right xs in + Right xs :: (match rest with [] -> [] | _ -> while_left rest) + in + while_left + (** Iterates over global variables in the given program, including both read and assigned variables. Order is unspecified and may have duplicates. *) let referenced_vars_of_prog = @@ -95,51 +105,58 @@ let flat_map_stmts (f : proc:_ Procedure.t -> _ Stmt.t -> - (ID.t * ID.t * _ Procedure.t, _ Stmt.t) Either.t) ~proc bid = - let stmts = - Procedure.get_block proc bid |> Option.get_exn_or "block not found" - |> fun b -> CCVector.to_list b.stmts - in + (ID.t * ID.t * _ Procedure.t, _ Stmt.t) Either.t) ~proc base_bid = + let open Either in + let b = Procedure.get_block proc base_bid |> Option.get_exn_or "not found" in + let stmts = CCVector.to_list b.stmts and base_name = ID.name base_bid in - let proc = - Procedure.modify_block proc bid (Block.fmap_stmts_copy CCVector.clear) - in - - let proc, block_id_pairs = + (* Map, while generating block names for bare statements returned by the mapping function. *) + let (_, proc), mapped = stmts - (* Map, while generating block names for bare statements returned by the mapping function. - Collects bare statements into a *mutable* vector for O(n) building. *) - |> List.fold_filter_map - (fun (basic_block, proc) stmt -> - match (basic_block, f ~proc stmt) with - (* emitting diamond with no previous basic block *) - | None, Left (first, last, proc) -> ((None, proc), Some (first, last)) - (* emitting diamond with previous basic block. emit that first. *) - | Some (prev_bid, vec), Left (first, last, proc) -> - ( ( None, - Procedure.modify_block proc prev_bid (fun b -> - { b with stmts = CCVector.freeze vec }) ), - Some (first, last) ) - (* collecting bare statement with no previous basic block. make a block. *) + |> List.fold_map + (fun (bid, proc) stmt -> + match (bid, f ~proc stmt) with + | _, Left (first, last, proc) -> ((None, proc), Left (first, last)) | None, Right s -> - let proc, bid = Procedure.fresh_block proc ~stmts:[] () in - ((Some (bid, CCVector.return s), proc), Some (bid, bid)) - (* collecting bare statement with previous basic block. *) - | Some (bid, vec), Right s -> - CCVector.push vec s; - ((Some (bid, vec), proc), None (* bid is already emitted *))) - (Some (bid, CCVector.create ()), proc) - |> function - | (Some (prev_bid, vec), proc), mapped -> - ( Procedure.modify_block proc prev_bid (fun b -> - { b with stmts = CCVector.freeze vec }), - mapped ) - | (None, proc), mapped -> (proc, mapped) + let name = base_name in + let proc, bid = Procedure.fresh_block proc ~name ~stmts:[] () in + ((Some bid, proc), Right (bid, s)) + | Some bid, Right s -> ((Some bid, proc), Right (bid, s))) + (Some base_bid, proc) in - - - - proc + (* Collects adjacent bare statements into a basic block, and inserts those statements. *) + let proc, block_id_pairs = + group_succ_either mapped + |> List.fold_flat_map + (fun proc -> function + | Left pairs | Right ([] as pairs) -> (proc, pairs) + | Right ((bid, _) :: _ as pairs) -> + let stmts = CCVector.of_list (List.map snd pairs) in + ( Procedure.modify_block proc bid (fun b -> { b with stmts }), + [ (bid, bid) ] )) + proc + in + (* Transplant predecessors and successors of the original block as needed. *) + let proc = + proc + |> (match List.last_opt block_id_pairs with + | Some (_, to_) -> Procedure.transplant_outgoing_edges ~from:base_bid ~to_ + | None -> Fun.id) + |> + match List.head_opt block_id_pairs with + | Some (hd, _) when not ID.(equal hd base_bid) -> + Procedure.add_goto ~from:base_bid ~targets:[ hd ] + | _ -> Fun.id + in + (* Insert gotos between mapped blocks. This must happen after transplanting + so we do not transplant these edges. *) + List.combine_gen block_id_pairs (List.drop 1 block_id_pairs) + |> Iter.of_gen + |> Iter.fold + (fun proc (first, second) -> + let _, prev = first and next, _ = second in + Procedure.add_goto proc ~from:prev ~targets:[ next ]) + proc let flat_map_blocks (f : proc:_ Procedure.t -> ID.t -> _ Block.t -> ID.t * ID.t * _ Procedure.t) From a908d885b07f88634033ca4dd9f4698fdc36c6b4 Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 23:21:29 +1000 Subject: [PATCH 08/39] touch and fix base_bid stmts not being deleted --- lib/transforms/aslp/aslp_util_internal.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index bb9210af..1f204a1c 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -124,15 +124,22 @@ let flat_map_stmts | Some bid, Right s -> ((Some bid, proc), Right (bid, s))) (Some base_bid, proc) in + let proc = + Procedure.modify_block proc base_bid (Block.fmap_stmts_copy CCVector.clear) + in (* Collects adjacent bare statements into a basic block, and inserts those statements. *) let proc, block_id_pairs = group_succ_either mapped + |> List.filter_map (function + | Right ((bid, _) :: _ as pairs) -> Some (Right (bid, List.map snd pairs)) + | Right [] -> None + | Left _ as xs -> Some xs) |> List.fold_flat_map (fun proc -> function - | Left pairs | Right ([] as pairs) -> (proc, pairs) - | Right ((bid, _) :: _ as pairs) -> - let stmts = CCVector.of_list (List.map snd pairs) in - ( Procedure.modify_block proc bid (fun b -> { b with stmts }), + | Left pairs -> (proc, pairs) + | Right (bid, stmts) -> + ( Procedure.modify_block proc bid (fun b -> + { b with stmts = CCVector.of_list stmts }), [ (bid, bid) ] )) proc in From f9892e15f6c0ea99e576986bc423ad9bf2dccbfa Mon Sep 17 00:00:00 2001 From: rina Date: Thu, 9 Jul 2026 23:34:26 +1000 Subject: [PATCH 09/39] nonempty list --- lib/transforms/aslp/aslp_util_internal.ml | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 1f204a1c..b6b1bf80 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -23,13 +23,19 @@ let span_while_some f = in step f [] +(** Groups successive list elements based on whether they are [Left] or [Right], + maintaining relative order. *) let[@tail_mod_cons] group_succ_either = let[@tail_mod_cons] rec while_left xs = let xs, rest = span_while_some Either.find_left xs in - Either.Left xs :: while_right rest + match xs with + | [] -> while_right rest + | h :: xs -> Either.Left (h, xs) :: while_right rest and[@tail_mod_cons] while_right xs = let xs, rest = span_while_some Either.find_right xs in - Right xs :: (match rest with [] -> [] | _ -> while_left rest) + match xs with + | [] -> [] + | h :: xs -> Either.Right (h, xs) :: while_left rest in while_left @@ -130,16 +136,12 @@ let flat_map_stmts (* Collects adjacent bare statements into a basic block, and inserts those statements. *) let proc, block_id_pairs = group_succ_either mapped - |> List.filter_map (function - | Right ((bid, _) :: _ as pairs) -> Some (Right (bid, List.map snd pairs)) - | Right [] -> None - | Left _ as xs -> Some xs) |> List.fold_flat_map (fun proc -> function - | Left pairs -> (proc, pairs) - | Right (bid, stmts) -> - ( Procedure.modify_block proc bid (fun b -> - { b with stmts = CCVector.of_list stmts }), + | Left (hd, tl) -> (proc, hd :: tl) + | Right ((bid, hd), rest) -> + let stmts = CCVector.of_list (hd :: List.map snd rest) in + ( Procedure.modify_block proc bid (fun b -> { b with stmts }), [ (bid, bid) ] )) proc in From 045d47bb9b2a8be4f44958c8090b0f33734ff880 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 15:30:20 +1000 Subject: [PATCH 10/39] support stmt list as flat_map function output --- lib/transforms/aslp/aslp_util_internal.ml | 23 ++++++++++++++++------- 1 file changed, 16 insertions(+), 7 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index b6b1bf80..e8f4023e 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -24,12 +24,16 @@ let span_while_some f = step f [] (** Groups successive list elements based on whether they are [Left] or [Right], - maintaining relative order. *) -let[@tail_mod_cons] group_succ_either = + maintaining relative order. + + [Left] and [Right] values within the returned list contain values like + [('a * 'a list)] to represent a non-empty list. *) +let[@tail_mod_cons] group_succ_either : + ('a, 'b) Either.t list -> ('a * 'a list, 'b * 'b list) Either.t list = let[@tail_mod_cons] rec while_left xs = let xs, rest = span_while_some Either.find_left xs in match xs with - | [] -> while_right rest + | [] -> while_right rest (* in case the input list starts with Right *) | h :: xs -> Either.Left (h, xs) :: while_right rest and[@tail_mod_cons] while_right xs = let xs, rest = span_while_some Either.find_right xs in @@ -39,6 +43,8 @@ let[@tail_mod_cons] group_succ_either = in while_left +(* TODO: these could be made lazy by using Seq.t rather than list *) + (** Iterates over global variables in the given program, including both read and assigned variables. Order is unspecified and may have duplicates. *) let referenced_vars_of_prog = @@ -111,7 +117,7 @@ let flat_map_stmts (f : proc:_ Procedure.t -> _ Stmt.t -> - (ID.t * ID.t * _ Procedure.t, _ Stmt.t) Either.t) ~proc base_bid = + (ID.t * ID.t * _ Procedure.t, _ Stmt.t list) Either.t) ~proc base_bid = let open Either in let b = Procedure.get_block proc base_bid |> Option.get_exn_or "not found" in let stmts = CCVector.to_list b.stmts and base_name = ID.name base_bid in @@ -126,8 +132,8 @@ let flat_map_stmts | None, Right s -> let name = base_name in let proc, bid = Procedure.fresh_block proc ~name ~stmts:[] () in - ((Some bid, proc), Right (bid, s)) - | Some bid, Right s -> ((Some bid, proc), Right (bid, s))) + ((Some bid, proc), Right (bid, Iter.of_list s)) + | Some bid, Right s -> ((Some bid, proc), Right (bid, Iter.of_list s))) (Some base_bid, proc) in let proc = @@ -140,7 +146,10 @@ let flat_map_stmts (fun proc -> function | Left (hd, tl) -> (proc, hd :: tl) | Right ((bid, hd), rest) -> - let stmts = CCVector.of_list (hd :: List.map snd rest) in + let stmts = + Iter.(append hd (flat_map snd (of_list rest))) + |> CCVector.of_iter |> CCVector.freeze + in ( Procedure.modify_block proc bid (fun b -> { b with stmts }), [ (bid, bid) ] )) proc From ce192a52bd6b0213b8c74f308b9a71493a552294 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 15:49:47 +1000 Subject: [PATCH 11/39] comments --- lib/transforms/aslp/aslp_util_internal.ml | 47 ++++++++++++++++------- 1 file changed, 33 insertions(+), 14 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index e8f4023e..32842e87 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -113,6 +113,21 @@ let replace_block ~old ~new_:(new_first, new_last) proc = if ID.equal old new_first || ID.equal old new_last then Fun.id else Fun.flip Procedure.remove_block old +(** Maps each statement in the given block through [f]. For each statement, [f] + may return either zero or more "bare" statements, {i or} a first/last pair + of new block-level control-flow. Returns [(first, last, proc)] where [proc] + is the updated procedure and [first] / [last] is the first / last block of + the combined map output. + + [first] and [last] may be the same. One or both of [first]/[last] may be the + same as the original block. In particular, any bare statements returned by + [f] for an initial segment of the block's statements will be retained in the + original block. If [f] returns a block ID pair, then the returned block IDs + should not be the same as the original block ID - except, perhaps, for the + first block of the first statement. + + Additionally, redirects the original block's incoming/outgoing edges to the + first / last block of the mapped output. *) let flat_map_stmts (f : proc:_ Procedure.t -> @@ -155,26 +170,30 @@ let flat_map_stmts proc in (* Transplant predecessors and successors of the original block as needed. *) + let first, last = + ( List.head_opt block_id_pairs |> Option.map_or fst ~default:base_bid, + List.last_opt block_id_pairs |> Option.map_or snd ~default:base_bid ) + in let proc = proc - |> (match List.last_opt block_id_pairs with - | Some (_, to_) -> Procedure.transplant_outgoing_edges ~from:base_bid ~to_ - | None -> Fun.id) + |> Procedure.transplant_outgoing_edges ~from:base_bid ~to_:last |> - match List.head_opt block_id_pairs with - | Some (hd, _) when not ID.(equal hd base_bid) -> - Procedure.add_goto ~from:base_bid ~targets:[ hd ] - | _ -> Fun.id + if not ID.(equal first base_bid) then + Procedure.add_goto ~from:base_bid ~targets:[ first ] + else Fun.id in (* Insert gotos between mapped blocks. This must happen after transplanting so we do not transplant these edges. *) - List.combine_gen block_id_pairs (List.drop 1 block_id_pairs) - |> Iter.of_gen - |> Iter.fold - (fun proc (first, second) -> - let _, prev = first and next, _ = second in - Procedure.add_goto proc ~from:prev ~targets:[ next ]) - proc + let proc = + List.combine_gen block_id_pairs (List.drop 1 block_id_pairs) + |> Iter.of_gen + |> Iter.fold + (fun proc (first, second) -> + let _, prev = first and next, _ = second in + Procedure.add_goto proc ~from:prev ~targets:[ next ]) + proc + in + (first, last, proc) let flat_map_blocks (f : proc:_ Procedure.t -> ID.t -> _ Block.t -> ID.t * ID.t * _ Procedure.t) From 224968c9729f90f9bae5e0795dd68c9df9d16292 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 16:52:30 +1000 Subject: [PATCH 12/39] add linear test --- test/transforms/dune | 2 +- test/transforms/test_aslp_runtime.ml | 78 ++++++++++++++++++++++++++++ 2 files changed, 79 insertions(+), 1 deletion(-) create mode 100644 test/transforms/test_aslp_runtime.ml diff --git a/test/transforms/dune b/test/transforms/dune index 21d4f519..ce123fe1 100644 --- a/test/transforms/dune +++ b/test/transforms/dune @@ -1,7 +1,7 @@ (library (name test_aslp) (package bincaml) - (modules test_aslp test_aslp_ibi) + (modules test_aslp test_aslp_ibi test_aslp_runtime) (inline_tests) (libraries bincaml.transforms) (preprocess diff --git a/test/transforms/test_aslp_runtime.ml b/test/transforms/test_aslp_runtime.ml new file mode 100644 index 00000000..4a45dc05 --- /dev/null +++ b/test/transforms/test_aslp_runtime.ml @@ -0,0 +1,78 @@ +open Lang +open Common + +let make_big_program n = + let lst = + Loader.Loadir.ast_of_string + {| +memory shared $mem : (bv64 -> bv8); +var $PC:bv64; +prog entry @main; + +proc @main() -> () { } +[ + block %main_code [ + call @_aarch64_eval(0xaa1f03ff:bv32, 0x100:bv64) { .asm = "mov xzr, xzr" }; + goto (%ret_1); + ]; + block %ret_1 [ return; ] +]; + |} + in + lst.prog + |> Program.map_procedures (fun _ -> + Procedure.map_blocks_nondet (fun (_, block) -> + let stmts = + block.stmts |> CCVector.to_iter |> Iter.repeat |> Iter.take n + |> Iter.flatten |> CCVector.of_iter |> CCVector.freeze + in + { block with stmts })) + +let millis_runtime_of f arg = + let start = Sys.time () in + ignore (f arg); + let t = (Sys.time () -. start) *. 1000. in + (* Printf.fprintf stderr "runtime millis: %f\n" t; *) + t + +let find_base_size ~target_millis f arg = + Iter.int_range_by ~step:100 100 10_000 + |> Iter.find_map (fun n -> + Some (millis_runtime_of f (arg n)) + |> Option.filter (fun t -> t >=. target_millis) + |> Option.map (CCPair.make n)) + |> Option.get_exn_or "couldn't get to target_millis" + +let%expect_test "lifting is sub-quadratic" = + let base_size, base_t = + find_base_size ~target_millis:10. Transforms.Aslp.transform_program + make_big_program + in + + let scale = 6 and threshold = 8 in + let big_t = + millis_runtime_of Transforms.Aslp.transform_program + (make_big_program (scale * base_size)) + in + let actual_scale = big_t /. base_t in + if big_t <=. Float.of_int threshold *. base_t then + Printf.printf "Pass: %dx bigger input took less than %x longer.\n" scale threshold + else begin + Printf.printf "Found base_size of %d taking base_t of %fms.\n" base_size + base_t; + Printf.printf "If linear, %dx bigger should take approx %dx longer.\n" scale + scale; + Printf.printf + {|We found it actually took %fx longer (%fms), which is +bigger than the allowed test threshold of %dx. Therefore, we fail this +test which aims to ensure it's approximately linear.|} + actual_scale big_t threshold + end; + [%expect + {| + Found base_size of 200 taking base_t of 12.154000ms. + If linear, 6x bigger should take approx 6x longer. + We found it actually took 9.639213x longer (117.155000ms), which is + bigger than the allowed test threshold of 8x. Therefore, we fail this + test which aims to ensure it's approximately linear. + |}] From 4d908c92c864c03873b403a7b3cd693f36142e84 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 16:56:34 +1000 Subject: [PATCH 13/39] delete unused test file --- test/transforms/test_aslp_zipper.ml | 67 ----------------------------- 1 file changed, 67 deletions(-) delete mode 100644 test/transforms/test_aslp_zipper.ml diff --git a/test/transforms/test_aslp_zipper.ml b/test/transforms/test_aslp_zipper.ml deleted file mode 100644 index 9c07557c..00000000 --- a/test/transforms/test_aslp_zipper.ml +++ /dev/null @@ -1,67 +0,0 @@ -open Lang -open Common -open Transforms.Aslp - -let%expect_test "diamond bfs" = - let d n = - Diamond.Diamond - { - value = n ^ "_merge"; - pred = Leaf (n ^ "_pred"); - left = Leaf (n ^ "_left"); - right = Leaf (n ^ "_right"); - } - in - let main = - Diamond.Diamond - { - value = "merge"; - pred = Leaf "pred"; - left = Leaf "left"; - right = Leaf "right"; - } - in - let zip = - Diamond_zipper.(of_diamond main |> move_in_to `L |> Result.get_ok) - in - let dup = Diamond_zipper.Lazy.duplicate zip in - assert ( - Diamond_zipper.to_diamond dup - |> Diamond.iter_forwards - |> Iter.for_all - (Diamond.equal_diamond String.equal main % Diamond_zipper.to_diamond)); - - let pp = Diamond_zipper.pp_zipper (Diamond_zipper.pp_zipper CCString.pp) in - - CCFormat.output Format.stdout pp dup; - [%expect - {| - (Diamond_zipper.Zipper ( - (Leaf - (Diamond_zipper.Zipper ((Leaf "left"), - [Left {value = "merge"; right = (Leaf "right"); pred = (Leaf "pred")} - ] - ))), - [Left { - value = - (Diamond_zipper.Zipper ((Leaf "left"), - [Left {value = "merge"; right = (Leaf "right"); pred = (Leaf "pred")} - ] - )); - right = - (Leaf - (Diamond_zipper.Zipper ((Leaf "right"), - [Right {value = "merge"; left = (Leaf "left"); - pred = (Leaf "pred")} - ] - ))); - pred = - (Leaf - (Diamond_zipper.Zipper ((Leaf "pred"), - [Pred {value = "merge"; left = (Leaf "left"); - right = (Leaf "right")} - ] - )))} - ] - )) - |}] From 3c276e1ebef714e36fcea43f2981cbd79fa74954 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 16:59:20 +1000 Subject: [PATCH 14/39] x --- test/transforms/test_aslp_runtime.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/transforms/test_aslp_runtime.ml b/test/transforms/test_aslp_runtime.ml index 4a45dc05..fcb3ed51 100644 --- a/test/transforms/test_aslp_runtime.ml +++ b/test/transforms/test_aslp_runtime.ml @@ -45,7 +45,7 @@ let find_base_size ~target_millis f arg = let%expect_test "lifting is sub-quadratic" = let base_size, base_t = - find_base_size ~target_millis:10. Transforms.Aslp.transform_program + find_base_size ~target_millis:15. Transforms.Aslp.transform_program make_big_program in @@ -70,9 +70,9 @@ test which aims to ensure it's approximately linear.|} end; [%expect {| - Found base_size of 200 taking base_t of 12.154000ms. + Found base_size of 300 taking base_t of 17.769000ms. If linear, 6x bigger should take approx 6x longer. - We found it actually took 9.639213x longer (117.155000ms), which is + We found it actually took 11.854747x longer (210.647000ms), which is bigger than the allowed test threshold of 8x. Therefore, we fail this test which aims to ensure it's approximately linear. |}] From 7e789a3ada378743c713c2a4bff7e29c4bdc6f24 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 17:12:17 +1000 Subject: [PATCH 15/39] =?UTF-8?q?use=20Aslp=5Futil=5Finternal.flat=5Fmap?= =?UTF-8?q?=5Fstmts=20=F0=9F=A4=A9=F0=9F=A4=A9?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- lib/transforms/aslp/aslp.ml | 60 +++++++---------------- lib/transforms/aslp/aslp_util_internal.ml | 11 +++-- test/transforms/test_aslp.ml | 7 ++- test/transforms/test_aslp_runtime.ml | 8 +-- 4 files changed, 31 insertions(+), 55 deletions(-) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index f8f91f32..f9589ae4 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -117,51 +117,29 @@ let insert_one_diamond ~proc dia = (first, last, proc) -(** Transforms the next {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsic within the - given block ID within the given procedure. - - The first intrinsic appearing within the block's statement list, if any, - will be transformed. The block will be split at this point. Any statements - after the intrinsic (and any successor edges) will be moved to the last - block of the freshly-inserted ASLp blocks. - - If a change happened, [Some] will be returned with the updated procedure, - along with the ID of the last block of the ASLp output (containing the - suffix of the original block's statements). If no intrinsic exists, [None] - will be returned. +(** Maps the given statement through the ASLp lifter transform, if applicable. + If the statement is a {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsic, then + returns [Left] with the lifted blocks. Otherwise, or if an error occurs, + returns [Right] with the original statement. If an error occurs while lifting through ASLp, an error attribute will be attached to the intrinsic (and it is excluded from subsequent calls). *) -let transform_one_stmt (module I : Bincaml_ibi.IBI) ~proc bid = - let b = Procedure.get_block proc bid |> Option.get_exn_or "block not found" in - - match next_aarch64_stmt (Vector.to_list b.stmts) with - | None -> None - | Some (before, (opcode, address, intrin_attrib), after) -> ( +let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt = + match aarch64_intrin_of_stmt stmt with + | None -> Either.Right [ stmt ] + | Some (opcode, address, attrib) -> ( match lift_opcode (module I) ~address opcode with | diamond -> let aslp_first, aslp_last, proc = insert_one_diamond ~proc diamond in - - let proc = - proc - |> Procedure.modify_block' ~id:bid ~f:(fun b -> - { b with stmts = Vector.of_list before }) - |> Procedure.modify_block' ~id:aslp_first ~f:(fun b -> - { b with attrib = intrin_attrib }) - |> Procedure.modify_block' ~id:aslp_last ~f:(fun b -> - Block.fmap_stmts_copy (Fun.flip CCVector.append_list after) b) - |> Procedure.transplant_outgoing_edges ~from:bid ~to_:aslp_last - |> Procedure.add_goto ~from:bid ~targets:[ aslp_first ] - in - Some (proc, aslp_last) + Either.Left + ( aslp_first, + aslp_last, + Procedure.modify_block' proc ~id:aslp_first ~f:(fun b -> + { b with attrib }) ) | exception error -> let error = `String (Printexc.to_string error) in - let intrin_stmt = - stmt_of_aarch64_intrin ~error (opcode, address, intrin_attrib) - in - let stmts = Vector.of_list (before @ (intrin_stmt :: after)) in - Some (Procedure.modify_block proc bid (fun b -> { b with stmts }), bid) - ) + let intrin = (opcode, address, attrib) in + Either.Right [ stmt_of_aarch64_intrin ~error intrin ]) (** Transforms the {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsics within the given block ID within the given procedure. @@ -169,10 +147,10 @@ let transform_one_stmt (module I : Bincaml_ibi.IBI) ~proc bid = Inserts control-flow edges between successive instructions within the block, and emits an assertion for the ITE expression representing the final [PC] value. *) -let rec transform_block (module I : Bincaml_ibi.IBI) ~proc bid = - match transform_one_stmt (module I) ~proc bid with - | Some (proc, bid) -> (transform_block [@tailcall]) (module I) ~proc bid - | None -> proc +let transform_block (module I : Bincaml_ibi.IBI) ~proc bid = + let f = map_one_stmt (module I) in + let _, _, proc = Aslp_util_internal.flat_map_stmts bid ~proc ~f in + proc (** Transforms the {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsics of all blocks within the given procedure. *) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 32842e87..9958a8c3 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -28,7 +28,7 @@ let span_while_some f = [Left] and [Right] values within the returned list contain values like [('a * 'a list)] to represent a non-empty list. *) -let[@tail_mod_cons] group_succ_either : +let group_succ_either : ('a, 'b) Either.t list -> ('a * 'a list, 'b * 'b list) Either.t list = let[@tail_mod_cons] rec while_left xs = let xs, rest = span_while_some Either.find_left xs in @@ -129,10 +129,11 @@ let replace_block ~old ~new_:(new_first, new_last) proc = Additionally, redirects the original block's incoming/outgoing edges to the first / last block of the mapped output. *) let flat_map_stmts - (f : - proc:_ Procedure.t -> - _ Stmt.t -> - (ID.t * ID.t * _ Procedure.t, _ Stmt.t list) Either.t) ~proc base_bid = + ~(f : + proc:_ Procedure.t -> + _ Stmt.t -> + (ID.t * ID.t * _ Procedure.t, _ Stmt.t list) Either.t) ~proc base_bid = + (* TODO: do we need a new type declaration for this big Either type? *) let open Either in let b = Procedure.get_block proc base_bid |> Option.get_exn_or "not found" in let stmts = CCVector.to_list b.stmts and base_name = ID.name base_bid in diff --git a/test/transforms/test_aslp.ml b/test/transforms/test_aslp.ml index 2d288a32..f73da071 100644 --- a/test/transforms/test_aslp.ml +++ b/test/transforms/test_aslp.ml @@ -203,9 +203,9 @@ proc @main() -> () { } $R30:bv64 := 0x400820:bv64; var BranchTaken:bool := true; $PC:bv64 := 0x400784:bv64; - assert boolor(eq(0x400784:bv64, $PC)); - goto (%ret_1); + goto (%main_code_1); ]; + block %main_code_1 [ assert boolor(eq(0x400784:bv64, $PC)); goto (%ret_1); ]; block %ret_1 [ return; ] ]; var $SP:bv64; @@ -278,6 +278,9 @@ proc @Sqrt() -> () { } ]; block %block_3 [ $PC:bv64 := if boolnot(eq($PSTATE_N, $PSTATE_V)) then 0x4007ec:bv64 else 0x4007e0:bv64; + goto (%Sqrt_code_5); + ]; + block %Sqrt_code_5 [ assert boolor(eq(0x4007fc:bv64, $PC), eq(0x4007e0:bv64, $PC)); goto (%Sqrt_code_3,%Sqrt_code); ]; diff --git a/test/transforms/test_aslp_runtime.ml b/test/transforms/test_aslp_runtime.ml index fcb3ed51..cae99dac 100644 --- a/test/transforms/test_aslp_runtime.ml +++ b/test/transforms/test_aslp_runtime.ml @@ -69,10 +69,4 @@ test which aims to ensure it's approximately linear.|} actual_scale big_t threshold end; [%expect - {| - Found base_size of 300 taking base_t of 17.769000ms. - If linear, 6x bigger should take approx 6x longer. - We found it actually took 11.854747x longer (210.647000ms), which is - bigger than the allowed test threshold of 8x. Therefore, we fail this - test which aims to ensure it's approximately linear. - |}] + {| Pass: 6x bigger input took less than 8 longer. |}] From 4507b64f5580b263a80f16d0a389326dd0b6f424 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 17:16:05 +1000 Subject: [PATCH 16/39] don't need error_attrib_key or include_failed anymore. we can just always include them --- lib/transforms/aslp/aslp.ml | 9 +++------ test/transforms/test_aslp_runtime.ml | 6 +++--- 2 files changed, 6 insertions(+), 9 deletions(-) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index f9589ae4..b00a1c8a 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -37,18 +37,15 @@ let lift_code_block (module I : Bincaml_ibi.IBI) ~address = (** {1 Interfacing with Bincaml IR} *) -and error_attrib_key = ".error" - (** Extracts the opcode, address, and attribute from the given Bincaml statement, if it is an {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsic call. Otherwise, returns [None]. Raises an exception if an {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsic call has an unexpected structure. *) -let aarch64_intrin_of_stmt ?(include_failed = false) ?default_address : +let aarch64_intrin_of_stmt ?default_address : Program.stmt -> (Bitvec.t * Bitvec.t * Attrib.attrib_map) option = function - | Stmt.Instr_IntrinCall { attrib; lhs; name = Aarch64Eval; args } - when include_failed || not (StringMap.mem error_attrib_key attrib) -> ( + | Stmt.Instr_IntrinCall { attrib; lhs; name = Aarch64Eval; args } -> ( let args = match (args, default_address) with | [ x ], Some default -> [ x; Expr.BasilExpr.bvconst default ] @@ -206,7 +203,7 @@ let apply_stmt_addresses_from_block (block : _ Block.t) = let apply_one address stmt = let address' = Bitvec.(add address (of_int ~size:64 4)) in - match aarch64_intrin_of_stmt ~include_failed:true ~default_address stmt with + match aarch64_intrin_of_stmt ~default_address stmt with | Some (opcode, a, attr) when Bitvec.equal a default_address -> (address', stmt_of_aarch64_intrin (opcode, address, attr)) | Some _ -> (address', stmt) (* increment address *) diff --git a/test/transforms/test_aslp_runtime.ml b/test/transforms/test_aslp_runtime.ml index cae99dac..50357cc1 100644 --- a/test/transforms/test_aslp_runtime.ml +++ b/test/transforms/test_aslp_runtime.ml @@ -56,7 +56,8 @@ let%expect_test "lifting is sub-quadratic" = in let actual_scale = big_t /. base_t in if big_t <=. Float.of_int threshold *. base_t then - Printf.printf "Pass: %dx bigger input took less than %x longer.\n" scale threshold + Printf.printf "Pass: %dx bigger input took less than %x longer.\n" scale + threshold else begin Printf.printf "Found base_size of %d taking base_t of %fms.\n" base_size base_t; @@ -68,5 +69,4 @@ bigger than the allowed test threshold of %dx. Therefore, we fail this test which aims to ensure it's approximately linear.|} actual_scale big_t threshold end; - [%expect - {| Pass: 6x bigger input took less than 8 longer. |}] + [%expect {| Pass: 6x bigger input took less than 8 longer. |}] From 946754996b13672200bb2a01c691e2b30c81cb8c Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 17:19:27 +1000 Subject: [PATCH 17/39] remove unused functions --- lib/lang/procedure.ml | 5 ++- lib/transforms/aslp/aslp_util_internal.ml | 52 ----------------------- 2 files changed, 4 insertions(+), 53 deletions(-) diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 8b421db7..352f44ba 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -456,7 +456,10 @@ let replace_edge p id (block : (Var.t, BasilExpr.t) Block.t) = [to_] is modified to additionally have the original outgoing edges of [from_]. - This includes any edges to [Return] nodes, if they exist on [from_]. *) + This includes any edges to [Return] nodes, if they exist on [from_]. + + TODO: how does this interact with phi nodes?? probably impossible to handle. +*) let transplant_outgoing_edges p ~from ~to_ : _ t = let replace_outgoing_uses ~from ~to_ g = G.fold_succ_e diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 9958a8c3..c74c5b32 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -55,49 +55,6 @@ let referenced_vars_of_prog = Iter.append (Block.read_vars_iter b) (Block.assigned_vars_iter b))) %> Iter.filter Var.is_global -(** Isolates statements satisfying the given predicate into their own block, - while maintaining sequential control-flow between them. *) -let isolate_stmts_of_block ?(label = "%singleton") ~proc f bid = - let stmts = - Procedure.get_block proc bid |> Option.get_exn_or "block not found" - |> fun b -> CCVector.to_list b.stmts - in - - (* Group, then flatten isolated statements into their own list. *) - let (grouped_stmts : _ Stmt.t list list) = - List.group_succ ~eq:(CCFun.compose_binop f Bool.equal) stmts - |> List.flat_map (function - | hd :: _ as xs when f hd -> List.map List.pure xs - | xs -> List.pure xs) - in - - (* Insert disconnected blocks for each group, reusing [bid] for the first group. *) - let proc, block_ids = - grouped_stmts - |> List.fold_map_i - (fun proc i stmts -> - if i = 0 then - let stmts = CCVector.of_list stmts in - (Procedure.modify_block proc bid (fun b -> { b with stmts }), bid) - else Procedure.fresh_block proc ~name:label ~stmts ()) - proc - in - - let proc = - match List.last_opt block_ids with - | Some to_ -> Procedure.transplant_outgoing_edges proc ~from:bid ~to_ - | None -> proc - in - - match block_ids with - | [] -> proc - | hd :: tl -> - List.fold_left - (fun (proc, from) next -> - (Procedure.add_goto proc ~from ~targets:[ next ], next)) - (proc, hd) tl - |> fst - (** Replaces uses of the old block ID with the new [(first, last)] block IDs. The incoming edges to [old] will be redirected to [first] and the outgoing edges of [old] will be rebased to originate from [last]. @@ -195,12 +152,3 @@ let flat_map_stmts proc in (first, last, proc) - -let flat_map_blocks - (f : proc:_ Procedure.t -> ID.t -> _ Block.t -> ID.t * ID.t * _ Procedure.t) - proc = - Procedure.fold_blocks_topo_fwd - (fun proc bid block -> - let first, last, proc = f ~proc bid block in - proc |> replace_block ~old:bid ~new_:(first, last)) - proc proc From 6d6cbcb96751fec8a4d3ed4d66676ff6df10bfd1 Mon Sep 17 00:00:00 2001 From: rina Date: Fri, 10 Jul 2026 17:31:25 +1000 Subject: [PATCH 18/39] remove unused function --- lib/transforms/aslp/aslp.ml | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index b00a1c8a..dddd4dac 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -73,17 +73,6 @@ let stmt_of_aarch64_intrin ?error : let args = Expr.BasilExpr.[ bvconst opcode; bvconst address ] in Stmt.Instr_IntrinCall { attrib; lhs = []; name = Aarch64Eval; args } -(** Extracts the next Aarch64 intrinsic from the given list of statements, - returning [Some (before, intrin, after)] if there exists an intrinsic. *) -let next_aarch64_stmt stmts = - let open CCOption.Infix in - let before, rest = - CCList.take_drop_while (Option.is_none % aarch64_intrin_of_stmt) stmts - in - let* hd, after = Aslp_util_internal.uncons rest in - let* intrin = aarch64_intrin_of_stmt hd in - Some (before, intrin, after) - (** Returns the Bincaml global variable representing heap memory. *) let aarch64_mem_of_prog prog = Program.get_decl_by_name "$mem" prog |> function From a9aef85a4c6f1cfa484c61b22c53a140c04bc3c1 Mon Sep 17 00:00:00 2001 From: rina Date: Sat, 11 Jul 2026 17:54:03 +1000 Subject: [PATCH 19/39] less characters --- lib/transforms/aslp/aslp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index dddd4dac..e2660091 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -120,7 +120,7 @@ let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt = Either.Left ( aslp_first, aslp_last, - Procedure.modify_block' proc ~id:aslp_first ~f:(fun b -> + Procedure.modify_block proc aslp_first (fun b -> { b with attrib }) ) | exception error -> let error = `String (Printexc.to_string error) in From 778eef64287f48114b7b9ee98dbe7faa41c66ea7 Mon Sep 17 00:00:00 2001 From: rina Date: Sat, 11 Jul 2026 18:24:41 +1000 Subject: [PATCH 20/39] blah. does it even work with the eager list in the first element? because we would need to compute the one *after* the group in order to know when to end the group. therefore, if we're in a bare statement group, we could still compute a block-pair ID before returning the bare statement group. i guess we would have to make it a Seq in the group lists too. but that seems hard to avoid re-computing. maybe just use persistent?? --- lib/transforms/aslp/aslp_util_internal.ml | 127 +++++++++++++++------- 1 file changed, 87 insertions(+), 40 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index c74c5b32..31c3aad8 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -4,46 +4,93 @@ open Lang open Common -(** Returns [Some (hd x, tl x)] if [x] is non-empty, otherwise returns [None]. -*) -let uncons = function [] -> None | hd :: tl -> Some (hd, tl) - -(** [span_while_some f xs] returns the longest prefix of [xs] where the elements - yield [Some] when mapped through [f]. - - These [Some] values are returned in the first tuple element. Upon reaching a - value which yields [None], that value and values after it are returned in - the second tuple element. *) -let span_while_some f = - let rec step f rev_somes all = - let x, rest = match all with [] -> (None, []) | hd :: tl -> (f hd, tl) in - match x with - | None -> (List.rev rev_somes, all) - | Some x -> (step [@tailcall]) f (x :: rev_somes) rest - in - step f [] - -(** Groups successive list elements based on whether they are [Left] or [Right], - maintaining relative order. - - [Left] and [Right] values within the returned list contain values like - [('a * 'a list)] to represent a non-empty list. *) -let group_succ_either : - ('a, 'b) Either.t list -> ('a * 'a list, 'b * 'b list) Either.t list = - let[@tail_mod_cons] rec while_left xs = - let xs, rest = span_while_some Either.find_left xs in - match xs with - | [] -> while_right rest (* in case the input list starts with Right *) - | h :: xs -> Either.Left (h, xs) :: while_right rest - and[@tail_mod_cons] while_right xs = - let xs, rest = span_while_some Either.find_right xs in - match xs with - | [] -> [] - | h :: xs -> Either.Right (h, xs) :: while_left rest - in - while_left +module List_util = struct + (** Returns [Some (hd x, tl x)] if [x] is non-empty, otherwise returns [None]. + *) + let uncons = function [] -> None | hd :: tl -> Some (hd, tl) + + (** [span_while_some f xs] returns the longest prefix of [xs] where the + elements yield [Some] when mapped through [f]. + + These [Some] values are returned in the first tuple element. Upon reaching + a value which yields [None], that value and values after it are returned + in the second tuple element. *) + let span_while_some f = + let rec step f rev_somes all = + let x, rest = + match all with [] -> (None, []) | hd :: tl -> (f hd, tl) + in + match x with + | None -> (List.rev rev_somes, all) + | Some x -> (step [@tailcall]) f (x :: rev_somes) rest + in + step f [] + + (** Groups successive list elements based on whether they are [Left] or + [Right], maintaining relative order. + + [Left] and [Right] values within the returned list contain values like + [('a * 'a list)] to represent a non-empty list. *) + let group_succ_either : + ('a, 'b) Either.t list -> ('a * 'a list, 'b * 'b list) Either.t list = + let[@tail_mod_cons] rec while_left xs = + let xs, rest = span_while_some Either.find_left xs in + match xs with + | [] -> while_right rest (* in case the input list starts with Right *) + | h :: xs -> Either.Left (h, xs) :: while_right rest + and[@tail_mod_cons] while_right xs = + let xs, rest = span_while_some Either.find_right xs in + match xs with + | [] -> [] + | h :: xs -> Either.Right (h, xs) :: while_left rest + in + while_left + + (* TODO: these could be made lazy by using Seq.t rather than list *) +end + +module Seq_util = struct + type a = int CCSeq.t + + (** [span_while_some f xs] returns the longest prefix of [xs] where the + elements yield [Some] when mapped through [f]. + + These [Some] values are returned in the first tuple element. Upon reaching + a value which yields [None], that value and values after it are returned + in the second tuple element. + + This function eagerly computes the [Some] prefix of the {!Seq.t}. *) + let span_while_some f : _ Seq.t -> _ list * _ Seq.t = + let rec step f rev_somes all = + match all () with + | Seq.Nil -> (List.rev rev_somes, Seq.empty) + | Seq.Cons (hd, tl) -> ( + match f hd with + | None -> (List.rev rev_somes, Seq.cons hd tl) + | Some x -> (step [@tailcall]) f (x :: rev_somes) tl) + in + step f [] + + (** Groups successive list elements based on whether they are [Left] or + [Right], maintaining relative order. -(* TODO: these could be made lazy by using Seq.t rather than list *) + [Left] and [Right] values within the returned list contain values like + [('a * 'a list)] to represent a non-empty list. *) + let group_succ_either : + ('a, 'b) Either.t Seq.t -> ('a * 'a list, 'b * 'b list) Either.t Seq.t = + let[@tail_mod_cons] rec while_left xs () = + let xs, rest = span_while_some Either.find_left xs in + match xs with + | [] -> while_right rest () (* in case the input starts with Right *) + | h :: xs -> Seq.Cons (Either.Left (h, xs), while_right rest) + and[@tail_mod_cons] while_right xs () = + let xs, rest = span_while_some Either.find_right xs in + match xs with + | [] -> Nil + | h :: xs -> Seq.Cons (Either.Right (h, xs), while_left rest) + in + while_left +end (** Iterates over global variables in the given program, including both read and assigned variables. Order is unspecified and may have duplicates. *) @@ -114,7 +161,7 @@ let flat_map_stmts in (* Collects adjacent bare statements into a basic block, and inserts those statements. *) let proc, block_id_pairs = - group_succ_either mapped + List_util.group_succ_either mapped |> List.fold_flat_map (fun proc -> function | Left (hd, tl) -> (proc, hd :: tl) From 58145f0fabde85c6634af268da5cd47799ae0fd5 Mon Sep 17 00:00:00 2001 From: rina Date: Sat, 11 Jul 2026 18:43:10 +1000 Subject: [PATCH 21/39] jfidosajfoidsajfidosa it not good Seq cannot have foldmap --- lib/transforms/aslp/aslp_util_internal.ml | 34 ++++++++++++----------- 1 file changed, 18 insertions(+), 16 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 31c3aad8..951a9875 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -59,17 +59,19 @@ module Seq_util = struct a value which yields [None], that value and values after it are returned in the second tuple element. - This function eagerly computes the [Some] prefix of the {!Seq.t}. *) - let span_while_some f : _ Seq.t -> _ list * _ Seq.t = - let rec step f rev_somes all = - match all () with - | Seq.Nil -> (List.rev rev_somes, Seq.empty) + The two returned sequences will traverse the input sequence separately, so + the sequence should support multiple iteration. *) + let span_while_some f : _ Seq.t -> _ Seq.t * _ Seq.t = + fun xs -> + let rec get_somes f xs () = + match xs () with + | Seq.Nil -> Seq.Nil | Seq.Cons (hd, tl) -> ( match f hd with - | None -> (List.rev rev_somes, Seq.cons hd tl) - | Some x -> (step [@tailcall]) f (x :: rev_somes) tl) + | None -> Seq.Nil + | Some x -> Seq.Cons (x, get_somes f tl)) in - step f [] + (get_somes f xs, Seq.drop_while (Option.is_some % f) xs) (** Groups successive list elements based on whether they are [Left] or [Right], maintaining relative order. @@ -77,17 +79,17 @@ module Seq_util = struct [Left] and [Right] values within the returned list contain values like [('a * 'a list)] to represent a non-empty list. *) let group_succ_either : - ('a, 'b) Either.t Seq.t -> ('a * 'a list, 'b * 'b list) Either.t Seq.t = + ('a, 'b) Either.t Seq.t -> ('a * 'a Seq.t, 'b * 'b Seq.t) Either.t Seq.t = let[@tail_mod_cons] rec while_left xs () = let xs, rest = span_while_some Either.find_left xs in - match xs with - | [] -> while_right rest () (* in case the input starts with Right *) - | h :: xs -> Seq.Cons (Either.Left (h, xs), while_right rest) + match xs () with + | Seq.Nil -> while_right rest () (* in case the input starts with Right *) + | Seq.Cons (h, xs) -> Seq.Cons (Either.Left (h, xs), while_right rest) and[@tail_mod_cons] while_right xs () = let xs, rest = span_while_some Either.find_right xs in - match xs with - | [] -> Nil - | h :: xs -> Seq.Cons (Either.Right (h, xs), while_left rest) + match xs () with + | Seq.Nil -> Nil + | Seq.Cons (h, xs) -> Seq.Cons (Either.Right (h, xs), while_left rest) in while_left end @@ -140,7 +142,7 @@ let flat_map_stmts (* TODO: do we need a new type declaration for this big Either type? *) let open Either in let b = Procedure.get_block proc base_bid |> Option.get_exn_or "not found" in - let stmts = CCVector.to_list b.stmts and base_name = ID.name base_bid in + let stmts = CCVector.to_seq b.stmts and base_name = ID.name base_bid in (* Map, while generating block names for bare statements returned by the mapping function. *) let (_, proc), mapped = From d3af79c09f40e409b34656890ec357262f018ad6 Mon Sep 17 00:00:00 2001 From: rina Date: Sun, 12 Jul 2026 02:23:15 +1000 Subject: [PATCH 22/39] Revert "jfidosajfoidsajfidosa it not good" This reverts commit 58145f0fabde85c6634af268da5cd47799ae0fd5. --- lib/transforms/aslp/aslp_util_internal.ml | 34 +++++++++++------------ 1 file changed, 16 insertions(+), 18 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 951a9875..31c3aad8 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -59,19 +59,17 @@ module Seq_util = struct a value which yields [None], that value and values after it are returned in the second tuple element. - The two returned sequences will traverse the input sequence separately, so - the sequence should support multiple iteration. *) - let span_while_some f : _ Seq.t -> _ Seq.t * _ Seq.t = - fun xs -> - let rec get_somes f xs () = - match xs () with - | Seq.Nil -> Seq.Nil + This function eagerly computes the [Some] prefix of the {!Seq.t}. *) + let span_while_some f : _ Seq.t -> _ list * _ Seq.t = + let rec step f rev_somes all = + match all () with + | Seq.Nil -> (List.rev rev_somes, Seq.empty) | Seq.Cons (hd, tl) -> ( match f hd with - | None -> Seq.Nil - | Some x -> Seq.Cons (x, get_somes f tl)) + | None -> (List.rev rev_somes, Seq.cons hd tl) + | Some x -> (step [@tailcall]) f (x :: rev_somes) tl) in - (get_somes f xs, Seq.drop_while (Option.is_some % f) xs) + step f [] (** Groups successive list elements based on whether they are [Left] or [Right], maintaining relative order. @@ -79,17 +77,17 @@ module Seq_util = struct [Left] and [Right] values within the returned list contain values like [('a * 'a list)] to represent a non-empty list. *) let group_succ_either : - ('a, 'b) Either.t Seq.t -> ('a * 'a Seq.t, 'b * 'b Seq.t) Either.t Seq.t = + ('a, 'b) Either.t Seq.t -> ('a * 'a list, 'b * 'b list) Either.t Seq.t = let[@tail_mod_cons] rec while_left xs () = let xs, rest = span_while_some Either.find_left xs in - match xs () with - | Seq.Nil -> while_right rest () (* in case the input starts with Right *) - | Seq.Cons (h, xs) -> Seq.Cons (Either.Left (h, xs), while_right rest) + match xs with + | [] -> while_right rest () (* in case the input starts with Right *) + | h :: xs -> Seq.Cons (Either.Left (h, xs), while_right rest) and[@tail_mod_cons] while_right xs () = let xs, rest = span_while_some Either.find_right xs in - match xs () with - | Seq.Nil -> Nil - | Seq.Cons (h, xs) -> Seq.Cons (Either.Right (h, xs), while_left rest) + match xs with + | [] -> Nil + | h :: xs -> Seq.Cons (Either.Right (h, xs), while_left rest) in while_left end @@ -142,7 +140,7 @@ let flat_map_stmts (* TODO: do we need a new type declaration for this big Either type? *) let open Either in let b = Procedure.get_block proc base_bid |> Option.get_exn_or "not found" in - let stmts = CCVector.to_seq b.stmts and base_name = ID.name base_bid in + let stmts = CCVector.to_list b.stmts and base_name = ID.name base_bid in (* Map, while generating block names for bare statements returned by the mapping function. *) let (_, proc), mapped = From 876cc14291e7189ca22d2fb7a4b30e21823c6e6d Mon Sep 17 00:00:00 2001 From: rina Date: Sun, 12 Jul 2026 02:23:16 +1000 Subject: [PATCH 23/39] Revert "blah. does it even work with the eager list in the first element?" This reverts commit 778eef64287f48114b7b9ee98dbe7faa41c66ea7. --- lib/transforms/aslp/aslp_util_internal.ml | 127 +++++++--------------- 1 file changed, 40 insertions(+), 87 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 31c3aad8..c74c5b32 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -4,93 +4,46 @@ open Lang open Common -module List_util = struct - (** Returns [Some (hd x, tl x)] if [x] is non-empty, otherwise returns [None]. - *) - let uncons = function [] -> None | hd :: tl -> Some (hd, tl) - - (** [span_while_some f xs] returns the longest prefix of [xs] where the - elements yield [Some] when mapped through [f]. - - These [Some] values are returned in the first tuple element. Upon reaching - a value which yields [None], that value and values after it are returned - in the second tuple element. *) - let span_while_some f = - let rec step f rev_somes all = - let x, rest = - match all with [] -> (None, []) | hd :: tl -> (f hd, tl) - in - match x with - | None -> (List.rev rev_somes, all) - | Some x -> (step [@tailcall]) f (x :: rev_somes) rest - in - step f [] - - (** Groups successive list elements based on whether they are [Left] or - [Right], maintaining relative order. - - [Left] and [Right] values within the returned list contain values like - [('a * 'a list)] to represent a non-empty list. *) - let group_succ_either : - ('a, 'b) Either.t list -> ('a * 'a list, 'b * 'b list) Either.t list = - let[@tail_mod_cons] rec while_left xs = - let xs, rest = span_while_some Either.find_left xs in - match xs with - | [] -> while_right rest (* in case the input list starts with Right *) - | h :: xs -> Either.Left (h, xs) :: while_right rest - and[@tail_mod_cons] while_right xs = - let xs, rest = span_while_some Either.find_right xs in - match xs with - | [] -> [] - | h :: xs -> Either.Right (h, xs) :: while_left rest - in - while_left - - (* TODO: these could be made lazy by using Seq.t rather than list *) -end - -module Seq_util = struct - type a = int CCSeq.t - - (** [span_while_some f xs] returns the longest prefix of [xs] where the - elements yield [Some] when mapped through [f]. - - These [Some] values are returned in the first tuple element. Upon reaching - a value which yields [None], that value and values after it are returned - in the second tuple element. - - This function eagerly computes the [Some] prefix of the {!Seq.t}. *) - let span_while_some f : _ Seq.t -> _ list * _ Seq.t = - let rec step f rev_somes all = - match all () with - | Seq.Nil -> (List.rev rev_somes, Seq.empty) - | Seq.Cons (hd, tl) -> ( - match f hd with - | None -> (List.rev rev_somes, Seq.cons hd tl) - | Some x -> (step [@tailcall]) f (x :: rev_somes) tl) - in - step f [] - - (** Groups successive list elements based on whether they are [Left] or - [Right], maintaining relative order. +(** Returns [Some (hd x, tl x)] if [x] is non-empty, otherwise returns [None]. +*) +let uncons = function [] -> None | hd :: tl -> Some (hd, tl) + +(** [span_while_some f xs] returns the longest prefix of [xs] where the elements + yield [Some] when mapped through [f]. + + These [Some] values are returned in the first tuple element. Upon reaching a + value which yields [None], that value and values after it are returned in + the second tuple element. *) +let span_while_some f = + let rec step f rev_somes all = + let x, rest = match all with [] -> (None, []) | hd :: tl -> (f hd, tl) in + match x with + | None -> (List.rev rev_somes, all) + | Some x -> (step [@tailcall]) f (x :: rev_somes) rest + in + step f [] + +(** Groups successive list elements based on whether they are [Left] or [Right], + maintaining relative order. + + [Left] and [Right] values within the returned list contain values like + [('a * 'a list)] to represent a non-empty list. *) +let group_succ_either : + ('a, 'b) Either.t list -> ('a * 'a list, 'b * 'b list) Either.t list = + let[@tail_mod_cons] rec while_left xs = + let xs, rest = span_while_some Either.find_left xs in + match xs with + | [] -> while_right rest (* in case the input list starts with Right *) + | h :: xs -> Either.Left (h, xs) :: while_right rest + and[@tail_mod_cons] while_right xs = + let xs, rest = span_while_some Either.find_right xs in + match xs with + | [] -> [] + | h :: xs -> Either.Right (h, xs) :: while_left rest + in + while_left - [Left] and [Right] values within the returned list contain values like - [('a * 'a list)] to represent a non-empty list. *) - let group_succ_either : - ('a, 'b) Either.t Seq.t -> ('a * 'a list, 'b * 'b list) Either.t Seq.t = - let[@tail_mod_cons] rec while_left xs () = - let xs, rest = span_while_some Either.find_left xs in - match xs with - | [] -> while_right rest () (* in case the input starts with Right *) - | h :: xs -> Seq.Cons (Either.Left (h, xs), while_right rest) - and[@tail_mod_cons] while_right xs () = - let xs, rest = span_while_some Either.find_right xs in - match xs with - | [] -> Nil - | h :: xs -> Seq.Cons (Either.Right (h, xs), while_left rest) - in - while_left -end +(* TODO: these could be made lazy by using Seq.t rather than list *) (** Iterates over global variables in the given program, including both read and assigned variables. Order is unspecified and may have duplicates. *) @@ -161,7 +114,7 @@ let flat_map_stmts in (* Collects adjacent bare statements into a basic block, and inserts those statements. *) let proc, block_id_pairs = - List_util.group_succ_either mapped + group_succ_either mapped |> List.fold_flat_map (fun proc -> function | Left (hd, tl) -> (proc, hd :: tl) From 729de802af96601b5a0a66ddb04a20652f009c8c Mon Sep 17 00:00:00 2001 From: rina Date: Sun, 12 Jul 2026 02:28:43 +1000 Subject: [PATCH 24/39] headings --- lib/transforms/aslp/aslp_util_internal.ml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index c74c5b32..4835c006 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -4,6 +4,8 @@ open Lang open Common +(** {1 General data processing} *) + (** Returns [Some (hd x, tl x)] if [x] is non-empty, otherwise returns [None]. *) let uncons = function [] -> None | hd :: tl -> Some (hd, tl) @@ -45,6 +47,8 @@ let group_succ_either : (* TODO: these could be made lazy by using Seq.t rather than list *) +(** {1 Bincaml utilities} *) + (** Iterates over global variables in the given program, including both read and assigned variables. Order is unspecified and may have duplicates. *) let referenced_vars_of_prog = From 5ae181d7e92b479be822408508c6007c688a3736 Mon Sep 17 00:00:00 2001 From: rina Date: Sun, 12 Jul 2026 02:56:08 +1000 Subject: [PATCH 25/39] touch. clear_stmts --- lib/lang/block.ml | 3 +++ lib/transforms/aslp/aslp_util_internal.ml | 15 ++++++--------- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/lib/lang/block.ml b/lib/lang/block.ml index 0233d0c1..cb411231 100644 --- a/lib/lang/block.ml +++ b/lib/lang/block.ml @@ -111,6 +111,9 @@ let fmap_stmts_copy (f : (('a, 'a, 'b) Stmt.t, 'mut) Vector.t -> unit) b = f v; { b with stmts = Vector.freeze v } +let clear_stmts (b : ('v, 'e) t) = + { b with stmts = Vector.create () |> Vector.freeze } + (** prepend statements to block statement list (copies underlying vector) *) let prepend_stmts (b : ('v, 'e) t) (nstmts : ('v, 'v, 'e) Stmt.t list) : ('v, 'e) t = diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 4835c006..5204dc55 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -97,7 +97,7 @@ let flat_map_stmts (* TODO: do we need a new type declaration for this big Either type? *) let open Either in let b = Procedure.get_block proc base_bid |> Option.get_exn_or "not found" in - let stmts = CCVector.to_list b.stmts and base_name = ID.name base_bid in + let stmts = CCVector.to_list b.stmts in (* Map, while generating block names for bare statements returned by the mapping function. *) let (_, proc), mapped = @@ -106,17 +106,15 @@ let flat_map_stmts (fun (bid, proc) stmt -> match (bid, f ~proc stmt) with | _, Left (first, last, proc) -> ((None, proc), Left (first, last)) + | Some bid, Right s -> ((Some bid, proc), Right (bid, Iter.of_list s)) | None, Right s -> - let name = base_name in + let name = ID.name base_bid in let proc, bid = Procedure.fresh_block proc ~name ~stmts:[] () in - ((Some bid, proc), Right (bid, Iter.of_list s)) - | Some bid, Right s -> ((Some bid, proc), Right (bid, Iter.of_list s))) + ((Some bid, proc), Right (bid, Iter.of_list s))) (Some base_bid, proc) in - let proc = - Procedure.modify_block proc base_bid (Block.fmap_stmts_copy CCVector.clear) - in (* Collects adjacent bare statements into a basic block, and inserts those statements. *) + let proc = Procedure.modify_block proc base_bid Block.clear_stmts in let proc, block_id_pairs = group_succ_either mapped |> List.fold_flat_map @@ -150,8 +148,7 @@ let flat_map_stmts List.combine_gen block_id_pairs (List.drop 1 block_id_pairs) |> Iter.of_gen |> Iter.fold - (fun proc (first, second) -> - let _, prev = first and next, _ = second in + (fun proc ((_, prev), (next, _)) -> Procedure.add_goto proc ~from:prev ~targets:[ next ]) proc in From 7ba140140e69abafccd85c26b52e0ccc5ce961fa Mon Sep 17 00:00:00 2001 From: rina Date: Sun, 12 Jul 2026 03:04:15 +1000 Subject: [PATCH 26/39] x --- lib/transforms/aslp/aslp_util_internal.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 5204dc55..199cdc19 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -95,15 +95,14 @@ let flat_map_stmts _ Stmt.t -> (ID.t * ID.t * _ Procedure.t, _ Stmt.t list) Either.t) ~proc base_bid = (* TODO: do we need a new type declaration for this big Either type? *) - let open Either in let b = Procedure.get_block proc base_bid |> Option.get_exn_or "not found" in - let stmts = CCVector.to_list b.stmts in (* Map, while generating block names for bare statements returned by the mapping function. *) let (_, proc), mapped = - stmts + b.stmts |> CCVector.to_list |> List.fold_map (fun (bid, proc) stmt -> + let open Either in match (bid, f ~proc stmt) with | _, Left (first, last, proc) -> ((None, proc), Left (first, last)) | Some bid, Right s -> ((Some bid, proc), Right (bid, Iter.of_list s)) @@ -119,10 +118,10 @@ let flat_map_stmts group_succ_either mapped |> List.fold_flat_map (fun proc -> function - | Left (hd, tl) -> (proc, hd :: tl) - | Right ((bid, hd), rest) -> + | Either.Left (hd, tl) -> (proc, hd :: tl) + | Either.Right ((bid, hd), rest) -> let stmts = - Iter.(append hd (flat_map snd (of_list rest))) + Iter.append hd (Iter.flat_map snd (Iter.of_list rest)) |> CCVector.of_iter |> CCVector.freeze in ( Procedure.modify_block proc bid (fun b -> { b with stmts }), From 00a9f7afa1ff4a23f34818d162a7867bdbc37d36 Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 13 Jul 2026 14:42:56 +1000 Subject: [PATCH 27/39] move to extras.ml --- lib/transforms/aslp/aslp_util_internal.ml | 43 +---------------------- lib/util/common.ml | 3 ++ lib/util/dune | 1 + lib/util/extras.ml | 43 +++++++++++++++++++++++ 4 files changed, 48 insertions(+), 42 deletions(-) create mode 100644 lib/util/extras.ml diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 199cdc19..6468ac34 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -4,47 +4,6 @@ open Lang open Common -(** {1 General data processing} *) - -(** Returns [Some (hd x, tl x)] if [x] is non-empty, otherwise returns [None]. -*) -let uncons = function [] -> None | hd :: tl -> Some (hd, tl) - -(** [span_while_some f xs] returns the longest prefix of [xs] where the elements - yield [Some] when mapped through [f]. - - These [Some] values are returned in the first tuple element. Upon reaching a - value which yields [None], that value and values after it are returned in - the second tuple element. *) -let span_while_some f = - let rec step f rev_somes all = - let x, rest = match all with [] -> (None, []) | hd :: tl -> (f hd, tl) in - match x with - | None -> (List.rev rev_somes, all) - | Some x -> (step [@tailcall]) f (x :: rev_somes) rest - in - step f [] - -(** Groups successive list elements based on whether they are [Left] or [Right], - maintaining relative order. - - [Left] and [Right] values within the returned list contain values like - [('a * 'a list)] to represent a non-empty list. *) -let group_succ_either : - ('a, 'b) Either.t list -> ('a * 'a list, 'b * 'b list) Either.t list = - let[@tail_mod_cons] rec while_left xs = - let xs, rest = span_while_some Either.find_left xs in - match xs with - | [] -> while_right rest (* in case the input list starts with Right *) - | h :: xs -> Either.Left (h, xs) :: while_right rest - and[@tail_mod_cons] while_right xs = - let xs, rest = span_while_some Either.find_right xs in - match xs with - | [] -> [] - | h :: xs -> Either.Right (h, xs) :: while_left rest - in - while_left - (* TODO: these could be made lazy by using Seq.t rather than list *) (** {1 Bincaml utilities} *) @@ -115,7 +74,7 @@ let flat_map_stmts (* Collects adjacent bare statements into a basic block, and inserts those statements. *) let proc = Procedure.modify_block proc base_bid Block.clear_stmts in let proc, block_id_pairs = - group_succ_either mapped + Extras.group_succ_either mapped |> List.fold_flat_map (fun proc -> function | Either.Left (hd, tl) -> (proc, hd :: tl) diff --git a/lib/util/common.ml b/lib/util/common.ml index 822d5d62..38dcd05e 100644 --- a/lib/util/common.ml +++ b/lib/util/common.ml @@ -11,6 +11,9 @@ module StringSet = Set.Make (String) module IntSet = Set.Make (Int) module Worklist = Worklist +(** Extra utilities *) +module Extras = Extras + (* Byte_slice extension for blitting to Bytes *) module Byte_slice = struct diff --git a/lib/util/dune b/lib/util/dune index 95903da4..e8bc4c88 100644 --- a/lib/util/dune +++ b/lib/util/dune @@ -6,6 +6,7 @@ fixed_width_arith mtypes common + extras unicode var ID diff --git a/lib/util/extras.ml b/lib/util/extras.ml new file mode 100644 index 00000000..ee89b715 --- /dev/null +++ b/lib/util/extras.ml @@ -0,0 +1,43 @@ +(** Extra general-purpose library functions which are not in Containers or + Stdlib. *) + +(** {1 List functions} *) + +(** Returns [Some (hd x, tl x)] if [x] is non-empty, otherwise returns [None]. +*) +let uncons = function [] -> None | hd :: tl -> Some (hd, tl) + +(** [span_while_some f xs] returns the longest prefix of [xs] where the elements + yield [Some] when mapped through [f]. + + These [Some] values are returned in the first tuple element. Upon reaching a + value which yields [None], that value and values after it are returned in + the second tuple element. *) +let span_while_some f = + let rec step f rev_somes all = + let x, rest = match all with [] -> (None, []) | hd :: tl -> (f hd, tl) in + match x with + | None -> (List.rev rev_somes, all) + | Some x -> (step [@tailcall]) f (x :: rev_somes) rest + in + step f [] + +(** Groups successive list elements based on whether they are [Left] or [Right], + maintaining relative order. + + [Left] and [Right] values within the returned list contain values like + [('a * 'a list)] to represent a non-empty list. *) +let group_succ_either : + ('a, 'b) Either.t list -> ('a * 'a list, 'b * 'b list) Either.t list = + let[@tail_mod_cons] rec while_left xs = + let xs, rest = span_while_some Either.find_left xs in + match xs with + | [] -> while_right rest (* in case the input list starts with Right *) + | h :: xs -> Either.Left (h, xs) :: while_right rest + and[@tail_mod_cons] while_right xs = + let xs, rest = span_while_some Either.find_right xs in + match xs with + | [] -> [] + | h :: xs -> Either.Right (h, xs) :: while_left rest + in + while_left From 527643d8457d61a6b8f20c1f38ac7e22ae78878c Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 13 Jul 2026 14:44:52 +1000 Subject: [PATCH 28/39] move referenced_vars_of_prog --- lib/lang/program.ml | 14 ++++++++++++-- lib/lang/program.mli | 4 ++++ lib/transforms/aslp/aslp.ml | 3 +-- lib/transforms/aslp/aslp_util_internal.ml | 10 ---------- 4 files changed, 17 insertions(+), 14 deletions(-) diff --git a/lib/lang/program.ml b/lib/lang/program.ml index 1ba360b3..6aea97da 100644 --- a/lib/lang/program.ml +++ b/lib/lang/program.ml @@ -93,9 +93,9 @@ let pretty_declaration d = | Procedure { definition } -> pretty_proc definition (*match definition with - | Some d -> + | Some d -> let param, rt = Types.uncurry (Var.typ binding) in - let param = + let param = text "let " ^ text (Var.name binding) ^ text (Var.to_decl_string_il binding) | None -> text @@ Var.to_decl_string_il binding) *) @@ -284,6 +284,16 @@ let flat_map_decls f p = else { prog with declarations = IDMap.remove i prog.declarations }) p +(** Iterates over global variables in the given program, including both read and + assigned variables. Order is unspecified and may have duplicates. *) +let referenced_vars_of_prog = + procs + %> Iter.flat_map + (snd %> Procedure.iter_blocks + %> Iter.flat_map (fun (_, b) -> + Iter.append (Block.read_vars_iter b) (Block.assigned_vars_iter b))) + %> Iter.filter Var.is_global + let pretty_to_chan chan (p : t) = let p = prog_pretty p in flush chan; diff --git a/lib/lang/program.mli b/lib/lang/program.mli index ea49abae..56f24e51 100644 --- a/lib/lang/program.mli +++ b/lib/lang/program.mli @@ -108,6 +108,10 @@ val decl_global : val decl_typ : ?attrib:'a Types.StringMap.t -> t -> Types.t -> t +val referenced_vars_of_prog : t -> Var.t Iter.t +(** Iterates over global variables in the given program, including both read and + assigned variables. Order is unspecified and may have duplicates. *) + val create_single_proc : ?name:string -> unit -> t * (Var.t, Expr.BasilExpr.t) Procedure.t diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index e2660091..67a8062d 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -153,8 +153,7 @@ let add_aarch64_global_declarations ?(add_all = false) prog = if add_all then Fun.const true else Fun.flip VarSet.mem - (Aslp_util_internal.referenced_vars_of_prog prog - |> Iter.to_set (module VarSet)) + (Program.referenced_vars_of_prog prog |> Iter.to_set (module VarSet)) in Lazy.force Aslp_lexpr.global_vars diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml index 6468ac34..4d969239 100644 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ b/lib/transforms/aslp/aslp_util_internal.ml @@ -8,16 +8,6 @@ open Common (** {1 Bincaml utilities} *) -(** Iterates over global variables in the given program, including both read and - assigned variables. Order is unspecified and may have duplicates. *) -let referenced_vars_of_prog = - Program.procs - %> Iter.flat_map - (snd %> Procedure.iter_blocks - %> Iter.flat_map (fun (_, b) -> - Iter.append (Block.read_vars_iter b) (Block.assigned_vars_iter b))) - %> Iter.filter Var.is_global - (** Replaces uses of the old block ID with the new [(first, last)] block IDs. The incoming edges to [old] will be redirected to [first] and the outgoing edges of [old] will be rebased to originate from [last]. From 9c6ccf28028c212e0e67f8da03fda2fa281f0959 Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 13 Jul 2026 14:48:47 +1000 Subject: [PATCH 29/39] move flat_map_stmts --- lib/lang/procedure.ml | 92 +++++++++++++++++++ lib/transforms/aslp/aslp.ml | 2 +- lib/transforms/aslp/aslp_util_internal.ml | 103 ---------------------- 3 files changed, 93 insertions(+), 104 deletions(-) delete mode 100644 lib/transforms/aslp/aslp_util_internal.ml diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 352f44ba..09f3629b 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -481,6 +481,21 @@ let transplant_incoming_edges p ~from ~to_ : _ t = in p |> map_graph (replace_incoming_uses ~from:(Begin from) ~to_:(Begin to_)) +(** Replaces uses of the old block ID with the new [(first, last)] block IDs. + The incoming edges to [old] will be redirected to [first] and the outgoing + edges of [old] will be rebased to originate from [last]. + + [first] and [last] may be the same. One or both of [first]/[last] may be the + same as [old]. If neither is the same as [old], [old] will be removed from + the procedure. *) +let replace_block ~old ~new_:(new_first, new_last) proc = + proc + |> transplant_incoming_edges ~from:old ~to_:new_first + |> transplant_outgoing_edges ~from:old ~to_:new_last + |> + if ID.equal old new_first || ID.equal old new_last then Fun.id + else Fun.flip remove_block old + let lookup_local_decl p v = Var.Decls.find_opt (local_decls p) v |> Option.or_lazy ~else_:(fun () -> @@ -652,6 +667,83 @@ let flat_map_stmts_topo_rev ?visit rewriter p = update_block p bid (Block.flat_map ~rev:true ~phi:Fun.id rewriter b)) p blocks +(** Maps each statement in the given block through [f]. For each statement, [f] + may return either zero or more "bare" statements, {i or} a first/last pair + of new block-level control-flow. Returns [(first, last, proc)] where [proc] + is the updated procedure and [first] / [last] is the first / last block of + the combined map output. + + [first] and [last] may be the same. One or both of [first]/[last] may be the + same as the original block. In particular, any bare statements returned by + [f] for an initial segment of the block's statements will be retained in the + original block. If [f] returns a block ID pair, then the returned block IDs + should not be the same as the original block ID - except, perhaps, for the + first block of the first statement. + + Additionally, redirects the original block's incoming/outgoing edges to the + first / last block of the mapped output. *) +let flat_map_stmts + ~(f : proc:_ t -> _ Stmt.t -> (ID.t * ID.t * _ t, _ Stmt.t list) Either.t) + ~proc base_bid = + (* TODO: do we need a new type declaration for this big Either type? *) + let b = get_block proc base_bid |> Option.get_exn_or "not found" in + + (* Map, while generating block names for bare statements returned by the mapping function. *) + let (_, proc), mapped = + b.stmts |> CCVector.to_list + |> List.fold_map + (fun (bid, proc) stmt -> + let open Either in + match (bid, f ~proc stmt) with + | _, Left (first, last, proc) -> ((None, proc), Left (first, last)) + | Some bid, Right s -> ((Some bid, proc), Right (bid, Iter.of_list s)) + | None, Right s -> + let name = ID.name base_bid in + let proc, bid = fresh_block proc ~name ~stmts:[] () in + ((Some bid, proc), Right (bid, Iter.of_list s))) + (Some base_bid, proc) + in + (* Collects adjacent bare statements into a basic block, and inserts those statements. *) + let proc = modify_block proc base_bid Block.clear_stmts in + let proc, block_id_pairs = + Extras.group_succ_either mapped + |> List.fold_flat_map + (fun proc -> function + | Either.Left (hd, tl) -> (proc, hd :: tl) + | Either.Right ((bid, hd), rest) -> + let stmts = + Iter.append hd (Iter.flat_map snd (Iter.of_list rest)) + |> CCVector.of_iter |> CCVector.freeze + in + ( modify_block proc bid (fun b -> { b with stmts }), + [ (bid, bid) ] )) + proc + in + (* Transplant predecessors and successors of the original block as needed. *) + let first, last = + ( List.head_opt block_id_pairs |> Option.map_or fst ~default:base_bid, + List.last_opt block_id_pairs |> Option.map_or snd ~default:base_bid ) + in + let proc = + proc + |> transplant_outgoing_edges ~from:base_bid ~to_:last + |> + if not ID.(equal first base_bid) then + add_goto ~from:base_bid ~targets:[ first ] + else Fun.id + in + (* Insert gotos between mapped blocks. This must happen after transplanting + so we do not transplant these edges. *) + let proc = + List.combine_gen block_id_pairs (List.drop 1 block_id_pairs) + |> Iter.of_gen + |> Iter.fold + (fun proc ((_, prev), (next, _)) -> + add_goto proc ~from:prev ~targets:[ next ]) + proc + in + (first, last, proc) + let pretty_spec show_var show_expr (p : ('a, 'b) proc_spec) = let open Containers_pp in let ml f v = if List.is_empty v then [] else [ f v ] in diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index 67a8062d..d27f69d1 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -135,7 +135,7 @@ let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt = value. *) let transform_block (module I : Bincaml_ibi.IBI) ~proc bid = let f = map_one_stmt (module I) in - let _, _, proc = Aslp_util_internal.flat_map_stmts bid ~proc ~f in + let _, _, proc = Procedure.flat_map_stmts bid ~proc ~f in proc (** Transforms the {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsics of all blocks diff --git a/lib/transforms/aslp/aslp_util_internal.ml b/lib/transforms/aslp/aslp_util_internal.ml deleted file mode 100644 index 4d969239..00000000 --- a/lib/transforms/aslp/aslp_util_internal.ml +++ /dev/null @@ -1,103 +0,0 @@ -(** Utils used in {!Aslp} which might be useful elsewhere. If the need arises, - these should be moved to a more accessible place! *) - -open Lang -open Common - -(* TODO: these could be made lazy by using Seq.t rather than list *) - -(** {1 Bincaml utilities} *) - -(** Replaces uses of the old block ID with the new [(first, last)] block IDs. - The incoming edges to [old] will be redirected to [first] and the outgoing - edges of [old] will be rebased to originate from [last]. - - [first] and [last] may be the same. One or both of [first]/[last] may be the - same as [old]. If neither is the same as [old], [old] will be removed from - the procedure. *) -let replace_block ~old ~new_:(new_first, new_last) proc = - proc - |> Procedure.transplant_incoming_edges ~from:old ~to_:new_first - |> Procedure.transplant_outgoing_edges ~from:old ~to_:new_last - |> - if ID.equal old new_first || ID.equal old new_last then Fun.id - else Fun.flip Procedure.remove_block old - -(** Maps each statement in the given block through [f]. For each statement, [f] - may return either zero or more "bare" statements, {i or} a first/last pair - of new block-level control-flow. Returns [(first, last, proc)] where [proc] - is the updated procedure and [first] / [last] is the first / last block of - the combined map output. - - [first] and [last] may be the same. One or both of [first]/[last] may be the - same as the original block. In particular, any bare statements returned by - [f] for an initial segment of the block's statements will be retained in the - original block. If [f] returns a block ID pair, then the returned block IDs - should not be the same as the original block ID - except, perhaps, for the - first block of the first statement. - - Additionally, redirects the original block's incoming/outgoing edges to the - first / last block of the mapped output. *) -let flat_map_stmts - ~(f : - proc:_ Procedure.t -> - _ Stmt.t -> - (ID.t * ID.t * _ Procedure.t, _ Stmt.t list) Either.t) ~proc base_bid = - (* TODO: do we need a new type declaration for this big Either type? *) - let b = Procedure.get_block proc base_bid |> Option.get_exn_or "not found" in - - (* Map, while generating block names for bare statements returned by the mapping function. *) - let (_, proc), mapped = - b.stmts |> CCVector.to_list - |> List.fold_map - (fun (bid, proc) stmt -> - let open Either in - match (bid, f ~proc stmt) with - | _, Left (first, last, proc) -> ((None, proc), Left (first, last)) - | Some bid, Right s -> ((Some bid, proc), Right (bid, Iter.of_list s)) - | None, Right s -> - let name = ID.name base_bid in - let proc, bid = Procedure.fresh_block proc ~name ~stmts:[] () in - ((Some bid, proc), Right (bid, Iter.of_list s))) - (Some base_bid, proc) - in - (* Collects adjacent bare statements into a basic block, and inserts those statements. *) - let proc = Procedure.modify_block proc base_bid Block.clear_stmts in - let proc, block_id_pairs = - Extras.group_succ_either mapped - |> List.fold_flat_map - (fun proc -> function - | Either.Left (hd, tl) -> (proc, hd :: tl) - | Either.Right ((bid, hd), rest) -> - let stmts = - Iter.append hd (Iter.flat_map snd (Iter.of_list rest)) - |> CCVector.of_iter |> CCVector.freeze - in - ( Procedure.modify_block proc bid (fun b -> { b with stmts }), - [ (bid, bid) ] )) - proc - in - (* Transplant predecessors and successors of the original block as needed. *) - let first, last = - ( List.head_opt block_id_pairs |> Option.map_or fst ~default:base_bid, - List.last_opt block_id_pairs |> Option.map_or snd ~default:base_bid ) - in - let proc = - proc - |> Procedure.transplant_outgoing_edges ~from:base_bid ~to_:last - |> - if not ID.(equal first base_bid) then - Procedure.add_goto ~from:base_bid ~targets:[ first ] - else Fun.id - in - (* Insert gotos between mapped blocks. This must happen after transplanting - so we do not transplant these edges. *) - let proc = - List.combine_gen block_id_pairs (List.drop 1 block_id_pairs) - |> Iter.of_gen - |> Iter.fold - (fun proc ((_, prev), (next, _)) -> - Procedure.add_goto proc ~from:prev ~targets:[ next ]) - proc - in - (first, last, proc) From 71d0674a48bc8ffdd6b3ca2c557cec1539c4adc2 Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 13 Jul 2026 14:49:28 +1000 Subject: [PATCH 30/39] rename to general_flat_map_stmts until we delete the other ones --- lib/lang/procedure.ml | 2 +- lib/transforms/aslp/aslp.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 09f3629b..8d1ad078 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -682,7 +682,7 @@ let flat_map_stmts_topo_rev ?visit rewriter p = Additionally, redirects the original block's incoming/outgoing edges to the first / last block of the mapped output. *) -let flat_map_stmts +let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> (ID.t * ID.t * _ t, _ Stmt.t list) Either.t) ~proc base_bid = (* TODO: do we need a new type declaration for this big Either type? *) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index d27f69d1..4aa59a84 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -135,7 +135,7 @@ let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt = value. *) let transform_block (module I : Bincaml_ibi.IBI) ~proc bid = let f = map_one_stmt (module I) in - let _, _, proc = Procedure.flat_map_stmts bid ~proc ~f in + let _, _, proc = Procedure.general_flat_map_stmts bid ~proc ~f in proc (** Transforms the {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsics of all blocks From 63f0aa0137647f11e1517d046a9bfef43c1f8fb7 Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 13 Jul 2026 14:50:52 +1000 Subject: [PATCH 31/39] move `proc` argument to end for piping --- lib/lang/procedure.ml | 12 ++++++------ lib/transforms/aslp/aslp.ml | 2 +- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 8d1ad078..f80e0ab2 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -667,11 +667,11 @@ let flat_map_stmts_topo_rev ?visit rewriter p = update_block p bid (Block.flat_map ~rev:true ~phi:Fun.id rewriter b)) p blocks -(** Maps each statement in the given block through [f]. For each statement, [f] - may return either zero or more "bare" statements, {i or} a first/last pair - of new block-level control-flow. Returns [(first, last, proc)] where [proc] - is the updated procedure and [first] / [last] is the first / last block of - the combined map output. +(** [general_flat_map_stmts ~f base_bid proc] maps each statement in the given + block ID through [f]. For each statement, [f] may return either zero or more + "bare" statements, {i or} a first/last pair of new block-level control-flow. + Returns [(first, last, proc)] where [proc] is the updated procedure and + [first] / [last] is the first / last block of the combined map output. [first] and [last] may be the same. One or both of [first]/[last] may be the same as the original block. In particular, any bare statements returned by @@ -684,7 +684,7 @@ let flat_map_stmts_topo_rev ?visit rewriter p = first / last block of the mapped output. *) let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> (ID.t * ID.t * _ t, _ Stmt.t list) Either.t) - ~proc base_bid = + base_bid proc = (* TODO: do we need a new type declaration for this big Either type? *) let b = get_block proc base_bid |> Option.get_exn_or "not found" in diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index 4aa59a84..3f1c0fe7 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -135,7 +135,7 @@ let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt = value. *) let transform_block (module I : Bincaml_ibi.IBI) ~proc bid = let f = map_one_stmt (module I) in - let _, _, proc = Procedure.general_flat_map_stmts bid ~proc ~f in + let _, _, proc = Procedure.general_flat_map_stmts bid ~f proc in proc (** Transforms the {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsics of all blocks From 329827e5219c8e4cd001277dae980b00d3bdd78f Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 13 Jul 2026 16:28:50 +1000 Subject: [PATCH 32/39] add and document `mapped_stmt` type --- lib/lang/procedure.ml | 50 ++++++++++++++++++++++++++----------- lib/transforms/aslp/aslp.ml | 9 ++++--- 2 files changed, 40 insertions(+), 19 deletions(-) diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index f80e0ab2..1e1176aa 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -403,8 +403,7 @@ let decl_block_exn p name ?(phis = []) let p = add_block p id ~phis ~stmts ~successors ~attrib () in (p, id) -let modify_block p id - (f : (Var.t, BasilExpr.t) Block.t -> (Var.t, BasilExpr.t) Block.t) = +let modify_block p id (f : _ Block.t -> _ Block.t) = let open Edge in let open G in let block = f (find_block p id) in @@ -667,25 +666,45 @@ let flat_map_stmts_topo_rev ?visit rewriter p = update_block p bid (Block.flat_map ~rev:true ~phi:Fun.id rewriter b)) p blocks +type ('v, 'e) mapped_stmt = + [ `Stmts of (Var.t, Var.t, BasilExpr.t) Stmt.t list + (** Zero or more straight-line statements. *) + | `Blocks of ID.t * ID.t * ('v, 'e) t + (** Block-level control-flow diamond. Represents control-flow entering at + the first ID and exiting at the second ID, and with some opaque + control-flow between them. + + The contained block IDs should be {b fresh} and should not have + control-flow edges to pre-existing blocks in the procedure. The two + block IDs may be the same ID (as long as it is fresh). + + The function building this [`Blocks] variant should modify the procedure + to insert the first/last blocks, as well as any other blocks or + control-flow edges {i between} them. This should be returned as the + third value in the variant. + + Generally, the procedure should not be modified in any other way. *) ] +(** Either a list of zero or more statements, {i or} a first/last pair of + block-level control-flow. This is used as the expected return type of + mapping one statement in {!general_flat_map_stmts}'s [~f] parameter. *) + (** [general_flat_map_stmts ~f base_bid proc] maps each statement in the given block ID through [f]. For each statement, [f] may return either zero or more "bare" statements, {i or} a first/last pair of new block-level control-flow. + See {!type-mapped_stmt} for details about [f]'s return type. + Returns [(first, last, proc)] where [proc] is the updated procedure and [first] / [last] is the first / last block of the combined map output. - [first] and [last] may be the same. One or both of [first]/[last] may be the - same as the original block. In particular, any bare statements returned by - [f] for an initial segment of the block's statements will be retained in the - original block. If [f] returns a block ID pair, then the returned block IDs - should not be the same as the original block ID - except, perhaps, for the - first block of the first statement. + The returned [first] and [last] may be the same. One or both of + [first]/[last] may be the same as the original block. In particular, any + bare statements returned by [f] for an initial segment of the block's + statements will be retained in the original block. Additionally, redirects the original block's incoming/outgoing edges to the first / last block of the mapped output. *) -let general_flat_map_stmts - ~(f : proc:_ t -> _ Stmt.t -> (ID.t * ID.t * _ t, _ Stmt.t list) Either.t) - base_bid proc = - (* TODO: do we need a new type declaration for this big Either type? *) +let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> _ mapped_stmt) base_bid + proc = let b = get_block proc base_bid |> Option.get_exn_or "not found" in (* Map, while generating block names for bare statements returned by the mapping function. *) @@ -695,9 +714,10 @@ let general_flat_map_stmts (fun (bid, proc) stmt -> let open Either in match (bid, f ~proc stmt) with - | _, Left (first, last, proc) -> ((None, proc), Left (first, last)) - | Some bid, Right s -> ((Some bid, proc), Right (bid, Iter.of_list s)) - | None, Right s -> + | _, `Blocks (first, last, proc) -> ((None, proc), Left (first, last)) + | Some bid, `Stmts s -> + ((Some bid, proc), Right (bid, Iter.of_list s)) + | None, `Stmts s -> let name = ID.name base_bid in let proc, bid = fresh_block proc ~name ~stmts:[] () in ((Some bid, proc), Right (bid, Iter.of_list s))) diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index 3f1c0fe7..2efcda11 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -110,14 +110,15 @@ let insert_one_diamond ~proc dia = If an error occurs while lifting through ASLp, an error attribute will be attached to the intrinsic (and it is excluded from subsequent calls). *) -let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt = +let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt : + _ Procedure.mapped_stmt = match aarch64_intrin_of_stmt stmt with - | None -> Either.Right [ stmt ] + | None -> `Stmts [ stmt ] | Some (opcode, address, attrib) -> ( match lift_opcode (module I) ~address opcode with | diamond -> let aslp_first, aslp_last, proc = insert_one_diamond ~proc diamond in - Either.Left + `Blocks ( aslp_first, aslp_last, Procedure.modify_block proc aslp_first (fun b -> @@ -125,7 +126,7 @@ let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt = | exception error -> let error = `String (Printexc.to_string error) in let intrin = (opcode, address, attrib) in - Either.Right [ stmt_of_aarch64_intrin ~error intrin ]) + `Stmts [ stmt_of_aarch64_intrin ~error intrin ]) (** Transforms the {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsics within the given block ID within the given procedure. From 62722ba76875152430856a65764c4260b0b1e04d Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 13 Jul 2026 16:34:43 +1000 Subject: [PATCH 33/39] assert that `Block IDs are fresh --- lib/lang/procedure.ml | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 1e1176aa..0ad95b6d 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -688,8 +688,8 @@ type ('v, 'e) mapped_stmt = block-level control-flow. This is used as the expected return type of mapping one statement in {!general_flat_map_stmts}'s [~f] parameter. *) -(** [general_flat_map_stmts ~f base_bid proc] maps each statement in the given - block ID through [f]. For each statement, [f] may return either zero or more +(** [general_flat_map_stmts ~f bid proc] maps each statement in the given block + ID through [f]. For each statement, [f] may return either zero or more "bare" statements, {i or} a first/last pair of new block-level control-flow. See {!type-mapped_stmt} for details about [f]'s return type. @@ -705,15 +705,23 @@ type ('v, 'e) mapped_stmt = first / last block of the mapped output. *) let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> _ mapped_stmt) base_bid proc = - let b = get_block proc base_bid |> Option.get_exn_or "not found" in + let existing_bids = + lazy (iter_blocks proc |> Iter.map fst |> Iter.to_set (module IDSet)) + in + let is_fresh = fun bid -> not (IDSet.mem bid (Lazy.force existing_bids)) in (* Map, while generating block names for bare statements returned by the mapping function. *) let (_, proc), mapped = - b.stmts |> CCVector.to_list + find_block proc base_bid |> Block.stmts_iter |> Iter.to_list |> List.fold_map (fun (bid, proc) stmt -> let open Either in match (bid, f ~proc stmt) with + | _, `Blocks (first, last, _) + when (not (is_fresh first)) || not (is_fresh last) -> + failwith + "general_flat_map_stmts: `Block variant requires fresh block \ + IDs" | _, `Blocks (first, last, proc) -> ((None, proc), Left (first, last)) | Some bid, `Stmts s -> ((Some bid, proc), Right (bid, Iter.of_list s)) From 27bb0380c15bfc36b191b954660396c32e169dc1 Mon Sep 17 00:00:00 2001 From: Kait <39479354+katrinafyi@users.noreply.github.com> Date: Mon, 13 Jul 2026 17:23:58 +1000 Subject: [PATCH 34/39] Update common.ml --- lib/util/common.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/util/common.ml b/lib/util/common.ml index 38dcd05e..bc79debb 100644 --- a/lib/util/common.ml +++ b/lib/util/common.ml @@ -11,8 +11,8 @@ module StringSet = Set.Make (String) module IntSet = Set.Make (Int) module Worklist = Worklist -(** Extra utilities *) module Extras = Extras +(** Extra utilities *) (* Byte_slice extension for blitting to Bytes *) From dd211e99e01da1b2a44c3e0f00ae2fc37d4622b3 Mon Sep 17 00:00:00 2001 From: rina Date: Mon, 13 Jul 2026 18:57:12 +1000 Subject: [PATCH 35/39] add `Blocks in case the user wants to return straight line blocks --- lib/lang/procedure.ml | 65 +++++++++++++++++++++++-------------- lib/transforms/aslp/aslp.ml | 2 +- 2 files changed, 41 insertions(+), 26 deletions(-) diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 0ad95b6d..53dc6899 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -669,14 +669,16 @@ let flat_map_stmts_topo_rev ?visit rewriter p = type ('v, 'e) mapped_stmt = [ `Stmts of (Var.t, Var.t, BasilExpr.t) Stmt.t list (** Zero or more straight-line statements. *) - | `Blocks of ID.t * ID.t * ('v, 'e) t - (** Block-level control-flow diamond. Represents control-flow entering at - the first ID and exiting at the second ID, and with some opaque - control-flow between them. + | `Blocks of (Var.t, BasilExpr.t) Block.t list + (** Zero or more straight-line blocks. *) + | `Graph of ID.t * ID.t * ('v, 'e) t + (** Multi-block subgraph. Represents control-flow entering at the first ID + and exiting at the second ID, and with some opaque control-flow between + them. - The contained block IDs should be {b fresh} and should not have - control-flow edges to pre-existing blocks in the procedure. The two - block IDs may be the same ID (as long as it is fresh). + The block IDs should be {b fresh} and should not have control-flow edges + to pre-existing blocks in the procedure. The two block IDs may be the + same ID (as long as it is fresh). The function building this [`Blocks] variant should modify the procedure to insert the first/last blocks, as well as any other blocks or @@ -711,25 +713,38 @@ let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> _ mapped_stmt) base_bid let is_fresh = fun bid -> not (IDSet.mem bid (Lazy.force existing_bids)) in (* Map, while generating block names for bare statements returned by the mapping function. *) - let (_, proc), mapped = + let (proc, _), mapped = find_block proc base_bid |> Block.stmts_iter |> Iter.to_list - |> List.fold_map - (fun (bid, proc) stmt -> - let open Either in - match (bid, f ~proc stmt) with - | _, `Blocks (first, last, _) - when (not (is_fresh first)) || not (is_fresh last) -> - failwith - "general_flat_map_stmts: `Block variant requires fresh block \ - IDs" - | _, `Blocks (first, last, proc) -> ((None, proc), Left (first, last)) - | Some bid, `Stmts s -> - ((Some bid, proc), Right (bid, Iter.of_list s)) - | None, `Stmts s -> - let name = ID.name base_bid in - let proc, bid = fresh_block proc ~name ~stmts:[] () in - ((Some bid, proc), Right (bid, Iter.of_list s))) - (Some base_bid, proc) + |> List.fold_flat_map + (fun (proc, bid) stmt -> + match f ~proc stmt with + | `Blocks [] | `Stmts [] -> ((proc, bid), []) + | `Blocks bs -> + let proc, bids = + List.fold_map + (fun proc b -> + let[@warning "+9"] { Block.attrib; stmts; phis } = b in + fresh_block proc ~attrib ~phis + ~stmts:(CCVector.to_list stmts) ()) + proc bs + in + ((proc, None), List.map (fun x -> Either.Left (x, x)) bids) + | `Graph (first, last, proc) -> + if is_fresh first && is_fresh last then + ((proc, None), [ Either.Left (first, last) ]) + else + failwith + "general_flat_map_stmts: `Block variant requires fresh \ + block IDs" + | `Stmts s -> + let name = ID.name base_bid and stmts = [] in + let proc, bid = + match bid with + | None -> fresh_block proc ~name ~stmts () + | Some bid -> (proc, bid) + in + ((proc, Some bid), [ Either.Right (bid, Iter.of_list s) ])) + (proc, Some base_bid) in (* Collects adjacent bare statements into a basic block, and inserts those statements. *) let proc = modify_block proc base_bid Block.clear_stmts in diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index 2efcda11..ee87936f 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -118,7 +118,7 @@ let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt : match lift_opcode (module I) ~address opcode with | diamond -> let aslp_first, aslp_last, proc = insert_one_diamond ~proc diamond in - `Blocks + `Graph ( aslp_first, aslp_last, Procedure.modify_block proc aslp_first (fun b -> From 1919e34cd8eaa9df8049c5cf0df5cc10d9ec1013 Mon Sep 17 00:00:00 2001 From: Kait <39479354+katrinafyi@users.noreply.github.com> Date: Mon, 13 Jul 2026 22:46:53 +1000 Subject: [PATCH 36/39] Update common.ml --- lib/util/common.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/lib/util/common.ml b/lib/util/common.ml index bc79debb..facec257 100644 --- a/lib/util/common.ml +++ b/lib/util/common.ml @@ -12,7 +12,6 @@ module IntSet = Set.Make (Int) module Worklist = Worklist module Extras = Extras -(** Extra utilities *) (* Byte_slice extension for blitting to Bytes *) From f1a00f1cbdff8cbb8e43ebc2bb5c67312bc9149f Mon Sep 17 00:00:00 2001 From: rina Date: Tue, 14 Jul 2026 13:17:39 +1000 Subject: [PATCH 37/39] fmt --- lib/util/common.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/lib/util/common.ml b/lib/util/common.ml index facec257..1c8e054c 100644 --- a/lib/util/common.ml +++ b/lib/util/common.ml @@ -10,7 +10,6 @@ module IntMap = Map.Make (Int) module StringSet = Set.Make (String) module IntSet = Set.Make (Int) module Worklist = Worklist - module Extras = Extras (* Byte_slice extension for blitting to Bytes *) From 7fd092948f1773718ec3a9135092d70b5eefbdd1 Mon Sep 17 00:00:00 2001 From: rina Date: Tue, 14 Jul 2026 17:25:20 +1000 Subject: [PATCH 38/39] working... IDSet.of_iter missing-record-field-pattern Or list straight-line list of blocks. --- lib/lang/procedure.ml | 80 +++++++++++++++++++++---------------------- 1 file changed, 40 insertions(+), 40 deletions(-) diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index 53dc6899..d927d51f 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -686,14 +686,13 @@ type ('v, 'e) mapped_stmt = third value in the variant. Generally, the procedure should not be modified in any other way. *) ] -(** Either a list of zero or more statements, {i or} a first/last pair of - block-level control-flow. This is used as the expected return type of - mapping one statement in {!general_flat_map_stmts}'s [~f] parameter. *) +(** Expected return type of mapping one statement through + {!general_flat_map_stmts}'s [~f] parameter. *) (** [general_flat_map_stmts ~f bid proc] maps each statement in the given block - ID through [f]. For each statement, [f] may return either zero or more - "bare" statements, {i or} a first/last pair of new block-level control-flow. - See {!type-mapped_stmt} for details about [f]'s return type. + ID through [f]. For each statement, [f] may return any number of blocks or + statememts. See {!type-mapped_stmt} for details and requirements about [f]'s + return value. Returns [(first, last, proc)] where [proc] is the updated procedure and [first] / [last] is the first / last block of the combined map output. @@ -707,44 +706,45 @@ type ('v, 'e) mapped_stmt = first / last block of the mapped output. *) let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> _ mapped_stmt) base_bid proc = - let existing_bids = - lazy (iter_blocks proc |> Iter.map fst |> Iter.to_set (module IDSet)) - in + let existing_bids = lazy (IDSet.of_iter (Iter.map fst (iter_blocks proc))) in let is_fresh = fun bid -> not (IDSet.mem bid (Lazy.force existing_bids)) in + (* Applies the [f] function while recording the current block ID for + [`Stmts] insertion, if available. + + Also normalises the output into either: + - an iter of already-inserted [(first,last)] bookend IDs, or + - a [(bid, stmts)] which will be inserted later into the specified [bid]. *) + let apply_f ~proc (cur_stmts_bid : ID.t option) stmt : + (_ t * ID.t option) + * ((ID.t * ID.t) Iter.t, ID.t * _ Stmt.t Iter.t) Either.t = + match f ~proc stmt with + | `Blocks [] | `Stmts [] -> ((proc, cur_stmts_bid), Left Iter.empty) + | `Blocks bs -> + let[@warning "+missing-record-field-pattern"] proc, bids = + List.fold_map + (fun proc { Block.attrib; stmts; phis } -> + fresh_block proc ~attrib ~phis ~stmts:(CCVector.to_list stmts) ()) + proc bs + in + ((proc, None), Left (Iter.map Pair.dup (Iter.of_list bids))) + | `Graph (first, last, proc) -> + if is_fresh first && is_fresh last then + ((proc, None), Left (Iter.singleton (first, last))) + else failwith "general_flat_map_stmts: `Graph blocks should be fresh" + | `Stmts stmts -> + let proc, bid = + match cur_stmts_bid with + | None -> fresh_block proc ~name:(ID.name base_bid) ~stmts:[] () + | Some bid -> (proc, bid) + in + ((proc, Some bid), Right (bid, Iter.of_list stmts)) + in + (* Map, while generating block names for bare statements returned by the mapping function. *) let (proc, _), mapped = find_block proc base_bid |> Block.stmts_iter |> Iter.to_list - |> List.fold_flat_map - (fun (proc, bid) stmt -> - match f ~proc stmt with - | `Blocks [] | `Stmts [] -> ((proc, bid), []) - | `Blocks bs -> - let proc, bids = - List.fold_map - (fun proc b -> - let[@warning "+9"] { Block.attrib; stmts; phis } = b in - fresh_block proc ~attrib ~phis - ~stmts:(CCVector.to_list stmts) ()) - proc bs - in - ((proc, None), List.map (fun x -> Either.Left (x, x)) bids) - | `Graph (first, last, proc) -> - if is_fresh first && is_fresh last then - ((proc, None), [ Either.Left (first, last) ]) - else - failwith - "general_flat_map_stmts: `Block variant requires fresh \ - block IDs" - | `Stmts s -> - let name = ID.name base_bid and stmts = [] in - let proc, bid = - match bid with - | None -> fresh_block proc ~name ~stmts () - | Some bid -> (proc, bid) - in - ((proc, Some bid), [ Either.Right (bid, Iter.of_list s) ])) - (proc, Some base_bid) + |> List.fold_map (fun (proc, b) -> apply_f ~proc b) (proc, Some base_bid) in (* Collects adjacent bare statements into a basic block, and inserts those statements. *) let proc = modify_block proc base_bid Block.clear_stmts in @@ -752,7 +752,7 @@ let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> _ mapped_stmt) base_bid Extras.group_succ_either mapped |> List.fold_flat_map (fun proc -> function - | Either.Left (hd, tl) -> (proc, hd :: tl) + | Either.Left (hd, tl) -> (proc, Iter.(to_list (append_l (hd :: tl)))) | Either.Right ((bid, hd), rest) -> let stmts = Iter.append hd (Iter.flat_map snd (Iter.of_list rest)) From c59fd9328c3715a819b2f7a1b2398b76e89c8539 Mon Sep 17 00:00:00 2001 From: agle Date: Wed, 15 Jul 2026 12:39:58 +1000 Subject: [PATCH 39/39] fix docs --- lib/lang/block.ml | 2 +- lib/lang/procedure.ml | 63 +++++++++++++++++-------------------- lib/transforms/aslp/aslp.ml | 2 +- 3 files changed, 31 insertions(+), 36 deletions(-) diff --git a/lib/lang/block.ml b/lib/lang/block.ml index cb411231..74fdcef7 100644 --- a/lib/lang/block.ml +++ b/lib/lang/block.ml @@ -106,7 +106,7 @@ let map ~phi f (b : ('v, 'e) t) : ('vv, 'ee) t = { stmts = Vector.map f b.stmts; phis = phi b.phis; attrib = b.attrib } (** Modify stmt list by creating a mutable copy of the underlying vector *) -let fmap_stmts_copy (f : (('a, 'a, 'b) Stmt.t, 'mut) Vector.t -> unit) b = +let fmap_stmts_copy (f : (('a, 'a, 'b) Stmt.t, Vector.rw) Vector.t -> unit) b = let v = Vector.copy b.stmts in f v; { b with stmts = Vector.freeze v } diff --git a/lib/lang/procedure.ml b/lib/lang/procedure.ml index d927d51f..1ede6454 100644 --- a/lib/lang/procedure.ml +++ b/lib/lang/procedure.ml @@ -672,39 +672,34 @@ type ('v, 'e) mapped_stmt = | `Blocks of (Var.t, BasilExpr.t) Block.t list (** Zero or more straight-line blocks. *) | `Graph of ID.t * ID.t * ('v, 'e) t - (** Multi-block subgraph. Represents control-flow entering at the first ID - and exiting at the second ID, and with some opaque control-flow between - them. - - The block IDs should be {b fresh} and should not have control-flow edges - to pre-existing blocks in the procedure. The two block IDs may be the - same ID (as long as it is fresh). - - The function building this [`Blocks] variant should modify the procedure - to insert the first/last blocks, as well as any other blocks or - control-flow edges {i between} them. This should be returned as the - third value in the variant. - - Generally, the procedure should not be modified in any other way. *) ] -(** Expected return type of mapping one statement through - {!general_flat_map_stmts}'s [~f] parameter. *) - -(** [general_flat_map_stmts ~f bid proc] maps each statement in the given block - ID through [f]. For each statement, [f] may return any number of blocks or - statememts. See {!type-mapped_stmt} for details and requirements about [f]'s - return value. - - Returns [(first, last, proc)] where [proc] is the updated procedure and - [first] / [last] is the first / last block of the combined map output. - - The returned [first] and [last] may be the same. One or both of - [first]/[last] may be the same as the original block. In particular, any - bare statements returned by [f] for an initial segment of the block's - statements will be retained in the original block. - - Additionally, redirects the original block's incoming/outgoing edges to the - first / last block of the mapped output. *) -let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> _ mapped_stmt) base_bid + (** Multi-block subgraph. [`Graph (begin, end, proc)] represents + control-flow entering at [begin] and exiting at the [end], and with any + control-flow between them. + + [proc] is the procedure modified to include fresh blocks [first] and + [end], as well as any other blocks or control-flow edges {i between} + them. [proc] should be unchanged aside from the addition of fresh blocks + and control-flow between them. [begin] should have no predcessors, and + dominate all new blocks, including [end]. [end] should have no + successors. + + [begin] and [end] may be the same block. *) ] +(** Program fragment to replace a statement during {!cfg_concatmap_block}: + either a list of sequential statements, list of sequential blocks, {i or} a + the procedure including an additional cfg fragment bounded by fresh entry + and exit block ids. *) + +(** [cfg_concatmap_block ~f bid proc] takes a function [f] from statement to a + code fragment, and replaces block [bid] in [proc] with the concatenated + result of mapping its statements through through [f]. [f] may return either + a statement list, block list, or [proc] modified to include a new CFG + fragment bounded by a begining or end block. See {!type-mapped_stmt} for + details about [f]'s return type. + + {b Returns} [(first, last, proc)] where [proc] is the updated procedure and + [first] / [last] is the first / last block of the concatenated output + program. *) +let cfg_concatmap_block ~(f : proc:_ t -> _ Stmt.t -> _ mapped_stmt) base_bid proc = let existing_bids = lazy (IDSet.of_iter (Iter.map fst (iter_blocks proc))) in let is_fresh = fun bid -> not (IDSet.mem bid (Lazy.force existing_bids)) in @@ -731,7 +726,7 @@ let general_flat_map_stmts ~(f : proc:_ t -> _ Stmt.t -> _ mapped_stmt) base_bid | `Graph (first, last, proc) -> if is_fresh first && is_fresh last then ((proc, None), Left (Iter.singleton (first, last))) - else failwith "general_flat_map_stmts: `Graph blocks should be fresh" + else failwith "cfg_concatmap_block: `Graph blocks should be fresh" | `Stmts stmts -> let proc, bid = match cur_stmts_bid with diff --git a/lib/transforms/aslp/aslp.ml b/lib/transforms/aslp/aslp.ml index ee87936f..f7b7e4d0 100644 --- a/lib/transforms/aslp/aslp.ml +++ b/lib/transforms/aslp/aslp.ml @@ -136,7 +136,7 @@ let map_one_stmt (module I : Bincaml_ibi.IBI) ~proc stmt : value. *) let transform_block (module I : Bincaml_ibi.IBI) ~proc bid = let f = map_one_stmt (module I) in - let _, _, proc = Procedure.general_flat_map_stmts bid ~f proc in + let _, _, proc = Procedure.cfg_concatmap_block bid ~f proc in proc (** Transforms the {!Lang.Stmt.Intrinsic.Aarch64Eval} intrinsics of all blocks