diff options
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 57 |
1 files changed, 31 insertions, 26 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 690a54a2..cec8ea69 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1092,11 +1092,11 @@ Proof. + next_stuck_cong. Qed. -Lemma load_double_preserved n rs1 m1 rs1' m1' rs2 m2 rd1 rd2 chk f a: forall +Lemma load_double_preserved n rs1 m1 rs1' m1' rs2 m2 rd1 rd2 chk1 chk2 f a: forall (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) - (HLOAD: exec_load_double lk chk f a rd1 rd2 rs1 m1 = Next rs1' m1'), - exists (rs2' : regset) (m2' : mem), Asm.exec_load_double tge chk f a rd1 rd2 rs2 m2 = Next rs2' m2' + (HLOAD: exec_load_double lk chk1 chk2 f a rd1 rd2 rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_load_double tge chk1 chk2 f a rd1 rd2 rs2 m2 = Next rs2' m2' /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). Proof. intros. @@ -1105,10 +1105,10 @@ Proof. erewrite <- !eval_addressing_preserved; eauto. destruct (is_pair_addressing_mode_correct a); try discriminate. destruct (Mem.loadv _ _ _); - destruct (Mem.loadv chk m2 + destruct (Mem.loadv chk2 m2 (eval_addressing lk - (get_offset_addr a match chk with - | Mint32 => 4 + (get_offset_addr a match chk1 with + | Mint32 | Many32 => 4 | _ => 8 end) rs1)); inversion HLOAD; auto. @@ -1141,11 +1141,11 @@ Proof. + next_stuck_cong. Qed. -Lemma store_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk a: forall +Lemma store_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk1 chk2 a: forall (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) - (HSTORE: exec_store_double lk chk a v1 v2 rs1 m1 = Next rs1' m1'), - exists (rs2' : regset) (m2' : mem), Asm.exec_store_double tge chk a v1 v2 rs2 m2 = Next rs2' m2' + (HSTORE: exec_store_double lk chk1 chk2 a v1 v2 rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_store_double tge chk1 chk2 a v1 v2 rs2 m2 = Next rs2' m2' /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). Proof. intros. @@ -1154,12 +1154,13 @@ Proof. erewrite <- !eval_addressing_preserved; eauto. destruct (is_pair_addressing_mode_correct a); try discriminate. destruct (Mem.storev _ _ _ _); - try destruct (Mem.storev chk m - (eval_addressing lk - (get_offset_addr a match chk with - | Mint32 => 4 - | _ => 8 - end) rs1) v2); + try destruct (Mem.storev chk2 m + (eval_addressing lk + (get_offset_addr a + match chk1 with + | Mint32 | Many32 => 4 + | _ => 8 + end) rs1) v2); inversion HSTORE; auto. repeat (econstructor; eauto). * eapply nextinstr_agree_but_pc; intros. @@ -1935,28 +1936,25 @@ Proof. rewrite <- (label_pos_preserved f); auto. inversion MATCHI; subst. destruct label_pos; next_stuck_cong. - destruct (((incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef) # X17 <- Vundef PC) eqn:INCRPC; next_stuck_cong. + destruct ((incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef PC) eqn:INCRPC; next_stuck_cong. inversion H0; auto. repeat (econstructor; eauto). rewrite !Pregmap.gso; try congruence. rewrite <- AGPC. unfold incrPC in *. destruct (rs1 PC) eqn:EQRS1; simpl in *; try discriminate. - replace (((rs2 # X16 <- Vundef) # X17 <- Vundef) # PC <- (Vptr b0 (Ptrofs.repr z))) with - ((((rs1 # PC <- (Vptr b0 (Ptrofs.add i1 (Ptrofs.repr (size bb))))) # X16 <- - Vundef) # X17 <- Vundef) # PC <- (Vptr b (Ptrofs.repr z))); auto. + replace ((rs2 # X16 <- Vundef) # PC <- (Vptr b0 (Ptrofs.repr z))) with + (((rs1 # PC <- (Vptr b0 (Ptrofs.add i1 (Ptrofs.repr (size bb))))) # X16 <- + Vundef) # PC <- (Vptr b (Ptrofs.repr z))); auto. eapply functional_extensionality; intros x. destruct (PregEq.eq x PC); subst. + rewrite Pregmap.gso in INCRPC; try congruence. - rewrite Pregmap.gso in INCRPC; try congruence. rewrite Pregmap.gss in INCRPC. rewrite !Pregmap.gss in *; congruence. + rewrite Pregmap.gso; auto. rewrite (Pregmap.gso (i := x) (j := PC)); auto. - destruct (PregEq.eq x X17); subst. + destruct (PregEq.eq x X16); subst. * rewrite !Pregmap.gss; auto. - * rewrite !(Pregmap.gso (i := x) (j:= X17)); auto. destruct (PregEq.eq x X16); subst. - -- rewrite !Pregmap.gss; auto. - -- rewrite !Pregmap.gso; auto. + * rewrite !Pregmap.gso; auto. Qed. Lemma last_instruction_cannot_be_label bb: @@ -2187,9 +2185,16 @@ Proof. reflexivity. } apply set_builtin_res_dont_move_pc_gen. -- erewrite !set_builtin_map_not_pc. - erewrite !undef_regs_other_2. - rewrite HPC; auto. all: rewrite preg_notin_charact; intros; try discriminate. + erewrite !undef_regs_other. + rewrite HPC; auto. + all: intros; simpl in *; destruct H3 as [HX16 | [HX30 | HDES]]; subst; try discriminate; + exploit list_in_map_inv; eauto; intros [mr [A B]]; subst; discriminate. -- intros. eapply undef_reg_preserved; eauto. + intros. destruct (PregEq.eq X16 r0); destruct (PregEq.eq X30 r0); subst. + rewrite Pregmap.gso, Pregmap.gss; try congruence. + do 2 (rewrite Pregmap.gso, Pregmap.gss; try discriminate; auto). + rewrite 2Pregmap.gss; auto. + rewrite !Pregmap.gso; auto. Qed. Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall |