From c3ce32da7d431069ef355296bef66b112a302b78 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 12:32:21 +0200 Subject: op simplify BTL intro --- aarch64/BTL_SEsimplify.v | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 aarch64/BTL_SEsimplify.v (limited to 'aarch64') diff --git a/aarch64/BTL_SEsimplify.v b/aarch64/BTL_SEsimplify.v new file mode 100644 index 00000000..34b41eee --- /dev/null +++ b/aarch64/BTL_SEsimplify.v @@ -0,0 +1,43 @@ +Require Import Coqlib Floats Values Memory. +Require Import Integers. +Require Import Op Registers. +Require Import BTL_SEtheory. +Require Import BTL_SEsimuref. + +(** Target op simplifications using "fake" values *) + +Definition target_op_simplify (op: operation) (lr: list reg) (hrs: ristate): option sval := + None. + +Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list reg) : option (condition * list_sval) := + None. + +(* Main proof of simplification *) + +(* +Lemma target_op_simplify_correct ge sp ctx op lr hrs fsv st args m: forall + (H: target_op_simplify op lr hrs = Some fsv) + (REF: ris_refines ctx hrs st) + (OK0: ris_ok ctx hrs) + (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args) + (OK2: eval_smem ctx (si_smem st) = Some m), + eval_sval ctx fsv = eval_operation ge sp op args m. +Proof. + unfold target_op_simplify; simpl. + intros H (LREF & SREF & SREG & SMEM) ? ? ?. + congruence. +Qed. + +Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall + (TARGET: target_cbranch_expanse hst c l = Some (c', l')) + (LREF : hsilocal_refines ge sp rs0 m0 hst st) + (OK: hsok_local ge sp rs0 m0 hst), + seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 = + seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. +Proof. + unfold target_cbranch_expanse, seval_condition; simpl. + intros H (LREF & SREF & SREG & SMEM) ?. + congruence. +Qed. +Global Opaque target_op_simplify. + Global Opaque target_cbranch_expanse.*) -- cgit 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 --- aarch64/ExpansionOracle.ml | 4 +- aarch64/PrepassSchedulingOracle.ml | 579 ++++++++++--------------------------- 2 files changed, 149 insertions(+), 434 deletions(-) (limited to 'aarch64') 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 + + -- cgit From 871e6642968f03f381e50ded05a687afb829e63a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 15:25:53 +0200 Subject: fix deps --- aarch64/PrepassSchedulingOracle.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index 0b3ba53a..6cb57c64 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -1,9 +1,10 @@ open AST -open RTL +open BTL open Maps open InstructionScheduler open Registers open PrepassSchedulingOracleDeps +open RTLcommonaux let use_alias_analysis () = false -- cgit From 6670aaf9a8d080de424f4f65fde8a36799645c9b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 21 Jul 2021 21:30:19 +0200 Subject: fix ci --- aarch64/BTL_SEsimplify.v | 28 +++++++++++++--------------- aarch64/ExpansionOracle.ml | 2 +- 2 files changed, 14 insertions(+), 16 deletions(-) (limited to 'aarch64') diff --git a/aarch64/BTL_SEsimplify.v b/aarch64/BTL_SEsimplify.v index 34b41eee..3e930439 100644 --- a/aarch64/BTL_SEsimplify.v +++ b/aarch64/BTL_SEsimplify.v @@ -14,30 +14,28 @@ Definition target_cbranch_expanse (prev: ristate) (cond: condition) (args: list (* Main proof of simplification *) -(* -Lemma target_op_simplify_correct ge sp ctx op lr hrs fsv st args m: forall +Lemma target_op_simplify_correct ctx op lr hrs fsv st args: forall (H: target_op_simplify op lr hrs = Some fsv) (REF: ris_refines ctx hrs st) (OK0: ris_ok ctx hrs) - (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args) - (OK2: eval_smem ctx (si_smem st) = Some m), - eval_sval ctx fsv = eval_operation ge sp op args m. + (OK1: eval_list_sval ctx (list_sval_inj (map (si_sreg st) lr)) = Some args), + eval_sval ctx fsv = eval_operation (cge ctx) (csp ctx) op args (cm0 ctx). Proof. unfold target_op_simplify; simpl. - intros H (LREF & SREF & SREG & SMEM) ? ? ?. + intros H ? ? ?. congruence. Qed. -Lemma target_cbranch_expanse_correct hst c l ge sp rs0 m0 st c' l': forall - (TARGET: target_cbranch_expanse hst c l = Some (c', l')) - (LREF : hsilocal_refines ge sp rs0 m0 hst st) - (OK: hsok_local ge sp rs0 m0 hst), - seval_condition ge sp c' (hsval_list_proj l') (si_smem st) rs0 m0 = - seval_condition ge sp c (list_sval_inj (map (si_sreg st) l)) (si_smem st) rs0 m0. +Lemma target_cbranch_expanse_correct hrs c l ctx st c' l': forall + (TARGET: target_cbranch_expanse hrs c l = Some (c', l')) + (REF: ris_refines ctx hrs st) + (OK: ris_ok ctx hrs), + eval_scondition ctx c' l' = + eval_scondition ctx c (list_sval_inj (map (si_sreg st) l)). Proof. - unfold target_cbranch_expanse, seval_condition; simpl. - intros H (LREF & SREF & SREG & SMEM) ?. + unfold target_cbranch_expanse; simpl. + intros H ? ?. congruence. Qed. Global Opaque target_op_simplify. - Global Opaque target_cbranch_expanse.*) +Global Opaque target_cbranch_expanse. diff --git a/aarch64/ExpansionOracle.ml b/aarch64/ExpansionOracle.ml index 0869007c..afcb29c2 100644 --- a/aarch64/ExpansionOracle.ml +++ b/aarch64/ExpansionOracle.ml @@ -12,4 +12,4 @@ let expanse n ibf btl = btl -let find_last_node_reg c = () +let find_last_reg c = () -- cgit From 056658bd2986d9e12ac07a54d25c08eb8a62ff60 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 28 Jul 2021 10:32:09 +0200 Subject: remove todos, clean --- aarch64/PrepassSchedulingOracle.ml | 1 - 1 file changed, 1 deletion(-) (limited to 'aarch64') diff --git a/aarch64/PrepassSchedulingOracle.ml b/aarch64/PrepassSchedulingOracle.ml index 6cb57c64..1935e785 100644 --- a/aarch64/PrepassSchedulingOracle.ml +++ b/aarch64/PrepassSchedulingOracle.ml @@ -107,7 +107,6 @@ let build_constraints_and_resources (opweights : opweights) insts btl = 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; -- cgit