From 4ec946cad316f6dc4299e19246a86dcb70dce64c Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 9 Oct 2020 15:47:28 +0200 Subject: exec_body_simulation without star' --- aarch64/Asmgenproof.v | 101 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 101 insertions(+) (limited to 'aarch64') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 4ee7c550..6b5b0913 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -967,6 +967,16 @@ Proof. generalize (list_length_z_aux_increase _ l1 2); omega. Qed. +Lemma eval_addressing_preserved a rs1 rs2: + (forall r : preg, r <> PC -> rs1 r = rs2 r) -> + eval_addressing lk a rs1 = Asm.eval_addressing tge a rs2. +Proof. + intros EQ. + destruct a; simpl; try (rewrite !EQ; congruence). auto. +Qed. + +Ltac next_stuck_cong := try (unfold Next, Stuck in *; congruence). + Lemma exec_basic_simulation: forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi (BASIC: exec_basic lk ge bi rs1 m1 = Next rs1' m1') @@ -975,6 +985,26 @@ Lemma exec_basic_simulation: exists rs2' m2', Asm.exec_instr tge tf tbi rs2 m2 = Next rs2' m2' /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + destruct bi. + 2: { + simpl in*. destruct ld. + { monadInv TRANSBI. destruct rd as [[r|]|]; try congruence. inversion EQ; subst. + simpl in *. unfold exec_load, Asm.exec_load in *. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + rewrite <- (eval_addressing_preserved a rs1 rs2); auto. + destruct (Mem.loadv _ _ _). + + inversion BASIC; auto. repeat (econstructor; eauto). + * intros. unfold Asm.nextinstr. rewrite (Pregmap.gso (i := r) (j := PC)); auto. + destruct (PregEq.eq r x). + { subst. rewrite !Pregmap.gss; auto. } + { rewrite !Pregmap.gso; auto. } + * unfold Asm.nextinstr. rewrite Pregmap.gss. rewrite !Pregmap.gso; try congruence. admit. + + next_stuck_cong. } + all:admit. + + } all:admit. Admitted. Lemma exec_body_simulation_star': forall @@ -1100,6 +1130,77 @@ Proof. rewrite H in H0; simpl in H0; repeat rewrite length_agree in H0; omega. Qed. +Lemma exec_body_simulation_plus_alt li: forall b ofs f bb rs m s2 rs' m' + (BLI: li = body bb) + (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'. +Proof. + induction li as [|a [|b]]; simpl. + - (* len(body bb) == 0 *) + congruence. + - (* len(body bb) == 1 *) + (* Contruct the MI hypothesis. *) + intros. rewrite <- BLI in *. simpl in *. + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & _). + assert (BDYLENPOS: (0 < length (body bb))%nat). { rewrite <- BLI; simpl; omega. } + exploit find_basic_instructions; eauto. + rewrite <- BLI; intros FINDBI. + destruct FINDBI as (i_next & (bi_next' & (NTHBI & TRANSBI & FIND_INSTR))). + inversion NTHBI; subst bi_next'. + destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong. + inversion BODY. subst. + destruct s as (rs1 & m1); simpl in *. + destruct s2 as (rs2 & m2); simpl in *. + exploit exec_basic_simulation; eauto. + intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). + + (* Code from the star' lemma bellow. We need this to exploit exec_step_internal. *) + exploit exec_basic_dont_move_PC; eauto. intros AGPC. + inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS']. + subst A. subst B. subst C. subst D. subst E. + rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT. + + inv MATCHI. symmetry in AGPC0. + rewrite ATPC in AGPC0. + unfold Val.offset_ptr in AGPC0. + simpl in FIND_INSTR; rewrite Z.add_0_r in FIND_INSTR. + + assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) + by (eapply size_of_blocks_bounds; eauto). + generalize (header_size_lt_block_size bb). rewrite length_agree; intros HEADER_LT. + generalize (Ptrofs.unsigned_range_2 ofs). intros (A & B). + + (* Execute internal step. *) + exploit (Asm.exec_step_internal tge b (Ptrofs.add ofs (Ptrofs.repr ((list_length_z (header bb))))) + {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |} + i_next rs2 m2); eauto. + { unfold Ptrofs.add. repeat (rewrite Ptrofs.unsigned_repr); + try rewrite length_agree; try split; try omega. + simpl; rewrite <- length_agree; assumption. } + + (* This is our STEP hypothesis. *) + intros STEP_NEXT. + + (* XXX New code --> no need to use the star' lemma this way. *) + eexists; split. + + apply plus_one. eauto. + + assert (BDYLEN: list_length_z (body bb) = 1). + { rewrite <- BLI. apply list_length_z_cons. } + assert (LEN1: size bb - Z.of_nat (length_opt (exit bb)) = list_length_z (header bb) + list_length_z (body bb)). + { rewrite bblock_size_aux. omega. } + rewrite BDYLEN in LEN1. rewrite LEN1. apply MI_NEXT. + - (* len(body bb) >= 1 *) + (* Comment factoriser le code pour éviter de répéter les étapes du ca précédent ? Utiliser une ltac serait trop lourd ? *) + +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)) -- cgit