From f3a7611729bfc859280161add562351058c3994f Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 23 Oct 2020 14:41:09 +0200 Subject: Asm gen proof for aarch64 from Asmblock is complete. --- aarch64/Asmgenproof.v | 151 ++++++++++++-------------------------------------- 1 file changed, 35 insertions(+), 116 deletions(-) (limited to 'aarch64/Asmgenproof.v') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index eed185a0..f28bcb2e 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1413,7 +1413,7 @@ Proof. - rewrite <- Nat2Z.inj_le; eapply is_tail_bound; eauto. } exploit internal_functions_unfold; eauto. - intros (tc & FINDtf & TRANStf & _). + intros (tc & FINDtf & TRANStf & _). exploit find_basic_instructions_alt; eauto. intros (tbi & (bi & (NTHBI & TRANSBI & FIND_INSTR))). exploit is_tail_list_nth_z; eauto. @@ -1595,9 +1595,9 @@ Lemma header_size_cons_nil: forall (l0: label) (l1: list label) l1 = nil. Proof. intros. - destruct l1 as [l2|l1]; try congruence. rewrite !list_length_z_cons in HSIZE. - assert (list_length_z l2 >= 0) by eapply list_length_z_pos. - assert (list_length_z l2 + 1 + 1 >= 2) by omega. + destruct l1; try congruence. rewrite !list_length_z_cons in HSIZE. + assert (list_length_z l1 >= 0) by eapply list_length_z_pos. + assert (list_length_z l1 + 1 + 1 >= 2) by omega. assert (2 <= 1) by omega. contradiction H1. omega. Qed. @@ -1665,7 +1665,7 @@ Lemma next_inst_incr_pc_preserved bb rs1 m1 rs1' m1' rs2 m2 f tf: forall (BOUNDED: size bb <= Ptrofs.max_unsigned) (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)) (NEXT: Next (incrPC (Ptrofs.repr (size bb)) rs1) m2 = Next rs1' m1'), - exists (rs2' : regset) (m2' : mem), + exists (rs2' : regset) (m2' : mem), Next (Asm.nextinstr rs2) m2 = Next rs2' m2' /\ match_states (State rs1' m1') (State rs2' m2'). Proof. @@ -1930,11 +1930,14 @@ Proof. induction res; simpl; intros; unfold Pregmap.set; try rewrite AG; eauto. Qed. -Lemma set_builtin_res_dont_move_pc_gen res: forall vres rs _rs v +Lemma set_builtin_res_dont_move_pc_gen res: forall vres rs _rs v1 v2 + (HV: v1 = v2) (AG : forall r : preg, r <> PC -> rs r = _rs r), - (set_res res vres rs) # PC <- v = - (set_res res vres _rs) # PC <- v. + (set_res res vres rs) # PC <- v1 = + (set_res res vres _rs) # PC <- v2. Proof. + intros. rewrite HV. generalize res vres rs _rs AG v2. + clear res vres rs _rs AG v1 v2 HV. induction res. - simpl; intros. apply pc_both_sides; intros. unfold Pregmap.set; try rewrite AG; eauto. @@ -1953,13 +1956,16 @@ Proof. - intros; simpl in *. rewrite IHres2. rewrite IHres1. reflexivity. Qed. -(*Unset Printing Notations.*) -(*Lemma undef_map_preg_not_pc (l: list mreg): forall rs,*) - (*undef_regs (map preg_of l) rs PC = rs PC.*) -(*Proof.*) - (*induction l.*) - (*- simpl; reflexivity.*) - (*- simpl.*) +Lemma undef_reg_preserved (rl: list mreg): forall rs _rs r + (NPC: r <> PC) + (AG : forall r : preg, r <> PC -> rs r = _rs r), + undef_regs (map preg_of rl) rs r = undef_regs (map preg_of rl) _rs r. +Proof. + induction rl. + - simpl; auto. + - simpl; intros. erewrite IHrl; eauto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of a)); try rewrite AG; eauto. +Qed. Lemma undef_regs_other: forall r rl rs, @@ -2060,110 +2066,23 @@ Proof. - eapply eval_builtin_args_match; eauto. - inv MATCHI; eauto. - inv MATCHI. - (* TODO lemmas for set_res, undef_regs ... *) unfold Asm.nextinstr, incrPC. - (*induction res.*) - (*-- erewrite !set_builtin_map_not_pc.*) - - (*eapply set_builtin_res_dont_move_pc_gen.*) - - - assert (HPC: Val.offset_ptr (rs PC) (Ptrofs.repr (size bb)) - = Val.offset_ptr (_rs PC) Ptrofs.one). - { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. - rewrite Ptrofs.add_assoc. unfold Ptrofs.add. - assert (BBPOS: size bb >= 1) by eapply bblock_size_pos. - rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega. - rewrite Ptrofs.unsigned_one. - replace (size bb - 1 + 1) with (size bb) by omega. - reflexivity. } - - - - - - destruct destroyed_by_builtin. - -- unfold map. simpl. - induction res. - ++ simpl; intros. update_x_access_r; try congruence. - rewrite HPC. - apply (pc_both_sides (rs # x <- vres) (_rs # x <- vres) - (Val.offset_ptr (_rs PC) Ptrofs.one)); intros. - unfold Pregmap.set; try rewrite AG; eauto. - ++ simpl; intros. rewrite HPC. - apply pc_both_sides; eauto. - ++ simpl; intros. - erewrite !set_builtin_map_not_pc. rewrite HPC. - eapply set_builtin_res_dont_move_pc_gen; intros. - eapply set_buitin_res_sym; eauto. - -- simpl. - assert (HPC': (undef_regs (map preg_of l) - rs # (preg_of m) <- Vundef) PC = rs PC). - { erewrite undef_regs_other_2. - 2: eapply preg_notin_charact; intros; discriminate. - erewrite Pregmap.gso; eauto; try discriminate. } - - - ++ simpl. update_x_access_r; try discriminate. - ++ simpl. - assert (rs # (preg_of m) <- Vundef = _rs # (preg_of m) <- Vundef). - { destruct (PregEq.eq PC (preg_of m)). rewrite <- e. - { unfold Pregmap.set; apply functional_extensionality; intros. - destruct (PregEq.eq x PC); try rewrite AG; eauto. } - { unfold Pregmap.set; apply functional_extensionality; intros. - destruct (PregEq.eq x PC); try rewrite AG; eauto } - - rewrite (Pregmap.gso (i := PC) (j := (preg_of a)) Vundef (rs # (preg_of m) <- Vundef)). - rewrite IHl. update_x_access_r; try discriminate. - - (Ptrofs.repr (size bb)) - induction res. - ++ erewrite !set_builtin_map_not_pc. - - eapply set_builtin_res_dont_move_pc_gen. -erewrite !set_builtin_map_not_pc. - update_x_access_r; try congruence. - - - - all:admit. -Admitted. - -Lemma set_builtin_res_pc_overwrite res: forall (bb: bblock) vres rs _rs - (AG : forall r : preg, r <> PC -> rs r = _rs r) - (HPC : Val.offset_ptr (rs PC) (Ptrofs.repr (size bb)) = - Val.offset_ptr (_rs PC) Ptrofs.one), - (set_res (map_builtin_res DR res) vres rs) # PC <- - (Val.offset_ptr (set_res (map_builtin_res DR res) vres rs PC) - (Ptrofs.repr (size bb))) = - (set_res (map_builtin_res DR res) vres _rs) # PC <- - (Val.offset_ptr (set_res (map_builtin_res DR res) vres _rs PC) Ptrofs.one). -Proof. - induction res. - - simpl; intros. update_x_access_r; try congruence. rewrite HPC. - apply (pc_both_sides (rs # x <- vres) (_rs # x <- vres) (Val.offset_ptr (_rs PC) Ptrofs.one)); intros. unfold Pregmap.set; try rewrite AG; eauto. - - simpl; intros. rewrite HPC. - apply pc_both_sides; eauto. - - simpl; intros. - (*rewrite <- (IHres2 bb (Val.loword vres) rs (set_res (map_builtin_res DR res1) (Val.hiword vres) _rs)).*) - (*+ rewrite (IHres2 bb (Val.loword vres) (set_res (map_builtin_res DR res1) (Val.hiword vres) rs) _rs).*) - (** rewrite (IHres2 bb (Val.loword vres) rs _rs); eauto.*) - (** intros. induction res1. 3: { simpl.*) - - (*assert ((Val.offset_ptr*) - (*(set_res (map_builtin_res DR res2) (Val.loword vres)*) - (*(set_res (map_builtin_res DR res1) (Val.hiword vres) rs) PC)*) - (*(Ptrofs.repr (size bb))) =*) - (*(Val.offset_ptr*) - (*(set_res (map_builtin_res DR res2) (Val.loword vres)*) - (*(set_res (map_builtin_res DR res1) (Val.hiword vres) _rs) PC)*) - (*Ptrofs.one)). {*) - erewrite !set_builtin_map_not_pc. rewrite HPC. - eapply set_builtin_res_dont_move_pc_gen; intros. - eapply set_buitin_res_sym; eauto. + assert (HPC: Val.offset_ptr (rs PC) (Ptrofs.repr (size bb)) + = Val.offset_ptr (_rs PC) Ptrofs.one). + { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. + rewrite Ptrofs.add_assoc. unfold Ptrofs.add. + assert (BBPOS: size bb >= 1) by eapply bblock_size_pos. + rewrite (Ptrofs.unsigned_repr (size bb - 1)); try omega. + rewrite Ptrofs.unsigned_one. + replace (size bb - 1 + 1) with (size bb) by omega. + 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. + -- intros. eapply undef_reg_preserved; eauto. Qed. - 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) -- cgit