From def0f40456a4fcf1c82a957a50a270a5a96319d1 Mon Sep 17 00:00:00 2001 From: Justus Fasse Date: Tue, 28 Jul 2020 09:38:51 +0200 Subject: Messy progress on exec_exit_simulation_plus Proves exec_exit_simulation_plus for cf_instruction (as opposed to builtins) --- aarch64/Asmgenproof.v | 30 +++++++++++++++++++++++++++--- 1 file changed, 27 insertions(+), 3 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 1412a3a4..b4dc08f6 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -759,13 +759,14 @@ Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall (ATPC: rs PC = Vptr b ofs), plus Asm.step tge s2 t (State rs' m'). Proof. - intros. apply plus_one. + intros. exploit internal_functions_unfold; eauto. intros (tc & FINDtf & TRANStf & _). exploit (find_instr_bblock (size bb - 1)); eauto. { generalize (bblock_size_pos bb). omega. } intros (i' & NTH & FIND_INSTR). + inv NTH. + rewrite last_instruction_cannot_be_label in *. discriminate. + destruct (exit bb) as [ctrl |] eqn:NEMPTY_EXIT'. 2: { contradiction. } @@ -775,11 +776,34 @@ Proof. list_length_z (header bb)) with (list_length_z (body bb)) in H by omega. rewrite list_nth_z_range_exceeded in H; try omega. discriminate. + destruct cfi. - * (* controlf low instruction *) + * (* control flow instruction *) + destruct s2. + rewrite H in EXIT. (* exit bb is a cfi *) + inv EXIT. + (* setup for exec_cfi_simulation *) + assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned). { + eapply size_of_blocks_bounds; eauto. + } + assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); omega. } + rewrite H in MATCHI. simpl in MATCHI. + exploit exec_cfi_simulation; eauto; intros. + (* extract exec_cfi_simulation's conclusion as separate hypotheses *) + destruct H4. destruct H4. destruct H4. rewrite H5. + inversion MATCHI. + apply plus_one. + eapply Asm.exec_step_internal; eauto. + - rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. eauto. + - simpl. replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) + with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption. + generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros. + unfold Ptrofs.add. + rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try omega. + rewrite Ptrofs.unsigned_repr; omega. + * (* builtin *) rewrite H in EXIT. inv EXIT. + destruct s2. admit. - * (* builtin *) admit. Admitted. Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall -- cgit