diff options
| -rw-r--r-- | aarch64/Asmblock.v | 2 | ||||
| -rw-r--r-- | aarch64/Asmgen.v | 2 | ||||
| -rw-r--r-- | aarch64/Asmgenproof.v | 185 |
3 files changed, 167 insertions, 22 deletions
diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v index ba6a64fa..be776323 100644 --- a/aarch64/Asmblock.v +++ b/aarch64/Asmblock.v @@ -2001,7 +2001,7 @@ Inductive step: state -> trace -> state -> Prop := Genv.find_funct_ptr ge b = Some (Internal f) -> find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bi -> exec_bblock f bi rs m t rs' m' -> - step (State rs m) E0 (State rs' m') + step (State rs m) t (State rs' m') | exec_step_external: forall b ef args res rs m t rs' m', rs PC = Vptr b Ptrofs.zero -> diff --git a/aarch64/Asmgen.v b/aarch64/Asmgen.v index 08ad176a..0124bf63 100644 --- a/aarch64/Asmgen.v +++ b/aarch64/Asmgen.v @@ -350,7 +350,7 @@ Fixpoint unfold (bbs: Asmblock.bblocks) : res Asm.code := Definition transf_function (f: Asmblock.function) : res Asm.function := do c <- unfold (Asmblock.fn_blocks f); - if zlt Ptrofs.max_unsigned (Z.of_nat (length c)) + if zlt Ptrofs.max_unsigned (list_length_z c) then Error (msg "Asmgen.trans_function: code size exceeded") else OK {| Asm.fn_sig := Asmblock.fn_sig f; Asm.fn_code := c |}. diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 7f30eddf..73921c03 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -75,6 +75,20 @@ Lemma functions_translated: Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. Proof (Genv.find_funct_ptr_transf_partial TRANSF). +Lemma internal_functions_translated: + forall b f, + Genv.find_funct_ptr ge b = Some (Internal f) -> + exists tf, + Genv.find_funct_ptr tge b = Some (Internal tf) /\ transf_function f = OK tf. +Proof. + intros; exploit functions_translated; eauto. + intros (x & FIND & TRANSf). + apply bind_inversion in TRANSf. + destruct TRANSf as (tf & TRANSf & X). + inv X. + eauto. +Qed. + Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop := | is_nth_label l: list_nth_z (header bb) n = Some l -> @@ -175,25 +189,43 @@ Proof. inv FINAL_s1; inv MATCH; constructor; assumption. Qed. -Definition max_pos (f : Asm.function) := length f.(Asm.fn_code). +Definition max_pos (f : Asm.function) := list_length_z f.(Asm.fn_code). Lemma functions_bound_max_pos: forall fb f tf, Genv.find_funct_ptr ge fb = Some (Internal f) -> transf_function f = OK tf -> - Z.of_nat (max_pos tf) <= Ptrofs.max_unsigned. + max_pos tf <= Ptrofs.max_unsigned. Proof. intros fb f tf FINDf TRANSf. unfold transf_function in TRANSf. apply bind_inversion in TRANSf. destruct TRANSf as (c & TRANSf). destruct TRANSf as (_ & TRANSf). - destruct (zlt Ptrofs.max_unsigned (Z.of_nat (length c))). + destruct (zlt _ _). - inversion TRANSf. - unfold max_pos. assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. } rewrite H; omega. Qed. +Lemma size_of_blocks_max_pos pos f tf bi: + find_bblock pos (fn_blocks f) = Some bi -> + transf_function f = OK tf -> + pos + size bi <= max_pos tf. +Admitted. + +Lemma size_of_blocks_bounds fb pos f bi: + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_bblock pos (fn_blocks f) = Some bi -> + pos + size bi <= Ptrofs.max_unsigned. +Proof. + intros; exploit internal_functions_translated; eauto. + intros (tf & _ & TRANSf). + assert (pos + size bi <= max_pos tf). { eapply size_of_blocks_max_pos; eauto. } + assert (max_pos tf <= Ptrofs.max_unsigned). { eapply functions_bound_max_pos; eauto. } + omega. +Qed. + Lemma one_le_max_unsigned: 1 <= Ptrofs.max_unsigned. Proof. @@ -208,7 +240,7 @@ Lemma match_internal_exec_label: match_internal n (State rs1 m1) (State rs2 m2) -> n >= 0 -> (* There is no step if n is already max_pos *) - n < Z.of_nat (max_pos tf) -> + n < (max_pos tf) -> exists rs2' m2', Asm.exec_instr tge tf (Asm.Plabel l) rs2 m2 = Next rs2' m2' /\ match_internal (n+1) (State rs1 m1) (State rs2' m2'). Proof. @@ -419,25 +451,135 @@ Proof. + constructor. Admitted. -Lemma step_simulation s1 t s1': - Asmblock.step lk ge s1 t s1' -> - forall s2, match_states s1 s2 -> - (exists s2', plus Asm.step tge s2 t s2' /\ match_states s1' s2'). +Lemma bblock_non_empty bb: body bb <> nil \/ exit bb <> None. +Admitted. + +Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)). +Admitted. + +Lemma exec_header_simulation b ofs f bb rs m: forall + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb), + exists s', star Asm.step tge (State rs m) E0 s' + /\ match_internal (list_length_z (header bb)) (State rs m) s'. +Admitted. + +Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (NEMPTY_BODY: body bb <> nil) + (MATCHI: match_internal (list_length_z (header bb)) (State rs m) s2) + (BODY: exec_body lk ge (body bb) rs m = Next rs' m'), + exists s2', plus Asm.step tge s2 E0 s2' + /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'. +Admitted. + +Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (MATCHI: match_internal (list_length_z (header bb)) (State rs m) s2) + (BODY: exec_body lk ge (body bb) rs m = Next rs' m'), + exists s2', star Asm.step tge s2 E0 s2' + /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'. +Proof. + intros. + destruct (body bb) eqn: Hbb. + - simpl in BODY. inv BODY. + eexists. split. + eapply star_refl; eauto. + assert (EQ: (size bb - Z.of_nat (length_opt (exit bb))) = list_length_z (header bb)). + { rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. omega. } + rewrite EQ; eauto. + - exploit exec_body_simulation_plus; congruence || eauto. + { rewrite Hbb; eauto. } + intros (s2' & PLUS & MATCHI'). + eexists; split; eauto. + eapply plus_star; eauto. +Qed. + +Lemma exec_body_dont_move_PC bb rs m rs' m': forall + (BODY: exec_body lk ge (body bb) rs m = Next rs' m'), + rs PC = rs' PC. +Admitted. + +Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (NEMPTY_EXIT: exit bb <> None) + (MATCHI: match_internal (size bb - Z.of_nat (length_opt (exit bb))) (State rs m) s2) + (EXIT: exec_exit ge f (Ptrofs.repr (size bb)) rs m (exit bb) t rs' m') + (ATPC: rs PC = Vptr b ofs), + plus Asm.step tge s2 t (State rs' m'). +Admitted. + +Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (MATCHI: match_internal (size bb - Z.of_nat (length_opt (exit bb))) (State rs m) s2) + (EXIT: exec_exit ge f (Ptrofs.repr (size bb)) rs m (exit bb) t rs' m') + (ATPC: rs PC = Vptr b ofs), + star Asm.step tge s2 t (State rs' m'). +Proof. + intros. + destruct (exit bb) eqn: Hex. + - eapply plus_star. + eapply exec_exit_simulation_plus; try rewrite Hex; congruence || eauto. + - inv MATCHI. + inv EXIT. + assert (X: rs2 = incrPC (Ptrofs.repr (size bb)) rs). { admit. } + subst; eapply star_refl; eauto. +Admitted. + +Lemma exec_bblock_simulation b ofs f tf bb t rs m rs' m': forall + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (FINDtf : Genv.find_funct_ptr tge b = Some (Internal tf)) + (TRANSf : transf_function f = OK tf) + (EXECBB: exec_bblock lk ge f bb rs m t rs' m'), + plus Asm.step tge (State rs m) t (State rs' m'). +Proof. + intros; destruct EXECBB as (rs1 & m1 & BODY & CTL). + generalize TRANSf. + intros TRANS. + monadInv TRANS. + destruct (zlt _ _); try congruence. + inv EQ. inv EQ0. + exploit exec_header_simulation; eauto. + intros (s0 & STAR & MATCH0). + eapply star_plus_trans; traceEq || eauto. + destruct (bblock_non_empty bb). + - (* body bb <> nil *) + exploit exec_body_simulation_plus; eauto. + intros (s1 & PLUS & MATCH1). + eapply plus_star_trans; traceEq || eauto. + eapply exec_exit_simulation_star; eauto. + erewrite <- exec_body_dont_move_PC; eauto. + - (* exit bb <> None *) + exploit exec_body_simulation_star; eauto. + intros (s1 & STAR1 & MATCH1). + eapply star_plus_trans; traceEq || eauto. + eapply exec_exit_simulation_plus; eauto. + erewrite <- exec_body_dont_move_PC; eauto. +Qed. + +Lemma step_simulation s t s': + Asmblock.step lk ge s t s' -> plus Asm.step tge s t s'. Proof. - intros STEP s2 MATCH. + intros STEP. inv STEP; simpl; exploit functions_translated; eauto; intros (tf0 & FINDtf & TRANSf); monadInv TRANSf. - - (* internal step *) admit. + - (* internal step *) eapply exec_bblock_simulation; eauto. - (* external step *) - eexists; split. - + apply plus_one. - rewrite <- MATCH. - exploit external_call_symbols_preserved; eauto. apply senv_preserved. - intros ?. - eapply Asm.exec_step_external; eauto. - + econstructor; eauto. -Admitted. + apply plus_one. + exploit external_call_symbols_preserved; eauto. apply senv_preserved. + intros ?. + eapply Asm.exec_step_external; eauto. +Qed. Lemma transf_program_correct: forward_simulation (Asmblock.semantics lk prog) (Asm.semantics tprog). @@ -446,8 +588,11 @@ Proof. - apply senv_preserved. - eexact transf_initial_states. - eexact transf_final_states. - - (* TODO step_simulation *) admit. -Admitted. + - (* TODO step_simulation *) + unfold match_states. + simpl; intros; subst; eexists; split; eauto. + eapply step_simulation; eauto. +Qed. End PRESERVATION. |