From a3319eb05543930844dedd9ac31ed1beaac3047e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 15:21:29 +0200 Subject: Fix compile on ARM/x86 backends --- Makefile | 7 +- aarch64/ExpansionOracle.ml | 4 +- aarch64/PrepassSchedulingOracle.ml | 579 +++++--------------- riscV/ExpansionOracle.ml | 1056 +----------------------------------- scheduling/BTLScheduleraux.ml | 195 +------ scheduling/BTL_Scheduler.v | 42 +- scheduling/BTLtoRTLproof.v | 8 +- x86/PrepassSchedulingOracle.ml | 4 +- 8 files changed, 181 insertions(+), 1714 deletions(-) diff --git a/Makefile b/Makefile index c9255fdb..10c4f4bf 100644 --- a/Makefile +++ b/Makefile @@ -152,15 +152,10 @@ BACKEND=\ Mach.v \ Bounds.v Stacklayout.v Stacking.v Stackingproof.v \ Asm.v Asmgen.v Asmgenproof.v Asmaux.v \ - RTLpathSE_simplify.v BTL_SEsimplify.v \ + BTL_SEsimplify.v \ $(BACKENDLIB) SCHEDULING= \ - RTLpathLivegenproof.v RTLpathSE_simu_specs.v \ - RTLpathLivegen.v RTLpathSE_impl.v \ - RTLpathproof.v RTLpathSE_theory.v \ - RTLpathSchedulerproof.v RTLpath.v \ - RTLpathScheduler.v RTLpathWFcheck.v \ BTL.v BTLmatchRTL.v BTLtoRTL.v BTLtoRTLproof.v RTLtoBTL.v RTLtoBTLproof.v \ BTL_Livecheck.v BTL_Scheduler.v BTL_Schedulerproof.v\ BTL_SEtheory.v BTL_SEsimuref.v BTL_SEimpl.v diff --git a/aarch64/ExpansionOracle.ml b/aarch64/ExpansionOracle.ml index 3b63b80d..0869007c 100644 --- a/aarch64/ExpansionOracle.ml +++ b/aarch64/ExpansionOracle.ml @@ -10,8 +10,6 @@ (* *) (* *************************************************************) -open RTLpathCommon - -let expanse (sb : superblock) code pm = (code, pm) +let expanse n ibf btl = btl let find_last_node_reg c = () diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index 2c3eb14f..0b3ba53a 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -6,472 +6,189 @@ open Registers open PrepassSchedulingOracleDeps let use_alias_analysis () = false - -let length_of_chunk = function -| Mint8signed -| Mint8unsigned -> 1 -| Mint16signed -| Mint16unsigned -> 2 -| Mint32 -| Mfloat32 -| Many32 -> 4 -| Mint64 -| Mfloat64 -| Many64 -> 8;; -let get_simple_dependencies (opweights : opweights) (seqa : (instruction*Regset.t) array) = +let build_constraints_and_resources (opweights : opweights) insts btl = let last_reg_reads : int list PTree.t ref = ref PTree.empty - and last_reg_write : (int*int) PTree.t ref = ref PTree.empty + and last_reg_write : (int * int) PTree.t ref = ref PTree.empty and last_mem_reads : int list ref = ref [] and last_mem_write : int option ref = ref None and last_branch : int option ref = ref None - and last_non_pipelined_op : int array = Array.make - opweights.nr_non_pipelined_units ( -1 ) - and latency_constraints : latency_constraint list ref = ref [] in + and last_non_pipelined_op : int array = + Array.make opweights.nr_non_pipelined_units (-1) + and latency_constraints : latency_constraint list ref = ref [] + and resources = ref [] in let add_constraint instr_from instr_to latency = assert (instr_from <= instr_to); assert (latency >= 0); - if instr_from = instr_to - then (if latency = 0 - then () - else failwith "PrepassSchedulingOracle.get_dependencies: negative self-loop") + if instr_from = instr_to then + if latency = 0 then () + else + failwith "PrepassSchedulingOracle.get_dependencies: negative self-loop" else latency_constraints := - { instr_from = instr_from; - instr_to = instr_to; - latency = latency - }:: !latency_constraints + { instr_from; instr_to; latency } :: !latency_constraints and get_last_reads reg = - match PTree.get reg !last_reg_reads - with Some l -> l - | None -> [] in + match PTree.get reg !last_reg_reads with Some l -> l | None -> [] + in let add_input_mem i = - if not (use_alias_analysis ()) - then - begin - begin - (* Read after write *) - match !last_mem_write with - | None -> () - | Some j -> add_constraint j i 1 - end; - last_mem_reads := i :: !last_mem_reads - end - and add_output_mem i = - if not (use_alias_analysis ()) - then - begin - begin - (* Write after write *) - match !last_mem_write with - | None -> () - | Some j -> add_constraint j i 1 - end; - (* Write after read *) - List.iter (fun j -> add_constraint j i 0) !last_mem_reads; - last_mem_write := Some i; - last_mem_reads := [] - end - and add_input_reg i reg = - begin + if not (use_alias_analysis ()) then ( (* Read after write *) - match PTree.get reg !last_reg_write with - | None -> () - | Some (j, latency) -> add_constraint j i latency - end; - last_reg_reads := PTree.set reg - (i :: get_last_reads reg) - !last_reg_reads - and add_output_reg i latency reg = - begin + (match !last_mem_write with None -> () | Some j -> add_constraint j i 1); + last_mem_reads := i :: !last_mem_reads) + and add_output_mem i = + if not (use_alias_analysis ()) then ( (* Write after write *) - match PTree.get reg !last_reg_write with - | None -> () - | Some (j, _) -> add_constraint j i 1 - end; - begin + (match !last_mem_write with None -> () | Some j -> add_constraint j i 1); (* Write after read *) - List.iter (fun j -> add_constraint j i 0) (get_last_reads reg) - end; + List.iter (fun j -> add_constraint j i 0) !last_mem_reads; + last_mem_write := Some i; + last_mem_reads := []) + and add_input_reg i reg = + (* Read after write *) + (match PTree.get reg !last_reg_write with + | None -> () + | Some (j, latency) -> add_constraint j i latency); + last_reg_reads := PTree.set reg (i :: get_last_reads reg) !last_reg_reads + and add_output_reg i latency reg = + (* Write after write *) + (match PTree.get reg !last_reg_write with + | None -> () + | Some (j, _) -> add_constraint j i 1); + (* Write after read *) + List.iter (fun j -> add_constraint j i 0) (get_last_reads reg); last_reg_write := PTree.set reg (i, latency) !last_reg_write; last_reg_reads := PTree.remove reg !last_reg_reads - in - let add_input_regs i regs = List.iter (add_input_reg i) regs in - let rec add_builtin_res i (res : reg builtin_res) = - match res with - | BR r -> add_output_reg i 10 r - | BR_none -> () - | BR_splitlong (hi, lo) -> add_builtin_res i hi; - add_builtin_res i lo in - let rec add_builtin_arg i (ba : reg builtin_arg) = - match ba with - | BA r -> add_input_reg i r - | BA_int _ | BA_long _ | BA_float _ | BA_single _ -> () - | BA_loadstack(_,_) -> add_input_mem i - | BA_addrstack _ -> () - | BA_loadglobal(_, _, _) -> add_input_mem i - | BA_addrglobal _ -> () - | BA_splitlong(hi, lo) -> add_builtin_arg i hi; - add_builtin_arg i lo - | BA_addptr(a1, a2) -> add_builtin_arg i a1; - add_builtin_arg i a2 in - let irreversible_action i = - match !last_branch with - | None -> () - | Some j -> add_constraint j i 1 in + in + let add_input_regs i regs = List.iter (add_input_reg i) regs + and irreversible_action i = + match !last_branch with None -> () | Some j -> add_constraint j i 1 + in let set_branch i = irreversible_action i; - last_branch := Some i in - let add_non_pipelined_resources i resources = + last_branch := Some i + and add_non_pipelined_resources i resources = Array.iter2 (fun latency last -> if latency >= 0 && last >= 0 then add_constraint last i latency) resources last_non_pipelined_op; - Array.iteri (fun rsc latency -> - if latency >= 0 - then last_non_pipelined_op.(rsc) <- i) resources + Array.iteri + (fun rsc latency -> if latency >= 0 then last_non_pipelined_op.(rsc) <- i) + resources in Array.iteri - begin - fun i (insn, other_uses) -> - List.iter (fun use -> - add_input_reg i use) - (Regset.elements other_uses); - - match insn with - | Inop _ -> () - | Iop(op, inputs, output, _) -> - add_non_pipelined_resources i - (opweights.non_pipelined_resources_of_op op (List.length inputs)); - (if Op.is_trapping_op op then irreversible_action i); - add_input_regs i inputs; - add_output_reg i (opweights.latency_of_op op (List.length inputs)) output - | Iload(trap, chunk, addressing, addr_regs, output, _) -> - (if trap=TRAP then irreversible_action i); - add_input_mem i; - add_input_regs i addr_regs; - add_output_reg i (opweights.latency_of_load trap chunk addressing (List.length addr_regs)) output - | Istore(chunk, addressing, addr_regs, input, _) -> - irreversible_action i; - add_input_regs i addr_regs; - add_input_reg i input; - add_output_mem i - | Icall(signature, ef, inputs, output, _) -> - set_branch i; - (match ef with - | Datatypes.Coq_inl r -> add_input_reg i r - | Datatypes.Coq_inr symbol -> () - ); - add_input_mem i; - add_input_regs i inputs; - add_output_reg i (opweights.latency_of_call signature ef) output; - add_output_mem i; - failwith "Icall" - | Itailcall(signature, ef, inputs) -> - set_branch i; - (match ef with - | Datatypes.Coq_inl r -> add_input_reg i r - | Datatypes.Coq_inr symbol -> () - ); - add_input_mem i; - add_input_regs i inputs; - failwith "Itailcall" - | Ibuiltin(ef, builtin_inputs, builtin_output, _) -> - set_branch i; - add_input_mem i; - List.iter (add_builtin_arg i) builtin_inputs; - add_builtin_res i builtin_output; - add_output_mem i; - failwith "Ibuiltin" - | Icond(cond, inputs, _, _, _) -> - set_branch i; - add_input_mem i; - add_input_regs i inputs - | Ijumptable(input, _) -> - set_branch i; - add_input_reg i input; - failwith "Ijumptable" - | Ireturn(Some input) -> - set_branch i; - add_input_reg i input; - failwith "Ireturn" - | Ireturn(None) -> - set_branch i; - failwith "Ireturn none" - end seqa; - !latency_constraints;; - -let resources_of_instruction (opweights : opweights) = function - | Inop _ -> Array.map (fun _ -> 0) opweights.pipelined_resource_bounds - | Iop(op, inputs, output, _) -> - opweights.resources_of_op op (List.length inputs) - | Iload(trap, chunk, addressing, addr_regs, output, _) -> - opweights.resources_of_load trap chunk addressing (List.length addr_regs) - | Istore(chunk, addressing, addr_regs, input, _) -> - opweights.resources_of_store chunk addressing (List.length addr_regs) - | Icall(signature, ef, inputs, output, _) -> - opweights.resources_of_call signature ef - | Ibuiltin(ef, builtin_inputs, builtin_output, _) -> - opweights.resources_of_builtin ef - | Icond(cond, args, _, _ , _) -> - opweights.resources_of_cond cond (List.length args) - | Itailcall _ | Ijumptable _ | Ireturn _ -> opweights.pipelined_resource_bounds - -let print_sequence pp (seqa : instruction array) = - Array.iteri ( - fun i (insn : instruction) -> - PrintRTL.print_instruction pp (i, insn)) seqa;; - -type unique_id = int - -type 'a symbolic_term_node = - | STop of Op.operation * 'a list - | STinitial_reg of int - | STother of int;; - -type symbolic_term = { - hash_id : unique_id; - hash_ct : symbolic_term symbolic_term_node - };; - -let rec print_term channel term = - match term.hash_ct with - | STop(op, args) -> - PrintOp.print_operation print_term channel (op, args) - | STinitial_reg n -> Printf.fprintf channel "x%d" n - | STother n -> Printf.fprintf channel "y%d" n;; - -type symbolic_term_table = { - st_table : (unique_id symbolic_term_node, symbolic_term) Hashtbl.t; - mutable st_next_id : unique_id };; - -let hash_init () = { - st_table = Hashtbl.create 20; - st_next_id = 0 - };; - -let ground_to_id = function - | STop(op, l) -> STop(op, List.map (fun t -> t.hash_id) l) - | STinitial_reg r -> STinitial_reg r - | STother i -> STother i;; - -let hash_node (table : symbolic_term_table) (term : symbolic_term symbolic_term_node) : symbolic_term = - let grounded = ground_to_id term in - match Hashtbl.find_opt table.st_table grounded with - | Some x -> x - | None -> - let term' = { hash_id = table.st_next_id; - hash_ct = term } in - (if table.st_next_id = max_int then failwith "hash: max_int"); - table.st_next_id <- table.st_next_id + 1; - Hashtbl.add table.st_table grounded term'; - term';; - -type access = { - base : symbolic_term; - offset : int64; - length : int - };; - -let term_equal a b = (a.hash_id = b.hash_id);; - -let access_of_addressing get_reg chunk addressing args = - match addressing, args with - | (Op.Aindexed ofs), [reg] -> Some - { base = get_reg reg; - offset = Camlcoq.camlint64_of_ptrofs ofs; - length = length_of_chunk chunk - } - | _, _ -> None ;; -(* TODO: global *) - -let symbolic_execution (seqa : instruction array) = - let regs = ref PTree.empty - and table = hash_init() in - let assign reg term = regs := PTree.set reg term !regs - and hash term = hash_node table term in - let get_reg reg = - match PTree.get reg !regs with - | None -> hash (STinitial_reg (Camlcoq.P.to_int reg)) - | Some x -> x in - let targets = Array.make (Array.length seqa) None in - Array.iteri - begin - fun i insn -> - match insn with - | Iop(Op.Omove, [input], output, _) -> - assign output (get_reg input) - | Iop(op, inputs, output, _) -> - assign output (hash (STop(op, List.map get_reg inputs))) - - | Iload(trap, chunk, addressing, args, output, _) -> - let access = access_of_addressing get_reg chunk addressing args in - targets.(i) <- access; - assign output (hash (STother(i))) - - | Icall(_, _, _, output, _) - | Ibuiltin(_, _, BR output, _) -> - assign output (hash (STother(i))) - - | Istore(chunk, addressing, args, va, _) -> - let access = access_of_addressing get_reg chunk addressing args in - targets.(i) <- access - - | Inop _ -> () - | Ibuiltin(_, _, BR_none, _) -> () - | Ibuiltin(_, _, BR_splitlong _, _) -> failwith "BR_splitlong" - - | Itailcall (_, _, _) - |Icond (_, _, _, _, _) - |Ijumptable (_, _) - |Ireturn _ -> () - end seqa; - targets;; - -let print_access channel = function - | None -> Printf.fprintf channel "any" - | Some x -> Printf.fprintf channel "%a + %Ld" print_term x.base x.offset;; - -let print_targets channel seqa = - let targets = symbolic_execution seqa in - Array.iteri - (fun i insn -> - match insn with - | Iload _ -> Printf.fprintf channel "%d: load %a\n" - i print_access targets.(i) - | Istore _ -> Printf.fprintf channel "%d: store %a\n" - i print_access targets.(i) - | _ -> () - ) seqa;; - -let may_overlap a0 b0 = - match a0, b0 with - | (None, _) | (_ , None) -> true - | (Some a), (Some b) -> - if term_equal a.base b.base - then (max a.offset b.offset) < - (min (Int64.add (Int64.of_int a.length) a.offset) - (Int64.add (Int64.of_int b.length) b.offset)) - else match a.base.hash_ct, b.base.hash_ct with - | STop(Op.Oaddrsymbol(ida, ofsa),[]), - STop(Op.Oaddrsymbol(idb, ofsb),[]) -> - (ida=idb) && - let ao = Int64.add a.offset (Camlcoq.camlint64_of_ptrofs ofsa) - and bo = Int64.add b.offset (Camlcoq.camlint64_of_ptrofs ofsb) in - (max ao bo) < - (min (Int64.add (Int64.of_int a.length) ao) - (Int64.add (Int64.of_int b.length) bo)) - | STop(Op.Oaddrstack _, []), - STop(Op.Oaddrsymbol _, []) - | STop(Op.Oaddrsymbol _, []), - STop(Op.Oaddrstack _, []) -> false - | STop(Op.Oaddrstack(ofsa),[]), - STop(Op.Oaddrstack(ofsb),[]) -> - let ao = Int64.add a.offset (Camlcoq.camlint64_of_ptrofs ofsa) - and bo = Int64.add b.offset (Camlcoq.camlint64_of_ptrofs ofsb) in - (max ao bo) < - (min (Int64.add (Int64.of_int a.length) ao) - (Int64.add (Int64.of_int b.length) bo)) - | _ -> true;; - -(* -(* TODO suboptimal quadratic algorithm *) -let get_alias_dependencies seqa = - let targets = symbolic_execution seqa - and deps = ref [] in - let add_constraint instr_from instr_to latency = - deps := { instr_from = instr_from; - instr_to = instr_to; - latency = latency - }:: !deps in - for i=0 to (Array.length seqa)-1 - do - for j=0 to i-1 - do - match seqa.(j), seqa.(i) with - | (Istore _), ((Iload _) | (Istore _)) -> - if may_overlap targets.(j) targets.(i) - then add_constraint j i 1 - | (Iload _), (Istore _) -> - if may_overlap targets.(j) targets.(i) - then add_constraint j i 0 - | (Istore _ | Iload _), (Icall _ | Ibuiltin _) - | (Icall _ | Ibuiltin _), (Icall _ | Ibuiltin _ | Iload _ | Istore _) -> - add_constraint j i 1 - | (Inop _ | Iop _), _ - | _, (Inop _ | Iop _) - | (Iload _), (Iload _) -> () - done - done; - !deps;; - *) - -let define_problem (opweights : opweights) seqa = - let simple_deps = get_simple_dependencies opweights seqa in - { max_latency = -1; + (fun i inst -> + match inst with + | Bnop _ -> + let rs = Array.map (fun _ -> 0) opweights.pipelined_resource_bounds in + resources := rs :: !resources + | Bop (op, lr, rd, _) -> + add_non_pipelined_resources i + (opweights.non_pipelined_resources_of_op op (List.length lr)); + if Op.is_trapping_op op then irreversible_action i; + add_input_regs i lr; + add_output_reg i (opweights.latency_of_op op (List.length lr)) rd; + let rs = opweights.resources_of_op op (List.length lr) in + resources := rs :: !resources + | Bload (trap, chk, addr, lr, rd, _) -> + if trap = TRAP then irreversible_action i; + add_input_mem i; + add_input_regs i lr; + add_output_reg i + (opweights.latency_of_load trap chk addr (List.length lr)) + rd; + let rs = opweights.resources_of_load trap chk addr (List.length lr) in + resources := rs :: !resources + | Bstore (chk, addr, lr, src, _) -> + irreversible_action i; + add_input_regs i lr; + add_input_reg i src; + add_output_mem i; + let rs = opweights.resources_of_store chk addr (List.length lr) in + resources := rs :: !resources + | Bcond (cond, lr, BF (Bgoto s, _), ibnot, _) -> + (* TODO gourdinl test with/out this line *) + let live = (get_some @@ PTree.get s btl).input_regs in + add_input_regs i (Regset.elements live); + set_branch i; + add_input_mem i; + add_input_regs i lr; + let rs = opweights.resources_of_cond cond (List.length lr) in + resources := rs :: !resources + | Bcond (_, _, _, _, _) -> + failwith "get_simple_dependencies: invalid Bcond" + | BF (_, _) -> failwith "get_simple_dependencies: BF" + | Bseq (_, _) -> failwith "get_simple_dependencies: Bseq") + insts; + (!latency_constraints, Array.of_list (List.rev !resources)) + +let define_problem (opweights : opweights) ibf btl = + let simple_deps, resources = + build_constraints_and_resources opweights ibf btl + in + { + max_latency = -1; resource_bounds = opweights.pipelined_resource_bounds; - instruction_usages = Array.map (resources_of_instruction opweights) (Array.map fst seqa); - latency_constraints = - (* if (use_alias_analysis ()) - then (get_alias_dependencies seqa) @ simple_deps - else *) simple_deps };; + instruction_usages = resources; + latency_constraints = simple_deps; + } let zigzag_scheduler problem early_ones = let nr_instructions = get_nr_instructions problem in - assert(nr_instructions = (Array.length early_ones)); + assert (nr_instructions = Array.length early_ones); match list_scheduler problem with | Some fwd_schedule -> - let fwd_makespan = fwd_schedule.((Array.length fwd_schedule) - 1) in - let constraints' = ref problem.latency_constraints in - Array.iteri (fun i is_early -> - if is_early then - constraints' := { - instr_from = i; - instr_to = nr_instructions ; - latency = fwd_makespan - fwd_schedule.(i) } ::!constraints' ) - early_ones; - validated_scheduler reverse_list_scheduler - { problem with latency_constraints = !constraints' } - | None -> None;; - -let prepass_scheduler_by_name name problem early_ones = + let fwd_makespan = fwd_schedule.(Array.length fwd_schedule - 1) in + let constraints' = ref problem.latency_constraints in + Array.iteri + (fun i is_early -> + if is_early then + constraints' := + { + instr_from = i; + instr_to = nr_instructions; + latency = fwd_makespan - fwd_schedule.(i); + } + :: !constraints') + early_ones; + validated_scheduler reverse_list_scheduler + { problem with latency_constraints = !constraints' } + | None -> None + +let prepass_scheduler_by_name name problem insts = match name with - | "zigzag" -> zigzag_scheduler problem early_ones + | "zigzag" -> + let early_ones = + Array.map + (fun inst -> + match inst with Bcond (_, _, _, _, _) -> true | _ -> false) + insts + in + zigzag_scheduler problem early_ones | _ -> scheduler_by_name name problem - -let schedule_sequence (seqa : (instruction*Regset.t) array) = + +let schedule_sequence insts btl = let opweights = OpWeights.get_opweights () in try - if (Array.length seqa) <= 1 - then None + if Array.length insts <= 1 then None else - begin - let nr_instructions = Array.length seqa in - (if !Clflags.option_debug_compcert > 6 - then Printf.printf "prepass scheduling length = %d\n" (Array.length seqa)); - let problem = define_problem opweights seqa in - (if !Clflags.option_debug_compcert > 7 - then (print_sequence stdout (Array.map fst seqa); - print_problem stdout problem)); - match prepass_scheduler_by_name - (!Clflags.option_fprepass_sched) - problem - (Array.map (fun (ins, _) -> - match ins with - | Icond _ -> true - | _ -> false) seqa) with - | None -> Printf.printf "no solution in prepass scheduling\n"; - None + let nr_instructions = Array.length insts in + let problem = define_problem opweights insts btl in + match + prepass_scheduler_by_name !Clflags.option_fprepass_sched problem insts + with + | None -> + Printf.printf "no solution in prepass scheduling\n"; + None | Some solution -> - let positions = Array.init nr_instructions (fun i -> i) in - Array.sort (fun i j -> - let si = solution.(i) and sj = solution.(j) in - if si < sj then -1 - else if si > sj then 1 - else i - j) positions; - Some positions - end - with (Failure s) -> + let positions = Array.init nr_instructions (fun i -> i) in + Array.sort + (fun i j -> + let si = solution.(i) and sj = solution.(j) in + if si < sj then -1 else if si > sj then 1 else i - j) + positions; + Some positions + with Failure s -> Printf.printf "failure in prepass scheduling: %s\n" s; - None;; - + None + + diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index bbcc6807..0869007c 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -10,1058 +10,6 @@ (* *) (* *************************************************************) -open RTLpathLivegenaux -open RTLpathCommon -open Datatypes -open Maps -open RTL -open Op -open Asmgen -open RTLpath -open! Integers -open Camlcoq -open Option -open AST -open DebugPrint -open RTLcommonaux +let expanse n ibf btl = btl -(** Mini CSE (a dynamic numbering is applied during expansion. - The CSE algorithm is inspired by the "static" one used in backend/CSE.v *) - -(** Managing virtual registers and node index *) - -let reg = ref 1 - -let node = ref 1 - -let r2p () = P.of_int !reg - -let n2p () = P.of_int !node - -let r2pi () = - reg := !reg + 1; - r2p () - -let n2pi () = - node := !node + 1; - n2p () - -(** Below are the types for rhs and equations *) - -type rhs = Sop of operation * int list | Smove - -type seq = Seq of int * rhs - -(** This is a mini abstraction to have a simpler representation during expansion - - Snop will be converted to Inop - - (Sr r) is inserted if the value was found in register r - - (Sexp dest rhs args succ) represent an instruction - (succesor may not be defined at this point, hence the use of type option) - - (Sfinalcond cond args succ1 succ2 info) represents a condition (which must - always be the last instruction in expansion list *) - -type expl = - | Snop of P.t - | Sr of P.t - | Sexp of P.t * rhs * P.t list * node option - | Sfinalcond of condition * P.t list * node * node * bool option - -(** Record used during the "dynamic" value numbering *) - -type numb = { - mutable nnext : int; (** Next unusued value number *) - mutable seqs : seq list; (** equations *) - mutable nreg : (P.t, int) Hashtbl.t; (** mapping registers to values *) - mutable nval : (int, P.t list) Hashtbl.t; - (** reverse mapping values to registers containing it *) -} - -let print_list_pos l = - debug "["; - List.iter (fun i -> debug "%d;" (p2i i)) l; - debug "]\n" - -let empty_numbering () = - { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 } - -let rec get_nvalues vn = function - | [] -> [] - | r :: rs -> - let v = - match Hashtbl.find_opt !vn.nreg r with - | Some v -> - debug "getnval r=%d |-> v=%d\n" (p2i r) v; - v - | None -> - let n = !vn.nnext in - debug "getnval r=%d |-> v=%d\n" (p2i r) n; - !vn.nnext <- !vn.nnext + 1; - Hashtbl.replace !vn.nreg r n; - Hashtbl.replace !vn.nval n [ r ]; - n - in - let vs = get_nvalues vn rs in - v :: vs - -let get_nval_ornil vn v = - match Hashtbl.find_opt !vn.nval v with None -> [] | Some l -> l - -let forget_reg vn rd = - match Hashtbl.find_opt !vn.nreg rd with - | Some v -> - debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v; - let old_regs = get_nval_ornil vn v in - debug "forget_reg: old_regs are:\n"; - print_list_pos old_regs; - Hashtbl.replace !vn.nval v - (List.filter (fun n -> not (P.eq n rd)) old_regs) - | None -> debug "forget_reg: no mapping for r=%d\n" (p2i rd) - -let update_reg vn rd v = - debug "update_reg: update v=%d with r=%d\n" v (p2i rd); - forget_reg vn rd; - let old_regs = get_nval_ornil vn v in - Hashtbl.replace !vn.nval v (rd :: old_regs) - -let rec find_valnum_rhs rh = function - | [] -> None - | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl - -let set_unknown vn rd = - debug "set_unknown: rd=%d\n" (p2i rd); - forget_reg vn rd; - Hashtbl.remove !vn.nreg rd - -let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> () - -let addrhs vn rd rh = - match find_valnum_rhs rh !vn.seqs with - | Some vres -> - debug "addrhs: Some v=%d\n" vres; - Hashtbl.replace !vn.nreg rd vres; - update_reg vn rd vres - | None -> - let n = !vn.nnext in - debug "addrhs: None v=%d\n" n; - !vn.nnext <- !vn.nnext + 1; - !vn.seqs <- Seq (n, rh) :: !vn.seqs; - update_reg vn rd n; - Hashtbl.replace !vn.nreg rd n - -let addsop vn v op rd = - debug "addsop\n"; - if op = Omove then ( - update_reg vn rd (List.hd v); - Hashtbl.replace !vn.nreg rd (List.hd v)) - else addrhs vn rd (Sop (op, v)) - -let rec kill_mem_operations = function - | (Seq (v, Sop (op, vl)) as eq) :: tl -> - if op_depends_on_memory op then kill_mem_operations tl - else eq :: kill_mem_operations tl - | [] -> [] - | eq :: tl -> eq :: kill_mem_operations tl - -let reg_valnum vn v = - debug "reg_valnum: trying to find a mapping for v=%d\n" v; - match Hashtbl.find !vn.nval v with - | [] -> None - | r :: rs -> - debug "reg_valnum: found a mapping r=%d\n" (p2i r); - Some r - -let rec reg_valnums vn = function - | [] -> Some [] - | v :: vs -> ( - match (reg_valnum vn v, reg_valnums vn vs) with - | Some r, Some rs -> Some (r :: rs) - | _, _ -> None) - -let find_rhs vn rh = - match find_valnum_rhs rh !vn.seqs with - | None -> None - | Some vres -> reg_valnum vn vres - -(** Functions to perform the dynamic reduction during CSE *) - -let extract_arg l = - if List.length l > 0 then - match List.hd l with - | Sr r -> (r, List.tl l) - | Sexp (rd, _, _, _) -> (rd, l) - | _ -> failwith "extract_arg: final instruction arg can not be extracted" - else failwith "extract_arg: trying to extract on an empty list" - -let extract_final vn fl fdest succ = - if List.length fl > 0 then - match List.hd fl with - | Sr r -> - if not (P.eq r fdest) then ( - let v = get_nvalues vn [ r ] in - addsop vn v Omove fdest; - Sexp (fdest, Smove, [ r ], Some succ) :: List.tl fl) - else Snop succ :: List.tl fl - | Sexp (rd, rh, args, None) -> - assert (rd = fdest); - Sexp (fdest, rh, args, Some succ) :: List.tl fl - | _ -> fl - else failwith "extract_final: trying to extract on an empty list" - -let addinst vn op args rd = - let v = get_nvalues vn args in - let rh = Sop (op, v) in - match find_rhs vn rh with - | Some r -> - debug "addinst: rhs found with r=%d\n" (p2i r); - Sr r - | None -> - addsop vn v op rd; - Sexp (rd, rh, args, None) - -(** Expansion functions *) - -type immt = - | Addiw - | Addil - | Andiw - | Andil - | Oriw - | Oril - | Xoriw - | Xoril - | Sltiw - | Sltiuw - | Sltil - | Sltiul - -let load_hilo32 vn dest hi lo = - let op1 = OEluiw hi in - if Int.eq lo Int.zero then [ addinst vn op1 [] dest ] - else - let r = r2pi () in - let op2 = OEaddiw (None, lo) in - let i1 = addinst vn op1 [] r in - let r', l = extract_arg [ i1 ] in - let i2 = addinst vn op2 [ r' ] dest in - i2 :: l - -let load_hilo64 vn dest hi lo = - let op1 = OEluil hi in - if Int64.eq lo Int64.zero then [ addinst vn op1 [] dest ] - else - let r = r2pi () in - let op2 = OEaddil (None, lo) in - let i1 = addinst vn op1 [] r in - let r', l = extract_arg [ i1 ] in - let i2 = addinst vn op2 [ r' ] dest in - i2 :: l - -let loadimm32 vn dest n = - match make_immed32 n with - | Imm32_single imm -> - let op1 = OEaddiw (Some X0_R, imm) in - [ addinst vn op1 [] dest ] - | Imm32_pair (hi, lo) -> load_hilo32 vn dest hi lo - -let loadimm64 vn dest n = - match make_immed64 n with - | Imm64_single imm -> - let op1 = OEaddil (Some X0_R, imm) in - [ addinst vn op1 [] dest ] - | Imm64_pair (hi, lo) -> load_hilo64 vn dest hi lo - | Imm64_large imm -> - let op1 = OEloadli imm in - [ addinst vn op1 [] dest ] - -let get_opimm optR imm = function - | Addiw -> OEaddiw (optR, imm) - | Andiw -> OEandiw imm - | Oriw -> OEoriw imm - | Xoriw -> OExoriw imm - | Sltiw -> OEsltiw imm - | Sltiuw -> OEsltiuw imm - | Addil -> OEaddil (optR, imm) - | Andil -> OEandil imm - | Oril -> OEoril imm - | Xoril -> OExoril imm - | Sltil -> OEsltil imm - | Sltiul -> OEsltiul imm - -let opimm32 vn a1 dest n optR op opimm = - match make_immed32 n with - | Imm32_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] - | Imm32_pair (hi, lo) -> - let r = r2pi () in - let l = load_hilo32 vn r hi lo in - let r', l' = extract_arg l in - let i = addinst vn op [ a1; r' ] dest in - i :: l' - -let opimm64 vn a1 dest n optR op opimm = - match make_immed64 n with - | Imm64_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] - | Imm64_pair (hi, lo) -> - let r = r2pi () in - let l = load_hilo64 vn r hi lo in - let r', l' = extract_arg l in - let i = addinst vn op [ a1; r' ] dest in - i :: l' - | Imm64_large imm -> - let r = r2pi () in - let op1 = OEloadli imm in - let i1 = addinst vn op1 [] r in - let r', l' = extract_arg [ i1 ] in - let i2 = addinst vn op [ a1; r' ] dest in - i2 :: l' - -let addimm32 vn a1 dest n optR = opimm32 vn a1 dest n optR Oadd Addiw - -let andimm32 vn a1 dest n = opimm32 vn a1 dest n None Oand Andiw - -let orimm32 vn a1 dest n = opimm32 vn a1 dest n None Oor Oriw - -let xorimm32 vn a1 dest n = opimm32 vn a1 dest n None Oxor Xoriw - -let sltimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltw None) Sltiw - -let sltuimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltuw None) Sltiuw - -let addimm64 vn a1 dest n optR = opimm64 vn a1 dest n optR Oaddl Addil - -let andimm64 vn a1 dest n = opimm64 vn a1 dest n None Oandl Andil - -let orimm64 vn a1 dest n = opimm64 vn a1 dest n None Oorl Oril - -let xorimm64 vn a1 dest n = opimm64 vn a1 dest n None Oxorl Xoril - -let sltimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltl None) Sltil - -let sltuimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltul None) Sltiul - -let is_inv_cmp = function Cle | Cgt -> true | _ -> false - -let make_optR is_x0 is_inv = - if is_x0 then if is_inv then Some X0_L else Some X0_R else None - -let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cond_int32s vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltw optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltw optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int32u vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEsequw optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsneuw optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltuw optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltuw optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltuw optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltuw optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int64s vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEseql optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsnel optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltl optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltl optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltl optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltl optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int64u vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEsequl optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsneul optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltul optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltul optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltul optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltul optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let is_normal_cmp = function Cne -> false | _ -> true - -let cond_float vn cmp f1 f2 dest = - match cmp with - | Ceq -> [ addinst vn OEfeqd [ f1; f2 ] dest ] - | Cne -> [ addinst vn OEfeqd [ f1; f2 ] dest ] - | Clt -> [ addinst vn OEfltd [ f1; f2 ] dest ] - | Cle -> [ addinst vn OEfled [ f1; f2 ] dest ] - | Cgt -> [ addinst vn OEfltd [ f2; f1 ] dest ] - | Cge -> [ addinst vn OEfled [ f2; f1 ] dest ] - -let cond_single vn cmp f1 f2 dest = - match cmp with - | Ceq -> [ addinst vn OEfeqs [ f1; f2 ] dest ] - | Cne -> [ addinst vn OEfeqs [ f1; f2 ] dest ] - | Clt -> [ addinst vn OEflts [ f1; f2 ] dest ] - | Cle -> [ addinst vn OEfles [ f1; f2 ] dest ] - | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ] - | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ] - -let expanse_cbranchimm_int32s vn cmp a1 n info succ1 succ2 = - if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cbranch_int32s false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int32u vn cmp a1 n info succ1 succ2 = - if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cbranch_int32u false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int64s vn cmp a1 n info succ1 succ2 = - if Int64.eq n Int64.zero then - cbranch_int64s true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cbranch_int64s false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int64u vn cmp a1 n info succ1 succ2 = - if Int64.eq n Int64.zero then - cbranch_int64u true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cbranch_int64u false cmp a1 r' info succ1 succ2 l' - -let expanse_condimm_int32s vn cmp a1 n dest = - if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest - else - match cmp with - | Ceq | Cne -> - let r = r2pi () in - let l = xorimm32 vn a1 r n in - let r', l' = extract_arg l in - cond_int32s vn true cmp r' r' dest @ l' - | Clt -> sltimm32 vn a1 dest n - | Cle -> - if Int.eq n (Int.repr Int.max_signed) then - let l = loadimm32 vn dest Int.one in - let r, l' = extract_arg l in - addinst vn (OEmayundef MUint) [ a1; r ] dest :: l' - else sltimm32 vn a1 dest (Int.add n Int.one) - | _ -> - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cond_int32s vn false cmp a1 r' dest @ l' - -let expanse_condimm_int32u vn cmp a1 n dest = - if Int.eq n Int.zero then cond_int32u vn true cmp a1 a1 dest - else - match cmp with - | Clt -> sltuimm32 vn a1 dest n - | _ -> - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cond_int32u vn false cmp a1 r' dest @ l' - -let expanse_condimm_int64s vn cmp a1 n dest = - if Int64.eq n Int64.zero then cond_int64s vn true cmp a1 a1 dest - else - match cmp with - | Ceq | Cne -> - let r = r2pi () in - let l = xorimm64 vn a1 r n in - let r', l' = extract_arg l in - cond_int64s vn true cmp r' r' dest @ l' - | Clt -> sltimm64 vn a1 dest n - | Cle -> - if Int64.eq n (Int64.repr Int64.max_signed) then - let l = loadimm32 vn dest Int.one in - let r, l' = extract_arg l in - addinst vn (OEmayundef MUlong) [ a1; r ] dest :: l' - else sltimm64 vn a1 dest (Int64.add n Int64.one) - | _ -> - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cond_int64s vn false cmp a1 r' dest @ l' - -let expanse_condimm_int64u vn cmp a1 n dest = - if Int64.eq n Int64.zero then cond_int64u vn true cmp a1 a1 dest - else - match cmp with - | Clt -> sltuimm64 vn a1 dest n - | _ -> - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cond_int64u vn false cmp a1 r' dest @ l' - -let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest = - let normal = is_normal_cmp cmp in - let normal' = if cnot then not normal else normal in - let insn = fn_cond vn cmp f1 f2 dest in - if normal' then insn - else - let r', l = extract_arg insn in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 info succ1 succ2 = - let r = r2pi () in - let normal = is_normal_cmp cmp in - let normal' = if cnot then not normal else normal in - let insn = fn_cond vn cmp f1 f2 r in - let r', l = extract_arg insn in - if normal' then - Sfinalcond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l - else Sfinalcond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l - -(** Form a list containing both sources and destination regs of an instruction *) - -let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] - -let get_regs_inst = function - | Inop _ -> [] - | Iop (_, args, dest, _) -> dest :: args - | Iload (_, _, _, args, dest, _) -> dest :: args - | Istore (_, _, args, src, _) -> src :: args - | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args) - | Itailcall (_, t, args) -> get_regindent t @ args - | Ibuiltin (_, args, dest, _) -> - AST.params_of_builtin_res dest @ AST.params_of_builtin_args args - | Icond (_, args, _, _, _) -> args - | Ijumptable (arg, _) -> [ arg ] - | Ireturn (Some r) -> [ r ] - | _ -> [] - -(** Modify pathmap according to the size of the expansion list *) - -let write_pathmap initial esize pm' = - debug "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize; - let path = get_some @@ PTree.get initial !pm' in - let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in - let path' = - { - psize = npsize; - input_regs = path.input_regs; - pre_output_regs = path.pre_output_regs; - output_regs = path.output_regs; - } - in - pm' := PTree.set initial path' !pm' - -(** Write a single instruction in the tree and update order *) - -let write_inst target_node inst code' new_order = - code' := PTree.set (P.of_int target_node) inst !code'; - new_order := P.of_int target_node :: !new_order - -(** Return olds args if the CSE numbering is empty *) - -let get_arguments vn vals args = - match reg_valnums vn vals with Some args' -> args' | None -> args - -(** Update the code tree with the expansion list *) - -let rec write_tree vn exp initial current code' new_order fturn = - debug "wt: node is %d\n" !node; - let target_node, next_node = - if fturn then (P.to_int initial, current) else (current, current - 1) - in - match exp with - | Sr r :: _ -> - failwith "write_tree: there are still some symbolic values in the list" - | Sexp (rd, Sop (op, vals), args, None) :: k -> - let args = get_arguments vn vals args in - let inst = Iop (op, args, rd, P.of_int next_node) in - write_inst target_node inst code' new_order; - write_tree vn k initial next_node code' new_order false - | [ Snop succ ] -> - let inst = Inop succ in - write_inst target_node inst code' new_order - | [ Sexp (rd, Sop (op, vals), args, Some succ) ] -> - let args = get_arguments vn vals args in - let inst = Iop (op, args, rd, succ) in - write_inst target_node inst code' new_order - | [ Sexp (rd, Smove, args, Some succ) ] -> - let inst = Iop (Omove, args, rd, succ) in - write_inst target_node inst code' new_order - | [ Sfinalcond (cond, args, succ1, succ2, info) ] -> - let inst = Icond (cond, args, succ1, succ2, info) in - write_inst target_node inst code' new_order - | [] -> () - | _ -> failwith "write_tree: invalid list" - -(** Main expansion function - TODO gourdinl to split? *) -let expanse (sb : superblock) code pm = - debug "#### New superblock for expansion oracle\n"; - let new_order = ref [] in - let liveins = ref sb.liveins in - let exp = ref [] in - let was_branch = ref false in - let was_exp = ref false in - let code' = ref code in - let pm' = ref pm in - let vn = ref (empty_numbering ()) in - Array.iter - (fun n -> - was_branch := false; - was_exp := false; - let inst = get_some @@ PTree.get n code in - (if !Clflags.option_fexpanse_rtlcond then - match inst with - (* Expansion of conditions - Ocmp *) - | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccomp\n"; - exp := cond_int32s vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccompu\n"; - exp := cond_int32u vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompimm\n"; - exp := expanse_condimm_int32s vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompuimm\n"; - exp := expanse_condimm_int32u vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccompl\n"; - exp := cond_int64s vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccomplu\n"; - exp := cond_int64u vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccomplimm\n"; - exp := expanse_condimm_int64s vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompluimm\n"; - exp := expanse_condimm_int64u vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Ccompf\n"; - exp := expanse_cond_fp vn false cond_float c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Cnotcompf\n"; - exp := expanse_cond_fp vn true cond_float c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Ccompfs\n"; - exp := expanse_cond_fp vn false cond_single c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Cnotcompfs\n"; - exp := expanse_cond_fp vn true cond_single c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - (* Expansion of branches - Ccomp *) - | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomp\n"; - exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompu\n"; - exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompimm\n"; - exp := expanse_cbranchimm_int32s vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompuimm\n"; - exp := expanse_cbranchimm_int32u vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompl\n"; - exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomplu\n"; - exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomplimm\n"; - exp := expanse_cbranchimm_int64s vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompluimm\n"; - exp := expanse_cbranchimm_int64u vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompf\n"; - exp := - expanse_cbranch_fp vn false cond_float c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Cnotcompf\n"; - exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompfs\n"; - exp := - expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Cnotcompfs\n"; - exp := - expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | _ -> ()); - (if !Clflags.option_fexpanse_others && not !was_exp then - match inst with - | Iop (Ofloatconst f, nil, dest, succ) -> ( - match make_immed64 (Floats.Float.to_bits f) with - | Imm64_single _ | Imm64_large _ -> () - | Imm64_pair (hi, lo) -> - debug "Iop/Ofloatconst\n"; - let r = r2pi () in - let l = load_hilo64 vn r hi lo in - let r', l' = extract_arg l in - exp := addinst vn Ofloat_of_bits [ r' ] dest :: l'; - exp := extract_final vn !exp dest succ; - was_exp := true) - | Iop (Osingleconst f, nil, dest, succ) -> ( - match make_immed32 (Floats.Float32.to_bits f) with - | Imm32_single imm -> () - | Imm32_pair (hi, lo) -> - debug "Iop/Osingleconst\n"; - let r = r2pi () in - let l = load_hilo32 vn r hi lo in - let r', l' = extract_arg l in - exp := addinst vn Osingle_of_bits [ r' ] dest :: l'; - exp := extract_final vn !exp dest succ; - was_exp := true) - | Iop (Ointconst n, nil, dest, succ) -> - debug "Iop/Ointconst\n"; - exp := loadimm32 vn dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Olongconst n, nil, dest, succ) -> - debug "Iop/Olongconst\n"; - exp := loadimm64 vn dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oaddimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oaddimm\n"; - exp := addimm32 vn a1 dest n None; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oaddlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oaddlimm\n"; - exp := addimm64 vn a1 dest n None; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oandimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oandimm\n"; - exp := andimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oandlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oandlimm\n"; - exp := andimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oorimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oorimm\n"; - exp := orimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oorlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oorlimm\n"; - exp := orimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oxorimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oxorimm\n"; - exp := xorimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oxorlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oxorlimm\n"; - exp := xorimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast8signed, a1 :: nil, dest, succ) -> - debug "Iop/cast8signed\n"; - let op = Oshlimm (Int.repr (Z.of_sint 24)) in - let r = r2pi () in - let i1 = addinst vn op [ a1 ] r in - let r', l = extract_arg [ i1 ] in - exp := - addinst vn (Oshrimm (Int.repr (Z.of_sint 24))) [ r' ] dest :: l; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast16signed, a1 :: nil, dest, succ) -> - debug "Iop/cast16signed\n"; - let op = Oshlimm (Int.repr (Z.of_sint 16)) in - let r = r2pi () in - let i1 = addinst vn op [ a1 ] r in - let r', l = extract_arg [ i1 ] in - exp := - addinst vn (Oshrimm (Int.repr (Z.of_sint 16))) [ r' ] dest :: l; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast32unsigned, a1 :: nil, dest, succ) -> - debug "Iop/Ocast32unsigned\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Ocast32signed in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in - exp := addinst vn op3 [ r2' ] dest :: l2; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oshrximm n, a1 :: nil, dest, succ) -> - if Int.eq n Int.zero then ( - debug "Iop/Oshrximm1\n"; - exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ]) - else if Int.eq n Int.one then ( - debug "Iop/Oshrximm2\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oadd in - let i2 = addinst vn op2 [ a1; r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrimm Int.one in - let i3 = addinst vn op3 [ r2' ] dest in - let r3, l3 = extract_arg (i3 :: l2) in - exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3) - else ( - debug "Iop/Oshrximm3\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let r3 = r2pi () in - let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshruimm (Int.sub Int.iwordsize n) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oadd in - let i3 = addinst vn op3 [ a1; r2' ] r3 in - let r3', l3 = extract_arg (i3 :: l2) in - - let op4 = Oshrimm n in - let i4 = addinst vn op4 [ r3' ] dest in - let r4, l4 = extract_arg (i4 :: l3) in - exp := addinst vn (OEmayundef (MUshrx n)) [ r4; r4 ] dest :: l4); - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oshrxlimm n, a1 :: nil, dest, succ) -> - if Int.eq n Int.zero then ( - debug "Iop/Oshrxlimm1\n"; - exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ]) - else if Int.eq n Int.one then ( - debug "Iop/Oshrxlimm2\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oaddl in - let i2 = addinst vn op2 [ a1; r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrlimm Int.one in - let i3 = addinst vn op3 [ r2' ] dest in - let r3, l3 = extract_arg (i3 :: l2) in - exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3) - else ( - debug "Iop/Oshrxlimm3\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let r3 = r2pi () in - let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oaddl in - let i3 = addinst vn op3 [ a1; r2' ] r3 in - let r3', l3 = extract_arg (i3 :: l2) in - - let op4 = Oshrlimm n in - let i4 = addinst vn op4 [ r3' ] dest in - let r4, l4 = extract_arg (i4 :: l3) in - exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4); - exp := extract_final vn !exp dest succ; - was_exp := true - | _ -> ()); - (* Update the CSE numbering *) - (if not !was_exp then - match inst with - | Iop (op, args, dest, succ) -> - let v = get_nvalues vn args in - addsop vn v op dest - | Iload (_, _, _, _, dst, _) -> set_unknown vn dst - | Istore (chk, addr, args, src, s) -> - !vn.seqs <- kill_mem_operations !vn.seqs - | Icall (_, _, _, _, _) | Itailcall (_, _, _) | Ibuiltin (_, _, _, _) -> - vn := empty_numbering () - | _ -> ()); - (* Update code, liveins, pathmap, and order of the superblock for one expansion *) - if !was_exp then ( - (if !was_branch && List.length !exp > 1 then - let lives = PTree.get n !liveins in - match lives with - | Some lives -> - let new_branch_pc = P.of_int (!node + 1) in - liveins := PTree.set new_branch_pc lives !liveins; - liveins := PTree.remove n !liveins - | _ -> ()); - node := !node + List.length !exp - 1; - write_pathmap sb.instructions.(0) (List.length !exp - 1) pm'; - write_tree vn (List.rev !exp) n !node code' new_order true) - else new_order := n :: !new_order) - sb.instructions; - sb.instructions <- Array.of_list (List.rev !new_order); - sb.liveins <- !liveins; - (!code', !pm') - -(** Compute the last used node and reg indexs *) - -let rec find_last_node_reg = function - | [] -> () - | (pc, i) :: k -> - let rec traverse_list var = function - | [] -> () - | e :: t -> - let e' = p2i e in - if e' > !var then var := e'; - traverse_list var t - in - traverse_list node [ pc ]; - traverse_list reg (get_regs_inst i); - find_last_node_reg k +let find_last_node_reg c = () diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml index b87636e1..98bc4590 100644 --- a/scheduling/BTLScheduleraux.ml +++ b/scheduling/BTLScheduleraux.ml @@ -1,199 +1,11 @@ -open AST open Maps -open Registers open BTL open BTLtypes open DebugPrint open PrintBTL open RTLcommonaux -open InstructionScheduler -open PrepassSchedulingOracleDeps - -let use_alias_analysis () = false - -let build_constraints_and_resources (opweights : opweights) insts btl = - let last_reg_reads : int list PTree.t ref = ref PTree.empty - and last_reg_write : (int * int) PTree.t ref = ref PTree.empty - and last_mem_reads : int list ref = ref [] - and last_mem_write : int option ref = ref None - and last_branch : int option ref = ref None - and last_non_pipelined_op : int array = - Array.make opweights.nr_non_pipelined_units (-1) - and latency_constraints : latency_constraint list ref = ref [] - and resources = ref [] in - let add_constraint instr_from instr_to latency = - assert (instr_from <= instr_to); - assert (latency >= 0); - if instr_from = instr_to then - if latency = 0 then () - else - failwith "PrepassSchedulingOracle.get_dependencies: negative self-loop" - else - latency_constraints := - { instr_from; instr_to; latency } :: !latency_constraints - and get_last_reads reg = - match PTree.get reg !last_reg_reads with Some l -> l | None -> [] - in - let add_input_mem i = - if not (use_alias_analysis ()) then ( - (* Read after write *) - (match !last_mem_write with None -> () | Some j -> add_constraint j i 1); - last_mem_reads := i :: !last_mem_reads) - and add_output_mem i = - if not (use_alias_analysis ()) then ( - (* Write after write *) - (match !last_mem_write with None -> () | Some j -> add_constraint j i 1); - (* Write after read *) - List.iter (fun j -> add_constraint j i 0) !last_mem_reads; - last_mem_write := Some i; - last_mem_reads := []) - and add_input_reg i reg = - (* Read after write *) - (match PTree.get reg !last_reg_write with - | None -> () - | Some (j, latency) -> add_constraint j i latency); - last_reg_reads := PTree.set reg (i :: get_last_reads reg) !last_reg_reads - and add_output_reg i latency reg = - (* Write after write *) - (match PTree.get reg !last_reg_write with - | None -> () - | Some (j, _) -> add_constraint j i 1); - (* Write after read *) - List.iter (fun j -> add_constraint j i 0) (get_last_reads reg); - last_reg_write := PTree.set reg (i, latency) !last_reg_write; - last_reg_reads := PTree.remove reg !last_reg_reads - in - let add_input_regs i regs = List.iter (add_input_reg i) regs - and irreversible_action i = - match !last_branch with None -> () | Some j -> add_constraint j i 1 - in - let set_branch i = - irreversible_action i; - last_branch := Some i - and add_non_pipelined_resources i resources = - Array.iter2 - (fun latency last -> - if latency >= 0 && last >= 0 then add_constraint last i latency) - resources last_non_pipelined_op; - Array.iteri - (fun rsc latency -> if latency >= 0 then last_non_pipelined_op.(rsc) <- i) - resources - in - Array.iteri - (fun i inst -> - match inst with - | Bnop _ -> - let rs = Array.map (fun _ -> 0) opweights.pipelined_resource_bounds in - resources := rs :: !resources - | Bop (op, lr, rd, _) -> - add_non_pipelined_resources i - (opweights.non_pipelined_resources_of_op op (List.length lr)); - if Op.is_trapping_op op then irreversible_action i; - add_input_regs i lr; - add_output_reg i (opweights.latency_of_op op (List.length lr)) rd; - let rs = opweights.resources_of_op op (List.length lr) in - resources := rs :: !resources - | Bload (trap, chk, addr, lr, rd, _) -> - if trap = TRAP then irreversible_action i; - add_input_mem i; - add_input_regs i lr; - add_output_reg i - (opweights.latency_of_load trap chk addr (List.length lr)) - rd; - let rs = opweights.resources_of_load trap chk addr (List.length lr) in - resources := rs :: !resources - | Bstore (chk, addr, lr, src, _) -> - irreversible_action i; - add_input_regs i lr; - add_input_reg i src; - add_output_mem i; - let rs = opweights.resources_of_store chk addr (List.length lr) in - resources := rs :: !resources - | Bcond (cond, lr, BF (Bgoto s, _), ibnot, _) -> - (* TODO gourdinl test with/out this line *) - let live = (get_some @@ PTree.get s btl).input_regs in - add_input_regs i (Regset.elements live); - set_branch i; - add_input_mem i; - add_input_regs i lr; - let rs = opweights.resources_of_cond cond (List.length lr) in - resources := rs :: !resources - | Bcond (_, _, _, _, _) -> - failwith "get_simple_dependencies: invalid Bcond" - | BF (_, _) -> failwith "get_simple_dependencies: BF" - | Bseq (_, _) -> failwith "get_simple_dependencies: Bseq") - insts; - (!latency_constraints, Array.of_list (List.rev !resources)) - -let define_problem (opweights : opweights) ibf btl = - let simple_deps, resources = - build_constraints_and_resources opweights ibf btl - in - { - max_latency = -1; - resource_bounds = opweights.pipelined_resource_bounds; - instruction_usages = resources; - latency_constraints = simple_deps; - } - -let zigzag_scheduler problem early_ones = - let nr_instructions = get_nr_instructions problem in - assert (nr_instructions = Array.length early_ones); - match list_scheduler problem with - | Some fwd_schedule -> - let fwd_makespan = fwd_schedule.(Array.length fwd_schedule - 1) in - let constraints' = ref problem.latency_constraints in - Array.iteri - (fun i is_early -> - if is_early then - constraints' := - { - instr_from = i; - instr_to = nr_instructions; - latency = fwd_makespan - fwd_schedule.(i); - } - :: !constraints') - early_ones; - validated_scheduler reverse_list_scheduler - { problem with latency_constraints = !constraints' } - | None -> None - -let prepass_scheduler_by_name name problem insts = - match name with - | "zigzag" -> - let early_ones = - Array.map - (fun inst -> - match inst with Bcond (_, _, _, _, _) -> true | _ -> false) - insts - in - zigzag_scheduler problem early_ones - | _ -> scheduler_by_name name problem - -let schedule_sequence insts btl = - let opweights = OpWeights.get_opweights () in - try - if Array.length insts <= 1 then None - else - let nr_instructions = Array.length insts in - let problem = define_problem opweights insts btl in - match - prepass_scheduler_by_name !Clflags.option_fprepass_sched problem insts - with - | None -> - Printf.printf "no solution in prepass scheduling\n"; - None - | Some solution -> - let positions = Array.init nr_instructions (fun i -> i) in - Array.sort - (fun i j -> - let si = solution.(i) and sj = solution.(j) in - if si < sj then -1 else if si > sj then 1 else i - j) - positions; - Some positions - with Failure s -> - Printf.printf "failure in prepass scheduling: %s\n" s; - None +open ExpansionOracle +open PrepassSchedulingOracle let flatten_blk_basics ibf = let ib = ibf.entry in @@ -241,7 +53,8 @@ let schedule_blk n ibf btl = let rec do_schedule btl = function | [] -> btl | (n, ibf) :: blks -> - let btl' = schedule_blk n ibf btl in + let code_exp = expanse n ibf btl in + let btl' = schedule_blk n ibf code_exp in do_schedule btl' blks let btl_scheduler f = diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index e7d2b37f..a3053add 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -60,35 +60,33 @@ Fixpoint check_symbolic_simu_rec (f1 f2: BTL.function) (lpc: list node): res uni end end. -Definition check_symbolic_simu (f1 f2: BTL.function): res unit := - check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))). - -Lemma check_symbolic_simu_rec_input_equiv lpc: forall f1 f2 x, - check_symbolic_simu_rec f1 f2 lpc = OK x -> - lpc = (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))) -> - equiv_input_regs f1 f2. +Definition erase_input_regs f1 f2 := + let code := PTree.map (fun pc ibf => + let oibf := match (fn_code f1)!pc with + | None => ibf + | Some oibf => oibf + end in + let regs := oibf.(input_regs) in + {| entry:= ibf.(entry); input_regs := regs; binfo := ibf.(binfo) |}) (fn_code f2) in + BTL.mkfunction (fn_sig f2) (fn_params f2) (fn_stacksize f2) code (fn_entrypoint f2). + +Lemma erase_input_regs_correct f1 f2 f3: + erase_input_regs f1 f2 = f3 -> + equiv_input_regs f1 f3. Proof. + unfold erase_input_regs; destruct f3; simpl; intros. + unfold equiv_input_regs; intuition auto. simpl. Admitted. -(* - unfold equiv_input_regs; induction lpc; simpl; intros f1 f2 x X EQL1. - - destruct (map _ _) eqn:EQL2; inv X; intuition; - symmetry in EQL1; apply map_eq_nil in EQL1; apply map_eq_nil in EQL2. - + destruct (fn_code f1), (fn_code f2); simpl in *; auto. - inv EQL2. - unfold PTree.elements in EQL1. - + admit. - + - destruct ((fn_code f1) ! a), ((fn_code f2) ! a); monadInv X. - eapply IHlpc; eauto. -Qed. - *) + +Definition check_symbolic_simu (f1 f2: BTL.function): res unit := + (*let f3 := erase_input_regs f1 f2 in*) + check_symbolic_simu_rec f1 f2 (List.map (fun elt => fst elt) (PTree.elements (fn_code f1))). Lemma check_symbolic_simu_input_equiv x f1 f2: check_symbolic_simu f1 f2 = OK x -> equiv_input_regs f1 f2. Proof. unfold check_symbolic_simu; simpl; intros X. - eapply check_symbolic_simu_rec_input_equiv; eauto. -Qed. +Admitted. Lemma check_symbolic_simu_rec_correct lpc: forall f1 f2 x, check_symbolic_simu_rec f1 f2 lpc = OK x -> diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 75f67d51..9b8dabab 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -231,13 +231,13 @@ Proof. - (* exec_load *) inv MIB. exists pc'; split; auto; constructor. apply plus_one. eapply exec_Iload; eauto. - erewrite <- eval_addressing_preserved; eauto. - intros; rewrite symbols_preserved; trivial. + all: erewrite <- eval_addressing_preserved; eauto; + intros; rewrite symbols_preserved; trivial. - (* exec_store *) inv MIB. exists pc'; split; auto; constructor. apply plus_one. eapply exec_Istore; eauto. - erewrite <- eval_addressing_preserved; eauto. - intros; rewrite symbols_preserved; trivial. + all: erewrite <- eval_addressing_preserved; eauto; + intros; rewrite symbols_preserved; trivial. - (* exec_seq_stop *) inv MIB; eauto. - (* exec_seq_continue *) diff --git a/x86/PrepassSchedulingOracle.ml b/x86/PrepassSchedulingOracle.ml index 7b6a1b14..31b4ea5b 100644 --- a/x86/PrepassSchedulingOracle.ml +++ b/x86/PrepassSchedulingOracle.ml @@ -1,5 +1,3 @@ -open RTL -open Registers (* Do not do anything *) -let schedule_sequence (seqa : (instruction*Regset.t) array) = None +let schedule_sequence inst btl = None -- cgit