From 45049f8a085bb916009ee9154d7218a1a287c0da Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Sun, 12 Jul 2020 22:35:01 +0200 Subject: Revert back to original definition of match_states (The simulation relation between aarch64's Asmblock and Asm as equality) --- aarch64/Asmgenproof.v | 180 +++----------------------------------------------- 1 file changed, 8 insertions(+), 172 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 23699f4a..97612601 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -44,12 +44,6 @@ Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}. -Record agree (rs1: regset) (rs2: regset) : Prop := mkagree { - agree_ir: forall r: iregsp, (rs1 r) = (rs2 r); - agree_fr: forall r: freg, (rs1 r) = (rs2 r); - agree_cr: forall r: crbit, (rs1 r) = (rs2 r); - agree_sp_def: (rs1 SP) <> Vundef; -}. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. @@ -81,11 +75,7 @@ Lemma functions_translated: Proof (Genv.find_funct_ptr_transf_partial TRANSF). (* Asmblock and Asm share the same definition of state *) -Inductive match_states: state -> state -> Prop := - | match_states_intro rs1 rs2 m - (AG: agree rs1 rs2) - (PC: rs1 PC = rs2 PC) - : match_states (State rs1 m) (State rs2 m). +Definition match_states (s1 s2 : state) := s1 = s2. Lemma transf_initial_states: forall s1, Asmblock.initial_state prog s1 -> @@ -97,9 +87,7 @@ Proof. - econstructor. eapply (Genv.init_mem_transf_partial TRANSF); eauto. - rewrite (match_program_main TRANSF); rewrite symbol_addresses_preserved. - unfold rs. unfold Vnullptr. unfold ge. - repeat (econstructor; eauto); simpl. - destruct Archi.ptr64; rewrite Pregmap.gss; discriminate. + unfold rs; reflexivity. Qed. Lemma transf_final_states: @@ -107,151 +95,9 @@ Lemma transf_final_states: match_states s1 s2 -> Asmblock.final_state s1 r -> Asm.final_state s2 r. Proof. intros s1 s2 r MATCH FINAL_s1. - inv FINAL_s1. inv MATCH. - inversion AG as (IR). - rewrite PC in *; rewrite IR in *; - constructor; trivial. + inv FINAL_s1; inv MATCH; constructor; assumption. Qed. -Lemma agree_but_pc: - forall rs1 rs2 r, - r <> PC -> agree rs1 rs2 -> - (rs1 r) = (rs2 r). -Proof. - intros rs1 rs2 r NOTPC AG. - inversion AG as (AGIR, AGFR, AGCR). - destruct r. - - apply AGIR. - - apply AGFR. - - apply AGCR. - - contradiction. -Qed. - -Lemma agree_mregs: - forall (rs1 rs2 : regset) (r: mreg), - agree rs1 rs2 -> forall r: mreg, (rs1 (preg_of r)) = (rs2 (preg_of r)). -Proof. - intros ? ? ? ? r. apply agree_but_pc; auto. - destruct r; discriminate. -Qed. - -Lemma agree_iregs: - forall (rs1 rs2 : regset) (r: iregsp), - agree rs1 rs2 -> (rs1 r) = (rs2 r). -Proof. - intros ? ? r. apply agree_but_pc; auto. - destruct r; discriminate. -Qed. - -Lemma agree_fregs: - forall (rs1 rs2 : regset) (r: freg), - agree rs1 rs2 -> (rs1 r) = (rs2 r). -Proof. - intros ? ? r. apply agree_but_pc; auto. - destruct r; discriminate. -Qed. - -Lemma agree_sp: - forall (rs1 rs2 : regset), - agree rs1 rs2 -> (rs1 SP) = (rs2 SP). -Proof. - intros ? ? r. apply agree_but_pc; auto. - discriminate. -Qed. - -(* Copied and adapted from PseudoAsmblockproof *) -Lemma extcall_arg_match ms rs m l v: - agree ms rs -> - extcall_arg ms m l v -> - extcall_arg rs m l v. -Proof. - destruct 2. - - erewrite agree_mregs; eauto. constructor. - - econstructor; eauto. erewrite <- agree_sp; eauto. -Qed. - -Local Hint Resolve extcall_arg_match: core. - -Lemma extcall_arg_pair_match: - forall ms rs m p v, - agree ms rs -> - extcall_arg_pair ms m p v -> - extcall_arg_pair rs m p v. -Proof. - destruct 2; constructor; eauto. -Qed. - -Local Hint Resolve extcall_arg_pair_match: core. - -Lemma extcall_args_match: - forall ms rs m, agree ms rs -> - forall ll vl, - list_forall2 (extcall_arg_pair ms m) ll vl -> - list_forall2 (extcall_arg_pair rs m) ll vl. -Proof. - induction 2; constructor; eauto. -Qed. - -Lemma extcall_arguments_match: - forall ms m rs sg args, - agree ms rs -> - extcall_arguments ms m sg args -> - extcall_arguments rs m sg args. -Proof. - unfold extcall_arguments, extcall_arguments; intros. - eapply extcall_args_match; eauto. -Qed. - -Lemma agree_undef_caller_save_regs_match: - forall rs1 rs2, - agree rs1 rs2 -> agree (undef_caller_save_regs rs1) (undef_caller_save_regs rs2). -Proof. - intros rs1 rs2 AG. - unfold undef_caller_save_regs. split; auto; intros. - - erewrite agree_iregs; auto. - - erewrite agree_fregs; auto. - - simpl; inversion AG; assumption. -Qed. - -Lemma agree_set_parallel: - forall rs1 rs2 r v, - agree rs1 rs2 -> - r <> SP \/ v <> Vundef -> (* TODO is the right case ever useful? *) - agree (rs1#r <- v) (rs2#r <- v). -Proof. - intros rs1 rs2 r v AG H. split; auto. - (* TODO refactor repetitive proof *) - - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r). - + reflexivity. - + erewrite agree_but_pc; eauto. discriminate. - - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r). - + reflexivity. - + erewrite agree_but_pc; eauto. discriminate. - - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r). - + reflexivity. - + erewrite agree_but_pc; eauto. discriminate. - - destruct H. - + rewrite Pregmap.gso; inv AG; auto. - + destruct (PregEq.eq SP r) as [SPr | SPnotr]. - * rewrite SPr; rewrite Pregmap.gss; assumption. - * rewrite Pregmap.gso; auto. inv AG; auto. -Qed. - -Lemma agree_set_pair: - forall rs1 rs2 p v, - agree rs1 rs2 -> - (* TODO assumption that pair does not include SP *) - agree (set_pair p v rs1) (set_pair p v rs2). -Proof. - intros rs1 rs2 p v AG. - destruct p; simpl. - - assert (r <> SP) as NOTSP. { admit. } - apply agree_set_parallel; auto. - - assert (rlo <> SP /\ rhi <> SP) as NOTSP. { admit. } destruct NOTSP. - apply agree_set_parallel; auto. - + apply agree_set_parallel; auto. -Admitted. - Lemma step_simulation s1 t s1': Asmblock.step lk ge s1 t s1' -> forall s2, match_states s1 s2 -> @@ -261,25 +107,15 @@ Proof. inv STEP; simpl; exploit functions_translated; eauto; intros (tf0 & FINDtf & TRANSf); monadInv TRANSf. - - (* internal step *) - destruct H2. (* exec_bblock *) - admit. + - (* internal step *) admit. - (* external step *) - inversion MATCH as (?, ?, ?, AG, AGPC). - exploit external_call_symbols_preserved; eauto. apply senv_preserved. - exploit extcall_arguments_match; eauto. - intros. eexists; split. + apply plus_one. - rewrite AGPC in *. + rewrite <- MATCH. + exploit external_call_symbols_preserved; eauto. apply senv_preserved. + intros ?. eapply Asm.exec_step_external; eauto. - + exploit agree_undef_caller_save_regs_match; eauto; intros AG'. - erewrite agree_iregs; eauto. - econstructor; auto. - apply agree_set_parallel. - apply agree_set_pair. - * apply agree_undef_caller_save_regs_match; auto. - * left. discriminate. + + econstructor; eauto. Admitted. Lemma transf_program_correct: -- cgit