diff options
Diffstat (limited to 'backend/Linearizeaux.ml')
-rw-r--r-- | backend/Linearizeaux.ml | 81 |
1 files changed, 78 insertions, 3 deletions
diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index 902724e0..5914f6a3 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -12,7 +12,12 @@ open LTL open Maps -open Camlcoq + +let debug_flag = ref false + +let debug fmt = + if !debug_flag then Printf.eprintf fmt + else Printf.ifprintf stderr fmt (* Trivial enumeration, in decreasing order of PC *) @@ -29,6 +34,8 @@ let enumerate_aux f reach = (* More clever enumeration that flattens basic blocks *) +open Camlcoq + module IntSet = Set.Make(struct type t = int let compare = compare end) (* Determine join points: reachable nodes that have > 1 predecessor *) @@ -80,7 +87,7 @@ let basic_blocks f joins = | [] -> assert false | Lbranch s :: _ -> next_in_block blk minpc s | Ltailcall (sig0, ros) :: _ -> end_block blk minpc - | Lcond (cond, args, ifso, ifnot) :: _ -> + | Lcond (cond, args, ifso, ifnot, _) :: _ -> end_block blk minpc; start_block ifso; start_block ifnot | Ljumptable(arg, tbl) :: _ -> end_block blk minpc; List.iter start_block tbl @@ -110,5 +117,73 @@ let flatten_blocks blks = (* Build the enumeration *) -let enumerate_aux f reach = +let enumerate_aux_flat f reach = flatten_blocks (basic_blocks f (join_points f)) + +(** + * Alternate enumeration based on traces as identified by Duplicate.v + * + * This is a slight alteration to the above heuristic, ensuring that any + * superblock will be contiguous in memory, while still following the original + * heuristic + * + * Slight change: instead of taking the minimum pc of the superblock, we just take + * the pc of the first block. + * (experimentally this leads to slightly better performance..) + *) + +let super_blocks f joins = + let blocks = ref [] in + let visited = ref IntSet.empty in + (* start_block: + pc is the function entry point + or a join point + or the successor of a conditional test *) + let rec start_block pc = + let npc = P.to_int pc in + if not (IntSet.mem npc !visited) then begin + visited := IntSet.add npc !visited; + in_block [] npc pc + end + (* in_block: add pc to block and check successors *) + and in_block blk minpc pc = + let blk = pc :: blk in + match PTree.get pc f.fn_code with + | None -> assert false + | Some b -> + let rec do_instr_list = function + | [] -> assert false + | Lbranch s :: _ -> next_in_block blk minpc s + | Ltailcall (sig0, ros) :: _ -> end_block blk minpc + | Lcond (cond, args, ifso, ifnot, pred) :: _ -> begin + match pred with + | None -> (end_block blk minpc; start_block ifso; start_block ifnot) + | Some true -> (next_in_block blk minpc ifso; start_block ifnot) + | Some false -> (next_in_block blk minpc ifnot; start_block ifso) + end + | Ljumptable(arg, tbl) :: _ -> + end_block blk minpc; List.iter start_block tbl + | Lreturn :: _ -> end_block blk minpc + | instr :: b' -> do_instr_list b' in + do_instr_list b + (* next_in_block: check if join point and either extend block + or start block *) + and next_in_block blk minpc pc = + let npc = P.to_int pc in + if IntSet.mem npc joins + then (end_block blk minpc; start_block pc) + else in_block blk minpc pc + (* end_block: record block that we just discovered *) + and end_block blk minpc = + blocks := (minpc, List.rev blk) :: !blocks + in + start_block f.fn_entrypoint; !blocks + +(* Build the enumeration *) + +let enumerate_aux_sb f reach = + flatten_blocks (super_blocks f (join_points f)) + +let enumerate_aux f reach = + if !Clflags.option_ftracelinearize then enumerate_aux_sb f reach + else enumerate_aux_flat f reach |