diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 14:08:52 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 14:08:52 +0200 |
commit | f9feebf866ec62fc57cb6e7deea9864b65945f16 (patch) | |
tree | 5f8685800e980d14be77a150420fc52825dc0761 | |
parent | 7556ba3dc77b1811b8a1063acc45ac1972865363 (diff) | |
download | compcert-kvx-f9feebf866ec62fc57cb6e7deea9864b65945f16.tar.gz compcert-kvx-f9feebf866ec62fc57cb6e7deea9864b65945f16.zip |
moving forward with proofs
-rw-r--r-- | backend/Allocation.v | 14 | ||||
-rw-r--r-- | backend/Allocproof.v | 44 |
2 files changed, 29 insertions, 29 deletions
diff --git a/backend/Allocation.v b/backend/Allocation.v index 2fa3fc0b..c1fbf90d 100644 --- a/backend/Allocation.v +++ b/backend/Allocation.v @@ -1029,7 +1029,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv) do e1 <- track_moves env mv2 e; do e2 <- transfer_use_def args dst args' dst' (destroyed_by_load chunk addr) e1; track_moves env mv1 e2 - | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => + | BSload2 trap addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => do e1 <- track_moves env mv3 e; let e2 := remove_equation (Eq kind_second_word dst (R dst2')) e1 in assertion (loc_unconstrained (R dst2') e2); @@ -1042,14 +1042,14 @@ Definition transfer_aux (f: RTL.function) (env: regenv) assertion (reg_unconstrained dst e5); do e6 <- add_equations args args1' e5; track_moves env mv1 e6 - | BSload2_1 addr args dst mv1 args' dst' mv2 s => + | BSload2_1 trap addr args dst mv1 args' dst' mv2 s => do e1 <- track_moves env mv2 e; let e2 := remove_equation (Eq kind_first_word dst (R dst')) e1 in assertion (reg_loc_unconstrained dst (R dst') e2); assertion (can_undef (destroyed_by_load Mint32 addr) e2); do e3 <- add_equations args args' e2; track_moves env mv1 e3 - | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => + | BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s => do e1 <- track_moves env mv2 e; let e2 := remove_equation (Eq kind_second_word dst (R dst')) e1 in assertion (reg_loc_unconstrained dst (R dst') e2); @@ -1265,10 +1265,10 @@ Definition successors_block_shape (bsh: block_shape) : list node := | BShighlong src dst mv s => s :: nil | BSop op args res mv1 args' res' mv2 s => s :: nil | BSopdead op args res mv s => s :: nil - | BSload chunk addr args dst mv1 args' dst' mv2 s => s :: nil - | BSload2 addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil - | BSload2_1 addr args dst mv1 args' dst' mv2 s => s :: nil - | BSload2_2 addr addr' args dst mv1 args' dst' mv2 s => s :: nil + | BSload trap chunk addr args dst mv1 args' dst' mv2 s => s :: nil + | BSload2 trap addr addr' args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s => s :: nil + | BSload2_1 trap addr args dst mv1 args' dst' mv2 s => s :: nil + | BSload2_2 trap addr addr' args dst mv1 args' dst' mv2 s => s :: nil | BSloaddead chunk addr args dst mv s => s :: nil | BSstore chunk addr args src mv1 args' src' s => s :: nil | BSstore2 addr addr' args src mv1 args1' src1' mv2 args2' src2' s => s :: nil diff --git a/backend/Allocproof.v b/backend/Allocproof.v index ac4122bc..428bcc0e 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -98,37 +98,37 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr (expand_moves mv (Lbranch s :: k)) | ebs_load: forall trap chunk addr args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> - expand_block_shape (BSload chunk addr args dst mv1 args' dst' mv2 s) + expand_block_shape (BSload trap chunk addr args dst mv1 args' dst' mv2 s) (Iload trap chunk addr args dst s) (expand_moves mv1 - (Lload chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_load2: forall addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k, + (Lload trap chunk addr args' dst' :: expand_moves mv2 (Lbranch s :: k))) + | ebs_load2: forall trap addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s k, wf_moves mv1 -> wf_moves mv2 -> wf_moves mv3 -> Archi.splitlong = true -> offset_addressing addr 4 = Some addr2 -> - expand_block_shape (BSload2 addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s) - (Iload Mint64 addr args dst s) + expand_block_shape (BSload2 trap addr addr2 args dst mv1 args1' dst1' mv2 args2' dst2' mv3 s) + (Iload trap Mint64 addr args dst s) (expand_moves mv1 - (Lload Mint32 addr args1' dst1' :: + (Lload trap Mint32 addr args1' dst1' :: expand_moves mv2 - (Lload Mint32 addr2 args2' dst2' :: + (Lload trap Mint32 addr2 args2' dst2' :: expand_moves mv3 (Lbranch s :: k)))) - | ebs_load2_1: forall addr args dst mv1 args' dst' mv2 s k, + | ebs_load2_1: forall trap addr args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> Archi.splitlong = true -> - expand_block_shape (BSload2_1 addr args dst mv1 args' dst' mv2 s) - (Iload Mint64 addr args dst s) + expand_block_shape (BSload2_1 trap addr args dst mv1 args' dst' mv2 s) + (Iload trap Mint64 addr args dst s) (expand_moves mv1 - (Lload Mint32 addr args' dst' :: + (Lload trap Mint32 addr args' dst' :: expand_moves mv2 (Lbranch s :: k))) - | ebs_load2_2: forall addr addr2 args dst mv1 args' dst' mv2 s k, + | ebs_load2_2: forall trap addr addr2 args dst mv1 args' dst' mv2 s k, wf_moves mv1 -> wf_moves mv2 -> Archi.splitlong = true -> offset_addressing addr 4 = Some addr2 -> - expand_block_shape (BSload2_2 addr addr2 args dst mv1 args' dst' mv2 s) - (Iload Mint64 addr args dst s) + expand_block_shape (BSload2_2 trap addr addr2 args dst mv1 args' dst' mv2 s) + (Iload trap Mint64 addr args dst s) (expand_moves mv1 - (Lload Mint32 addr2 args' dst' :: + (Lload trap Mint32 addr2 args' dst' :: expand_moves mv2 (Lbranch s :: k))) | ebs_load_dead: forall trap chunk addr args dst mv s k, wf_moves mv -> @@ -1970,8 +1970,8 @@ Ltac UseShape := end. Remark addressing_not_long: - forall env f addr args dst s r, - wt_instr f env (Iload Mint64 addr args dst s) -> Archi.splitlong = true -> + forall trap env f addr args dst s r, + wt_instr f env (Iload trap Mint64 addr args dst s) -> Archi.splitlong = true -> In r args -> r <> dst. Proof. intros. inv H. @@ -1981,7 +1981,7 @@ Proof. { rewrite <- H5. apply in_map; auto. } assert (C: env r = Tint). { apply A in B. rewrite B. unfold Tptr. rewrite Archi.splitlong_ptr32 by auto. auto. } - red; intros; subst r. rewrite C in H8; discriminate. + red; intros; subst r. rewrite C in H9; discriminate. Qed. (** The proof of semantic preservation is a simulation argument of the @@ -2083,7 +2083,7 @@ Proof. eapply wt_exec_Iop; eauto. (* load regular *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit (exec_moves mv1); eauto. intros [ls1 [A1 B1]]. exploit transfer_use_def_satisf; eauto. intros [X Y]. exploit eval_addressing_lessdef; eauto. intros [a' [F G]]. @@ -2100,7 +2100,7 @@ Proof. econstructor; eauto. (* load pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. @@ -2155,7 +2155,7 @@ Proof. econstructor; eauto. (* load first word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. @@ -2185,7 +2185,7 @@ Proof. econstructor; eauto. (* load second word of a pair *) -- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. +- generalize (wt_exec_Iload _ _ _ _ _ _ _ _ _ _ _ _ WTI H1 WTRS). intros WTRS'. exploit loadv_int64_split; eauto. intros (v1 & v2 & LOAD1 & LOAD2 & V1 & V2). set (v2' := if Archi.big_endian then v2 else v1) in *. set (v1' := if Archi.big_endian then v1 else v2) in *. |