diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 18:21:55 +0100 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2021-01-07 18:21:55 +0100 |
commit | 10da6dfa77f155d9d1e36e28c8bb8552601355f9 (patch) | |
tree | c04e52f494b1d41c5616d55d6e95e805cce69a60 | |
parent | 728888d8a3f70afd526f6c4454327f52ea4c4746 (diff) | |
download | compcert-kvx-10da6dfa77f155d9d1e36e28c8bb8552601355f9.tar.gz compcert-kvx-10da6dfa77f155d9d1e36e28c8bb8552601355f9.zip |
update kvx
-rw-r--r-- | kvx/Asmblockdeps.v | 8 | ||||
-rw-r--r-- | kvx/Asmblockgenproof0.v | 1 | ||||
-rw-r--r-- | kvx/Asmblockgenproof1.v | 50 | ||||
-rw-r--r-- | kvx/Asmvliw.v | 84 |
4 files changed, 45 insertions, 98 deletions
diff --git a/kvx/Asmblockdeps.v b/kvx/Asmblockdeps.v index 67430b54..b6d18c3e 100644 --- a/kvx/Asmblockdeps.v +++ b/kvx/Asmblockdeps.v @@ -398,8 +398,8 @@ Definition control_eval (o: control_op) (l: list value) := end | Ocbu bt l, [Val v; Val vpc] => match cmpu_for_btest bt with - | (Some c, Int) => eval_branch_deps fn l vpc (Val_cmpu_bool c v (Vint (Int.repr 0))) - | (Some c, Long) => eval_branch_deps fn l vpc (Val_cmplu_bool c v (Vlong (Int64.repr 0))) + | (Some c, Int) => eval_branch_deps fn l vpc (Val.mxcmpu_bool c v (Vint (Int.repr 0))) + | (Some c, Long) => eval_branch_deps fn l vpc (Val.mxcmplu_bool c v (Vlong (Int64.repr 0))) | (None, _) => None end | Odiv, [Val v1; Val v2] => @@ -1232,12 +1232,12 @@ Proof. (* Pcbu *) + rewrite (H0 PC). Simpl. rewrite (H0 r). destruct (cmpu_for_btest _); simpl; auto. destruct o; simpl; auto. unfold par_eval_branch. unfold eval_branch_deps. unfold incrPC. Simpl. destruct i. - ++ destruct (Val_cmpu_bool _ _ _); simpl; auto. destruct b. + ++ destruct (Val.mxcmpu_bool _ _ _); simpl; auto. destruct b. +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. +++ repeat (econstructor; eauto). intros rr; destruct rr; Simpl. - ++ destruct (Val_cmplu_bool _ _ _); simpl; auto. destruct b. + ++ destruct (Val.mxcmplu_bool _ _ _); simpl; auto. destruct b. +++ unfold par_goto_label. unfold goto_label_deps. destruct (label_pos _ _ _); simpl; auto. Simpl. destruct (Val.offset_ptr _ _); simpl; auto. eexists; split; try split; Simpl. intros rr; destruct rr; Simpl. diff --git a/kvx/Asmblockgenproof0.v b/kvx/Asmblockgenproof0.v index 1af59238..12bb863a 100644 --- a/kvx/Asmblockgenproof0.v +++ b/kvx/Asmblockgenproof0.v @@ -36,7 +36,6 @@ Require Import Asmblock. Require Import Asmblockgen. Require Import Conventions1. Require Import Axioms. -Require Import Machblockgenproof. (* FIXME: only use to import [is_tail_app] and [is_tail_app_inv] *) Require Import Asmblockprops. Module MB:=Machblock. diff --git a/kvx/Asmblockgenproof1.v b/kvx/Asmblockgenproof1.v index 74b9b62b..c6ad70ab 100644 --- a/kvx/Asmblockgenproof1.v +++ b/kvx/Asmblockgenproof1.v @@ -256,7 +256,7 @@ Lemma transl_compu_correct: exists rs', exec_straight ge (transl_comp cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ (Val_cmpu_bool cmp rs#r1 rs#r2 = Some b -> + /\ (Val.mxcmpu_bool cmp rs#r1 rs#r2 = Some b -> exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . @@ -272,8 +272,8 @@ Proof. assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)). { rewrite Heqrs'. auto. } rewrite H0. rewrite <- H. - remember (Val_cmpu_bool cmp rs#r1 rs#r2) as cmpubool. - destruct cmp; simpl; unfold Val_cmpu; + remember (Val.mxcmpu_bool cmp rs#r1 rs#r2) as cmpubool. + destruct cmp; simpl; unfold Val.mxcmpu; rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto; destruct b0; simpl; auto. } @@ -285,7 +285,7 @@ Lemma transl_compui_correct: exists rs', exec_straight ge (transl_compi cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ (Val_cmpu_bool cmp rs#r1 (Vint n) = Some b -> + /\ (Val.mxcmpu_bool cmp rs#r1 (Vint n) = Some b -> exec_control ge fn (Some (PCtlFlow ((Pcb BTwnez RTMP lbl)))) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . @@ -301,8 +301,8 @@ Proof. assert ((nextblock tbb rs') # RTMP = (compare_int (itest_for_cmp cmp Unsigned) rs # r1 (Vint n))). { rewrite Heqrs'. auto. } rewrite H0. rewrite <- H. - remember (Val_cmpu_bool cmp rs#r1 (Vint n)) as cmpubool. - destruct cmp; simpl; unfold Val_cmpu; + remember (Val.mxcmpu_bool cmp rs#r1 (Vint n)) as cmpubool. + destruct cmp; simpl; unfold Val.mxcmpu; rewrite <- Heqcmpubool; destruct cmpubool; simpl; auto; destruct b0; simpl; auto. } @@ -656,7 +656,7 @@ Lemma transl_complu_correct: exists rs', exec_straight ge (transl_compl cmp Unsigned r1 r2 lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val_cmplu_bool cmp rs#r1 rs#r2 = Some b -> + /\ ( Val.mxcmplu_bool cmp rs#r1 rs#r2 = Some b -> exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . @@ -672,9 +672,9 @@ Proof. assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 rs # r2)). { rewrite Heqrs'. auto. } rewrite H0. rewrite <- H. - remember (Val_cmplu_bool cmp rs#r1 rs#r2) as cmpbool. + remember (Val.mxcmplu_bool cmp rs#r1 rs#r2) as cmpbool. destruct cmp; simpl; - unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + unfold compare_long, Val.mxcmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto. } rewrite H0. simpl; auto. @@ -685,7 +685,7 @@ Lemma transl_compilu_correct: exists rs', exec_straight ge (transl_compil cmp Unsigned r1 n lbl k) rs m (Pcb BTwnez RTMP lbl ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b -> + /\ ( Val.mxcmplu_bool cmp rs#r1 (Vlong n) = Some b -> exec_control ge fn (Some (PCtlFlow (Pcb BTwnez RTMP lbl))) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . @@ -701,9 +701,9 @@ Proof. assert ((nextblock tbb rs') # RTMP = (compare_long (itest_for_cmp cmp Unsigned) rs # r1 (Vlong n))). { rewrite Heqrs'. auto. } rewrite H0. rewrite <- H. - remember (Val_cmplu_bool cmp rs#r1 (Vlong n)) as cmpbool. + remember (Val.mxcmplu_bool cmp rs#r1 (Vlong n)) as cmpbool. destruct cmp; simpl; - unfold compare_long, Val_cmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; + unfold compare_long, Val.mxcmplu; rewrite <- Heqcmpbool; destruct cmpbool; simpl; auto; destruct b0; simpl; auto. } rewrite H0. simpl; auto. @@ -715,7 +715,7 @@ Lemma transl_opt_compuimm_correct: exists rs', exists insn, exec_straight_opt (transl_opt_compuimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val_cmpu_bool cmp rs#r1 (Vint n) = Some b -> + /\ ( Val.mxcmpu_bool cmp rs#r1 (Vint n) = Some b -> exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . Proof. @@ -791,7 +791,7 @@ Lemma transl_opt_compluimm_correct: exists rs', exists insn, exec_straight_opt (transl_opt_compluimm n cmp r1 lbl k) rs m ((PControl insn) ::g k) rs' m /\ (forall r : preg, r <> PC -> r <> RTMP -> rs' r = rs r) - /\ ( Val_cmplu_bool cmp rs#r1 (Vlong n) = Some b -> + /\ ( Val.mxcmplu_bool cmp rs#r1 (Vlong n) = Some b -> exec_control ge fn (Some insn) (nextblock tbb rs') m = eval_branch fn lbl (nextblock tbb rs') m (Some b)) . Proof. @@ -859,7 +859,7 @@ Proof. destruct cmp; discriminate. Qed. -Local Hint Resolve Val_cmpu_bool_correct Val_cmplu_bool_correct: core. +Local Hint Resolve Val.mxcmpu_bool_correct Val.mxcmplu_bool_correct: core. Lemma transl_cbranch_correct_1: forall cond args lbl k c m ms b sp rs m' tbb, @@ -988,7 +988,7 @@ Proof. split. * constructor. eexact A'. * split; auto. - { apply C'; auto. eapply Val_cmplu_bool_correct; eauto. } + { apply C'; auto. eapply Val.mxcmplu_bool_correct; eauto. } (* Ccompf *) - exploit (transl_compf_correct c0 x x0 lbl); eauto. intros (rs' & A & B & C). @@ -1078,7 +1078,7 @@ Lemma transl_cond_int32u_correct: forall cmp rd r1 r2 k rs m, exists rs', exec_straight ge (basics_to_code (transl_cond_int32u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m - /\ rs'#rd = Val_cmpu cmp rs#r1 rs#r2 + /\ rs'#rd = Val.mxcmpu cmp rs#r1 rs#r2 /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. @@ -1122,7 +1122,7 @@ Lemma transl_cond_int64u_correct: forall cmp rd r1 r2 k rs m, exists rs', exec_straight ge (basics_to_code (transl_cond_int64u cmp rd r1 r2 k)) rs m (basics_to_code k) rs' m - /\ rs'#rd = Val_cmplu cmp rs#r1 rs#r2 + /\ rs'#rd = Val.mxcmplu cmp rs#r1 rs#r2 /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. Proof. intros. destruct cmp; simpl. @@ -1163,7 +1163,7 @@ Proof. split; intros; Simpl. Qed. -Local Hint Resolve Val_cmpu_correct Val_cmplu_correct: core. +Local Hint Resolve Val.mxcmpu_correct Val.mxcmplu_correct: core. Lemma transl_condimm_int32u_correct: forall cmp rd r1 n k rs m, @@ -1279,12 +1279,12 @@ Proof. - econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. - cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float32.cmp_swap. + replace (Cge) with (swap_comparison Cle); auto. rewrite Float32.cmp_swap. destruct (Float32.cmp _ _ _); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. unfold Val.cmpfs. unfold Val.cmpfs_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. - cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float32.cmp_swap. + replace (Clt) with (swap_comparison Cgt); auto. rewrite Float32.cmp_swap. destruct (Float32.cmp _ _ _); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. @@ -1345,12 +1345,12 @@ Proof. - econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. - cutrewrite (Cge = swap_comparison Cle); auto. rewrite Float.cmp_swap. + replace (Cge) with (swap_comparison Cle); auto. rewrite Float.cmp_swap. destruct (Float.cmp _ _ _); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. unfold Val.cmpf. unfold Val.cmpf_bool. destruct (rs r1); auto. destruct (rs r2); auto. simpl. - cutrewrite (Clt = swap_comparison Cgt); auto. rewrite Float.cmp_swap. + replace (Clt) with (swap_comparison Cgt); auto. rewrite Float.cmp_swap. destruct (Float.cmp _ _ _); auto. - econstructor; split. apply exec_straight_one; [simpl; eauto]. split; intros; Simpl. @@ -1374,7 +1374,7 @@ Proof. exploit transl_cond_int32s_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; eauto. + (* cmpu *) exploit transl_cond_int32u_correct; eauto. simpl. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B; eapply Val_cmpu_correct. + exists rs'; repeat split; eauto. rewrite B; eapply Val.mxcmpu_correct. + (* cmpimm *) apply transl_condimm_int32s_correct; eauto with asmgen. + (* cmpuimm *) @@ -1385,7 +1385,7 @@ Proof. + (* cmplu *) exploit transl_cond_int64u_correct; eauto. simpl. intros (rs' & A & B & C). exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. - eapply Val_cmplu_correct. + eapply Val.mxcmplu_correct. + (* cmplimm *) exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. simpl. intros (rs' & A & B & C). diff --git a/kvx/Asmvliw.v b/kvx/Asmvliw.v index 91d119bf..8afe8d07 100644 --- a/kvx/Asmvliw.v +++ b/kvx/Asmvliw.v @@ -853,58 +853,6 @@ Definition cmpu_for_btest (bt: btest) := end. -(* **** a few lemma on comparisons of unsigned (e.g. pointers) *) - -Definition Val_cmpu_bool cmp v1 v2: option bool := - Val.cmpu_bool (fun _ _ => true) cmp v1 v2. - -Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: - (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b - -> (Val_cmpu_bool cmp v1 v2) = Some b. -Proof. - intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto). -Qed. - -Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2). - -Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val): - Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2) - (Val_cmpu cmp v1 v2). -Proof. - unfold Val.cmpu, Val_cmpu. - remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob; cbn. - - erewrite Val_cmpu_bool_correct; eauto. - econstructor. - - econstructor. -Qed. - -Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val) - := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2). - -Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b: - (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b - -> (Val_cmplu_bool cmp v1 v2) = Some b. -Proof. - intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto). -Qed. - -Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2). - -Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val): - Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2)) - (Val_cmplu cmp v1 v2). -Proof. - unfold Val.cmplu, Val_cmplu. - remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob. - destruct ob as [b|]; cbn. - - erewrite Val_cmplu_bool_correct; eauto. - cbn. econstructor. - - econstructor. -Qed. - - - (** **** Comparing integers *) Definition compare_int (t: itest) (v1 v2: val): val := match t with @@ -914,12 +862,12 @@ Definition compare_int (t: itest) (v1 v2: val): val := | ITge => Val.cmp Cge v1 v2 | ITle => Val.cmp Cle v1 v2 | ITgt => Val.cmp Cgt v1 v2 - | ITneu => Val_cmpu Cne v1 v2 - | ITequ => Val_cmpu Ceq v1 v2 - | ITltu => Val_cmpu Clt v1 v2 - | ITgeu => Val_cmpu Cge v1 v2 - | ITleu => Val_cmpu Cle v1 v2 - | ITgtu => Val_cmpu Cgt v1 v2 + | ITneu => Val.mxcmpu Cne v1 v2 + | ITequ => Val.mxcmpu Ceq v1 v2 + | ITltu => Val.mxcmpu Clt v1 v2 + | ITgeu => Val.mxcmpu Cge v1 v2 + | ITleu => Val.mxcmpu Cle v1 v2 + | ITgtu => Val.mxcmpu Cgt v1 v2 end. Definition compare_long (t: itest) (v1 v2: val): val := @@ -930,12 +878,12 @@ Definition compare_long (t: itest) (v1 v2: val): val := | ITge => Val.cmpl Cge v1 v2 | ITle => Val.cmpl Cle v1 v2 | ITgt => Val.cmpl Cgt v1 v2 - | ITneu => Some (Val_cmplu Cne v1 v2) - | ITequ => Some (Val_cmplu Ceq v1 v2) - | ITltu => Some (Val_cmplu Clt v1 v2) - | ITgeu => Some (Val_cmplu Cge v1 v2) - | ITleu => Some (Val_cmplu Cle v1 v2) - | ITgtu => Some (Val_cmplu Cgt v1 v2) + | ITneu => Some (Val.mxcmplu Cne v1 v2) + | ITequ => Some (Val.mxcmplu Ceq v1 v2) + | ITltu => Some (Val.mxcmplu Clt v1 v2) + | ITgeu => Some (Val.mxcmplu Cge v1 v2) + | ITleu => Some (Val.mxcmplu Cle v1 v2) + | ITgtu => Some (Val.mxcmplu Cgt v1 v2) end in match res with | Some v => v @@ -1147,13 +1095,13 @@ Definition cmove bt v1 v2 v3 := Definition cmoveu bt v1 v2 v3 := match cmpu_for_btest bt with | (Some c, Int) => - match Val_cmpu_bool c v2 (Vint Int.zero) with + match Val.mxcmpu_bool c v2 (Vint Int.zero) with | None => Vundef | Some true => v3 | Some false => v1 end | (Some c, Long) => - match Val_cmplu_bool c v2 (Vlong Int64.zero) with + match Val.mxcmplu_bool c v2 (Vlong Int64.zero) with | None => Vundef | Some true => v3 | Some false => v1 @@ -1529,8 +1477,8 @@ Definition parexec_control (f: function) (oc: option control) (rsr rsw: regset) end | Pcbu bt r l => match cmpu_for_btest bt with - | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val_cmpu_bool c rsr#r (Vint (Int.repr 0))) - | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val_cmplu_bool c rsr#r (Vlong (Int64.repr 0))) + | (Some c, Int) => par_eval_branch f l rsr rsw mw (Val.mxcmpu_bool c rsr#r (Vint (Int.repr 0))) + | (Some c, Long) => par_eval_branch f l rsr rsw mw (Val.mxcmplu_bool c rsr#r (Vlong (Int64.repr 0))) | (None, _) => Stuck end (**r Pseudo-instructions *) |