diff options
| -rw-r--r-- | aarch64/Asmblockdeps.v | 252 | ||||
| -rw-r--r-- | aarch64/PostpassSchedulingOracle.ml | 42 |
2 files changed, 227 insertions, 67 deletions
diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index e1a49a55..88cca121 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -242,13 +242,12 @@ Definition flags_testcond_value (c: testcond) (vCN vCZ vCC vCV: val) := end end. -Definition cset_eval (c: testcond) (vCN vCZ vCC vCV: val) := +Definition csetsel_eval (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) (is_set: bool) := let res := flags_testcond_value c vCN vCZ vCC vCV in - (if_opt_bool_val res (Vint Int.one) (Vint Int.zero)). - -Definition csel_eval (c: testcond) (v1 v2 vCN vCZ vCC vCV: val) := - let res := flags_testcond_value c vCN vCZ vCC vCV in - (if_opt_bool_val res v1 v2). + (if is_set then + (if_opt_bool_val res (Vint Int.one) (Vint Int.zero)) + else + (if_opt_bool_val res v1 v2)). Definition fmovi_eval (fsz: fsize) (v: val) := match fsz with @@ -270,6 +269,23 @@ Definition fnmul_eval (fsz: fsize) (v1 v2: val) := Definition op:=op_wrap. +Definition cflags_eval (c: testcond) (l: list value) (v1 v2: val) (is_set: bool) := + match c, l with + | TCeq, [Val vCZ] => Some (Val (csetsel_eval TCeq v1 v2 Vundef vCZ Vundef Vundef is_set)) + | TCne, [Val vCZ] => Some (Val (csetsel_eval TCne v1 v2 Vundef vCZ Vundef Vundef is_set)) + | TChs, [Val vCC] => Some (Val (csetsel_eval TChs v1 v2 Vundef Vundef vCC Vundef is_set)) + | TClo, [Val vCC] => Some (Val (csetsel_eval TClo v1 v2 Vundef Vundef vCC Vundef is_set)) + | TCmi, [Val vCN] => Some (Val (csetsel_eval TCmi v1 v2 vCN Vundef Vundef Vundef is_set)) + | TCpl, [Val vCN] => Some (Val (csetsel_eval TCpl v1 v2 vCN Vundef Vundef Vundef is_set)) + | TChi, [Val vCZ; Val vCC] => Some (Val (csetsel_eval TChi v1 v2 Vundef vCZ vCC Vundef is_set)) + | TCls, [Val vCZ; Val vCC] => Some (Val (csetsel_eval TCls v1 v2 Vundef vCZ vCC Vundef is_set)) + | TCge, [Val vCN; Val vCV] => Some (Val (csetsel_eval TCge v1 v2 vCN Vundef Vundef vCV is_set)) + | TClt, [Val vCN; Val vCV] => Some (Val (csetsel_eval TClt v1 v2 vCN Vundef Vundef vCV is_set)) + | TCgt, [Val vCN; Val vCZ; Val vCV] => Some (Val (csetsel_eval TCgt v1 v2 vCN vCZ Vundef vCV is_set)) + | TCle, [Val vCN; Val vCZ; Val vCV] => Some (Val (csetsel_eval TCle v1 v2 vCN vCZ Vundef vCV is_set)) + | _, _ => None + end. + Definition arith_op_eval (op: arith_op) (l: list value) := match op, l with | OArithP n, [] => Some (Val (arith_eval_p Ge.(_lk) n)) @@ -297,10 +313,10 @@ Definition arith_op_eval (op: arith_op) (l: list value) := | OArithComparisonP_CZ n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CZ))) | OArithComparisonP_CC n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CC))) | OArithComparisonP_CV n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CV))) - | Ocset c, [Val vCN; Val vCZ; Val vCC; Val vCV] => Some (Val (cset_eval c vCN vCZ vCC vCV)) + | Ocset c, l => cflags_eval c l Vundef Vundef true | Ofmovi fsz, [Val v] => Some (Val (fmovi_eval fsz v)) | Ofmovi_XZR fsz, [] => Some (Val (fmovi_eval_xzr fsz)) - | Ocsel c, [Val v1; Val v2; Val vCN; Val vCZ; Val vCC; Val vCV] => Some (Val (csel_eval c v1 v2 vCN vCZ vCC vCV)) + | Ocsel c, Val v1 :: Val v2 :: l' => cflags_eval c l' v1 v2 false | Ofnmul fsz, [Val v1; Val v2] => Some (Val (fnmul_eval fsz v1 v2)) | _, _ => None end. @@ -330,6 +346,107 @@ Definition op_eval (op: op) (l:list value) := (*| _, _ => None*) end. +Definition vz_eq (vz1 vz2: val) : ?? bool := + RET (match vz1 with + | Vint i1 => match vz2 with + | Vint i2 => Int.eq i1 i2 + | _ => false + end + | Vlong l1 => match vz2 with + | Vlong l2 => Int64.eq l1 l2 + | _ => false + end + | _ => false + end). + +Lemma vz_eq_correct vz1 vz2: + WHEN vz_eq vz1 vz2 ~> b THEN b = true -> vz1 = vz2. +Proof. + wlp_simplify. + destruct vz1; destruct vz2; trivial; try discriminate. + - eapply f_equal; apply Int.same_if_eq; auto. + - eapply f_equal. apply Int64.same_if_eq; auto. +Qed. +Hint Resolve vz_eq_correct: wlp. + +Definition is_eq (is1 is2: isize) : ?? bool := + RET (match is1 with + | W => match is2 with + | W => true + | _ => false + end + | X => match is2 with + | X => true + | _ => false + end + end). + +Lemma is_eq_correct is1 is2: + WHEN is_eq is1 is2 ~> b THEN b = true -> is1 = is2. +Proof. + wlp_simplify; destruct is1; destruct is2; trivial; try discriminate. +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 => @@ -341,15 +458,15 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool := | OArithRR0R n1 => match o2 with OArithRR0R n2 => phys_eq n1 n2 | _ => RET false end | OArithRR0R_XZR n1 vz1 => - match o2 with OArithRR0R_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end + match o2 with OArithRR0R_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end | OArithRR0 n1 => match o2 with OArithRR0 n2 => phys_eq n1 n2 | _ => RET false end | OArithRR0_XZR n1 vz1 => - match o2 with OArithRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end + match o2 with OArithRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end | OArithARRRR0 n1 => match o2 with OArithARRRR0 n2 => phys_eq n1 n2 | _ => RET false end | OArithARRRR0_XZR n1 vz1 => - match o2 with OArithARRRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (phys_eq vz1 vz2) | _ => RET false end + match o2 with OArithARRRR0_XZR n2 vz2 => iandb (phys_eq n1 n2) (vz_eq vz1 vz2) | _ => RET false end | OArithComparisonPP_CN n1 => match o2 with OArithComparisonPP_CN n2 => phys_eq n1 n2 | _ => RET false end | OArithComparisonPP_CZ n1 => @@ -359,21 +476,21 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool := | OArithComparisonPP_CV n1 => match o2 with OArithComparisonPP_CV n2 => phys_eq n1 n2 | _ => RET false end | OArithComparisonR0R_CN n1 is1 => - match o2 with OArithComparisonR0R_CN n2 is2 => iandb (phys_eq n1 n2) (phys_eq is1 is2) | _ => RET false end + match o2 with OArithComparisonR0R_CN n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end | OArithComparisonR0R_CZ n1 is1 => - match o2 with OArithComparisonR0R_CZ n2 is2 => iandb (phys_eq n1 n2) (phys_eq is1 is2) | _ => RET false end + match o2 with OArithComparisonR0R_CZ n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end | OArithComparisonR0R_CC n1 is1 => - match o2 with OArithComparisonR0R_CC n2 is2 => iandb (phys_eq n1 n2) (phys_eq is1 is2) | _ => RET false end + match o2 with OArithComparisonR0R_CC n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end | OArithComparisonR0R_CV n1 is1 => - match o2 with OArithComparisonR0R_CV n2 is2 => iandb (phys_eq n1 n2) (phys_eq is1 is2) | _ => RET false end + match o2 with OArithComparisonR0R_CV n2 is2 => iandb (phys_eq n1 n2) (is_eq is1 is2) | _ => RET false end | OArithComparisonR0R_CN_XZR n1 is1 vz1 => - match o2 with OArithComparisonR0R_CN_XZR n2 is2 vz2 => iandb (phys_eq vz1 vz2) (iandb (phys_eq n1 n2) (phys_eq is1 is2)) | _ => RET false end + match o2 with OArithComparisonR0R_CN_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end | OArithComparisonR0R_CZ_XZR n1 is1 vz1 => - match o2 with OArithComparisonR0R_CZ_XZR n2 is2 vz2 => iandb (phys_eq vz1 vz2) (iandb (phys_eq n1 n2) (phys_eq is1 is2)) | _ => RET false end + match o2 with OArithComparisonR0R_CZ_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end | OArithComparisonR0R_CC_XZR n1 is1 vz1 => - match o2 with OArithComparisonR0R_CC_XZR n2 is2 vz2 => iandb (phys_eq vz1 vz2) (iandb (phys_eq n1 n2) (phys_eq is1 is2)) | _ => RET false end + match o2 with OArithComparisonR0R_CC_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end | OArithComparisonR0R_CV_XZR n1 is1 vz1 => - match o2 with OArithComparisonR0R_CV_XZR n2 is2 vz2 => iandb (phys_eq vz1 vz2) (iandb (phys_eq n1 n2) (phys_eq is1 is2)) | _ => RET false end + match o2 with OArithComparisonR0R_CV_XZR n2 is2 vz2 => iandb (vz_eq vz1 vz2) (iandb (phys_eq n1 n2) (is_eq is1 is2)) | _ => RET false end | OArithComparisonP_CN n1 => match o2 with OArithComparisonP_CN n2 => phys_eq n1 n2 | _ => RET false end | OArithComparisonP_CZ n1 => @@ -383,13 +500,13 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool := | OArithComparisonP_CV n1 => match o2 with OArithComparisonP_CV n2 => phys_eq n1 n2 | _ => RET false end | Ocset c1 => - match o2 with Ocset c2 => phys_eq c1 c2 | _ => RET false end + match o2 with Ocset c2 => struct_eq c1 c2 | _ => RET false end | Ofmovi fsz1 => match o2 with Ofmovi fsz2 => phys_eq fsz1 fsz2 | _ => RET false end | Ofmovi_XZR fsz1 => match o2 with Ofmovi_XZR fsz2 => phys_eq fsz1 fsz2 | _ => RET false end | Ocsel c1 => - match o2 with Ocsel c2 => phys_eq c1 c2 | _ => RET false end + match o2 with Ocsel c2 => struct_eq c1 c2 | _ => RET false end | Ofnmul fsz1 => match o2 with Ofnmul fsz2 => phys_eq fsz1 fsz2 | _ => RET false end end. @@ -399,7 +516,10 @@ Ltac my_wlp_simplify := wlp_xsimplify ltac:(intros; subst; simpl in * |- *; cong Lemma arith_op_eq_correct o1 o2: WHEN arith_op_eq o1 o2 ~> b THEN b = true -> o1 = o2. Proof. - destruct o1, o2; my_wlp_simplify; try congruence. + destruct o1, o2; my_wlp_simplify; try congruence; + try (destruct vz; destruct vz0); try (destruct is; destruct is0); + repeat apply f_equal; try congruence; + try apply Int.same_if_eq; try apply Int64.same_if_eq; try auto. Qed. Hint Resolve arith_op_eq_correct: wlp. Opaque arith_op_eq_correct. @@ -621,6 +741,22 @@ Definition trans_exit (ex: option control) : L.inst := end . +Definition get_testcond_rlocs (c: testcond) := + match c with + | TCeq => (PReg(#CZ) @ Enil) + | TCne => (PReg(#CZ) @ Enil) + | TChs => (PReg(#CC) @ Enil) + | TClo => (PReg(#CC) @ Enil) + | TCmi => (PReg(#CN) @ Enil) + | TCpl => (PReg(#CN) @ Enil) + | TChi => (PReg(#CZ) @ PReg(#CC) @ Enil) + | TCls => (PReg(#CZ) @ PReg(#CC) @ Enil) + | TCge => (PReg(#CN) @ PReg(#CV) @ Enil) + | TClt => (PReg(#CN) @ PReg(#CV) @ Enil) + | TCgt => (PReg(#CN) @ PReg(#CZ) @ PReg(#CV) @ Enil) + | TCle => (PReg(#CN) @ PReg(#CZ) @ PReg(#CV) @ Enil) + end. + Definition trans_arith (ai: ar_instruction) : inst := match ai with | PArithP n rd => [(#rd, Op(Arith (OArithP n)) Enil)] @@ -670,14 +806,18 @@ Definition trans_arith (ai: ar_instruction) : inst := (#CZ, Op(Arith (OArithComparisonP_CZ n)) (PReg(#r1) @ Enil)); (#CC, Op(Arith (OArithComparisonP_CC n)) (PReg(#r1) @ Enil)); (#CV, Op(Arith (OArithComparisonP_CV n)) (PReg(#r1) @ Enil))] - | Pcset rd c => [(#rd, Op(Arith (Ocset c)) (PReg(#CN) @ PReg(#CZ) @ PReg(#CC) @ PReg(#CV) @ Enil))] + | Pcset rd c => + let lr := get_testcond_rlocs c in + [(#rd, Op(Arith (Ocset c)) lr)] | Pfmovi fsz rd r1 => let lr := match r1 with | RR0 r1' => Op(Arith (Ofmovi fsz)) (PReg(#r1') @ Enil) | XZR => Op(Arith (Ofmovi_XZR fsz)) Enil end in [(#rd, lr)] - | Pcsel rd r1 r2 c => [(#rd, Op(Arith (Ocsel c)) (PReg(#r1) @ PReg(#r2) @ PReg(#CN) @ PReg(#CZ) @ PReg(#CC) @ PReg(#CV) @ Enil))] + | Pcsel rd r1 r2 c => + let lr := get_testcond_rlocs c in + [(#rd, Op(Arith (Ocsel c)) (PReg(#r1) @ PReg (#r2) @ lr))] | Pfnmul fsz rd r1 r2 => [(#rd, Op(Arith (Ofnmul fsz)) (PReg(#r1) @ PReg(#r2) @ Enil))] end. @@ -909,21 +1049,6 @@ Proof. + simpl; try rewrite <- HEQV; unfold ppos; try congruence. Qed. -(*Lemma sr_cn_update_both: forall sr rsr rr v*) - (*(HEQV: forall r : preg, sr (# r) = Val (rsr r)),*) - (*(sr <[ #CN <- Val (v) ]>) (#rr) =*) - (*Val (rsr # CN <- v rr).*) -(*Proof.*) - (*intros. unfold assign.*) - (*destruct (PregEq.eq CN rr); subst.*) - (*- rewrite Pregmap.gss. simpl. reflexivity.*) - (*- rewrite Pregmap.gso; eauto.*) - (*destruct rr; try congruence.*) - (*+ destruct d as [i|f]; try destruct i as [ir|]; try destruct f; try destruct ir; try rewrite HEQV; simpl; try congruence.*) - (*+ destruct c; simpl; try rewrite <- HEQV; unfold ppos; try congruence.*) - (*+ simpl; try rewrite <- HEQV; unfold ppos; try congruence.*) -(*Qed.*) - Lemma sr_update_overwrite: forall sr pos v1 v2, (sr <[ pos <- v1 ]>) <[ pos <- v2 ]> = (sr <[ pos <- v2 ]>). Proof. @@ -1194,21 +1319,6 @@ Proof. discriminate_preg_flags ]). Qed. -Lemma if_opt_bool_val_cond: forall sr mr (rd r1 r2: dreg) c rsr rr - (HMEM: sr pmem = Memstate mr) - (HEQV: forall r : preg, sr (# r) = Val (rsr r)), - (sr <[ #rd <- Val - (if_opt_bool_val - (flags_testcond_value c (rsr CN) (rsr CZ) (rsr CC) (rsr CV)) - (rsr r1) (rsr r2)) ]>) (# rr) = - Val (rsr # rd <- (if_opt_bool_val (eval_testcond c rsr) (rsr r1) (rsr r2)) rr). -Proof. - intros. unfold flags_testcond_value, eval_testcond. - destruct c; destruct (rsr _); - try (DIRN1 rd; DPRI rr; SRVUPDATE; - rewrite Pregmap.gso; unfold assign; try destruct (R.eq_dec); sr_val_rwrt; auto; discriminate_ppos). -Qed. - (** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *) (*Module PChk := ParallelChecks L PosPseudoRegSet.*) @@ -1288,7 +1398,8 @@ Proof. try (eapply compare_int_res; eauto); try (eapply compare_float_res; eauto). - (* Pcset *) - simpl; (*DI0N0 rd.*) unfold eval_testcond, cset_eval; destruct c; + simpl; (*DI0N0 rd.*) unfold eval_testcond, get_testcond_rlocs, cflags_eval; + unfold csetsel_eval; unfold flags_testcond_value, list_exp_eval; destruct c; simpl; repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos); destruct (rsr CZ); simpl; (eexists; split; [| split]; [reflexivity | DI0N0 rd; eauto | idtac]); @@ -1297,10 +1408,13 @@ Proof. - (* Pfmovi *) simpl; destruct r1; simpl; destruct fsz; TARITH sr; intros rr; DPRI rr; SRVUPDATE. - (* Pcsel *) - simpl; DIRN1 r1; DIRN1 r2; unfold csel_eval; + simpl. + unfold eval_testcond, cflags_eval. DIRN1 r1; DIRN1 r2; destruct c; simpl; repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos); - (eexists; split; [| split]; [reflexivity | DDRF rd; eauto | idtac]); - intros; erewrite <- if_opt_bool_val_cond; eauto. + (eexists; split; [| split]; [reflexivity | DDRF rd; eauto | idtac]). + all: intros rr; destruct (PregEq.eq rr rd); + [ subst; erewrite Pregmap.gss; erewrite sr_gss; reflexivity | + try erewrite Pregmap.gso; try erewrite assign_diff; try rewrite H0; try fold (ppos rd); try eapply ppos_discr; eauto ]. - (* Pfnmul *) simpl; destruct fsz; TARITH sr; intros rr; DPRI rr; SRVUPDATE. Qed. @@ -2037,7 +2151,7 @@ Definition string_of_name_ArithComparisonP_CZ (n: arith_comparison_p) : pstring end. Definition string_of_name_ArithComparisonP_CC (n: arith_comparison_p) : pstring := -match n with + match n with | Pfcmp0 _ => "ArithComparisonP_CC=>Pfcmp0" | Pcmpimm _ _ => "ArithComparisonP_CC=>Pcmpimm" | Pcmnimm _ _ => "ArithComparisonP_CC=>Pcmnimm" @@ -2045,13 +2159,29 @@ match n with end. Definition string_of_name_ArithComparisonP_CV (n: arith_comparison_p) : pstring := -match n with + match n with | Pfcmp0 _ => "ArithComparisonP_CV=>Pfcmp0" | Pcmpimm _ _ => "ArithComparisonP_CV=>Pcmpimm" | Pcmnimm _ _ => "ArithComparisonP_CV=>Pcmnimm" | Ptstimm _ _ => "ArithComparisonP_CV=>Ptstimm" end. +Definition string_of_name_cset (c: testcond) : pstring := + match c with + | TCeq => "Cset=>TCeq" + | TCne => "Cset=>TCne" + | TChs => "Cset=>TChs" + | TClo => "Cset=>TClo" + | TCmi => "Cset=>TCmi" + | TCpl => "Cset=>TCpl" + | TChi => "Cset=>TChi" + | TCls => "Cset=>TCls" + | TCge => "Cset=>TCge" + | TClt => "Cset=>TClt" + | TCgt => "Cset=>TCgt" + | TCle => "Cset=>TCle" + end. + Definition string_of_arith (op: arith_op): pstring := match op with | OArithP n => string_of_name_ArithP n @@ -2079,7 +2209,7 @@ Definition string_of_arith (op: arith_op): pstring := | OArithComparisonP_CZ n => string_of_name_ArithComparisonP_CZ n | OArithComparisonP_CC n => string_of_name_ArithComparisonP_CC n | OArithComparisonP_CV n => string_of_name_ArithComparisonP_CV n - | Ocset _ => "Ocset" + | Ocset c => string_of_name_cset c | Ofmovi _ => "Ofmovi" | Ofmovi_XZR _ => "Ofmovi_XZR" | Ocsel _ => "Ocsel" diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml index 831080d5..7c8bd144 100644 --- a/aarch64/PostpassSchedulingOracle.ml +++ b/aarch64/PostpassSchedulingOracle.ml @@ -212,6 +212,14 @@ let reg_of_ireg0 r = let reg_of_freg r = Reg (Asm.DR (Asm.FR r)) +let flags_wlocs = + [ + Reg (Asm.CR Asm.CN); + Reg (Asm.CR Asm.CZ); + Reg (Asm.CR Asm.CC); + Reg (Asm.CR Asm.CV); + ] + let arith_p_rec i rd = { inst = arith_p_real i; @@ -266,7 +274,7 @@ let arith_arrrr0_rec i rd r1 r2 r3 = let arith_comparison_pp_rec i r1 r2 = { inst = arith_comparison_pp_real i; - write_locs = []; + write_locs = flags_wlocs; read_locs = [ r1; r2 ]; is_control = false; } @@ -275,7 +283,7 @@ let arith_comparison_r0r_rec i r1 r2 = let rlocs = if is_XZR r1 then [ r2 ] else [ r1; r2 ] in { inst = arith_comparison_r0r_real i; - write_locs = []; + write_locs = flags_wlocs; read_locs = rlocs; is_control = false; } @@ -283,7 +291,7 @@ let arith_comparison_r0r_rec i r1 r2 = let arith_comparison_p_rec i r1 = { inst = arith_comparison_p_real i; - write_locs = []; + write_locs = flags_wlocs; read_locs = [ r1 ]; is_control = false; } @@ -331,14 +339,36 @@ let cvtuw2x_rec rd r1 = let cvtx2w_rec rd = { inst = cvtx2w_real; write_locs = []; read_locs = []; is_control = false } +let get_testcond_rlocs c = + match c with + | Asm.TCeq -> [ Reg (Asm.CR Asm.CZ) ] + | Asm.TCne -> [ Reg (Asm.CR Asm.CZ) ] + | Asm.TChs -> [ Reg (Asm.CR Asm.CC) ] + | Asm.TClo -> [ Reg (Asm.CR Asm.CC) ] + | Asm.TCmi -> [ Reg (Asm.CR Asm.CN) ] + | Asm.TCpl -> [ Reg (Asm.CR Asm.CN) ] + | Asm.TChi -> [ Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CC) ] + | Asm.TCls -> [ Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CC) ] + | Asm.TCge -> [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CV) ] + | Asm.TClt -> [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CV) ] + | Asm.TCgt -> + [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CV) ] + | Asm.TCle -> + [ Reg (Asm.CR Asm.CN); Reg (Asm.CR Asm.CZ); Reg (Asm.CR Asm.CV) ] + let cset_rec rd c = - { inst = cset_real; write_locs = [ rd ]; read_locs = []; is_control = false } + { + inst = cset_real; + write_locs = [ rd ]; + read_locs = get_testcond_rlocs c; + is_control = false; + } let csel_rec rd r1 r2 c = { inst = csel_real; write_locs = [ rd ]; - read_locs = [ r1; r2 ]; + read_locs = [ r1; r2 ] @ get_testcond_rlocs c; is_control = false; } @@ -891,7 +921,7 @@ let smart_schedule bb = let bblock_schedule bb = let identity_mode = not !Clflags.option_fpostpass in - if (debug && not identity_mode) then ( + if debug && not identity_mode then ( Printf.eprintf "###############################\n"; Printf.eprintf "SCHEDULING\n" ); if identity_mode then pack_result bb else smart_schedule bb |