From ea3f2755c1c1a733c2a5886d8b82afce6fdcad03 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 11 Nov 2020 22:04:34 +0100 Subject: Finishing PArith cases in abb, and linking the pass to compile --- aarch64/Asmblockdeps.v | 866 +++++++++++++++++++++++++++---------------------- 1 file changed, 479 insertions(+), 387 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index 29d91d1c..e1a49a55 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -90,7 +90,6 @@ Inductive arith_op := | OArithComparisonPP_CZ (n: arith_comparison_pp) | OArithComparisonPP_CC (n: arith_comparison_pp) | OArithComparisonPP_CV (n: arith_comparison_pp) - | OArithComparisonR0R (n: arith_comparison_r0r) | OArithComparisonR0R_CN (n: arith_comparison_r0r) (is: isize) | OArithComparisonR0R_CZ (n: arith_comparison_r0r) (is: isize) | OArithComparisonR0R_CC (n: arith_comparison_r0r) (is: isize) @@ -99,7 +98,15 @@ Inductive arith_op := | OArithComparisonR0R_CZ_XZR (n: arith_comparison_r0r) (is: isize) (vz: val) | OArithComparisonR0R_CC_XZR (n: arith_comparison_r0r) (is: isize) (vz: val) | OArithComparisonR0R_CV_XZR (n: arith_comparison_r0r) (is: isize) (vz: val) - | OArithComparisonP (n: arith_comparison_p) + | OArithComparisonP_CN (n: arith_comparison_p) + | OArithComparisonP_CZ (n: arith_comparison_p) + | OArithComparisonP_CC (n: arith_comparison_p) + | OArithComparisonP_CV (n: arith_comparison_p) + | Ocset (c: testcond) + | Ofmovi (fsz: fsize) + | Ofmovi_XZR (fsz: fsize) + | Ocsel (c: testcond) + | Ofnmul (fsz: fsize) . Inductive op_wrap := @@ -108,6 +115,8 @@ Inductive op_wrap := | Control (co: control_op) . +Coercion Arith: arith_op >-> op_wrap. + Definition v_compare_int (v1 v2: val) : CRflags := {| _CN := (Val.negative (Val.sub v1 v2)); _CZ := (Val_cmpu Ceq v1 v2); @@ -156,10 +165,109 @@ Definition arith_eval_comparison_pp (n: arith_comparison_pp) (v1 v2: val) := | Pfcmp D => v_compare_float v1' v2' end. +Definition arith_eval_comparison_p (n: arith_comparison_p) (v: val) := + let (v1',v2') := arith_prepare_comparison_p n v in + match n with + | Pcmpimm W _ | Pcmnimm W _ | Ptstimm W _ => v_compare_int v1' v2' + | Pcmpimm X _ | Pcmnimm X _ | Ptstimm X _ => v_compare_long v1' v2' + | Pfcmp0 S => v_compare_single v1' v2' + | Pfcmp0 D => v_compare_float v1' v2' + end. + Definition arith_eval_comparison_r0r (n: arith_comparison_r0r) (v1 v2: val) (is: isize) := let (v1',v2') := arith_prepare_comparison_r0r n v1 v2 in if is then v_compare_int v1' v2' else v_compare_long v1' v2'. +Definition flags_testcond_value (c: testcond) (vCN vCZ vCC vCV: val) := + match c with + | TCeq => (**r equal *) + match vCZ with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + | TCne => (**r not equal *) + match vCZ with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TClo => (**r unsigned less than *) + match vCC with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TCls => (**r unsigned less or equal *) + match vCC, vCZ with + | Vint c, Vint z => Some (Int.eq c Int.zero || Int.eq z Int.one) + | _, _ => None + end + | TChs => (**r unsigned greater or equal *) + match vCC with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + | TChi => (**r unsigned greater *) + match vCC, vCZ with + | Vint c, Vint z => Some (Int.eq c Int.one && Int.eq z Int.zero) + | _, _ => None + end + | TClt => (**r signed less than *) + match vCV, vCN with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.one) + | _, _ => None + end + | TCle => (**r signed less or equal *) + match vCV, vCN, vCZ with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.one || Int.eq z Int.one) + | _, _, _ => None + end + | TCge => (**r signed greater or equal *) + match vCV, vCN with + | Vint o, Vint s => Some (Int.eq (Int.xor o s) Int.zero) + | _, _ => None + end + | TCgt => (**r signed greater *) + match vCV, vCN, vCZ with + | Vint o, Vint s, Vint z => Some (Int.eq (Int.xor o s) Int.zero && Int.eq z Int.zero) + | _, _, _ => None + end + | TCpl => (**r positive *) + match vCN with + | Vint n => Some (Int.eq n Int.zero) + | _ => None + end + | TCmi => (**r negative *) + match vCN with + | Vint n => Some (Int.eq n Int.one) + | _ => None + end + end. + +Definition cset_eval (c: testcond) (vCN vCZ vCC vCV: val) := + 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). + +Definition fmovi_eval (fsz: fsize) (v: val) := + match fsz with + | S => float32_of_bits v + | D => float64_of_bits v + end. + +Definition fmovi_eval_xzr (fsz: fsize) := + match fsz with + | S => float32_of_bits (Vint Int.zero) + | D => float64_of_bits (Vlong Int64.zero) + end. + +Definition fnmul_eval (fsz: fsize) (v1 v2: val) := + match fsz with + | S => Val.negfs (Val.mulfs v1 v2) + | D => Val.negf (Val.mulf v1 v2) + end. + Definition op:=op_wrap. Definition arith_op_eval (op: arith_op) (l: list value) := @@ -185,6 +293,15 @@ Definition arith_op_eval (op: arith_op) (l: list value) := | OArithComparisonR0R_CZ_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CZ))) | OArithComparisonR0R_CC_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CC))) | OArithComparisonR0R_CV_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CV))) + | OArithComparisonP_CN n, [Val v] => Some (Val ((arith_eval_comparison_p n v).(_CN))) + | 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)) + | 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)) + | Ofnmul fsz, [Val v1; Val v2] => Some (Val (fnmul_eval fsz v1 v2)) | _, _ => None end. @@ -257,31 +374,24 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool := 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 | 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 - (*| OArithRR n1 => *) - (*match o2 with OArithRR n2 => phys_eq n1 n2 | _ => RET false end*) - (*| OArithRI32 n1 i1 =>*) - (*match o2 with OArithRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*) - (*| OArithRI64 n1 i1 =>*) - (*match o2 with OArithRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*) - (*| OArithRF32 n1 i1 =>*) - (*match o2 with OArithRF32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*) - (*| OArithRF64 n1 i1 =>*) - (*match o2 with OArithRF64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*) - (*| OArithRRR n1 =>*) - (*match o2 with OArithRRR n2 => phys_eq n1 n2 | _ => RET false end*) - (*| OArithRRI32 n1 i1 =>*) - (*match o2 with OArithRRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*) - (*| OArithRRI64 n1 i1 =>*) - (*match o2 with OArithRRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*) - (*| OArithARRR n1 =>*) - (*match o2 with OArithARRR n2 => phys_eq n1 n2 | _ => RET false end*) - (*| OArithARR n1 =>*) - (*match o2 with OArithARR n2 => phys_eq n1 n2 | _ => RET false end*) - (*| OArithARRI32 n1 i1 =>*) - (*match o2 with OArithARRI32 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*) - (*| OArithARRI64 n1 i1 =>*) - (*match o2 with OArithARRI64 n2 i2 => iandb (phys_eq n1 n2) (phys_eq i1 i2) | _ => RET false end*) - | _ => RET false + | OArithComparisonP_CN n1 => + match o2 with OArithComparisonP_CN n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonP_CZ n1 => + match o2 with OArithComparisonP_CZ n2 => phys_eq n1 n2 | _ => RET false end + | OArithComparisonP_CC n1 => + match o2 with OArithComparisonP_CC n2 => phys_eq n1 n2 | _ => RET false end + | 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 + | 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 + | Ofnmul fsz1 => + match o2 with Ofnmul fsz2 => phys_eq fsz1 fsz2 | _ => RET false end end. Ltac my_wlp_simplify := wlp_xsimplify ltac:(intros; subst; simpl in * |- *; congruence || intuition eauto with wlp). @@ -555,17 +665,22 @@ Definition trans_arith (ai: ar_instruction) : inst := (#CC, Op(Arith (OArithComparisonR0R_CC_XZR n is vz)) (PReg(#r2) @ Enil)); (#CV, Op(Arith (OArithComparisonR0R_CV_XZR n is vz)) (PReg(#r2) @ Enil))] end - | _ => [] - (*| PArithR n d => [(#d, Op (Arith (OArithR n)) Enil)]*) - (*| PArithRR n d s => [(#d, Op (Arith (OArithRR n)) (PReg(#s) @ Enil))]*) - (*| PArithRI32 n d i => [(#d, Op (Arith (OArithRI32 n i)) Enil)]*) - (*| PArithRI64 n d i => [(#d, Op (Arith (OArithRI64 n i)) Enil)]*) - (*| PArithRF32 n d i => [(#d, Op (Arith (OArithRF32 n i)) Enil)]*) - (*| PArithRF64 n d i => [(#d, Op (Arith (OArithRF64 n i)) Enil)]*) - (*| PArithRRR n d s1 s2 => [(#d, Op (Arith (OArithRRR n)) (PReg(#s1) @ PReg(#s2) @ Enil))]*) + | PArithComparisonP n r1 => + [(#CN, Op(Arith (OArithComparisonP_CN n)) (PReg(#r1) @ Enil)); + (#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))] + | 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))] + | Pfnmul fsz rd r1 r2 => [(#rd, Op(Arith (Ofnmul fsz)) (PReg(#r1) @ PReg(#r2) @ Enil))] end. - Definition trans_basic (b: basic) : inst := match b with | PArith ai => trans_arith ai @@ -892,16 +1007,16 @@ Ltac discriminate_ppos := try apply freg_not_CV; try(simpl; discriminate). -Ltac replace_regs_pos := - try replace (7) with (ppos XSP) by eauto; - try replace (2) with (ppos CN) by eauto; - try replace (3) with (ppos CZ) by eauto; - try replace (4) with (ppos CC) by eauto; - try replace (5) with (ppos CV) by eauto. +Ltac replace_regs_pos sr := + try replace (sr 7) with (sr (ppos XSP)) by eauto; + try replace (sr 2) with (sr (ppos CN)) by eauto; + try replace (sr 3) with (sr (ppos CZ)) by eauto; + try replace (sr 4) with (sr (ppos CC)) by eauto; + try replace (sr 5) with (sr (ppos CV)) by eauto. -Ltac TARITH := +Ltac TARITH sr := replace_ppos; - replace_regs_pos; + replace_regs_pos sr; try sr_val_rwrt; try (eexists; split; [| split]); eauto; try (sr_memstate_rwrt; rewrite assign_diff; @@ -1079,6 +1194,21 @@ 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.*) @@ -1110,28 +1240,28 @@ Proof. induction i. all: intros MS EARITH; subst; inv MS; unfold exec_arith_instr. - (* PArithP *) - DIRN1 rd; TARITH; intros rr; DPRF rr; SRVUPDATE. + DIRN1 rd; TARITH sr; intros rr; DPRF rr; SRVUPDATE. - (* PArithPP *) - DIRN1 rs; DIRN1 rd; TARITH; + DIRN1 rs; DIRN1 rd; TARITH sr; intros rr; DPRI rr; SRVUPDATE. - (* PArithPPP *) - DIRN1 r1; DIRN1 r2; DIRN1 rd; TARITH; + DIRN1 r1; DIRN1 r2; DIRN1 rd; TARITH sr; intros rr; DPRI rr; SRVUPDATE. - (* PArithRR0R *) simpl. destruct r1. - + (* OArithRR0R *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE. - + (* OArithRR0R_XZR *) simpl; destruct (arith_rr0r_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE. + + (* OArithRR0R *) simpl; TARITH sr; intros rr; DPRI rr; SRVUPDATE. + + (* OArithRR0R_XZR *) simpl; destruct (arith_rr0r_isize _); TARITH sr; intros rr; DPRI rr; SRVUPDATE. - (* PArithRR0 *) simpl. destruct r1. - + (* OArithRR0 *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE. - + (* OArithRR0_XZR *) simpl; destruct (arith_rr0_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE. + + (* OArithRR0 *) simpl; TARITH sr; intros rr; DPRI rr; SRVUPDATE. + + (* OArithRR0_XZR *) simpl; destruct (arith_rr0_isize _); TARITH sr; intros rr; DPRI rr; SRVUPDATE. - (* PArithARRRR0 *) simpl. destruct r3. - + (* OArithARRRR0 *) simpl; TARITH; intros rr; DPRI rr; SRVUPDATE. - + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); TARITH; intros rr; DPRI rr; SRVUPDATE. + + (* OArithARRRR0 *) simpl; TARITH sr; intros rr; DPRI rr; SRVUPDATE. + + (* OArithARRRR0_XZR *) simpl; destruct (arith_arrrr0_isize _); TARITH sr; intros rr; DPRI rr; SRVUPDATE. - (* PArithComparisonPP *) DIRN1 r2; DIRN1 r1; destruct i; - repeat (replace_ppos; replace_regs_pos; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos); + repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos); (eexists; split; [| split]; [reflexivity | eauto | idtac]); unfold arith_eval_comparison_pp; destruct arith_prepare_comparison_pp; simpl; intros rr; try destruct sz; @@ -1141,95 +1271,39 @@ Proof. - (* PArithComparisonR0R *) simpl. destruct r1; ( simpl; destruct i; - repeat (replace_ppos; replace_regs_pos; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos); + repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos); (eexists; split; [| split]; [reflexivity | eauto | idtac]); unfold arith_eval_comparison_r0r, arith_comparison_r0r_isize; destruct arith_prepare_comparison_r0r; destruct is; simpl; intros rr; try destruct sz; try (eapply compare_long_res; eauto); try (eapply compare_int_res; eauto)). - - - all:admit. - - (* -(* Ploadsymbol *) - - destruct i. eexists; split; [| split]. - * simpl. reflexivity. - * Simpl. - * simpl. intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithRR *) - - eexists; split; [| split]. - * simpl. rewrite (H0 rs). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithRI32 *) - - eexists; split; [|split]. - * simpl. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithRI64 *) - - eexists; split; [|split]. - * simpl. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithRF32 *) - - eexists; split; [|split]. - * simpl. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithRF64 *) - - eexists; split; [|split]. - * simpl. reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithRRR *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rs1). rewrite (H0 rs2). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithRRI32 *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rs). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithRRI64 *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rs). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithARRR *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rd). rewrite (H0 rs1). rewrite (H0 rs2). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithARR *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithARRI32 *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl. -(* PArithARRI64 *) - - eexists; split; [|split]. - * simpl. rewrite (H0 rd). rewrite (H0 rs). reflexivity. - * Simpl. - * intros rr; destruct rr; Simpl. - destruct (ireg_eq g rd); subst; Simpl.*) -Admitted. + - (* PArithComparisonP *) + DIRN1 r1; destruct i; + repeat (replace_ppos; replace_regs_pos sr; sr_val_rwrt; try rewrite !assign_diff; discriminate_ppos); + (eexists; split; [| split]; [reflexivity | eauto | idtac]); + unfold arith_eval_comparison_p; destruct arith_prepare_comparison_p; + simpl; intros rr; try destruct sz; + try (eapply compare_single_res; eauto); + try (eapply compare_long_res; eauto); + try (eapply compare_int_res; eauto); + try (eapply compare_float_res; eauto). + - (* Pcset *) + simpl; (*DI0N0 rd.*) unfold eval_testcond, cset_eval; destruct c; + 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]); + intros rr; DPRI rr; SRVUPDATE; + rewrite Pregmap.gso; unfold assign; try destruct (R.eq_dec); sr_val_rwrt; auto; discriminate_ppos. + - (* Pfmovi *) + simpl; destruct r1; simpl; destruct fsz; TARITH sr; intros rr; DPRI rr; SRVUPDATE. + - (* Pcsel *) + simpl; DIRN1 r1; DIRN1 r2; unfold csel_eval; + 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. + - (* Pfnmul *) + simpl; destruct fsz; TARITH sr; intros rr; DPRI rr; SRVUPDATE. +Qed. Theorem bisimu_basic rsr mr sr bi: match_states (State rsr mr) sr -> @@ -1723,322 +1797,339 @@ Admitted. (** Used for debug traces *) -(* -Definition gpreg_name (gpr: gpreg) := - match gpr with - | GPR0 => Str ("GPR0") | GPR1 => Str ("GPR1") | GPR2 => Str ("GPR2") | GPR3 => Str ("GPR3") | GPR4 => Str ("GPR4") - | GPR5 => Str ("GPR5") | GPR6 => Str ("GPR6") | GPR7 => Str ("GPR7") | GPR8 => Str ("GPR8") | GPR9 => Str ("GPR9") - | GPR10 => Str ("GPR10") | GPR11 => Str ("GPR11") | GPR12 => Str ("GPR12") | GPR13 => Str ("GPR13") | GPR14 => Str ("GPR14") - | GPR15 => Str ("GPR15") | GPR16 => Str ("GPR16") | GPR17 => Str ("GPR17") | GPR18 => Str ("GPR18") | GPR19 => Str ("GPR19") - | GPR20 => Str ("GPR20") | GPR21 => Str ("GPR21") | GPR22 => Str ("GPR22") | GPR23 => Str ("GPR23") | GPR24 => Str ("GPR24") - | GPR25 => Str ("GPR25") | GPR26 => Str ("GPR26") | GPR27 => Str ("GPR27") | GPR28 => Str ("GPR28") | GPR29 => Str ("GPR29") - | GPR30 => Str ("GPR30") | GPR31 => Str ("GPR31") | GPR32 => Str ("GPR32") | GPR33 => Str ("GPR33") | GPR34 => Str ("GPR34") - | GPR35 => Str ("GPR35") | GPR36 => Str ("GPR36") | GPR37 => Str ("GPR37") | GPR38 => Str ("GPR38") | GPR39 => Str ("GPR39") - | GPR40 => Str ("GPR40") | GPR41 => Str ("GPR41") | GPR42 => Str ("GPR42") | GPR43 => Str ("GPR43") | GPR44 => Str ("GPR44") - | GPR45 => Str ("GPR45") | GPR46 => Str ("GPR46") | GPR47 => Str ("GPR47") | GPR48 => Str ("GPR48") | GPR49 => Str ("GPR49") - | GPR50 => Str ("GPR50") | GPR51 => Str ("GPR51") | GPR52 => Str ("GPR52") | GPR53 => Str ("GPR53") | GPR54 => Str ("GPR54") - | GPR55 => Str ("GPR55") | GPR56 => Str ("GPR56") | GPR57 => Str ("GPR57") | GPR58 => Str ("GPR58") | GPR59 => Str ("GPR59") - | GPR60 => Str ("GPR60") | GPR61 => Str ("GPR61") | GPR62 => Str ("GPR62") | GPR63 => Str ("GPR63") - end. +Definition ireg_name (ir: ireg) : pstring := + match ir with + | X0 => Str ("X0") | X1 => Str ("X1") | X2 => Str ("X2") | X3 => Str ("X3") | X4 => Str ("X4") | X5 => Str ("X5") | X6 => Str ("X6") | X7 => Str ("X7") + | X8 => Str ("X8") | X9 => Str ("X9") | X10 => Str ("X10") | X11 => Str ("X11") | X12 => Str ("X12") | X13 => Str ("X13") | X14 => Str ("X14") | X15 => Str ("X15") + | X16 => Str ("X16") | X17 => Str ("X17") | X18 => Str ("X18") | X19 => Str ("X19") | X20 => Str ("X20") | X21 => Str ("X21") | X22 => Str ("X22") | X23 => Str ("X23") + | X24 => Str ("X24") | X25 => Str ("X25") | X26 => Str ("X26") | X27 => Str ("X27") | X28 => Str ("X28") | X29 => Str ("X29") | X30 => Str ("X30") + end +. + +Definition freg_name (fr: freg) : pstring := + match fr with + | D0 => Str ("D0") | D1 => Str ("D1") | D2 => Str ("D2") | D3 => Str ("D3") | D4 => Str ("D4") | D5 => Str ("D5") | D6 => Str ("D6") | D7 => Str ("D7") + | D8 => Str ("D8") | D9 => Str ("D9") | D10 => Str ("D10") | D11 => Str ("D11") | D12 => Str ("D12") | D13 => Str ("D13") | D14 => Str ("D14") | D15 => Str ("D15") + | D16 => Str ("D16") | D17 => Str ("D17") | D18 => Str ("D18") | D19 => Str ("D19") | D20 => Str ("D20") | D21 => Str ("D21") | D22 => Str ("D22") | D23 => Str ("D23") + | D24 => Str ("D24") | D25 => Str ("D25") | D26 => Str ("D26") | D27 => Str ("D27") | D28 => Str ("D28") | D29 => Str ("D29") | D30 => Str ("D30") | D31 => Str ("D31") + end +. Definition string_of_name (x: P.R.t): ?? pstring := if (Pos.eqb x pmem) then RET (Str "MEM") else match inv_ppos x with - | Some RA => RET (Str ("RA")) - | Some PC => RET (Str ("PC")) - | Some (IR gpr) => RET (gpreg_name gpr) - | _ => RET (Str ("UNDEFINED")) + | Some (CR cr) => match cr with + | CN => RET (Str ("CN")) + | CZ => RET (Str ("CZ")) + | CC => RET (Str ("CC")) + | CV => RET (Str ("CV")) + end + | Some (PC) => RET (Str ("PC")) + | Some (DR dr) => match dr with + | IR ir => match ir with + | XSP => RET (Str ("XSP")) + | RR1 irr => RET (ireg_name irr) + end + | FR fr => RET (freg_name fr) + end + | _ => RET (Str ("UNDEFINED")) end. -Definition string_of_name_r (n: arith_name_r): pstring := +Definition string_of_name_ArithP (n: arith_p) : pstring := match n with - | Ploadsymbol _ _ => "Ploadsymbol" + | Padrp _ _ => "Padrp" + | Pmovz _ _ _ => "Pmov" + | Pmovn _ _ _ => "Pmov" + | Pfmovimms _ => "Pfmovimm" + | Pfmovimmd _ => "Pfmovimm" end. -Definition string_of_name_rr (n: arith_name_rr): pstring := +Definition string_of_name_ArithPP (n: arith_pp) : pstring := match n with - Pmv => "Pmv" - | Pnegw => "Pnegw" - | Pnegl => "Pnegl" - | Pcvtl2w => "Pcvtl2w" - | Psxwd => "Psxwd" - | Pzxwd => "Pzxwd" - | Pextfz _ _ => "Pextfz" - | Pextfs _ _ => "Pextfs" - | Pextfzl _ _ => "Pextfzl" - | Pextfsl _ _ => "Pextfsl" - | Pfabsd => "Pfabsd" - | Pfabsw => "Pfabsw" - | Pfnegd => "Pfnegd" - | Pfnegw => "Pfnegw" - | Pfinvw => "Pfinvw" - | Pfnarrowdw => "Pfnarrowdw" - | Pfwidenlwd => "Pfwidenlwd" - | Pfloatwrnsz => "Pfloatwrnsz" - | Pfloatuwrnsz => "Pfloatuwrnsz" - | Pfloatudrnsz => "Pfloatudrnsz" - | Pfloatdrnsz => "Pfloatdrnsz" - | Pfixedwrzz => "Pfixedwrzz" - | Pfixeduwrzz => "Pfixeduwrzz" - | Pfixeddrzz => "Pfixeddrzz" - | Pfixedudrzz => "Pfixedudrzz" - | Pfixeddrzz_i32 => "Pfixeddrzz_i32" - | Pfixedudrzz_i32 => "Pfixedudrzz_i32" + | Pmov => "Pmov" + | Pmovk _ _ _ => "Pmovk" + | Paddadr _ _ => "Paddadr" + | Psbfiz _ _ _ => "Psbfiz" + | Psbfx _ _ _ => "Psbfx" + | Pubfiz _ _ _ => "Pubfiz" + | Pubfx _ _ _ => "Pubfx" + | Pfmov => "Pfmov" + | Pfcvtds => "Pfcvtds" + | Pfcvtsd => "Pfcvtsd" + | Pfabs _ => "Pfabs" + | Pfneg _ => "Pfneg" + | Pscvtf _ _ => "Pscvtf" + | Pucvtf _ _ => "Pucvtf" + | Pfcvtzs _ _ => "Pfcvtzs" + | Pfcvtzu _ _ => "Pfcvtzu" + | Paddimm _ _ => "Paddimm" + | Psubimm _ _ => "Psubimm" end. -Definition string_of_name_ri32 (n: arith_name_ri32): pstring := +Definition string_of_name_ArithPPP (n: arith_ppp) : pstring := match n with - | Pmake => "Pmake" + | Pasrv _ => "Pasrv" + | Plslv _ => "Plslv" + | Plsrv _ => "Plsrv" + | Prorv _ => "Prorv" + | Psmulh => "Psmulh" + | Pumulh => "Pumulh" + | Psdiv _ => "Psdiv" + | Pudiv _ => "Pudiv" + | Paddext _ => "Paddext" + | Psubext _ => "Psubext" + | Pfadd _ => "Pfadd" + | Pfdiv _ => "Pfdiv" + | Pfmul _ => "Pfmul" + | Pfsub _ => "Pfsub" end. -Definition string_of_name_ri64 (n: arith_name_ri64): pstring := +Definition string_of_name_ArithRR0R (n: arith_rr0r) : pstring := match n with - | Pmakel => "Pmakel" + | Padd _ _ => "ArithRR0R=>Padd" + | Psub _ _ => "ArithRR0R=>Psub" + | Pand _ _ => "ArithRR0R=>Pand" + | Pbic _ _ => "ArithRR0R=>Pbic" + | Peon _ _ => "ArithRR0R=>Peon" + | Peor _ _ => "ArithRR0R=>Peor" + | Porr _ _ => "ArithRR0R=>Porr" + | Porn _ _ => "ArithRR0R=>Porn" end. -Definition string_of_name_rf32 (n: arith_name_rf32): pstring := +Definition string_of_name_ArithRR0R_XZR (n: arith_rr0r) : pstring := match n with - | Pmakefs => "Pmakefs" + | Padd _ _ => "ArithRR0R_XZR=>Padd" + | Psub _ _ => "ArithRR0R_XZR=>Psub" + | Pand _ _ => "ArithRR0R_XZR=>Pand" + | Pbic _ _ => "ArithRR0R_XZR=>Pbic" + | Peon _ _ => "ArithRR0R_XZR=>Peon" + | Peor _ _ => "ArithRR0R_XZR=>Peor" + | Porr _ _ => "ArithRR0R_XZR=>Porr" + | Porn _ _ => "ArithRR0R_XZR=>Porn" end. -Definition string_of_name_rf64 (n: arith_name_rf64): pstring := +Definition string_of_name_ArithRR0 (n: arith_rr0) : pstring := match n with - | Pmakef => "Pmakef" + | Pandimm _ _ => "ArithRR0=>Pandimm" + | Peorimm _ _ => "ArithRR0=>Peorimm" + | Porrimm _ _ => "ArithRR0=>Porrimm" end. -Definition string_of_name_rrr (n: arith_name_rrr): pstring := +Definition string_of_name_ArithRR0_XZR (n: arith_rr0) : pstring := +match n with + | Pandimm _ _ => "ArithRR0_XZR=>Pandimm" + | Peorimm _ _ => "ArithRR0_XZR=>Peorimm" + | Porrimm _ _ => "ArithRR0_XZR=>Porrimm" + end. + +Definition string_of_name_ArithARRRR0 (n: arith_arrrr0) : pstring := match n with - | Pcompw _ => "Pcompw" - | Pcompl _ => "Pcompl" - | Pfcompw _ => "Pfcompw" - | Pfcompl _ => "Pfcompl" - | Paddw => "Paddw" - | Paddxw _ => "Paddxw" - | Psubw => "Psubw" - | Prevsubxw _ => "Prevsubxw" - | Pmulw => "Pmulw" - | Pandw => "Pandw" - | Pnandw => "Pnandw" - | Porw => "Porw" - | Pnorw => "Pnorw" - | Pxorw => "Pxorw" - | Pnxorw => "Pnxorw" - | Pandnw => "Pandnw" - | Pornw => "Pornw" - | Psraw => "Psraw" - | Psrlw => "Psrlw" - | Psrxw => "Psrxw" - | Psllw => "Psllw" - | Paddl => "Paddl" - | Paddxl _ => "Paddxl" - | Psubl => "Psubl" - | Prevsubxl _ => "Prevsubxl" - | Pandl => "Pandl" - | Pnandl => "Pnandl" - | Porl => "Porl" - | Pnorl => "Pnorl" - | Pxorl => "Pxorl" - | Pnxorl => "Pnxorl" - | Pandnl => "Pandnl" - | Pornl => "Pornl" - | Pmull => "Pmull" - | Pslll => "Pslll" - | Psrll => "Psrll" - | Psrxl => "Psrxl" - | Psral => "Psral" - | Pfaddd => "Pfaddd" - | Pfaddw => "Pfaddw" - | Pfsbfd => "Pfsbfd" - | Pfsbfw => "Pfsbfw" - | Pfmuld => "Pfmuld" - | Pfmulw => "Pfmulw" - | Pfmind => "Pfmind" - | Pfminw => "Pfminw" - | Pfmaxd => "Pfmaxd" - | Pfmaxw => "Pfmaxw" + | Pmadd _ => "ArithARRRR0=>Pmadd" + | Pmsub _ => "ArithARRRR0=>Pmsub" end. -Definition string_of_name_rri32 (n: arith_name_rri32): pstring := +Definition string_of_name_ArithARRRR0_XZR (n: arith_arrrr0) : pstring := match n with - Pcompiw _ => "Pcompiw" - | Paddiw => "Paddiw" - | Paddxiw _ => "Paddxiw" - | Prevsubiw => "Prevsubiw" - | Prevsubxiw _ => "Prevsubxiw" - | Pmuliw => "Pmuliw" - | Pandiw => "Pandiw" - | Pnandiw => "Pnandiw" - | Poriw => "Poriw" - | Pnoriw => "Pnoriw" - | Pxoriw => "Pxoriw" - | Pnxoriw => "Pnxoriw" - | Pandniw => "Pandniw" - | Porniw => "Porniw" - | Psraiw => "Psraiw" - | Psrliw => "Psrliw" - | Psrxiw => "Psrxiw" - | Pslliw => "Pslliw" - | Proriw => "Proriw" - | Psllil => "Psllil" - | Psrlil => "Psrlil" - | Psrail => "Psrail" - | Psrxil => "Psrxil" + | Pmadd _ => "ArithARRRR0_XZR=>Pmadd" + | Pmsub _ => "ArithARRRR0_XZR=>Pmsub" end. -Definition string_of_name_rri64 (n: arith_name_rri64): pstring := +Definition string_of_name_ArithComparisonPP_CN (n: arith_comparison_pp) : pstring := match n with - Pcompil _ => "Pcompil" - | Paddil => "Paddil" - | Prevsubil => "Prevsubil" - | Paddxil _ => "Paddxil" - | Prevsubxil _ => "Prevsubxil" - | Pmulil => "Pmulil" - | Pandil => "Pandil" - | Pnandil => "Pnandil" - | Poril => "Poril" - | Pnoril => "Pnoril" - | Pxoril => "Pxoril" - | Pnxoril => "Pnxoril" - | Pandnil => "Pandnil" - | Pornil => "Pornil" + | Pcmpext _ => "ArithComparisonPP_CN=>Pcmpext" + | Pcmnext _ => "ArithComparisonPP_CN=>Pcmnext" + | Pfcmp _ => "ArithComparisonPP_CN=>Pfcmp" end. -Definition string_of_name_arrr (n: arith_name_arrr): pstring := +Definition string_of_name_ArithComparisonPP_CZ (n: arith_comparison_pp) : pstring := match n with - | Pmaddw => "Pmaddw" - | Pmaddl => "Pmaddl" - | Pmsubw => "Pmsubw" - | Pmsubl => "Pmsubl" - | Pcmove _ => "Pcmove" - | Pcmoveu _ => "Pcmoveu" - | Pfmaddfw => "Pfmaddfw" - | Pfmaddfl => "Pfmaddfl" - | Pfmsubfw => "Pfmsubfw" - | Pfmsubfl => "Pfmsubfl" + | Pcmpext _ => "ArithComparisonPP_CZ=>Pcmpext" + | Pcmnext _ => "ArithComparisonPP_CZ=>Pcmnext" + | Pfcmp _ => "ArithComparisonPP_CZ=>Pfcmp" + end. + +Definition string_of_name_ArithComparisonPP_CC (n: arith_comparison_pp) : pstring := +match n with + | Pcmpext _ => "ArithComparisonPP_CC=>Pcmpext" + | Pcmnext _ => "ArithComparisonPP_CC=>Pcmnext" + | Pfcmp _ => "ArithComparisonPP_CC=>Pfcmp" + end. + +Definition string_of_name_ArithComparisonPP_CV (n: arith_comparison_pp) : pstring := +match n with + | Pcmpext _ => "ArithComparisonPP_CV=>Pcmpext" + | Pcmnext _ => "ArithComparisonPP_CV=>Pcmnext" + | Pfcmp _ => "ArithComparisonPP_CV=>Pfcmp" end. -Definition string_of_name_arr (n: arith_name_arr): pstring := +Definition string_of_name_ArithComparisonR0R_CN (n: arith_comparison_r0r) : pstring := match n with - | Pinsf _ _ => "Pinsf" - | Pinsfl _ _ => "Pinsfl" + | Pcmp _ _ => "ArithComparisonR0R_CN=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CN=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CN=>Ptst" end. -Definition string_of_name_arri32 (n: arith_name_arri32): pstring := +Definition string_of_name_ArithComparisonR0R_CZ (n: arith_comparison_r0r) : pstring := match n with - | Pmaddiw => "Pmaddw" - | Pcmoveiw _ => "Pcmoveiw" - | Pcmoveuiw _ => "Pcmoveuiw" + | Pcmp _ _ => "ArithComparisonR0R_CZ=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CZ=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CZ=>Ptst" end. -Definition string_of_name_arri64 (n: arith_name_arri64): pstring := +Definition string_of_name_ArithComparisonR0R_CC (n: arith_comparison_r0r) : pstring := match n with - | Pmaddil => "Pmaddl" - | Pcmoveil _ => "Pcmoveil" - | Pcmoveuil _ => "Pcmoveuil" + | Pcmp _ _ => "ArithComparisonR0R_CC=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CC=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CC=>Ptst" end. -Definition string_of_arith (op: arith_op): pstring := - match op with - | OArithR n => string_of_name_r n - | OArithRR n => string_of_name_rr n - | OArithRI32 n _ => string_of_name_ri32 n - | OArithRI64 n _ => string_of_name_ri64 n - | OArithRF32 n _ => string_of_name_rf32 n - | OArithRF64 n _ => string_of_name_rf64 n - | OArithRRR n => string_of_name_rrr n - | OArithRRI32 n _ => string_of_name_rri32 n - | OArithRRI64 n _ => string_of_name_rri64 n - | OArithARRR n => string_of_name_arrr n - | OArithARR n => string_of_name_arr n - | OArithARRI32 n _ => string_of_name_arri32 n - | OArithARRI64 n _ => string_of_name_arri64 n +Definition string_of_name_ArithComparisonR0R_CV (n: arith_comparison_r0r) : pstring := + match n with + | Pcmp _ _ => "ArithComparisonR0R_CV=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CV=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CV=>Ptst" end. -Definition string_of_load_name (n: load_name) : pstring := +Definition string_of_name_ArithComparisonR0R_CN_XZR (n: arith_comparison_r0r) : pstring := match n with - Plb => "Plb" - | Plbu => "Plbu" - | Plh => "Plh" - | Plhu => "Plhu" - | Plw => "Plw" - | Plw_a => "Plw_a" - | Pld => "Pld" - | Pld_a => "Pld_a" - | Pfls => "Pfls" - | Pfld => "Pfld" + | Pcmp _ _ => "ArithComparisonR0R_CN_XZR=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CN_XZR=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CN_XZR=>Ptst" end. -Definition string_of_load (op: load_op): pstring := - match op with - | OLoadRRO n _ _ => string_of_load_name n - | OLoadRRR n _ => string_of_load_name n - | OLoadRRRXS n _ => string_of_load_name n +Definition string_of_name_ArithComparisonR0R_CZ_XZR (n: arith_comparison_r0r) : pstring := + match n with + | Pcmp _ _ => "ArithComparisonR0R_CZ_XZR=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CZ_XZR=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CZ_XZR=>Ptst" + end. + +Definition string_of_name_ArithComparisonR0R_CC_XZR (n: arith_comparison_r0r) : pstring := +match n with + | Pcmp _ _ => "ArithComparisonR0R_CC_XZR=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CC_XZR=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CC_XZR=>Ptst" end. -Definition string_of_store_name (n: store_name) : pstring := +Definition string_of_name_ArithComparisonR0R_CV_XZR (n: arith_comparison_r0r) : pstring := +match n with + | Pcmp _ _ => "ArithComparisonR0R_CV_XZR=>Pcmp" + | Pcmn _ _ => "ArithComparisonR0R_CV_XZR=>Pcmn" + | Ptst _ _ => "ArithComparisonR0R_CV_XZR=>Ptst" + end. + +Definition string_of_name_ArithComparisonP_CN (n: arith_comparison_p) : pstring := match n with - Psb => "Psb" - | Psh => "Psh" - | Psw => "Psw" - | Psw_a => "Psw_a" - | Psd => "Psd" - | Psd_a => "Psd_a" - | Pfss => "Pfss" - | Pfsd => "Pfsd" + | Pfcmp0 _ => "ArithComparisonP_CN=>Pfcmp0" + | Pcmpimm _ _ => "ArithComparisonP_CN=>Pcmpimm" + | Pcmnimm _ _ => "ArithComparisonP_CN=>Pcmnimm" + | Ptstimm _ _ => "ArithComparisonP_CN=>Ptstimm" + end. + +Definition string_of_name_ArithComparisonP_CZ (n: arith_comparison_p) : pstring := + match n with + | Pfcmp0 _ => "ArithComparisonP_CZ=>Pfcmp0" + | Pcmpimm _ _ => "ArithComparisonP_CZ=>Pcmpimm" + | Pcmnimm _ _ => "ArithComparisonP_CZ=>Pcmnimm" + | Ptstimm _ _ => "ArithComparisonP_CZ=>Ptstimm" + end. + +Definition string_of_name_ArithComparisonP_CC (n: arith_comparison_p) : pstring := +match n with + | Pfcmp0 _ => "ArithComparisonP_CC=>Pfcmp0" + | Pcmpimm _ _ => "ArithComparisonP_CC=>Pcmpimm" + | Pcmnimm _ _ => "ArithComparisonP_CC=>Pcmnimm" + | Ptstimm _ _ => "ArithComparisonP_CC=>Ptstimm" + end. + +Definition string_of_name_ArithComparisonP_CV (n: arith_comparison_p) : pstring := +match n with + | Pfcmp0 _ => "ArithComparisonP_CV=>Pfcmp0" + | Pcmpimm _ _ => "ArithComparisonP_CV=>Pcmpimm" + | Pcmnimm _ _ => "ArithComparisonP_CV=>Pcmnimm" + | Ptstimm _ _ => "ArithComparisonP_CV=>Ptstimm" end. -Definition string_of_store (op: store_op) : pstring := +Definition string_of_arith (op: arith_op): pstring := match op with - | OStoreRRO n _ => string_of_store_name n - | OStoreRRR n => string_of_store_name n - | OStoreRRRXS n => string_of_store_name n + | OArithP n => string_of_name_ArithP n + | OArithPP n => string_of_name_ArithPP n + | OArithPPP n => string_of_name_ArithPPP n + | OArithRR0R n => string_of_name_ArithRR0R n + | OArithRR0R_XZR n _ => string_of_name_ArithRR0R_XZR n + | OArithRR0 n => string_of_name_ArithRR0 n + | OArithRR0_XZR n _ => string_of_name_ArithRR0_XZR n + | OArithARRRR0 n => string_of_name_ArithARRRR0 n + | OArithARRRR0_XZR n _ => string_of_name_ArithARRRR0_XZR n + | OArithComparisonPP_CN n => string_of_name_ArithComparisonPP_CN n + | OArithComparisonPP_CZ n => string_of_name_ArithComparisonPP_CZ n + | OArithComparisonPP_CC n => string_of_name_ArithComparisonPP_CC n + | OArithComparisonPP_CV n => string_of_name_ArithComparisonPP_CV n + | OArithComparisonR0R_CN n _ => string_of_name_ArithComparisonR0R_CN n + | OArithComparisonR0R_CZ n _ => string_of_name_ArithComparisonR0R_CZ n + | OArithComparisonR0R_CC n _ => string_of_name_ArithComparisonR0R_CC n + | OArithComparisonR0R_CV n _ => string_of_name_ArithComparisonR0R_CV n + | OArithComparisonR0R_CN_XZR n _ _ => string_of_name_ArithComparisonR0R_CN_XZR n + | OArithComparisonR0R_CZ_XZR n _ _ => string_of_name_ArithComparisonR0R_CZ_XZR n + | OArithComparisonR0R_CC_XZR n _ _ => string_of_name_ArithComparisonR0R_CC_XZR n + | OArithComparisonR0R_CV_XZR n _ _ => string_of_name_ArithComparisonR0R_CV_XZR n + | OArithComparisonP_CN n => string_of_name_ArithComparisonP_CN n + | 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" + | Ofmovi _ => "Ofmovi" + | Ofmovi_XZR _ => "Ofmovi_XZR" + | Ocsel _ => "Ocsel" + | Ofnmul _ => "Ofnmul" end. Definition string_of_control (op: control_op) : pstring := match op with - | Oj_l _ => "Oj_l" - | Ocb _ _ => "Ocb" - | Ocbu _ _ => "Ocbu" - | Odiv => "Odiv" - | Odivu => "Odivu" - | Ojumptable _ => "Ojumptable" - | OError => "OError" + | Ob _ => "Ob" | OIncremPC _ => "OIncremPC" + (*| Oj_l _ => "Oj_l"*) + (*| Ocb _ _ => "Ocb"*) + (*| Ocbu _ _ => "Ocbu"*) + (*| Odiv => "Odiv"*) + (*| Odivu => "Odivu"*) + (*| Ojumptable _ => "Ojumptable"*) + (*| OError => "OError"*) + (*| OIncremPC _ => "OIncremPC"*) end. Definition string_of_op (op: P.op): ?? pstring := match op with | Arith op => RET (string_of_arith op) - | Load op => RET (string_of_load op) - | Store op => RET (string_of_store op) + (*| Load op => RET (string_of_load op)*) + (*| Store op => RET (string_of_store op)*) | Control op => RET (string_of_control op) - | Allocframe _ _ => RET (Str "Allocframe") - | Allocframe2 _ _ => RET (Str "Allocframe2") - | Freeframe _ _ => RET (Str "Freeframe") - | Freeframe2 _ _ => RET (Str "Freeframe2") - | Constant _ => RET (Str "Constant") - | Fail => RET (Str "Fail") + (*| Allocframe _ _ => RET (Str "Allocframe")*) + (*| Allocframe2 _ _ => RET (Str "Allocframe2")*) + (*| Freeframe _ _ => RET (Str "Freeframe")*) + (*| Freeframe2 _ _ => RET (Str "Freeframe2")*) + (*| Constant _ => RET (Str "Constant")*) + (*| Fail => RET (Str "Fail")*) end. - *) End SECT_BBLOCK_EQUIV. (** REWRITE RULES *) -(*Definition is_constant (o: op): bool :=*) - (*match o with*) - (*| Constant _ | OArithR _ | OArithRI32 _ _ | OArithRI64 _ _ | OArithRF32 _ _ | OArithRF64 _ _ => true*) - (*| _ => false*) - (*end.*) +Definition is_constant (o: op): bool := + match o with + | OArithP _ | OArithRR0_XZR _ _ | Ofmovi_XZR _ => true + | _ => false + end. -(*Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None.*) -(*Proof.*) - (*destruct o; simpl in * |- *; try congruence.*) - (*destruct ao; simpl in * |- *; try congruence;*) - (*destruct n; simpl in * |- *; try congruence;*) - (*unfold arith_eval; destruct ge; simpl in * |- *; try congruence.*) -(*Qed.*) +Lemma is_constant_correct ge o: is_constant o = true -> op_eval ge o [] <> None. +Proof. + destruct o; simpl in * |- *; try congruence. + destruct op0; simpl in * |- *; try congruence; + destruct n; simpl in * |- *; try congruence; + unfold arith_eval; destruct ge; simpl in * |- *; try congruence. +Qed. Definition main_reduce (t: Terms.term):= RET (Terms.nofail is_constant t). @@ -2052,7 +2143,7 @@ Qed. Definition reduce := {| Terms.result := main_reduce; Terms.result_correct := main_reduce_correct |}. -Definition bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock) : ?? bool := +Definition bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock) : ?? bool := if verb then IST.verb_bblock_simu_test reduce string_of_name string_of_op (trans_block p1) (trans_block p2) else @@ -2062,23 +2153,24 @@ Local Hint Resolve IST.bblock_simu_test_correct bblock_simu_reduce IST.verb_bblo (** Main simulation (Impure) theorem *) Theorem bblock_simu_test_correct verb p1 p2 : - WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn, Asmblockprops.bblock_simu ge fn p1 p2. + WHEN bblock_simu_test verb p1 p2 ~> b THEN b=true -> forall ge fn lk, Asmblockprops.bblock_simu lk ge fn p1 p2. Proof. wlp_simplify. -Qed. +Admitted. +(*Qed.*) Hint Resolve bblock_simu_test_correct: wlp. (** ** Coerce bblock_simu_test into a pure function (this is a little unsafe like all oracles in CompCert). *) Import UnsafeImpure. -Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmvliw.bblock): bool := +Definition pure_bblock_simu_test (verb: bool) (p1 p2: Asmblock.bblock): bool := match unsafe_coerce (bblock_simu_test verb p1 p2) with | Some b => b | None => false end. -Theorem pure_bblock_simu_test_correct verb p1 p2 ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2. +Theorem pure_bblock_simu_test_correct verb p1 p2 lk ge fn: pure_bblock_simu_test verb p1 p2 = true -> Asmblockprops.bblock_simu lk ge fn p1 p2. Proof. unfold pure_bblock_simu_test. destruct (unsafe_coerce (bblock_simu_test verb p1 p2)) eqn: UNSAFE; try discriminate. @@ -2086,9 +2178,9 @@ Proof. apply unsafe_coerce_not_really_correct; eauto. Qed. -Definition bblock_simub: Asmvliw.bblock -> Asmvliw.bblock -> bool := pure_bblock_simu_test true. +Definition bblock_simub: Asmblock.bblock -> Asmblock.bblock -> bool := pure_bblock_simu_test true. -Lemma bblock_simub_correct p1 p2 ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu ge fn p1 p2. +Lemma bblock_simub_correct p1 p2 lk ge fn: bblock_simub p1 p2 = true -> Asmblockprops.bblock_simu lk ge fn p1 p2. Proof. eapply (pure_bblock_simu_test_correct true). -Qed.*) +Qed. -- cgit