From a74f6b45d72834b5b8417297017bd81424123d98 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 7 Mar 2010 15:52:58 +0000 Subject: 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 --- cfrontend/Cminorgen.v | 285 +++-- cfrontend/Cminorgenproof.v | 2543 ++++++++++++++++++++++++++------------------ cfrontend/Csem.v | 85 +- cfrontend/Csharpminor.v | 101 +- cfrontend/Cshmgen.v | 7 +- cfrontend/Cshmgenproof1.v | 36 +- cfrontend/Cshmgenproof2.v | 2 +- cfrontend/Cshmgenproof3.v | 194 ++-- 8 files changed, 1957 insertions(+), 1296 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index f48b0ab8..ba3a2bfa 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -20,9 +20,8 @@ Require Import Maps. Require Import Ordered. Require Import AST. Require Import Integers. -Require Mem. +Require Import Memdata. Require Import Csharpminor. -Require Import Op. Require Import Cminor. Open Local Scope string_scope. @@ -49,14 +48,132 @@ Open Local Scope error_monad_scope. of Cminor. *) -(** Translation of constants. *) +(** Compile-time information attached to each Csharpminor + variable: global variables, local variables, function parameters. + [Var_local] denotes a scalar local variable whose address is not + taken; it will be translated to a Cminor local variable of the + same name. [Var_stack_scalar] and [Var_stack_array] denote + local variables that are stored as sub-blocks of the Cminor stack + data block. [Var_global_scalar] and [Var_global_array] denote + global variables, stored in the global symbols with the same names. *) -Definition transl_constant (cst: Csharpminor.constant): constant := - match cst with - | Csharpminor.Ointconst n => Ointconst n - | Csharpminor.Ofloatconst n => Ofloatconst n +Inductive var_info: Type := + | Var_local: memory_chunk -> var_info + | Var_stack_scalar: memory_chunk -> Z -> var_info + | Var_stack_array: Z -> var_info + | Var_global_scalar: memory_chunk -> var_info + | Var_global_array: var_info. + +Definition compilenv := PMap.t var_info. + +(** Infer the type or memory chunk of the result of an expression. *) + +Definition chunktype_const (c: Csharpminor.constant) := + match c with + | Csharpminor.Ointconst n => Mint32 + | Csharpminor.Ofloatconst n => Mfloat64 end. +Definition chunktype_unop (op: unary_operation) := + match op with + | Ocast8unsigned => Mint8unsigned + | Ocast8signed => Mint8signed + | Ocast16unsigned => Mint16unsigned + | Ocast16signed => Mint16signed + | Onegint => Mint32 + | Onotbool => Mint32 + | Onotint => Mint32 + | Onegf => Mfloat64 + | Oabsf => Mfloat64 + | Osingleoffloat => Mfloat32 + | Ointoffloat => Mint32 + | Ointuoffloat => Mint32 + | Ofloatofint => Mfloat64 + | Ofloatofintu => Mfloat64 + end. + +Definition chunktype_binop (op: binary_operation) := + match op with + | Oadd => Mint32 + | Osub => Mint32 + | Omul => Mint32 + | Odiv => Mint32 + | Odivu => Mint32 + | Omod => Mint32 + | Omodu => Mint32 + | Oand => Mint32 + | Oor => Mint32 + | Oxor => Mint32 + | Oshl => Mint32 + | Oshr => Mint32 + | Oshru => Mint32 + | Oaddf => Mfloat64 + | Osubf => Mfloat64 + | Omulf => Mfloat64 + | Odivf => Mfloat64 + | Ocmp c => Mint8unsigned + | Ocmpu c => Mint8unsigned + | Ocmpf c => Mint8unsigned + end. + +Definition chunktype_compat (src dst: memory_chunk) : bool := + match src, dst with + | Mint8unsigned, (Mint8unsigned|Mint16unsigned|Mint16signed|Mint32) => true + | Mint8signed, (Mint8signed|Mint16unsigned|Mint16signed|Mint32) => true + | Mint16unsigned, (Mint16unsigned|Mint32) => true + | Mint16signed, (Mint16signed|Mint32) => true + | Mint32, Mint32 => true + | Mfloat32, (Mfloat32|Mfloat64) => true + | Mfloat64, Mfloat64 => true + | _, _ => false + end. + +Definition chunk_for_type (ty: typ) : memory_chunk := + match ty with Tint => Mint32 | Tfloat => Mfloat64 end. + +Definition chunktype_merge (c1 c2: memory_chunk) : res memory_chunk := + if chunktype_compat c1 c2 then + OK c2 + else if chunktype_compat c2 c1 then + OK c1 + else if typ_eq (type_of_chunk c1) (type_of_chunk c2) then + OK (chunk_for_type (type_of_chunk c1)) + else + Error(msg "Cminorgen: chunktype_merge"). + +Fixpoint chunktype_expr (cenv: compilenv) (e: Csharpminor.expr) + {struct e}: res memory_chunk := + match e with + | Csharpminor.Evar id => + match cenv!!id with + | Var_local chunk => OK chunk + | Var_stack_scalar chunk ofs => OK chunk + | Var_global_scalar chunk => OK chunk + | _ => Error(msg "Cminorgen.chunktype_expr") + end + | Csharpminor.Eaddrof id => + OK Mint32 + | Csharpminor.Econst cst => + OK (chunktype_const cst) + | Csharpminor.Eunop op e1 => + OK (chunktype_unop op) + | Csharpminor.Ebinop op e1 e2 => + OK (chunktype_binop op) + | Csharpminor.Eload chunk e => + OK chunk + | Csharpminor.Econdition e1 e2 e3 => + do chunk2 <- chunktype_expr cenv e2; + do chunk3 <- chunktype_expr cenv e3; + chunktype_merge chunk2 chunk3 + end. + +Definition type_expr (cenv: compilenv) (e: Csharpminor.expr): res typ := + do c <- chunktype_expr cenv e; OK(type_of_chunk c). + +Definition type_exprlist (cenv: compilenv) (el: list Csharpminor.expr): + res (list typ) := + mmap (type_expr cenv) el. + (** [make_cast chunk e] returns a Cminor expression that normalizes the value of Cminor expression [e] as prescribed by the memory chunk [chunk]. For instance, 8-bit sign extension is performed if @@ -74,10 +191,9 @@ Definition make_cast (chunk: memory_chunk) (e: expr): expr := end. (** When the translation of an expression is stored in memory, - the normalization performed by [make_cast] can be redundant + a cast at the toplevel of the expression can be redundant with that implicitly performed by the memory store. - [store_arg] detects this case and strips away the redundant - normalization. *) + [store_arg] detects this case and strips away the redundant cast. *) Definition store_arg (chunk: memory_chunk) (e: expr) : expr := match e with @@ -103,26 +219,7 @@ Definition make_stackaddr (ofs: Z): expr := Definition make_globaladdr (id: ident): expr := Econst (Oaddrsymbol id Int.zero). -(** Compile-time information attached to each Csharpminor - variable: global variables, local variables, function parameters. - [Var_local] denotes a scalar local variable whose address is not - taken; it will be translated to a Cminor local variable of the - same name. [Var_stack_scalar] and [Var_stack_array] denote - local variables that are stored as sub-blocks of the Cminor stack - data block. [Var_global_scalar] and [Var_global_array] denote - global variables, stored in the global symbols with the same names. *) - -Inductive var_info: Type := - | Var_local: memory_chunk -> var_info - | Var_stack_scalar: memory_chunk -> Z -> var_info - | Var_stack_array: Z -> var_info - | Var_global_scalar: memory_chunk -> var_info - | Var_global_array: var_info. - -Definition compilenv := PMap.t var_info. - -(** Generation of Cminor code corresponding to accesses to Csharpminor - local variables: reads, assignments, and taking the address of. *) +(** Generation of a Cminor expression for reading a Csharpminor variable. *) Definition var_get (cenv: compilenv) (id: ident): res expr := match PMap.get id cenv with @@ -136,24 +233,67 @@ Definition var_get (cenv: compilenv) (id: ident): res expr := Error(msg "Cminorgen.var_get") end. -Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): res stmt := +(** Generation of a Cminor expression for taking the address of + a Csharpminor variable. *) + +Definition var_addr (cenv: compilenv) (id: ident): res expr := + match PMap.get id cenv with + | Var_local chunk => Error(msg "Cminorgen.var_addr") + | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs) + | Var_stack_array ofs => OK (make_stackaddr ofs) + | _ => OK (make_globaladdr id) + end. + +(** Generation of a Cminor statement performing an assignment to + a variable. [rhs_chunk] is the inferred chunk type for the + right-hand side. If the variable was allocated to a Cminor variable, + a cast may need to be inserted to normalize the value of the r.h.s., + as per Csharpminor's semantics. *) + +Definition var_set (cenv: compilenv) + (id: ident) (rhs: expr) (rhs_chunk: memory_chunk): res stmt := match PMap.get id cenv with | Var_local chunk => - OK(Sassign id (make_cast chunk rhs)) + if chunktype_compat rhs_chunk chunk then + OK(Sassign id rhs) + else if typ_eq (type_of_chunk chunk) (type_of_chunk rhs_chunk) then + OK(Sassign id (make_cast chunk rhs)) + else + Error(msg "Cminorgen.var_set.1") | Var_stack_scalar chunk ofs => OK(make_store chunk (make_stackaddr ofs) rhs) | Var_global_scalar chunk => OK(make_store chunk (make_globaladdr id) rhs) | _ => - Error(msg "Cminorgen.var_set") + Error(msg "Cminorgen.var_set.2") end. -Definition var_addr (cenv: compilenv) (id: ident): res expr := +(** A variant of [var_set] used for initializing function parameters + and storing the return values of function calls. The value to + be stored already resides in the Cminor variable called [id]. + Moreover, its chunk type is not known, only its int-or-float type. *) + +Definition var_set_self (cenv: compilenv) (id: ident) (ty: typ): res stmt := match PMap.get id cenv with - | Var_local chunk => Error(msg "Cminorgen.var_addr") - | Var_stack_scalar chunk ofs => OK (make_stackaddr ofs) - | Var_stack_array ofs => OK (make_stackaddr ofs) - | _ => OK (make_globaladdr id) + | Var_local chunk => + if typ_eq (type_of_chunk chunk) ty then + OK(Sassign id (make_cast chunk (Evar id))) + else + Error(msg "Cminorgen.var_set_self.1") + | Var_stack_scalar chunk ofs => + OK(make_store chunk (make_stackaddr ofs) (Evar id)) + | Var_global_scalar chunk => + OK(make_store chunk (make_globaladdr id) (Evar id)) + | _ => + Error(msg "Cminorgen.var_set_self.2") + end. + +(** Translation of constants. *) + +Definition transl_constant (cst: Csharpminor.constant): constant := + match cst with + | Csharpminor.Ointconst n => Ointconst n + | Csharpminor.Ofloatconst n => Ofloatconst n end. (** Translation of expressions. All the hard work is done by the @@ -234,16 +374,27 @@ Fixpoint switch_env (ls: lbl_stmt) (e: exit_env) {struct ls}: exit_env := | LScase _ _ ls' => false :: switch_env ls' e end. -(** Translation of statements. The only nonobvious part is - the translation of [switch] statements, outlined above. *) +(** Translation of statements. The nonobvious part is + the translation of [switch] statements, outlined above. + Also note the additional type checks on arguments to calls and returns. + These checks should always succeed for C#minor code generated from + well-typed Clight code, but are necessary for the correctness proof + to go through. +*) + +Definition typ_of_opttyp (ot: option typ) := + match ot with None => Tint | Some t => t end. -Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) +Fixpoint transl_stmt (ret: option typ) (cenv: compilenv) + (xenv: exit_env) (s: Csharpminor.stmt) {struct s}: res stmt := match s with | Csharpminor.Sskip => OK Sskip | Csharpminor.Sassign id e => - do te <- transl_expr cenv e; var_set cenv id te + do chunk <- chunktype_expr cenv e; + do te <- transl_expr cenv e; + var_set cenv id te chunk | Csharpminor.Sstore chunk e1 e2 => do te1 <- transl_expr cenv e1; do te2 <- transl_expr cenv e2; @@ -251,26 +402,32 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) | Csharpminor.Scall None sig e el => do te <- transl_expr cenv e; do tel <- transl_exprlist cenv el; - OK (Scall None sig te tel) + do tyl <- type_exprlist cenv el; + if list_eq_dec typ_eq tyl sig.(sig_args) + then OK (Scall None sig te tel) + else Error(msg "Cminorgen.transl_stmt(call0)") | Csharpminor.Scall (Some id) sig e el => do te <- transl_expr cenv e; do tel <- transl_exprlist cenv el; - do s <- var_set cenv id (Evar id); - OK (Sseq (Scall (Some id) sig te tel) s) + do tyl <- type_exprlist cenv el; + do s <- var_set_self cenv id (proj_sig_res sig); + if list_eq_dec typ_eq tyl sig.(sig_args) + then OK (Sseq (Scall (Some id) sig te tel) s) + else Error(msg "Cminorgen.transl_stmt(call1)") | Csharpminor.Sseq s1 s2 => - do ts1 <- transl_stmt cenv xenv s1; - do ts2 <- transl_stmt cenv xenv s2; + do ts1 <- transl_stmt ret cenv xenv s1; + do ts2 <- transl_stmt ret cenv xenv s2; OK (Sseq ts1 ts2) | Csharpminor.Sifthenelse e s1 s2 => do te <- transl_expr cenv e; - do ts1 <- transl_stmt cenv xenv s1; - do ts2 <- transl_stmt cenv xenv s2; + do ts1 <- transl_stmt ret cenv xenv s1; + do ts2 <- transl_stmt ret cenv xenv s2; OK (Sifthenelse te ts1 ts2) | Csharpminor.Sloop s => - do ts <- transl_stmt cenv xenv s; + do ts <- transl_stmt ret cenv xenv s; OK (Sloop ts) | Csharpminor.Sblock s => - do ts <- transl_stmt cenv (true :: xenv) s; + do ts <- transl_stmt ret cenv (true :: xenv) s; OK (Sblock ts) | Csharpminor.Sexit n => OK (Sexit (shift_exit xenv n)) @@ -278,27 +435,31 @@ Fixpoint transl_stmt (cenv: compilenv) (xenv: exit_env) (s: Csharpminor.stmt) let cases := switch_table ls O in let default := length cases in do te <- transl_expr cenv e; - transl_lblstmt cenv (switch_env ls xenv) ls (Sswitch te cases default) + transl_lblstmt ret cenv (switch_env ls xenv) ls (Sswitch te cases default) | Csharpminor.Sreturn None => OK (Sreturn None) | Csharpminor.Sreturn (Some e) => - do te <- transl_expr cenv e; OK (Sreturn (Some te)) + do te <- transl_expr cenv e; + do ty <- type_expr cenv e; + if typ_eq ty (typ_of_opttyp ret) + then OK (Sreturn (Some te)) + else Error(msg "Cminorgen.transl_stmt(return)") | Csharpminor.Slabel lbl s => - do ts <- transl_stmt cenv xenv s; OK (Slabel lbl ts) + do ts <- transl_stmt ret cenv xenv s; OK (Slabel lbl ts) | Csharpminor.Sgoto lbl => OK (Sgoto lbl) end -with transl_lblstmt (cenv: compilenv) (xenv: exit_env) - (ls: Csharpminor.lbl_stmt) (body: stmt) +with transl_lblstmt (ret: option typ) (cenv: compilenv) + (xenv: exit_env) (ls: Csharpminor.lbl_stmt) (body: stmt) {struct ls}: res stmt := match ls with | Csharpminor.LSdefault s => - do ts <- transl_stmt cenv xenv s; + do ts <- transl_stmt ret cenv xenv s; OK (Sseq (Sblock body) ts) | Csharpminor.LScase _ s ls' => - do ts <- transl_stmt cenv xenv s; - transl_lblstmt cenv (List.tail xenv) ls' (Sseq (Sblock body) ts) + do ts <- transl_stmt ret cenv xenv s; + transl_lblstmt ret cenv (List.tail xenv) ls' (Sseq (Sblock body) ts) end. (** Computation of the set of variables whose address is taken in @@ -379,7 +540,7 @@ Definition assign_variable (PMap.set id (Var_stack_array ofs) cenv, ofs + Zmax 0 sz) | (id, Vscalar chunk) => if Identset.mem id atk then - let sz := Mem.size_chunk chunk in + let sz := size_chunk chunk in let ofs := align stacksize sz in (PMap.set id (Var_stack_scalar chunk ofs) cenv, ofs + sz) else @@ -425,7 +586,7 @@ Fixpoint store_parameters match params with | nil => OK Sskip | (id, chunk) :: rem => - do s1 <- var_set cenv id (Evar id); + do s1 <- var_set_self cenv id (type_of_chunk chunk); do s2 <- store_parameters cenv rem; OK (Sseq s1 s2) end. @@ -471,7 +632,7 @@ Definition make_vars (params: list ident) (vars: list ident) Definition transl_funbody (cenv: compilenv) (stacksize: Z) (f: Csharpminor.function): res function := - do tbody <- transl_stmt cenv nil f.(Csharpminor.fn_body); + do tbody <- transl_stmt f.(fn_return) cenv nil f.(Csharpminor.fn_body); do sparams <- store_parameters cenv f.(Csharpminor.fn_params); OK (mkfunction (Csharpminor.fn_sig f) diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index a472e709..c79555c0 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -12,20 +12,23 @@ (** Correctness proof for Cminor generation. *) +Require Import Coq.Program.Equality. Require Import FSets. Require Import Coqlib. +Require Intv. Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memdata. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. +Require Import Switch. Require Import Csharpminor. -Require Import Op. Require Import Cminor. Require Import Cminorgen. @@ -51,20 +54,19 @@ Lemma function_ptr_translated: Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef gce f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar TRANSL). - +Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). Lemma functions_translated: forall (v: val) (f: Csharpminor.fundef), Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef gce f = OK tf. -Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL). +Proof (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). Lemma sig_preserved_body: forall f tf cenv size, transl_funbody cenv size f = OK tf -> - tf.(fn_sig) = f.(Csharpminor.fn_sig). + tf.(fn_sig) = Csharpminor.fn_sig f. Proof. intros. monadInv H. reflexivity. Qed. @@ -112,6 +114,193 @@ Proof. intro. rewrite PMap.gi. auto. Qed. +(** * Derived properties of memory operations *) + +Lemma load_freelist: + forall fbl chunk m b ofs m', + (forall b' lo hi, In (b', lo, hi) fbl -> b' <> b) -> + Mem.free_list m fbl = Some m' -> + Mem.load chunk m' b ofs = Mem.load chunk m b ofs. +Proof. + induction fbl; intros. + simpl in H0. congruence. + destruct a as [[b' lo] hi]. + generalize H0. simpl. case_eq (Mem.free m b' lo hi); try congruence. + intros m1 FR1 FRL. + transitivity (Mem.load chunk m1 b ofs). + eapply IHfbl; eauto. intros. eapply H. eauto with coqlib. + eapply Mem.load_free; eauto. left. apply sym_not_equal. eapply H. auto with coqlib. +Qed. + +Lemma perm_freelist: + forall fbl m m' b ofs p, + Mem.free_list m fbl = Some m' -> + Mem.perm m' b ofs p -> + Mem.perm m b ofs p. +Proof. + induction fbl; simpl; intros until p. + congruence. + destruct a as [[b' lo] hi]. case_eq (Mem.free m b' lo hi); try congruence. + intros. eauto with mem. +Qed. + +Lemma nextblock_freelist: + forall fbl m m', + Mem.free_list m fbl = Some m' -> + Mem.nextblock m' = Mem.nextblock m. +Proof. + induction fbl; intros until m'; simpl. + congruence. + destruct a as [[b lo] hi]. + case_eq (Mem.free m b lo hi); intros; try congruence. + transitivity (Mem.nextblock m0). eauto. eapply Mem.nextblock_free; eauto. +Qed. + +Lemma free_list_freeable: + forall l m m', + Mem.free_list m l = Some m' -> + forall b lo hi, + In (b, lo, hi) l -> Mem.range_perm m b lo hi Freeable. +Proof. + induction l; simpl; intros. + contradiction. + revert H. destruct a as [[b' lo'] hi']. + caseEq (Mem.free m b' lo' hi'); try congruence. + intros m1 FREE1 FREE2. + destruct H0. inv H. + eauto with mem. + red; intros. eapply Mem.perm_free_3; eauto. exploit IHl; eauto. +Qed. + +Lemma bounds_freelist: + forall b l m m', + Mem.free_list m l = Some m' -> Mem.bounds m' b = Mem.bounds m b. +Proof. + induction l; simpl; intros. + inv H; auto. + revert H. destruct a as [[b' lo'] hi']. + caseEq (Mem.free m b' lo' hi'); try congruence. + intros m1 FREE1 FREE2. + transitivity (Mem.bounds m1 b). eauto. eapply Mem.bounds_free; eauto. +Qed. + +Lemma nextblock_storev: + forall chunk m addr v m', + Mem.storev chunk m addr v = Some m' -> Mem.nextblock m' = Mem.nextblock m. +Proof. + unfold Mem.storev; intros. destruct addr; try discriminate. + eapply Mem.nextblock_store; eauto. +Qed. + +(** * Normalized values and operations over memory chunks *) + +(** A value is normalized with respect to a memory chunk if it is + invariant under the cast (truncation, sign extension) corresponding to + the chunk. *) + +Definition val_normalized (v: val) (chunk: memory_chunk) : Prop := + Val.load_result chunk v = v. + +Lemma val_normalized_has_type: + forall chunk v, val_normalized v chunk -> Val.has_type v (type_of_chunk chunk). +Proof. + intros until v; unfold val_normalized, Val.load_result. + destruct chunk; destruct v; intro EQ; try (inv EQ); simpl; exact I. +Qed. + +Lemma val_has_type_normalized: + forall ty v, Val.has_type v ty -> val_normalized v (chunk_for_type ty). +Proof. + unfold Val.has_type, val_normalized; intros; destruct ty; destruct v; + contradiction || reflexivity. +Qed. + +Lemma chunktype_const_correct: + forall c v, + Csharpminor.eval_constant c = Some v -> + val_normalized v (chunktype_const c). +Proof. + unfold Csharpminor.eval_constant; intros. + destruct c; inv H; unfold val_normalized; auto. +Qed. + +Lemma chunktype_unop_correct: + forall op v1 v, + Csharpminor.eval_unop op v1 = Some v -> + val_normalized v (chunktype_unop op). +Proof. + intros; destruct op; simpl in *; unfold val_normalized. + inv H. destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. compute; auto. + inv H. destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto. + inv H. destruct v1; simpl; auto. rewrite Int.zero_ext_idem; auto. compute; auto. + inv H. destruct v1; simpl; auto. rewrite Int.sign_ext_idem; auto. compute; auto. + destruct v1; inv H; auto. + destruct v1; inv H. destruct (Int.eq i Int.zero); auto. reflexivity. + destruct v1; inv H; auto. + destruct v1; inv H; auto. + destruct v1; inv H; auto. + inv H. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem; auto. + destruct v1; inv H; auto. + destruct v1; inv H; auto. + destruct v1; inv H; auto. + destruct v1; inv H; auto. +Qed. + +Lemma chunktype_binop_correct: + forall op v1 v2 m v, + Csharpminor.eval_binop op v1 v2 m = Some v -> + val_normalized v (chunktype_binop op). +Proof. + intros; destruct op; simpl in *; unfold val_normalized; + destruct v1; destruct v2; try (inv H; reflexivity). + destruct (eq_block b b0); inv H; auto. + destruct (Int.eq i0 Int.zero); inv H; auto. + destruct (Int.eq i0 Int.zero); inv H; auto. + destruct (Int.eq i0 Int.zero); inv H; auto. + destruct (Int.eq i0 Int.zero); inv H; auto. + destruct (Int.ltu i0 Int.iwordsize); inv H; auto. + destruct (Int.ltu i0 Int.iwordsize); inv H; auto. + destruct (Int.ltu i0 Int.iwordsize); inv H; auto. + inv H; destruct (Int.cmp c i i0); reflexivity. + unfold eval_compare_null in H. destruct (Int.eq i Int.zero). + destruct c; inv H; auto. inv H. + unfold eval_compare_null in H. destruct (Int.eq i0 Int.zero). + destruct c; inv H; auto. inv H. + destruct (Mem.valid_pointer m b (Int.signed i) && + Mem.valid_pointer m b0 (Int.signed i0)). + destruct (eq_block b b0); inv H. destruct (Int.cmp c i i0); auto. + destruct c; inv H1; auto. inv H. + inv H. destruct (Int.cmpu c i i0); auto. + inv H. destruct (Float.cmp c f f0); auto. +Qed. + +Lemma chunktype_compat_correct: + forall src dst v, + chunktype_compat src dst = true -> + val_normalized v src -> val_normalized v dst. +Proof. + unfold val_normalized; intros. rewrite <- H0. + destruct src; destruct dst; simpl in H; try discriminate; auto; + destruct v; simpl; auto. +Admitted. + +Lemma chunktype_merge_correct: + forall c1 c2 c v, + chunktype_merge c1 c2 = OK c -> + val_normalized v c1 \/ val_normalized v c2 -> + val_normalized v c. +Proof. + intros until v. unfold chunktype_merge. + case_eq (chunktype_compat c1 c2). + intros. inv H0. destruct H1. eapply chunktype_compat_correct; eauto. auto. + case_eq (chunktype_compat c2 c1). + intros. inv H1. destruct H2. auto. eapply chunktype_compat_correct; eauto. + intros. destruct (typ_eq (type_of_chunk c1) (type_of_chunk c2)); inv H1. + apply val_has_type_normalized. destruct H2. + apply val_normalized_has_type. auto. + rewrite e. apply val_normalized_has_type. auto. +Qed. + (** * Correspondence between Csharpminor's and Cminor's environments and memory states *) (** In Csharpminor, every variable is stored in a separate memory block. @@ -125,12 +314,12 @@ Qed. to a sub-block of Cminor block [b] at offset [ofs]. A memory injection [f] defines a relation [val_inject f] between - values and a relation [mem_inject f] between memory states. - These relations, defined in file [Memory], will be used intensively + values and a relation [Mem.inject f] between memory states. + These relations will be used intensively in our proof of simulation between Csharpminor and Cminor executions. - In the remainder of this section, we define relations between - Csharpminor and Cminor environments and call stacks. *) + In this section, we define the relation between + Csharpminor and Cminor environments. *) (** Matching for a Csharpminor variable [id]. - If this variable is mapped to a Cminor local variable, the @@ -187,7 +376,7 @@ Record match_env (f: meminj) (cenv: compilenv) me_vars: forall id, match_var f id e m te sp (PMap.get id cenv); -(** The range [lo, hi] must not be empty. *) +(** [lo, hi] is a proper interval. *) me_low_high: lo <= hi; @@ -215,9 +404,16 @@ Record match_env (f: meminj) (cenv: compilenv) (i.e. allocated before the stack data for the current Cminor function). *) me_incr: forall b tb delta, - f b = Some(tb, delta) -> b < lo -> tb < sp + f b = Some(tb, delta) -> b < lo -> tb < sp; + +(** The sizes of blocks appearing in [e] agree with their types *) + me_bounds: + forall id b lv, + PTree.get id e = Some(b, lv) -> Mem.bounds m b = (0, sizeof lv) }. +Hint Resolve me_low_high. + (** Global environments match if the memory injection [f] leaves unchanged the references to global symbols and functions. *) @@ -231,72 +427,28 @@ Record match_globalenvs (f: meminj) : Prop := forall b, b < 0 -> f b = Some(b, 0) }. -(** Call stacks represent abstractly the execution state of the current - Csharpminor and Cminor functions, as well as the states of the - calling functions. A call stack is a list of frames, each frame - collecting information on the current execution state of a Csharpminor - function and its Cminor translation. *) - -Record frame : Type := - mkframe { - fr_cenv: compilenv; - fr_e: Csharpminor.env; - fr_te: env; - fr_sp: block; - fr_low: Z; - fr_high: Z - }. - -Definition callstack : Type := list frame. - -(** Matching of call stacks imply matching of environments for each of - the frames, plus matching of the global environments, plus disjointness - conditions over the memory blocks allocated for local variables - and Cminor stack data. *) - -Inductive match_callstack: meminj -> callstack -> Z -> Z -> mem -> Prop := - | mcs_nil: - forall f bound tbound m, - match_globalenvs f -> - match_callstack f nil bound tbound m - | mcs_cons: - forall f cenv e te sp lo hi cs bound tbound m, - hi <= bound -> - sp < tbound -> - match_env f cenv e m te sp lo hi -> - match_callstack f cs lo sp m -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m. - (** The remainder of this section is devoted to showing preservation - of the [match_callstack] invariant under various assignments and memory + of the [match_en] invariant under various assignments and memory stores. First: preservation by memory stores to ``mapped'' blocks (block that have a counterpart in the Cminor execution). *) +Ltac geninv x := + let H := fresh in (generalize x; intro H; inv H). + Lemma match_env_store_mapped: forall f cenv e m1 m2 te sp lo hi chunk b ofs v, f b <> None -> - store chunk m1 b ofs v = Some m2 -> + Mem.store chunk m1 b ofs v = Some m2 -> match_env f cenv e m1 te sp lo hi -> match_env f cenv e m2 te sp lo hi. Proof. - intros. inversion H1. constructor; auto. + intros; inv H1; constructor; auto. (* vars *) - intros. generalize (me_vars0 id); intro. - inversion H2; econstructor; eauto. - rewrite <- H5. eapply load_store_other; eauto. + intros. geninv (me_vars0 id); econstructor; eauto. + rewrite <- H4. eapply Mem.load_store_other; eauto. left. congruence. -Qed. - -Lemma match_callstack_mapped: - forall f cs bound tbound m1, - match_callstack f cs bound tbound m1 -> - forall chunk b ofs v m2, - f b <> None -> - store chunk m1 b ofs v = Some m2 -> - match_callstack f cs bound tbound m2. -Proof. - induction 1; intros; econstructor; eauto. - eapply match_env_store_mapped; eauto. + (* bounds *) + intros. rewrite (Mem.bounds_store _ _ _ _ _ _ H0). eauto. Qed. (** Preservation by assignment to a Csharpminor variable that is @@ -307,27 +459,28 @@ Qed. Lemma match_env_store_local: forall f cenv e m1 m2 te sp lo hi id b chunk v tv, e!id = Some(b, Vscalar chunk) -> + Val.has_type v (type_of_chunk chunk) -> val_inject f (Val.load_result chunk v) tv -> - store chunk m1 b 0 v = Some m2 -> + Mem.store chunk m1 b 0 v = Some m2 -> match_env f cenv e m1 te sp lo hi -> match_env f cenv e m2 (PTree.set id tv te) sp lo hi. Proof. - intros. inversion H2. constructor; auto. - intros. generalize (me_vars0 id0); intro. - inversion H3; subst. + intros. inv H3. constructor; auto. + (* vars *) + intros. geninv (me_vars0 id0). (* var_local *) case (peq id id0); intro. (* the stored variable *) - subst id0. - change Csharpminor.var_kind with var_kind in H4. - rewrite H in H5. injection H5; clear H5; intros; subst b0 chunk0. + subst id0. + assert (b0 = b) by congruence. subst. + assert (chunk0 = chunk) by congruence. subst. econstructor. eauto. - eapply load_store_same; eauto. auto. + eapply Mem.load_store_same; eauto. auto. rewrite PTree.gss. reflexivity. auto. (* a different variable *) econstructor; eauto. - rewrite <- H6. eapply load_store_other; eauto. + rewrite <- H6. eapply Mem.load_store_other; eauto. rewrite PTree.gso; auto. (* var_stack_scalar *) econstructor; eauto. @@ -337,49 +490,393 @@ Proof. econstructor; eauto. (* var_global_array *) econstructor; eauto. + (* bounds *) + intros. rewrite (Mem.bounds_store _ _ _ _ _ _ H2). eauto. Qed. -Lemma match_env_store_above: - forall f cenv e m1 m2 te sp lo hi chunk b v, - store chunk m1 b 0 v = Some m2 -> - hi <= b -> +(** The [match_env] relation is preserved by any memory operation + that preserves sizes and loads from blocks in the [lo, hi] range. *) + +Lemma match_env_invariant: + forall f cenv e m1 m2 te sp lo hi, + (forall b ofs chunk v, + lo <= b < hi -> Mem.load chunk m1 b ofs = Some v -> + Mem.load chunk m2 b ofs = Some v) -> + (forall b, + lo <= b < hi -> Mem.bounds m2 b = Mem.bounds m1 b) -> match_env f cenv e m1 te sp lo hi -> match_env f cenv e m2 te sp lo hi. Proof. - intros. inversion H1; constructor; auto. - intros. generalize (me_vars0 id); intro. - inversion H2; econstructor; eauto. - rewrite <- H5. eapply load_store_other; eauto. - left. generalize (me_bounded0 _ _ _ H4). unfold block in *. omega. + intros. inv H1. constructor; eauto. + (* vars *) + intros. geninv (me_vars0 id); econstructor; eauto. + (* bounds *) + intros. rewrite H0. eauto. eauto. Qed. -Lemma match_callstack_store_above: - forall f cs bound tbound m1, - match_callstack f cs bound tbound m1 -> - forall chunk b v m2, - store chunk m1 b 0 v = Some m2 -> - bound <= b -> - match_callstack f cs bound tbound m2. +(** [match_env] is insensitive to the Cminor values of stack-allocated data. *) + +Lemma match_env_extensional: + forall f cenv e m te1 sp lo hi te2, + match_env f cenv e m te1 sp lo hi -> + (forall id chunk, cenv!!id = Var_local chunk -> te2!id = te1!id) -> + match_env f cenv e m te2 sp lo hi. Proof. - induction 1; intros; econstructor; eauto. - eapply match_env_store_above with (b := b); eauto. omega. + intros. inv H; econstructor; eauto. + intros. geninv (me_vars0 id); econstructor; eauto. + rewrite <- H5. eauto. +Qed. + +(** [match_env] and allocations *) + +Inductive alloc_condition: var_info -> var_kind -> block -> option (block * Z) -> Prop := + | alloc_cond_local: forall chunk sp, + alloc_condition (Var_local chunk) (Vscalar chunk) sp None + | alloc_cond_stack_scalar: forall chunk pos sp, + alloc_condition (Var_stack_scalar chunk pos) (Vscalar chunk) sp (Some(sp, pos)) + | alloc_cond_stack_array: forall pos sz sp, + alloc_condition (Var_stack_array pos) (Varray sz) sp (Some(sp, pos)). + +Lemma match_env_alloc_same: + forall f1 cenv e m1 te sp lo lv m2 b f2 id info tv, + match_env f1 cenv e m1 te sp lo (Mem.nextblock m1) -> + Mem.alloc m1 0 (sizeof lv) = (m2, b) -> + inject_incr f1 f2 -> + alloc_condition info lv sp (f2 b) -> + (forall b', b' <> b -> f2 b' = f1 b') -> + te!id = Some tv -> + e!id = None -> + match_env f2 (PMap.set id info cenv) (PTree.set id (b, lv) e) m2 te sp lo (Mem.nextblock m2). +Proof. + intros until tv. + intros ME ALLOC INCR ACOND OTHER TE E. +(* + assert (ALLOC_RES: b = Mem.nextblock m1) by eauto with mem. + assert (ALLOC_NEXT: Mem.nextblock m2 = Zsucc(Mem.nextblock m1)) by eauto with mem. +*) + inv ME; constructor. +(* vars *) + intros. rewrite PMap.gsspec. destruct (peq id0 id). subst id0. + (* the new var *) + inv ACOND; econstructor. + (* local *) + rewrite PTree.gss. reflexivity. + eapply Mem.load_alloc_same'; eauto. omega. simpl; omega. apply Zdivide_0. + auto. eauto. constructor. + (* stack scalar *) + rewrite PTree.gss; reflexivity. + econstructor; eauto. rewrite Int.add_commut; rewrite Int.add_zero; auto. + (* stack array *) + rewrite PTree.gss; reflexivity. + econstructor; eauto. rewrite Int.add_commut; rewrite Int.add_zero; auto. + (* the other vars *) + geninv (me_vars0 id0); econstructor. + (* local *) + rewrite PTree.gso; eauto. eapply Mem.load_alloc_other; eauto. + rewrite OTHER; auto. + exploit me_bounded0; eauto. exploit Mem.alloc_result; eauto. unfold block; omega. + eauto. eapply val_inject_incr; eauto. + (* stack scalar *) + rewrite PTree.gso; eauto. eapply val_inject_incr; eauto. + (* stack array *) + rewrite PTree.gso; eauto. eapply val_inject_incr; eauto. + (* global scalar *) + rewrite PTree.gso; auto. auto. + (* global array *) + rewrite PTree.gso; auto. +(* low high *) + exploit Mem.nextblock_alloc; eauto. unfold block in *; omega. +(* bounded *) + exploit Mem.alloc_result; eauto. intro RES. + exploit Mem.nextblock_alloc; eauto. intro NEXT. + intros until lv0. rewrite PTree.gsspec. destruct (peq id0 id); intro EQ. + inv EQ. unfold block in *; omega. + exploit me_bounded0; eauto. unfold block in *; omega. +(* inj *) + intros until lv2. repeat rewrite PTree.gsspec. + exploit Mem.alloc_result; eauto. intro RES. + destruct (peq id1 id); destruct (peq id2 id); subst; intros A1 A2 DIFF. + congruence. + inv A1. exploit me_bounded0; eauto. unfold block; omega. + inv A2. exploit me_bounded0; eauto. unfold block; omega. + eauto. +(* inv *) + intros. destruct (zeq b0 b). + subst. exists id; exists lv. apply PTree.gss. + exploit me_inv0; eauto. rewrite <- OTHER; eauto. + intros [id' [lv' A]]. exists id'; exists lv'. + rewrite PTree.gso; auto. congruence. +(* incr *) + intros. eapply me_incr0; eauto. rewrite <- OTHER; eauto. + exploit Mem.alloc_result; eauto. unfold block; omega. +(* bounds *) + intros. rewrite PTree.gsspec in H. + rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). + destruct (peq id0 id). + inv H. apply dec_eq_true. + rewrite dec_eq_false. eauto. + apply Mem.valid_not_valid_diff with m1. + exploit me_bounded0; eauto. intros [A B]. auto. + eauto with mem. +Qed. + +Lemma match_env_alloc_other: + forall f1 cenv e m1 te sp lo hi sz m2 b f2, + match_env f1 cenv e m1 te sp lo hi -> + Mem.alloc m1 0 sz = (m2, b) -> + inject_incr f1 f2 -> + (forall b', b' <> b -> f2 b' = f1 b') -> + hi <= b -> + match f2 b with None => True | Some(b',ofs) => sp < b' end -> + match_env f2 cenv e m2 te sp lo hi. +Proof. + intros until f2; intros ME ALLOC INCR OTHER BOUND TBOUND. + inv ME. + assert (BELOW: forall id b' lv, e!id = Some(b', lv) -> b' <> b). + intros. exploit me_bounded0; eauto. exploit Mem.alloc_result; eauto. + unfold block in *; omega. + econstructor; eauto. +(* vars *) + intros. geninv (me_vars0 id); econstructor. + (* local *) + eauto. eapply Mem.load_alloc_other; eauto. + rewrite OTHER; eauto. eauto. eapply val_inject_incr; eauto. + (* stack scalar *) + eauto. eapply val_inject_incr; eauto. + (* stack array *) + eauto. eapply val_inject_incr; eauto. + (* global scalar *) + auto. auto. + (* global array *) + auto. +(* inv *) + intros. rewrite OTHER in H. eauto. + red; intro; subst b0. rewrite H in TBOUND. omegaContradiction. +(* incr *) + intros. eapply me_incr0; eauto. rewrite <- OTHER; eauto. + exploit Mem.alloc_result; eauto. unfold block in *; omega. +(* bounds *) + intros. rewrite (Mem.bounds_alloc_other _ _ _ _ _ ALLOC). eauto. + exploit me_bounded0; eauto. +Qed. + +(** [match_env] and external calls *) + +Remark inject_incr_separated_same: + forall f1 f2 m1 m1', + inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' -> + forall b, Mem.valid_block m1 b -> f2 b = f1 b. +Proof. + intros. case_eq (f1 b). + intros [b' delta] EQ. apply H; auto. + intros EQ. case_eq (f2 b). + intros [b'1 delta1] EQ1. exploit H0; eauto. intros [C D]. contradiction. + auto. +Qed. + +Remark inject_incr_separated_same': + forall f1 f2 m1 m1', + inject_incr f1 f2 -> inject_separated f1 f2 m1 m1' -> + forall b b' delta, + f2 b = Some(b', delta) -> Mem.valid_block m1' b' -> f1 b = Some(b', delta). +Proof. + intros. case_eq (f1 b). + intros [b'1 delta1] EQ. exploit H; eauto. congruence. + intros. exploit H0; eauto. intros [C D]. contradiction. +Qed. + +Lemma match_env_external_call: + forall f1 cenv e m1 te sp lo hi m2 f2 m1', + match_env f1 cenv e m1 te sp lo hi -> + mem_unchanged_on (loc_unmapped f1) m1 m2 -> + inject_incr f1 f2 -> + inject_separated f1 f2 m1 m1' -> + (forall b, Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b) -> + hi <= Mem.nextblock m1 -> sp < Mem.nextblock m1' -> + match_env f2 cenv e m2 te sp lo hi. +Proof. + intros until m1'. intros ME UNCHANGED INCR SEPARATED BOUNDS VALID VALID'. + destruct UNCHANGED as [UNCHANGED1 UNCHANGED2]. + inversion ME. constructor; auto. +(* vars *) + intros. geninv (me_vars0 id); try (econstructor; eauto; fail). + (* local *) + econstructor. + eauto. + apply UNCHANGED2; eauto. + rewrite <- H3. eapply inject_incr_separated_same; eauto. + red. exploit me_bounded0; eauto. omega. + eauto. eauto. +(* inv *) + intros. apply me_inv0 with delta. eapply inject_incr_separated_same'; eauto. +(* incr *) + intros. + exploit inject_incr_separated_same; eauto. + instantiate (1 := b). red; omega. intros. + apply me_incr0 with b delta. congruence. auto. +(* bounds *) + intros. rewrite BOUNDS; eauto. + red. exploit me_bounded0; eauto. omega. +Qed. + +(** * Invariant on abstract call stacks *) + +(** Call stacks represent abstractly the execution state of the current + Csharpminor and Cminor functions, as well as the states of the + calling functions. A call stack is a list of frames, each frame + collecting information on the current execution state of a Csharpminor + function and its Cminor translation. *) + +Inductive frame : Type := + Frame(cenv: compilenv) + (tf: Cminor.function) + (e: Csharpminor.env) + (te: Cminor.env) + (sp: block) + (lo hi: Z). + +Definition callstack : Type := list frame. + +(** Matching of call stacks imply: +- matching of environments for each of the frames +- matching of the global environments +- separation conditions over the memory blocks allocated for C#minor local variables; +- separation conditions over the memory blocks allocated for Cminor stack data; +- freeable permissions on the parts of the Cminor stack data blocks + that are not images of C#minor local variable blocks. +*) + +Definition padding_freeable (f: meminj) (m: mem) (tm: mem) (sp: block) (sz: Z) : Prop := + forall ofs, + 0 <= ofs < sz -> + Mem.perm tm sp ofs Freeable + \/ exists b, exists delta, + f b = Some(sp, delta) + /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta. + +Inductive match_callstack (f: meminj) (m: mem) (tm: mem): + callstack -> Z -> Z -> Prop := + | mcs_nil: + forall bound tbound, + match_globalenvs f -> + match_callstack f m tm nil bound tbound + | mcs_cons: + forall cenv tf e te sp lo hi cs bound tbound + (BOUND: hi <= bound) + (TBOUND: sp < tbound) + (MENV: match_env f cenv e m te sp lo hi) + (PERM: padding_freeable f m tm sp tf.(fn_stackspace)) + (MCS: match_callstack f m tm cs lo sp), + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) bound tbound. + +(** [match_callstack] implies [match_globalenvs]. *) + +Lemma match_callstack_match_globalenvs: + forall f m tm cs bound tbound, + match_callstack f m tm cs bound tbound -> + match_globalenvs f. +Proof. + induction 1; eauto. +Qed. + +(** We now show invariance properties for [match_callstack] that + generalize those for [match_env]. *) + +Lemma padding_freeable_invariant: + forall f1 m1 tm1 sp sz cenv e te lo hi f2 m2 tm2, + padding_freeable f1 m1 tm1 sp sz -> + match_env f1 cenv e m1 te sp lo hi -> + (forall ofs, Mem.perm tm1 sp ofs Freeable -> Mem.perm tm2 sp ofs Freeable) -> + (forall b, b < hi -> Mem.bounds m2 b = Mem.bounds m1 b) -> + (forall b, b < hi -> f2 b = f1 b) -> + padding_freeable f2 m2 tm2 sp sz. +Proof. + intros; red; intros. + exploit H; eauto. intros [A | [b [delta [A B]]]]. + left; auto. + exploit me_inv; eauto. intros [id [lv C]]. + exploit me_bounded; eauto. intros [D E]. + right; exists b; exists delta. split. + rewrite H3; auto. + rewrite H2; auto. +Qed. + +Lemma match_callstack_store_mapped: + forall f m tm chunk b b' delta ofs ofs' v tv m' tm', + f b = Some(b', delta) -> + Mem.store chunk m b ofs v = Some m' -> + Mem.store chunk tm b' ofs' tv = Some tm' -> + forall cs lo hi, + match_callstack f m tm cs lo hi -> + match_callstack f m' tm' cs lo hi. +Proof. + induction 4. + constructor; auto. + constructor; auto. + eapply match_env_store_mapped; eauto. congruence. + eapply padding_freeable_invariant; eauto. + intros; eauto with mem. + intros. eapply Mem.bounds_store; eauto. +Qed. + +Lemma match_callstack_storev_mapped: + forall f m tm chunk a ta v tv m' tm', + val_inject f a ta -> + Mem.storev chunk m a v = Some m' -> + Mem.storev chunk tm ta tv = Some tm' -> + forall cs lo hi, + match_callstack f m tm cs lo hi -> + match_callstack f m' tm' cs lo hi. +Proof. + intros. destruct a; simpl in H0; try discriminate. + inv H. simpl in H1. + eapply match_callstack_store_mapped; eauto. +Qed. + +Lemma match_callstack_invariant: + forall f m tm cs bound tbound, + match_callstack f m tm cs bound tbound -> + forall m' tm', + (forall cenv e te sp lo hi, + hi <= bound -> + match_env f cenv e m te sp lo hi -> + match_env f cenv e m' te sp lo hi) -> + (forall b, + b < bound -> Mem.bounds m' b = Mem.bounds m b) -> + (forall b ofs p, + b < tbound -> Mem.perm tm b ofs p -> Mem.perm tm' b ofs p) -> + match_callstack f m' tm' cs bound tbound. +Proof. + induction 1; intros. + constructor; auto. + constructor; auto. + eapply padding_freeable_invariant; eauto. + intros. apply H1. omega. eapply IHmatch_callstack; eauto. - inversion H1. omega. + intros. eapply H0; eauto. inv MENV; omega. + intros. apply H1; auto. inv MENV; omega. + intros. apply H2; auto. omega. Qed. Lemma match_callstack_store_local: - forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv, + forall f cenv e te sp lo hi cs bound tbound m1 m2 tm tf id b chunk v tv, e!id = Some(b, Vscalar chunk) -> + Val.has_type v (type_of_chunk chunk) -> val_inject f (Val.load_result chunk v) tv -> - store chunk m1 b 0 v = Some m2 -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 -> - match_callstack f (mkframe cenv e (PTree.set id tv te) sp lo hi :: cs) bound tbound m2. + Mem.store chunk m1 b 0 v = Some m2 -> + match_callstack f m1 tm (Frame cenv tf e te sp lo hi :: cs) bound tbound -> + match_callstack f m2 tm (Frame cenv tf e (PTree.set id tv te) sp lo hi :: cs) bound tbound. Proof. - intros. inversion H2. constructor; auto. + intros. inv H3. constructor; auto. eapply match_env_store_local; eauto. - eapply match_callstack_store_above; eauto. - inversion H16. - generalize (me_bounded0 _ _ _ H). omega. + eapply padding_freeable_invariant; eauto. + intros. eapply Mem.bounds_store; eauto. + eapply match_callstack_invariant; eauto. + intros. apply match_env_invariant with m1; auto. + intros. rewrite <- H6. eapply Mem.load_store_other; eauto. + left. inv MENV. exploit me_bounded0; eauto. unfold block in *; omega. + intros. eapply Mem.bounds_store; eauto. + intros. eapply Mem.bounds_store; eauto. Qed. (** A variant of [match_callstack_store_local] where the Cminor environment @@ -387,436 +884,385 @@ Qed. In this case, [match_callstack] is preserved even if no assignment takes place on the Cminor side. *) -Lemma match_env_extensional: - forall f cenv e m te1 sp lo hi, - match_env f cenv e m te1 sp lo hi -> - forall te2, - (forall id, te2!id = te1!id) -> - match_env f cenv e m te2 sp lo hi. -Proof. - induction 1; intros; econstructor; eauto. - intros. generalize (me_vars0 id); intro. - inversion H0; econstructor; eauto. - rewrite H. auto. -Qed. - Lemma match_callstack_store_local_unchanged: - forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv, + forall f cenv e te sp lo hi cs bound tbound m1 m2 id b chunk v tv tf tm, e!id = Some(b, Vscalar chunk) -> + Val.has_type v (type_of_chunk chunk) -> val_inject f (Val.load_result chunk v) tv -> - store chunk m1 b 0 v = Some m2 -> + Mem.store chunk m1 b 0 v = Some m2 -> te!id = Some tv -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m1 -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m2. + match_callstack f m1 tm (Frame cenv tf e te sp lo hi :: cs) bound tbound -> + match_callstack f m2 tm (Frame cenv tf e te sp lo hi :: cs) bound tbound. Proof. - intros. inversion H3. constructor; auto. - apply match_env_extensional with (PTree.set id tv te). - eapply match_env_store_local; eauto. + intros. exploit match_callstack_store_local; eauto. intro MCS. + inv MCS. constructor; auto. eapply match_env_extensional; eauto. intros. rewrite PTree.gsspec. case (peq id0 id); intros. congruence. auto. - eapply match_callstack_store_above; eauto. - inversion H17. - generalize (me_bounded0 _ _ _ H). omega. Qed. -(** Preservation of [match_callstack] by freeing all blocks allocated - for local variables at function entry (on the Csharpminor side). *) - Lemma match_callstack_incr_bound: - forall f cs bound tbound m, - match_callstack f cs bound tbound m -> - forall bound' tbound', + forall f m tm cs bound tbound bound' tbound', + match_callstack f m tm cs bound tbound -> bound <= bound' -> tbound <= tbound' -> - match_callstack f cs bound' tbound' m. + match_callstack f m tm cs bound' tbound'. Proof. intros. inversion H; constructor; auto. omega. omega. Qed. -Lemma load_freelist: - forall fbl chunk m b ofs, - (forall b', In b' fbl -> b' <> b) -> - load chunk (free_list m fbl) b ofs = load chunk m b ofs. -Proof. - induction fbl; simpl; intros. - auto. - rewrite load_free. apply IHfbl. - intros. apply H. tauto. - apply sym_not_equal. apply H. tauto. -Qed. - -Lemma match_env_freelist: - forall f cenv e m te sp lo hi fbl, - match_env f cenv e m te sp lo hi -> - (forall b, In b fbl -> hi <= b) -> - match_env f cenv e (free_list m fbl) te sp lo hi. -Proof. - intros. inversion H. econstructor; eauto. - intros. generalize (me_vars0 id); intro. - inversion H1; econstructor; eauto. - rewrite <- H4. apply load_freelist. - intros. generalize (H0 _ H8); intro. - generalize (me_bounded0 _ _ _ H3). unfold block; omega. -Qed. - -Lemma match_callstack_freelist_rec: - forall f cs bound tbound m, - match_callstack f cs bound tbound m -> - forall fbl, - (forall b, In b fbl -> bound <= b) -> - match_callstack f cs bound tbound (free_list m fbl). -Proof. - induction 1; intros; constructor; auto. - eapply match_env_freelist; eauto. - intros. generalize (H3 _ H4). omega. - apply IHmatch_callstack. intros. - generalize (H3 _ H4). inversion H1. omega. -Qed. - -Lemma blocks_of_env_charact: - forall b e, - In b (blocks_of_env e) <-> - exists id, exists lv, e!id = Some(b, lv). -Proof. - unfold blocks_of_env. - set (f := fun id_b_lv : positive * (block * var_kind) => - let (_, y) := id_b_lv in let (b0, _) := y in b0). - intros; split; intros. - exploit list_in_map_inv; eauto. intros [[id [b' lv]] [A B]]. - simpl in A. subst b'. exists id; exists lv. apply PTree.elements_complete. auto. - destruct H as [id [lv EQ]]. - change b with (f (id, (b, lv))). apply List.in_map. - apply PTree.elements_correct. auto. -Qed. - -Lemma match_callstack_freelist: - forall f cenv e te sp lo hi cs bound tbound m tm, - mem_inject f m tm -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) bound tbound m -> - match_callstack f cs bound tbound (free_list m (blocks_of_env e)) - /\ mem_inject f (free_list m (blocks_of_env e)) (free tm sp). -Proof. - intros. inv H0. inv H14. split. - apply match_callstack_incr_bound with lo sp. - apply match_callstack_freelist_rec. auto. - intros. rewrite blocks_of_env_charact in H0. - destruct H0 as [id [lv EQ]]. exploit me_bounded0; eauto. omega. - omega. omega. - apply Mem.free_inject; auto. - intros. rewrite blocks_of_env_charact. eauto. -Qed. - -(** Preservation of [match_callstack] when allocating a block for - a local variable on the Csharpminor side. *) +(** Preservation of [match_callstack] by freeing all blocks allocated + for local variables at function entry (on the Csharpminor side) + and simultaneously freeing the Cminor stack data block. *) -Lemma load_from_alloc_is_undef: - forall m1 chunk m2 b, - alloc m1 0 (size_chunk chunk) = (m2, b) -> - load chunk m2 b 0 = Some Vundef. +Lemma in_blocks_of_env: + forall e id b lv, + e!id = Some(b, lv) -> In (b, 0, sizeof lv) (blocks_of_env e). Proof. - intros. - assert (exists v, load chunk m2 b 0 = Some v). - apply valid_access_load. - eapply valid_access_alloc_same; eauto. omega. omega. apply Zdivide_0. - destruct H0 as [v LOAD]. rewrite LOAD. decEq. - eapply load_alloc_same; eauto. + unfold blocks_of_env; intros. + change (b, 0, sizeof lv) with (block_of_binding (id, (b, lv))). + apply List.in_map. apply PTree.elements_correct. auto. Qed. -Lemma match_env_alloc_same: - forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data tv, - alloc m1 0 (sizeof lv) = (m2, b) -> - match info with - | Var_local chunk => data = None /\ lv = Vscalar chunk - | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk - | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz - | Var_global_scalar chunk => False - | Var_global_array => False - end -> - match_env f1 cenv1 e1 m1 te sp lo m1.(nextblock) -> - te!id = Some tv -> - e1!id = None -> - let f2 := extend_inject b data f1 in - let cenv2 := PMap.set id info cenv1 in - let e2 := PTree.set id (b, lv) e1 in - inject_incr f1 f2 -> - match_env f2 cenv2 e2 m2 te sp lo m2.(nextblock). +Lemma in_blocks_of_env_inv: + forall b lo hi e, + In (b, lo, hi) (blocks_of_env e) -> + exists id, exists lv, e!id = Some(b, lv) /\ lo = 0 /\ hi = sizeof lv. Proof. - intros. - assert (b = m1.(nextblock)). - injection H; intros. auto. - assert (m2.(nextblock) = Zsucc m1.(nextblock)). - injection H; intros. rewrite <- H7; reflexivity. - inversion H1. constructor. - (* me_vars *) - intros id0. unfold cenv2. rewrite PMap.gsspec. case (peq id0 id); intros. - (* same var *) - subst id0. destruct info. - (* info = Var_local chunk *) - elim H0; intros. - apply match_var_local with b Vundef tv. - unfold e2; rewrite PTree.gss. congruence. - eapply load_from_alloc_is_undef; eauto. - rewrite H8 in H. unfold sizeof in H. eauto. - unfold f2, extend_inject, eq_block. rewrite zeq_true. auto. - auto. - constructor. - (* info = Var_stack_scalar chunk ofs *) - elim H0; intros. - apply match_var_stack_scalar with b. - unfold e2; rewrite PTree.gss. congruence. - eapply val_inject_ptr. - unfold f2, extend_inject, eq_block. rewrite zeq_true. eauto. - rewrite Int.add_commut. rewrite Int.add_zero. auto. - (* info = Var_stack_array z *) - elim H0; intros A [sz B]. - apply match_var_stack_array with sz b. - unfold e2; rewrite PTree.gss. congruence. - eapply val_inject_ptr. - unfold f2, extend_inject, eq_block. rewrite zeq_true. eauto. - rewrite Int.add_commut. rewrite Int.add_zero. auto. - (* info = Var_global *) - contradiction. - contradiction. - (* other vars *) - generalize (me_vars0 id0); intros. - inversion H7. - eapply match_var_local with (v := v); eauto. - unfold e2; rewrite PTree.gso; eauto. - eapply load_alloc_other; eauto. - unfold f2, extend_inject, eq_block; rewrite zeq_false; auto. - generalize (me_bounded0 _ _ _ H9). unfold block in *; omega. - econstructor; eauto. - unfold e2; rewrite PTree.gso; eauto. - econstructor; eauto. - unfold e2; rewrite PTree.gso; eauto. - econstructor; eauto. - unfold e2; rewrite PTree.gso; eauto. - econstructor; eauto. - unfold e2; rewrite PTree.gso; eauto. - (* lo <= hi *) - unfold block in *; omega. - (* me_bounded *) - intros until lv0. unfold e2; rewrite PTree.gsspec. - case (peq id0 id); intros. - subst id0. inversion H7. subst b0. unfold block in *; omega. - generalize (me_bounded0 _ _ _ H7). rewrite H6. omega. - (* me_inj *) - intros until lv2. unfold e2; repeat rewrite PTree.gsspec. - case (peq id1 id); case (peq id2 id); intros. - congruence. - inversion H7. subst b1. rewrite H5. - generalize (me_bounded0 _ _ _ H8). unfold block; omega. - inversion H8. subst b2. rewrite H5. - generalize (me_bounded0 _ _ _ H7). unfold block; omega. - eauto. - (* me_inv *) - intros until delta. unfold f2, extend_inject, eq_block. - case (zeq b0 b); intros. - subst b0. exists id; exists lv. unfold e2. apply PTree.gss. - exploit me_inv0; eauto. intros [id' [lv' EQ]]. - exists id'; exists lv'. unfold e2. rewrite PTree.gso; auto. - congruence. - (* me_incr *) - intros until delta. unfold f2, extend_inject, eq_block. - case (zeq b0 b); intros. - subst b0. unfold block in *; omegaContradiction. - eauto. + unfold blocks_of_env; intros. + exploit list_in_map_inv; eauto. intros [[id [b' lv]] [A B]]. + unfold block_of_binding in A. inv A. + exists id; exists lv; intuition. apply PTree.elements_complete. auto. Qed. -Lemma match_env_alloc_other: - forall f1 cenv e m1 m2 te sp lo hi chunk b data, - alloc m1 0 (sizeof chunk) = (m2, b) -> - match data with None => True | Some (b', delta') => sp < b' end -> - hi <= m1.(nextblock) -> - match_env f1 cenv e m1 te sp lo hi -> - let f2 := extend_inject b data f1 in - inject_incr f1 f2 -> - match_env f2 cenv e m2 te sp lo hi. +(* +Lemma free_list_perm: + forall l m m', + Mem.free_list m l = Some m' -> + forall b ofs p, + Mem.perm m' b ofs p -> Mem.perm m b ofs p. Proof. - intros. - assert (b = m1.(nextblock)). injection H; auto. - rewrite <- H4 in H1. - inversion H2. constructor; auto. - (* me_vars *) - intros. generalize (me_vars0 id); intro. - inversion H5. - eapply match_var_local with (v := v); eauto. - eapply load_alloc_other; eauto. - unfold f2, extend_inject, eq_block. rewrite zeq_false. auto. - generalize (me_bounded0 _ _ _ H7). unfold block in *; omega. - econstructor; eauto. - econstructor; eauto. - econstructor; eauto. - econstructor; eauto. - (* me_bounded *) - intros until delta. unfold f2, extend_inject, eq_block. - case (zeq b0 b); intros. rewrite H5 in H0. omegaContradiction. - eauto. - (* me_incr *) - intros until delta. unfold f2, extend_inject, eq_block. - case (zeq b0 b); intros. subst b0. omegaContradiction. - eauto. + induction l; simpl; intros. + inv H; auto. + revert H. destruct a as [[b' lo'] hi']. + caseEq (Mem.free m b' lo' hi'); try congruence. + intros m1 FREE1 FREE2. + eauto with mem. Qed. +*) -Lemma match_callstack_alloc_other: - forall f1 cs bound tbound m1, - match_callstack f1 cs bound tbound m1 -> - forall lv m2 b data, - alloc m1 0 (sizeof lv) = (m2, b) -> - match data with None => True | Some (b', delta') => tbound <= b' end -> - bound <= m1.(nextblock) -> - let f2 := extend_inject b data f1 in +Lemma match_callstack_freelist: + forall f cenv tf e te sp lo hi cs m m' tm, + Mem.inject f m tm -> + Mem.free_list m (blocks_of_env e) = Some m' -> + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> + exists tm', + Mem.free tm sp 0 tf.(fn_stackspace) = Some tm' + /\ match_callstack f m' tm' cs (Mem.nextblock m') (Mem.nextblock tm') + /\ Mem.inject f m' tm'. +Proof. + intros until tm; intros INJ FREELIST MCS. inv MCS. inv MENV. + assert ({tm' | Mem.free tm sp 0 (fn_stackspace tf) = Some tm'}). + apply Mem.range_perm_free. + red; intros. + exploit PERM; eauto. intros [A | [b [delta [A B]]]]. + auto. + exploit me_inv0; eauto. intros [id [lv C]]. + exploit me_bounds0; eauto. intro D. rewrite D in B; simpl in B. + assert (Mem.range_perm m b 0 (sizeof lv) Freeable). + eapply free_list_freeable; eauto. eapply in_blocks_of_env; eauto. + replace ofs with ((ofs - delta) + delta) by omega. + eapply Mem.perm_inject; eauto. apply H0. omega. + destruct X as [tm' FREE]. + exploit nextblock_freelist; eauto. intro NEXT. + exploit Mem.nextblock_free; eauto. intro NEXT'. + exists tm'. split. auto. split. + rewrite NEXT; rewrite NEXT'. + apply match_callstack_incr_bound with lo sp; try omega. + apply match_callstack_invariant with m tm; auto. + intros. apply match_env_invariant with m; auto. + intros. rewrite <- H2. eapply load_freelist; eauto. + intros. exploit in_blocks_of_env_inv; eauto. + intros [id [lv [A [B C]]]]. + exploit me_bounded0; eauto. unfold block; omega. + intros. eapply bounds_freelist; eauto. + intros. eapply bounds_freelist; eauto. + intros. eapply Mem.perm_free_1; eauto. left; unfold block; omega. + eapply Mem.free_inject; eauto. + intros. exploit me_inv0; eauto. intros [id [lv A]]. + exists 0; exists (sizeof lv); split. + eapply in_blocks_of_env; eauto. + exploit me_bounds0; eauto. intro B. + exploit Mem.perm_in_bounds; eauto. rewrite B; simpl. auto. +Qed. + +(** Preservation of [match_callstack] by allocations. *) + +Lemma match_callstack_alloc_below: + forall f1 m1 tm sz m2 b f2, + Mem.alloc m1 0 sz = (m2, b) -> inject_incr f1 f2 -> - match_callstack f2 cs bound tbound m2. + (forall b', b' <> b -> f2 b' = f1 b') -> + forall cs bound tbound, + match_callstack f1 m1 tm cs bound tbound -> + bound <= b -> + match f2 b with None => True | Some(b',ofs) => tbound <= b' end -> + match_callstack f2 m2 tm cs bound tbound. Proof. - induction 1; intros. + induction 4; intros. constructor. - inversion H. constructor. - intros. auto. - intros. elim (mg_symbols0 _ _ H4); intros. - split; auto. elim (H3 b0); intros; congruence. - intros. generalize (mg_functions0 _ H4). elim (H3 b0); congruence. - constructor. auto. auto. - unfold f2; eapply match_env_alloc_other; eauto. - destruct data; auto. destruct p. omega. omega. - unfold f2; eapply IHmatch_callstack; eauto. - destruct data; auto. destruct p. omega. - inversion H1; omega. + inv H2. constructor. + intros. exploit mg_symbols0; eauto. intros [A B]. auto. + intros. rewrite H1; auto. + exploit Mem.alloc_result; eauto. + generalize (Mem.nextblock_pos m1). + unfold block; omega. + constructor; auto. + eapply match_env_alloc_other; eauto. omega. destruct (f2 b); auto. destruct p; omega. + eapply padding_freeable_invariant; eauto. + intros. eapply Mem.bounds_alloc_other; eauto. unfold block; omega. + intros. apply H1. unfold block; omega. + apply IHmatch_callstack. + inv MENV; omega. + destruct (f2 b); auto. destruct p; omega. Qed. Lemma match_callstack_alloc_left: - forall m1 lv m2 b info f1 cenv1 e1 te sp lo id data cs tv tbound, - alloc m1 0 (sizeof lv) = (m2, b) -> - match info with - | Var_local chunk => data = None /\ lv = Vscalar chunk - | Var_stack_scalar chunk pos => data = Some(sp, pos) /\ lv = Vscalar chunk - | Var_stack_array pos => data = Some(sp, pos) /\ exists sz, lv = Varray sz - | Var_global_scalar chunk => False - | Var_global_array => False - end -> - match_callstack f1 (mkframe cenv1 e1 te sp lo m1.(nextblock) :: cs) m1.(nextblock) tbound m1 -> - te!id = Some tv -> - e1!id = None -> - let f2 := extend_inject b data f1 in - let cenv2 := PMap.set id info cenv1 in - let e2 := PTree.set id (b, lv) e1 in + forall f1 m1 tm cenv tf e te sp lo cs lv m2 b f2 info id tv, + match_callstack f1 m1 tm + (Frame cenv tf e te sp lo (Mem.nextblock m1) :: cs) + (Mem.nextblock m1) (Mem.nextblock tm) -> + Mem.alloc m1 0 (sizeof lv) = (m2, b) -> inject_incr f1 f2 -> - match_callstack f2 (mkframe cenv2 e2 te sp lo m2.(nextblock) :: cs) m2.(nextblock) tbound m2. -Proof. - intros. inversion H1. constructor. omega. auto. - unfold f2, cenv2, e2. eapply match_env_alloc_same; eauto. - unfold f2; eapply match_callstack_alloc_other; eauto. - destruct info. - elim H0; intros. rewrite H20. auto. - elim H0; intros. rewrite H20. omega. - elim H0; intros. rewrite H20. omega. - contradiction. - contradiction. - inversion H18; omega. + alloc_condition info lv sp (f2 b) -> + (forall b', b' <> b -> f2 b' = f1 b') -> + te!id = Some tv -> + e!id = None -> + match_callstack f2 m2 tm + (Frame (PMap.set id info cenv) tf (PTree.set id (b, lv) e) te sp lo (Mem.nextblock m2) :: cs) + (Mem.nextblock m2) (Mem.nextblock tm). +Proof. + intros until tv; intros MCS ALLOC INCR ACOND OTHER TE E. + inv MCS. + exploit Mem.alloc_result; eauto. intro RESULT. + exploit Mem.nextblock_alloc; eauto. intro NEXT. + constructor. + omega. auto. + eapply match_env_alloc_same; eauto. + eapply padding_freeable_invariant; eauto. + intros. eapply Mem.bounds_alloc_other; eauto. unfold block in *; omega. + intros. apply OTHER. unfold block in *; omega. + eapply match_callstack_alloc_below; eauto. + inv MENV. unfold block in *; omega. + inv ACOND. auto. omega. omega. Qed. Lemma match_callstack_alloc_right: - forall f cs bound tm1 m tm2 lo hi b, - alloc tm1 lo hi = (tm2, b) -> - match_callstack f cs bound tm1.(nextblock) m -> - match_callstack f cs bound tm2.(nextblock) m. -Proof. - intros. eapply match_callstack_incr_bound; eauto. omega. - injection H; intros. rewrite <- H2; simpl. omega. -Qed. - -Lemma match_env_alloc: - forall m1 l h m2 b tm1 tm2 tb f1 ce e te sp lo hi, - alloc m1 l h = (m2, b) -> - alloc tm1 l h = (tm2, tb) -> - match_env f1 ce e m1 te sp lo hi -> - hi <= m1.(nextblock) -> - sp < tm1.(nextblock) -> - let f2 := extend_inject b (Some(tb, 0)) f1 in - inject_incr f1 f2 -> - match_env f2 ce e m2 te sp lo hi. + forall f m tm cs tf sp tm' te, + match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) -> + Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) -> + Mem.inject f m tm -> + match_callstack f m tm' + (Frame gce tf empty_env te sp (Mem.nextblock m) (Mem.nextblock m) :: cs) + (Mem.nextblock m) (Mem.nextblock tm'). Proof. + intros. + exploit Mem.alloc_result; eauto. intro RES. + exploit Mem.nextblock_alloc; eauto. intro NEXT. + constructor. omega. unfold block in *; omega. +(* match env *) + constructor. +(* vars *) + intros. generalize (global_compilenv_charact id); intro. + destruct (gce!!id); try contradiction. + constructor. apply PTree.gempty. auto. + constructor. apply PTree.gempty. +(* low high *) + omega. +(* bounded *) + intros. rewrite PTree.gempty in H2. congruence. +(* inj *) + intros. rewrite PTree.gempty in H2. congruence. +(* inv *) intros. - assert (BEQ: b = m1.(nextblock)). injection H; auto. - assert (TBEQ: tb = tm1.(nextblock)). injection H0; auto. - inversion H1. constructor; auto. - (* me_vars *) - intros. generalize (me_vars0 id); intro. inversion H5. - (* var_local *) - eapply match_var_local with (v := v); eauto. - eapply load_alloc_other; eauto. - generalize (me_bounded0 _ _ _ H7). intro. - unfold f2, extend_inject. case (zeq b0 b); intro. - subst b0. rewrite BEQ in H12. omegaContradiction. - auto. - (* var_stack_scalar *) - econstructor; eauto. - (* var_stack_array *) - econstructor; eauto. - (* var_global_scalar *) - econstructor; eauto. - (* var_global_array *) - econstructor; eauto. - (* me_bounded *) - intros until delta. unfold f2, extend_inject. case (zeq b0 b); intro. - intro. injection H5; clear H5; intros. - rewrite H6 in TBEQ. rewrite TBEQ in H3. omegaContradiction. - eauto. - (* me_inj *) - intros until delta. unfold f2, extend_inject. case (zeq b0 b); intros. - injection H5; clear H5; intros; subst b0 tb0 delta. - rewrite BEQ in H6. omegaContradiction. - eauto. -Qed. - -Lemma match_callstack_alloc_rec: - forall f1 cs bound tbound m1, - match_callstack f1 cs bound tbound m1 -> - forall l h m2 b tm1 tm2 tb, - alloc m1 l h = (m2, b) -> - alloc tm1 l h = (tm2, tb) -> - bound <= m1.(nextblock) -> - tbound <= tm1.(nextblock) -> - let f2 := extend_inject b (Some(tb, 0)) f1 in - inject_incr f1 f2 -> - match_callstack f2 cs bound tbound m2. + assert (sp <> sp). apply Mem.valid_not_valid_diff with tm. + eapply Mem.valid_block_inject_2; eauto. eauto with mem. + tauto. +(* incr *) + intros. rewrite RES. change (Mem.valid_block tm tb). + eapply Mem.valid_block_inject_2; eauto. +(* bounds *) + unfold empty_env; intros. rewrite PTree.gempty in H2. congruence. +(* padding freeable *) + red; intros. left. eapply Mem.perm_alloc_2; eauto. +(* previous call stack *) + rewrite RES. apply match_callstack_invariant with m tm; auto. + intros. eapply Mem.perm_alloc_1; eauto. +Qed. + +(** Decidability of the predicate "this is not a padding location" *) + +Definition is_reachable (f: meminj) (m: mem) (sp: block) (ofs: Z) : Prop := + exists b, exists delta, + f b = Some(sp, delta) + /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta. + +Lemma is_reachable_dec: + forall f cenv e m te sp lo hi ofs, + match_env f cenv e m te sp lo hi -> + {is_reachable f m sp ofs} + {~is_reachable f m sp ofs}. Proof. - induction 1; intros. - constructor. - inversion H. constructor. - intros. elim (mg_symbols0 _ _ H5); intros. - split; auto. elim (H4 b0); intros; congruence. - intros. generalize (mg_functions0 _ H5). elim (H4 b0); congruence. - constructor. auto. auto. - unfold f2. eapply match_env_alloc; eauto. omega. omega. - unfold f2; eapply IHmatch_callstack; eauto. - inversion H1; omega. - omega. -Qed. - -Lemma match_callstack_alloc: - forall f1 cs m1 tm1 l h m2 b tm2 tb, - match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1 -> - alloc m1 l h = (m2, b) -> - alloc tm1 l h = (tm2, tb) -> - let f2 := extend_inject b (Some(tb, 0)) f1 in + intros. + set (P := fun (b: block) => + match f b with + | None => False + | Some(b', delta) => + b' = sp /\ Mem.low_bound m b + delta <= ofs < Mem.high_bound m b + delta + end). + assert ({forall b, Intv.In b (lo, hi) -> ~P b} + {exists b, Intv.In b (lo, hi) /\ P b}). + apply Intv.forall_dec. intro b. unfold P. + destruct (f b) as [[b' delta] | ]. + destruct (eq_block b' sp). + destruct (zle (Mem.low_bound m b + delta) ofs). + destruct (zlt ofs (Mem.high_bound m b + delta)). + right; auto. + left; intuition. + left; intuition. + left; intuition. + left; intuition. + inv H. destruct H0. + right; red; intros [b [delta [A [B C]]]]. + elim (n b). + exploit me_inv0; eauto. intros [id [lv D]]. exploit me_bounded0; eauto. + red. rewrite A. auto. + left. destruct e0 as [b [A B]]. red in B; revert B. + case_eq (f b). intros [b' delta] EQ [C [D E]]. subst b'. + exists b; exists delta. auto. + tauto. +Qed. + +(** Preservation of [match_callstack] by external calls. *) + +Lemma match_callstack_external_call: + forall f1 f2 m1 m2 m1' m2', + mem_unchanged_on (loc_unmapped f1) m1 m2 -> + mem_unchanged_on (loc_out_of_reach f1 m1) m1' m2' -> inject_incr f1 f2 -> - match_callstack f2 cs m2.(nextblock) tm2.(nextblock) m2. + inject_separated f1 f2 m1 m1' -> + (forall b, Mem.valid_block m1 b -> Mem.bounds m2 b = Mem.bounds m1 b) -> + forall cs bound tbound, + match_callstack f1 m1 m1' cs bound tbound -> + bound <= Mem.nextblock m1 -> tbound <= Mem.nextblock m1' -> + match_callstack f2 m2 m2' cs bound tbound. +Proof. + intros until m2'. + intros UNMAPPED OUTOFREACH INCR SEPARATED BOUNDS. + destruct OUTOFREACH as [OUTOFREACH1 OUTOFREACH2]. + induction 1; intros; constructor. +(* base case *) + constructor; intros. + exploit mg_symbols; eauto. intros [A B]. auto. + replace (f2 b) with (f1 b). eapply mg_functions; eauto. + symmetry. eapply inject_incr_separated_same; eauto. + red. generalize (Mem.nextblock_pos m1); omega. +(* inductive case *) + auto. auto. + eapply match_env_external_call; eauto. omega. omega. + (* padding-freeable *) + red; intros. + destruct (is_reachable_dec _ _ _ _ _ _ _ _ ofs MENV). + destruct i as [b [delta [A B]]]. + right; exists b; exists delta; split. + apply INCR; auto. rewrite BOUNDS. auto. + exploit me_inv; eauto. intros [id [lv C]]. + exploit me_bounded; eauto. intros. red; omega. + exploit PERM; eauto. intros [A|A]; try contradiction. left. + apply OUTOFREACH1; auto. red; intros. + assert ((ofs < Mem.low_bound m1 b0 + delta \/ ofs >= Mem.high_bound m1 b0 + delta) + \/ Mem.low_bound m1 b0 + delta <= ofs < Mem.high_bound m1 b0 + delta) + by omega. destruct H4; auto. + elim n. exists b0; exists delta; auto. + (* induction *) + eapply IHmatch_callstack; eauto. inv MENV; omega. omega. +Qed. + +Remark external_call_nextblock_incr: + forall ef vargs m1 t vres m2, + external_call ef vargs m1 t vres m2 -> + Mem.nextblock m1 <= Mem.nextblock m2. Proof. - intros. unfold f2 in *. - apply match_callstack_incr_bound with m1.(nextblock) tm1.(nextblock). - eapply match_callstack_alloc_rec; eauto. omega. omega. - injection H0; intros; subst m2; simpl; omega. - injection H1; intros; subst tm2; simpl; omega. + intros. + generalize (external_call_valid_block _ _ _ _ _ _ (Mem.nextblock m1 - 1) H). + unfold Mem.valid_block. omega. Qed. -(** [match_callstack] implies [match_globalenvs]. *) +(** * Soundness of chunk and type inference. *) -Lemma match_callstack_match_globalenvs: - forall f cs bound tbound m, - match_callstack f cs bound tbound m -> - match_globalenvs f. +Lemma load_normalized: + forall chunk m b ofs v, + Mem.load chunk m b ofs = Some v -> val_normalized v chunk. Proof. - induction 1; eauto. + intros. + exploit Mem.load_type; eauto. intro TY. + exploit Mem.load_cast; eauto. intro CST. + red. destruct chunk; destruct v; simpl in *; auto; contradiction. +Qed. + +Lemma chunktype_expr_correct: + forall f m tm cenv tf e te sp lo hi cs bound tbound, + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) bound tbound -> + forall a v, + Csharpminor.eval_expr gve e m a v -> + forall chunk (CTE: chunktype_expr cenv a = OK chunk), + val_normalized v chunk. +Proof. + intros until tbound; intro MCS. induction 1; intros; try (monadInv CTE). +(* var *) + assert (chunk0 = chunk). + unfold chunktype_expr in CTE. + inv MCS. inv MENV. generalize (me_vars0 id); intro MV. + inv MV; rewrite <- H1 in CTE; monadInv CTE; inv H; try congruence. + unfold gve in H6. simpl in H6. congruence. + subst chunk0. + inv H; exploit load_normalized; eauto. unfold val_normalized; auto. +(* const *) + eapply chunktype_const_correct; eauto. +(* unop *) + eapply chunktype_unop_correct; eauto. +(* binop *) + eapply chunktype_binop_correct; eauto. +(* load *) + destruct v1; simpl in H0; try discriminate. + eapply load_normalized; eauto. +(* cond *) + eapply chunktype_merge_correct; eauto. + destruct vb1; eauto. +Qed. + +Lemma type_expr_correct: + forall f m tm cenv tf e te sp lo hi cs bound tbound, + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) bound tbound -> + forall a v ty, + Csharpminor.eval_expr gve e m a v -> + type_expr cenv a = OK ty -> + Val.has_type v ty. +Proof. + intros. monadInv H1. apply val_normalized_has_type. + eapply chunktype_expr_correct; eauto. +Qed. + +Lemma type_exprlist_correct: + forall f m tm cenv tf e te sp lo hi cs bound tbound, + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) bound tbound -> + forall al vl tyl, + Csharpminor.eval_exprlist gve e m al vl -> + type_exprlist cenv al = OK tyl -> + Val.has_type_list vl tyl. +Proof. + intros. monadInv H1. + generalize al vl H0 tyl H2. induction 1; intros. + inv H3. simpl. auto. + inv H5. simpl. split. + eapply type_expr_correct; eauto. + auto. Qed. (** * Correctness of Cminor construction functions *) @@ -910,7 +1356,7 @@ Lemma eval_binop_compat: Csharpminor.eval_binop op v1 v2 m = Some v -> val_inject f v1 tv1 -> val_inject f v2 tv2 -> - mem_inject f m tm -> + Mem.inject f m tm -> exists tv, Cminor.eval_binop op tv1 tv2 = Some tv /\ val_inject f v tv. @@ -924,8 +1370,8 @@ Proof. destruct (eq_block b1 b0); inv H4. assert (b3 = b2) by congruence. subst b3. unfold eq_block; rewrite zeq_true. TrivialOp. - replace x0 with x by congruence. decEq. decEq. - apply Int.sub_shifted. + replace delta0 with delta by congruence. + decEq. decEq. apply Int.sub_shifted. inv H0; try discriminate; inv H1; inv H; TrivialOp. inv H0; try discriminate; inv H1; inv H; TrivialOp. destruct (Int.eq i0 Int.zero); inv H1. TrivialOp. @@ -952,28 +1398,28 @@ Proof. exists v; split; auto. eapply val_inject_eval_compare_null; eauto. exists v; split; auto. eapply val_inject_eval_compare_null; eauto. (* cmp ptr ptr *) - caseEq (valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b0 (Int.signed ofs0)); + caseEq (Mem.valid_pointer m b1 (Int.signed ofs1) && Mem.valid_pointer m b0 (Int.signed ofs0)); intro EQ; rewrite EQ in H4; try discriminate. elim (andb_prop _ _ EQ); intros. destruct (eq_block b1 b0); inv H4. (* same blocks in source *) assert (b3 = b2) by congruence. subst b3. - assert (x0 = x) by congruence. subst x0. + assert (delta0 = delta) by congruence. subst delta0. exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split. unfold eq_block; rewrite zeq_true; simpl. decEq. decEq. rewrite Int.translate_cmp. auto. - eapply valid_pointer_inject_no_overflow; eauto. - eapply valid_pointer_inject_no_overflow; eauto. + eapply Mem.valid_pointer_inject_no_overflow; eauto. + eapply Mem.valid_pointer_inject_no_overflow; eauto. apply val_inject_val_of_bool. (* different blocks in source *) simpl. exists v; split; [idtac | eapply val_inject_eval_compare_mismatch; eauto]. destruct (eq_block b2 b3); auto. - exploit different_pointers_inject; eauto. intros [A|A]. + exploit Mem.different_pointers_inject; eauto. intros [A|A]. congruence. decEq. destruct c; simpl in H6; inv H6; unfold Int.cmp. - predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr x)) (Int.add ofs0 (Int.repr x0)). + predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)). congruence. auto. - predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr x)) (Int.add ofs0 (Int.repr x0)). + predSpec Int.eq Int.eq_spec (Int.add ofs1 (Int.repr delta)) (Int.add ofs0 (Int.repr delta0)). congruence. auto. (* cmpu *) inv H0; try discriminate; inv H1; inv H; TrivialOp. @@ -1038,6 +1484,29 @@ Qed. (** Correctness of [make_store]. *) +Inductive val_content_inject (f: meminj): memory_chunk -> val -> val -> Prop := + | val_content_inject_8_signed: + forall n, + val_content_inject f Mint8signed (Vint (Int.sign_ext 8 n)) (Vint n) + | val_content_inject_8_unsigned: + forall n, + val_content_inject f Mint8unsigned (Vint (Int.zero_ext 8 n)) (Vint n) + | val_content_inject_16_signed: + forall n, + val_content_inject f Mint16signed (Vint (Int.sign_ext 16 n)) (Vint n) + | val_content_inject_16_unsigned: + forall n, + val_content_inject f Mint16unsigned (Vint (Int.zero_ext 16 n)) (Vint n) + | val_content_inject_32: + forall n, + val_content_inject f Mfloat32 (Vfloat (Float.singleoffloat n)) (Vfloat n) + | val_content_inject_base: + forall chunk v1 v2, + val_inject f v1 v2 -> + val_content_inject f chunk v1 v2. + +Hint Resolve val_content_inject_base. + Lemma store_arg_content_inject: forall f sp te tm a v va chunk, eval_expr tge sp te tm a va -> @@ -1056,12 +1525,30 @@ Proof. destruct chunk; trivial; inv H; simpl in H6; inv H6; econstructor; (split; [eauto|idtac]); - destruct v1; simpl in H0; inv H0; try (constructor; constructor). - apply val_content_inject_8. auto. apply Int.zero_ext_idem. compute; auto. - apply val_content_inject_8; auto. apply Int.zero_ext_sign_ext. compute; auto. - apply val_content_inject_16; auto. apply Int.zero_ext_idem. compute; auto. - apply val_content_inject_16; auto. apply Int.zero_ext_sign_ext. compute; auto. - apply val_content_inject_32. apply Float.singleoffloat_idem. + destruct v1; simpl in H0; inv H0; constructor; constructor. +Qed. + +Lemma storev_mapped_inject': + forall f chunk m1 a1 v1 n1 m2 a2 v2, + Mem.inject f m1 m2 -> + Mem.storev chunk m1 a1 v1 = Some n1 -> + val_inject f a1 a2 -> + val_content_inject f chunk v1 v2 -> + exists n2, + Mem.storev chunk m2 a2 v2 = Some n2 /\ Mem.inject f n1 n2. +Proof. + intros. + assert (forall v1', + (forall b ofs, Mem.store chunk m1 b ofs v1 = Mem.store chunk m1 b ofs v1') -> + Mem.storev chunk m1 a1 v1' = Some n1). + intros. rewrite <- H0. destruct a1; simpl; auto. + inv H2; (eapply Mem.storev_mapped_inject; [eauto|idtac|eauto|eauto]); + auto; apply H3; intros. + apply Mem.store_int8_sign_ext. + apply Mem.store_int8_zero_ext. + apply Mem.store_int16_sign_ext. + apply Mem.store_int16_zero_ext. + apply Mem.store_float32_truncate. Qed. Lemma make_store_correct: @@ -1069,69 +1556,63 @@ Lemma make_store_correct: eval_expr tge sp te tm addr tvaddr -> eval_expr tge sp te tm rhs tvrhs -> Mem.storev chunk m vaddr vrhs = Some m' -> - mem_inject f m tm -> + Mem.inject f m tm -> val_inject f vaddr tvaddr -> val_inject f vrhs tvrhs -> - exists tm', + exists tm', exists tvrhs', step tge (State fn (make_store chunk addr rhs) k sp te tm) E0 (State fn Sskip k sp te tm') - /\ mem_inject f m' tm' - /\ nextblock tm' = nextblock tm. + /\ Mem.storev chunk tm tvaddr tvrhs' = Some tm' + /\ Mem.inject f m' tm'. Proof. intros. unfold make_store. exploit store_arg_content_inject. eexact H0. eauto. intros [tv [EVAL VCINJ]]. - exploit storev_mapped_inject_1; eauto. + exploit storev_mapped_inject'; eauto. intros [tm' [STORE MEMINJ]]. - exists tm'. - split. eapply step_store; eauto. - split. auto. - unfold storev in STORE; destruct tvaddr; try discriminate. - eapply nextblock_store; eauto. + exists tm'; exists tv. + split. eapply step_store; eauto. + auto. Qed. (** Correctness of the variable accessors [var_get], [var_addr], and [var_set]. *) Lemma var_get_correct: - forall cenv id a f e te sp lo hi m cs tm b chunk v, + forall cenv id a f tf e te sp lo hi m cs tm b chunk v, var_get cenv id = OK a -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> - mem_inject f m tm -> + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> + Mem.inject f m tm -> eval_var_ref gve e id b chunk -> - load chunk m b 0 = Some v -> + Mem.load chunk m b 0 = Some v -> exists tv, eval_expr tge (Vptr sp Int.zero) te tm a tv /\ val_inject f v tv. Proof. unfold var_get; intros. - assert (match_var f id e m te sp cenv!!id). - inversion H0. inversion H17. auto. - inversion H4; subst; rewrite <- H5 in H; inversion H; subst. + assert (match_var f id e m te sp cenv!!id). inv H0. inv MENV. auto. + inv H4; rewrite <- H5 in H; inv H; inv H2; try congruence. (* var_local *) - inversion H2; [subst|congruence]. exists v'; split. - apply eval_Evar. auto. - replace v with v0. auto. congruence. + apply eval_Evar. auto. + congruence. (* var_stack_scalar *) - inversion H2; [subst|congruence]. assert (b0 = b). congruence. subst b0. assert (chunk0 = chunk). congruence. subst chunk0. - exploit loadv_inject; eauto. - unfold loadv. eexact H3. + exploit Mem.loadv_inject; eauto. + unfold Mem.loadv. eexact H3. intros [tv [LOAD INJ]]. exists tv; split. eapply eval_Eload; eauto. eapply make_stackaddr_correct; eauto. auto. (* var_global_scalar *) - inversion H2; [congruence|subst]. simpl in H9; simpl in H10. + simpl in *. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H11. destruct (mg_symbols0 _ _ H9) as [A B]. + inv H2. exploit mg_symbols0; eauto. intros [A B]. assert (chunk0 = chunk). congruence. subst chunk0. - assert (loadv chunk m (Vptr b Int.zero) = Some v). assumption. assert (val_inject f (Vptr b Int.zero) (Vptr b Int.zero)). - econstructor; eauto. - generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13). + econstructor; eauto. + exploit Mem.loadv_inject; eauto. simpl. eauto. intros [tv [LOAD INJ]]. exists tv; split. eapply eval_Eload; eauto. eapply make_globaladdr_correct; eauto. @@ -1139,8 +1620,8 @@ Proof. Qed. Lemma var_addr_correct: - forall cenv id a f e te sp lo hi m cs tm b, - match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> + forall cenv id a f tf e te sp lo hi m cs tm b, + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> var_addr cenv id = OK a -> eval_var_addr gve e id b -> exists tv, @@ -1149,201 +1630,188 @@ Lemma var_addr_correct: Proof. unfold var_addr; intros. assert (match_var f id e m te sp cenv!!id). - inversion H. inversion H15. auto. - inversion H2; subst; rewrite <- H3 in H0; inversion H0; subst; clear H0. + inv H. inv MENV. auto. + inv H2; rewrite <- H3 in H0; inv H0; inv H1; try congruence. (* var_stack_scalar *) - inversion H1; [subst|congruence]. exists (Vptr sp (Int.repr ofs)); split. - eapply make_stackaddr_correct. - replace b with b0. auto. congruence. + eapply make_stackaddr_correct. congruence. (* var_stack_array *) - inversion H1; [subst|congruence]. exists (Vptr sp (Int.repr ofs)); split. - eapply make_stackaddr_correct. - replace b with b0. auto. congruence. + eapply make_stackaddr_correct. congruence. (* var_global_scalar *) - inversion H1; [congruence|subst]. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H7. destruct (mg_symbols0 _ _ H6) as [A B]. + inv H1. exploit mg_symbols0; eauto. intros [A B]. exists (Vptr b Int.zero); split. eapply make_globaladdr_correct. eauto. econstructor; eauto. (* var_global_array *) - inversion H1; [congruence|subst]. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H6. destruct (mg_symbols0 _ _ H5) as [A B]. + inv H1. exploit mg_symbols0; eauto. intros [A B]. exists (Vptr b Int.zero); split. eapply make_globaladdr_correct. eauto. econstructor; eauto. Qed. Lemma var_set_correct: - forall cenv id rhs a f e te sp lo hi m cs tm tv v m' fn k, - var_set cenv id rhs = OK a -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> + forall cenv id rhs rhs_chunk a f tf e te sp lo hi m cs tm tv v m' fn k, + var_set cenv id rhs rhs_chunk = OK a -> + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> eval_expr tge (Vptr sp Int.zero) te tm rhs tv -> val_inject f v tv -> - mem_inject f m tm -> + Mem.inject f m tm -> exec_assign gve e m id v m' -> + val_normalized v rhs_chunk -> exists te', exists tm', step tge (State fn a k (Vptr sp Int.zero) te tm) E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\ - mem_inject f m' tm' /\ - match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m' /\ + Mem.inject f m' tm' /\ + match_callstack f m' tm' (Frame cenv tf e te' sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm') /\ (forall id', id' <> id -> te'!id' = te!id'). Proof. - unfold var_set; intros. - inv H4. - assert (NEXTBLOCK: nextblock m' = nextblock m). - eapply nextblock_store; eauto. - inversion H0; subst. - assert (match_var f id e m te sp cenv!!id). inversion H19; auto. - inv H4; rewrite <- H7 in H; inv H. + intros until k. + intros VS MCS EVAL VINJ MINJ ASG VNORM. + unfold var_set in VS. inv ASG. + assert (NEXTBLOCK: Mem.nextblock m' = Mem.nextblock m). + eapply Mem.nextblock_store; eauto. + assert (MV: match_var f id e m te sp cenv!!id). + inv MCS. inv MENV. auto. + inv MV; rewrite <- H1 in VS; inv VS; inv H; try congruence. (* var_local *) - inversion H5; [subst|congruence]. assert (b0 = b) by congruence. subst b0. assert (chunk0 = chunk) by congruence. subst chunk0. + generalize H8; clear H8. case_eq (chunktype_compat rhs_chunk chunk). + (* compatible chunks *) + intros CCOMPAT EQ; inv EQ. + exploit chunktype_compat_correct; eauto. intro VNORM'. + exists (PTree.set id tv te); exists tm. + split. eapply step_assign. eauto. + split. eapply Mem.store_unmapped_inject; eauto. + split. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. + eapply val_normalized_has_type; eauto. red in VNORM'. congruence. + intros. apply PTree.gso; auto. + (* incompatible chunks but same type *) + intros. destruct (typ_eq (type_of_chunk chunk) (type_of_chunk rhs_chunk)); inv H8. exploit make_cast_correct; eauto. - intros [tv' [EVAL INJ]]. + intros [tv' [EVAL' INJ']]. exists (PTree.set id tv' te); exists tm. split. eapply step_assign. eauto. - split. eapply store_unmapped_inject; eauto. + split. eapply Mem.store_unmapped_inject; eauto. split. rewrite NEXTBLOCK. eapply match_callstack_store_local; eauto. + rewrite e0. eapply val_normalized_has_type; eauto. intros. apply PTree.gso; auto. (* var_stack_scalar *) - inversion H5; [subst|congruence]. assert (b0 = b) by congruence. subst b0. assert (chunk0 = chunk) by congruence. subst chunk0. - assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. + assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption. exploit make_store_correct. eapply make_stackaddr_correct. eauto. eauto. eauto. eauto. eauto. - intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. + intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]]. exists te; exists tm'. split. eauto. split. auto. - split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. - eapply match_callstack_mapped; eauto. - inversion H9; congruence. + split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). + eapply match_callstack_storev_mapped; eauto. auto. (* var_global_scalar *) - inversion H5; [congruence|subst]. simpl in H4; simpl in H10. + simpl in *. assert (chunk0 = chunk) by congruence. subst chunk0. - assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. + assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H12. destruct (mg_symbols0 _ _ H4) as [A B]. + exploit mg_symbols; eauto. intros [A B]. exploit make_store_correct. eapply make_globaladdr_correct; eauto. - eauto. eauto. eauto. eauto. eauto. - intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. + eauto. eauto. eauto. eauto. eauto. + intros [tm' [tvrhs' [EVAL' [STORE' TNEXTBLOCK]]]]. exists te; exists tm'. split. eauto. split. auto. - split. rewrite NEXTBLOCK; rewrite TNEXTBLOCK. - eapply match_callstack_mapped; eauto. congruence. + split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). + eapply match_callstack_store_mapped; eauto. auto. Qed. -Lemma match_env_extensional': - forall f cenv e m te1 sp lo hi, - match_env f cenv e m te1 sp lo hi -> - forall te2, - (forall id, - match cenv!!id with - | Var_local _ => te2!id = te1!id - | _ => True - end) -> - match_env f cenv e m te2 sp lo hi. -Proof. - induction 1; intros; econstructor; eauto. - intros. generalize (me_vars0 id); intro. - inversion H0; econstructor; eauto. - generalize (H id). rewrite <- H1. congruence. -Qed. - - Lemma match_callstack_extensional: - forall f cenv e te1 te2 sp lo hi cs bound tbound m, - (forall id, - match cenv!!id with - | Var_local _ => te2!id = te1!id - | _ => True - end) -> - match_callstack f (mkframe cenv e te1 sp lo hi :: cs) bound tbound m -> - match_callstack f (mkframe cenv e te2 sp lo hi :: cs) bound tbound m. + forall f cenv tf e te1 te2 sp lo hi cs bound tbound m tm, + (forall id chunk, cenv!!id = Var_local chunk -> te2!id = te1!id) -> + match_callstack f m tm (Frame cenv tf e te1 sp lo hi :: cs) bound tbound -> + match_callstack f m tm (Frame cenv tf e te2 sp lo hi :: cs) bound tbound. Proof. intros. inv H0. constructor; auto. - apply match_env_extensional' with te1; auto. + apply match_env_extensional with te1; auto. Qed. Lemma var_set_self_correct: - forall cenv id a f e te sp lo hi m cs tm tv v m' fn k, - var_set cenv id (Evar id) = OK a -> - match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> + forall cenv id ty a f tf e te sp lo hi m cs tm tv te' v m' fn k, + var_set_self cenv id ty = OK a -> + match_callstack f m tm (Frame cenv tf e te sp lo hi :: cs) (Mem.nextblock m) (Mem.nextblock tm) -> val_inject f v tv -> - mem_inject f m tm -> + Mem.inject f m tm -> exec_assign gve e m id v m' -> - exists te', exists tm', - step tge (State fn a k (Vptr sp Int.zero) (PTree.set id tv te) tm) - E0 (State fn Sskip k (Vptr sp Int.zero) te' tm') /\ - mem_inject f m' tm' /\ - match_callstack f (mkframe cenv e te' sp lo hi :: cs) m'.(nextblock) tm'.(nextblock) m'. -Proof. - unfold var_set; intros. - inv H3. - assert (NEXTBLOCK: nextblock m' = nextblock m). - eapply nextblock_store; eauto. - inversion H0; subst. - assert (EVAR: eval_expr tge (Vptr sp Int.zero) (PTree.set id tv te) tm (Evar id) tv). - constructor. apply PTree.gss. - assert (match_var f id e m te sp cenv!!id). inversion H18; auto. - inv H3; rewrite <- H6 in H; inv H. + Val.has_type v ty -> + te'!id = Some tv -> + (forall i, i <> id -> te'!i = te!i) -> + exists te'', exists tm', + step tge (State fn a k (Vptr sp Int.zero) te' tm) + E0 (State fn Sskip k (Vptr sp Int.zero) te'' tm') /\ + Mem.inject f m' tm' /\ + match_callstack f m' tm' (Frame cenv tf e te'' sp lo hi :: cs) (Mem.nextblock m') (Mem.nextblock tm') /\ + (forall id', id' <> id -> te''!id' = te'!id'). +Proof. + intros until k. + intros VS MCS VINJ MINJ ASG VTY VAL OTHERS. + unfold var_set_self in VS. inv ASG. + assert (NEXTBLOCK: Mem.nextblock m' = Mem.nextblock m). + eapply Mem.nextblock_store; eauto. + assert (MV: match_var f id e m te sp cenv!!id). + inv MCS. inv MENV. auto. + assert (EVAR: eval_expr tge (Vptr sp Int.zero) te' tm (Evar id) tv). + constructor. auto. + inv MV; rewrite <- H1 in VS; inv VS; inv H; try congruence. (* var_local *) - inversion H4; [subst|congruence]. assert (b0 = b) by congruence. subst b0. assert (chunk0 = chunk) by congruence. subst chunk0. - exploit make_cast_correct; eauto. - intros [tv' [EVAL INJ]]. - exists (PTree.set id tv' (PTree.set id tv te)); exists tm. + destruct (typ_eq (type_of_chunk chunk) ty); inv H8. + exploit make_cast_correct; eauto. + intros [tv' [EVAL' INJ']]. + exists (PTree.set id tv' te'); exists tm. split. eapply step_assign. eauto. - split. eapply store_unmapped_inject; eauto. - rewrite NEXTBLOCK. + split. eapply Mem.store_unmapped_inject; eauto. + split. rewrite NEXTBLOCK. apply match_callstack_extensional with (PTree.set id tv' te). - intros. destruct (cenv!!id0); auto. - repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. + intros. repeat rewrite PTree.gsspec. destruct (peq id0 id); auto. eapply match_callstack_store_local; eauto. + intros; apply PTree.gso; auto. (* var_stack_scalar *) - inversion H4; [subst|congruence]. assert (b0 = b) by congruence. subst b0. assert (chunk0 = chunk) by congruence. subst chunk0. - assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. + assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption. exploit make_store_correct. eapply make_stackaddr_correct. eauto. eauto. eauto. eauto. eauto. - intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. - exists (PTree.set id tv te); exists tm'. + intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]]. + exists te'; exists tm'. split. eauto. split. auto. - rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). apply match_callstack_extensional with te. - intros. caseEq (cenv!!id0); intros; auto. - rewrite PTree.gsspec. destruct (peq id0 id). congruence. auto. - eapply match_callstack_mapped; eauto. - inversion H8; congruence. + intros. apply OTHERS. congruence. + eapply match_callstack_storev_mapped; eauto. + auto. (* var_global_scalar *) - inversion H4; [congruence|subst]. simpl in H3; simpl in H9. + simpl in *. assert (chunk0 = chunk) by congruence. subst chunk0. - assert (storev chunk m (Vptr b Int.zero) v = Some m'). assumption. + assert (Mem.storev chunk m (Vptr b Int.zero) v = Some m'). assumption. assert (match_globalenvs f). eapply match_callstack_match_globalenvs; eauto. - inversion H11. destruct (mg_symbols0 _ _ H3) as [A B]. + exploit mg_symbols; eauto. intros [A B]. exploit make_store_correct. eapply make_globaladdr_correct; eauto. - eauto. eauto. eauto. eauto. eauto. - intros [tm' [EVAL [MEMINJ TNEXTBLOCK]]]. - exists (PTree.set id tv te); exists tm'. + eauto. eauto. eauto. eauto. eauto. + intros [tm' [tvrhs' [EVAL' [STORE' MEMINJ]]]]. + exists te'; exists tm'. split. eauto. split. auto. - rewrite NEXTBLOCK; rewrite TNEXTBLOCK. + split. rewrite NEXTBLOCK. rewrite (nextblock_storev _ _ _ _ _ STORE'). apply match_callstack_extensional with te. - intros. caseEq (cenv!!id0); intros; auto. - rewrite PTree.gsspec. destruct (peq id0 id). congruence. auto. - eapply match_callstack_mapped; eauto. congruence. + intros. apply OTHERS. congruence. + eapply match_callstack_store_mapped; eauto. + auto. Qed. (** * Correctness of stack allocation of local variables *) @@ -1361,26 +1829,38 @@ Proof. destruct (zlt sz 8); omega. Qed. -Remark assign_variables_incr: - forall atk vars cenv sz cenv' sz', - assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'. +Remark assign_variable_incr: + forall atk id lv cenv sz cenv' sz', + assign_variable atk (id, lv) (cenv, sz) = (cenv', sz') -> sz <= sz'. Proof. - induction vars; intros until sz'; simpl. - intro. replace sz' with sz. omega. congruence. - destruct a. destruct v. case (Identset.mem i atk); intros. - generalize (IHvars _ _ _ _ H). - generalize (size_chunk_pos m). intro. - generalize (align_le sz (size_chunk m) H0). omega. - eauto. - intro. generalize (IHvars _ _ _ _ H). + intros until sz'; simpl. + destruct lv. case (Identset.mem id atk); intros. + inv H. generalize (size_chunk_pos m). intro. + generalize (align_le sz (size_chunk m) H). omega. + inv H. omega. + intros. inv H. generalize (align_le sz (array_alignment z) (array_alignment_pos z)). assert (0 <= Zmax 0 z). apply Zmax_bound_l. omega. omega. Qed. + +Remark assign_variables_incr: + forall atk vars cenv sz cenv' sz', + assign_variables atk vars (cenv, sz) = (cenv', sz') -> sz <= sz'. +Proof. + induction vars; intros until sz'. + simpl; intros. replace sz' with sz. omega. congruence. +Opaque assign_variable. + destruct a as [id lv]. simpl. + case_eq (assign_variable atk (id, lv) (cenv, sz)). intros cenv1 sz1 EQ1 EQ2. + apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto. +Transparent assign_variable. +Qed. + Remark inj_offset_aligned_array: forall stacksize sz, - inj_offset_aligned (align stacksize (array_alignment sz)) sz. + Mem.inj_offset_aligned (align stacksize (array_alignment sz)) sz. Proof. intros; red; intros. apply Zdivides_trans with (array_alignment sz). @@ -1402,7 +1882,7 @@ Qed. Remark inj_offset_aligned_array': forall stacksize sz, - inj_offset_aligned (align stacksize (array_alignment sz)) (Zmax 0 sz). + Mem.inj_offset_aligned (align stacksize (array_alignment sz)) (Zmax 0 sz). Proof. intros. replace (array_alignment sz) with (array_alignment (Zmax 0 sz)). @@ -1413,7 +1893,7 @@ Qed. Remark inj_offset_aligned_var: forall stacksize chunk, - inj_offset_aligned (align stacksize (size_chunk chunk)) (size_chunk chunk). + Mem.inj_offset_aligned (align stacksize (size_chunk chunk)) (size_chunk chunk). Proof. intros. replace (align stacksize (size_chunk chunk)) @@ -1422,31 +1902,127 @@ Proof. decEq. destruct chunk; reflexivity. Qed. +Lemma match_callstack_alloc_variable: + forall atk id lv cenv sz cenv' sz' tm sp e tf m m' b te lo cs f tv, + assign_variable atk (id, lv) (cenv, sz) = (cenv', sz') -> + Mem.valid_block tm sp -> + Mem.bounds tm sp = (0, tf.(fn_stackspace)) -> + Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable -> + tf.(fn_stackspace) <= Int.max_signed -> + Mem.alloc m 0 (sizeof lv) = (m', b) -> + match_callstack f m tm + (Frame cenv tf e te sp lo (Mem.nextblock m) :: cs) + (Mem.nextblock m) (Mem.nextblock tm) -> + Mem.inject f m tm -> + 0 <= sz -> sz' <= tf.(fn_stackspace) -> + (forall b delta, f b = Some(sp, delta) -> Mem.high_bound m b + delta <= sz) -> + e!id = None -> + te!id = Some tv -> + exists f', + inject_incr f f' + /\ Mem.inject f' m' tm + /\ match_callstack f' m' tm + (Frame cenv' tf (PTree.set id (b, lv) e) te sp lo (Mem.nextblock m') :: cs) + (Mem.nextblock m') (Mem.nextblock tm) + /\ (forall b delta, + f' b = Some(sp, delta) -> Mem.high_bound m' b + delta <= sz'). +Proof. + intros until tv. intros ASV VALID BOUNDS PERMS NOOV ALLOC MCS INJ LO HI RANGE E TE. + generalize ASV. unfold assign_variable. + caseEq lv. + (* 1. lv = LVscalar chunk *) + intros chunk LV. case (Identset.mem id atk). + (* 1.1 info = Var_stack_scalar chunk ofs *) + set (ofs := align sz (size_chunk chunk)). + intro EQ; injection EQ; intros; clear EQ. rewrite <- H0. + generalize (size_chunk_pos chunk); intro SIZEPOS. + generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS. + exploit Mem.alloc_left_mapped_inject. + eauto. eauto. eauto. + instantiate (1 := ofs). + generalize Int.min_signed_neg. omega. + right; rewrite BOUNDS; simpl. generalize Int.min_signed_neg. omega. + intros. apply Mem.perm_implies with Freeable; auto with mem. + apply PERMS. rewrite LV in H1. simpl in H1. omega. + rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. + apply inj_offset_aligned_var. + intros. generalize (RANGE _ _ H1). omega. + intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]]. + exists f1; split. auto. split. auto. split. + eapply match_callstack_alloc_left; eauto. + rewrite <- LV; auto. + rewrite SAME; constructor. + intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). + destruct (eq_block b0 b); simpl. + subst b0. assert (delta = ofs) by congruence. subst delta. + rewrite LV. simpl. omega. + rewrite OTHER in H1; eauto. generalize (RANGE _ _ H1). omega. + (* 1.2 info = Var_local chunk *) + intro EQ; injection EQ; intros; clear EQ. subst sz'. rewrite <- H0. + exploit Mem.alloc_left_unmapped_inject; eauto. + intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]]. + exists f1; split. auto. split. auto. split. + eapply match_callstack_alloc_left; eauto. + rewrite <- LV; auto. + rewrite SAME; constructor. + intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). + destruct (eq_block b0 b); simpl. + subst b0. congruence. + rewrite OTHER in H; eauto. + (* 2 info = Var_stack_array ofs *) + intros dim LV EQ. injection EQ; clear EQ; intros. rewrite <- H0. + assert (0 <= Zmax 0 dim). apply Zmax1. + generalize (align_le sz (array_alignment dim) (array_alignment_pos dim)). intro. + set (ofs := align sz (array_alignment dim)) in *. + exploit Mem.alloc_left_mapped_inject. eauto. eauto. eauto. + instantiate (1 := ofs). + generalize Int.min_signed_neg. omega. + right; rewrite BOUNDS; simpl. generalize Int.min_signed_neg. omega. + intros. apply Mem.perm_implies with Freeable; auto with mem. + apply PERMS. rewrite LV in H3. simpl in H3. omega. + rewrite LV; simpl. rewrite Zminus_0_r. unfold ofs. + apply inj_offset_aligned_array'. + intros. generalize (RANGE _ _ H3). omega. + intros [f1 [MINJ1 [INCR1 [SAME OTHER]]]]. + exists f1; split. auto. split. auto. split. + eapply match_callstack_alloc_left; eauto. + rewrite <- LV; auto. + rewrite SAME; constructor. + intros. rewrite (Mem.bounds_alloc _ _ _ _ _ ALLOC). + destruct (eq_block b0 b); simpl. + subst b0. assert (delta = ofs) by congruence. subst delta. + rewrite LV. simpl. omega. + rewrite OTHER in H3; eauto. generalize (RANGE _ _ H3). omega. +Qed. + Lemma match_callstack_alloc_variables_rec: - forall tm sp cenv' sz' te lo cs atk, - valid_block tm sp -> - low_bound tm sp = 0 -> - high_bound tm sp = sz' -> - sz' <= Int.max_signed -> + forall tm sp cenv' tf te lo cs atk, + Mem.valid_block tm sp -> + Mem.bounds tm sp = (0, tf.(fn_stackspace)) -> + Mem.range_perm tm sp 0 tf.(fn_stackspace) Freeable -> + tf.(fn_stackspace) <= Int.max_signed -> forall e m vars e' m', alloc_variables e m vars e' m' -> forall f cenv sz, - assign_variables atk vars (cenv, sz) = (cenv', sz') -> - match_callstack f (mkframe cenv e te sp lo m.(nextblock) :: cs) - m.(nextblock) tm.(nextblock) m -> - mem_inject f m tm -> + assign_variables atk vars (cenv, sz) = (cenv', tf.(fn_stackspace)) -> + match_callstack f m tm + (Frame cenv tf e te sp lo (Mem.nextblock m) :: cs) + (Mem.nextblock m) (Mem.nextblock tm) -> + Mem.inject f m tm -> 0 <= sz -> - (forall b delta, f b = Some(sp, delta) -> high_bound m b + delta <= sz) -> + (forall b delta, + f b = Some(sp, delta) -> Mem.high_bound m b + delta <= sz) -> (forall id lv, In (id, lv) vars -> te!id <> None) -> list_norepet (List.map (@fst ident var_kind) vars) -> (forall id lv, In (id, lv) vars -> e!id = None) -> exists f', inject_incr f f' - /\ mem_inject f' m' tm - /\ match_callstack f' (mkframe cenv' e' te sp lo m'.(nextblock) :: cs) - m'.(nextblock) tm.(nextblock) m'. + /\ Mem.inject f' m' tm + /\ match_callstack f' m' tm + (Frame cenv' tf e' te sp lo (Mem.nextblock m') :: cs) + (Mem.nextblock m') (Mem.nextblock tm). Proof. - intros until atk. intros VB LB HB NOOV. + intros until atk. intros VALID BOUNDS PERM NOOV. induction 1. (* base case *) intros. simpl in H. inversion H; subst cenv sz. @@ -1462,81 +2038,18 @@ Proof. assert (exists tv, te!id = Some tv). assert (te!id <> None). eapply DEFINED. simpl; left; auto. destruct (te!id). exists v; auto. congruence. - elim H1; intros tv TEID; clear H1. - assert (UNDEFINED1: forall (id0 : ident) (lv0 : var_kind), - In (id0, lv0) vars -> - (PTree.set id (b1, lv) e)!id0 = None). - intros. rewrite PTree.gso. eapply UNDEFINED; eauto with coqlib. - simpl in NOREPET. inversion NOREPET. red; intro; subst id0. - elim H4. change id with (fst (id, lv0)). apply List.in_map. auto. - assert (NOREPET1: list_norepet (map (fst (A:=ident) (B:=var_kind)) vars)). - inv NOREPET; auto. - generalize ASV1. unfold assign_variable. - caseEq lv. - (* 1. lv = LVscalar chunk *) - intros chunk LV. case (Identset.mem id atk). - (* 1.1 info = Var_stack_scalar chunk ... *) - set (ofs := align sz (size_chunk chunk)). - intro EQ; injection EQ; intros; clear EQ. - set (f1 := extend_inject b1 (Some (sp, ofs)) f). - generalize (size_chunk_pos chunk); intro SIZEPOS. - generalize (align_le sz (size_chunk chunk) SIZEPOS). fold ofs. intro SZOFS. - assert (mem_inject f1 m1 tm /\ inject_incr f f1). - assert (Int.min_signed < 0). compute; auto. - generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro. - unfold f1; eapply alloc_mapped_inject; eauto. - omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. - rewrite Zminus_0_r. unfold ofs. rewrite LV. simpl. - apply inj_offset_aligned_var. - intros. left. generalize (BOUND _ _ H5). omega. - elim H3; intros MINJ1 INCR1; clear H3. - exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. - rewrite <- H1. omega. - intros until delta; unfold f1, extend_inject, eq_block. - rewrite (high_bound_alloc _ _ _ _ _ H b). - case (zeq b b1); intros. - inversion H3. unfold sizeof; rewrite LV. omega. - generalize (BOUND _ _ H3). omega. - intros [f' [INCR2 [MINJ2 MATCH2]]]. - exists f'; intuition. eapply inject_incr_trans; eauto. - (* 1.2 info = Var_local chunk *) - intro EQ; injection EQ; intros; clear EQ. subst sz1. - exploit alloc_unmapped_inject; eauto. - set (f1 := extend_inject b1 None f). intros [MINJ1 INCR1]. - exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. - intros until delta; unfold f1, extend_inject, eq_block. - rewrite (high_bound_alloc _ _ _ _ _ H b). - case (zeq b b1); intros. discriminate. - eapply BOUND; eauto. - intros [f' [INCR2 [MINJ2 MATCH2]]]. - exists f'; intuition. eapply inject_incr_trans; eauto. - (* 2. lv = LVarray dim, info = Var_stack_array *) - intros dim LV EQ. injection EQ; clear EQ; intros. - assert (0 <= Zmax 0 dim). apply Zmax1. - generalize (align_le sz (array_alignment dim) (array_alignment_pos dim)). intro. - set (ofs := align sz (array_alignment dim)) in *. - set (f1 := extend_inject b1 (Some (sp, ofs)) f). - assert (mem_inject f1 m1 tm /\ inject_incr f f1). - assert (Int.min_signed < 0). compute; auto. - generalize (assign_variables_incr _ _ _ _ _ _ ASVS). intro. - unfold f1; eapply alloc_mapped_inject; eauto. - omega. omega. omega. omega. unfold sizeof; rewrite LV. omega. - rewrite Zminus_0_r. unfold ofs. rewrite LV. simpl. - apply inj_offset_aligned_array'. - intros. left. generalize (BOUND _ _ H7). omega. - destruct H5 as [MINJ1 INCR1]. - exploit IHalloc_variables; eauto. - unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto with coqlib. - rewrite <- H1. omega. - intros until delta; unfold f1, extend_inject, eq_block. - rewrite (high_bound_alloc _ _ _ _ _ H b). - case (zeq b b1); intros. - inversion H5. unfold sizeof; rewrite LV. omega. - generalize (BOUND _ _ H5). omega. - intros [f' [INCR2 [MINJ2 MATCH2]]]. - exists f'; intuition. eapply inject_incr_trans; eauto. + destruct H1 as [tv TEID]. + assert (sz1 <= fn_stackspace tf). eapply assign_variables_incr; eauto. + exploit match_callstack_alloc_variable; eauto with coqlib. + intros [f1 [INCR1 [INJ1 [MCS1 BOUND1]]]]. + exploit IHalloc_variables; eauto. + apply Zle_trans with sz; auto. eapply assign_variable_incr; eauto. + inv NOREPET; auto. + intros. rewrite PTree.gso. eapply UNDEFINED; eauto with coqlib. + simpl in NOREPET. inversion NOREPET. red; intro; subst id0. + elim H5. change id with (fst (id, lv0)). apply List.in_map. auto. + intros [f2 [INCR2 [INJ2 MCS2]]]. + exists f2; intuition. eapply inject_incr_trans; eauto. Qed. Lemma set_params_defined: @@ -1578,56 +2091,32 @@ Qed. of Csharpminor local variables and of the Cminor stack data block. *) Lemma match_callstack_alloc_variables: - forall fn cenv sz m e m' tm tm' sp f cs targs body, - build_compilenv gce fn = (cenv, sz) -> - sz <= Int.max_signed -> + forall fn cenv tf m e m' tm tm' sp f cs targs body, + build_compilenv gce fn = (cenv, tf.(fn_stackspace)) -> + tf.(fn_stackspace) <= Int.max_signed -> list_norepet (fn_params_names fn ++ fn_vars_names fn) -> alloc_variables Csharpminor.empty_env m (fn_variables fn) e m' -> - Mem.alloc tm 0 sz = (tm', sp) -> - match_callstack f cs m.(nextblock) tm.(nextblock) m -> - mem_inject f m tm -> + Mem.alloc tm 0 tf.(fn_stackspace) = (tm', sp) -> + match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) -> + Mem.inject f m tm -> let tvars := make_vars (fn_params_names fn) (fn_vars_names fn) body in let te := set_locals tvars (set_params targs (fn_params_names fn)) in exists f', inject_incr f f' - /\ mem_inject f' m' tm' - /\ match_callstack f' (mkframe cenv e te sp m.(nextblock) m'.(nextblock) :: cs) - m'.(nextblock) tm'.(nextblock) m'. + /\ Mem.inject f' m' tm' + /\ match_callstack f' m' tm' + (Frame cenv tf e te sp (Mem.nextblock m) (Mem.nextblock m') :: cs) + (Mem.nextblock m') (Mem.nextblock tm'). Proof. intros. - assert (SP: sp = nextblock tm). injection H3; auto. unfold build_compilenv in H. - eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto with mem. - eapply low_bound_alloc_same; eauto. - eapply high_bound_alloc_same; eauto. - (* match_callstack *) - constructor. omega. change (valid_block tm' sp). eapply valid_new_block; eauto. - constructor. - (* me_vars *) - intros. generalize (global_compilenv_charact id). - destruct (gce!!id); intro; try contradiction. - constructor. - unfold Csharpminor.empty_env. apply PTree.gempty. auto. - constructor. - unfold Csharpminor.empty_env. apply PTree.gempty. - (* me_low_high *) - omega. - (* me_bounded *) - intros until lv. unfold Csharpminor.empty_env. rewrite PTree.gempty. congruence. - (* me_inj *) - intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence. - (* me_inv *) - intros. exploit mi_mappedblocks; eauto. intro A. - elim (fresh_block_alloc _ _ _ _ _ H3 A). - (* me_incr *) - intros. exploit mi_mappedblocks; eauto. intro A. - rewrite SP; auto. - rewrite SP; auto. - eapply alloc_right_inject; eauto. - omega. - intros. exploit mi_mappedblocks; eauto. unfold valid_block; intro. - unfold block in SP; omegaContradiction. - (* defined *) + eapply match_callstack_alloc_variables_rec; eauto with mem. + eapply Mem.bounds_alloc_same; eauto. + red; intros; eauto with mem. + eapply match_callstack_alloc_right; eauto. + eapply Mem.alloc_right_inject; eauto. omega. + intros. elim (Mem.valid_not_valid_diff tm sp sp); eauto with mem. + eapply Mem.valid_block_inject_2; eauto. intros. unfold te. apply set_locals_params_defined. elim (in_app_or _ _ _ H6); intros. elim (list_in_map_inv _ _ _ H7). intros x [A B]. @@ -1645,15 +2134,16 @@ Qed. (** Correctness of the code generated by [store_parameters] to store in memory the values of parameters that are stack-allocated. *) -Inductive vars_vals_match: - meminj -> list (ident * memory_chunk) -> list val -> env -> Prop := +Inductive vars_vals_match (f:meminj): + list (ident * memory_chunk) -> list val -> env -> Prop := | vars_vals_nil: - forall f te, + forall te, vars_vals_match f nil nil te | vars_vals_cons: - forall f te id chunk vars v vals tv, + forall te id chunk vars v vals tv, te!id = Some tv -> val_inject f v tv -> + Val.has_type v (type_of_chunk chunk) -> vars_vals_match f vars vals te -> vars_vals_match f ((id, chunk) :: vars) (v :: vals) te. @@ -1666,24 +2156,25 @@ Lemma vars_vals_match_extensional: Proof. induction 1; intros. constructor. - econstructor; eauto. rewrite <- H. eapply H2. left. reflexivity. - apply IHvars_vals_match. intros. eapply H2; eauto. right. eauto. + econstructor; eauto. + rewrite <- H. eauto with coqlib. + apply IHvars_vals_match. intros. eapply H3; eauto with coqlib. Qed. Lemma store_parameters_correct: forall e m1 params vl m2, bind_parameters e m1 params vl m2 -> - forall s f te1 cenv sp lo hi cs tm1 fn k, + forall s f te1 cenv tf sp lo hi cs tm1 fn k, vars_vals_match f params vl te1 -> - list_norepet (List.map (@fst ident memory_chunk) params) -> - mem_inject f m1 tm1 -> - match_callstack f (mkframe cenv e te1 sp lo hi :: cs) m1.(nextblock) tm1.(nextblock) m1 -> + list_norepet (List.map param_name params) -> + Mem.inject f m1 tm1 -> + match_callstack f m1 tm1 (Frame cenv tf e te1 sp lo hi :: cs) (Mem.nextblock m1) (Mem.nextblock tm1) -> store_parameters cenv params = OK s -> exists te2, exists tm2, star step tge (State fn s k (Vptr sp Int.zero) te1 tm1) E0 (State fn Sskip k (Vptr sp Int.zero) te2 tm2) - /\ mem_inject f m2 tm2 - /\ match_callstack f (mkframe cenv e te2 sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2. + /\ Mem.inject f m2 tm2 + /\ match_callstack f m2 tm2 (Frame cenv tf e te2 sp lo hi :: cs) (Mem.nextblock m2) (Mem.nextblock tm2). Proof. induction 1. (* base case *) @@ -1692,17 +2183,15 @@ Proof. (* inductive case *) intros until k. intros VVM NOREPET MINJ MATCH STOREP. monadInv STOREP. - inversion VVM. subst f0 id0 chunk0 vars v vals te. - inversion NOREPET. subst hd tl. - exploit var_set_correct; eauto. - constructor; auto. - econstructor; eauto. - econstructor; eauto. + inv VVM. + inv NOREPET. + exploit var_set_self_correct; eauto. + econstructor; eauto. econstructor; eauto. intros [te2 [tm2 [EXEC1 [MINJ1 [MATCH1 UNCHANGED1]]]]]. assert (vars_vals_match f params vl te2). apply vars_vals_match_extensional with te1; auto. intros. apply UNCHANGED1. red; intro; subst id0. - elim H4. change id with (fst (id, lv)). apply List.in_map. auto. + elim H4. change id with (param_name (id, lv)). apply List.in_map. auto. exploit IHbind_parameters; eauto. intros [te3 [tm3 [EXEC2 [MINJ2 MATCH2]]]]. exists te3; exists tm3. @@ -1715,50 +2204,42 @@ Qed. Lemma vars_vals_match_holds_1: forall f params args targs, - list_norepet (List.map (@fst ident memory_chunk) params) -> - List.length params = List.length args -> + list_norepet (List.map param_name params) -> val_list_inject f args targs -> + Val.has_type_list args (List.map type_of_chunk (List.map param_chunk params)) -> vars_vals_match f params args (set_params targs (List.map (@fst ident memory_chunk) params)). Proof. - induction params; destruct args; simpl; intros; try discriminate. + induction params; simpl; intros. + destruct args; simpl in H1; try contradiction. inv H0. constructor. - inversion H1. subst v0 vl targs. - inversion H. subst hd tl. - destruct a as [id chunk]. econstructor. - simpl. rewrite PTree.gss. reflexivity. - auto. + destruct args; simpl in H1; try contradiction. destruct H1. inv H0. inv H. + destruct a as [id chunk]; simpl in *. econstructor. + rewrite PTree.gss. reflexivity. + auto. auto. apply vars_vals_match_extensional - with (set_params vl' (map (@fst ident memory_chunk) params)). + with (set_params vl' (map param_name params)). eapply IHparams; eauto. intros. simpl. apply PTree.gso. red; intro; subst id0. - elim H5. change (fst (id, chunk)) with (fst (id, lv)). - apply List.in_map; auto. + elim H4. change id with (param_name (id, lv)). apply List.in_map; auto. Qed. Lemma vars_vals_match_holds: forall f params args targs, - List.length params = List.length args -> + list_norepet (List.map param_name params) -> val_list_inject f args targs -> + Val.has_type_list args (List.map type_of_chunk (List.map param_chunk params)) -> forall vars, - list_norepet (vars ++ List.map (@fst ident memory_chunk) params) -> + list_norepet (vars ++ List.map param_name params) -> vars_vals_match f params args - (set_locals vars (set_params targs (List.map (@fst ident memory_chunk) params))). + (set_locals vars (set_params targs (List.map param_name params))). Proof. induction vars; simpl; intros. eapply vars_vals_match_holds_1; eauto. - inversion H1. subst hd tl. + inv H2. eapply vars_vals_match_extensional; eauto. - intros. apply PTree.gso. red; intro; subst id; elim H4. - apply in_or_app. right. change a with (fst (a, lv)). apply List.in_map; auto. -Qed. - -Lemma bind_parameters_length: - forall e m1 params args m2, - bind_parameters e m1 params args m2 -> - List.length params = List.length args. -Proof. - induction 1; simpl; eauto. + intros. apply PTree.gso. red; intro; subst id; elim H5. + apply in_or_app. right. change a with (param_name (a, lv)). apply List.in_map; auto. Qed. Remark identset_removelist_charact: @@ -1815,45 +2296,44 @@ Qed. and initialize the blocks corresponding to function parameters). *) Lemma function_entry_ok: - forall fn m e m1 vargs m2 f cs tm cenv sz tm1 sp tvargs body s fn' k, + forall fn m e m1 vargs m2 f cs tm cenv tf tm1 sp tvargs body s fn' k, + list_norepet (fn_params_names fn ++ fn_vars_names fn) -> alloc_variables empty_env m (fn_variables fn) e m1 -> bind_parameters e m1 fn.(Csharpminor.fn_params) vargs m2 -> - match_callstack f cs m.(nextblock) tm.(nextblock) m -> - build_compilenv gce fn = (cenv, sz) -> - sz <= Int.max_signed -> - Mem.alloc tm 0 sz = (tm1, sp) -> + match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm) -> + build_compilenv gce fn = (cenv, tf.(fn_stackspace)) -> + tf.(fn_stackspace) <= Int.max_signed -> + Mem.alloc tm 0 tf.(fn_stackspace) = (tm1, sp) -> let vars := make_vars (fn_params_names fn) (fn_vars_names fn) body in let te := set_locals vars (set_params tvargs (fn_params_names fn)) in val_list_inject f vargs tvargs -> - mem_inject f m tm -> - list_norepet (fn_params_names fn ++ fn_vars_names fn) -> + Val.has_type_list vargs (Csharpminor.fn_sig fn).(sig_args) -> + Mem.inject f m tm -> store_parameters cenv fn.(Csharpminor.fn_params) = OK s -> exists f2, exists te2, exists tm2, star step tge (State fn' s k (Vptr sp Int.zero) te tm1) E0 (State fn' Sskip k (Vptr sp Int.zero) te2 tm2) - /\ mem_inject f2 m2 tm2 + /\ Mem.inject f2 m2 tm2 /\ inject_incr f f2 - /\ match_callstack f2 - (mkframe cenv e te2 sp m.(nextblock) m1.(nextblock) :: cs) - m2.(nextblock) tm2.(nextblock) m2. + /\ match_callstack f2 m2 tm2 + (Frame cenv tf e te2 sp (Mem.nextblock m) (Mem.nextblock m1) :: cs) + (Mem.nextblock m2) (Mem.nextblock tm2). Proof. - intros. - exploit bind_parameters_length; eauto. intro LEN1. + intros. exploit match_callstack_alloc_variables; eauto. intros [f1 [INCR1 [MINJ1 MATCH1]]]. exploit vars_vals_match_holds. - eauto. apply val_list_inject_incr with f. eauto. eauto. - eapply make_vars_norepet. auto. + eapply list_norepet_append_left. eexact H. + apply val_list_inject_incr with f. eauto. eauto. + auto. eapply make_vars_norepet. auto. intro VVM. exploit store_parameters_correct. - eauto. eauto. - unfold fn_params_names in H7. eapply list_norepet_append_left; eauto. - eexact MINJ1. fold (fn_params_names fn). eexact MATCH1. eauto. + eauto. eauto. eapply list_norepet_append_left; eauto. + eexact MINJ1. fold (fn_params_names fn). eexact MATCH1. eauto. intros [te2 [tm2 [EXEC [MINJ2 MATCH2]]]]. - exists f1; exists te2; exists tm2. - split. eauto. auto. + exists f1; exists te2; exists tm2. eauto. Qed. (** * Semantic preservation for the translation *) @@ -1890,11 +2370,11 @@ Proof. Qed. Lemma transl_expr_correct: - forall f m tm cenv e te sp lo hi cs - (MINJ: mem_inject f m tm) - (MATCH: match_callstack f - (mkframe cenv e te sp lo hi :: cs) - m.(nextblock) tm.(nextblock) m), + forall f m tm cenv tf e te sp lo hi cs + (MINJ: Mem.inject f m tm) + (MATCH: match_callstack f m tm + (Frame cenv tf e te sp lo hi :: cs) + (Mem.nextblock m) (Mem.nextblock tm)), forall a v, Csharpminor.eval_expr gve e m a v -> forall ta @@ -1922,7 +2402,7 @@ Proof. exists tv; split. econstructor; eauto. auto. (* Eload *) exploit IHeval_expr; eauto. intros [tv1 [EVAL1 INJ1]]. - exploit loadv_inject; eauto. intros [tv [LOAD INJ]]. + exploit Mem.loadv_inject; eauto. intros [tv [LOAD INJ]]. exists tv; split. econstructor; eauto. auto. (* Econdition *) exploit IHeval_expr1; eauto. intros [tv1 [EVAL1 INJ1]]. @@ -1935,11 +2415,11 @@ Proof. Qed. Lemma transl_exprlist_correct: - forall f m tm cenv e te sp lo hi cs - (MINJ: mem_inject f m tm) - (MATCH: match_callstack f - (mkframe cenv e te sp lo hi :: cs) - m.(nextblock) tm.(nextblock) m), + forall f m tm cenv tf e te sp lo hi cs + (MINJ: Mem.inject f m tm) + (MATCH: match_callstack f m tm + (Frame cenv tf e te sp lo hi :: cs) + (Mem.nextblock m) (Mem.nextblock tm)), forall a v, Csharpminor.eval_exprlist gve e m a v -> forall ta @@ -1957,86 +2437,84 @@ Qed. (** ** Semantic preservation for statements and functions *) -Inductive match_cont: Csharpminor.cont -> Cminor.cont -> compilenv -> exit_env -> callstack -> Prop := - | match_Kstop: forall cenv xenv, - match_cont Csharpminor.Kstop Kstop cenv xenv nil - | match_Kseq: forall s k ts tk cenv xenv cs, - transl_stmt cenv xenv s = OK ts -> - match_cont k tk cenv xenv cs -> - match_cont (Csharpminor.Kseq s k) (Kseq ts tk) cenv xenv cs - | match_Kseq2: forall s1 s2 k ts1 tk cenv xenv cs, - transl_stmt cenv xenv s1 = OK ts1 -> - match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs -> +Inductive match_cont: Csharpminor.cont -> Cminor.cont -> option typ -> compilenv -> exit_env -> callstack -> Prop := + | match_Kstop: forall ty cenv xenv, + match_cont Csharpminor.Kstop Kstop ty cenv xenv nil + | match_Kseq: forall s k ts tk ty cenv xenv cs, + transl_stmt ty cenv xenv s = OK ts -> + match_cont k tk ty cenv xenv cs -> + match_cont (Csharpminor.Kseq s k) (Kseq ts tk) ty cenv xenv cs + | match_Kseq2: forall s1 s2 k ts1 tk ty cenv xenv cs, + transl_stmt ty cenv xenv s1 = OK ts1 -> + match_cont (Csharpminor.Kseq s2 k) tk ty cenv xenv cs -> match_cont (Csharpminor.Kseq (Csharpminor.Sseq s1 s2) k) - (Kseq ts1 tk) cenv xenv cs - | match_Kblock: forall k tk cenv xenv cs, - match_cont k tk cenv xenv cs -> - match_cont (Csharpminor.Kblock k) (Kblock tk) cenv (true :: xenv) cs - | match_Kblock2: forall k tk cenv xenv cs, - match_cont k tk cenv xenv cs -> - match_cont k (Kblock tk) cenv (false :: xenv) cs - | match_Kcall_none: forall fn e k tfn sp te tk cenv xenv lo hi cs sz cenv', + (Kseq ts1 tk) ty cenv xenv cs + | match_Kblock: forall k tk ty cenv xenv cs, + match_cont k tk ty cenv xenv cs -> + match_cont (Csharpminor.Kblock k) (Kblock tk) ty cenv (true :: xenv) cs + | match_Kblock2: forall k tk ty cenv xenv cs, + match_cont k tk ty cenv xenv cs -> + match_cont k (Kblock tk) ty cenv (false :: xenv) cs + | match_Kcall_none: forall fn e k tfn sp te tk ty cenv xenv lo hi cs sz cenv', transl_funbody cenv sz fn = OK tfn -> - match_cont k tk cenv xenv cs -> + match_cont k tk fn.(fn_return) cenv xenv cs -> match_cont (Csharpminor.Kcall None fn e k) (Kcall None tfn (Vptr sp Int.zero) te tk) - cenv' nil - (mkframe cenv e te sp lo hi :: cs) - | match_Kcall_some: forall id fn e k tfn s sp te tk cenv xenv lo hi cs sz cenv', + ty cenv' nil + (Frame cenv tfn e te sp lo hi :: cs) + | match_Kcall_some: forall id fn e k tfn s sp te tk ty cenv xenv lo hi cs sz cenv', transl_funbody cenv sz fn = OK tfn -> - var_set cenv id (Evar id) = OK s -> - match_cont k tk cenv xenv cs -> + var_set_self cenv id (typ_of_opttyp ty) = OK s -> + match_cont k tk fn.(fn_return) cenv xenv cs -> match_cont (Csharpminor.Kcall (Some id) fn e k) (Kcall (Some id) tfn (Vptr sp Int.zero) te (Kseq s tk)) - cenv' nil - (mkframe cenv e te sp lo hi :: cs). + ty cenv' nil + (Frame cenv tfn e te sp lo hi :: cs). Inductive match_states: Csharpminor.state -> Cminor.state -> Prop := | match_state: forall fn s k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz (TRF: transl_funbody cenv sz fn = OK tfn) - (TR: transl_stmt cenv xenv s = OK ts) - (MINJ: mem_inject f m tm) - (MCS: match_callstack f - (mkframe cenv e te sp lo hi :: cs) - m.(nextblock) tm.(nextblock) m) - (MK: match_cont k tk cenv xenv cs), + (TR: transl_stmt fn.(fn_return) cenv xenv s = OK ts) + (MINJ: Mem.inject f m tm) + (MCS: match_callstack f m tm + (Frame cenv tfn e te sp lo hi :: cs) + (Mem.nextblock m) (Mem.nextblock tm)) + (MK: match_cont k tk fn.(fn_return) cenv xenv cs), match_states (Csharpminor.State fn s k e m) (State tfn ts tk (Vptr sp Int.zero) te tm) | match_state_seq: forall fn s1 s2 k e m tfn ts1 tk sp te tm cenv xenv f lo hi cs sz (TRF: transl_funbody cenv sz fn = OK tfn) - (TR: transl_stmt cenv xenv s1 = OK ts1) - (MINJ: mem_inject f m tm) - (MCS: match_callstack f - (mkframe cenv e te sp lo hi :: cs) - m.(nextblock) tm.(nextblock) m) - (MK: match_cont (Csharpminor.Kseq s2 k) tk cenv xenv cs), + (TR: transl_stmt fn.(fn_return) cenv xenv s1 = OK ts1) + (MINJ: Mem.inject f m tm) + (MCS: match_callstack f m tm + (Frame cenv tfn e te sp lo hi :: cs) + (Mem.nextblock m) (Mem.nextblock tm)) + (MK: match_cont (Csharpminor.Kseq s2 k) tk fn.(fn_return) cenv xenv cs), match_states (Csharpminor.State fn (Csharpminor.Sseq s1 s2) k e m) (State tfn ts1 tk (Vptr sp Int.zero) te tm) | match_callstate: forall fd args k m tfd targs tk tm f cs cenv (TR: transl_fundef gce fd = OK tfd) - (MINJ: mem_inject f m tm) - (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m) - (MK: match_cont k tk cenv nil cs) + (MINJ: Mem.inject f m tm) + (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm)) + (MK: match_cont k tk (Csharpminor.funsig fd).(sig_res) cenv nil cs) (ISCC: Csharpminor.is_call_cont k) - (ARGSINJ: val_list_inject f args targs), + (ARGSINJ: val_list_inject f args targs) + (ARGSTY: Val.has_type_list args (Csharpminor.funsig fd).(sig_args)), match_states (Csharpminor.Callstate fd args k m) (Callstate tfd targs tk tm) | match_returnstate: - forall v k m tv tk tm f cs cenv - (MINJ: mem_inject f m tm) - (MCS: match_callstack f cs m.(nextblock) tm.(nextblock) m) - (MK: match_cont k tk cenv nil cs) - (RESINJ: val_inject f v tv), + forall v k m tv tk tm f cs ty cenv + (MINJ: Mem.inject f m tm) + (MCS: match_callstack f m tm cs (Mem.nextblock m) (Mem.nextblock tm)) + (MK: match_cont k tk ty cenv nil cs) + (RESINJ: val_inject f v tv) + (RESTY: Val.has_type v (typ_of_opttyp ty)), match_states (Csharpminor.Returnstate v k m) (Returnstate tv tk tm). -Remark nextblock_freelist: - forall lb m, nextblock (free_list m lb) = nextblock m. -Proof. induction lb; intros; simpl; auto. Qed. - Remark val_inject_function_pointer: forall v fd f tv, Genv.find_funct tge v = Some fd -> @@ -2052,22 +2530,22 @@ Proof. Qed. Lemma match_call_cont: - forall k tk cenv xenv cs, - match_cont k tk cenv xenv cs -> - match_cont (Csharpminor.call_cont k) (call_cont tk) cenv nil cs. + forall k tk ty cenv xenv cs, + match_cont k tk ty cenv xenv cs -> + match_cont (Csharpminor.call_cont k) (call_cont tk) ty cenv nil cs. Proof. induction 1; simpl; auto; econstructor; eauto. Qed. Lemma match_is_call_cont: - forall tfn te sp tm k tk cenv xenv cs, - match_cont k tk cenv xenv cs -> + forall tfn te sp tm k tk ty cenv xenv cs, + match_cont k tk ty cenv xenv cs -> Csharpminor.is_call_cont k -> exists tk', star step tge (State tfn Sskip tk sp te tm) E0 (State tfn Sskip tk' sp te tm) /\ is_call_cont tk' - /\ match_cont k tk' cenv nil cs. + /\ match_cont k tk' ty cenv nil cs. Proof. induction 1; simpl; intros; try contradiction. econstructor; split. apply star_refl. split. exact I. econstructor; eauto. @@ -2080,8 +2558,6 @@ Qed. (** Properties of [switch] compilation *) -Require Import Switch. - Remark switch_table_shift: forall n sl base dfl, switch_target n (S dfl) (switch_table sl (S base)) = @@ -2097,20 +2573,20 @@ Proof. induction sl; intros; simpl. auto. decEq; auto. Qed. -Inductive transl_lblstmt_cont (cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop := +Inductive transl_lblstmt_cont (ty: option typ) (cenv: compilenv) (xenv: exit_env): lbl_stmt -> cont -> cont -> Prop := | tlsc_default: forall s k ts, - transl_stmt cenv (switch_env (LSdefault s) xenv) s = OK ts -> - transl_lblstmt_cont cenv xenv (LSdefault s) k (Kblock (Kseq ts k)) + transl_stmt ty cenv (switch_env (LSdefault s) xenv) s = OK ts -> + transl_lblstmt_cont ty cenv xenv (LSdefault s) k (Kblock (Kseq ts k)) | tlsc_case: forall i s ls k ts k', - transl_stmt cenv (switch_env (LScase i s ls) xenv) s = OK ts -> - transl_lblstmt_cont cenv xenv ls k k' -> - transl_lblstmt_cont cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')). + transl_stmt ty cenv (switch_env (LScase i s ls) xenv) s = OK ts -> + transl_lblstmt_cont ty cenv xenv ls k k' -> + transl_lblstmt_cont ty cenv xenv (LScase i s ls) k (Kblock (Kseq ts k')). Lemma switch_descent: - forall cenv xenv k ls body s, - transl_lblstmt cenv (switch_env ls xenv) ls body = OK s -> + forall ty cenv xenv k ls body s, + transl_lblstmt ty cenv (switch_env ls xenv) ls body = OK s -> exists k', - transl_lblstmt_cont cenv xenv ls k k' + transl_lblstmt_cont ty cenv xenv ls k k' /\ (forall f sp e m, plus step tge (State f s k sp e m) E0 (State f body k' sp e m)). Proof. @@ -2127,14 +2603,14 @@ Proof. Qed. Lemma switch_ascent: - forall f n sp e m cenv xenv k ls k1, + forall f n sp e m ty cenv xenv k ls k1, let tbl := switch_table ls O in let ls' := select_switch n ls in - transl_lblstmt_cont cenv xenv ls k k1 -> + transl_lblstmt_cont ty cenv xenv ls k k1 -> exists k2, star step tge (State f (Sexit (switch_target n (length tbl) tbl)) k1 sp e m) E0 (State f (Sexit O) k2 sp e m) - /\ transl_lblstmt_cont cenv xenv ls' k k2. + /\ transl_lblstmt_cont ty cenv xenv ls' k k2. Proof. induction ls; intros; unfold tbl, ls'; simpl. inv H. econstructor; split. apply star_refl. econstructor; eauto. @@ -2151,10 +2627,10 @@ Proof. Qed. Lemma switch_match_cont: - forall cenv xenv k cs tk ls tk', - match_cont k tk cenv xenv cs -> - transl_lblstmt_cont cenv xenv ls tk tk' -> - match_cont (Csharpminor.Kseq (seq_of_lbl_stmt ls) k) tk' cenv (false :: switch_env ls xenv) cs. + forall ty cenv xenv k cs tk ls tk', + match_cont k tk ty cenv xenv cs -> + transl_lblstmt_cont ty cenv xenv ls tk tk' -> + match_cont (Csharpminor.Kseq (seq_of_lbl_stmt ls) k) tk' ty cenv (false :: switch_env ls xenv) cs. Proof. induction ls; intros; simpl. inv H0. apply match_Kblock2. econstructor; eauto. @@ -2162,11 +2638,11 @@ Proof. Qed. Lemma transl_lblstmt_suffix: - forall n cenv xenv ls body ts, - transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> + forall n ty cenv xenv ls body ts, + transl_lblstmt ty cenv (switch_env ls xenv) ls body = OK ts -> let ls' := select_switch n ls in exists body', exists ts', - transl_lblstmt cenv (switch_env ls' xenv) ls' body' = OK ts'. + transl_lblstmt ty cenv (switch_env ls' xenv) ls' body' = OK ts'. Proof. induction ls; simpl; intros. monadInv H. @@ -2180,13 +2656,13 @@ Qed. Lemma switch_match_states: forall fn k e m tfn ts tk sp te tm cenv xenv f lo hi cs sz ls body tk' (TRF: transl_funbody cenv sz fn = OK tfn) - (TR: transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts) - (MINJ: mem_inject f m tm) - (MCS: match_callstack f - (mkframe cenv e te sp lo hi :: cs) - m.(nextblock) tm.(nextblock) m) - (MK: match_cont k tk cenv xenv cs) - (TK: transl_lblstmt_cont cenv xenv ls tk tk'), + (TR: transl_lblstmt (fn_return fn) cenv (switch_env ls xenv) ls body = OK ts) + (MINJ: Mem.inject f m tm) + (MCS: match_callstack f m tm + (Frame cenv tfn e te sp lo hi :: cs) + (Mem.nextblock m) (Mem.nextblock tm)) + (MK: match_cont k tk (fn_return fn) cenv xenv cs) + (TK: transl_lblstmt_cont (fn_return fn) cenv xenv ls tk tk'), exists S, plus step tge (State tfn (Sexit O) tk' (Vptr sp Int.zero) te tm) E0 S /\ match_states (Csharpminor.State fn (seq_of_lbl_stmt ls) k e m) S. @@ -2206,22 +2682,35 @@ Qed. Section FIND_LABEL. Variable lbl: label. +Variable ty: option typ. Variable cenv: compilenv. Variable cs: callstack. Remark find_label_var_set: - forall id e s k, - var_set cenv id e = OK s -> + forall id e chunk s k, + var_set cenv id e chunk = OK s -> find_label lbl s k = None. Proof. intros. unfold var_set in H. - destruct (cenv!!id); monadInv H; reflexivity. + destruct (cenv!!id); try (monadInv H; reflexivity). + destruct (chunktype_compat chunk m). inv H; auto. + destruct (typ_eq (type_of_chunk m) (type_of_chunk chunk)); inv H; auto. +Qed. + +Remark find_label_var_set_self: + forall id ty s k, + var_set_self cenv id ty = OK s -> + find_label lbl s k = None. +Proof. + intros. unfold var_set_self in H. + destruct (cenv!!id); try (monadInv H; reflexivity). + destruct (typ_eq (type_of_chunk m) ty0); inv H; reflexivity. Qed. Lemma transl_lblstmt_find_label_context: - forall cenv xenv ls body ts tk1 tk2 ts' tk', - transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> - transl_lblstmt_cont cenv xenv ls tk1 tk2 -> + forall xenv ls body ts tk1 tk2 ts' tk', + transl_lblstmt ty cenv (switch_env ls xenv) ls body = OK ts -> + transl_lblstmt_cont ty cenv xenv ls tk1 tk2 -> find_label lbl body tk2 = Some (ts', tk') -> find_label lbl ts tk1 = Some (ts', tk'). Proof. @@ -2234,30 +2723,30 @@ Qed. Lemma transl_find_label: forall s k xenv ts tk, - transl_stmt cenv xenv s = OK ts -> - match_cont k tk cenv xenv cs -> + transl_stmt ty cenv xenv s = OK ts -> + match_cont k tk ty cenv xenv cs -> match Csharpminor.find_label lbl s k with | None => find_label lbl ts tk = None | Some(s', k') => exists ts', exists tk', exists xenv', find_label lbl ts tk = Some(ts', tk') - /\ transl_stmt cenv xenv' s' = OK ts' - /\ match_cont k' tk' cenv xenv' cs + /\ transl_stmt ty cenv xenv' s' = OK ts' + /\ match_cont k' tk' ty cenv xenv' cs end with transl_lblstmt_find_label: forall ls xenv body k ts tk tk1, - transl_lblstmt cenv (switch_env ls xenv) ls body = OK ts -> - match_cont k tk cenv xenv cs -> - transl_lblstmt_cont cenv xenv ls tk tk1 -> + transl_lblstmt ty cenv (switch_env ls xenv) ls body = OK ts -> + match_cont k tk ty cenv xenv cs -> + transl_lblstmt_cont ty cenv xenv ls tk tk1 -> find_label lbl body tk1 = None -> match Csharpminor.find_label_ls lbl ls k with | None => find_label lbl ts tk = None | Some(s', k') => exists ts', exists tk', exists xenv', find_label lbl ts tk = Some(ts', tk') - /\ transl_stmt cenv xenv' s' = OK ts' - /\ match_cont k' tk' cenv xenv' cs + /\ transl_stmt ty cenv xenv' s' = OK ts' + /\ match_cont k' tk' ty cenv xenv' cs end. Proof. intros. destruct s; try (monadInv H); simpl; auto. @@ -2265,7 +2754,10 @@ Proof. eapply find_label_var_set; eauto. (* call *) destruct o; monadInv H; simpl; auto. - eapply find_label_var_set; eauto. + destruct (list_eq_dec typ_eq x1 (sig_args s)); monadInv EQ4. + simpl. eapply find_label_var_set_self; eauto. + destruct (list_eq_dec typ_eq x1 (sig_args s)); monadInv EQ3. + simpl; eauto. (* seq *) exploit (transl_find_label s1). eauto. eapply match_Kseq. eexact EQ1. eauto. destruct (Csharpminor.find_label lbl s1 (Csharpminor.Kseq s2 k)) as [[s' k'] | ]. @@ -2287,6 +2779,7 @@ Proof. eapply transl_lblstmt_find_label. eauto. eauto. eauto. reflexivity. (* return *) destruct o; monadInv H; auto. + destruct (typ_eq x0 (typ_of_opttyp ty)); monadInv EQ2; auto. (* label *) destruct (ident_eq lbl l). exists x; exists tk; exists xenv; auto. @@ -2316,7 +2809,7 @@ Proof. induction vars; intros. monadInv H. auto. simpl in H. destruct a as [id lv]. monadInv H. - simpl. rewrite (find_label_var_set id (Evar id)); auto. + simpl. rewrite (find_label_var_set_self id (type_of_chunk lv)); auto. Qed. End FIND_LABEL. @@ -2324,12 +2817,12 @@ End FIND_LABEL. Lemma transl_find_label_body: forall cenv xenv size f tf k tk cs lbl s' k', transl_funbody cenv size f = OK tf -> - match_cont k tk cenv xenv cs -> + match_cont k tk (fn_return f) cenv xenv cs -> Csharpminor.find_label lbl f.(Csharpminor.fn_body) (Csharpminor.call_cont k) = Some (s', k') -> exists ts', exists tk', exists xenv', find_label lbl tf.(fn_body) (call_cont tk) = Some(ts', tk') - /\ transl_stmt cenv xenv' s' = OK ts' - /\ match_cont k' tk' cenv xenv' cs. + /\ transl_stmt (fn_return f) cenv xenv' s' = OK ts' + /\ match_cont k' tk' (fn_return f) cenv xenv' cs. Proof. intros. monadInv H. simpl. rewrite (find_label_store_parameters lbl cenv (Csharpminor.fn_params f)); auto. @@ -2337,8 +2830,7 @@ Proof. instantiate (1 := lbl). rewrite H1. auto. Qed. - -Require Import Coq.Program.Equality. +(** The simulation diagram. *) Fixpoint seq_left_depth (s: Csharpminor.stmt) : nat := match s with @@ -2384,16 +2876,17 @@ Proof. (* skip call *) monadInv TR. left. exploit match_is_call_cont; eauto. intros [tk' [A [B C]]]. - exploit match_callstack_freelist; eauto. intros [P Q]. + exploit match_callstack_freelist; eauto. intros [tm' [P [Q R]]]. econstructor; split. eapply plus_right. eexact A. apply step_skip_call. auto. - rewrite (sig_preserved_body _ _ _ _ TRF). auto. traceEq. - econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. + rewrite (sig_preserved_body _ _ _ _ TRF). auto. eauto. traceEq. + econstructor; eauto. exact I. (* assign *) monadInv TR. exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. - exploit var_set_correct; eauto. intros [te' [tm' [EXEC [MINJ' [MCS' OTHER]]]]]. + exploit var_set_correct; eauto. eapply chunktype_expr_correct; eauto. + intros [te' [tm' [EXEC [MINJ' [MCS' OTHER]]]]]. left; econstructor; split. apply plus_one. eexact EXEC. econstructor; eauto. @@ -2405,19 +2898,20 @@ Proof. exploit transl_expr_correct. eauto. eauto. eexact H0. eauto. intros [tv2 [EVAL2 VINJ2]]. exploit make_store_correct. eexact EVAL1. eexact EVAL2. eauto. eauto. auto. auto. - intros [tm' [EXEC [MINJ' NEXTBLOCK]]]. + intros [tm' [tv' [EXEC [STORE' MINJ']]]]. left; econstructor; split. apply plus_one. eexact EXEC. - unfold storev in H1; destruct vaddr; try discriminate. econstructor; eauto. - replace (nextblock m') with (nextblock m). rewrite NEXTBLOCK. eauto. - eapply match_callstack_mapped; eauto. inv VINJ1. congruence. - symmetry. eapply nextblock_store; eauto. + eapply match_callstack_storev_mapped. eexact VINJ1. eauto. eauto. + rewrite (nextblock_storev _ _ _ _ _ H1). + rewrite (nextblock_storev _ _ _ _ _ STORE'). + eauto. (* call *) simpl in H1. exploit functions_translated; eauto. intros [tfd [FIND TRANS]]. simpl in TR. destruct optid; monadInv TR. (* with return value *) + destruct (list_eq_dec typ_eq x1 (sig_args (Csharpminor.funsig fd))); monadInv EQ4. exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]]. assert (tvf = vf). @@ -2434,7 +2928,10 @@ Proof. econstructor; eauto. eapply match_Kcall_some with (cenv' := cenv); eauto. red; auto. + eapply type_exprlist_correct; eauto. + (* without return value *) + destruct (list_eq_dec typ_eq x1 (sig_args (Csharpminor.funsig fd))); monadInv EQ3. exploit transl_expr_correct; eauto. intros [tvf [EVAL1 VINJ1]]. assert (tvf = vf). @@ -2450,6 +2947,7 @@ Proof. econstructor; eauto. eapply match_Kcall_none with (cenv' := cenv); eauto. red; auto. + eapply type_exprlist_correct; eauto. (* seq *) monadInv TR. @@ -2531,23 +3029,21 @@ Proof. (* return none *) monadInv TR. left. - exploit match_callstack_freelist; eauto. intros [A B]. + exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]]. econstructor; split. - apply plus_one. apply step_return_0. -(* - rewrite (sig_preserved_body _ _ _ _ TRF). auto. -*) - econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. - eapply match_call_cont; eauto. + apply plus_one. eapply step_return_0. eauto. + econstructor; eauto. eapply match_call_cont; eauto. + simpl; auto. (* return some *) - monadInv TR. left. + monadInv TR. destruct (typ_eq x0 (typ_of_opttyp (fn_return f))); monadInv EQ2. + left. exploit transl_expr_correct; eauto. intros [tv [EVAL VINJ]]. - exploit match_callstack_freelist; eauto. intros [A B]. + exploit match_callstack_freelist; eauto. intros [tm' [A [B C]]]. econstructor; split. - apply plus_one. apply step_return_1. eauto. - econstructor; eauto. rewrite nextblock_freelist. simpl. eauto. - eapply match_call_cont; eauto. + apply plus_one. eapply step_return_1. eauto. eauto. + econstructor; eauto. eapply match_call_cont; eauto. + eapply type_expr_correct; eauto. (* label *) monadInv TR. @@ -2569,8 +3065,11 @@ Proof. destruct (zle sz Int.max_signed); try congruence. intro TRBODY. generalize TRBODY; intro TMP. monadInv TMP. - caseEq (alloc tm 0 sz). intros tm' sp ALLOC'. - exploit function_entry_ok; eauto. + set (tf := mkfunction (Csharpminor.fn_sig f) (fn_params_names f) + (make_vars (fn_params_names f) (fn_vars_names f) (Sseq x1 x0)) + sz (Sseq x1 x0)) in *. + caseEq (Mem.alloc tm 0 (fn_stackspace tf)). intros tm' sp ALLOC'. + exploit function_entry_ok; eauto; simpl; auto. intros [f2 [te2 [tm2 [EXEC [MINJ2 [IINCR MCS2]]]]]]. left; econstructor; split. eapply plus_left. constructor; simpl; eauto. @@ -2583,10 +3082,19 @@ Proof. (* external call *) monadInv TR. - exploit event_match_inject; eauto. intros [A B]. + exploit external_call_mem_inject; eauto. + intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]]. left; econstructor; split. apply plus_one. econstructor; eauto. econstructor; eauto. + apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm). + eapply match_callstack_external_call; eauto. + intros. eapply external_call_bounds; eauto. + omega. omega. + eapply external_call_nextblock_incr; eauto. + eapply external_call_nextblock_incr; eauto. + simpl. change (Val.has_type vres (proj_sig_res (ef_sig ef))). + eapply external_call_well_typed; eauto. (* return *) inv MK; inv H. @@ -2595,26 +3103,29 @@ Proof. apply plus_one. econstructor; eauto. simpl. econstructor; eauto. (* one argument *) - exploit var_set_self_correct; eauto. - intros [te' [tm' [A [B C]]]]. + exploit var_set_self_correct. eauto. eauto. eauto. eauto. eauto. eauto. + instantiate (1 := PTree.set id tv te). apply PTree.gss. + intros; apply PTree.gso; auto. + intros [te' [tm' [A [B [C D]]]]]. left; econstructor; split. eapply plus_left. econstructor. simpl. eapply star_left. econstructor. eapply star_one. eexact A. reflexivity. traceEq. - econstructor; eauto. + econstructor; eauto. Qed. Lemma match_globalenvs_init: - let m := Genv.init_mem prog in - match_globalenvs (meminj_init m). + forall m, + Genv.init_mem prog = Some m -> + match_globalenvs (Mem.flat_inj (Mem.nextblock m)). Proof. intros. constructor. intros. split. - unfold meminj_init. rewrite zlt_true. auto. - unfold m; eapply Genv.find_symbol_not_fresh; eauto. - rewrite <- H. apply symbols_preserved. - intros. unfold meminj_init. rewrite zlt_true. auto. - generalize (nextblock_pos m). omega. + unfold Mem.flat_inj. rewrite zlt_true. auto. + eapply Genv.find_symbol_not_fresh; eauto. + rewrite <- H0. apply symbols_preserved. + intros. unfold Mem.flat_inj. rewrite zlt_true. auto. + generalize (Mem.nextblock_pos m). omega. Qed. Lemma transl_initial_states: @@ -2625,21 +3136,19 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [FIND TR]]. econstructor; split. econstructor. + apply (Genv.init_mem_transf_partial2 _ _ _ TRANSL). eauto. simpl. fold tge. rewrite symbols_preserved. - replace (prog_main tprog) with (prog_main prog). eexact H. + replace (prog_main tprog) with (prog_main prog). eexact H0. symmetry. unfold transl_program in TRANSL. eapply transform_partial_program2_main; eauto. eexact FIND. - rewrite <- H1. apply sig_preserved; auto. - rewrite (Genv.init_mem_transf_partial2 _ _ _ TRANSL). - fold m0. - eapply match_callstate with (f := meminj_init m0) (cs := @nil frame). + rewrite <- H2. apply sig_preserved; auto. + eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame). auto. - apply init_inject. unfold m0. apply Genv.initmem_inject_neutral. - constructor. apply match_globalenvs_init. + eapply Genv.initmem_inject; eauto. + constructor. apply match_globalenvs_init. auto. instantiate (1 := gce). constructor. - red; auto. - constructor. + red; auto. constructor. rewrite H2; simpl; auto. Qed. Lemma transl_final_states: diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index f352df70..bd26b0f9 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -22,7 +22,7 @@ Require Import Integers. Require Import Floats. Require Import Values. Require Import AST. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Csyntax. @@ -294,8 +294,8 @@ Function sem_cmp (c:comparison) match v1,v2 with | Vint n1, Vint n2 => Some (Val.of_bool (Int.cmp c n1 n2)) | Vptr b1 ofs1, Vptr b2 ofs2 => - if valid_pointer m b1 (Int.signed ofs1) - && valid_pointer m b2 (Int.signed ofs2) then + if Mem.valid_pointer m b1 (Int.signed ofs1) + && Mem.valid_pointer m b2 (Int.signed ofs2) then if zeq b1 b2 then Some (Val.of_bool (Int.cmp c ofs1 ofs2)) else sem_cmp_mismatch c @@ -412,15 +412,15 @@ Inductive cast : val -> type -> type -> val -> Prop := maps names of functions and global variables to memory block references, and function pointers to their definitions. (See module [Globalenvs].) *) -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef type. (** The local environment maps local variables to block references. The current value of the variable is stored in the associated memory block. *) -Definition env := PTree.t block. (* map variable -> location *) +Definition env := PTree.t (block * type). (* map variable -> location & type *) -Definition empty_env: env := (PTree.empty block). +Definition empty_env: env := (PTree.empty (block * type)). (** [load_value_of_type ty m b ofs] computes the value of a datum of type [ty] residing in memory [m] at block [b], offset [ofs]. @@ -463,7 +463,7 @@ Inductive alloc_variables: env -> mem -> | alloc_variables_cons: forall e m id ty vars m1 b1 m2 e2, Mem.alloc m 0 (sizeof ty) = (m1, b1) -> - alloc_variables (PTree.set id b1 e) m1 vars e2 m2 -> + alloc_variables (PTree.set id (b1, ty) e) m1 vars e2 m2 -> alloc_variables e m ((id, ty) :: vars) e2 m2. (** Initialization of local variables that are parameters to a function. @@ -479,15 +479,18 @@ Inductive bind_parameters: env -> bind_parameters e m nil nil m | bind_parameters_cons: forall e m id ty params v1 vl b m1 m2, - PTree.get id e = Some b -> + PTree.get id e = Some(b, ty) -> store_value_of_type ty m b Int.zero v1 = Some m1 -> bind_parameters e m1 params vl m2 -> bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. -(** Return the list of blocks in the codomain of [e]. *) +(** Return the list of blocks in the codomain of [e], with low and high bounds. *) -Definition blocks_of_env (e: env) : list block := - List.map (@snd ident block) (PTree.elements e). +Definition block_of_binding (id_b_ty: ident * (block * type)) := + match id_b_ty with (id, (b, ty)) => (b, 0, sizeof ty) end. + +Definition blocks_of_env (e: env) : list (block * Z * Z) := + List.map block_of_binding (PTree.elements e). (** Selection of the appropriate case of a [switch], given the value [n] of the selector expression. *) @@ -586,7 +589,7 @@ Inductive eval_expr: expr -> val -> Prop := with eval_lvalue: expr -> block -> int -> Prop := | eval_Evar_local: forall id l ty, - e!id = Some l -> + e!id = Some(l, ty) -> eval_lvalue (Expr (Evar id) ty) l Int.zero | eval_Evar_global: forall id l ty, e!id = None -> @@ -844,20 +847,23 @@ Inductive step: state -> trace -> state -> Prop := step (State f Sskip (Kfor3 a2 a3 s k) e m) E0 (State f (Sfor Sskip a2 a3 s) k e m) - | step_return_0: forall f k e m, + | step_return_0: forall f k e m m', f.(fn_return) = Tvoid -> + Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn None) k e m) - E0 (Returnstate Vundef (call_cont k) (Mem.free_list m (blocks_of_env e))) - | step_return_1: forall f a k e m v, + E0 (Returnstate Vundef (call_cont k) m') + | step_return_1: forall f a k e m v m', f.(fn_return) <> Tvoid -> eval_expr e m a v -> + Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn (Some a)) k e m) - E0 (Returnstate v (call_cont k) (Mem.free_list m (blocks_of_env e))) - | step_skip_call: forall f k e m, + E0 (Returnstate v (call_cont k) m') + | step_skip_call: forall f k e m m', is_call_cont k -> f.(fn_return) = Tvoid -> + Mem.free_list m (blocks_of_env e) = Some m' -> step (State f Sskip k e m) - E0 (Returnstate Vundef k (Mem.free_list m (blocks_of_env e))) + E0 (Returnstate Vundef k m') | step_switch: forall f a sl k e m n, eval_expr e m a (Vint n) -> @@ -886,10 +892,10 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k e m2) - | step_external_function: forall id targs tres vargs k m vres t, - event_match (external_function id targs tres) vargs t vres -> + | step_external_function: forall id targs tres vargs k m vres t m', + external_call (external_function id targs tres) vargs m t vres m' -> step (Callstate (External id targs tres) vargs k m) - t (Returnstate vres k m) + t (Returnstate vres k m') | step_returnstate_0: forall v f e k m, step (Returnstate v (Kcall None f e k) m) @@ -1084,15 +1090,16 @@ Inductive exec_stmt: env -> mem -> statement -> trace -> mem -> outcome -> Prop by the call. *) with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := - | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres, + | eval_funcall_internal: forall m f vargs t e m1 m2 m3 out vres m4, alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) e m1 -> bind_parameters e m1 f.(fn_params) vargs m2 -> exec_stmt e m2 f.(fn_body) t m3 out -> outcome_result_value out f.(fn_return) vres -> - eval_funcall m (Internal f) vargs t (Mem.free_list m3 (blocks_of_env e)) vres - | eval_funcall_external: forall m id targs tres vargs t vres, - event_match (external_function id targs tres) vargs t vres -> - eval_funcall m (External id targs tres) vargs t m vres. + Mem.free_list m3 (blocks_of_env e) = Some m4 -> + eval_funcall m (Internal f) vargs t m4 vres + | eval_funcall_external: forall m id targs tres vargs t vres m', + external_call (external_function id targs tres) vargs m t vres m' -> + eval_funcall m (External id targs tres) vargs t m' vres. Scheme exec_stmt_ind2 := Minimality for exec_stmt Sort Prop with eval_funcall_ind2 := Minimality for eval_funcall Sort Prop. @@ -1212,9 +1219,9 @@ End SEMANTICS. 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 -> initial_state p (Callstate f nil Kstop m0). @@ -1236,18 +1243,18 @@ Definition exec_program (p: program) (beh: program_behavior) : Prop := (** Big-step execution of a whole program. *) Inductive bigstep_program_terminates (p: program): trace -> int -> Prop := - | bigstep_program_terminates_intro: forall b f m1 t r, + | bigstep_program_terminates_intro: forall b f m0 m1 t 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 -> eval_funcall ge m0 f nil t m1 (Vint r) -> bigstep_program_terminates p t r. Inductive bigstep_program_diverges (p: program): traceinf -> Prop := - | bigstep_program_diverges_intro: forall b f t, + | bigstep_program_diverges_intro: 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 -> evalinf_funcall ge m0 f nil t -> @@ -1525,16 +1532,16 @@ Proof. (* Out_normal *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. - destruct H5. subst vres. apply step_skip_call; auto. + destruct H6. subst vres. apply step_skip_call; auto. (* Out_return None *) assert (fn_return f = Tvoid /\ vres = Vundef). destruct (fn_return f); auto || contradiction. - destruct H6. subst vres. - rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. + destruct H7. subst vres. + rewrite <- (is_call_cont_call_cont k H5). rewrite <- H6. apply step_return_0; auto. (* Out_return Some *) destruct H3. subst vres. - rewrite <- (is_call_cont_call_cont k H4). rewrite <- H5. + rewrite <- (is_call_cont_call_cont k H5). rewrite <- H6. eapply step_return_1; eauto. reflexivity. traceEq. @@ -1697,9 +1704,9 @@ Qed. Theorem bigstep_program_terminates_exec: forall t r, bigstep_program_terminates prog t r -> exec_program prog (Terminates t r). Proof. - intros. inv H. unfold ge0, m0 in *. + intros. inv H. econstructor. - econstructor. eauto. eauto. + econstructor. eauto. eauto. eauto. apply eval_funcall_steps. eauto. red; auto. econstructor. Qed. @@ -1717,7 +1724,7 @@ Proof. eapply evalinf_funcall_forever; eauto. destruct (forever_silent_or_reactive _ _ _ _ _ _ H) as [A | [t [s' [T' [B [C D]]]]]]. - left. econstructor. econstructor. eauto. eauto. auto. + left. econstructor. econstructor; eauto. eauto. right. exists t. split. econstructor. econstructor; eauto. eauto. auto. subst T. rewrite <- (E0_right t) at 1. apply traceinf_prefix_app. constructor. diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 5cdbd84b..2fddc6c2 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.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 Cminor. @@ -89,13 +89,24 @@ Inductive var_kind : Type := | Vscalar: memory_chunk -> var_kind | Varray: Z -> var_kind. -(** Functions are composed of a signature, a list of parameter names +Definition sizeof (lv: var_kind) : Z := + match lv with + | Vscalar chunk => size_chunk chunk + | Varray sz => Zmax 0 sz + end. + +(** Functions are composed of a return type, a list of parameter names with associated memory chunks (parameters must be scalar), a list of local variables with associated [var_kind] description, and a statement representing the function body. *) +Definition param_name (p: ident * memory_chunk) := fst p. +Definition param_chunk (p: ident * memory_chunk) := snd p. +Definition variable_name (v: ident * var_kind) := fst v. +Definition variable_kind (v: ident * var_kind) := snd v. + Record function : Type := mkfunction { - fn_sig: signature; + fn_return: option typ; fn_params: list (ident * memory_chunk); fn_vars: list (ident * var_kind); fn_body: stmt @@ -105,12 +116,25 @@ Definition fundef := AST.fundef function. Definition program : Type := AST.program fundef var_kind. +Definition fn_sig (f: function) := + mksignature (List.map type_of_chunk (List.map param_chunk f.(fn_params))) + f.(fn_return). + Definition funsig (fd: fundef) := match fd with - | Internal f => f.(fn_sig) - | External ef => ef.(ef_sig) + | Internal f => fn_sig f + | External ef => ef_sig ef end. +Definition var_of_param (p: ident * memory_chunk) : ident * var_kind := + (fst p, Vscalar (snd p)). + +Definition fn_variables (f: function) := + List.map var_of_param f.(fn_params) ++ f.(fn_vars). + +Definition fn_params_names (f: function) := List.map param_name f.(fn_params). +Definition fn_vars_names (f: function) := List.map variable_name f.(fn_vars). + (** * Operational semantics *) (** Three kinds of evaluation environments are involved: @@ -120,28 +144,11 @@ Definition funsig (fd: fundef) := to memory blocks and variable informations. *) -Definition genv := Genv.t fundef. +Definition genv := Genv.t fundef var_kind. Definition gvarenv := PTree.t var_kind. Definition env := PTree.t (block * var_kind). Definition empty_env : env := PTree.empty (block * var_kind). -Definition sizeof (lv: var_kind) : Z := - match lv with - | Vscalar chunk => size_chunk chunk - | Varray sz => Zmax 0 sz - end. - -Definition fn_variables (f: function) := - List.map - (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) f.(fn_params) - ++ f.(fn_vars). - -Definition fn_params_names (f: function) := - List.map (@fst ident memory_chunk) f.(fn_params). - -Definition fn_vars_names (f: function) := - List.map (@fst ident var_kind) f.(fn_vars). - (** Continuations *) Inductive cont: Type := @@ -256,8 +263,8 @@ Definition eval_binop (op: binary_operation) (arg1 arg2: val) (m: mem): option val := match op, arg1, arg2 with | Cminor.Ocmp c, Vptr b1 n1, Vptr b2 n2 => - if valid_pointer m b1 (Int.signed n1) - && valid_pointer m b2 (Int.signed n2) + if Mem.valid_pointer m b1 (Int.signed n1) + && Mem.valid_pointer m b2 (Int.signed n2) then Cminor.eval_binop op arg1 arg2 else None | _, _, _ => @@ -279,11 +286,13 @@ Inductive alloc_variables: env -> mem -> alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 -> alloc_variables e m ((id, lv) :: vars) e2 m2. -(** List of blocks mentioned in an environment *) +(** List of blocks mentioned in an environment, with low and high bounds *) + +Definition block_of_binding (id_b_lv: ident * (block * var_kind)) := + match id_b_lv with (id, (b, lv)) => (b, 0, sizeof lv) end. -Definition blocks_of_env (e: env) : list block := - List.map (fun id_b_lv => match id_b_lv with (id, (b, lv)) => b end) - (PTree.elements e). +Definition blocks_of_env (e: env) : list (block * Z * Z) := + List.map block_of_binding (PTree.elements e). (** Initialization of local variables that are parameters. The value of the corresponding argument is stored into the memory block @@ -418,11 +427,12 @@ Inductive step: state -> trace -> state -> Prop := | step_skip_block: forall f k e m, step (State f Sskip (Kblock k) e m) E0 (State f Sskip k e m) - | step_skip_call: forall f k e m, + | step_skip_call: forall f k e m m', is_call_cont k -> - f.(fn_sig).(sig_res) = None -> + f.(fn_return) = None -> + Mem.free_list m (blocks_of_env e) = Some m' -> step (State f Sskip k e m) - E0 (Returnstate Vundef k (Mem.free_list m (blocks_of_env e))) + E0 (Returnstate Vundef k m') | step_assign: forall f id a k e m m' v, eval_expr e m a v -> @@ -478,18 +488,17 @@ Inductive step: state -> trace -> state -> Prop := step (State f (Sswitch a cases) k e m) E0 (State f (seq_of_lbl_stmt (select_switch n cases)) k e m) - | step_return_0: forall f k e m, - f.(fn_sig).(sig_res) = None -> + | step_return_0: forall f k e m m', + f.(fn_return) = None -> + Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn None) k e m) - E0 (Returnstate Vundef (call_cont k) - (Mem.free_list m (blocks_of_env e))) - | step_return_1: forall f a k e m v, - f.(fn_sig).(sig_res) <> None -> + E0 (Returnstate Vundef (call_cont k) m') + | step_return_1: forall f a k e m v m', + f.(fn_return) <> None -> eval_expr e m a v -> + Mem.free_list m (blocks_of_env e) = Some m' -> step (State f (Sreturn (Some a)) k e m) - E0 (Returnstate v (call_cont k) - (Mem.free_list m (blocks_of_env e))) - + E0 (Returnstate v (call_cont k) m') | step_label: forall f lbl s k e m, step (State f (Slabel lbl s) k e m) E0 (State f s k e m) @@ -506,10 +515,10 @@ Inductive step: state -> trace -> state -> Prop := step (Callstate (Internal f) vargs k m) E0 (State f f.(fn_body) k e m2) - | 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 e k m m', exec_opt_assign e m optid v m' -> @@ -524,9 +533,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) -> diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index b40b94c7..548c8df8 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -34,11 +34,6 @@ Open Local Scope error_monad_scope. (** * Operations on C types *) -Definition signature_of_function (f: Csyntax.function) : signature := - mksignature - (typlist_of_typelist (type_of_params (Csyntax.fn_params f))) - (opttyp_of_type (Csyntax.fn_return f)). - Definition chunk_of_type (ty: type): res memory_chunk := match access_mode ty with | By_value chunk => OK chunk @@ -615,7 +610,7 @@ Definition transl_function (f: Csyntax.function) : res function := do tparams <- transl_params (Csyntax.fn_params f); do tvars <- transl_vars (Csyntax.fn_vars f); do tbody <- transl_statement 1%nat 0%nat (Csyntax.fn_body f); - OK (mkfunction (signature_of_function f) tparams tvars tbody). + OK (mkfunction (opttyp_of_type (Csyntax.fn_return f)) tparams tvars tbody). Definition transl_fundef (f: Csyntax.fundef) : res fundef := match f with diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index 86ecd2a4..ebc188e8 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -20,7 +20,7 @@ Require Import Floats. Require Import AST. Require Import Values. Require Import Events. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Csyntax. Require Import Csem. @@ -31,6 +31,29 @@ Require Import Cshmgen. (** * Properties of operations over types *) +Remark type_of_chunk_of_type: + forall ty chunk, + chunk_of_type ty = OK chunk -> + type_of_chunk chunk = typ_of_type ty. +Proof. + intros. unfold chunk_of_type in H. destruct ty; simpl in H; try monadInv H. + destruct i; destruct s; monadInv H; reflexivity. + destruct f; monadInv H; reflexivity. + reflexivity. reflexivity. +Qed. + +Remark transl_params_types: + forall p tp, + transl_params p = OK tp -> + map type_of_chunk (map param_chunk tp) = typlist_of_typelist (type_of_params p). +Proof. + induction p; simpl; intros. + inv H. auto. + destruct a as [id ty]. generalize H; clear H. case_eq (chunk_of_type ty); intros. + monadInv H0. simpl. f_equal; auto. apply type_of_chunk_of_type; auto. + inv H0. +Qed. + Lemma transl_fundef_sig1: forall f tf args res, transl_fundef f = OK tf -> @@ -39,9 +62,10 @@ Lemma transl_fundef_sig1: Proof. intros. destruct f; monadInv H. monadInv EQ. simpl. - simpl in H0. inversion H0. reflexivity. - simpl. - simpl in H0. congruence. + simpl in H0. inversion H0. + unfold fn_sig; simpl. unfold signature_of_type. f_equal. + apply transl_params_types; auto. + simpl. simpl in H0. congruence. Qed. Lemma transl_fundef_sig2: @@ -109,7 +133,7 @@ Qed. Lemma transl_params_names: forall vars tvars, transl_params vars = OK tvars -> - List.map (@fst ident memory_chunk) tvars = Ctyping.var_names vars. + List.map param_name tvars = Ctyping.var_names vars. Proof. exact (map_partial_names _ _ chunk_of_type). Qed. @@ -117,7 +141,7 @@ Qed. Lemma transl_vars_names: forall vars tvars, transl_vars vars = OK tvars -> - List.map (@fst ident var_kind) tvars = Ctyping.var_names vars. + List.map variable_name tvars = Ctyping.var_names vars. Proof. exact (map_partial_names _ _ var_kind_of_type). Qed. diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index 199192c1..769aee7f 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -20,7 +20,7 @@ Require Import Floats. Require Import AST. Require Import Values. Require Import Events. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Csyntax. Require Import Csem. diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 836f1e4b..7e3658b5 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -20,7 +20,7 @@ Require Import Floats. Require Import AST. Require Import Values. Require Import Events. -Require Import Mem. +Require Import Memory. Require Import Globalenvs. Require Import Smallstep. Require Import Csyntax. @@ -52,13 +52,13 @@ Lemma functions_translated: forall v f, Genv.find_funct ge v = Some f -> exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf. -Proof (Genv.find_funct_transf_partial2 transl_fundef transl_globvar TRANSL). +Proof (Genv.find_funct_transf_partial2 transl_fundef transl_globvar _ TRANSL). Lemma function_ptr_translated: forall b f, Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf. -Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar TRANSL). +Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar _ TRANSL). Lemma functions_well_typed: forall v f, @@ -82,41 +82,24 @@ Proof. assumption. Qed. -Lemma sig_translated: - forall fd tfd targs tres, - classify_fun (type_of_fundef fd) = fun_case_f targs tres -> - transl_fundef fd = OK tfd -> - funsig tfd = signature_of_type targs tres. -Proof. - intros. destruct fd; monadInv H0; inv H. - monadInv EQ. simpl. auto. - simpl. auto. -Qed. - (** * Matching between environments *) (** In this section, we define a matching relation between a Clight local environment and a Csharpminor local environment, parameterized by an assignment of types to the Clight variables. *) -Definition match_var_kind (ty: type) (vk: var_kind) : Prop := - match access_mode ty with - | By_value chunk => vk = Vscalar chunk - | _ => True - end. - Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop := mk_match_env { me_local: - forall id b, - e!id = Some b -> - exists vk, exists ty, + forall id b ty, + e!id = Some (b, ty) -> + exists vk, tyenv!id = Some ty - /\ match_var_kind ty vk + /\ var_kind_of_type ty = OK vk /\ te!id = Some (b, vk); me_local_inv: forall id b vk, - te!id = Some (b, vk) -> e!id = Some b; + te!id = Some (b, vk) -> exists ty, e!id = Some(b, ty); me_global: forall id ty, e!id = None -> tyenv!id = Some ty -> @@ -124,64 +107,44 @@ Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop := (forall chunk, access_mode ty = By_value chunk -> (global_var_env tprog)!id = Some (Vscalar chunk)) }. - Lemma match_env_same_blocks: forall tyenv e te, match_env tyenv e te -> - forall b, In b (Csem.blocks_of_env e) <-> In b (blocks_of_env te). -Proof. - intros. inv H. - unfold Csem.blocks_of_env, blocks_of_env. - set (f := (fun id_b_lv : positive * (block * var_kind) => - let (_, y) := id_b_lv in let (b0, _) := y in b0)). - split; intros. - exploit list_in_map_inv; eauto. intros [[id b'] [A B]]. - simpl in A; subst b'. - exploit (me_local0 id b). apply PTree.elements_complete; auto. - intros [vk [ty [C [D E]]]]. - change b with (f (id, (b, vk))). - apply List.in_map. apply PTree.elements_correct. auto. - exploit list_in_map_inv; eauto. intros [[id [b' vk]] [A B]]. - simpl in A; subst b'. - exploit (me_local_inv0 id b vk). apply PTree.elements_complete; auto. - intro. - change b with (snd (id, b)). - apply List.in_map. apply PTree.elements_correct. auto. -Qed. - -Remark free_list_charact: - forall l m, - free_list m l = - mkmem (fun b => if In_dec eq_block b l then empty_block 0 0 else m.(blocks) b) - m.(nextblock) - m.(nextblock_pos). + blocks_of_env te = Csem.blocks_of_env e. Proof. - induction l; intros; simpl. - destruct m; simpl. decEq. apply extensionality. auto. - rewrite IHl. unfold free; simpl. decEq. apply extensionality; intro b. - unfold update. destruct (eq_block a b). - subst b. apply zeq_true. - rewrite zeq_false; auto. - destruct (In_dec eq_block b l); auto. -Qed. - -Lemma mem_free_list_same: - forall m l1 l2, - (forall b, In b l1 <-> In b l2) -> - free_list m l1 = free_list m l2. -Proof. - intros. repeat rewrite free_list_charact. decEq. apply extensionality; intro b. - destruct (In_dec eq_block b l1); destruct (In_dec eq_block b l2); auto. - rewrite H in i. contradiction. - rewrite <- H in i. contradiction. + intros. + set (R := fun (x: (block * type)) (y: (block * var_kind)) => + match x, y with + | (b1, ty), (b2, vk) => b2 = b1 /\ var_kind_of_type ty = OK vk + end). + assert (list_forall2 + (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y)) + (PTree.elements e) (PTree.elements te)). + apply PTree.elements_canonical_order. + intros id [b ty] GET. exploit me_local; eauto. intros [vk [A [B C]]]. + exists (b, vk); split; auto. red. auto. + intros id [b vk] GET. + exploit me_local_inv; eauto. intros [ty A]. + exploit me_local; eauto. intros [vk' [B [C D]]]. + assert (vk' = vk) by congruence. subst vk'. + exists (b, ty); split; auto. red. auto. + + unfold blocks_of_env, Csem.blocks_of_env. + generalize H0. induction 1. auto. + simpl. f_equal; auto. + unfold block_of_binding, Csem.block_of_binding. + destruct a1 as [id1 [blk1 ty1]]. destruct b1 as [id2 [blk2 vk2]]. + simpl in *. destruct H1 as [A [B C]]. subst blk2 id2. f_equal. + apply sizeof_var_kind_of_type. auto. Qed. Lemma match_env_free_blocks: - forall tyenv e te m, + forall tyenv e te m m', match_env tyenv e te -> - Mem.free_list m (Csem.blocks_of_env e) = Mem.free_list m (blocks_of_env te). + Mem.free_list m (Csem.blocks_of_env e) = Some m' -> + Mem.free_list m (blocks_of_env te) = Some m'. Proof. - intros. apply mem_free_list_same. intros; eapply match_env_same_blocks; eauto. + intros. rewrite (match_env_same_blocks _ _ _ H). auto. Qed. Definition match_globalenv (tyenv: typenv) (gv: gvarenv): Prop := @@ -203,14 +166,6 @@ Proof. intros. red in H. eauto. Qed. -Lemma match_var_kind_of_type: - forall ty vk, var_kind_of_type ty = OK vk -> match_var_kind ty vk. -Proof. - intros; red. - caseEq (access_mode ty); auto. - intros chunk AM. generalize (var_kind_by_value _ _ AM). congruence. -Qed. - (** The following lemmas establish the [match_env] invariant at the beginning of a function invocation, after allocation of local variables and initialization of the parameters. *) @@ -233,17 +188,16 @@ Proof. caseEq (transl_vars vars); simpl; [intros tvrs TVARS | congruence]. intro EQ; inversion EQ; subst tvars; clear EQ. set (te2 := PTree.set id (b1, vk) te1). - assert (match_env (add_var tyenv (id, ty)) (PTree.set id b1 e) te2). + assert (match_env (add_var tyenv (id, ty)) (PTree.set id (b1, ty) e) te2). inversion H1. unfold te2, add_var. constructor. (* me_local *) - intros until b. simpl. repeat rewrite PTree.gsspec. + intros until ty0. simpl. repeat rewrite PTree.gsspec. destruct (peq id0 id); intros. - inv H3. exists vk; exists ty; intuition. - apply match_var_kind_of_type. congruence. + inv H3. exists vk; intuition. auto. (* me_local_inv *) intros until vk0. repeat rewrite PTree.gsspec. - destruct (peq id0 id); intros. congruence. eauto. + destruct (peq id0 id); intros. exists ty; congruence. eauto. (* me_global *) intros until ty0. repeat rewrite PTree.gsspec. simpl. destruct (peq id0 id); intros. discriminate. @@ -276,9 +230,8 @@ Proof. unfold store_value_of_type in H0. rewrite H4 in H0. apply bind_parameters_cons with b m1. assert (tyenv!id = Some ty). apply H2. apply in_eq. - destruct (me_local _ _ _ H3 _ _ H) as [vk [ty' [A [B C]]]]. - assert (ty' = ty) by congruence. subst ty'. - red in B; rewrite H4 in B. congruence. + destruct (me_local _ _ _ H3 _ _ _ H) as [vk [A [B C]]]. + exploit var_kind_by_value; eauto. congruence. assumption. apply IHbind_parameters with tyenv; auto. intros. apply H2. apply in_cons; auto. @@ -422,9 +375,9 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. - assert (ty' = ty) by congruence. subst ty'. - red in B; rewrite ACC in B. + exploit me_local; eauto. intros [vk [A [B C]]]. + assert (vk = Vscalar chunk). + exploit var_kind_by_value; eauto. congruence. subst vk. eapply eval_Evar. eapply eval_var_ref_local. eauto. assumption. @@ -440,7 +393,7 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. + exploit me_local; eauto. intros [vk [A [B C]]]. eapply eval_Eaddrof. eapply eval_var_addr_local. eauto. (* global variable *) @@ -473,9 +426,10 @@ Proof. inversion H2; clear H2; subst. inversion H; subst; clear H. (* local variable *) - exploit me_local; eauto. intros [vk [ty' [A [B C]]]]. - assert (ty' = ty) by congruence. subst ty'. - red in B; rewrite ACC in B; subst vk. + exploit me_local; eauto. intros [vk [A [B C]]]. + assert (vk = Vscalar chunk). + exploit var_kind_by_value; eauto. congruence. + subst vk. eapply step_assign. eauto. econstructor. eapply eval_var_ref_local. eauto. assumption. (* global variable *) @@ -514,10 +468,11 @@ Proof. (* local variable *) split. auto. subst id0 ty l ofs. exploit me_local; eauto. - intros [vk [ty [A [B C]]]]. - assert (ty = typeof lhs) by congruence. rewrite <- H3. - generalize B; unfold match_var_kind. destruct (access_mode ty); auto. - intros. subst vk. apply eval_var_ref_local; auto. + intros [vk [A [B C]]]. + case_eq (access_mode (typeof lhs)); intros; auto. + assert (vk = Vscalar m0). + exploit var_kind_by_value; eauto. congruence. + subst vk. apply eval_var_ref_local; auto. (* global variable *) split. auto. subst id0 ty l ofs. exploit me_global; eauto. intros [A B]. @@ -542,7 +497,6 @@ Proof. constructor. econstructor. eauto. auto. Qed. - (** * Proof of semantic preservation *) (** ** Semantic preservation for expressions *) @@ -794,12 +748,12 @@ Qed. Lemma transl_Evar_local_correct: forall (id : ident) (l : block) (ty : type), - e ! id = Some l -> + e ! id = Some(l, ty) -> eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero. Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. exploit (me_local _ _ _ MENV); eauto. - intros [vk [ty' [A [B C]]]]. + intros [vk [A [B C]]]. econstructor. eapply eval_var_addr_local. eauto. Qed. @@ -1296,7 +1250,7 @@ Proof. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_exprlist_correct; eauto. - eapply sig_translated; eauto. congruence. + eapply transl_fundef_sig1; eauto. congruence. econstructor; eauto. eapply functions_well_typed; eauto. econstructor; eauto. simpl. auto. @@ -1310,7 +1264,7 @@ Proof. apply plus_one. econstructor; eauto. exploit transl_expr_correct; eauto. exploit transl_exprlist_correct; eauto. - eapply sig_translated; eauto. congruence. + eapply transl_fundef_sig1; eauto. congruence. econstructor; eauto. eapply functions_well_typed; eauto. econstructor; eauto. simpl; auto. @@ -1521,16 +1475,18 @@ Proof. monadInv TR. inv MTR. econstructor; split. apply plus_one. constructor. monadInv TRF. simpl. rewrite H. auto. - rewrite (match_env_free_blocks _ _ _ m MENV). econstructor; eauto. + eapply match_env_free_blocks; eauto. + econstructor; eauto. eapply match_cont_call_cont. eauto. (* return some *) - monadInv TR. inv MTR. inv WT. inv H2. + monadInv TR. inv MTR. inv WT. inv H3. econstructor; split. apply plus_one. constructor. monadInv TRF. simpl. - unfold opttyp_of_type. destruct (fn_return f); congruence. - exploit transl_expr_correct; eauto. - rewrite (match_env_free_blocks _ _ _ m MENV). econstructor; eauto. + unfold opttyp_of_type. destruct (Csyntax.fn_return f); congruence. + exploit transl_expr_correct; eauto. + eapply match_env_free_blocks; eauto. + econstructor; eauto. eapply match_cont_call_cont. eauto. (* skip call *) @@ -1539,7 +1495,8 @@ Proof. econstructor; split. apply plus_one. apply step_skip_call. auto. monadInv TRF. simpl. rewrite H0. auto. - rewrite (match_env_free_blocks _ _ _ m MENV). constructor. eauto. + eapply match_env_free_blocks; eauto. + constructor. eauto. (* switch *) monadInv TR. inv WT. @@ -1627,7 +1584,7 @@ Proof. exploit function_ptr_translated; eauto. intros [tf [A B]]. assert (C: Genv.find_symbol tge (prog_main tprog) = Some b). rewrite symbols_preserved. replace (prog_main tprog) with (prog_main prog). - exact H1. symmetry. unfold transl_program in TRANSL. + exact H2. symmetry. unfold transl_program in TRANSL. eapply transform_partial_program2_main; eauto. exploit function_ptr_well_typed. eauto. intro WTF. assert (exists targs, type_of_fundef f = Tfunction targs (Tint I32 Signed)). @@ -1635,16 +1592,15 @@ Proof. eapply Genv.find_funct_ptr_symbol_inversion; eauto. destruct H as [targs D]. assert (targs = Tnil). - inv H0. inv H9. simpl in D. unfold type_of_function in D. rewrite <- H4 in D. + inv H0. inv H10. simpl in D. unfold type_of_function in D. rewrite <- H5 in D. simpl in D. congruence. - simpl in D. inv D. inv H8. inv H. - destruct targs; simpl in H5; congruence. + simpl in D. inv D. + exploit external_call_arity; eauto. destruct targs; simpl; congruence. subst targs. assert (funsig tf = signature_of_type Tnil (Tint I32 Signed)). - eapply sig_translated; eauto. rewrite D; auto. + eapply transl_fundef_sig2; eauto. econstructor; split. - econstructor; eauto. - rewrite (@Genv.init_mem_transf_partial2 _ _ _ _ transl_fundef transl_globvar prog tprog TRANSL). + econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto. constructor; auto. constructor. exact I. Qed. -- cgit