diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/Asm.v | 10 | ||||
| -rw-r--r-- | arm/Asmgen.v | 4 | ||||
| -rw-r--r-- | arm/Asmgenproof.v | 16 | ||||
| -rw-r--r-- | arm/SelectOp.vp | 2 | ||||
| -rw-r--r-- | arm/SelectOpproof.v | 2 |
5 files changed, 18 insertions, 16 deletions
@@ -84,8 +84,8 @@ Module Pregmap := EMap(PregEq). (** Conventional names for stack pointer ([SP]) and return address ([RA]) *) -Notation "'SP'" := IR13 (only parsing). -Notation "'RA'" := IR14 (only parsing). +Notation "'SP'" := IR13 (only parsing) : asm. +Notation "'RA'" := IR14 (only parsing) : asm. (** The instruction set. Most instructions correspond exactly to actual instructions of the ARM processor. See the ARM @@ -294,8 +294,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/arm/Asmgen.v b/arm/Asmgen.v index bbfad3c9..e7a3b4fa 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -23,8 +23,8 @@ Require Import Mach. Require Import Asm. Require Import Compopts. -Open Local Scope string_scope. -Open Local Scope error_monad_scope. +Local Open Scope string_scope. +Local Open Scope error_monad_scope. (** Extracting integer or float registers. *) diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index ade121c5..09c20d5c 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -852,8 +852,10 @@ Opaque loadind. - (* 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 (fn_code x0))); inversion EQ1. clear EQ1. + destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inversion EQ1. clear EQ1. subst x0. monadInv EQ0. + set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Pstr IR14 IR13 (SOimm (Ptrofs.to_int (fn_retaddr_ofs f))) :: x0) in *. + set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. @@ -865,12 +867,10 @@ Opaque loadind. set (rs2 := nextinstr (rs0#IR12 <- (parent_sp s) #IR13 <- (Vptr stk Ptrofs.zero))). set (rs3 := nextinstr rs2). assert (EXEC_PROLOGUE: - exec_straight tge x - (fn_code x) rs0 m' - x1 rs3 m3'). - replace (fn_code x) - with (Pallocframe (fn_stacksize f) (fn_link_ofs f) :: Pstr IR14 IR13 (SOimm (Ptrofs.to_int (fn_retaddr_ofs f))) :: x1) - by (rewrite <- H5; auto). + exec_straight tge tf + (fn_code tf) rs0 m' + x0 rs3 m3'). + change (fn_code tf) with tfbody; unfold tfbody. apply exec_straight_two with rs2 m2'. unfold exec_instr. rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). unfold Tptr, chunk_of_type, Archi.ptr64 in F. rewrite F. auto. @@ -884,7 +884,7 @@ Opaque loadind. econstructor; eauto. change (rs3 PC) with (Val.offset_ptr (Val.offset_ptr (rs0 PC) Ptrofs.one) Ptrofs.one). rewrite ATPC. simpl. constructor; eauto. - subst x. eapply code_tail_next_int. omega. + eapply code_tail_next_int. omega. eapply code_tail_next_int. omega. constructor. unfold rs3, rs2. apply agree_nextinstr. apply agree_nextinstr. diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp index 80a5d753..3d4e8661 100644 --- a/arm/SelectOp.vp +++ b/arm/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/arm/SelectOpproof.v b/arm/SelectOpproof.v index e520b3cf..dd194498 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -25,7 +25,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 *) |