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 /backend | |
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 'backend')
-rw-r--r-- | backend/Allocproof.v | 23 | ||||
-rw-r--r-- | backend/CSE.v | 4 | ||||
-rw-r--r-- | backend/CSEproof.v | 51 | ||||
-rw-r--r-- | backend/Cminor.v | 65 | ||||
-rw-r--r-- | backend/CminorSel.v | 34 | ||||
-rw-r--r-- | backend/Constpropproof.v | 57 | ||||
-rw-r--r-- | backend/LTL.v | 24 | ||||
-rw-r--r-- | backend/LTLin.v | 28 | ||||
-rw-r--r-- | backend/LTLintyping.v | 1 | ||||
-rw-r--r-- | backend/LTLtyping.v | 1 | ||||
-rw-r--r-- | backend/Linear.v | 30 | ||||
-rw-r--r-- | backend/Linearizeproof.v | 24 | ||||
-rw-r--r-- | backend/Lineartyping.v | 1 | ||||
-rw-r--r-- | backend/Mach.v | 4 | ||||
-rw-r--r-- | backend/Machabstr.v | 24 | ||||
-rw-r--r-- | backend/Machabstr2concr.v | 669 | ||||
-rw-r--r-- | backend/Machconcr.v | 22 | ||||
-rw-r--r-- | backend/Machtyping.v | 24 | ||||
-rw-r--r-- | backend/RTL.v | 140 | ||||
-rw-r--r-- | backend/RTLgenproof.v | 132 | ||||
-rw-r--r-- | backend/RTLgenspec.v | 2 | ||||
-rw-r--r-- | backend/RTLtyping.v | 36 | ||||
-rw-r--r-- | backend/RTLtypingaux.ml | 1 | ||||
-rw-r--r-- | backend/Reloadproof.v | 55 | ||||
-rw-r--r-- | backend/Selection.v | 2 | ||||
-rw-r--r-- | backend/Selectionproof.v | 17 | ||||
-rw-r--r-- | backend/Stackingproof.v | 29 | ||||
-rw-r--r-- | backend/Tailcallproof.v | 280 | ||||
-rw-r--r-- | backend/Tunnelingproof.v | 11 | ||||
-rw-r--r-- | backend/Tunnelingtyping.v | 2 |
30 files changed, 951 insertions, 842 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index 10eaa5b1..3f526aa4 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -21,7 +21,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Smallstep. Require Import Globalenvs. @@ -423,14 +423,14 @@ Lemma functions_translated: Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial transf_fundef TRANSF). +Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF). Lemma function_ptr_translated: forall (b: block) (f: RTL.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF). +Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). Lemma sig_function_translated: forall f tf, @@ -482,7 +482,7 @@ Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> Prop (rs#res <- rv) (Locmap.set (assign res) rv ls)) -> match_stackframes - (RTL.Stackframe res (RTL.fn_code f) sp pc rs :: s) + (RTL.Stackframe res f sp pc rs :: s) (LTL.Stackframe (assign res) (transf_fun f live assign) sp ls pc :: ts). Inductive match_states: RTL.state -> LTL.state -> Prop := @@ -493,7 +493,7 @@ Inductive match_states: RTL.state -> LTL.state -> Prop := (ANL: analyze f = Some live) (ASG: regalloc f live (live0 f live) env = Some assign) (AG: agree assign (transfer f pc live!!pc) rs ls), - match_states (RTL.State s (RTL.fn_code f) sp pc rs m) + match_states (RTL.State s f sp pc rs m) (LTL.State ts (transf_fun f live assign) sp pc ls m) | match_states_call: forall s f args m ts tf, @@ -532,7 +532,7 @@ Ltac WellTypedHyp := Ltac TranslInstr := match goal with | H: (PTree.get _ _ = Some _) |- _ => - simpl; rewrite PTree.gmap; rewrite H; simpl; auto + simpl in H; simpl; rewrite PTree.gmap; rewrite H; simpl; auto end. Ltac MatchStates := @@ -646,7 +646,7 @@ Proof. (* Icall *) exploit transl_find_function; eauto. intros [tf [TFIND TF]]. - generalize (regalloc_correct_1 f0 env live _ _ _ _ ASG H).
unfold correct_alloc_instr. intros [CORR1 [CORR2 CORR3]]. + generalize (regalloc_correct_1 f env live _ _ _ _ ASG H).
unfold correct_alloc_instr. intros [CORR1 [CORR2 CORR3]]. assert (rs##args = map ls (map assign args)). eapply agree_eval_regs; eauto. econstructor; split. @@ -735,14 +735,13 @@ Lemma transf_initial_states: Proof. intros. inversion H. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. - assert (MEM: (Genv.init_mem tprog) = (Genv.init_mem prog)). - exact (Genv.init_mem_transf_partial _ _ TRANSF). - exists (LTL.Callstate nil tf nil (Genv.init_mem tprog)); split. + exists (LTL.Callstate nil tf nil m0); split. econstructor; eauto. + eapply Genv.init_mem_transf_partial; eauto. rewrite symbols_preserved. rewrite (transform_partial_program_main _ _ TRANSF). auto. - rewrite <- H2. apply sig_function_translated; auto. - rewrite MEM. constructor; auto. constructor. + rewrite <- H3. apply sig_function_translated; auto. + constructor; auto. constructor. Qed. Lemma transf_final_states: diff --git a/backend/CSE.v b/backend/CSE.v index 98b7bbf5..ff79be54 100644 --- a/backend/CSE.v +++ b/backend/CSE.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 Registers. @@ -265,7 +265,7 @@ Definition equation_holds | Load chunk addr vl => exists a, eval_addressing ge sp addr (List.map valuation vl) = Some a /\ - loadv chunk m a = Some (valuation vres) + Mem.loadv chunk m a = Some (valuation vres) end. Definition numbering_holds diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 7f942464..fcc867af 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.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. @@ -404,7 +404,7 @@ Definition rhs_evals_to | Load chunk addr vl => exists a, eval_addressing ge sp addr (List.map valu vl) = Some a /\ - loadv chunk m a = Some v + Mem.loadv chunk m a = Some v end. Lemma equation_evals_to_holds_1: @@ -510,7 +510,7 @@ Lemma add_load_satisfiable: wf_numbering n -> numbering_satisfiable ge sp rs m n -> eval_addressing ge sp addr rs##args = Some a -> - loadv chunk m a = Some v -> + Mem.loadv chunk m a = Some v -> numbering_satisfiable ge sp (rs#dst <- v) m (add_load n dst chunk addr args). @@ -668,7 +668,7 @@ Lemma find_load_correct: find_load n chunk addr args = Some r -> exists a, eval_addressing ge sp addr rs##args = Some a /\ - loadv chunk m a = Some rs#r. + Mem.loadv chunk m a = Some rs#r. Proof. intros until r. intros WF [valu NH]. unfold find_load. caseEq (valnum_regs n args). intros n' vl VR FIND. @@ -783,21 +783,19 @@ Qed. Inductive match_stackframes: stackframe -> stackframe -> Prop := match_stackframes_intro: - forall res c sp pc rs f, - c = f.(RTL.fn_code) -> + forall res sp pc rs f, (forall v m, numbering_satisfiable ge sp (rs#res <- v) m (analyze f)!!pc) -> match_stackframes - (Stackframe res c sp pc rs) - (Stackframe res (transf_code (analyze f) c) sp pc rs). + (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). Inductive match_states: state -> state -> Prop := | match_states_intro: - forall s c sp pc rs m s' f - (CF: c = f.(RTL.fn_code)) + forall s sp pc rs m s' f (SAT: numbering_satisfiable ge sp rs m (analyze f)!!pc) (STACKS: list_forall2 match_stackframes s s'), - match_states (State s c sp pc rs m) - (State s' (transf_code (analyze f) c) sp pc rs m) + match_states (State s f sp pc rs m) + (State s' (transf_function f) sp pc rs m) | match_states_call: forall s f args m s', list_forall2 match_stackframes s s' -> @@ -812,9 +810,9 @@ Inductive match_states: state -> state -> Prop := Ltac TransfInstr := match goal with | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => - cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr)); - [ simpl - | unfold transf_code; rewrite PTree.gmap; + cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr)); + [ simpl transf_instr + | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; unfold option_map; rewrite H1; reflexivity ] end. @@ -829,14 +827,14 @@ Proof. induction 1; intros; inv MS; try (TransfInstr; intro C). (* Inop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. + exists (State s' (transf_function f) sp pc' rs m); split. apply exec_Inop; auto. econstructor; eauto. eapply analysis_correct_1; eauto. simpl; auto. unfold transfer; rewrite H; auto. (* Iop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. + exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. assert (eval_operation tge sp op rs##args = Some v). rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. generalize C; clear C. @@ -855,14 +853,14 @@ Proof. eapply add_op_satisfiable; eauto. apply wf_analyze. (* Iload *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split. + exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split. assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. generalize C; clear C. caseEq (find_load (analyze f)!!pc chunk addr args). intros r FIND CODE. eapply exec_Iop'; eauto. simpl. assert (exists a, eval_addressing ge sp addr rs##args = Some a - /\ loadv chunk m a = Some rs#r). + /\ Mem.loadv chunk m a = Some rs#r). eapply find_load_correct; eauto. eapply wf_analyze; eauto. elim H3; intros a' [A B]. @@ -874,7 +872,7 @@ Proof. eapply add_load_satisfiable; eauto. apply wf_analyze. (* Istore *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split. + exists (State s' (transf_function f) sp pc' rs m'); split. assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. eapply exec_Istore; eauto. @@ -886,7 +884,7 @@ Proof. (* Icall *) exploit find_function_translated; eauto. intro FIND'. econstructor; split. - eapply exec_Icall with (f := transf_fundef f); eauto. + eapply exec_Icall; eauto. apply sig_preserved. econstructor; eauto. constructor; auto. @@ -898,7 +896,7 @@ Proof. (* Itailcall *) exploit find_function_translated; eauto. intro FIND'. econstructor; split. - eapply exec_Itailcall with (f := transf_fundef f); eauto. + eapply exec_Itailcall; eauto. apply sig_preserved. econstructor; eauto. @@ -951,15 +949,14 @@ Lemma transf_initial_states: exists st2, initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. - exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. + exists (Callstate nil (transf_fundef f) nil m0); split. econstructor; eauto. + apply Genv.init_mem_transf; auto. change (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. apply funct_ptr_translated; auto. - rewrite <- H2. apply sig_preserved. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). - constructor. constructor. auto. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. + rewrite <- H3. apply sig_preserved. + constructor. constructor. Qed. Lemma transf_final_states: diff --git a/backend/Cminor.v b/backend/Cminor.v index aa9c5116..094bef73 100644 --- a/backend/Cminor.v +++ b/backend/Cminor.v @@ -22,7 +22,7 @@ Require Import Integers. Require Import Floats. Require Import Events. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Smallstep. Require Import Switch. @@ -144,7 +144,7 @@ Definition funsig (fd: fundef) := - [env]: local environments, map local variables to values. *) -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef unit. Definition env := PTree.t val. (** The following functions build the initial local environment at @@ -402,11 +402,12 @@ Inductive step: state -> trace -> state -> Prop := | step_skip_block: forall f k sp e m, step (State f Sskip (Kblock k) sp e m) E0 (State f Sskip k sp e m) - | step_skip_call: forall f k sp e m, + | step_skip_call: forall f k sp e m m', is_call_cont k -> f.(fn_sig).(sig_res) = None -> + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> step (State f Sskip k (Vptr sp Int.zero) e m) - E0 (Returnstate Vundef k (Mem.free m sp)) + E0 (Returnstate Vundef k m') | step_assign: forall f id a k sp e m v, eval_expr sp e m a v -> @@ -428,13 +429,14 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Scall optid sig a bl) k sp e m) E0 (Callstate fd vargs (Kcall optid f sp e k) m) - | step_tailcall: forall f sig a bl k sp e m vf vargs fd, + | step_tailcall: forall f sig a bl k sp e m vf vargs fd m', eval_expr (Vptr sp Int.zero) e m a vf -> eval_exprlist (Vptr sp Int.zero) e m bl vargs -> Genv.find_funct ge vf = Some fd -> funsig fd = sig -> + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) - E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) + E0 (Callstate fd vargs (call_cont k) m') | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) @@ -469,13 +471,15 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sswitch a cases default) k sp e m) E0 (State f (Sexit (switch_target n default cases)) k sp e m) - | step_return_0: forall f k sp e m, + | step_return_0: forall f k sp e m m', + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> step (State f (Sreturn None) k (Vptr sp Int.zero) e m) - E0 (Returnstate Vundef (call_cont k) (Mem.free m sp)) - | step_return_1: forall f a k sp e m v, + E0 (Returnstate Vundef (call_cont k) m') + | step_return_1: forall f a k sp e m v m', eval_expr (Vptr sp Int.zero) e m a v -> + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m) - E0 (Returnstate v (call_cont k) (Mem.free m sp)) + E0 (Returnstate v (call_cont k) m') | step_label: forall f lbl s k sp e m, step (State f (Slabel lbl s) k sp e m) @@ -491,10 +495,10 @@ Inductive step: state -> trace -> state -> Prop := set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') - | step_external_function: forall ef vargs k m t vres, - event_match ef vargs t vres -> + | step_external_function: forall ef vargs k m t vres m', + external_call ef vargs m t vres m' -> step (Callstate (External ef) vargs k m) - t (Returnstate vres k m) + t (Returnstate vres k m') | step_return: forall v optid f sp e k m, step (Returnstate v (Kcall optid f sp e k) m) @@ -508,9 +512,9 @@ End RELSEM. without arguments and with an empty continuation. *) Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b f, + | initial_state_intro: forall b f m0, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> @@ -560,12 +564,16 @@ Definition outcome_result_value end. Definition outcome_free_mem - (out: outcome) (m: mem) (sp: block) : mem := + (out: outcome) (m: mem) (sp: block) (sz: Z) (m': mem) := match out with - | Out_tailcall_return _ => m - | _ => Mem.free m sp + | Out_tailcall_return _ => m' = m + | _ => Mem.free m sp 0 sz = Some m' end. +(***** REVISE - PROBLEMS WITH free *) + +(****************************** + Section NATURALSEM. Variable ge: genv. @@ -580,16 +588,17 @@ Inductive eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := | eval_funcall_internal: - forall m f vargs m1 sp e t e2 m2 out vres, + forall m f vargs m1 sp e t e2 m2 out vres m3, Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) -> set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> exec_stmt (Vptr sp Int.zero) e m1 f.(fn_body) t e2 m2 out -> outcome_result_value out f.(fn_sig).(sig_res) vres -> - eval_funcall m (Internal f) vargs t (outcome_free_mem out m2 sp) vres + outcome_free_mem out m2 sp f.(fn_stackspace) m3 -> + eval_funcall m (Internal f) vargs t m3 vres | eval_funcall_external: - forall ef m args t res, - event_match ef args t res -> - eval_funcall m (External ef) args t m res + forall ef m args t res m', + external_call ef args m t res m' -> + eval_funcall m (External ef) args t m' res (** Execution of a statement: [exec_stmt ge sp e m s t e' m' out] means that statement [s] executes with outcome [out]. @@ -759,9 +768,9 @@ End NATURALSEM. Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := | bigstep_program_terminates_intro: - forall b f t m r, + forall b f m0 t m r, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> @@ -770,9 +779,9 @@ Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := Inductive bigstep_program_diverges (p: program): traceinf -> Prop := | bigstep_program_diverges_intro: - forall b f t, + forall b f m0 t, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> @@ -1116,6 +1125,6 @@ Qed. End BIGSTEP_TO_TRANSITION. - +***************************************************) diff --git a/backend/CminorSel.v b/backend/CminorSel.v index 85338720..231af8fb 100644 --- a/backend/CminorSel.v +++ b/backend/CminorSel.v @@ -19,7 +19,7 @@ Require Import Integers. Require Import Floats. Require Import Events. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Cminor. Require Import Op. Require Import Globalenvs. @@ -105,7 +105,7 @@ Definition funsig (fd: fundef) := - [lenv]: let environments, map de Bruijn indices to values. *) -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef unit. Definition letenv := list val. (** Continuations *) @@ -260,11 +260,12 @@ Inductive step: state -> trace -> state -> Prop := | step_skip_block: forall f k sp e m, step (State f Sskip (Kblock k) sp e m) E0 (State f Sskip k sp e m) - | step_skip_call: forall f k sp e m, + | step_skip_call: forall f k sp e m m', is_call_cont k -> f.(fn_sig).(sig_res) = None -> + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> step (State f Sskip k (Vptr sp Int.zero) e m) - E0 (Returnstate Vundef k (Mem.free m sp)) + E0 (Returnstate Vundef k m') | step_assign: forall f id a k sp e m v, eval_expr sp e m nil a v -> @@ -287,13 +288,14 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Scall optid sig a bl) k sp e m) E0 (Callstate fd vargs (Kcall optid f sp e k) m) - | step_tailcall: forall f sig a bl k sp e m vf vargs fd, + | step_tailcall: forall f sig a bl k sp e m vf vargs fd m', eval_expr (Vptr sp Int.zero) e m nil a vf -> eval_exprlist (Vptr sp Int.zero) e m nil bl vargs -> Genv.find_funct ge vf = Some fd -> funsig fd = sig -> + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> step (State f (Stailcall sig a bl) k (Vptr sp Int.zero) e m) - E0 (Callstate fd vargs (call_cont k) (Mem.free m sp)) + E0 (Callstate fd vargs (call_cont k) m') | step_seq: forall f s1 s2 k sp e m, step (State f (Sseq s1 s2) k sp e m) @@ -327,13 +329,15 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sswitch a cases default) k sp e m) E0 (State f (Sexit (switch_target n default cases)) k sp e m) - | step_return_0: forall f k sp e m, + | step_return_0: forall f k sp e m m', + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> step (State f (Sreturn None) k (Vptr sp Int.zero) e m) - E0 (Returnstate Vundef (call_cont k) (Mem.free m sp)) - | step_return_1: forall f a k sp e m v, + E0 (Returnstate Vundef (call_cont k) m') + | step_return_1: forall f a k sp e m v m', eval_expr (Vptr sp Int.zero) e m nil a v -> + Mem.free m sp 0 f.(fn_stackspace) = Some m' -> step (State f (Sreturn (Some a)) k (Vptr sp Int.zero) e m) - E0 (Returnstate v (call_cont k) (Mem.free m sp)) + E0 (Returnstate v (call_cont k) m') | step_label: forall f lbl s k sp e m, step (State f (Slabel lbl s) k sp e m) @@ -349,10 +353,10 @@ Inductive step: state -> trace -> state -> Prop := set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e -> step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k (Vptr sp Int.zero) e m') - | step_external_function: forall ef vargs k m t vres, - event_match ef vargs t vres -> + | step_external_function: forall ef vargs k m t vres m', + external_call ef vargs m t vres m' -> step (Callstate (External ef) vargs k m) - t (Returnstate vres k m) + t (Returnstate vres k m') | step_return: forall v optid f sp e k m, step (Returnstate v (Kcall optid f sp e k) m) @@ -361,9 +365,9 @@ Inductive step: state -> trace -> state -> Prop := End RELSEM. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b f, + | initial_state_intro: forall b f m0, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index fff9a60d..6671960c 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -19,7 +19,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import Events. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Smallstep. Require Import Op. @@ -152,7 +152,7 @@ Lemma functions_translated: Genv.find_funct tge v = Some (transf_fundef f). Proof. intros. - exact (Genv.find_funct_transf transf_fundef H). + exact (Genv.find_funct_transf transf_fundef _ _ H). Qed. Lemma function_ptr_translated: @@ -161,7 +161,7 @@ Lemma function_ptr_translated: Genv.find_funct_ptr tge b = Some (transf_fundef f). Proof. intros. - exact (Genv.find_funct_ptr_transf transf_fundef H). + exact (Genv.find_funct_ptr_transf transf_fundef _ _ H). Qed. Lemma sig_function_translated: @@ -220,21 +220,19 @@ Qed. Inductive match_stackframes: stackframe -> stackframe -> Prop := match_stackframe_intro: - forall res c sp pc rs f, - c = f.(RTL.fn_code) -> + forall res sp pc rs f, (forall v, regs_match_approx ge (analyze f)!!pc (rs#res <- v)) -> match_stackframes - (Stackframe res c sp pc rs) - (Stackframe res (transf_code (analyze f) c) sp pc rs). + (Stackframe res f sp pc rs) + (Stackframe res (transf_function f) sp pc rs). Inductive match_states: state -> state -> Prop := | match_states_intro: - forall s c sp pc rs m f s' - (CF: c = f.(RTL.fn_code)) + forall s sp pc rs m f s' (MATCH: regs_match_approx ge (analyze f)!!pc rs) (STACKS: list_forall2 match_stackframes s s'), - match_states (State s c sp pc rs m) - (State s' (transf_code (analyze f) c) sp pc rs m) + match_states (State s f sp pc rs m) + (State s' (transf_function f) sp pc rs m) | match_states_call: forall s f args m s', list_forall2 match_stackframes s s' -> @@ -249,9 +247,9 @@ Inductive match_states: state -> state -> Prop := Ltac TransfInstr := match goal with | H1: (PTree.get ?pc ?c = Some ?instr), f: function |- _ => - cut ((transf_code (analyze f) c)!pc = Some(transf_instr (analyze f)!!pc instr)); - [ simpl - | unfold transf_code; rewrite PTree.gmap; + cut ((transf_function f).(fn_code)!pc = Some(transf_instr (analyze f)!!pc instr)); + [ simpl transf_instr + | unfold transf_function, transf_code; simpl; rewrite PTree.gmap; unfold option_map; rewrite H1; reflexivity ] end. @@ -267,7 +265,7 @@ Proof. induction 1; intros; inv MS. (* Inop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. + exists (State s' (transf_function f) sp pc' rs m); split. TransfInstr; intro. eapply exec_Inop; eauto. econstructor; eauto. eapply analyze_correct_1 with (pc := pc); eauto. @@ -275,11 +273,11 @@ Proof. unfold transfer; rewrite H. auto. (* Iop *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#res <- v) m); split. + exists (State s' (transf_function f) sp pc' (rs#res <- v) m); split. TransfInstr. caseEq (op_strength_reduction (approx_reg (analyze f)!!pc) op args); intros op' args' OSR. assert (eval_operation tge sp op' rs##args' = Some v). - rewrite (eval_operation_preserved symbols_preserved). + rewrite (eval_operation_preserved _ _ symbols_preserved). generalize (op_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs MATCH op args v). rewrite OSR; simpl. auto. @@ -305,12 +303,12 @@ Proof. caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); intros addr' args' ASR. assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved symbols_preserved). + rewrite (eval_addressing_preserved _ _ symbols_preserved). generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs MATCH addr args). rewrite ASR; simpl. congruence. TransfInstr. rewrite ASR. intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' (rs#dst <- v) m); split. + exists (State s' (transf_function f) sp pc' (rs#dst <- v) m); split. eapply exec_Iload; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. @@ -321,12 +319,12 @@ Proof. caseEq (addr_strength_reduction (approx_reg (analyze f)!!pc) addr args); intros addr' args' ASR. assert (eval_addressing tge sp addr' rs##args' = Some a). - rewrite (eval_addressing_preserved symbols_preserved). + rewrite (eval_addressing_preserved _ _ symbols_preserved). generalize (addr_strength_reduction_correct ge (approx_reg (analyze f)!!pc) sp rs MATCH addr args). rewrite ASR; simpl. congruence. TransfInstr. rewrite ASR. intro. - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m'); split. + exists (State s' (transf_function f) sp pc' rs m'); split. eapply exec_Istore; eauto. econstructor; eauto. eapply analyze_correct_1; eauto. simpl; auto. @@ -351,7 +349,7 @@ Proof. constructor; auto. (* Icond, true *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp ifso rs m); split. + exists (State s' (transf_function f) sp ifso rs m); split. caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); intros cond' args' CSR. assert (eval_condition cond' rs##args' = Some true). @@ -371,7 +369,7 @@ Proof. unfold transfer; rewrite H; auto. (* Icond, false *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp ifnot rs m); split. + exists (State s' (transf_function f) sp ifnot rs m); split. caseEq (cond_strength_reduction (approx_reg (analyze f)!!pc) cond args); intros cond' args' CSR. assert (eval_condition cond' rs##args' = Some false). @@ -391,7 +389,7 @@ Proof. unfold transfer; rewrite H; auto. (* Ijumptable *) - exists (State s' (transf_code (analyze f) (fn_code f)) sp pc' rs m); split. + exists (State s' (transf_function f) sp pc' rs m); split. caseEq (intval (approx_reg (analyze f)!!pc) arg); intros. exploit intval_correct; eauto. eexact MATCH. intro VRS. eapply exec_Inop; eauto. TransfInstr. rewrite H2. @@ -403,7 +401,7 @@ Proof. unfold transfer; rewrite H; auto. (* Ireturn *) - exists (Returnstate s' (regmap_optget or Vundef rs) (free m stk)); split. + exists (Returnstate s' (regmap_optget or Vundef rs) m'); split. eapply exec_Ireturn; eauto. TransfInstr; auto. constructor; auto. @@ -432,15 +430,14 @@ Lemma transf_initial_states: Proof. intros. inversion H. exploit function_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. + exists (Callstate nil (transf_fundef f) nil m0); split. econstructor; eauto. + apply Genv.init_mem_transf; auto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. reflexivity. - rewrite <- H2. apply sig_function_translated. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). - constructor. constructor. auto. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. + rewrite <- H3. apply sig_function_translated. + constructor. constructor. Qed. Lemma transf_final_states: diff --git a/backend/LTL.v b/backend/LTL.v index 6a693361..2a1172ab 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -21,7 +21,7 @@ Require Import AST. Require Import Integers. Require Import Values. Require Import Events. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Smallstep. Require Import Op. @@ -67,7 +67,7 @@ Definition funsig (fd: fundef) := (** * Operational semantics *) -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef unit. Definition locset := Locmap.t. Definition locmap_optget (ol: option loc) (dfl: val) (ls: locset) : val := @@ -189,12 +189,13 @@ Inductive step: state -> trace -> state -> Prop := E0 (Callstate (Stackframe res f sp (postcall_locs rs) pc' :: s) f' (List.map rs args) m) | exec_Ltailcall: - forall s f stk pc rs m sig ros args f', + forall s f stk pc rs m sig ros args f' m', (fn_code f)!pc = Some(Ltailcall sig ros args) -> find_function ros rs = Some f' -> funsig f' = sig -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) pc rs m) - E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) + E0 (Callstate s f' (List.map rs args) m') | exec_Lcond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> @@ -215,20 +216,21 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp pc rs m) E0 (State s f sp pc' rs m) | exec_Lreturn: - forall s f stk pc rs m or, + forall s f stk pc rs m or m', (fn_code f)!pc = Some(Lreturn or) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) pc rs m) - E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk)) + E0 (Returnstate s (locmap_optget or Vundef rs) m') | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> step (Callstate s (Internal f) args m) E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m') | exec_function_external: - forall s ef t args res m, - event_match ef args t res -> + forall s ef t args res m m', + external_call ef args m t res m' -> step (Callstate s (External ef) args m) - t (Returnstate s res m) + t (Returnstate s res m') | exec_return: forall res f sp rs pc s vres m, step (Returnstate (Stackframe res f sp rs pc :: s) vres m) @@ -242,9 +244,9 @@ End RELSEM. by the calling conventions. *) Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b f, + | initial_state_intro: forall b f m0, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> diff --git a/backend/LTLin.v b/backend/LTLin.v index e3533388..c3b432ba 100644 --- a/backend/LTLin.v +++ b/backend/LTLin.v @@ -21,7 +21,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -72,7 +72,7 @@ Definition funsig (fd: fundef) := | External ef => ef.(ef_sig) end. -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef unit. Definition locset := Locmap.t. (** * Operational semantics *) @@ -163,13 +163,13 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lload: forall s f sp chunk addr args dst b rs m a v, eval_addressing ge sp addr (map rs args) = Some a -> - loadv chunk m a = Some v -> + Mem.loadv chunk m a = Some v -> step (State s f sp (Lload chunk addr args dst :: b) rs m) E0 (State s f sp b (Locmap.set dst v rs) m) | exec_Lstore: forall s f sp chunk addr args src b rs m m' a, eval_addressing ge sp addr (map rs args) = Some a -> - storev chunk m a (rs src) = Some m' -> + Mem.storev chunk m a (rs src) = Some m' -> step (State s f sp (Lstore chunk addr args src :: b) rs m) E0 (State s f sp b rs m') | exec_Lcall: @@ -180,11 +180,12 @@ Inductive step: state -> trace -> state -> Prop := E0 (Callstate (Stackframe res f sp (postcall_locs rs) b :: s) f' (List.map rs args) m) | exec_Ltailcall: - forall s f stk sig ros args b rs m f', + forall s f stk sig ros args b rs m f' m', find_function ros rs = Some f' -> sig = funsig f' -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros args :: b) rs m) - E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) + E0 (Callstate s f' (List.map rs args) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -213,19 +214,20 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Ljumptable arg tbl :: b) rs m) E0 (State s f sp b' rs m) | exec_Lreturn: - forall s f stk rs m or b, + forall s f stk rs m or b m', + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Lreturn or :: b) rs m) - E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk)) + E0 (Returnstate s (locmap_optget or Vundef rs) m') | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> step (Callstate s (Internal f) args m) E0 (State s f (Vptr stk Int.zero) f.(fn_code) (init_locs args f.(fn_params)) m') | exec_function_external: - forall s ef args t res m, - event_match ef args t res -> + forall s ef args t res m m', + external_call ef args m t res m' -> step (Callstate s (External ef) args m) - t (Returnstate s res m) + t (Returnstate s res m') | exec_return: forall res f sp rs b s vres m, step (Returnstate (Stackframe res f sp rs b :: s) vres m) @@ -234,9 +236,9 @@ Inductive step: state -> trace -> state -> Prop := End RELSEM. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b f, + | initial_state_intro: forall b f m0, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v index 10058907..69422e0c 100644 --- a/backend/LTLintyping.v +++ b/backend/LTLintyping.v @@ -16,6 +16,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. +Require Import Memdata. Require Import Op. Require Import RTL. Require Import Locations. diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v index 9a2322c7..e1e43f56 100644 --- a/backend/LTLtyping.v +++ b/backend/LTLtyping.v @@ -16,6 +16,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. +Require Import Memdata. Require Import Op. Require Import RTL. Require Import Locations. diff --git a/backend/Linear.v b/backend/Linear.v index bf21cb7d..be07b827 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -22,7 +22,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -67,7 +67,7 @@ Definition funsig (fd: fundef) := | External ef => ef.(ef_sig) end. -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef unit. Definition locset := Locmap.t. (** * Operational semantics *) @@ -253,13 +253,13 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lload: forall s f sp chunk addr args dst b rs m a v, eval_addressing ge sp addr (reglist rs args) = Some a -> - loadv chunk m a = Some v -> + Mem.loadv chunk m a = Some v -> step (State s f sp (Lload chunk addr args dst :: b) rs m) E0 (State s f sp b (Locmap.set (R dst) v rs) m) | exec_Lstore: forall s f sp chunk addr args src b rs m m' a, eval_addressing ge sp addr (reglist rs args) = Some a -> - storev chunk m a (rs (R src)) = Some m' -> + Mem.storev chunk m a (rs (R src)) = Some m' -> step (State s f sp (Lstore chunk addr args src :: b) rs m) E0 (State s f sp b rs m') | exec_Lcall: @@ -269,11 +269,12 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Lcall sig ros :: b) rs m) E0 (Callstate (Stackframe f sp rs b:: s) f' rs m) | exec_Ltailcall: - forall s f stk sig ros b rs m f', + forall s f stk sig ros b rs m f' m', find_function ros rs = Some f' -> sig = funsig f' -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Ltailcall sig ros :: b) rs m) - E0 (Callstate s f' (return_regs (parent_locset s) rs) (Mem.free m stk)) + E0 (Callstate s f' (return_regs (parent_locset s) rs) m') | exec_Llabel: forall s f sp lbl b rs m, step (State s f sp (Llabel lbl :: b) rs m) @@ -302,21 +303,22 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Ljumptable arg tbl :: b) rs m) E0 (State s f sp b' rs m) | exec_Lreturn: - forall s f stk b rs m, + forall s f stk b rs m m', + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk Int.zero) (Lreturn :: b) rs m) - E0 (Returnstate s (return_regs (parent_locset s) rs) (Mem.free m stk)) + E0 (Returnstate s (return_regs (parent_locset s) rs) m') | exec_function_internal: forall s f rs m m' stk, - alloc m 0 f.(fn_stacksize) = (m', stk) -> + Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> step (Callstate s (Internal f) rs m) E0 (State s f (Vptr stk Int.zero) f.(fn_code) (call_regs rs) m') | exec_function_external: - forall s ef args res rs1 rs2 m t, - event_match ef args t res -> + forall s ef args res rs1 rs2 m t m', + external_call ef args m t res m' -> args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) -> rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 -> step (Callstate s (External ef) rs1 m) - t (Returnstate s rs2 m) + t (Returnstate s rs2 m') | exec_return: forall s f sp rs0 c rs m, step (Returnstate (Stackframe f sp rs0 c :: s) rs m) @@ -325,9 +327,9 @@ Inductive step: state -> trace -> state -> Prop := End RELSEM. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b f, + | initial_state_intro: forall b f m0, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index c79908d6..5d670650 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -19,7 +19,7 @@ Require Import FSets. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Errors. @@ -49,14 +49,14 @@ Lemma functions_translated: Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial transf_fundef TRANSF). +Proof (Genv.find_funct_transf_partial transf_fundef _ TRANSF). Lemma function_ptr_translated: forall v f, Genv.find_funct_ptr ge v = Some f -> exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF). +Proof (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). Lemma symbols_preserved: forall id, @@ -73,6 +73,14 @@ Proof. inv H. reflexivity. Qed. +Lemma stacksize_preserved: + forall f tf, + transf_function f = OK tf -> + LTLin.fn_stacksize tf = LTL.fn_stacksize f. +Proof. + intros. monadInv H. auto. +Qed. + Lemma find_function_translated: forall ros ls f, LTL.find_function ge ros ls = Some f -> @@ -593,6 +601,7 @@ Proof. econstructor; split. apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto. symmetry; apply sig_preserved; auto. + rewrite (stacksize_preserved _ _ TRF). eauto. econstructor; eauto. destruct ros; simpl in H0. eapply Genv.find_funct_prop; eauto. @@ -656,6 +665,7 @@ Proof. simpl in EQ. subst c. econstructor; split. apply plus_one. eapply exec_Lreturn; eauto. + rewrite (stacksize_preserved _ _ TRF). eauto. econstructor; eauto. (* internal function *) @@ -692,16 +702,14 @@ Lemma transf_initial_states: Proof. intros. inversion H. exploit function_ptr_translated; eauto. intros [tf [A B]]. - exists (Callstate nil tf nil (Genv.init_mem tprog)); split. - econstructor; eauto. + exists (Callstate nil tf nil m0); split. + econstructor; eauto. eapply Genv.init_mem_transf_partial; eauto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). - rewrite <- H2. apply sig_preserved. auto. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). + rewrite <- H3. apply sig_preserved. auto. constructor. constructor. auto. eapply Genv.find_funct_ptr_prop; eauto. - symmetry. apply Genv.init_mem_transf_partial with transf_fundef. auto. Qed. Lemma transf_final_states: diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v index 1fe77378..028e1200 100644 --- a/backend/Lineartyping.v +++ b/backend/Lineartyping.v @@ -16,6 +16,7 @@ Require Import Coqlib. Require Import Maps. Require Import AST. Require Import Integers. +Require Import Memdata. Require Import Op. Require Import RTL. Require Import Locations. diff --git a/backend/Mach.v b/backend/Mach.v index f7e85c3e..e89ff3b1 100644 --- a/backend/Mach.v +++ b/backend/Mach.v @@ -22,7 +22,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Op. @@ -84,7 +84,7 @@ Definition funsig (fd: fundef) := | External ef => ef.(ef_sig) end. -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef unit. (** * Dynamic semantics *) diff --git a/backend/Machabstr.v b/backend/Machabstr.v index a2630a2b..ceaf9a68 100644 --- a/backend/Machabstr.v +++ b/backend/Machabstr.v @@ -15,10 +15,10 @@ Require Import Coqlib. Require Import Maps. Require Import AST. -Require Import Mem. +Require Import Memory. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -262,10 +262,11 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mcall sig ros :: c) rs fr m) E0 (Callstate (Stackframe f sp c fr :: s) f' rs m) | exec_Mtailcall: - forall s f stk soff sig ros c rs fr m f', + forall s f stk soff sig ros c rs fr m f' m', find_function ros rs = Some f' -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m) - E0 (Callstate s f' rs (Mem.free m stk)) + E0 (Callstate s f' rs m') | exec_Mgoto: forall s f sp lbl c rs fr m c', find_label lbl f.(fn_code) = Some c' -> @@ -290,9 +291,10 @@ Inductive step: state -> trace -> state -> Prop := step (State s f sp (Mjumptable arg tbl :: c) rs fr m) E0 (State s f sp c' rs fr m) | exec_Mreturn: - forall s f stk soff c rs fr m, + forall s f stk soff c rs fr m m', + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> step (State s f (Vptr stk soff) (Mreturn :: c) rs fr m) - E0 (Returnstate s rs (Mem.free m stk)) + E0 (Returnstate s rs m') | exec_function_internal: forall s f rs m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -300,12 +302,12 @@ Inductive step: state -> trace -> state -> Prop := E0 (State s f (Vptr stk (Int.repr (-f.(fn_framesize)))) f.(fn_code) rs empty_frame m') | exec_function_external: - forall s ef args res rs1 rs2 m t, - event_match ef args t res -> + forall s ef args res rs1 rs2 m t m', + external_call ef args m t res m' -> extcall_arguments (parent_function s) rs1 (parent_frame s) ef.(ef_sig) args -> rs2 = (rs1#(Conventions.loc_result ef.(ef_sig)) <- res) -> step (Callstate s (External ef) rs1 m) - t (Returnstate s rs2 m) + t (Returnstate s rs2 m') | exec_return: forall f sp c fr s rs m, step (Returnstate (Stackframe f sp c fr :: s) rs m) @@ -314,9 +316,9 @@ Inductive step: state -> trace -> state -> Prop := End RELSEM. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b f, + | initial_state_intro: forall b f m0, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> initial_state p (Callstate nil f (Regmap.init Vundef) m0). diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 89529fd4..7714f3d5 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -74,19 +74,27 @@ Hypothesis wt_f: wt_function f. semantics. [ms] is the current memory state in the concrete semantics. The stack pointer is [Vptr sp base] in both semantics. *) -Inductive frame_match (fr: frame) - (sp: block) (base: int) - (mm ms: mem) : Prop := - frame_match_intro: - valid_block ms sp -> - low_bound mm sp = 0 -> - low_bound ms sp = -f.(fn_framesize) -> - high_bound ms sp >= 0 -> - base = Int.repr (-f.(fn_framesize)) -> - (forall ty ofs, - -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) -> - load (chunk_of_type ty) ms sp ofs = Some(fr ty ofs)) -> - frame_match fr sp base mm ms. +Record frame_match (fr: frame) + (sp: block) (base: int) + (mm ms: mem) : Prop := + mk_frame_match { + fm_valid_1: + Mem.valid_block mm sp; + fm_valid_2: + Mem.valid_block ms sp; + fm_base: + base = Int.repr(- f.(fn_framesize)); + fm_stackdata_pos: + Mem.low_bound mm sp = 0; + fm_write_perm: + Mem.range_perm ms sp (-f.(fn_framesize)) 0 Freeable; + fm_contents_match: + forall ty ofs, + -f.(fn_framesize) <= ofs -> ofs + AST.typesize ty <= 0 -> (4 | ofs) -> + exists v, + Mem.load (chunk_of_type ty) ms sp ofs = Some v + /\ Val.lessdef (fr ty ofs) v + }. (** The following two innocuous-looking lemmas are the key results showing that [sp]-relative memory accesses in the concrete @@ -94,8 +102,8 @@ Inductive frame_match (fr: frame) semantics. First, a value [v] that has type [ty] is preserved when stored in memory with chunk [chunk_of_type ty], then read back with the same chunk. The typing hypothesis is crucial here: - for instance, a float value reads back as [Vundef] when stored - and load with chunk [Mint32]. *) + for instance, a float value is not preserved when stored + and loaded with chunk [Mint32]. *) Lemma load_result_ty: forall v ty, @@ -127,14 +135,15 @@ Lemma frame_match_load_stack: frame_match fr sp base mm ms -> 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> (4 | Int.signed ofs) -> - load_stack ms (Vptr sp base) ty ofs = - Some (fr ty (Int.signed ofs - f.(fn_framesize))). + exists v, + load_stack ms (Vptr sp base) ty ofs = Some v + /\ Val.lessdef (fr ty (Int.signed ofs - f.(fn_framesize))) v. Proof. intros. inv H. inv wt_f. - unfold load_stack, Val.add, loadv. + unfold load_stack, Val.add, Mem.loadv. replace (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs)) with (Int.signed ofs - fn_framesize f). - apply H7. omega. omega. + apply fm_contents_match0. omega. omega. apply Zdivide_minus_l; auto. assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). apply Int.signed_repr. @@ -149,9 +158,9 @@ Lemma frame_match_get_slot: forall fr sp base mm ms ty ofs v, frame_match fr sp base mm ms -> get_slot f fr ty (Int.signed ofs) v -> - load_stack ms (Vptr sp base) ty ofs = Some v. + exists v', load_stack ms (Vptr sp base) ty ofs = Some v' /\ Val.lessdef v v'. Proof. - intros. inversion H. inv H0. inv H7. eapply frame_match_load_stack; eauto. + intros. inv H0. inv H1. eapply frame_match_load_stack; eauto. Qed. (** Assigning a value to a frame slot (in the abstract semantics) @@ -160,19 +169,20 @@ Qed. and activation records is preserved. *) Lemma frame_match_store_stack: - forall fr sp base mm ms ty ofs v, + forall fr sp base mm ms ty ofs v v', frame_match fr sp base mm ms -> - 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + 0 <= Int.signed ofs -> Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> (4 | Int.signed ofs) -> Val.has_type v ty -> + Val.lessdef v v' -> Mem.extends mm ms -> exists ms', - store_stack ms (Vptr sp base) ty ofs v = Some ms' /\ + store_stack ms (Vptr sp base) ty ofs v' = Some ms' /\ frame_match (update ty (Int.signed ofs - f.(fn_framesize)) v fr) sp base mm ms' /\ Mem.extends mm ms'. Proof. intros. inv H. inv wt_f. - unfold store_stack, Val.add, storev. + unfold store_stack, Val.add, Mem.storev. assert (Int.signed (Int.add (Int.repr (- fn_framesize f)) ofs) = Int.signed ofs - fn_framesize f). assert (Int.signed (Int.repr (-fn_framesize f)) = -fn_framesize f). @@ -183,58 +193,84 @@ Proof. apply Zle_trans with 0. generalize (AST.typesize_pos ty). omega. compute; congruence. rewrite H. - assert (exists ms', store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v = Some ms'). - apply valid_access_store. - constructor. auto. omega. - rewrite size_type_chunk. omega. + assert ({ ms' | Mem.store (chunk_of_type ty) ms sp (Int.signed ofs - fn_framesize f) v' = Some ms'}). + apply Mem.valid_access_store. constructor. + apply Mem.range_perm_implies with Freeable; auto with mem. + red; intros; apply fm_write_perm0. + rewrite <- size_type_chunk in H1. + generalize (size_chunk_pos (chunk_of_type ty)). + omega. replace (align_chunk (chunk_of_type ty)) with 4. apply Zdivide_minus_l; auto. destruct ty; auto. - destruct H8 as [ms' STORE]. - generalize (low_bound_store _ _ _ _ _ _ STORE sp). intro LB. - generalize (high_bound_store _ _ _ _ _ _ STORE sp). intro HB. + destruct X as [ms' STORE]. exists ms'. split. exact STORE. (* frame match *) - split. constructor; try congruence. - eauto with mem. intros. unfold update. - destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0. + split. constructor. + (* valid *) + eauto with mem. + eauto with mem. + (* base *) + auto. + (* stackdata_pos *) + auto. + (* write_perm *) + red; intros; eauto with mem. + (* contents *) + intros. + exploit fm_contents_match0; eauto. intros [v0 [LOAD0 VLD0]]. + assert (exists v1, Mem.load (chunk_of_type ty0) ms' sp ofs0 = Some v1). + apply Mem.valid_access_load; eauto with mem. + destruct H9 as [v1 LOAD1]. + exists v1; split; auto. + unfold update. + destruct (zeq (Int.signed ofs - fn_framesize f) ofs0). subst ofs0. destruct (typ_eq ty ty0). subst ty0. (* same *) - transitivity (Some (Val.load_result (chunk_of_type ty) v)). - eapply load_store_same; eauto. - decEq. apply load_result_ty; auto. + inv H4. + assert (Some v1 = Some (Val.load_result (chunk_of_type ty) v')). + rewrite <- LOAD1. eapply Mem.load_store_same; eauto. + replace (type_of_chunk (chunk_of_type ty)) with ty. auto. + destruct ty; auto. + inv H4. rewrite load_result_ty; auto. + auto. (* mismatch *) - eapply load_store_mismatch'; eauto with mem. - destruct ty; destruct ty0; simpl; congruence. + auto. destruct (zle (ofs0 + AST.typesize ty0) (Int.signed ofs - fn_framesize f)). (* disjoint *) - rewrite <- H9; auto. eapply load_store_other; eauto. - right; left. rewrite size_type_chunk; auto. + assert (Some v1 = Some v0). + rewrite <- LOAD0; rewrite <- LOAD1. + eapply Mem.load_store_other; eauto. + right; left. rewrite size_type_chunk; auto. + inv H9. auto. destruct (zle (Int.signed ofs - fn_framesize f + AST.typesize ty)). - rewrite <- H9; auto. eapply load_store_other; eauto. - right; right. rewrite size_type_chunk; auto. + assert (Some v1 = Some v0). + rewrite <- LOAD0; rewrite <- LOAD1. + eapply Mem.load_store_other; eauto. + right; right. rewrite size_type_chunk; auto. + inv H9. auto. (* overlap *) - eapply load_store_overlap'; eauto with mem. - rewrite size_type_chunk; auto. - rewrite size_type_chunk; auto. + auto. (* extends *) - eapply store_outside_extends; eauto. - left. rewrite size_type_chunk. omega. + eapply Mem.store_outside_extends; eauto. + left. rewrite fm_stackdata_pos0. + rewrite size_type_chunk. omega. Qed. Lemma frame_match_set_slot: - forall fr sp base mm ms ty ofs v fr', + forall fr sp base mm ms ty ofs v fr' v', frame_match fr sp base mm ms -> set_slot f fr ty (Int.signed ofs) v fr' -> Val.has_type v ty -> + Val.lessdef v v' -> Mem.extends mm ms -> exists ms', - store_stack ms (Vptr sp base) ty ofs v = Some ms' /\ + store_stack ms (Vptr sp base) ty ofs v' = Some ms' /\ frame_match fr' sp base mm ms' /\ Mem.extends mm ms'. Proof. - intros. inv H0. inv H3. eapply frame_match_store_stack; eauto. + intros. inv H0. inv H4. eapply frame_match_store_stack; eauto. Qed. (** Agreement is preserved by stores within blocks other than the @@ -243,45 +279,40 @@ Qed. Lemma frame_match_store_other: forall fr sp base mm ms chunk b ofs v ms', frame_match fr sp base mm ms -> - store chunk ms b ofs v = Some ms' -> + Mem.store chunk ms b ofs v = Some ms' -> sp <> b -> frame_match fr sp base mm ms'. Proof. - intros. inv H. - generalize (low_bound_store _ _ _ _ _ _ H0 sp). intro LB. - generalize (high_bound_store _ _ _ _ _ _ H0 sp). intro HB. - apply frame_match_intro; auto. - eauto with mem. - congruence. - congruence. - intros. rewrite <- H7; auto. - eapply load_store_other; eauto. + intros. inv H. constructor; auto. + eauto with mem. + red; intros; eauto with mem. + intros. exploit fm_contents_match0; eauto. intros [v0 [LOAD LD]]. + exists v0; split; auto. rewrite <- LOAD. eapply Mem.load_store_other; eauto. Qed. (** Agreement is preserved by parallel stores in the Machabstr and the Machconcr semantics. *) Lemma frame_match_store: - forall fr sp base mm ms chunk b ofs v mm' ms', + forall fr sp base mm ms chunk b ofs v mm' v' ms', frame_match fr sp base mm ms -> - store chunk mm b ofs v = Some mm' -> - store chunk ms b ofs v = Some ms' -> + Mem.store chunk mm b ofs v = Some mm' -> + Mem.store chunk ms b ofs v' = Some ms' -> frame_match fr sp base mm' ms'. Proof. - intros. inv H. - generalize (low_bound_store _ _ _ _ _ _ H0 sp). intro LBm. - generalize (low_bound_store _ _ _ _ _ _ H1 sp). intro LBs. - generalize (high_bound_store _ _ _ _ _ _ H0 sp). intro HBm. - generalize (high_bound_store _ _ _ _ _ _ H1 sp). intro HBs. - apply frame_match_intro; auto. + intros. inv H. constructor; auto. eauto with mem. - congruence. congruence. congruence. - intros. rewrite <- H7; auto. eapply load_store_other; eauto. - destruct (zeq sp b). subst b. right. + eauto with mem. + rewrite (Mem.bounds_store _ _ _ _ _ _ H0). auto. + red; intros; eauto with mem. + intros. exploit fm_contents_match0; eauto. intros [v0 [LOAD LD]]. + exists v0; split; auto. rewrite <- LOAD. eapply Mem.load_store_other; eauto. + destruct (zeq sp b); auto. subst b. right. rewrite size_type_chunk. - assert (valid_access mm chunk sp ofs) by eauto with mem. - inv H9. left. omega. - auto. + assert (Mem.valid_access mm chunk sp ofs Nonempty) by eauto with mem. + exploit Mem.store_valid_access_3. eexact H0. intro. + exploit Mem.valid_access_in_bounds. eauto. rewrite fm_stackdata_pos0. + omega. Qed. (** Memory allocation of the Cminor stack data block (in the abstract @@ -291,68 +322,111 @@ Qed. remain true. *) Lemma frame_match_new: - forall mm ms mm' ms' sp sp', - mm.(nextblock) = ms.(nextblock) -> - alloc mm 0 f.(fn_stacksize) = (mm', sp) -> - alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp') -> - sp = sp' /\ + forall mm ms mm' ms' sp, + Mem.alloc mm 0 f.(fn_stacksize) = (mm', sp) -> + Mem.alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms', sp) -> frame_match empty_frame sp (Int.repr (-f.(fn_framesize))) mm' ms'. Proof. intros. - assert (sp = sp'). - exploit alloc_result. eexact H0. exploit alloc_result. eexact H1. - congruence. - subst sp'. split. auto. - generalize (low_bound_alloc_same _ _ _ _ _ H0). intro LBm. - generalize (low_bound_alloc_same _ _ _ _ _ H1). intro LBs. - generalize (high_bound_alloc_same _ _ _ _ _ H0). intro HBm. - generalize (high_bound_alloc_same _ _ _ _ _ H1). intro HBs. inv wt_f. constructor; simpl; eauto with mem. - rewrite HBs. auto. - intros. - eapply load_alloc_same'; eauto. + rewrite (Mem.bounds_alloc_same _ _ _ _ _ H). auto. + red; intros. eapply Mem.perm_alloc_2; eauto. omega. + intros. exists Vundef; split. + eapply Mem.load_alloc_same'; eauto. rewrite size_type_chunk. omega. - replace (align_chunk (chunk_of_type ty)) with 4; auto. destruct ty; auto. + replace (align_chunk (chunk_of_type ty)) with 4; auto. + destruct ty; auto. + unfold empty_frame. auto. Qed. Lemma frame_match_alloc: - forall mm ms fr sp base lom him los his mm' ms' bm bs, - mm.(nextblock) = ms.(nextblock) -> + forall mm ms fr sp base lom him los his mm' ms' b, frame_match fr sp base mm ms -> - alloc mm lom him = (mm', bm) -> - alloc ms los his = (ms', bs) -> + Mem.alloc mm lom him = (mm', b) -> + Mem.alloc ms los his = (ms', b) -> frame_match fr sp base mm' ms'. Proof. - intros. inversion H0. - assert (valid_block mm sp). red. rewrite H. auto. - exploit low_bound_alloc_other. eexact H1. eexact H9. intro LBm. - exploit high_bound_alloc_other. eexact H1. eexact H9. intro HBm. - exploit low_bound_alloc_other. eexact H2. eexact H3. intro LBs. - exploit high_bound_alloc_other. eexact H2. eexact H3. intro HBs. - apply frame_match_intro. - eapply valid_block_alloc; eauto. - congruence. congruence. congruence. auto. auto. - intros. eapply load_alloc_other; eauto. + intros. inversion H. + assert (sp <> b). + apply Mem.valid_not_valid_diff with ms; eauto with mem. + constructor; auto. + eauto with mem. + eauto with mem. + rewrite (Mem.bounds_alloc_other _ _ _ _ _ H0); auto. + red; intros; eauto with mem. + intros. exploit fm_contents_match0; eauto. intros [v [LOAD LD]]. + exists v; split; auto. eapply Mem.load_alloc_other; eauto. Qed. (** [frame_match] relations are preserved by freeing a block other than the one pointed to by [sp]. *) Lemma frame_match_free: - forall fr sp base mm ms b, + forall fr sp base mm ms b lom him los his mm' ms', frame_match fr sp base mm ms -> sp <> b -> - frame_match fr sp base (free mm b) (free ms b). + Mem.free mm b lom him = Some mm' -> + Mem.free ms b los his = Some ms' -> + frame_match fr sp base mm' ms'. +Proof. + intros. inversion H. constructor; auto. + eauto with mem. + eauto with mem. + rewrite (Mem.bounds_free _ _ _ _ _ H1). auto. + red; intros; eauto with mem. + intros. rewrite (Mem.load_free _ _ _ _ _ H2); auto. +Qed. + +Lemma frame_match_delete: + forall fr sp base mm ms mm', + frame_match fr sp base mm ms -> + Mem.free mm sp 0 f.(fn_stacksize) = Some mm' -> + Mem.extends mm ms -> + exists ms', + Mem.free ms sp (-f.(fn_framesize)) f.(fn_stacksize) = Some ms' + /\ Mem.extends mm' ms'. Proof. intros. inversion H. - generalize (low_bound_free mm _ _ H0); intro LBm. - generalize (low_bound_free ms _ _ H0); intro LBs. - generalize (high_bound_free mm _ _ H0); intro HBm. - generalize (high_bound_free ms _ _ H0); intro HBs. - apply frame_match_intro; auto. - congruence. congruence. congruence. - intros. rewrite <- H6; auto. apply load_free. auto. + assert (Mem.range_perm mm sp 0 (fn_stacksize f) Freeable). + eapply Mem.free_range_perm; eauto. + assert ({ ms' | Mem.free ms sp (-f.(fn_framesize)) f.(fn_stacksize) = Some ms' }). + apply Mem.range_perm_free. + red; intros. destruct (zlt ofs 0). + apply fm_write_perm0. omega. + eapply Mem.perm_extends; eauto. apply H2. omega. + destruct X as [ms' FREE]. exists ms'; split; auto. + eapply Mem.free_right_extends; eauto. + eapply Mem.free_left_extends; eauto. + intros; red; intros. + exploit Mem.perm_in_bounds; eauto. + rewrite (Mem.bounds_free _ _ _ _ _ H0). rewrite fm_stackdata_pos0; intro. + exploit Mem.perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. + auto. +Qed. + +(** [frame_match] is preserved by external calls. *) + +Lemma frame_match_external_call: + forall fr sp base mm ms mm' ms' ef vargs vres t vargs' vres', + frame_match fr sp base mm ms -> + Mem.extends mm ms -> + external_call ef vargs mm t vres mm' -> + Mem.extends mm' ms' -> + external_call ef vargs' ms t vres' ms' -> + mem_unchanged_on (loc_out_of_bounds mm) ms ms' -> + frame_match fr sp base mm' ms'. +Proof. + intros. destruct H4 as [A B]. inversion H. constructor. + eapply external_call_valid_block; eauto. + eapply external_call_valid_block; eauto. + auto. + rewrite (external_call_bounds _ _ _ _ _ _ _ H1); auto. + red; intros. apply A; auto. red. omega. + intros. exploit fm_contents_match0; eauto. intros [v [C D]]. + exists v; split; auto. + apply B; auto. + rewrite size_type_chunk; intros; red. omega. Qed. End FRAME_MATCH. @@ -430,61 +504,130 @@ Proof. simpl. omega. Qed. +Definition is_pointer_or_int (v: val) : Prop := + match v with + | Vint _ => True + | Vptr _ _ => True + | _ => False + end. + +Remark is_pointer_has_type: + forall v, is_pointer_or_int v -> Val.has_type v Tint. +Proof. + intros; destruct v; elim H; exact I. +Qed. + +Lemma frame_match_load_stack_pointer: + forall fr sp base mm ms ty ofs, + frame_match f fr sp base mm ms -> + 0 <= Int.signed ofs /\ Int.signed ofs + AST.typesize ty <= f.(fn_framesize) -> + (4 | Int.signed ofs) -> + is_pointer_or_int (fr ty (Int.signed ofs - f.(fn_framesize))) -> + load_stack ms (Vptr sp base) ty ofs = Some (fr ty (Int.signed ofs - f.(fn_framesize))). +Proof. + intros. exploit frame_match_load_stack; eauto. + intros [v [LOAD LD]]. + inv LD. auto. rewrite <- H4 in H2. elim H2. +Qed. + Lemma frame_match_load_link: forall fr sp base mm ms, frame_match f (extend_frame fr) sp base mm ms -> - load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some (parent_sp cs). + is_pointer_or_int (parent_sp cs) -> + load_stack ms (Vptr sp base) Tint f.(fn_link_ofs) = Some(parent_sp cs). Proof. intros. inversion wt_f. - replace (parent_sp cs) with - (extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))). - eapply frame_match_load_stack; eauto. - - unfold extend_frame. rewrite update_other. apply update_same. simpl. omega. + assert (parent_sp cs = + extend_frame fr Tint (Int.signed f.(fn_link_ofs) - f.(fn_framesize))). + unfold extend_frame. rewrite update_other. rewrite update_same. auto. + simpl. omega. + rewrite H1; eapply frame_match_load_stack_pointer; eauto. + rewrite <- H1; auto. Qed. Lemma frame_match_load_retaddr: forall fr sp base mm ms, frame_match f (extend_frame fr) sp base mm ms -> - load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some (parent_ra cs). + is_pointer_or_int (parent_ra cs) -> + load_stack ms (Vptr sp base) Tint f.(fn_retaddr_ofs) = Some(parent_ra cs). Proof. intros. inversion wt_f. - replace (parent_ra cs) with - (extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))). - eapply frame_match_load_stack; eauto. - unfold extend_frame. apply update_same. + assert (parent_ra cs = + extend_frame fr Tint (Int.signed f.(fn_retaddr_ofs) - f.(fn_framesize))). + unfold extend_frame. rewrite update_same. auto. + rewrite H1; eapply frame_match_load_stack_pointer; eauto. + rewrite <- H1; auto. Qed. Lemma frame_match_function_entry: - forall mm ms mm' ms1 sp sp', - extends mm ms -> - alloc mm 0 f.(fn_stacksize) = (mm', sp) -> - alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp') -> - Val.has_type (parent_sp cs) Tint -> - Val.has_type (parent_ra cs) Tint -> + forall mm ms mm' sp, + Mem.extends mm ms -> + Mem.alloc mm 0 f.(fn_stacksize) = (mm', sp) -> + is_pointer_or_int (parent_sp cs) -> + is_pointer_or_int (parent_ra cs) -> let base := Int.repr (-f.(fn_framesize)) in - exists ms2, exists ms3, - sp = sp' /\ + exists ms1, exists ms2, exists ms3, + Mem.alloc ms (- f.(fn_framesize)) f.(fn_stacksize) = (ms1, sp) /\ store_stack ms1 (Vptr sp base) Tint f.(fn_link_ofs) (parent_sp cs) = Some ms2 /\ store_stack ms2 (Vptr sp base) Tint f.(fn_retaddr_ofs) (parent_ra cs) = Some ms3 /\ frame_match f (extend_frame empty_frame) sp base mm' ms3 /\ - extends mm' ms3. + Mem.extends mm' ms3. Proof. intros. inversion wt_f. - exploit alloc_extends; eauto. omega. omega. intros [A EXT0]. - exploit frame_match_new. eauto. inv H. eexact H4. eauto. eauto. eauto. - fold base. intros [C FM0]. - destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ - FM0 wt_function_link wt_function_link_aligned H2 EXT0) - as [ms2 [STORE1 [FM1 EXT1]]]. - destruct (frame_match_store_stack _ wt_f _ _ _ _ _ Tint _ _ - FM1 wt_function_retaddr wt_function_retaddr_aligned H3 EXT1) - as [ms3 [STORE2 [FM3 EXT3]]]. - exists ms2; exists ms3; auto. + exploit Mem.alloc_extends; eauto. + instantiate (1 := -f.(fn_framesize)). omega. + instantiate (1 := f.(fn_stacksize)). omega. + intros [ms1 [A EXT0]]. + exploit frame_match_new; eauto. fold base. intros FM0. + exploit frame_match_store_stack. eauto. eexact FM0. + instantiate (1 := fn_link_ofs f); omega. + instantiate (1 := Tint). simpl; omega. + auto. apply is_pointer_has_type. eexact H1. constructor. auto. + intros [ms2 [STORE1 [FM1 EXT1]]]. + exploit frame_match_store_stack. eauto. eexact FM1. + instantiate (1 := fn_retaddr_ofs f); omega. + instantiate (1 := Tint). simpl; omega. + auto. apply is_pointer_has_type. eexact H2. constructor. auto. + intros [ms3 [STORE2 [FM2 EXT2]]]. + exists ms1; exists ms2; exists ms3; auto. Qed. End EXTEND_FRAME. +(** ** The ``less defined than'' relation between register states. *) + +Definition regset_lessdef (rs1 rs2: regset) : Prop := + forall r, Val.lessdef (rs1 r) (rs2 r). + +Lemma regset_lessdef_list: + forall rs1 rs2, regset_lessdef rs1 rs2 -> + forall rl, Val.lessdef_list (rs1##rl) (rs2##rl). +Proof. + induction rl; simpl. + constructor. + constructor; auto. +Qed. + +Lemma regset_lessdef_set: + forall rs1 rs2 r v1 v2, + regset_lessdef rs1 rs2 -> Val.lessdef v1 v2 -> + regset_lessdef (rs1#r <- v1) (rs2#r <- v2). +Proof. + intros; red; intros. unfold Regmap.set. + destruct (RegEq.eq r0 r); auto. +Qed. + +Lemma regset_lessdef_find_function_ptr: + forall ge ros rs1 rs2 fb, + find_function_ptr ge ros rs1 = Some fb -> + regset_lessdef rs1 rs2 -> + find_function_ptr ge ros rs2 = Some fb. +Proof. + unfold find_function_ptr; intros; destruct ros; simpl in *. + generalize (H0 m); intro LD; inv LD. auto. rewrite <- H2 in H. congruence. + auto. +Qed. + (** ** Invariant for stacks *) Section SIMULATION. @@ -518,12 +661,26 @@ Inductive match_stacks: wt_function f -> frame_match f (extend_frame f ts fr) sp base mm ms -> stack_below ts sp -> - Val.has_type ra Tint -> + is_pointer_or_int ra -> match_stacks s ts mm ms -> match_stacks (Machabstr.Stackframe f (Vptr sp base) c fr :: s) (Machconcr.Stackframe fb (Vptr sp base) ra c :: ts) mm ms. +Lemma match_stacks_parent_sp_pointer: + forall s ts mm ms, + match_stacks s ts mm ms -> is_pointer_or_int (Machconcr.parent_sp ts). +Proof. + induction 1; simpl; auto. +Qed. + +Lemma match_stacks_parent_ra_pointer: + forall s ts mm ms, + match_stacks s ts mm ms -> is_pointer_or_int (Machconcr.parent_ra ts). +Proof. + induction 1; simpl; auto. +Qed. + (** If [match_stacks] holds, a lookup in the parent frame in the Machabstr semantics corresponds to two memory loads in the Machconcr semantics, one to load the pointer to the parent's @@ -533,7 +690,9 @@ Lemma match_stacks_get_parent: forall s ts mm ms ty ofs v, match_stacks s ts mm ms -> get_slot (parent_function s) (parent_frame s) ty (Int.signed ofs) v -> - load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v. + exists v', + load_stack ms (Machconcr.parent_sp ts) ty ofs = Some v' + /\ Val.lessdef v v'. Proof. intros. inv H; simpl in H0. inv H0. inv H. simpl in H1. elimtype False. generalize (AST.typesize_pos ty). omega. @@ -542,7 +701,7 @@ Proof. Qed. (** Preservation of the [match_stacks] invariant - by various kinds of memory stores. *) + by various kinds of memory operations. *) Remark stack_below_trans: forall ts b b', @@ -556,7 +715,7 @@ Lemma match_stacks_store_other: forall s ts ms mm, match_stacks s ts mm ms -> forall chunk b ofs v ms', - store chunk ms b ofs v = Some ms' -> + Mem.store chunk ms b ofs v = Some ms' -> stack_below ts b -> match_stacks s ts mm ms'. Proof. @@ -593,9 +752,9 @@ Qed. Lemma match_stacks_store: forall s ts ms mm, match_stacks s ts mm ms -> - forall chunk b ofs v mm' ms', - store chunk mm b ofs v = Some mm' -> - store chunk ms b ofs v = Some ms' -> + forall chunk b ofs v mm' v' ms', + Mem.store chunk mm b ofs v = Some mm' -> + Mem.store chunk ms b ofs v' = Some ms' -> match_stacks s ts mm' ms'. Proof. induction 1; intros. @@ -607,28 +766,28 @@ Qed. Lemma match_stacks_alloc: forall s ts ms mm, match_stacks s ts mm ms -> - forall lom him mm' bm los his ms' bs, - mm.(nextblock) = ms.(nextblock) -> - alloc mm lom him = (mm', bm) -> - alloc ms los his = (ms', bs) -> + forall lom him mm' b los his ms', + Mem.alloc mm lom him = (mm', b) -> + Mem.alloc ms los his = (ms', b) -> match_stacks s ts mm' ms'. Proof. induction 1; intros. constructor. - econstructor; eauto. - eapply frame_match_alloc; eauto. + econstructor; eauto. eapply frame_match_alloc; eauto. Qed. Lemma match_stacks_free: forall s ts ms mm, match_stacks s ts mm ms -> - forall b, + forall b lom him los his mm' ms', + Mem.free mm b lom him = Some mm' -> + Mem.free ms b los his = Some ms' -> stack_below ts b -> - match_stacks s ts (Mem.free mm b) (Mem.free ms b). + match_stacks s ts mm' ms'. Proof. induction 1; intros. constructor. - red in H5; simpl in H5. + red in H7; simpl in H7. econstructor; eauto. eapply frame_match_free; eauto. unfold block; omega. eapply IHmatch_stacks; eauto. @@ -636,21 +795,36 @@ Proof. Qed. Lemma match_stacks_function_entry: - forall s ts mm ms lom him mm' los his ms' stk, + forall s ts ms mm, match_stacks s ts mm ms -> - alloc mm lom him = (mm', stk) -> - alloc ms los his = (ms', stk) -> + forall lom him mm' stk los his ms', + Mem.alloc mm lom him = (mm', stk) -> + Mem.alloc ms los his = (ms', stk) -> match_stacks s ts mm' ms' /\ stack_below ts stk. Proof. intros. - assert (stk = nextblock mm). eapply Mem.alloc_result; eauto. - assert (stk = nextblock ms). eapply Mem.alloc_result; eauto. - split. - eapply match_stacks_alloc; eauto. congruence. - red. - inv H; simpl. - unfold nullptr. apply Zgt_lt. apply nextblock_pos. - inv H6. red in H. rewrite H3. auto. + assert (stk = Mem.nextblock mm) by eauto with mem. + split. eapply match_stacks_alloc; eauto. + red. inv H; simpl. + unfold Mem.nullptr. apply Zgt_lt. apply Mem.nextblock_pos. + inv H5. auto. +Qed. + +Lemma match_stacks_external_call: + forall s ts mm ms, + match_stacks s ts mm ms -> + forall ef vargs t vres mm' ms' vargs' vres', + Mem.extends mm ms -> + external_call ef vargs mm t vres mm' -> + Mem.extends mm' ms' -> + external_call ef vargs' ms t vres' ms' -> + mem_unchanged_on (loc_out_of_bounds mm) ms ms' -> + match_stacks s ts mm' ms'. +Proof. + induction 1; intros. + constructor. + econstructor; eauto. + eapply frame_match_external_call; eauto. Qed. (** ** Invariant between states. *) @@ -666,27 +840,30 @@ Qed. Inductive match_states: Machabstr.state -> Machconcr.state -> Prop := | match_states_intro: - forall s f sp base c rs fr mm ts fb ms + forall s f sp base c rs fr mm ts trs fb ms (STACKS: match_stacks s ts mm ms) (FM: frame_match f (extend_frame f ts fr) sp base mm ms) (BELOW: stack_below ts sp) + (RLD: regset_lessdef rs trs) (MEXT: Mem.extends mm ms) (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)), match_states (Machabstr.State s f (Vptr sp base) c rs fr mm) - (Machconcr.State ts fb (Vptr sp base) c rs ms) + (Machconcr.State ts fb (Vptr sp base) c trs ms) | match_states_call: - forall s f rs mm ts fb ms + forall s f rs mm ts trs fb ms (STACKS: match_stacks s ts mm ms) (MEXT: Mem.extends mm ms) + (RLD: regset_lessdef rs trs) (FIND: Genv.find_funct_ptr ge fb = Some f), match_states (Machabstr.Callstate s f rs mm) - (Machconcr.Callstate ts fb rs ms) + (Machconcr.Callstate ts fb trs ms) | match_states_return: - forall s rs mm ts ms + forall s rs mm ts trs ms (STACKS: match_stacks s ts mm ms) - (MEXT: Mem.extends mm ms), + (MEXT: Mem.extends mm ms) + (RLD: regset_lessdef rs trs), match_states (Machabstr.Returnstate s rs mm) - (Machconcr.Returnstate ts rs ms). + (Machconcr.Returnstate ts trs ms). (** * The proof of simulation *) @@ -725,20 +902,26 @@ Qed. (** Preservation of arguments to external functions. *) Lemma transl_extcall_arguments: - forall rs s sg args ts m ms, + forall rs s sg args ts trs m ms, Machabstr.extcall_arguments (parent_function s) rs (parent_frame s) sg args -> + regset_lessdef rs trs -> match_stacks s ts m ms -> - extcall_arguments rs ms (parent_sp ts) sg args. + exists targs, + extcall_arguments trs ms (parent_sp ts) sg targs + /\ Val.lessdef_list args targs. Proof. unfold Machabstr.extcall_arguments, extcall_arguments; intros. - assert (forall locs vals, - Machabstr.extcall_args (parent_function s) rs (parent_frame s) locs vals -> - extcall_args rs ms (parent_sp ts) locs vals). - induction locs; intros; inv H1. - constructor. + generalize (Conventions.loc_arguments sg) args H. + induction l; intros; inv H2. + exists (@nil val); split; constructor. + exploit IHl; eauto. intros [targs [A B]]. + inv H7. exists (trs r :: targs); split. + constructor; auto. constructor. + constructor; auto. + exploit match_stacks_get_parent; eauto. intros [targ [C D]]. + exists (targ :: targs); split. + constructor; auto. constructor; auto. constructor; auto. - inv H6. constructor. constructor. eapply match_stacks_get_parent; eauto. - auto. Qed. Hypothesis wt_prog: wt_program p. @@ -757,11 +940,11 @@ Proof. (* Mgetstack *) assert (WTF: wt_function f) by (inv WTS; auto). - exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. + exploit frame_match_get_slot; eauto. eapply get_slot_extends; eauto. + intros [v' [A B]]. + exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split. constructor; auto. - eapply frame_match_get_slot; eauto. - eapply get_slot_extends; eauto. - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. eapply regset_lessdef_set; eauto. (* Msetstack *) assert (WTF: wt_function f) by (inv WTS; auto). @@ -769,41 +952,51 @@ Proof. inv WTS. generalize (wt_function_instrs _ WTF _ (is_tail_in TAIL)); intro WTI. inv WTI. apply WTRS. - exploit frame_match_set_slot; eauto. + exploit frame_match_set_slot. eauto. eauto. eapply set_slot_extends; eauto. + auto. apply RLD. auto. intros [ms' [STORE [FM' EXT']]]. - exists (State ts fb (Vptr sp0 base) c rs ms'); split. + exists (State ts fb (Vptr sp0 base) c trs ms'); split. apply exec_Msetstack; auto. econstructor; eauto. eapply match_stacks_store_slot; eauto. (* Mgetparam *) assert (WTF: wt_function f) by (inv WTS; auto). - exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. + exploit match_stacks_get_parent; eauto. intros [v' [A B]]. + exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split. eapply exec_Mgetparam; eauto. eapply frame_match_load_link; eauto. - eapply match_stacks_get_parent; eauto. - econstructor; eauto with coqlib. + eapply match_stacks_parent_sp_pointer; eauto. + econstructor; eauto with coqlib. apply regset_lessdef_set; eauto. (* Mop *) - exists (State ts fb (Vptr sp0 base) c (rs#res <- v) ms); split. + exploit eval_operation_lessdef. 2: eauto. + eapply regset_lessdef_list; eauto. + intros [v' [A B]]. + exists (State ts fb (Vptr sp0 base) c (trs#res <- v') ms); split. apply exec_Mop; auto. - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. apply regset_lessdef_set; eauto. (* Mload *) - exists (State ts fb (Vptr sp0 base) c (rs#dst <- v) ms); split. + exploit eval_addressing_lessdef. 2: eauto. eapply regset_lessdef_list; eauto. + intros [a' [A B]]. + exploit Mem.loadv_extends. eauto. eauto. eexact B. + intros [v' [C D]]. + exists (State ts fb (Vptr sp0 base) c (trs#dst <- v') ms); split. eapply exec_Mload; eauto. - destruct a; simpl in H0; try discriminate. - simpl. eapply Mem.load_extends; eauto. - econstructor; eauto with coqlib. + econstructor; eauto with coqlib. apply regset_lessdef_set; eauto. (* Mstore *) - destruct a; simpl in H0; try discriminate. - exploit Mem.store_within_extends; eauto. intros [ms' [STORE MEXT']]. - exists (State ts fb (Vptr sp0 base) c rs ms'); split. + exploit eval_addressing_lessdef. 2: eauto. eapply regset_lessdef_list; eauto. + intros [a' [A B]]. + exploit Mem.storev_extends. eauto. eauto. eexact B. apply RLD. + intros [ms' [C D]]. + exists (State ts fb (Vptr sp0 base) c trs ms'); split. eapply exec_Mstore; eauto. + destruct a; simpl in H0; try congruence. inv B. simpl in C. econstructor; eauto with coqlib. - eapply match_stacks_store; eauto. + eapply match_stacks_store. eauto. eexact H0. eexact C. eapply frame_match_store; eauto. (* Mcall *) @@ -814,7 +1007,7 @@ Proof. inv WTS. eapply is_tail_cons_left; eauto. destruct H0 as [ra' RETADDR]. econstructor; split. - eapply exec_Mcall; eauto. + eapply exec_Mcall; eauto. eapply regset_lessdef_find_function_ptr; eauto. econstructor; eauto. econstructor; eauto. inv WTS; auto. exact I. @@ -822,12 +1015,13 @@ Proof. assert (WTF: wt_function f) by (inv WTS; auto). exploit find_function_find_function_ptr; eauto. intros [fb' [FIND' FINDFUNCT]]. + exploit frame_match_delete; eauto. intros [ms' [A B]]. econstructor; split. eapply exec_Mtailcall; eauto. - eapply frame_match_load_link; eauto. - eapply frame_match_load_retaddr; eauto. - econstructor; eauto. eapply match_stacks_free; auto. - apply free_extends; auto. + eapply regset_lessdef_find_function_ptr; eauto. + eapply frame_match_load_link; eauto. eapply match_stacks_parent_sp_pointer; eauto. + eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto. + econstructor; eauto. eapply match_stacks_free; eauto. (* Mgoto *) econstructor; split. @@ -837,49 +1031,50 @@ Proof. (* Mcond *) econstructor; split. eapply exec_Mcond_true; eauto. + eapply eval_condition_lessdef; eauto. apply regset_lessdef_list; auto. econstructor; eauto. econstructor; split. eapply exec_Mcond_false; eauto. + eapply eval_condition_lessdef; eauto. apply regset_lessdef_list; auto. econstructor; eauto. (* Mjumptable *) econstructor; split. - eapply exec_Mjumptable; eauto. + eapply exec_Mjumptable; eauto. + generalize (RLD arg); intro LD. rewrite H in LD. inv LD. auto. econstructor; eauto. (* Mreturn *) assert (WTF: wt_function f) by (inv WTS; auto). + exploit frame_match_delete; eauto. intros [ms' [A B]]. econstructor; split. eapply exec_Mreturn; eauto. - eapply frame_match_load_link; eauto. - eapply frame_match_load_retaddr; eauto. + eapply frame_match_load_link; eauto. eapply match_stacks_parent_sp_pointer; eauto. + eapply frame_match_load_retaddr; eauto. eapply match_stacks_parent_ra_pointer; eauto. econstructor; eauto. eapply match_stacks_free; eauto. - apply free_extends; auto. (* internal function *) assert (WTF: wt_function f). inv WTS. inv H5. auto. - caseEq (alloc ms (- f.(fn_framesize)) f.(fn_stacksize)). - intros ms' stk' ALLOC. - assert (Val.has_type (parent_sp ts) Tint). - inv STACKS; simpl; auto. - assert (Val.has_type (parent_ra ts) Tint). - inv STACKS; simpl; auto. - destruct (frame_match_function_entry _ WTF _ _ _ _ _ _ _ - MEXT H ALLOC H0 H1) - as [ms2 [ms3 [EQ [STORE1 [STORE2 [FM MEXT']]]]]]. - subst stk'. + exploit frame_match_function_entry. eauto. eauto. eauto. + instantiate (1 := ts). eapply match_stacks_parent_sp_pointer; eauto. + eapply match_stacks_parent_ra_pointer; eauto. + intros [ms1 [ms2 [ms3 [ALLOC [STORE1 [STORE2 [FM MEXT']]]]]]]. econstructor; split. eapply exec_function_internal; eauto. exploit match_stacks_function_entry; eauto. intros [STACKS' BELOW]. econstructor; eauto. eapply match_stacks_store_slot with (ms := ms2); eauto. - eapply match_stacks_store_slot with (ms := ms'); eauto. + eapply match_stacks_store_slot with (ms := ms1); eauto. (* external function *) + exploit transl_extcall_arguments; eauto. intros [targs [A B]]. + exploit external_call_mem_extends; eauto. + intros [tres [ms' [C [D [E F]]]]]. econstructor; split. - eapply exec_function_external; eauto. - eapply transl_extcall_arguments; eauto. + eapply exec_function_external. eauto. eexact C. eexact A. reflexivity. econstructor; eauto. + eapply match_stacks_external_call; eauto. + apply regset_lessdef_set; auto. (* return *) inv STACKS. @@ -894,8 +1089,10 @@ Lemma equiv_initial_states: Proof. intros. inversion H. econstructor; split. - econstructor. eauto. - split. econstructor. constructor. apply Mem.extends_refl. auto. + econstructor. eauto. eauto. + split. econstructor. constructor. apply Mem.extends_refl. + unfold Regmap.init; red; intros. constructor. + auto. econstructor. simpl; intros; contradiction. eapply Genv.find_funct_ptr_prop; eauto. red; intros; exact I. @@ -906,7 +1103,9 @@ Lemma equiv_final_states: match_states st1 st2 /\ wt_state st1 -> Machabstr.final_state st1 r -> Machconcr.final_state st2 r. Proof. intros. inv H0. destruct H. inv H. inv STACKS. - constructor; auto. + constructor. + generalize (RLD (Conventions.loc_result (mksignature nil (Some Tint)))). + rewrite H1. intro LD. inv LD. auto. Qed. Theorem exec_program_equiv: diff --git a/backend/Machconcr.v b/backend/Machconcr.v index 84ae0a4f..a6be4bc2 100644 --- a/backend/Machconcr.v +++ b/backend/Machconcr.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -179,13 +179,14 @@ Inductive step: state -> trace -> state -> Prop := E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) f' rs m) | exec_Mtailcall: - forall s fb stk soff sig ros c rs m f f', + forall s fb stk soff sig ros c rs m f f' m', find_function_ptr ge ros rs = 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' -> step (State s fb (Vptr stk soff) (Mtailcall sig ros :: c) rs m) - E0 (Callstate s f' rs (Mem.free m stk)) + E0 (Callstate s f' rs m') | exec_Mgoto: forall s fb f sp lbl c rs m c', Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -213,12 +214,13 @@ Inductive step: state -> trace -> state -> Prop := step (State s fb sp (Mjumptable arg tbl :: c) rs m) E0 (State s fb sp c' rs m) | exec_Mreturn: - forall s fb stk soff c rs m f, + forall s fb stk soff c rs m f 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' -> step (State s fb (Vptr stk soff) (Mreturn :: c) rs m) - E0 (Returnstate s rs (Mem.free m stk)) + E0 (Returnstate s rs m') | exec_function_internal: forall s fb rs m f m1 m2 m3 stk, Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -229,13 +231,13 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate s fb rs m) E0 (State s fb sp f.(fn_code) rs m3) | exec_function_external: - forall s fb rs m t rs' ef args res, + forall s fb rs m t rs' ef args res m', Genv.find_funct_ptr ge fb = Some (External ef) -> - event_match ef args t res -> + external_call ef args m t res m' -> extcall_arguments rs m (parent_sp s) ef.(ef_sig) args -> rs' = (rs#(Conventions.loc_result ef.(ef_sig)) <- res) -> step (Callstate s fb rs m) - t (Returnstate s rs' m) + t (Returnstate s rs' m') | exec_return: forall s f sp ra c rs m, step (Returnstate (Stackframe f sp ra c :: s) rs m) @@ -244,9 +246,9 @@ Inductive step: state -> trace -> state -> Prop := End RELSEM. Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall fb, + | initial_state_intro: forall fb m0, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some fb -> initial_state p (Callstate nil fb (Regmap.init Vundef) m0). diff --git a/backend/Machtyping.v b/backend/Machtyping.v index 8b40001a..c2e797ae 100644 --- a/backend/Machtyping.v +++ b/backend/Machtyping.v @@ -15,10 +15,10 @@ Require Import Coqlib. Require Import Maps. Require Import AST. -Require Import Mem. +Require Import Memory. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Op. @@ -194,14 +194,6 @@ Proof. constructor; auto. Qed. -Lemma wt_event_match: - forall ef args t res, - event_match ef args t res -> - Val.has_type res (proj_sig_res ef.(ef_sig)). -Proof. - induction 1. inversion H0; exact I. -Qed. - Section SUBJECT_REDUCTION. Inductive wt_stackframe: stackframe -> Prop := @@ -259,7 +251,7 @@ Proof. simpl in H. rewrite <- H2. replace v with (rs r1). apply WTRS. congruence. replace (mreg_type res) with (snd (type_of_operation op)). - apply type_of_operation_sound with fundef ge rs##args sp; auto. + apply type_of_operation_sound with fundef unit ge rs##args sp; auto. rewrite <- H5; reflexivity. apply wt_setreg; auto. inversion H1. rewrite H7. @@ -267,18 +259,18 @@ Proof. assert (WTFD: wt_fundef f'). destruct ros; simpl in H. - apply (Genv.find_funct_prop wt_fundef wt_p H). + apply (Genv.find_funct_prop wt_fundef _ _ wt_p H). destruct (Genv.find_symbol ge i); try discriminate. - apply (Genv.find_funct_ptr_prop wt_fundef wt_p H). + apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H). econstructor; eauto. intros. elim H0; intro. subst s0. econstructor; eauto with coqlib. auto. assert (WTFD: wt_fundef f'). destruct ros; simpl in H. - apply (Genv.find_funct_prop wt_fundef wt_p H). + apply (Genv.find_funct_prop wt_fundef _ _ wt_p H). destruct (Genv.find_symbol ge i); try discriminate. - apply (Genv.find_funct_ptr_prop wt_fundef wt_p H). + apply (Genv.find_funct_ptr_prop wt_fundef _ _ wt_p H). econstructor; eauto. (* apply wt_setreg; auto. exact I. *) @@ -293,7 +285,7 @@ Proof. apply wt_empty_frame. econstructor; eauto. apply wt_setreg; auto. - generalize (wt_event_match _ _ _ _ H). + generalize (external_call_well_typed _ _ _ _ _ _ H). unfold proj_sig_res, Conventions.loc_result. destruct (sig_res (ef_sig ef)). destruct t0; simpl; auto. diff --git a/backend/RTL.v b/backend/RTL.v index b2ee80fc..c5d4d7d0 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -22,7 +22,7 @@ Require Import AST. Require Import Integers. Require Import Values. Require Import Events. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Smallstep. Require Import Op. @@ -115,7 +115,7 @@ Definition funsig (fd: fundef) := (** * Operational semantics *) -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef unit. Definition regset := Regmap.t val. Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := @@ -128,8 +128,8 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := set of transitions between states. A state captures the current point in the execution. Three kinds of states appear in the transitions: -- [State cs c sp pc rs m] describes an execution point within a function. - [c] is the code for the current function (a CFG). +- [State cs f sp pc rs m] describes an execution point within a function. + [f] is the current function. [sp] is the pointer to the stack block for its current activation (as in Cminor). [pc] is the current program point (CFG node) within the code [c]. @@ -145,10 +145,10 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset := [v] is the return value and [m] the current memory state. In all three kinds of states, the [cs] parameter represents the call stack. -It is a list of frames [Stackframe res c sp pc rs]. Each frame represents +It is a list of frames [Stackframe res f sp pc rs]. Each frame represents a function call in progress. [res] is the pseudo-register that will receive the result of the call. -[c] is the code of the calling function. +[f] is the calling function. [sp] is its stack pointer. [pc] is the program point for the instruction that follows the call. [rs] is the state of registers in the calling function. @@ -157,7 +157,7 @@ a function call in progress. Inductive stackframe : Type := | Stackframe: forall (res: reg) (**r where to store the result *) - (c: code) (**r code of calling function *) + (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (pc: node) (**r program point in calling function *) (rs: regset), (**r register state in calling function *) @@ -166,7 +166,7 @@ Inductive stackframe : Type := Inductive state : Type := | State: forall (stack: list stackframe) (**r call stack *) - (c: code) (**r current code *) + (f: function) (**r current function *) (sp: val) (**r stack pointer *) (pc: node) (**r current program point in [c] *) (rs: regset) (**r register state *) @@ -206,107 +206,109 @@ Definition find_function Inductive step: state -> trace -> state -> Prop := | exec_Inop: - forall s c sp pc rs m pc', - c!pc = Some(Inop pc') -> - step (State s c sp pc rs m) - E0 (State s c sp pc' rs m) + forall s f sp pc rs m pc', + (fn_code f)!pc = Some(Inop pc') -> + step (State s f sp pc rs m) + E0 (State s f sp pc' rs m) | exec_Iop: - forall s c sp pc rs m op args res pc' v, - c!pc = Some(Iop op args res pc') -> + forall s f sp pc rs m op args res pc' v, + (fn_code f)!pc = Some(Iop op args res pc') -> eval_operation ge sp op rs##args = Some v -> - step (State s c sp pc rs m) - E0 (State s c sp pc' (rs#res <- v) m) + step (State s f sp pc rs m) + E0 (State s f sp pc' (rs#res <- v) m) | exec_Iload: - forall s c sp pc rs m chunk addr args dst pc' a v, - c!pc = Some(Iload chunk addr args dst pc') -> + forall s f sp pc rs m chunk addr args dst pc' a v, + (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> - step (State s c sp pc rs m) - E0 (State s c sp pc' (rs#dst <- v) m) + step (State s f sp pc rs m) + E0 (State s f sp pc' (rs#dst <- v) m) | exec_Istore: - forall s c sp pc rs m chunk addr args src pc' a m', - c!pc = Some(Istore chunk addr args src pc') -> + forall s f sp pc rs m chunk addr args src pc' a m', + (fn_code f)!pc = Some(Istore chunk addr args src pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.storev chunk m a rs#src = Some m' -> - step (State s c sp pc rs m) - E0 (State s c sp pc' rs m') + step (State s f sp pc rs m) + E0 (State s f sp pc' rs m') | exec_Icall: - forall s c sp pc rs m sig ros args res pc' f, - c!pc = Some(Icall sig ros args res pc') -> - find_function ros rs = Some f -> - funsig f = sig -> - step (State s c sp pc rs m) - E0 (Callstate (Stackframe res c sp pc' rs :: s) f rs##args m) + forall s f sp pc rs m sig ros args res pc' fd, + (fn_code f)!pc = Some(Icall sig ros args res pc') -> + find_function ros rs = Some fd -> + funsig fd = sig -> + step (State s f sp pc rs m) + E0 (Callstate (Stackframe res f sp pc' rs :: s) fd rs##args m) | exec_Itailcall: - forall s c stk pc rs m sig ros args f, - c!pc = Some(Itailcall sig ros args) -> - find_function ros rs = Some f -> - funsig f = sig -> - step (State s c (Vptr stk Int.zero) pc rs m) - E0 (Callstate s f rs##args (Mem.free m stk)) + forall s f stk pc rs m sig ros args fd m', + (fn_code f)!pc = Some(Itailcall sig ros args) -> + find_function ros rs = Some fd -> + funsig fd = sig -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s f (Vptr stk Int.zero) pc rs m) + E0 (Callstate s fd rs##args m') | exec_Icond_true: - forall s c sp pc rs m cond args ifso ifnot, - c!pc = Some(Icond cond args ifso ifnot) -> + forall s f sp pc rs m cond args ifso ifnot, + (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> eval_condition cond rs##args = Some true -> - step (State s c sp pc rs m) - E0 (State s c sp ifso rs m) + step (State s f sp pc rs m) + E0 (State s f sp ifso rs m) | exec_Icond_false: - forall s c sp pc rs m cond args ifso ifnot, - c!pc = Some(Icond cond args ifso ifnot) -> + forall s f sp pc rs m cond args ifso ifnot, + (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> eval_condition cond rs##args = Some false -> - step (State s c sp pc rs m) - E0 (State s c sp ifnot rs m) + step (State s f sp pc rs m) + E0 (State s f sp ifnot rs m) | exec_Ijumptable: - forall s c sp pc rs m arg tbl n pc', - c!pc = Some(Ijumptable arg tbl) -> + forall s f sp pc rs m arg tbl n pc', + (fn_code f)!pc = Some(Ijumptable arg tbl) -> rs#arg = Vint n -> list_nth_z tbl (Int.signed n) = Some pc' -> - step (State s c sp pc rs m) - E0 (State s c sp pc' rs m) + step (State s f sp pc rs m) + E0 (State s f sp pc' rs m) | exec_Ireturn: - forall s c stk pc rs m or, - c!pc = Some(Ireturn or) -> - step (State s c (Vptr stk Int.zero) pc rs m) - E0 (Returnstate s (regmap_optget or Vundef rs) (Mem.free m stk)) + forall s f stk pc rs m or m', + (fn_code f)!pc = Some(Ireturn or) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + step (State s f (Vptr stk Int.zero) pc rs m) + E0 (Returnstate s (regmap_optget or Vundef rs) m') | exec_function_internal: forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> step (Callstate s (Internal f) args m) E0 (State s - f.(fn_code) + f (Vptr stk Int.zero) f.(fn_entrypoint) (init_regs args f.(fn_params)) m') | exec_function_external: - forall s ef args res t m, - event_match ef args t res -> + forall s ef args res t m m', + external_call ef args m t res m' -> step (Callstate s (External ef) args m) - t (Returnstate s res m) + t (Returnstate s res m') | exec_return: - forall res c sp pc rs s vres m, - step (Returnstate (Stackframe res c sp pc rs :: s) vres m) - E0 (State s c sp pc (rs#res <- vres) m). + forall res f sp pc rs s vres m, + step (Returnstate (Stackframe res f sp pc rs :: s) vres m) + E0 (State s f sp pc (rs#res <- vres) m). Lemma exec_Iop': - forall s c sp pc rs m op args res pc' rs' v, - c!pc = Some(Iop op args res pc') -> + forall s f sp pc rs m op args res pc' rs' v, + (fn_code f)!pc = Some(Iop op args res pc') -> eval_operation ge sp op rs##args = Some v -> rs' = (rs#res <- v) -> - step (State s c sp pc rs m) - E0 (State s c sp pc' rs' m). + step (State s f sp pc rs m) + E0 (State s f sp pc' rs' m). Proof. intros. subst rs'. eapply exec_Iop; eauto. Qed. Lemma exec_Iload': - forall s c sp pc rs m chunk addr args dst pc' rs' a v, - c!pc = Some(Iload chunk addr args dst pc') -> + forall s f sp pc rs m chunk addr args dst pc' rs' a v, + (fn_code f)!pc = Some(Iload chunk addr args dst pc') -> eval_addressing ge sp addr rs##args = Some a -> Mem.loadv chunk m a = Some v -> rs' = (rs#dst <- v) -> - step (State s c sp pc rs m) - E0 (State s c sp pc' rs' m). + step (State s f sp pc rs m) + E0 (State s f sp pc' rs' m). Proof. intros. subst rs'. eapply exec_Iload; eauto. Qed. @@ -319,9 +321,9 @@ End RELSEM. without arguments and with an empty call stack. *) Inductive initial_state (p: program): state -> Prop := - | initial_state_intro: forall b f, + | initial_state_intro: forall b f m0, let ge := Genv.globalenv p in - let m0 := Genv.init_mem p in + Genv.init_mem p = Some m0 -> Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index d07bd081..f4d1342a 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Smallstep. Require Import Globalenvs. @@ -337,7 +337,7 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. Proof - (Genv.find_funct_ptr_transf_partial transl_fundef TRANSL). + (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL). Lemma functions_translated: forall (v: val) (f: CminorSel.fundef), @@ -345,7 +345,7 @@ Lemma functions_translated: exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. Proof - (Genv.find_funct_transf_partial transl_fundef TRANSL). + (Genv.find_funct_transf_partial transl_fundef _ TRANSL). Lemma sig_transl_function: forall (f: CminorSel.fundef) (tf: RTL.fundef), @@ -365,10 +365,10 @@ Qed. (** Correctness of the code generated by [add_move]. *) Lemma tr_move_correct: - forall r1 ns r2 nd cs code sp rs m, - tr_move code ns r1 nd r2 -> + forall r1 ns r2 nd cs f sp rs m, + tr_move f.(fn_code) ns r1 nd r2 -> exists rs', - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\ + star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ rs'#r2 = rs#r1 /\ (forall r, r <> r2 -> rs'#r = rs#r). Proof. @@ -382,13 +382,13 @@ Qed. (** Correctness of the code generated by [store_var] and [store_optvar]. *) Lemma tr_store_var_correct: - forall rs cs code map r id ns nd e sp m, - tr_store_var code map r id ns nd -> + forall rs cs f map r id ns nd e sp m, + tr_store_var f.(fn_code) map r id ns nd -> map_wf map -> match_env map e nil rs -> exists rs', - star step tge (State cs code sp ns rs m) - E0 (State cs code sp nd rs' m) + star step tge (State cs f sp ns rs m) + E0 (State cs f sp nd rs' m) /\ match_env map (PTree.set id rs#r e) nil rs'. Proof. intros. destruct H as [rv [A B]]. @@ -402,13 +402,13 @@ Proof. Qed. Lemma tr_store_optvar_correct: - forall rs cs code map r optid ns nd e sp m, - tr_store_optvar code map r optid ns nd -> + forall rs cs f map r optid ns nd e sp m, + tr_store_optvar f.(fn_code) map r optid ns nd -> map_wf map -> match_env map e nil rs -> exists rs', - star step tge (State cs code sp ns rs m) - E0 (State cs code sp nd rs' m) + star step tge (State cs f sp ns rs m) + E0 (State cs f sp nd rs' m) /\ match_env map (set_optvar optid rs#r e) nil rs'. Proof. intros. destruct optid; simpl in *. @@ -419,15 +419,15 @@ Qed. (** Correctness of the translation of [switch] statements *) Lemma transl_switch_correct: - forall cs sp e m code map r nexits t ns, - tr_switch code map r nexits t ns -> + forall cs sp e m f map r nexits t ns, + tr_switch f.(fn_code) map r nexits t ns -> forall rs i act, rs#r = Vint i -> map_wf map -> match_env map e nil rs -> comptree_match i t = Some act -> exists nd, exists rs', - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) /\ + star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ nth_error nexits act = Some nd /\ match_env map e nil rs'. Proof. @@ -458,7 +458,7 @@ Proof. set (rs1 := rs#rt <- (Vint(Int.sub i ofs))). assert (ME1: match_env map e nil rs1). unfold rs1. eauto with rtlg. - assert (EX1: step tge (State cs code sp n rs m) E0 (State cs code sp n1 rs1 m)). + assert (EX1: step tge (State cs f sp n rs m) E0 (State cs f sp n1 rs1 m)). eapply exec_Iop; eauto. predSpec Int.eq Int.eq_spec ofs Int.zero; simpl. rewrite H10. rewrite Int.sub_zero_l. congruence. @@ -521,12 +521,12 @@ Variable m: mem. Definition transl_expr_prop (le: letenv) (a: expr) (v: val) : Prop := - forall cs code map pr ns nd rd rs + forall cs f map pr ns nd rd rs (MWF: map_wf map) - (TE: tr_expr code map pr a ns nd rd) + (TE: tr_expr f.(fn_code) map pr a ns nd rd) (ME: match_env map e le rs), exists rs', - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) + star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ match_env map e le rs' /\ rs'#rd = v /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). @@ -536,25 +536,25 @@ Definition transl_expr_prop Definition transl_exprlist_prop (le: letenv) (al: exprlist) (vl: list val) : Prop := - forall cs code map pr ns nd rl rs + forall cs f map pr ns nd rl rs (MWF: map_wf map) - (TE: tr_exprlist code map pr al ns nd rl) + (TE: tr_exprlist f.(fn_code) map pr al ns nd rl) (ME: match_env map e le rs), exists rs', - star step tge (State cs code sp ns rs m) E0 (State cs code sp nd rs' m) + star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ match_env map e le rs' /\ rs'##rl = vl /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). Definition transl_condition_prop (le: letenv) (a: condexpr) (vb: bool) : Prop := - forall cs code map pr ns ntrue nfalse rs + forall cs f map pr ns ntrue nfalse rs (MWF: map_wf map) - (TE: tr_condition code map pr a ns ntrue nfalse) + (TE: tr_condition f.(fn_code) map pr a ns ntrue nfalse) (ME: match_env map e le rs), exists rs', - star step tge (State cs code sp ns rs m) E0 - (State cs code sp (if vb then ntrue else nfalse) rs' m) + star step tge (State cs f sp ns rs m) E0 + (State cs f sp (if vb then ntrue else nfalse) rs' m) /\ match_env map e le rs' /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). @@ -604,7 +604,7 @@ Proof. split. eapply star_right. eexact EX1. eapply exec_Iop; eauto. subst vargs. - rewrite (@eval_operation_preserved CminorSel.fundef RTL.fundef ge tge). + rewrite (@eval_operation_preserved CminorSel.fundef _ _ _ ge tge). auto. exact symbols_preserved. traceEq. (* Match-env *) @@ -621,7 +621,7 @@ Lemma transl_expr_Eload_correct: eval_exprlist ge sp e m le args vargs -> transl_exprlist_prop le args vargs -> Op.eval_addressing ge sp addr vargs = Some vaddr -> - loadv chunk m vaddr = Some v -> + Mem.loadv chunk m vaddr = Some v -> transl_expr_prop le (Eload chunk addr args) v. Proof. intros; red; intros. inv TE. @@ -629,7 +629,7 @@ Proof. exists (rs1#rd <- v). (* Exec *) split. eapply star_right. eexact EX1. eapply exec_Iload; eauto. - rewrite RES1. rewrite (@eval_addressing_preserved _ _ ge tge). + rewrite RES1. rewrite (@eval_addressing_preserved _ _ _ _ ge tge). exact H1. exact symbols_preserved. traceEq. (* Match-env *) split. eauto with rtlg. @@ -650,7 +650,7 @@ Lemma transl_expr_Econdition_correct: Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. - assert (tr_expr code map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd). + assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd). destruct vcond; auto. exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. @@ -767,7 +767,7 @@ Lemma transl_condition_CEcondition_correct: Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. - assert (tr_condition code map pr (if vcond then ifso else ifnot) + assert (tr_condition f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue' else nfalse') ntrue nfalse). destruct vcond; auto. exploit H2; eauto. intros [rs2 [EX2 [ME2 OTHER2]]]. @@ -977,12 +977,13 @@ Qed. *) -Inductive tr_funbody (c: code) (map: mapping) (f: CminorSel.function) +Inductive tr_fun (tf: function) (map: mapping) (f: CminorSel.function) (ngoto: labelmap) (nret: node) (rret: option reg) : Prop := - | tr_funbody_intro: forall nentry r, + | tr_fun_intro: forall nentry r, rret = ret_reg f.(CminorSel.fn_sig) r -> - tr_stmt c map f.(fn_body) nentry nret nil ngoto nret rret -> - tr_funbody c map f ngoto nret rret. + tr_stmt tf.(fn_code) map f.(fn_body) nentry nret nil ngoto nret rret -> + tf.(fn_stacksize) = f.(fn_stackspace) -> + tr_fun tf map f ngoto nret rret. Inductive tr_cont: RTL.code -> mapping -> CminorSel.cont -> node -> list node -> labelmap -> node -> option reg -> @@ -1006,25 +1007,25 @@ Inductive tr_cont: RTL.code -> mapping -> with match_stacks: CminorSel.cont -> list RTL.stackframe -> Prop := | match_stacks_stop: match_stacks Kstop nil - | match_stacks_call: forall optid f sp e k r c n rs cs map nexits ngoto nret rret n', + | match_stacks_call: forall optid f sp e k r tf n rs cs map nexits ngoto nret rret n', map_wf map -> - tr_funbody c map f ngoto nret rret -> + tr_fun tf map f ngoto nret rret -> match_env map e nil rs -> - tr_store_optvar c map r optid n n' -> + tr_store_optvar tf.(fn_code) map r optid n n' -> ~reg_in_map map r -> - tr_cont c map k n' nexits ngoto nret rret cs -> - match_stacks (Kcall optid f sp e k) (Stackframe r c sp n rs :: cs). + tr_cont tf.(fn_code) map k n' nexits ngoto nret rret cs -> + match_stacks (Kcall optid f sp e k) (Stackframe r tf sp n rs :: cs). Inductive match_states: CminorSel.state -> RTL.state -> Prop := | match_state: - forall f s k sp e m cs c ns rs map ncont nexits ngoto nret rret + forall f s k sp e m cs tf ns rs map ncont nexits ngoto nret rret (MWF: map_wf map) - (TS: tr_stmt c map s ns ncont nexits ngoto nret rret) - (TF: tr_funbody c map f ngoto nret rret) - (TK: tr_cont c map k ncont nexits ngoto nret rret cs) + (TS: tr_stmt tf.(fn_code) map s ns ncont nexits ngoto nret rret) + (TF: tr_fun tf map f ngoto nret rret) + (TK: tr_cont tf.(fn_code) map k ncont nexits ngoto nret rret cs) (ME: match_env map e nil rs), match_states (CminorSel.State f s k sp e m) - (RTL.State cs c sp ns rs m) + (RTL.State cs tf sp ns rs m) | match_callstate: forall f args k m cs tf (TF: transl_fundef f = OK tf) @@ -1109,15 +1110,19 @@ Proof. (* skip return *) inv TS. - assert (c!ncont = Some(Ireturn rret) /\ match_stacks k cs). - inv TK; simpl in H; try contradiction; auto. - destruct H1. + assert ((fn_code tf)!ncont = Some(Ireturn rret) + /\ match_stacks k cs). + inv TK; simpl in H; try contradiction; auto. + destruct H2. assert (rret = None). inv TF. unfold ret_reg. rewrite H0. auto. + assert (fn_stacksize tf = fn_stackspace f). + inv TF. auto. subst rret. econstructor; split. left; apply plus_one. eapply exec_Ireturn. eauto. - simpl. constructor; auto. + rewrite H5. eauto. + constructor; auto. (* assign *) inv TS. @@ -1152,7 +1157,7 @@ Proof. intros [rs' [A [B [C D]]]]. exploit transl_exprlist_correct; eauto. intros [rs'' [E [F [G J]]]]. - exploit functions_translated; eauto. intros [tf [P Q]]. + exploit functions_translated; eauto. intros [tf' [P Q]]. econstructor; split. left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. eapply exec_Icall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. @@ -1166,12 +1171,14 @@ Proof. intros [rs' [A [B [C D]]]]. exploit transl_exprlist_correct; eauto. intros [rs'' [E [F [G J]]]]. - exploit functions_translated; eauto. intros [tf [P Q]]. + exploit functions_translated; eauto. intros [tf' [P Q]]. exploit match_stacks_call_cont; eauto. intros [U V]. + assert (fn_stacksize tf = fn_stackspace f). inv TF; auto. econstructor; split. left; eapply plus_right. eapply star_trans. eexact A. eexact E. reflexivity. eapply exec_Itailcall; eauto. simpl. rewrite J. rewrite C. eauto. simpl; auto. apply sig_transl_function; auto. + rewrite H2; eauto. traceEq. rewrite G. constructor; auto. (* seq *) @@ -1234,17 +1241,21 @@ Proof. (* return none *) inv TS. exploit match_stacks_call_cont; eauto. intros [U V]. + inversion TF. econstructor; split. left; apply plus_one. eapply exec_Ireturn; eauto. - simpl. constructor; auto. + rewrite H2; eauto. + constructor; auto. (* return some *) inv TS. exploit transl_expr_correct; eauto. intros [rs' [A [B [C D]]]]. - exploit match_stacks_call_cont; eauto. intros [U V]. + exploit match_stacks_call_cont; eauto. intros [U V]. + inversion TF. econstructor; split. - left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. traceEq. + left; eapply plus_right. eexact A. eapply exec_Ireturn; eauto. + rewrite H4; eauto. traceEq. simpl. rewrite C. constructor; auto. (* label *) @@ -1301,11 +1312,12 @@ Proof. induction 1. exploit function_ptr_translated; eauto. intros [tf [A B]]. econstructor; split. - econstructor. rewrite (transform_partial_program_main _ _ TRANSL). fold tge. - rewrite symbols_preserved. eexact H. + econstructor. apply (Genv.init_mem_transf_partial _ _ TRANSL); eauto. + rewrite (transform_partial_program_main _ _ TRANSL). fold tge. + rewrite symbols_preserved. eauto. eexact A. - rewrite <- H1. apply sig_transl_function; auto. - rewrite (Genv.init_mem_transf_partial _ _ TRANSL). constructor. auto. constructor. + rewrite <- H2. apply sig_transl_function; auto. + constructor. auto. constructor. Qed. Lemma transl_final_states: diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 037eb3fb..51fb945e 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -27,7 +27,7 @@ Require Import AST. Require Import Integers. Require Import Values. Require Import Events. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Switch. Require Import Op. diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index d8e2f212..68f38c0d 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -20,7 +20,7 @@ Require Import Op. Require Import Registers. Require Import Globalenvs. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Integers. Require Import Events. Require Import Smallstep. @@ -454,14 +454,6 @@ Proof. apply wt_regset_assign; auto. Qed. -Lemma wt_event_match: - forall ef args t res, - event_match ef args t res -> - Val.has_type res (proj_sig_res ef.(ef_sig)). -Proof. - induction 1. inversion H0; exact I. -Qed. - Inductive wt_stackframes: list stackframe -> option typ -> Prop := | wt_stackframes_nil: wt_stackframes nil (Some Tint) @@ -471,7 +463,7 @@ Inductive wt_stackframes: list stackframe -> option typ -> Prop := wt_regset env rs -> env res = match tyres with None => Tint | Some t => t end -> wt_stackframes s (sig_res (fn_sig f)) -> - wt_stackframes (Stackframe res (fn_code f) sp pc rs :: s) tyres. + wt_stackframes (Stackframe res f sp pc rs :: s) tyres. Inductive wt_state: state -> Prop := | wt_state_intro: @@ -479,7 +471,7 @@ Inductive wt_state: state -> Prop := (WT_STK: wt_stackframes s (sig_res (fn_sig f))) (WT_FN: wt_function f env) (WT_RS: wt_regset env rs), - wt_state (State s (fn_code f) sp pc rs m) + wt_state (State s f sp pc rs m) | wt_state_call: forall s f args m, wt_stackframes s (sig_res (funsig f)) -> @@ -517,7 +509,7 @@ Proof. econstructor; eauto. apply wt_regset_assign. auto. replace (env res) with (snd (type_of_operation op)). - apply type_of_operation_sound with fundef ge rs##args sp; auto. + apply type_of_operation_sound with fundef unit ge rs##args sp; auto. rewrite <- H6. reflexivity. (* Iload *) econstructor; eauto. @@ -526,29 +518,29 @@ Proof. (* Istore *) econstructor; eauto. (* Icall *) - assert (wt_fundef f). + assert (wt_fundef fd). destruct ros; simpl in H0. - pattern f. apply Genv.find_funct_prop with fundef unit p (rs#r). + pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r). exact wt_p. exact H0. caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0. - pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b. + pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b. exact wt_p. exact H0. discriminate. econstructor; eauto. econstructor; eauto. rewrite <- H7. apply wt_regset_list. auto. (* Itailcall *) - assert (wt_fundef f). + assert (wt_fundef fd). destruct ros; simpl in H0. - pattern f. apply Genv.find_funct_prop with fundef unit p (rs#r). + pattern fd. apply Genv.find_funct_prop with fundef unit p (rs#r). exact wt_p. exact H0. caseEq (Genv.find_symbol ge i); intros; rewrite H1 in H0. - pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b. + pattern fd. apply Genv.find_funct_ptr_prop with fundef unit p b. exact wt_p. exact H0. discriminate. econstructor; eauto. - rewrite H5; auto. - rewrite <- H6. apply wt_regset_list. auto. + rewrite H6; auto. + rewrite <- H7. apply wt_regset_list. auto. (* Icond *) econstructor; eauto. econstructor; eauto. @@ -557,7 +549,7 @@ Proof. (* Ireturn *) econstructor; eauto. destruct or; simpl in *. - rewrite <- H1. apply WT_RS. exact I. + rewrite <- H2. apply WT_RS. exact I. (* internal function *) simpl in *. inv H5. inversion H1; subst. econstructor; eauto. @@ -566,7 +558,7 @@ Proof. simpl in *. inv H5. econstructor; eauto. change (Val.has_type res (proj_sig_res (ef_sig ef))). - eapply wt_event_match; eauto. + eapply external_call_well_typed; eauto. (* return *) inv H1. econstructor; eauto. apply wt_regset_assign; auto. congruence. diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index 406ca07a..868fb8df 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -16,6 +16,7 @@ open Datatypes open Camlcoq open Maps open AST +open Memdata open Op open Registers open RTL diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index 21d5f380..7d730118 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -875,7 +875,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop := (AG: agree rs ls) (WT: wt_function f) (TL: is_tail c (LTLin.fn_code f)) - (MMD: Mem.lessdef m tm), + (MMD: Mem.extends m tm), match_states (LTLin.State s f sp c rs m) (Linear.State s' (transf_function f) sp (transf_code f c) ls tm) | match_states_call: @@ -885,7 +885,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop := (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call -> ls l = parent_locset s' l) (WT: wt_fundef f) - (MMD: Mem.lessdef m tm), + (MMD: Mem.extends m tm), match_states (LTLin.Callstate s f args m) (Linear.Callstate s' (transf_fundef f) ls tm) | match_states_return: @@ -894,7 +894,7 @@ Inductive match_states: LTLin.state -> Linear.state -> Prop := (AG: Val.lessdef res (ls (R (Conventions.loc_result sig)))) (PRES: forall l, ~In l temporaries -> ~In l destroyed_at_call -> ls l = parent_locset s' l) - (MMD: Mem.lessdef m tm), + (MMD: Mem.extends m tm), match_states (LTLin.Returnstate s res m) (Linear.Returnstate s' ls tm). @@ -1006,8 +1006,7 @@ Proof. rewrite B. eapply agree_locs; eauto. rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. destruct H1 as [ta [P Q]]. - exploit Mem.loadv_lessdef; eauto. - intros [tv [R S]]. + exploit Mem.loadv_extends; eauto. intros [tv [R S]]. exploit add_spill_correct. intros [ls3 [D [E F]]]. left; econstructor; split. @@ -1038,7 +1037,7 @@ Proof. destruct H1 as [ta [P Q]]. assert (X: Val.lessdef (rs src) (ls2 (R rsrc))). rewrite E. eapply agree_loc; eauto. - exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto. + exploit Mem.storev_extends. eexact MMD. eauto. eexact Q. eexact X. intros [tm2 [Y Z]]. left; econstructor; split. eapply plus_right. eauto. @@ -1072,7 +1071,7 @@ Proof. eapply agree_exten; eauto. apply Loc.diff_sym. apply loc_acceptable_noteq_diff. auto. red; intros; subst src. simpl in H8. intuition congruence. - exploit Mem.storev_lessdef. eexact MMD. eexact Q. eexact X. eauto. + exploit Mem.storev_extends. eexact MMD. eauto. eexact Q. eexact X. intros [tm2 [Y Z]]. left; econstructor; split. eapply star_plus_trans. eauto. @@ -1157,15 +1156,16 @@ Proof. ExploitWT. inversion WTI. subst ros0 args0. assert (WTF': wt_fundef f'). eapply find_function_wt; eauto. rewrite <- H0. + exploit Mem.free_parallel_extends; eauto. intros [tm' [FREE MMD']]. destruct ros as [fn | id]. (* indirect call *) - red in H4. destruct H4 as [OK1 [OK2 OK3]]. - rewrite <- H0 in H3. rewrite <- H0 in OK3. + red in H5. destruct H5 as [OK1 [OK2 OK3]]. + rewrite <- H0 in H4. rewrite <- H0 in OK3. destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero) args sig (add_reload fn IT1 (Ltailcall sig (inl ident IT1) :: transf_code f b)) - ls tm H3 H5) + ls tm H4 H6) as [ls2 [A [B C]]]. destruct (add_reload_correct tge s' (transf_function f) (Vptr stk Int.zero) fn IT1 (Ltailcall sig (inl ident IT1) :: transf_code f b) @@ -1191,13 +1191,12 @@ Proof. eapply match_stackframes_change_sig; eauto. rewrite return_regs_arguments; auto. congruence. exact (return_regs_preserve (parent_locset s') ls3). - apply Mem.free_lessdef; auto. (* direct call *) - rewrite <- H0 in H3. + rewrite <- H0 in H4. destruct (parallel_move_arguments_correct tge s' (transf_function f) (Vptr stk Int.zero) args sig (Ltailcall sig (inr mreg id) :: transf_code f b) - ls tm H3 H5) + ls tm H4 H6) as [ls3 [D [E F]]]. assert (ARGS: Val.lessdef_list (map rs args) (map ls3 (loc_arguments sig))). @@ -1214,7 +1213,6 @@ Proof. eapply match_stackframes_change_sig; eauto. rewrite return_regs_arguments; auto. congruence. exact (return_regs_preserve (parent_locset s') ls3). - apply Mem.free_lessdef; auto. (* Llabel *) left; econstructor; split. @@ -1272,29 +1270,29 @@ Proof. eapply LTLin.find_label_is_tail; eauto. (* Lreturn *) - ExploitWT; inv WTI. + ExploitWT; inv WTI. + exploit Mem.free_parallel_extends; eauto. intros [tm' [FREE MMD']]. destruct or; simpl. (* with an argument *) exploit add_reload_correct. intros [ls2 [A [B C]]]. left; econstructor; split. - eapply plus_right. eauto. eapply exec_Lreturn; eauto. + eapply plus_right. eauto. eapply exec_Lreturn; eauto. traceEq. econstructor; eauto. rewrite return_regs_result. rewrite B. apply agree_loc; auto. apply return_regs_preserve. - apply Mem.free_lessdef; auto. (* without an argument *) left; econstructor; split. apply plus_one. eapply exec_Lreturn; eauto. econstructor; eauto. apply return_regs_preserve. - apply Mem.free_lessdef; auto. (* internal function *) simpl in WT. inversion_clear WT. inversion H0. simpl in AG. - caseEq (alloc tm 0 (LTLin.fn_stacksize f)). intros tm' tstk TALLOC. - exploit Mem.alloc_lessdef; eauto. intros [P Q]. subst tstk. + exploit Mem.alloc_extends. eauto. eauto. + instantiate (1 := 0); omega. instantiate (1 := LTLin.fn_stacksize f); omega. + intros [tm' [ALLOC MMD']]. destruct (parallel_move_parameters_correct tge s' (transf_function f) (Vptr stk Int.zero) (LTLin.fn_params f) (LTLin.fn_sig f) (transf_code f (LTLin.fn_code f)) (call_regs ls) tm' @@ -1310,8 +1308,8 @@ Proof. econstructor; eauto with coqlib. (* external function *) - exploit event_match_lessdef; eauto. - intros [res' [A B]]. + exploit external_call_mem_extends; eauto. + intros [res' [tm' [A [B [C D]]]]]. left; econstructor; split. apply plus_one. eapply exec_function_external; eauto. econstructor; eauto. @@ -1338,16 +1336,15 @@ Lemma transf_initial_states: Proof. intros. inversion H. econstructor; split. - econstructor. - change (prog_main tprog) with (prog_main prog). + econstructor. + apply Genv.init_mem_transf; eauto. rewrite symbols_preserved. eauto. apply function_ptr_translated; eauto. rewrite sig_preserved. auto. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). - econstructor; eauto. constructor. rewrite H2; auto. - rewrite H2. simpl. constructor. + econstructor; eauto. constructor. rewrite H3; auto. + rewrite H3. simpl. constructor. eapply Genv.find_funct_ptr_prop; eauto. - apply Mem.lessdef_refl. symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf; auto. + apply Mem.extends_refl. Qed. Lemma transf_final_states: diff --git a/backend/Selection.v b/backend/Selection.v index 4355faf5..e822fdf7 100644 --- a/backend/Selection.v +++ b/backend/Selection.v @@ -28,7 +28,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/backend/Selectionproof.v b/backend/Selectionproof.v index 70cbeb41..1da7884e 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.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. @@ -300,7 +300,7 @@ Lemma functions_translated: Genv.find_funct tge v = Some (sel_fundef f). Proof. intros. - exact (Genv.find_funct_transf sel_fundef H). + exact (Genv.find_funct_transf sel_fundef _ _ H). Qed. Lemma function_ptr_translated: @@ -309,7 +309,7 @@ Lemma function_ptr_translated: Genv.find_funct_ptr tge b = Some (sel_fundef f). Proof. intros. - exact (Genv.find_funct_ptr_transf sel_fundef H). + exact (Genv.find_funct_ptr_transf sel_fundef _ _ H). Qed. Lemma sig_function_translated: @@ -428,6 +428,7 @@ Proof. econstructor; split. econstructor. destruct k; simpl in H; simpl; auto. rewrite <- H0; reflexivity. + simpl. eauto. constructor; auto. (* (* assign *) @@ -457,11 +458,11 @@ Proof. constructor; auto. destruct b; auto. (* Sreturn None *) econstructor; split. - econstructor. + econstructor. simpl; eauto. constructor; auto. apply call_cont_commut. (* Sreturn Some *) econstructor; split. - econstructor. simpl. eauto with evalexpr. + econstructor. simpl. eauto with evalexpr. simpl; eauto. constructor; auto. apply call_cont_commut. (* Sgoto *) econstructor; split. @@ -477,10 +478,10 @@ Proof. induction 1. econstructor; split. econstructor. - simpl. fold tge. rewrite symbols_preserved. eexact H. + apply Genv.init_mem_transf; eauto. + simpl. fold tge. rewrite symbols_preserved. eexact H0. apply function_ptr_translated. eauto. - rewrite <- H1. apply sig_function_translated; auto. - unfold tprog, sel_program. rewrite Genv.init_mem_transf. + rewrite <- H2. apply sig_function_translated; auto. constructor; auto. Qed. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index ba429589..f44eac2e 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -27,7 +27,7 @@ Require Import AST. Require Import Integers. Require Import Values. Require Import Op. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -1145,7 +1145,7 @@ Lemma functions_translated: exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf. Proof - (Genv.find_funct_transf_partial transf_fundef TRANSF). + (Genv.find_funct_transf_partial transf_fundef _ TRANSF). Lemma function_ptr_translated: forall v f, @@ -1153,7 +1153,7 @@ Lemma function_ptr_translated: exists tf, Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf. Proof - (Genv.find_funct_ptr_transf_partial transf_fundef TRANSF). + (Genv.find_funct_ptr_transf_partial transf_fundef _ TRANSF). Lemma sig_preserved: forall f tf, transf_fundef f = OK tf -> Mach.funsig tf = Linear.funsig f. @@ -1166,6 +1166,15 @@ Proof. intro. inversion H. reflexivity. Qed. +Lemma stacksize_preserved: + forall f tf, transf_function f = OK tf -> Mach.fn_stacksize tf = Linear.fn_stacksize f. +Proof. + intros until tf; unfold transf_function. + destruct (zlt (Linear.fn_stacksize f) 0). simpl; congruence. + destruct (zlt (- Int.min_signed) (fe_size (make_env (function_bounds f)))). simpl; congruence. + intros. inversion H; reflexivity. +Qed. + Lemma find_function_translated: forall f0 tf0 ls ls0 rs fr cs ros f, agree f0 tf0 ls ls0 rs fr cs -> @@ -1478,10 +1487,12 @@ Proof. simpl. intuition congruence. simpl. intuition congruence. econstructor; split. eapply plus_right. eexact A. - simpl shift_sp. eapply exec_Mtailcall; eauto. traceEq. + simpl shift_sp. eapply exec_Mtailcall; eauto. + rewrite (stacksize_preserved _ _ TRANSL); eauto. + traceEq. econstructor; eauto. intros; symmetry; eapply agree_return_regs; eauto. - intros. inv WTI. generalize (H3 _ H0). tauto. + intros. inv WTI. generalize (H4 _ H0). tauto. apply agree_callee_save_return_regs. (* Llabel *) @@ -1524,7 +1535,9 @@ Proof. intros [ls' [A [B C]]]. econstructor; split. eapply plus_right. eauto. - simpl shift_sp. econstructor; eauto. traceEq. + simpl shift_sp. econstructor; eauto. + rewrite (stacksize_preserved _ _ TRANSL); eauto. + traceEq. econstructor; eauto. intros. symmetry. eapply agree_return_regs; eauto. apply agree_callee_save_return_regs. @@ -1583,13 +1596,13 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. + eapply Genv.init_mem_transf_partial; eauto. rewrite (transform_partial_program_main _ _ TRANSF). rewrite symbols_preserved. eauto. eauto. - rewrite (Genv.init_mem_transf_partial _ _ TRANSF). econstructor; eauto. constructor. eapply Genv.find_funct_ptr_prop; eauto. - intros. rewrite H2 in H4. simpl in H4. contradiction. + intros. rewrite H3 in H5. simpl in H5. contradiction. simpl; red; auto. Qed. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 8681d84a..0ca4c028 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import AST. Require Import Integers. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Op. Require Import Events. Require Import Globalenvs. @@ -227,66 +227,6 @@ Proof. apply regset_set. auto. auto. Qed. -(** ** Agreement between the size of a stack block and a function *) - -(** To reason over deallocation of empty stack blocks, we need to - maintain the invariant that the bounds of a stack block - for function [f] are always [0, f.(fn_stacksize)]. *) - -Inductive match_stacksize: function -> block -> mem -> Z -> Prop := - | match_stacksize_intro: forall f sp m bound, - sp < bound -> - low_bound m sp = 0 -> - high_bound m sp = f.(fn_stacksize) -> - match_stacksize f sp m bound. - -Lemma match_stacksize_store: - forall m m' chunk b ofs v f sp bound, - store chunk m b ofs v = Some m' -> - match_stacksize f sp m bound -> - match_stacksize f sp m' bound. -Proof. - intros. inv H0. constructor. auto. - rewrite <- H2. eapply Mem.low_bound_store; eauto. - rewrite <- H3. eapply Mem.high_bound_store; eauto. -Qed. - -Lemma match_stacksize_alloc_other: - forall m m' lo hi b f sp bound, - alloc m lo hi = (m', b) -> - match_stacksize f sp m bound -> - bound <= m.(nextblock) -> - match_stacksize f sp m' bound. -Proof. - intros. inv H0. - assert (valid_block m sp). red. omega. - constructor. auto. - rewrite <- H3. eapply low_bound_alloc_other; eauto. - rewrite <- H4. eapply high_bound_alloc_other; eauto. -Qed. - -Lemma match_stacksize_alloc_same: - forall m f m' sp, - alloc m 0 f.(fn_stacksize) = (m', sp) -> - match_stacksize f sp m' m'.(nextblock). -Proof. - intros. constructor. - unfold alloc in H. inv H. simpl. omega. - eapply low_bound_alloc_same; eauto. - eapply high_bound_alloc_same; eauto. -Qed. - -Lemma match_stacksize_free: - forall f sp m b bound, - match_stacksize f sp m bound -> - bound <= b -> - match_stacksize f sp (free m b) bound. -Proof. - intros. inv H. constructor. auto. - rewrite <- H2. apply low_bound_free. unfold block; omega. - rewrite <- H3. apply high_bound_free. unfold block; omega. -Qed. - (** * Proof of semantic preservation *) Section PRESERVATION. @@ -319,6 +259,13 @@ Proof. destruct (zeq (fn_stacksize f) 0); auto. Qed. +Lemma stacksize_preserved: + forall f, fn_stacksize (transf_function f) = fn_stacksize f. +Proof. + unfold transf_function. intros. + destruct (zeq (fn_stacksize f) 0); auto. +Qed. + Lemma find_function_translated: forall ros rs rs' f, find_function ge ros rs = Some f -> @@ -370,131 +317,58 @@ We first define the simulation invariant between call stacks. The first two cases are standard, but the third case corresponds to a frame that was eliminated by the transformation. *) -Inductive match_stackframes: mem -> Z -> list stackframe -> list stackframe -> Prop := - | match_stackframes_nil: forall m bound, - match_stackframes m bound nil nil - | match_stackframes_normal: forall m bound stk stk' res sp pc rs rs' f, - match_stackframes m sp stk stk' -> - match_stacksize f sp m bound -> +Inductive match_stackframes: list stackframe -> list stackframe -> Prop := + | match_stackframes_nil: + match_stackframes nil nil + | match_stackframes_normal: forall stk stk' res sp pc rs rs' f, + match_stackframes stk stk' -> regset_lessdef rs rs' -> - match_stackframes m bound - (Stackframe res f.(fn_code) (Vptr sp Int.zero) pc rs :: stk) - (Stackframe res (transf_function f).(fn_code) (Vptr sp Int.zero) pc rs' :: stk') - | match_stackframes_tail: forall m bound stk stk' res sp pc rs f, - match_stackframes m sp stk stk' -> - match_stacksize f sp m bound -> + match_stackframes + (Stackframe res f (Vptr sp Int.zero) pc rs :: stk) + (Stackframe res (transf_function f) (Vptr sp Int.zero) pc rs' :: stk') + | match_stackframes_tail: forall stk stk' res sp pc rs f, + match_stackframes stk stk' -> is_return_spec f pc res -> f.(fn_stacksize) = 0 -> - match_stackframes m bound - (Stackframe res f.(fn_code) (Vptr sp Int.zero) pc rs :: stk) + match_stackframes + (Stackframe res f (Vptr sp Int.zero) pc rs :: stk) stk'. -(** In [match_stackframes m bound s s'], the memory state [m] is used - to check that the sizes of the stack blocks agree with what was - declared by the corresponding functions. The [bound] parameter - is used to enforce separation between the stack blocks. *) - -Lemma match_stackframes_incr: - forall m bound s s' bound', - match_stackframes m bound s s' -> - bound <= bound' -> - match_stackframes m bound' s s'. -Proof. - intros. inv H; econstructor; eauto. - inv H2. constructor; auto. omega. - inv H2. constructor; auto. omega. -Qed. - -Lemma match_stackframes_store: - forall m bound s s', - match_stackframes m bound s s' -> - forall chunk b ofs v m', - store chunk m b ofs v = Some m' -> - match_stackframes m' bound s s'. -Proof. - induction 1; intros. - constructor. - econstructor; eauto. eapply match_stacksize_store; eauto. - econstructor; eauto. eapply match_stacksize_store; eauto. -Qed. - -Lemma match_stackframes_alloc: - forall m lo hi m' sp s s', - match_stackframes m (nextblock m) s s' -> - alloc m lo hi = (m', sp) -> - match_stackframes m' sp s s'. -Proof. - intros. - assert (forall bound s s', - match_stackframes m bound s s' -> - bound <= m.(nextblock) -> - match_stackframes m' bound s s'). - induction 1; intros. constructor. - constructor; auto. apply IHmatch_stackframes; auto. inv H2. omega. - eapply match_stacksize_alloc_other; eauto. - econstructor; eauto. apply IHmatch_stackframes; auto. inv H2. omega. - eapply match_stacksize_alloc_other; eauto. - exploit alloc_result; eauto. intro. rewrite H2. - eapply H1; eauto. omega. -Qed. - -Lemma match_stackframes_free: - forall f sp m s s', - match_stacksize f sp m (nextblock m) -> - match_stackframes m sp s s' -> - match_stackframes (free m sp) (nextblock (free m sp)) s s'. -Proof. - intros. simpl. - assert (forall bound s s', - match_stackframes m bound s s' -> - bound <= sp -> - match_stackframes (free m sp) bound s s'). - induction 1; intros. constructor. - constructor; auto. apply IHmatch_stackframes; auto. inv H2; omega. - apply match_stacksize_free; auto. - econstructor; eauto. apply IHmatch_stackframes; auto. inv H2; omega. - apply match_stacksize_free; auto. - - apply match_stackframes_incr with sp. apply H1; auto. omega. - inv H. omega. -Qed. - (** Here is the invariant relating two states. The first three cases are standard. Note the ``less defined than'' conditions - over values, register states, and memory states. *) + over values and register states, and the corresponding ``extends'' + relation over memory states. *) Inductive match_states: state -> state -> Prop := | match_states_normal: forall s sp pc rs m s' rs' m' f - (STKSZ: match_stacksize f sp m m.(nextblock)) - (STACKS: match_stackframes m sp s s') + (STACKS: match_stackframes s s') (RLD: regset_lessdef rs rs') - (MLD: Mem.lessdef m m'), - match_states (State s f.(fn_code) (Vptr sp Int.zero) pc rs m) - (State s' (transf_function f).(fn_code) (Vptr sp Int.zero) pc rs' m') + (MLD: Mem.extends m m'), + match_states (State s f (Vptr sp Int.zero) pc rs m) + (State s' (transf_function f) (Vptr sp Int.zero) pc rs' m') | match_states_call: forall s f args m s' args' m', - match_stackframes m m.(nextblock) s s' -> + match_stackframes s s' -> Val.lessdef_list args args' -> - Mem.lessdef m m' -> + Mem.extends m m' -> match_states (Callstate s f args m) (Callstate s' (transf_fundef f) args' m') | match_states_return: forall s v m s' v' m', - match_stackframes m m.(nextblock) s s' -> + match_stackframes s s' -> Val.lessdef v v' -> - Mem.lessdef m m' -> + Mem.extends m m' -> match_states (Returnstate s v m) (Returnstate s' v' m') | match_states_interm: forall s sp pc rs m s' m' f r v' - (STKSZ: match_stacksize f sp m m.(nextblock)) - (STACKS: match_stackframes m sp s s') - (MLD: Mem.lessdef m m'), + (STACKS: match_stackframes s s') + (MLD: Mem.extends m m'), is_return_spec f pc r -> f.(fn_stacksize) = 0 -> Val.lessdef (rs#r) v' -> - match_states (State s f.(fn_code) (Vptr sp Int.zero) pc rs m) + match_states (State s f (Vptr sp Int.zero) pc rs m) (Returnstate s' v' m'). (** The last case of [match_states] corresponds to the execution @@ -516,7 +390,7 @@ Inductive match_states: state -> state -> Prop := Definition measure (st: state) : nat := match st with - | State s c sp pc rs m => (List.length s * (niter + 2) + return_measure c pc + 1)%nat + | State s f sp pc rs m => (List.length s * (niter + 2) + return_measure f.(fn_code) pc + 1)%nat | Callstate s f args m => 0%nat | Returnstate s v m => (List.length s * (niter + 2))%nat end. @@ -557,7 +431,7 @@ Proof. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. exploit eval_operation_lessdef; eauto. intros [v' [EVAL' VLD]]. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#res <- v') m'); split. eapply exec_Iop; eauto. rewrite <- EVAL'. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. apply regset_set; auto. @@ -571,9 +445,9 @@ Proof. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. exploit eval_addressing_lessdef; eauto. intros [a' [ADDR' ALD]]. - exploit loadv_lessdef; eauto. + exploit Mem.loadv_extends; eauto. intros [v' [LOAD' VLD]]. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' (rs'#dst <- v') m'); split. eapply exec_Iload with (a := a'). eauto. rewrite <- ADDR'. apply eval_addressing_preserved. exact symbols_preserved. eauto. econstructor; eauto. apply regset_set; auto. @@ -583,88 +457,91 @@ Proof. assert (Val.lessdef_list (rs##args) (rs'##args)). apply regset_get_list; auto. exploit eval_addressing_lessdef; eauto. intros [a' [ADDR' ALD]]. - exploit storev_lessdef. 4: eexact H1. eauto. eauto. apply RLD. + exploit Mem.storev_extends. 2: eexact H1. eauto. eauto. apply RLD. intros [m'1 [STORE' MLD']]. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'1); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'1); split. eapply exec_Istore with (a := a'). eauto. rewrite <- ADDR'. apply eval_addressing_preserved. exact symbols_preserved. eauto. destruct a; simpl in H1; try discriminate. econstructor; eauto. - eapply match_stacksize_store; eauto. - rewrite (nextblock_store _ _ _ _ _ _ H1). auto. - eapply match_stackframes_store; eauto. (* call *) exploit find_function_translated; eauto. intro FIND'. TransfInstr. (* call turned tailcall *) - left. exists (Callstate s' (transf_fundef f) (rs'##args) (Mem.free m' sp0)); split. + assert ({ m'' | Mem.free m' sp0 0 (fn_stacksize (transf_function f)) = Some m''}). + apply Mem.range_perm_free. rewrite stacksize_preserved. rewrite H7. + red; intros; omegaContradiction. + destruct X as [m'' FREE]. + left. exists (Callstate s' (transf_fundef fd) (rs'##args) m''); split. eapply exec_Itailcall; eauto. apply sig_preserved. constructor. eapply match_stackframes_tail; eauto. apply regset_get_list; auto. - apply Mem.free_right_lessdef; auto. inv STKSZ. omega. + eapply Mem.free_right_extends; eauto. + rewrite stacksize_preserved. rewrite H7. intros. omegaContradiction. (* call that remains a call *) - left. exists (Callstate (Stackframe res (fn_code (transf_function f0)) (Vptr sp0 Int.zero) pc' rs' :: s') - (transf_fundef f) (rs'##args) m'); split. + left. exists (Callstate (Stackframe res (transf_function f) (Vptr sp0 Int.zero) pc' rs' :: s') + (transf_fundef fd) (rs'##args) m'); split. eapply exec_Icall; eauto. apply sig_preserved. constructor. constructor; auto. apply regset_get_list; auto. auto. (* tailcall *) - exploit find_function_translated; eauto. intro FIND'. + exploit find_function_translated; eauto. intro FIND'. + exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]]. TransfInstr. - left. exists (Callstate s' (transf_fundef f) (rs'##args) (Mem.free m' stk)); split. - eapply exec_Itailcall; eauto. apply sig_preserved. - constructor. eapply match_stackframes_free; eauto. - apply regset_get_list; auto. apply Mem.free_lessdef; auto. + left. exists (Callstate s' (transf_fundef fd) (rs'##args) m'1); split. + eapply exec_Itailcall; eauto. apply sig_preserved. + rewrite stacksize_preserved; auto. + constructor. auto. apply regset_get_list; auto. auto. (* cond true *) TransfInstr. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) ifso rs' m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifso rs' m'); split. eapply exec_Icond_true; eauto. apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto. constructor; auto. (* cond false *) TransfInstr. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) ifnot rs' m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) ifnot rs' m'); split. eapply exec_Icond_false; eauto. apply eval_condition_lessdef with (rs##args); auto. apply regset_get_list; auto. constructor; auto. (* jumptable *) TransfInstr. - left. exists (State s' (fn_code (transf_function f)) (Vptr sp0 Int.zero) pc' rs' m'); split. + left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'); split. eapply exec_Ijumptable; eauto. generalize (RLD arg). rewrite H0. intro. inv H2. auto. constructor; auto. (* return *) + exploit Mem.free_parallel_extends; eauto. intros [m'1 [FREE EXT]]. TransfInstr. - left. exists (Returnstate s' (regmap_optget or Vundef rs') (free m' stk)); split. - apply exec_Ireturn; auto. - constructor. - eapply match_stackframes_free; eauto. + left. exists (Returnstate s' (regmap_optget or Vundef rs') m'1); split. + apply exec_Ireturn; auto. rewrite stacksize_preserved; auto. + constructor. auto. destruct or; simpl. apply RLD. constructor. - apply Mem.free_lessdef; auto. + auto. (* eliminated return None *) assert (or = None) by congruence. subst or. right. split. simpl. omega. split. auto. - constructor. - eapply match_stackframes_free; eauto. + constructor. auto. simpl. constructor. - apply Mem.free_left_lessdef; auto. + eapply Mem.free_left_extends; eauto. (* eliminated return Some *) assert (or = Some r) by congruence. subst or. right. split. simpl. omega. split. auto. - constructor. - eapply match_stackframes_free; eauto. + constructor. auto. simpl. auto. - apply Mem.free_left_lessdef; auto. + eapply Mem.free_left_extends; eauto. (* internal call *) - caseEq (alloc m'0 0 (fn_stacksize f)). intros m'1 stk' ALLOC'. - exploit alloc_lessdef; eauto. intros [EQ1 LD']. subst stk'. + exploit Mem.alloc_extends; eauto. + instantiate (1 := 0). omega. + instantiate (1 := fn_stacksize f). omega. + intros [m'1 [ALLOC EXT]]. assert (fn_stacksize (transf_function f) = fn_stacksize f /\ fn_entrypoint (transf_function f) = fn_entrypoint f /\ fn_params (transf_function f) = fn_params f). @@ -673,13 +550,12 @@ Proof. left. econstructor; split. simpl. eapply exec_function_internal; eauto. rewrite EQ1; eauto. rewrite EQ2. rewrite EQ3. constructor; auto. - eapply match_stacksize_alloc_same; eauto. - eapply match_stackframes_alloc; eauto. apply regset_init_regs. auto. (* external call *) - exploit event_match_lessdef; eauto. intros [res' [EVM' VLD']]. - left. exists (Returnstate s' res' m'); split. + exploit external_call_mem_extends; eauto. + intros [res' [m2' [A [B [C D]]]]]. + left. exists (Returnstate s' res' m2'); split. simpl. econstructor; eauto. constructor; auto. @@ -705,15 +581,13 @@ Lemma transf_initial_states: Proof. intros. inv H. exploit funct_ptr_translated; eauto. intro FIND. - exists (Callstate nil (transf_fundef f) nil (Genv.init_mem tprog)); split. - econstructor; eauto. + exists (Callstate nil (transf_fundef f) nil m0); split. + econstructor; eauto. apply Genv.init_mem_transf. auto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. reflexivity. - rewrite <- H2. apply sig_preserved. - replace (Genv.init_mem tprog) with (Genv.init_mem prog). - constructor. constructor. constructor. apply lessdef_refl. - symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. + rewrite <- H3. apply sig_preserved. + constructor. constructor. constructor. apply Mem.extends_refl. Qed. Lemma transf_final_states: diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 92ec68cf..4cbcbd4f 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import UnionFind. Require Import AST. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -348,15 +348,14 @@ Lemma transf_initial_states: exists st2, initial_state tp st2 /\ match_states st1 st2. Proof. intros. inversion H. - exists (Callstate nil (tunnel_fundef f) nil (Genv.init_mem tp)); split. + exists (Callstate nil (tunnel_fundef f) nil m0); split. econstructor; eauto. + apply Genv.init_mem_transf; auto. change (prog_main tp) with (prog_main p). rewrite symbols_preserved. eauto. apply function_ptr_translated; auto. - rewrite <- H2. apply sig_preserved. - replace (Genv.init_mem tp) with (Genv.init_mem p). - constructor. constructor. auto. - symmetry. unfold tp, tunnel_program. apply Genv.init_mem_transf. + rewrite <- H3. apply sig_preserved. + constructor. constructor. Qed. Lemma transf_final_states: diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index 834e8e18..743b4681 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.v @@ -17,7 +17,7 @@ Require Import Maps. Require Import UnionFind. Require Import AST. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Op. Require Import Locations. |