From ffc27e4048ac3e963054de1ff27bb5387f259ad1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sun, 13 Dec 2020 14:08:04 +0100 Subject: Removing the PseudoAsm IR --- aarch64/Asmblockgenproof.v | 39 +++++++++++++++++++++++++++++---------- 1 file changed, 29 insertions(+), 10 deletions(-) (limited to 'aarch64/Asmblockgenproof.v') diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 41082772..bd96ff3b 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -5,8 +5,8 @@ CURRENTLY A STUB ! Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. -Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock IterList. -Require Import PseudoAsmblockproof Asmblockgen. +Require Import Op Locations Machblock Conventions Asmblock IterList. +Require Import Asmblockgen Asmblockgenproof0. Module MB := Machblock. Module AB := Asmblock. @@ -20,13 +20,8 @@ Proof. intros. eapply match_transform_partial_program; eauto. Qed. -Parameter next: MB.function -> Z -> Z. - Section PRESERVATION. -Lemma next_progress: forall (f:MB.function) (pos:Z), (pos < (next f pos))%Z. -Admitted. - Variable lk: aarch64_linker. Variable prog: Machblock.program. Variable tprog: Asmblock.program. @@ -38,15 +33,39 @@ Let tge := Genv.globalenv tprog. Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. -Lemma functions_bound_max_pos: forall fb f, +(*Lemma functions_bound_max_pos: forall fb f, Genv.find_funct_ptr ge fb = Some (Internal f) -> (max_pos next f) <= Ptrofs.max_unsigned. -Admitted. +Admitted.*) + +Lemma transf_function_no_overflow: + forall f tf, + transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned. +Proof. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. + omega. +Qed. +(** Existence of return addresses *) + +Lemma return_address_exists: + forall b f c, is_tail (b :: c) f.(MB.fn_code) -> + exists ra, return_address_offset f c ra. +Proof. + intros. eapply Asmblockgenproof0.return_address_exists; eauto. + +- intros. monadInv H0. + destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. monadInv EQ. simpl. + exists x; exists true; split; auto. + repeat constructor. +- exact transf_function_no_overflow. +Qed. +Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := + Asmblockgenproof0.return_address_offset. Lemma transf_program_correct: - forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics lk tprog). + forward_simulation (MB.semantics return_address_offset prog) (AB.semantics lk tprog). Admitted. End PRESERVATION. -- cgit