diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Asm.v | 10 | ||||
| -rw-r--r-- | powerpc/Asmgen.v | 4 | ||||
| -rw-r--r-- | powerpc/Asmgenproof.v | 19 | ||||
| -rw-r--r-- | powerpc/SelectOp.vp | 2 | ||||
| -rw-r--r-- | powerpc/SelectOpproof.v | 2 |
5 files changed, 23 insertions, 14 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 3c269083..cc554eb1 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -87,8 +87,8 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) -Notation "'SP'" := GPR1 (only parsing). -Notation "'RA'" := LR (only parsing). +Notation "'SP'" := GPR1 (only parsing) : asm. +Notation "'RA'" := LR (only parsing) : asm. (** Symbolic constants. Immediate operands to an arithmetic instruction or an indexed memory access can be either integer literals, @@ -385,8 +385,10 @@ Definition program := AST.program fundef unit. Definition regset := Pregmap.t val. Definition genv := Genv.t fundef unit. -Notation "a # b" := (a b) (at level 1, only parsing). -Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level). +Notation "a # b" := (a b) (at level 1, only parsing) : asm. +Notation "a # b <- c" := (Pregmap.set b c a) (at level 1, b at next level) : asm. + +Open Scope asm. (** Undefining some registers *) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 799d208e..fc04b15d 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -22,8 +22,8 @@ Require Import Locations. Require Import Mach. Require Import Asm. -Open Local Scope string_scope. -Open Local Scope error_monad_scope. +Local Open Scope string_scope. +Local Open Scope error_monad_scope. (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 447a53a0..6f0390b9 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -876,7 +876,7 @@ Local Transparent destroyed_by_jumptable. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. + destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. @@ -887,15 +887,23 @@ Local Transparent destroyed_by_jumptable. intros [m3' [P Q]]. (* Execution of function prologue *) monadInv EQ0. rewrite transl_code'_transl_code in EQ1. + set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) + (fn_retaddr_ofs f) + :: Pmflr GPR0 + :: Pstw GPR0 (Cint (Ptrofs.to_int (fn_retaddr_ofs f))) + GPR1 + :: Pcfi_rel_offset + (Ptrofs.to_int (fn_retaddr_ofs f)) :: x0) in *. + set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)). set (rs3 := nextinstr (rs2#GPR0 <- (rs0#LR))). set (rs4 := nextinstr rs3). set (rs5 := nextinstr rs4). assert (EXEC_PROLOGUE: - exec_straight tge x - x.(fn_code) rs0 m' - x1 rs5 m3'). - rewrite <- H5 at 2. simpl. + exec_straight tge tf + tf.(fn_code) rs0 m' + x0 rs5 m3'). + change (fn_code tf) with tfbody; unfold tfbody. apply exec_straight_step with rs2 m2'. unfold exec_instr. rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite F. auto. auto. @@ -911,7 +919,6 @@ Local Transparent destroyed_by_jumptable. econstructor; eauto. change (rs5 PC) with (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one) Ptrofs.one) Ptrofs.one). rewrite ATPC. simpl. constructor; eauto. - subst x; simpl in g. unfold fn_code. eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. diff --git a/powerpc/SelectOp.vp b/powerpc/SelectOp.vp index 79f05295..b5e3ed7e 100644 --- a/powerpc/SelectOp.vp +++ b/powerpc/SelectOp.vp @@ -44,7 +44,7 @@ Require Import Floats. Require Import Op. Require Import CminorSel. -Open Local Scope cminorsel_scope. +Local Open Scope cminorsel_scope. (** ** Constants **) diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index e31e847a..548fbce2 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -26,7 +26,7 @@ Require Import Op. Require Import CminorSel. Require Import SelectOp. -Open Local Scope cminorsel_scope. +Local Open Scope cminorsel_scope. Local Transparent Archi.ptr64. (** * Useful lemmas and tactics *) |