From 7c784807d9a3664332e9bca6cb9a967873abf8a6 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 11 Nov 2020 00:21:58 +0100 Subject: PArithCmpR0R in checker --- aarch64/Asmblockdeps.v | 166 ++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 130 insertions(+), 36 deletions(-) (limited to 'aarch64/Asmblockdeps.v') diff --git a/aarch64/Asmblockdeps.v b/aarch64/Asmblockdeps.v index df9586c1..29d91d1c 100644 --- a/aarch64/Asmblockdeps.v +++ b/aarch64/Asmblockdeps.v @@ -91,7 +91,14 @@ Inductive arith_op := | OArithComparisonPP_CC (n: arith_comparison_pp) | OArithComparisonPP_CV (n: arith_comparison_pp) | OArithComparisonR0R (n: arith_comparison_r0r) - | OArithComparisonR0R_XZR (n: arith_comparison_r0r) (vz: val) + | OArithComparisonR0R_CN (n: arith_comparison_r0r) (is: isize) + | OArithComparisonR0R_CZ (n: arith_comparison_r0r) (is: isize) + | OArithComparisonR0R_CC (n: arith_comparison_r0r) (is: isize) + | OArithComparisonR0R_CV (n: arith_comparison_r0r) (is: isize) + | OArithComparisonR0R_CN_XZR (n: arith_comparison_r0r) (is: isize) (vz: val) + | 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) . @@ -101,6 +108,12 @@ Inductive op_wrap := | Control (co: control_op) . +Definition v_compare_int (v1 v2: val) : CRflags := + {| _CN := (Val.negative (Val.sub v1 v2)); + _CZ := (Val_cmpu Ceq v1 v2); + _CC := (Val_cmpu Cge v1 v2); + _CV := (Val.sub_overflow v1 v2) |}. + Definition v_compare_long (v1 v2: val) : CRflags := {| _CN := (Val.negativel (Val.subl v1 v2)); _CZ := (Val_cmplu Ceq v1 v2); @@ -141,7 +154,11 @@ Definition arith_eval_comparison_pp (n: arith_comparison_pp) (v1 v2: val) := | Pcmpext _ | Pcmnext _ => v_compare_long v1' v2' | Pfcmp S => v_compare_single v1' v2' | Pfcmp D => v_compare_float v1' v2' - end. + 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 op:=op_wrap. @@ -160,6 +177,14 @@ Definition arith_op_eval (op: arith_op) (l: list value) := | OArithComparisonPP_CZ n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CZ))) | OArithComparisonPP_CC n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CC))) | OArithComparisonPP_CV n, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_pp n v1 v2).(_CV))) + | OArithComparisonR0R_CN n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CN))) + | OArithComparisonR0R_CZ n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CZ))) + | OArithComparisonR0R_CC n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CC))) + | OArithComparisonR0R_CV n is, [Val v1; Val v2] => Some (Val ((arith_eval_comparison_r0r n v1 v2 is).(_CV))) + | OArithComparisonR0R_CN_XZR n is vz, [Val v2] => Some (Val ((arith_eval_comparison_r0r n vz v2 is).(_CN))) + | 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))) | _, _ => None end. @@ -216,6 +241,22 @@ Definition arith_op_eq (o1 o2: arith_op): ?? bool := match o2 with OArithComparisonPP_CC n2 => phys_eq n1 n2 | _ => RET false end | 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 + | OArithComparisonR0R_CZ n1 is1 => + match o2 with OArithComparisonR0R_CZ n2 is2 => iandb (phys_eq n1 n2) (phys_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 + | OArithComparisonR0R_CV n1 is1 => + match o2 with OArithComparisonR0R_CV n2 is2 => iandb (phys_eq n1 n2) (phys_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 + | 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 + | 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 + | 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 =>*) @@ -475,37 +516,45 @@ Definition trans_arith (ai: ar_instruction) : inst := | PArithP n rd => [(#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 => let lr := match r1 with - | RR0 r1' => Op(Arith (OArithRR0R n)) (PReg(#r1') @ PReg(#r2) @ Enil) - | XZR => let vz := match arith_rr0r_isize n with - | W => Vint Int.zero - | X => Vlong Int64.zero - end in - Op(Arith (OArithRR0R_XZR n vz)) (PReg(#r2) @ Enil) - end in - [(#rd, lr)] - | PArithRR0 n rd r1 => let lr := match r1 with - | RR0 r1' => Op(Arith (OArithRR0 n)) (PReg(#r1') @ Enil) - | XZR => let vz := match arith_rr0_isize n with - | W => Vint Int.zero - | X => Vlong Int64.zero - end in - Op(Arith (OArithRR0_XZR n vz)) (Enil) - end in - [(#rd, lr)] - | PArithARRRR0 n rd r1 r2 r3 => let lr := match r3 with - | RR0 r3' => Op(Arith (OArithARRRR0 n)) (PReg(#r1) @ PReg (#r2) @ PReg(#r3') @ Enil) - | XZR => let vz := match arith_arrrr0_isize n with - | W => Vint Int.zero - | X => Vlong Int64.zero - end in - Op(Arith (OArithARRRR0_XZR n vz)) (PReg(#r1) @ PReg(#r2) @ Enil) - end in - [(#rd, lr)] - | PArithComparisonPP n r1 r2 => [(#CN, Op(Arith (OArithComparisonPP_CN n)) (PReg(#r1) @ PReg(#r2) @ Enil)); - (#CZ, Op(Arith (OArithComparisonPP_CZ n)) (PReg(#r1) @ PReg(#r2) @ Enil)); - (#CC, Op(Arith (OArithComparisonPP_CC n)) (PReg(#r1) @ PReg(#r2) @ Enil)); - (#CV, Op(Arith (OArithComparisonPP_CV n)) (PReg(#r1) @ PReg(#r2) @ Enil))] + | PArithRR0R n rd r1 r2 => + let lr := match r1 with + | RR0 r1' => Op(Arith (OArithRR0R n)) (PReg(#r1') @ PReg(#r2) @ Enil) + | XZR => let vz := if arith_rr0r_isize n then Vint Int.zero else Vlong Int64.zero in + Op(Arith (OArithRR0R_XZR n vz)) (PReg(#r2) @ Enil) + end in + [(#rd, lr)] + | PArithRR0 n rd r1 => + let lr := match r1 with + | RR0 r1' => Op(Arith (OArithRR0 n)) (PReg(#r1') @ Enil) + | XZR => let vz := if arith_rr0_isize n then Vint Int.zero else Vlong Int64.zero in + Op(Arith (OArithRR0_XZR n vz)) (Enil) + end in + [(#rd, lr)] + | PArithARRRR0 n rd r1 r2 r3 => + let lr := match r3 with + | RR0 r3' => Op(Arith (OArithARRRR0 n)) (PReg(#r1) @ PReg (#r2) @ PReg(#r3') @ Enil) + | XZR => let vz := if arith_arrrr0_isize n then Vint Int.zero else Vlong Int64.zero in + Op(Arith (OArithARRRR0_XZR n vz)) (PReg(#r1) @ PReg(#r2) @ Enil) + end in + [(#rd, lr)] + | PArithComparisonPP n r1 r2 => + [(#CN, Op(Arith (OArithComparisonPP_CN n)) (PReg(#r1) @ PReg(#r2) @ Enil)); + (#CZ, Op(Arith (OArithComparisonPP_CZ n)) (PReg(#r1) @ PReg(#r2) @ Enil)); + (#CC, Op(Arith (OArithComparisonPP_CC n)) (PReg(#r1) @ PReg(#r2) @ Enil)); + (#CV, Op(Arith (OArithComparisonPP_CV n)) (PReg(#r1) @ PReg(#r2) @ Enil))] + | PArithComparisonR0R n r1 r2 => + let is := arith_comparison_r0r_isize n in + match r1 with + | RR0 r1' => [(#CN, Op(Arith (OArithComparisonR0R_CN n is)) (PReg(#r1') @ PReg(#r2) @ Enil)); + (#CZ, Op(Arith (OArithComparisonR0R_CZ n is)) (PReg(#r1') @ PReg(#r2) @ Enil)); + (#CC, Op(Arith (OArithComparisonR0R_CC n is)) (PReg(#r1') @ PReg(#r2) @ Enil)); + (#CV, Op(Arith (OArithComparisonR0R_CV n is)) (PReg(#r1') @ PReg(#r2) @ Enil))] + | XZR => let vz := if is then Vint Int.zero else Vlong Int64.zero in + [(#CN, Op(Arith (OArithComparisonR0R_CN_XZR n is vz)) (PReg(#r2) @ Enil)); + (#CZ, Op(Arith (OArithComparisonR0R_CZ_XZR n is vz)) (PReg(#r2) @ Enil)); + (#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))]*) @@ -804,7 +853,7 @@ Ltac replace_ppos := try erewrite !ireg_pos_ppos; try erewrite !freg_pos_ppos. -Ltac DI0N0 ir0 := destruct ir0 as [rr0DIRN0|]; subst; simpl. +Ltac DI0N0 ir0 := destruct ir0; subst; simpl. Ltac DIRN1 ir := destruct ir as [irrDIRN1|]; subst; try destruct irrDIRN1; simpl. @@ -993,6 +1042,43 @@ Proof. discriminate_preg_flags ]). Qed. +Lemma compare_int_res_aux: forall sr mr rsr rr + (HMEM: sr pmem = Memstate mr) + (HEQV: forall r : preg, sr (# r) = Val (rsr r)), + ((((sr <[ 2 <- Val (_CN (v_compare_int Vundef Vundef)) ]>) <[ 3 <- + Val (_CZ (v_compare_int Vundef Vundef)) ]>) <[ 4 <- + Val (_CC (v_compare_int Vundef Vundef)) ]>) <[ 5 <- + Val (_CV (v_compare_int Vundef Vundef)) ]>) (# rr) = +Val + ((compare_int rsr Vundef Vundef) rr). +Proof. + intros. unfold v_compare_int, compare_int. + (destruct rr; + [ DDRF d; discriminate_preg_flags | + validate_crbit_flags c | + discriminate_preg_flags ]). +Qed. + +Lemma compare_int_res: forall sr mr rsr rr v1 v2 + (HMEM: sr pmem = Memstate mr) + (HEQV: forall r : preg, sr (# r) = Val (rsr r)), + ((((sr <[ 2 <- Val (_CN (v_compare_int v1 v2)) ]>) <[ 3 <- + Val (_CZ (v_compare_int v1 v2)) ]>) <[ 4 <- + Val (_CC (v_compare_int v1 v2)) ]>) <[ 5 <- + Val (_CV (v_compare_int v1 v2)) ]>) (# rr) = +Val + ((compare_int rsr v1 v2) rr). +Proof. + intros. + destruct v1; destruct v2; + try eapply compare_int_res_aux; eauto; + unfold v_compare_int, compare_int; + (destruct rr; + [ DDRF d; discriminate_preg_flags | + validate_crbit_flags c | + discriminate_preg_flags ]). +Qed. + (** Parallelizability test of a bblock (bundle), and bisimulation of the Asmblock and L parallel semantics *) (*Module PChk := ParallelChecks L PosPseudoRegSet.*) @@ -1052,8 +1138,16 @@ Proof. try (eapply compare_single_res; eauto); try (eapply compare_long_res; eauto); try (eapply compare_float_res; eauto). - - admit. - + - (* PArithComparisonR0R *) + simpl. destruct r1; ( + simpl; destruct i; + repeat (replace_ppos; replace_regs_pos; 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. (* -- cgit