diff options
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 180 |
1 files changed, 172 insertions, 8 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 97612601..23699f4a 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -44,6 +44,12 @@ 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. @@ -75,7 +81,11 @@ Lemma functions_translated: Proof (Genv.find_funct_ptr_transf_partial TRANSF). (* Asmblock and Asm share the same definition of state *) -Definition match_states (s1 s2 : state) := s1 = s2. +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). Lemma transf_initial_states: forall s1, Asmblock.initial_state prog s1 -> @@ -87,7 +97,9 @@ Proof. - econstructor. eapply (Genv.init_mem_transf_partial TRANSF); eauto. - rewrite (match_program_main TRANSF); rewrite symbol_addresses_preserved. - unfold rs; reflexivity. + unfold rs. unfold Vnullptr. unfold ge. + repeat (econstructor; eauto); simpl. + destruct Archi.ptr64; rewrite Pregmap.gss; discriminate. Qed. Lemma transf_final_states: @@ -95,9 +107,151 @@ 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; constructor; assumption. + inv FINAL_s1. inv MATCH. + inversion AG as (IR). + rewrite PC in *; rewrite IR in *; + constructor; trivial. 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 -> @@ -107,15 +261,25 @@ Proof. inv STEP; simpl; exploit functions_translated; eauto; intros (tf0 & FINDtf & TRANSf); monadInv TRANSf. - - (* internal step *) admit. + - (* internal step *) + destruct H2. (* exec_bblock *) + 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 <- MATCH. - exploit external_call_symbols_preserved; eauto. apply senv_preserved. - intros ?. + rewrite AGPC in *. eapply Asm.exec_step_external; eauto. - + econstructor; 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. Admitted. Lemma transf_program_correct: |