diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-07 15:52:58 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2010-03-07 15:52:58 +0000 |
commit | a74f6b45d72834b5b8417297017bd81424123d98 (patch) | |
tree | d291cf3f05397658f0fe9d8ecce9b8785a50d270 /powerpc | |
parent | 54cba6d4cae1538887f296a62be1c99378fe0916 (diff) | |
download | compcert-a74f6b45d72834b5b8417297017bd81424123d98.tar.gz compcert-a74f6b45d72834b5b8417297017bd81424123d98.zip |
Merge of the newmem and newextcalls branches:
- Revised memory model with concrete representation of ints & floats,
and per-byte access permissions
- Revised Globalenvs implementation
- Matching changes in all languages and proofs.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1282 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/Asm.v | 26 | ||||
-rw-r--r-- | powerpc/Asmgen.v | 8 | ||||
-rw-r--r-- | powerpc/Asmgenproof.v | 110 | ||||
-rw-r--r-- | powerpc/Asmgenproof1.v | 2 | ||||
-rw-r--r-- | powerpc/Asmgenretaddr.v | 2 | ||||
-rw-r--r-- | powerpc/ConstpropOpproof.v | 2 | ||||
-rw-r--r-- | powerpc/Op.v | 41 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 3 | ||||
-rw-r--r-- | powerpc/SelectOp.v | 2 | ||||
-rw-r--r-- | powerpc/SelectOpproof.v | 35 |
10 files changed, 122 insertions, 109 deletions
diff --git a/powerpc/Asm.v b/powerpc/Asm.v index 60c3d34d..fe6cf864 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -18,7 +18,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -126,7 +126,7 @@ Inductive instruction : Type := | Peqv: ireg -> ireg -> ireg -> instruction (**r bitwise not-xor *) | Pextsb: ireg -> ireg -> instruction (**r 8-bit sign extension *) | Pextsh: ireg -> ireg -> instruction (**r 16-bit sign extension *) - | Pfreeframe: int -> instruction (**r deallocate stack frame and restore previous frame *) + | Pfreeframe: Z -> Z -> int -> instruction (**r deallocate stack frame and restore previous frame *) | Pfabs: freg -> freg -> instruction (**r float absolute value *) | Pfadd: freg -> freg -> freg -> instruction (**r float addition *) | Pfcmpu: freg -> freg -> instruction (**r float comparison *) @@ -285,7 +285,7 @@ lbl: .long 0x43300000, 0x00000000 This cannot be expressed in our memory model, which does not reflect the fact that stack frames are adjacent and allocated/freed following a stack discipline. -- [Pfreeframe ofs]: in the formal semantics, this pseudo-instruction +- [Pfreeframe lo hi ofs]: in the formal semantics, this pseudo-instruction reads the word at offset [ofs] in the block pointed by [r1] (the stack pointer), frees this block, and sets [r1] to the value of the word at offset [ofs]. In the printed PowerPC assembly code, this @@ -349,7 +349,7 @@ Module Pregmap := EMap(PregEq). [Vzero] or [Vone]. *) Definition regset := Pregmap.t val. -Definition genv := Genv.t fundef. +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). @@ -651,12 +651,16 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome OK (nextinstr (rs#rd <- (Val.sign_ext 8 rs#r1))) m | Pextsh rd r1 => OK (nextinstr (rs#rd <- (Val.sign_ext 16 rs#r1))) m - | Pfreeframe ofs => + | Pfreeframe lo hi ofs => match Mem.loadv Mint32 m (Val.add rs#GPR1 (Vint ofs)) with | None => Error | Some v => match rs#GPR1 with - | Vptr stk ofs => OK (nextinstr (rs#GPR1 <- v)) (Mem.free m stk) + | Vptr stk ofs => + match Mem.free m stk lo hi with + | None => Error + | Some m' => OK (nextinstr (rs#GPR1 <- v)) m' + end | _ => Error end end @@ -874,23 +878,23 @@ Inductive step: state -> trace -> state -> Prop := exec_instr c i rs m = OK rs' m' -> step (State rs m) E0 (State rs' m') | exec_step_external: - forall b ef args res rs m t rs', + forall b ef args res rs m t rs' m', rs PC = Vptr b Int.zero -> Genv.find_funct_ptr ge b = Some (External ef) -> - event_match ef args t res -> + external_call ef args m t res m' -> extcall_arguments rs m ef.(ef_sig) args -> rs' = (rs#(loc_external_result ef.(ef_sig)) <- res #PC <- (rs LR)) -> - step (State rs m) t (State rs' m). + step (State rs m) t (State rs' m'). End RELSEM. (** Execution of whole programs. *) Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: + | initial_state_intro: forall m0, + Genv.init_mem p = Some m0 -> let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in let rs0 := (Pregmap.init Vundef) # PC <- (symbol_offset ge p.(prog_main) Int.zero) diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 2c65ca4d..ca42d563 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -19,7 +19,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Op. Require Import Locations. @@ -487,12 +487,12 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := Pmtctr (ireg_of r) :: Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR12 :: - Pfreeframe f.(fn_link_ofs) :: + Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbctr :: k | Mtailcall sig (inr symb) => Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR12 :: - Pfreeframe f.(fn_link_ofs) :: + Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pbs symb :: k | Mlabel lbl => Plabel lbl :: k @@ -508,7 +508,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) (k: code) := | Mreturn => Plwz GPR12 (Cint f.(fn_retaddr_ofs)) GPR1 :: Pmtlr GPR12 :: - Pfreeframe f.(fn_link_ofs) :: + Pfreeframe (-f .(fn_framesize)) f.(fn_stacksize) f.(fn_link_ofs) :: Pblr :: k end. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index a2fc6108..5be47347 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -19,7 +19,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -55,7 +55,7 @@ Lemma functions_translated: Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = Errors.OK tf. Proof - (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF). + (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). Lemma functions_transl: forall f b, @@ -776,13 +776,25 @@ Proof. rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. Qed. +Remark loadv_8_signed_unsigned: + forall m a v, + Mem.loadv Mint8signed m a = Some v -> + exists v', Mem.loadv Mint8unsigned m a = Some v' /\ v = Val.sign_ext 8 v'. +Proof. + unfold Mem.loadv; intros. destruct a; try congruence. + generalize (Mem.load_int8_signed_unsigned m b (Int.signed i)). + rewrite H. destruct (Mem.load Mint8unsigned m b (Int.signed i)). + simpl; intros. exists v0; split; congruence. + simpl; congruence. +Qed. + Lemma exec_Mload_prop: forall (s : list stackframe) (fb : block) (sp : val) (chunk : memory_chunk) (addr : addressing) (args : list mreg) (dst : mreg) (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (a v : val), eval_addressing ge sp addr ms ## args = Some a -> - loadv chunk m a = Some v -> + Mem.loadv chunk m a = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mload chunk addr args dst :: c) ms m) E0 (Machconcr.State s fb sp c (Regmap.set dst v ms) m). Proof. @@ -797,11 +809,7 @@ Proof. try (eapply transl_load_correct; eauto; intros; simpl; unfold preg_of; rewrite H6; auto). (* Mint8signed *) - generalize (loadv_8_signed_unsigned m a). - rewrite H0. - caseEq (loadv Mint8unsigned m a); - [idtac | simpl;intros;discriminate]. - intros v' LOAD' EQ. simpl in EQ. injection EQ. intro EQ1. clear EQ. + exploit loadv_8_signed_unsigned; eauto. intros [v' [LOAD EQ]]. assert (X1: forall (cst : constant) (r1 : ireg) (rs1 : regset), exec_instr tge (transl_function f) (Plbz (ireg_of dst) cst r1) rs1 m = load1 tge Mint8unsigned (preg_of dst) cst r1 rs1 m). @@ -815,30 +823,46 @@ Proof. Mint8unsigned addr args (Pextsb (ireg_of dst) (ireg_of dst) :: transl_code f c) ms sp rs m dst a v' - X1 X2 AG H3 H7 LOAD'). + X1 X2 AG H3 H7 LOAD). intros [rs2 [EX1 AG1]]. exists (nextinstr (rs2#(ireg_of dst) <- v)). split. eapply exec_straight_trans. eexact EX1. apply exec_straight_one. simpl. rewrite <- (ireg_val _ _ _ dst AG1);auto. rewrite Regmap.gss. - rewrite EQ1. reflexivity. reflexivity. + rewrite EQ. reflexivity. reflexivity. eauto with ppcgen. Qed. +Lemma storev_8_signed_unsigned: + forall m a v, + Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. +Proof. + intros. unfold Mem.storev. destruct a; auto. + apply Mem.store_signed_unsigned_8. +Qed. + +Lemma storev_16_signed_unsigned: + forall m a v, + Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. +Proof. + intros. unfold Mem.storev. destruct a; auto. + apply Mem.store_signed_unsigned_16. +Qed. + Lemma exec_Mstore_prop: forall (s : list stackframe) (fb : block) (sp : val) (chunk : memory_chunk) (addr : addressing) (args : list mreg) (src : mreg) (c : list Mach.instruction) (ms : mreg -> val) (m m' : mem) (a : val), eval_addressing ge sp addr ms ## args = Some a -> - storev chunk m a (ms src) = Some m' -> + Mem.storev chunk m a (ms src) = Some m' -> exec_instr_prop (Machconcr.State s fb sp (Mstore chunk addr args src :: c) ms m) E0 (Machconcr.State s fb sp c ms m'). Proof. intros; red; intros; inv MS. generalize (wt_function_instrs _ WTF _ (INCL _ (in_eq _ _))). intro WTI; inversion WTI. - rewrite <- (eval_addressing_preserved symbols_preserved) in H. + rewrite <- (eval_addressing_preserved _ _ symbols_preserved) in H. left; eapply exec_straight_steps; eauto with coqlib. destruct chunk; simpl; simpl in H6; try (rewrite storev_8_signed_unsigned in H0); @@ -928,14 +952,15 @@ Qed. Lemma exec_Mtailcall_prop: forall (s : list stackframe) (fb stk : block) (soff : int) (sig : signature) (ros : mreg + ident) (c : list Mach.instruction) - (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block), + (ms : Mach.regset) (m : mem) (f: Mach.function) (f' : block) m', find_function_ptr ge ros ms = Some f' -> Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mtailcall sig ros :: c) ms m) E0 - (Callstate s f' ms (free m stk)). + (Callstate s f' ms m'). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. @@ -953,9 +978,9 @@ Proof. set (rs6 := rs5#PC <- (rs5 CTR)). assert (exec_straight tge (transl_function f) (transl_code f (Mtailcall sig (inl ident m0) :: c)) rs m - (Pbctr :: transl_code f c) rs5 (free m stk)). + (Pbctr :: transl_code f c) rs5 m'). simpl. apply exec_straight_step with rs2 m. - simpl. rewrite <- (ireg_val _ _ _ _ AG H6). reflexivity. reflexivity. + simpl. rewrite <- (ireg_val _ _ _ _ AG H7). reflexivity. reflexivity. apply exec_straight_step with rs3 m. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. change (rs2 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). @@ -966,13 +991,13 @@ Proof. apply exec_straight_one. simpl. change (rs4 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). unfold load_stack in H1; simpl in H1. - simpl. rewrite H1. reflexivity. reflexivity. - left; exists (State rs6 (free m stk)); split. + simpl. rewrite H1. rewrite H3. reflexivity. reflexivity. + left; exists (State rs6 m'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone) Vone). - rewrite <- H7; simpl. eauto. + rewrite <- H8; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. @@ -983,7 +1008,7 @@ Proof. unfold rs4, rs3, rs2; auto 10 with ppcgen. assert (AG5: agree ms (parent_sp s) rs5). unfold rs5. apply agree_nextinstr. - split. reflexivity. intros. inv AG4. rewrite H12. + split. reflexivity. intros. inv AG4. rewrite H13. rewrite Pregmap.gso; auto with ppcgen. unfold rs6; auto with ppcgen. change (rs6 PC) with (ms m0). @@ -996,7 +1021,7 @@ Proof. set (rs5 := rs4#PC <- (Vptr f' Int.zero)). assert (exec_straight tge (transl_function f) (transl_code f (Mtailcall sig (inr mreg i) :: c)) rs m - (Pbs i :: transl_code f c) rs4 (free m stk)). + (Pbs i :: transl_code f c) rs4 m'). simpl. apply exec_straight_step with rs2 m. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. rewrite <- (sp_val _ _ _ AG). @@ -1007,13 +1032,13 @@ Proof. apply exec_straight_one. simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). unfold load_stack in H1; simpl in H1. - simpl. rewrite H1. reflexivity. reflexivity. - left; exists (State rs5 (free m stk)); split. + simpl. rewrite H1. rewrite H3. reflexivity. reflexivity. + left; exists (State rs5 m'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite <- H7; simpl. eauto. + rewrite <- H8; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. @@ -1025,7 +1050,7 @@ Proof. unfold rs3, rs2; auto 10 with ppcgen. assert (AG4: agree ms (parent_sp s) rs4). unfold rs4. apply agree_nextinstr. - split. reflexivity. intros. inv AG3. rewrite H12. + split. reflexivity. intros. inv AG3. rewrite H13. rewrite Pregmap.gso; auto with ppcgen. unfold rs5; auto with ppcgen. Qed. @@ -1191,12 +1216,13 @@ Qed. Lemma exec_Mreturn_prop: forall (s : list stackframe) (fb stk : block) (soff : int) - (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function), + (c : list Mach.instruction) (ms : Mach.regset) (m : mem) (f: Mach.function) m', Genv.find_funct_ptr ge fb = Some (Internal f) -> load_stack m (Vptr stk soff) Tint f.(fn_link_ofs) = Some (parent_sp s) -> load_stack m (Vptr stk soff) Tint f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk (- f.(fn_framesize)) f.(fn_stacksize) = Some m' -> exec_instr_prop (Machconcr.State s fb (Vptr stk soff) (Mreturn :: c) ms m) E0 - (Returnstate s ms (free m stk)). + (Returnstate s ms m'). Proof. intros; red; intros; inv MS. assert (f0 = f) by congruence. subst f0. @@ -1206,7 +1232,7 @@ Proof. set (rs5 := rs4#PC <- (parent_ra s)). assert (exec_straight tge (transl_function f) (transl_code f (Mreturn :: c)) rs m - (Pblr :: transl_code f c) rs4 (free m stk)). + (Pblr :: transl_code f c) rs4 m'). simpl. apply exec_straight_three with rs2 m rs3 m. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. unfold load_stack in H1. simpl in H1. @@ -1216,18 +1242,18 @@ Proof. simpl. change (rs3 GPR1) with (rs GPR1). rewrite <- (sp_val _ _ _ AG). simpl. unfold load_stack in H0. simpl in H0. - rewrite H0. reflexivity. + rewrite H0. rewrite H2. reflexivity. reflexivity. reflexivity. reflexivity. - left; exists (State rs5 (free m stk)); split. + left; exists (State rs5 m'); split. (* execution *) - apply plus_right' with E0 (State rs4 (free m stk)) E0. + apply plus_right' with E0 (State rs4 m') E0. eapply exec_straight_exec; eauto. inv AT. econstructor. change (rs4 PC) with (Val.add (Val.add (Val.add (rs PC) Vone) Vone) Vone). - rewrite <- H3. simpl. eauto. + rewrite <- H4. simpl. eauto. apply functions_transl; eauto. - generalize (functions_transl_no_overflow _ _ H4); intro NOOV. - simpl in H5. eapply find_instr_tail. + generalize (functions_transl_no_overflow _ _ H5); intro NOOV. + simpl in H6. eapply find_instr_tail. eapply code_tail_next_int; auto. eapply code_tail_next_int; auto. eapply code_tail_next_int; eauto. @@ -1249,7 +1275,7 @@ Lemma exec_function_internal_prop: forall (s : list stackframe) (fb : block) (ms : Mach.regset) (m : mem) (f : function) (m1 m2 m3 : mem) (stk : block), Genv.find_funct_ptr ge fb = Some (Internal f) -> - alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) -> + Mem.alloc m (- fn_framesize f) (fn_stacksize f) = (m1, stk) -> let sp := Vptr stk (Int.repr (- fn_framesize f)) in store_stack m1 sp Tint f.(fn_link_ofs) (parent_sp s) = Some m2 -> store_stack m2 sp Tint f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> @@ -1258,7 +1284,7 @@ Lemma exec_function_internal_prop: Proof. intros; red; intros; inv MS. assert (WTF: wt_function f). - generalize (Genv.find_funct_ptr_prop wt_fundef wt_prog H); intro TY. + generalize (Genv.find_funct_ptr_prop wt_fundef _ _ wt_prog H); intro TY. inversion TY; auto. exploit functions_transl; eauto. intro TFIND. generalize (functions_transl_no_overflow _ _ H); intro NOOV. @@ -1307,19 +1333,19 @@ Qed. Lemma exec_function_external_prop: forall (s : list stackframe) (fb : block) (ms : Mach.regset) (m : mem) (t0 : trace) (ms' : RegEq.t -> val) - (ef : external_function) (args : list val) (res : val), + (ef : external_function) (args : list val) (res : val) (m': mem), Genv.find_funct_ptr ge fb = Some (External ef) -> - event_match ef args t0 res -> + external_call ef args m t0 res m' -> Machconcr.extcall_arguments ms m (parent_sp s) (ef_sig ef) args -> ms' = Regmap.set (Conventions.loc_result (ef_sig ef)) res ms -> exec_instr_prop (Machconcr.Callstate s fb ms m) - t0 (Machconcr.Returnstate s ms' m). + t0 (Machconcr.Returnstate s ms' m'). Proof. intros; red; intros; inv MS. exploit functions_translated; eauto. intros [tf [A B]]. simpl in B. inv B. left; exists (State (rs#(loc_external_result (ef_sig ef)) <- res #PC <- (rs LR)) - m); split. + m'); split. apply plus_one. eapply exec_step_external; eauto. eapply extcall_arguments_match; eauto. econstructor; eauto. @@ -1367,14 +1393,14 @@ Proof. intros. inversion H. unfold ge0 in *. econstructor; split. econstructor. + eapply Genv.init_mem_transf_partial; eauto. replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) with (Vptr fb Int.zero). - rewrite (Genv.init_mem_transf_partial _ _ TRANSF). econstructor; eauto. constructor. split. auto. intros. repeat rewrite Pregmap.gso; auto with ppcgen. unfold symbol_offset. rewrite (transform_partial_program_main _ _ TRANSF). - rewrite symbols_preserved. unfold ge; rewrite H0. auto. + rewrite symbols_preserved. unfold ge; rewrite H1. auto. Qed. Lemma transf_final_states: diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 7329e539..60c49690 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -18,7 +18,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Op. Require Import Locations. diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v index d414752c..d55635b1 100644 --- a/powerpc/Asmgenretaddr.v +++ b/powerpc/Asmgenretaddr.v @@ -22,7 +22,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Op. Require Import Locations. diff --git a/powerpc/ConstpropOpproof.v b/powerpc/ConstpropOpproof.v index 2e28d23f..b5e2e8ee 100644 --- a/powerpc/ConstpropOpproof.v +++ b/powerpc/ConstpropOpproof.v @@ -17,7 +17,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Op. Require Import Registers. diff --git a/powerpc/Op.v b/powerpc/Op.v index c6e196f3..7a9aa500 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -29,7 +29,8 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memdata. +Require Import Memory. Require Import Globalenvs. Set Implicit Arguments. @@ -182,7 +183,7 @@ Definition offset_sp (sp: val) (delta: int) : option val := end. Definition eval_operation - (F: Type) (genv: Genv.t F) (sp: val) + (F V: Type) (genv: Genv.t F V) (sp: val) (op: operation) (vl: list val): option val := match op, vl with | Omove, v1::nil => Some v1 @@ -265,7 +266,7 @@ Definition eval_operation end. Definition eval_addressing - (F: Type) (genv: Genv.t F) (sp: val) + (F V: Type) (genv: Genv.t F V) (sp: val) (addr: addressing) (vl: list val) : option val := match addr, vl with | Aindexed n, Vptr b1 n1 :: nil => @@ -360,9 +361,9 @@ Qed. Section GENV_TRANSF. -Variable F1 F2: Type. -Variable ge1: Genv.t F1. -Variable ge2: Genv.t F2. +Variable F1 F2 V1 V2: Type. +Variable ge1: Genv.t F1 V1. +Variable ge2: Genv.t F2 V2. Hypothesis agree_on_symbols: forall (s: ident), Genv.find_symbol ge2 s = Genv.find_symbol ge1 s. @@ -480,25 +481,14 @@ Definition type_of_addressing (addr: addressing) : list typ := | Ainstack _ => nil end. -Definition type_of_chunk (c: memory_chunk) : typ := - match c with - | Mint8signed => Tint - | Mint8unsigned => Tint - | Mint16signed => Tint - | Mint16unsigned => Tint - | Mint32 => Tint - | Mfloat32 => Tfloat - | Mfloat64 => Tfloat - end. - (** Weak type soundness results for [eval_operation]: the result values, when defined, are always of the type predicted by [type_of_operation]. *) Section SOUNDNESS. -Variable A: Type. -Variable genv: Genv.t A. +Variable A V: Type. +Variable genv: Genv.t A V. Lemma type_of_operation_sound: forall op vl sp v, @@ -548,8 +538,7 @@ Proof. destruct v; destruct chunk; exact I. intros until v. unfold Mem.loadv. destruct addr; intros; try discriminate. - generalize (Mem.load_inv _ _ _ _ _ H0). - intros [X Y]. subst v. apply H. + eapply Mem.load_type; eauto. Qed. End SOUNDNESS. @@ -560,8 +549,8 @@ End SOUNDNESS. Section EVAL_OP_TOTAL. -Variable F: Type. -Variable genv: Genv.t F. +Variable F V: Type. +Variable genv: Genv.t F V. Definition find_symbol_offset (id: ident) (ofs: int) : val := match Genv.find_symbol genv id with @@ -746,8 +735,8 @@ End EVAL_OP_TOTAL. Section EVAL_LESSDEF. -Variable F: Type. -Variable genv: Genv.t F. +Variable F V: Type. +Variable genv: Genv.t F V. Ltac InvLessdef := match goal with @@ -834,7 +823,7 @@ End EVAL_LESSDEF. Definition op_for_binary_addressing (addr: addressing) : operation := Oadd. Lemma eval_op_for_binary_addressing: - forall (F: Type) (ge: Genv.t F) sp addr args v, + forall (F V: Type) (ge: Genv.t F V) sp addr args v, (length args >= 2)%nat -> eval_addressing ge sp addr args = Some v -> eval_operation ge sp (op_for_binary_addressing addr) args = Some v. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 10170f9e..a1e5afe3 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -288,7 +288,8 @@ let print_instruction oc labels = function fprintf oc " extsb %a, %a\n" ireg r1 ireg r2 | Pextsh(r1, r2) -> fprintf oc " extsh %a, %a\n" ireg r1 ireg r2 - | Pfreeframe ofs -> + | Pfreeframe(lo, hi, ofs) -> + (* Note: could also do an add on GPR1 using lo and hi *) fprintf oc " lwz %a, %ld(%a)\n" ireg GPR1 (camlint_of_coqint ofs) ireg GPR1 | Pfabs(r1, r2) -> fprintf oc " fabs %a, %a\n" freg r1 freg r2 diff --git a/powerpc/SelectOp.v b/powerpc/SelectOp.v index 2f4d76e5..d03645ef 100644 --- a/powerpc/SelectOp.v +++ b/powerpc/SelectOp.v @@ -42,7 +42,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Cminor. Require Import Op. diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 2736e9e9..d4a45dab 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -18,7 +18,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -657,25 +657,18 @@ Qed. Lemma loadv_cast: forall chunk addr v, - loadv chunk m addr = Some v -> + Mem.loadv chunk m addr = Some v -> match chunk with - | Mint8signed => loadv chunk m addr = Some(Val.sign_ext 8 v) - | Mint8unsigned => loadv chunk m addr = Some(Val.zero_ext 8 v) - | Mint16signed => loadv chunk m addr = Some(Val.sign_ext 16 v) - | Mint16unsigned => loadv chunk m addr = Some(Val.zero_ext 16 v) - | Mfloat32 => loadv chunk m addr = Some(Val.singleoffloat v) + | Mint8signed => v = Val.sign_ext 8 v + | Mint8unsigned => v = Val.zero_ext 8 v + | Mint16signed => v = Val.sign_ext 16 v + | Mint16unsigned => v = Val.zero_ext 16 v + | Mfloat32 => v = Val.singleoffloat v | _ => True end. Proof. - intros. rewrite H. destruct addr; simpl in H; try discriminate. - exploit Mem.load_inv; eauto. - set (v' := (getN (pred_size_chunk chunk) (Int.signed i) (contents (blocks m b)))). - intros [A B]. subst v. destruct chunk; auto; destruct v'; simpl; auto. - rewrite Int.sign_ext_idem; auto. compute; auto. - rewrite Int.zero_ext_idem; auto. compute; auto. - rewrite Int.sign_ext_idem; auto. compute; auto. - rewrite Int.zero_ext_idem; auto. compute; auto. - rewrite Float.singleoffloat_idem; auto. + intros. destruct addr; simpl in H; try discriminate. + eapply Mem.load_cast. eauto. Qed. Theorem eval_cast8signed: @@ -686,7 +679,7 @@ Proof. intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.sign_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. @@ -698,7 +691,7 @@ Proof. intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.zero_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. @@ -710,7 +703,7 @@ Proof. intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.sign_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. @@ -722,7 +715,7 @@ Proof. intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.zero_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. @@ -733,7 +726,7 @@ Theorem eval_singleoffloat: Proof. intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. |