diff options
| -rw-r--r-- | aarch64/Asmblockdeps.v | 193 | ||||
| -rw-r--r-- | aarch64/Asmgenproof.v | 48 | ||||
| -rw-r--r-- | aarch64/PostpassSchedulingOracle.ml | 159 |
3 files changed, 77 insertions, 323 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index bd460209..0427d1c4 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -13,13 +13,12 @@ (* *) (* *************************************************************) -(** * Translation from [Asmvliw] to [AbstractBB] *) +(** * Translation from [Asmblock] to [AbstractBB] *) -(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmvliw] into [L]. - [AbstractBB] will then define two semantics for [L]: a sequential and a parallel one. - We prove a bisimulation between the parallel semantics of [L] and [AsmVLIW]. - We also prove a bisimulation between the sequential semantics of [L] and [Asmblock]. - Then, the checkers on [Asmblock] and [Asmvliw] are deduced from those of [L]. +(** We define a specific instance [L] of [AbstractBB] and translate [bblocks] from [Asmblock] into [L]. + [AbstractBB] will then define a sequential semantics for [L]. + We prove a bisimulation between the sequential semantics of [L] and [Asmblock]. + Then, the checker on [Asmblock] is deduced from those of [L]. *) Require Import AST. @@ -114,7 +113,6 @@ Definition value := value_wrap. Record CRflags := { _CN: val; _CZ:val; _CC: val; _CV: val }. Inductive control_op := - (*| Oj_l (l: label)*) | Ob (l: label) | Obc (c: testcond) (l: label) | Obl (id: ident) @@ -327,6 +325,10 @@ Definition flags_testcond_value (c: testcond) (vCN vCZ vCC vCV: val) := end end. +(* The is argument is used to identify the source inst and avoid rewriting some code + 0 -> Ocset + 1 -> Ocsel + 2 -> Obc *) Definition cond_eval_is (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) (is: Z) := let res := flags_testcond_value c vCN vCZ vCC vCV in match is, res with @@ -355,7 +357,6 @@ Definition fnmul_eval (fsz: fsize) (v1 v2: val) := end. Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is: Z) := - match c, l with | TCeq, [Val vCZ] => cond_eval_is TCeq v1 v2 Vundef vCZ Vundef Vundef is | TCne, [Val vCZ] => cond_eval_is TCne v1 v2 Vundef vCZ Vundef Vundef is @@ -646,65 +647,6 @@ Proof. Qed. Hint Resolve is_eq_correct: wlp. -(*Definition testcond_eq (c1 c2: testcond) : ?? bool :=*) - (*RET (match c1 with*) - (*| TCeq => match c2 with*) - (*| TCeq => true*) - (*| _ => false*) - (*end*) - (*| TCne => match c2 with*) - (*| TCne => true*) - (*| _ => false*) - (*end*) - (*| TChs => match c2 with*) - (*| TChs => true*) - (*| _ => false*) - (*end*) - (*| TClo => match c2 with*) - (*| TClo => true*) - (*| _ => false*) - (*end*) - (*| TCmi => match c2 with*) - (*| TCmi => true*) - (*| _ => false*) - (*end*) - (*| TCpl => match c2 with*) - (*| TCpl => true*) - (*| _ => false*) - (*end*) - (*| TChi => match c2 with*) - (*| TChi => true*) - (*| _ => false*) - (*end*) - (*| TCls => match c2 with*) - (*| TCls => true*) - (*| _ => false*) - (*end*) - (*| TCge => match c2 with*) - (*| TCge => true*) - (*| _ => false*) - (*end*) - (*| TClt => match c2 with*) - (*| TClt => true*) - (*| _ => false*) - (*end*) - (*| TCgt => match c2 with*) - (*| TCgt => true*) - (*| _ => false*) - (*end*) - (*| TCle => match c2 with*) - (*| TCle => true*) - (*| _ => false*) - (*end*) - (*end).*) - -(*Lemma testcond_eq_correct c1 c2:*) - (*WHEN testcond_eq c1 c2 ~> b THEN b = true -> c1 = c2.*) -(*Proof.*) - (*wlp_simplify; destruct c1; destruct c2; trivial; try discriminate.*) -(*Qed.*) -(*Hint Resolve testcond_eq_correct: wlp.*) - Definition arith_op_eq (o1 o2: arith_op): ?? bool := match o1 with | OArithP n1 => @@ -802,14 +744,6 @@ Definition control_op_eq (c1 c2: control_op): ?? bool := match c2 with Otbz sz2 n2 lbl2 => iandb (RET (Int.eq n1 n2)) (iandb (phys_eq sz1 sz2) (phys_eq lbl1 lbl2)) | _ => RET false end | Obtbl tbl1 => match c2 with Obtbl tbl2 => (phys_eq tbl1 tbl2) | _ => RET false end - (*| Ocbu bt1 l1 =>*) - (*match c2 with Ocbu bt2 l2 => iandb (phys_eq bt1 bt2) (phys_eq l1 l2) | _ => RET false end*) - (*| Ojumptable tbl1 =>*) - (*match c2 with Ojumptable tbl2 => phys_eq tbl1 tbl2 | _ => RET false end*) - (*| Odiv =>*) - (*match c2 with Odiv => RET true | _ => RET false end*) - (*| Odivu =>*) - (*match c2 with Odivu => RET true | _ => RET false end*) | OIncremPC sz1 => match c2 with OIncremPC sz2 => RET (Z.eqb sz1 sz2) | _ => RET false end | OError => @@ -921,7 +855,6 @@ Definition op_eq (o1 o2: op): ?? bool := match o2 with Cvtx2w => RET true | _ => RET false end | Constant c1 => match o2 with Constant c2 => phys_eq c1 c2 | _ => RET false end - (*| _ => RET false*) end. Lemma op_eq_correct o1 o2: @@ -947,7 +880,7 @@ Module IST := ImpSimu L ImpPosDict. Import L. Import P. -(** Compilation from [Asmvliw] to [L] *) +(** Compilation from [Asmblock] to [L] *) Local Open Scope positive_scope. @@ -981,11 +914,6 @@ Proof. destruct r; destruct r'; try contradiction; discriminate. Qed. -(*Lemma creg_to_pos_discr: forall r r', r <> r' -> freg_to_pos r <> freg_to_pos r'.*) -(*Proof.*) - (*destruct r; destruct r'; try contradiction; discriminate.*) -(*Qed.*) - Definition ppos (r: preg) : R.t := match r with | CR c => match c with @@ -1005,13 +933,6 @@ Definition ppos (r: preg) : R.t := end . -(*Definition ppos_ireg0 (r: ireg0) : R.t :=*) - (*match r with*) - (*| RR0 p => ppos p*) - (*| XZR => 71*) - (*end*) -(*.*) - Notation "# r" := (ppos r) (at level 100, right associativity). Lemma not_eq_add: @@ -1147,7 +1068,9 @@ Definition trans_exit (ex: option control) : L.inst := Definition trans_arith (ai: ar_instruction) : inst := match ai with - | PArithP n rd => [(#rd, Op(Arith (OArithP n)) Enil)] + | PArithP n rd => + if destroy_X16 n then [(#rd, Op(Arith (OArithP n)) Enil); (#X16, Op (Constant Vundef) Enil)] + else [(#rd, Op(Arith (OArithP n)) Enil)] | PArithPP n rd r1 => [(#rd, Op(Arith (OArithPP n)) (PReg(#r1) @ Enil))] | PArithPPP n rd r1 r2 => [(#rd, Op(Arith (OArithPPP n)) (PReg(#r1) @ PReg(#r2) @ Enil))] | PArithRR0R n rd r1 r2 => @@ -1306,14 +1229,6 @@ Proof. intros. congruence. Qed. -(*Lemma inv_ppos_from_ireg: forall (ir: ireg),*) - (*exists x,*) - (*inv_ppos (x) = Some (DR (IR ir)).*) -(*Proof.*) - (*intros. unfold inv_ppos.*) - (*eexists (ireg_to_pos ir). destruct ir; simpl; reflexivity.*) -(*Qed.*) - Lemma ireg_pos_ppos: forall (sr: state) r, sr (ireg_to_pos r) = sr (# r). Proof. @@ -1466,19 +1381,6 @@ Proof. destruct (R.eq_dec pos x); reflexivity. Qed. -(*Ltac Simplif :=*) - (*[>((rewrite nextblock_inv by eauto with asmgen)<]*) - (*[>|| (rewrite nextblock_inv1 by eauto with asmgen)<]*) - (*((rewrite Pregmap.gss)*) - (*[>|| (rewrite nextblock_pc)<]*) - (*|| (rewrite Pregmap.gso by eauto with asmgen)*) - (*|| (rewrite assign_diff by (auto; try discriminate; try (apply ppos_discr; try discriminate; congruence); try (apply ppos_pmem_discr); *) - (*try (apply not_eq_sym; apply ppos_discr; try discriminate; congruence); try (apply not_eq_sym; apply ppos_pmem_discr); auto))*) - (*|| (rewrite assign_eq)*) - (*); auto with asmgen.*) - -(*Ltac Simpl := repeat Simplif.*) - Ltac sr_val_rwrt := repeat match goal with | [H: forall r: preg, ?sr (# r) = Val (?rsr r) |- _ ] @@ -1501,7 +1403,7 @@ Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl Ltac DDRM dr := destruct dr as [irsDDRF|frDDRF]; - [destruct irsDDRF as [irsDDRF|] + [destruct irsDDRF | idtac ]. Ltac DDRF dr := @@ -1575,7 +1477,7 @@ Ltac Simpl_update := try eapply sr_xsp_update_both; eauto; try eapply sr_pc_update_both; eauto. -Ltac Simpl sr := Simpl_exists sr; intros rr; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr; Simpl_update. +Ltac Simpl sr := Simpl_exists sr; try (intros rr; try rewrite sr_update_overwrite; replace_regs_pos sr; DPRM rr); Simpl_update. Ltac destruct_res_flag rsr := try (rewrite Pregmap.gso; discriminate_ppos); destruct (rsr _); simpl; try reflexivity. @@ -1596,6 +1498,10 @@ Ltac validate_crbit_flags c := rewrite sr_gss; rewrite Pregmap.gss; reflexivity ]. +Ltac destruct_reg_neq r1 r2 := + destruct (PregEq.eq r1 r2); subst; + [ rewrite sr_gss; rewrite Pregmap.gss; reflexivity | + rewrite assign_diff; try rewrite Pregmap.gso; fold (ppos r1); try apply ppos_discr; auto]. Lemma reg_update_overwrite: forall rsr sr r rd v1 v2 (HEQV: forall r : preg, sr (# r) = Val (rsr r)), @@ -1757,29 +1663,12 @@ Proof. discriminate_preg_flags ]). Qed. -(** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *) - -(*Module PChk := ParallelChecks L PosPseudoRegSet.*) - -(*Definition bblock_para_check (p: Asmvliw.bblock) : bool :=*) - (*PChk.is_parallelizable (trans_block p).*) - Section SECT_SEQ. -(*Import PChk.*) - -(*Arguments Pos.add: simpl never.*) -(*Arguments ppos: simpl never.*) - Variable Ge: genv. Lemma trans_arith_correct rsr mr sr rsw' old i: - (*Ge = Genv ge fn ->*) - (*match_states (State rs m) m' ->*) - (*exists em,*) - (*L.inst_run Ge (trans_arith o) m' old = Some em /\ match_states .*) match_states (State rsr mr) sr -> - (*match_states (State rsw mw) sw ->*) exec_arith_instr Ge.(_lk) i rsr = rsw' -> exists sw, inst_run Ge (trans_arith i) sr old = Some sw @@ -1788,7 +1677,16 @@ Proof. induction i. all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr. - (* PArithP *) - DIRN1 rd; Simpl sr. + destruct i. + 1,2,3: DIRN1 rd; Simpl sr. + (* Special case for Pmovimms/Pmovimmd *) + all: DIRN1 rd; Simpl sr; + try (rewrite assign_diff; discriminate_ppos; reflexivity); + try replace 24 with (#X16) by auto; + try replace 7 with (#XSP) by auto; + try (Simpl_update; intros rr; destruct_reg_neq r rr); + try (Simpl_update; intros rr; destruct_reg_neq XSP rr); + try (Simpl_update; intros rr; destruct_reg_neq f0 rr). - (* PArithPP *) DIRN1 rs; DIRN1 rd; Simpl sr. - (* PArithPPP *) @@ -1860,7 +1758,6 @@ Theorem bisimu_basic rsr mr sr bi: match_states (State rsr mr) sr -> match_outcome (exec_basic Ge.(_lk) Ge.(_genv) bi rsr mr) (inst_run Ge (trans_basic bi) sr sr). Proof. - (* a little tactic to automate reasoning on preg_eq *) Local Hint Resolve not_eq_sym ppos_pmem_discr ppos_discr: core. Local Ltac preg_eq_discr r rd := @@ -2253,32 +2150,6 @@ Proof. - congruence. Qed. -(*Lemma bblock_para_check_correct ge fn bb rs m rs' m':*) - (*Ge = Genv ge fn ->*) - (*exec_bblock ge fn bb rs m = Next rs' m' ->*) - (*bblock_para_check bb = true ->*) - (*det_parexec ge fn bb rs m rs' m'.*) -(*Proof.*) - (*intros H H0 H1 o H2. unfold bblock_para_check in H1.*) - (*exploit (bisimu rs m bb ge fn); eauto. eapply trans_state_match.*) - (*rewrite H0; simpl.*) - (*intros (s2' & EXEC & MS).*) - (*exploit bisimu_par. 2: apply (trans_state_match (State rs m)). all: eauto.*) - (*intros (o2' & PRUN & MO).*) - (*exploit parallelizable_correct. apply is_para_correct_aux. eassumption.*) - (*intro. eapply H3 in PRUN. clear H3. destruct o2'.*) - (*- inv PRUN. inv H3. unfold exec in EXEC; unfold trans_state in H.*) - (*assert (x = s2') by congruence. subst. clear H.*) - (*assert (m0 = s2') by (apply functional_extensionality; auto). subst. clear H4.*) - (*destruct o; try discriminate. inv MO. inv H. assert (s2' = x) by congruence. subst.*) - (*exploit (state_equiv (State rs' m') (State rs0 m0)).*) - (*2: eapply H4. eapply MS. intro H. inv H. reflexivity.*) - (*- unfold match_outcome in MO. destruct o.*) - (*+ inv MO. inv H3. discriminate.*) - (*+ clear MO. unfold exec in EXEC.*) - (*unfold trans_state in PRUN; rewrite EXEC in PRUN. discriminate.*) -(*Qed.*) - End SECT_SEQ. Section SECT_BBLOCK_EQUIV. @@ -2644,13 +2515,7 @@ Definition string_of_control (op: control_op) : pstring := | Otbz _ _ _ => "Otbz" | Obtbl _ => "Obtbl" | OIncremPC _ => "OIncremPC" - (*| Oj_l _ => "Oj_l"*) - (*| Ocbu _ _ => "Ocbu"*) - (*| Odiv => "Odiv"*) - (*| Odivu => "Odivu"*) - (*| Ojumptable _ => "Ojumptable"*) | OError => "OError" - (*| OIncremPC _ => "OIncremPC"*) end. Definition string_of_allocf (op: allocf_op) : pstring := diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index d062654b..7266cce8 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -787,18 +787,19 @@ Lemma exec_arith_instr_dont_move_PC ai rs rs': forall Proof. destruct ai; simpl; intros; try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate). - - destruct i; simpl in BASIC. - + unfold compare_long in BASIC; rewrite <- BASIC. - repeat rewrite Pregmap.gso; try discriminate. reflexivity. - + unfold compare_long in BASIC; rewrite <- BASIC. - repeat rewrite Pregmap.gso; try discriminate. reflexivity. - + destruct sz; - try (unfold compare_single in BASIC || unfold compare_float in BASIC); - destruct (rs r1), (rs r2); - try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). - - destruct i; simpl in BASIC; destruct is; - try (unfold compare_int in BASIC || unfold compare_long in BASIC); - try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). + - destruct i; simpl in BASIC; + unfold compare_long in BASIC; rewrite <- BASIC; + repeat rewrite Pregmap.gso; try discriminate; reflexivity. + - destruct i; simpl in BASIC. + 1,2: rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity. + destruct sz; + try (unfold compare_single in BASIC || unfold compare_float in BASIC); + destruct (rs r1), (rs r2); + try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). + - destruct i; simpl in BASIC; + destruct is; + try (unfold compare_int in BASIC || unfold compare_long in BASIC); + try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). - destruct i; simpl in BASIC; destruct sz; try (unfold compare_single in BASIC || unfold compare_float in BASIC); destruct (rs r1); @@ -1259,7 +1260,28 @@ Proof. destruct bi. { (* PArith *) simpl in *; destruct i. - 1,2,3,4,5,6: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *) + 1: { + destruct i. + 1,2,3: + try (destruct sumbool_rec; try congruence); + try (monadInv TRANSBI); + try (destruct_reg_inv); + try (inv_matchi); + try (exploit next_inst_preserved; eauto); + try (repeat destruct_reg_size); + try (destruct_ir0_reg). + 1,2: (* Special case for Pfmovimmd / Pfmovimms *) + try (monadInv TRANSBI); + try (destruct_reg_inv); + try (inv_matchi); + inversion BASIC; clear BASIC; subst; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; try congruence); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + } + 1,2,3,4,5: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *) destruct i; try (destruct sumbool_rec; try congruence); try (monadInv TRANSBI); diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index 821a1d53..463d65b5 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -17,7 +17,7 @@ open Asmblock open OpWeightsAsm open InstructionScheduler -let debug = true +let debug = false (** * Extracting infos from Asm instructions @@ -40,7 +40,7 @@ let arith_p_real = function | Padrp (_, _) -> Adrp | Pmovz (_, _, _) -> Movz | Pmovn (_, _, _) -> Movn - | Pfmovimms _ -> Fmov (* TODO not sure about this and below too *) + | Pfmovimms _ -> Fmov (* XXX We could also use load, but Fmov may be more convenient for tuning *) | Pfmovimmd _ -> Fmov let arith_pp_real = function @@ -223,10 +223,15 @@ let regXSP = Reg (Asm.DR (Asm.IR Asm.XSP)) let flags_wlocs = [ reg_of_cr Asm.CN; reg_of_cr Asm.CZ; reg_of_cr Asm.CC; reg_of_cr Asm.CV ] +let get_arith_p_wlocs = function + | Pfmovimms _ -> [ reg_of_ireg Asm.X16 ] + | Pfmovimmd _ -> [ reg_of_ireg Asm.X16 ] + | _ -> [] + let arith_p_rec i rd = { inst = arith_p_real i; - write_locs = [ rd ]; + write_locs = [ rd ] @ get_arith_p_wlocs i; read_locs = []; is_control = false; } @@ -459,7 +464,6 @@ let basic_rec i = | Pcvtx2w rd -> cvtx2w_rec (reg_of_ireg rd) let builtin_rec ef args res = - (* XXX verify this *) { inst = builtin_real; write_locs = [ Mem ]; @@ -490,7 +494,6 @@ let ctl_flow_rec i = read_locs = [ reg_of_pc ]; is_control = true; } - (* XXX not sure about X30 *) | Pbs (id, sg) -> { inst = bs_real; @@ -555,8 +558,6 @@ let ctl_flow_rec i = is_control = true; } -(* XXX Verify this (Pbtbl) *) - let control_rec i = match i with | Pbuiltin (ef, args, res) -> builtin_rec ef args res @@ -577,30 +578,12 @@ type inst_info = { write_locs : location list; read_locs : location list; is_control : bool; - usage : int array; (* resources consumed by the instruction *) + usage : int array; latency : int; } -(** Abstraction providing all the necessary informations for solving the scheduling problem *) - -(*(** Resources *)*) -(*type rname = Rissue | Rtiny | Rlite | Rfull | Rlsu | Rmau | Rbcu | Rtca | Rauxr | Rauxw | Rcrrp | Rcrwl | Rcrwh | Rnop*) - -(*let resource_names = [Rissue; Rtiny; Rlite; Rfull; Rlsu; Rmau; Rbcu; Rtca; Rauxr; Rauxw; Rcrrp; Rcrwl; Rcrwh; Rnop]*) - -(*let rec find_index elt l =*) -(*match l with*) -(*| [] -> raise Not_found*) -(*| e::l -> if (e == elt) then 0*) -(*else 1 + find_index elt l*) -(*let resource_id resource : int = find_index resource resource_names*) - -(*let resource_bounds : int array = Array.of_list (List.map resource_bound resource_names)*) - -(*let rec empty_inter la = function*) -(*| [] -> true*) -(*| b::lb -> if (List.mem b la) then false else empty_inter la lb*) +(** Abstraction providing all the necessary informations for solving the scheduling problem *) let rec_to_info (r : ab_inst_rec) : inst_info = let opweights = OpWeightsAsm.get_opweights () in @@ -616,8 +599,6 @@ let rec_to_info (r : ab_inst_rec) : inst_info = let instruction_infos bb = List.map rec_to_info (instruction_recs bb) -(*let instruction_infos bb = instruction_recs bb*) - let instruction_usages bb = let usages = List.map (fun info -> info.usage) (instruction_infos bb) in Array.of_list usages @@ -626,25 +607,9 @@ let instruction_usages bb = * Latency constraints building *) -(*(* type access = { inst: int; loc: location } *)*) - -(*let preg2int pr = Camlcoq.P.to_int @@ Asmblockdeps.ppos pr*) - -(*let loc2int = function*) -(*| Mem -> 1*) -(*| Reg pr -> preg2int pr*) - -(*(* module HashedLoc = struct*) - (*type t = { loc: location; key: int }*) - (*let equal l1 l2 = (l1.key = l2.key)*) - (*let hash l = l.key*) - (*let create (l:location) : t = { loc=l; key = loc2int l }*) -(*end *)*) - -(*(* module LocHash = Hashtbl.Make(HashedLoc) *)*) module LocHash = Hashtbl -(*(* Hash table : location => list of instruction ids *)*) +(* Hash table : location => list of instruction ids *) let rec intlist n = if n < 0 then failwith "intlist: n < 0" @@ -662,10 +627,6 @@ let rec get_accesses hashloc (ll : location list) = let compute_latency (ifrom : inst_info) = ifrom.latency -(*let dlat = inst_info_to_dlatency ito*) -(*in let lat = ifrom.latency + dlat*) -(*in assert (lat >= 0); if (lat == 0) then 1 else lat*) - let latency_constraints bb = let written = LocHash.create 70 and read = LocHash.create 70 @@ -726,8 +687,6 @@ let latency_constraints bb = * Using the InstructionScheduler *) -(* TODO RESUME HERE *) - let opweights = OpWeightsAsm.get_opweights () let build_problem bb = @@ -738,32 +697,11 @@ let build_problem bb = latency_constraints = latency_constraints bb; } -(*let rec find_min_opt (l: int option list) =*) -(*match l with*) -(*| [] -> None *) -(*| e :: l ->*) -(*begin match find_min_opt l with*) -(*| None -> e*) -(*| Some m ->*) -(*begin match e with*) -(*| None -> Some m*) -(*| Some n -> if n < m then Some n else Some m*) -(*end*) -(*end*) - -(*let rec filter_indexes predicate = function*) -(*| [] -> []*) -(*| e :: l -> if (predicate e) then e :: (filter_indexes predicate l) else filter_indexes predicate l*) - let get_from_indexes indexes l = List.map (List.nth l) indexes (*let is_basic = function PBasic _ -> true | _ -> false*) let is_control = function PControl _ -> true | _ -> false -(*let to_basic = function*) -(*| PBasic i -> i*) -(*| _ -> failwith "to_basic: control instruction found"*) - let to_control = function | PControl i -> i | _ -> failwith "to_control: basic instruction found" @@ -786,35 +724,11 @@ let repack li hd = { header = hd; body = instrs_to_bdy cut_li; exit = Some (to_control last) } else { header = hd; body = instrs_to_bdy li; exit = None } -(*let extract_some o = match o with Some e -> e | None -> failwith "extract_some: None found"*) - -(*let rec find_min = function*) -(*| [] -> None*) -(*| e :: l ->*) -(*match find_min l with*) -(*| None -> Some e*) -(*| Some m -> if (e < m) then Some e else Some m*) - -(*let rec remove_all m = function*) -(*| [] -> []*) -(*| e :: l -> if m=e then remove_all m l*) -(*else e :: (remove_all m l)*) - -(*let rec find_mins l = match find_min l with*) -(*| None -> []*) -(*| Some m -> m :: find_mins (remove_all m l)*) - -(*let find_all_indices m l = *) -(*let rec find m off = function*) -(*| [] -> []*) -(*| e :: l -> if m=e then off :: find m (off+1) l*) -(*else find m (off+1) l*) -(*in find m 0 l*) - module TimeHash = Hashtbl (*Hash table : time => list of instruction ids *) +(* Flattening the minpack result *) let hashtbl2flatarray h maxint = let rec f i = match TimeHash.find_opt h i with @@ -833,6 +747,7 @@ let find_max l = in match f l with None -> raise Not_found | Some m -> m +(* We still use the minpack algorithm even without bundles, but the result is then flattened *) (*(* [0, 2, 3, 1, 1, 2, 4, 5] -> [[0], [3, 4], [1, 5], [2], [6], [7]] *)*) let minpack_list (l : int list) = let timehash = TimeHash.create (List.length l) in @@ -847,10 +762,6 @@ let minpack_list (l : int list) = f 0 l; hashtbl2flatarray timehash (find_max l) -(*let minpack_list l =*) -(*let mins = find_mins l*) -(*in List.map (fun m -> find_all_indices m l) mins*) - let bb_to_instrs bb = body_to_instrs bb.body @ match bb.exit with None -> [] | Some e -> [ PControl e ] @@ -861,21 +772,6 @@ let build_solution bb sol = let pack = minpack_list tmp and instrs = bb_to_instrs bb in repack (get_from_indexes pack instrs) bb.header -(*in let rec bund hd = function*) -(*| [] -> []*) -(*| pack :: packs -> repack (get_from_indexes pack instrs) hd :: (bund [] packs)*) -(*in bund bb.header packs*) - -(*let print_inst oc = function i -> TargetPrinter.Target.print_instructions oc i*) -(*| Asm.Pallocframe(sz, ofs) -> Printf.fprintf oc " Pallocframe\n"*) -(*| Asm.Pfreeframe(sz, ofs) -> Printf.fprintf oc " Pfreeframe\n"*) -(*| Asm.Pbuiltin(ef, args, res) -> Printf.fprintf oc " Pbuiltin\n"*) - -(*let print_bb oc bb =*) -(*match Asmgen.Asmblock_TRANSF.unfold_bblock bb with*) -(*| Errors.OK instructions -> List.iter (print_inst oc) instructions*) -(*| Errors.Error _ -> Printf.eprintf "Error in print_bb"*) - let print_schedule sched = print_string "[ "; Array.iter (fun x -> Printf.printf "%d; " x) sched; @@ -898,35 +794,6 @@ let do_schedule bb = (* Pack result *) let pack_result (bb : bblock) = (bb.body, bb.exit) -(** - * Separates the opaque instructions such as Pfreeframe and Pallocframe - *) - -(*let is_opaque = function*) -(*| Pallocframe _ | Pfreeframe _ -> true*) -(*| _ -> false*) - -(*(* Returns : (accumulated instructions, remaining instructions, opaque instruction if found) *)*) -(*let rec biggest_wo_opaque = function - | [] -> ([], [], None) - | i :: li -> if is_opaque i then ([], li, Some i) - else let big, rem, opaque = biggest_wo_opaque li in (i :: big, rem, opaque);; - -let separate_opaque bb = - let instrs = bb_to_instrs bb - in let rec f hd li = - match li with - | [] -> [] - | li -> let big, rem, opaque = biggest_wo_opaque li in - match opaque with - | Some i -> - (match big with - | [] -> (repack [i] hd) :: (f [] rem) - | big -> (repack big hd) :: (bundlize [i] []) :: (f [] rem) - ) - | None -> (bundlize big hd) :: (f [] rem) - in f bb.header instrs*) - let smart_schedule bb = let bb' = try do_schedule bb with |