diff options
author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-23 11:58:19 +0200 |
---|---|---|
committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-07-23 11:58:19 +0200 |
commit | 8289c850a9e24406e8ce34cf3a0d53840ce02903 (patch) | |
tree | 07d4aea1ba1f4810193967ac998f8477fb33a19a | |
parent | a42119b0149f887fc109c607ea13c647f920022e (diff) | |
download | compcert-kvx-8289c850a9e24406e8ce34cf3a0d53840ce02903.tar.gz compcert-kvx-8289c850a9e24406e8ce34cf3a0d53840ce02903.zip |
proof of exec_header_simulation
-rw-r--r-- | aarch64/Asmgenproof.v | 101 |
1 files changed, 91 insertions, 10 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 2f05355f..4a1f4de4 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -89,6 +89,26 @@ Proof. eauto. Qed. +Lemma internal_functions_unfold: + forall b f, + Genv.find_funct_ptr ge b = Some (Internal f) -> + exists tc, + Genv.find_funct_ptr tge b = Some (Internal (Asm.mkfunction (fn_sig f) tc)) + /\ unfold (fn_blocks f) = OK tc + /\ list_length_z tc <= Ptrofs.max_unsigned. +Proof. + intros. + exploit internal_functions_translated; eauto. + intros (tf & FINDtf & TRANStf). + unfold transf_function in TRANStf. + monadInv TRANStf. + destruct (zlt _ _); try congruence. + inv EQ. inv EQ0. + eexists; intuition eauto. + omega. +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 -> @@ -104,7 +124,7 @@ Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop := i = control_to_instruction cfi -> is_nth_inst bb n i. -Lemma find_instr_bblock pos n lb tlb bb: +Lemma find_instr_bblock n pos lb tlb bb: find_bblock pos lb = Some bb -> unfold lb = OK tlb -> 0 <= n < size bb -> @@ -233,6 +253,7 @@ Proof. unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega. Qed. +(* NB: does not seem useful anymore, with the [exec_header_simulation] proof below Lemma match_internal_exec_label: forall n rs1 m1 rs2 m2 l fb f tf, Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -260,6 +281,7 @@ Proof. * apply Z.ge_le; assumption. * rewrite <- functions_bound_max_pos; eauto; omega. Qed. +*) Lemma incrPC_agree_but_pc: forall rs r ofs, @@ -463,16 +485,82 @@ Proof. - left. discriminate. Qed. +Lemma list_length_z_aux_increase A (l: list A): forall acc, + list_length_z_aux l acc >= acc. +Proof. + induction l; simpl; intros. + - omega. + - generalize (IHl (Z.succ acc)). omega. +Qed. + +Lemma bblock_size_aux_pos bb: list_length_z (body bb) + Z.of_nat (length_opt (exit bb)) >= 1. +Admitted. (* NB: from bblock_non_empty *) + 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 bblock_size_pos bb: size bb >= 1. +Proof. + rewrite (bblock_size_aux bb). + generalize (bblock_size_aux_pos bb). + generalize (list_length_z_pos (header bb)). + omega. +Qed. + +Lemma size_header b pos f bb: forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock pos (fn_blocks f) = Some bb), + list_length_z (header bb) <= 1. +Admitted. + +Lemma list_nth_z_neg A (l: list A): forall n, + n < 0 -> list_nth_z l n = None. +Proof. + induction l; simpl; auto. + intros n H; destruct (zeq _ _); (try eapply IHl); omega. +Qed. + + 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. +Proof. + intros. + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & _). + assert (BNDhead: list_length_z (header bb) <= 1). { eapply size_header; eauto. } + destruct (header bb) as [|l[|]] eqn: EQhead. + + (* header nil *) + eexists; split. + - eapply star_refl. + - split; eauto. + unfold list_length_z; rewrite !ATPC; simpl. + rewrite Ptrofs.add_zero; auto. + + (* header one *) + assert (Lhead: list_length_z (header bb) = 1). { rewrite EQhead; unfold list_length_z; simpl. auto. } + exploit (find_instr_bblock 0); eauto. + { generalize (bblock_size_pos bb). omega. } + intros (i & NTH & FIND_INSTR). + inv NTH. + * rewrite EQhead in H; simpl in H. inv H. + cutrewrite (Ptrofs.unsigned ofs + 0 = Ptrofs.unsigned ofs) in FIND_INSTR; try omega. + eexists. split. + - eapply star_one. + eapply Asm.exec_step_internal; eauto. + simpl; eauto. + - unfold list_length_z; simpl. split; eauto. + intros r; destruct r; simpl; congruence || auto. + * (* absurd case *) + erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; omega]. + * (* absurd case *) + rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). omega. + + (* absurd case *) + unfold list_length_z in BNDhead. simpl in *. + generalize (list_length_z_aux_increase _ l1 2); omega. +Qed. Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall (ATPC: rs PC = Vptr b ofs) @@ -550,21 +638,14 @@ Proof. subst; eapply star_refl; eauto. Qed. -Lemma exec_bblock_simulation b ofs f tf bb t rs m rs' m': forall +Lemma exec_bblock_simulation b ofs f 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. |