From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Cminorgen.v | 221 ++++++--------- cfrontend/Cminorgenproof.v | 694 +++++++++++++++++++++------------------------ cfrontend/Csem.v | 3 +- cfrontend/Csharpminor.v | 150 +++------- cfrontend/Cshmgen.v | 276 +++++++++--------- cfrontend/Cshmgenproof1.v | 134 ++++----- cfrontend/Cshmgenproof2.v | 103 +++---- cfrontend/Cshmgenproof3.v | 179 ++++++------ cfrontend/Csyntax.v | 11 +- 9 files changed, 755 insertions(+), 1016 deletions(-) (limited to 'cfrontend') diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v index a3afae2..23faf78 100644 --- a/cfrontend/Cminorgen.v +++ b/cfrontend/Cminorgen.v @@ -3,6 +3,7 @@ Require Import FSets. Require FSetAVL. Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import Ordered. Require Import AST. @@ -11,7 +12,9 @@ Require Mem. Require Import Csharpminor. Require Import Op. Require Import Cminor. -Require Cmconstr. + +Open Local Scope string_scope. +Open Local Scope error_monad_scope. (** The main task in translating Csharpminor to Cminor is to explicitly stack-allocate local variables whose address is taken: these local @@ -35,57 +38,12 @@ Require Cmconstr. the ``normalize at assignment-time'' semantics of Csharpminor. *) -(** Translation of operators. *) +(** Translation of constants. *) -Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr := - match el with - | Enil => - match op with - | Csharpminor.Ointconst n => Some(Eop (Ointconst n) Enil) - | Csharpminor.Ofloatconst n => Some(Eop (Ofloatconst n) Enil) - | _ => None - end - | Econs e1 Enil => - match op with - | Csharpminor.Ocast8unsigned => Some(Cmconstr.cast8unsigned e1) - | Csharpminor.Ocast8signed => Some(Cmconstr.cast8signed e1) - | Csharpminor.Ocast16unsigned => Some(Cmconstr.cast16unsigned e1) - | Csharpminor.Ocast16signed => Some(Cmconstr.cast16signed e1) - | Csharpminor.Onotint => Some(Cmconstr.notint e1) - | Csharpminor.Onotbool => Some(Cmconstr.notbool e1) - | Csharpminor.Onegf => Some(Cmconstr.negfloat e1) - | Csharpminor.Oabsf => Some(Cmconstr.absfloat e1) - | Csharpminor.Osingleoffloat => Some(Cmconstr.singleoffloat e1) - | Csharpminor.Ointoffloat => Some(Cmconstr.intoffloat e1) - | Csharpminor.Ofloatofint => Some(Cmconstr.floatofint e1) - | Csharpminor.Ofloatofintu => Some(Cmconstr.floatofintu e1) - | _ => None - end - | Econs e1 (Econs e2 Enil) => - match op with - | Csharpminor.Oadd => Some(Cmconstr.add e1 e2) - | Csharpminor.Osub => Some(Cmconstr.sub e1 e2) - | Csharpminor.Omul => Some(Cmconstr.mul e1 e2) - | Csharpminor.Odiv => Some(Cmconstr.divs e1 e2) - | Csharpminor.Odivu => Some(Cmconstr.divu e1 e2) - | Csharpminor.Omod => Some(Cmconstr.mods e1 e2) - | Csharpminor.Omodu => Some(Cmconstr.modu e1 e2) - | Csharpminor.Oand => Some(Cmconstr.and e1 e2) - | Csharpminor.Oor => Some(Cmconstr.or e1 e2) - | Csharpminor.Oxor => Some(Cmconstr.xor e1 e2) - | Csharpminor.Oshl => Some(Cmconstr.shl e1 e2) - | Csharpminor.Oshr => Some(Cmconstr.shr e1 e2) - | Csharpminor.Oshru => Some(Cmconstr.shru e1 e2) - | Csharpminor.Oaddf => Some(Cmconstr.addf e1 e2) - | Csharpminor.Osubf => Some(Cmconstr.subf e1 e2) - | Csharpminor.Omulf => Some(Cmconstr.mulf e1 e2) - | Csharpminor.Odivf => Some(Cmconstr.divf e1 e2) - | Csharpminor.Ocmp c => Some(Cmconstr.cmp c e1 e2) - | Csharpminor.Ocmpu c => Some(Cmconstr.cmpu c e1 e2) - | Csharpminor.Ocmpf c => Some(Cmconstr.cmpf c e1 e2) - | _ => None - end - | _ => None +Definition transl_constant (cst: Csharpminor.constant): constant := + match cst with + | Csharpminor.Ointconst n => Ointconst n + | Csharpminor.Ofloatconst n => Ofloatconst n end. (** [make_cast chunk e] returns a Cminor expression that normalizes @@ -95,45 +53,38 @@ Definition make_op (op: Csharpminor.operation) (el: exprlist): option expr := Definition make_cast (chunk: memory_chunk) (e: expr): expr := match chunk with - | Mint8signed => Cmconstr.cast8signed e - | Mint8unsigned => Cmconstr.cast8unsigned e - | Mint16signed => Cmconstr.cast16signed e - | Mint16unsigned => Cmconstr.cast16unsigned e + | Mint8signed => Eunop Ocast8signed e + | Mint8unsigned => Eunop Ocast8unsigned e + | Mint16signed => Eunop Ocast16signed e + | Mint16unsigned => Eunop Ocast16unsigned e | Mint32 => e - | Mfloat32 => Cmconstr.singleoffloat e + | Mfloat32 => Eunop Osingleoffloat e | Mfloat64 => e end. -Definition make_load (chunk: memory_chunk) (e: expr): expr := - Cmconstr.load chunk e. - Definition store_arg (chunk: memory_chunk) (e: expr) : expr := match e with - | Eop op (Econs e1 Enil) => - match op with - | Ocast8signed => - match chunk with Mint8signed => e1 | _ => e end - | Ocast8unsigned => - match chunk with Mint8unsigned => e1 | _ => e end - | Ocast16signed => - match chunk with Mint16signed => e1 | _ => e end - | Ocast16unsigned => - match chunk with Mint16unsigned => e1 | _ => e end - | Osingleoffloat => - match chunk with Mfloat32 => e1 | _ => e end - | _ => e - end + | Eunop Ocast8signed e1 => + match chunk with Mint8signed => e1 | _ => e end + | Eunop Ocast8unsigned e1 => + match chunk with Mint8unsigned => e1 | _ => e end + | Eunop Ocast16signed e1 => + match chunk with Mint16signed => e1 | _ => e end + | Eunop Ocast16unsigned e1 => + match chunk with Mint16unsigned => e1 | _ => e end + | Eunop Osingleoffloat e1 => + match chunk with Mfloat32 => e1 | _ => e end | _ => e end. Definition make_store (chunk: memory_chunk) (e1 e2: expr): stmt := - Sexpr(Cmconstr.store chunk e1 (store_arg chunk e2)). + Sexpr (Estore chunk e1 (store_arg chunk e2)). Definition make_stackaddr (ofs: Z): expr := - Eop (Oaddrstack (Int.repr ofs)) Enil. + Econst (Oaddrstack (Int.repr ofs)). Definition make_globaladdr (id: ident): expr := - Eop (Oaddrsymbol id Int.zero) Enil. + Econst (Oaddrsymbol id Int.zero). (** Compile-time information attached to each Csharpminor variable: global variables, local variables, function parameters. @@ -156,134 +107,127 @@ Definition compilenv := PMap.t var_info. (** Generation of Cminor code corresponding to accesses to Csharpminor local variables: reads, assignments, and taking the address of. *) -Definition var_get (cenv: compilenv) (id: ident): option expr := +Definition var_get (cenv: compilenv) (id: ident): res expr := match PMap.get id cenv with | Var_local chunk => - Some(Evar id) + OK(Evar id) | Var_stack_scalar chunk ofs => - Some(make_load chunk (make_stackaddr ofs)) + OK(Eload chunk (make_stackaddr ofs)) | Var_global_scalar chunk => - Some(make_load chunk (make_globaladdr id)) + OK(Eload chunk (make_globaladdr id)) | _ => - None + Error(msg "Cminorgen.var_get") end. -Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): option stmt := +Definition var_set (cenv: compilenv) (id: ident) (rhs: expr): res stmt := match PMap.get id cenv with | Var_local chunk => - Some(Sassign id (make_cast chunk rhs)) + OK(Sassign id (make_cast chunk rhs)) | Var_stack_scalar chunk ofs => - Some(make_store chunk (make_stackaddr ofs) rhs) + OK(make_store chunk (make_stackaddr ofs) rhs) | Var_global_scalar chunk => - Some(make_store chunk (make_globaladdr id) rhs) + OK(make_store chunk (make_globaladdr id) rhs) | _ => - None + Error(msg "Cminorgen.var_set") end. -Definition var_addr (cenv: compilenv) (id: ident): option expr := +Definition var_addr (cenv: compilenv) (id: ident): res expr := match PMap.get id cenv with - | Var_local chunk => None - | Var_stack_scalar chunk ofs => Some (make_stackaddr ofs) - | Var_stack_array ofs => Some (make_stackaddr ofs) - | _ => Some (make_globaladdr id) - end. - -(** The translation from Csharpminor to Cminor can fail, which we - encode by returning option types ([None] denotes error). - Propagation of errors is done in monadic style, using the following - [bind] monadic composition operator, and a [do] notation inspired - by Haskell's. *) - -Definition bind (A B: Set) (a: option A) (b: A -> option B): option B := - match a with - | None => None - | Some x => b x + | 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. -Notation "'do' X <- A ; B" := (bind _ _ A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). - (** Translation of expressions. All the hard work is done by the [make_*] and [var_*] functions defined above. *) Fixpoint transl_expr (cenv: compilenv) (e: Csharpminor.expr) - {struct e}: option expr := + {struct e}: res expr := match e with | Csharpminor.Evar id => var_get cenv id | Csharpminor.Eaddrof id => var_addr cenv id - | Csharpminor.Eop op el => - do tel <- transl_exprlist cenv el; make_op op tel + | Csharpminor.Econst cst => + OK (Econst (transl_constant cst)) + | Csharpminor.Eunop op e1 => + do te1 <- transl_expr cenv e1; + OK (Eunop op te1) + | Csharpminor.Ebinop op e1 e2 => + do te1 <- transl_expr cenv e1; + do te2 <- transl_expr cenv e2; + OK (Ebinop op te1 te2) | Csharpminor.Eload chunk e => - do te <- transl_expr cenv e; Some (make_load chunk te) + do te <- transl_expr cenv e; + OK (Eload chunk te) | Csharpminor.Ecall sig e el => do te <- transl_expr cenv e; do tel <- transl_exprlist cenv el; - Some (Ecall sig te tel) + OK (Ecall sig te tel) | Csharpminor.Econdition e1 e2 e3 => do te1 <- transl_expr cenv e1; do te2 <- transl_expr cenv e2; do te3 <- transl_expr cenv e3; - Some (Cmconstr.conditionalexpr te1 te2 te3) + OK (Econdition te1 te2 te3) | Csharpminor.Elet e1 e2 => do te1 <- transl_expr cenv e1; do te2 <- transl_expr cenv e2; - Some (Elet te1 te2) + OK (Elet te1 te2) | Csharpminor.Eletvar n => - Some (Eletvar n) + OK (Eletvar n) | Csharpminor.Ealloc e => do te <- transl_expr cenv e; - Some (Ealloc te) + OK (Ealloc te) end with transl_exprlist (cenv: compilenv) (el: Csharpminor.exprlist) - {struct el}: option exprlist := + {struct el}: res exprlist := match el with | Csharpminor.Enil => - Some Enil + OK Enil | Csharpminor.Econs e1 e2 => do te1 <- transl_expr cenv e1; do te2 <- transl_exprlist cenv e2; - Some (Econs te1 te2) + OK (Econs te1 te2) end. (** Translation of statements. Entirely straightforward. *) Fixpoint transl_stmt (cenv: compilenv) (s: Csharpminor.stmt) - {struct s}: option stmt := + {struct s}: res stmt := match s with | Csharpminor.Sskip => - Some Sskip + OK Sskip | Csharpminor.Sexpr e => - do te <- transl_expr cenv e; Some(Sexpr te) + do te <- transl_expr cenv e; OK(Sexpr te) | Csharpminor.Sassign id e => do te <- transl_expr cenv e; var_set cenv id te | Csharpminor.Sstore chunk e1 e2 => do te1 <- transl_expr cenv e1; do te2 <- transl_expr cenv e2; - Some (make_store chunk te1 te2) + OK (make_store chunk te1 te2) | Csharpminor.Sseq s1 s2 => do ts1 <- transl_stmt cenv s1; do ts2 <- transl_stmt cenv s2; - Some (Sseq ts1 ts2) + OK (Sseq ts1 ts2) | Csharpminor.Sifthenelse e s1 s2 => do te <- transl_expr cenv e; do ts1 <- transl_stmt cenv s1; do ts2 <- transl_stmt cenv s2; - Some (Cmconstr.ifthenelse te ts1 ts2) + OK (Sifthenelse te ts1 ts2) | Csharpminor.Sloop s => do ts <- transl_stmt cenv s; - Some (Sloop ts) + OK (Sloop ts) | Csharpminor.Sblock s => do ts <- transl_stmt cenv s; - Some (Sblock ts) + OK (Sblock ts) | Csharpminor.Sexit n => - Some (Sexit n) + OK (Sexit n) | Csharpminor.Sswitch e cases default => - do te <- transl_expr cenv e; Some(Sswitch te cases default) + do te <- transl_expr cenv e; OK(Sswitch te cases default) | Csharpminor.Sreturn None => - Some (Sreturn None) + OK (Sreturn None) | Csharpminor.Sreturn (Some e) => - do te <- transl_expr cenv e; Some (Sreturn (Some te)) + do te <- transl_expr cenv e; OK (Sreturn (Some te)) end. (** Computation of the set of variables whose address is taken in @@ -295,7 +239,10 @@ Fixpoint addr_taken_expr (e: Csharpminor.expr): Identset.t := match e with | Csharpminor.Evar id => Identset.empty | Csharpminor.Eaddrof id => Identset.add id Identset.empty - | Csharpminor.Eop op el => addr_taken_exprlist el + | Csharpminor.Econst cst => Identset.empty + | Csharpminor.Eunop op e1 => addr_taken_expr e1 + | Csharpminor.Ebinop op e1 e2 => + Identset.union (addr_taken_expr e1) (addr_taken_expr e2) | Csharpminor.Eload chunk e => addr_taken_expr e | Csharpminor.Ecall sig e el => Identset.union (addr_taken_expr e) (addr_taken_exprlist el) @@ -416,23 +363,23 @@ Fixpoint store_parameters overflow machine arithmetic and lead to incorrect code. *) Definition transl_function - (gce: compilenv) (f: Csharpminor.function): option function := + (gce: compilenv) (f: Csharpminor.function): res function := let (cenv, stacksize) := build_compilenv gce f in if zle stacksize Int.max_signed then do tbody <- transl_stmt cenv f.(Csharpminor.fn_body); - Some (mkfunction + OK (mkfunction (Csharpminor.fn_sig f) (Csharpminor.fn_params_names f) (Csharpminor.fn_vars_names f) stacksize (Sseq (store_parameters cenv f.(Csharpminor.fn_params)) tbody)) - else None. + else Error(msg "Cminorgen: too many local variables, stack size exceeded"). -Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): option fundef := +Definition transl_fundef (gce: compilenv) (f: Csharpminor.fundef): res fundef := transf_partial_fundef (transl_function gce) f. -Definition transl_globvar (vk: var_kind) := Some tt. +Definition transl_globvar (vk: var_kind) := OK tt. -Definition transl_program (p: Csharpminor.program) : option program := +Definition transl_program (p: Csharpminor.program) : res program := let gce := build_global_compilenv p in transform_partial_program2 (transl_fundef gce) transl_globvar p. diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index ad31ff1..5bcb880 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -2,6 +2,7 @@ Require Import FSets. Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. @@ -11,68 +12,49 @@ Require Import Mem. Require Import Events. Require Import Globalenvs. Require Import Csharpminor. -Require Import Op. Require Import Cminor. -Require Cmconstr. Require Import Cminorgen. -Require Import Cmconstrproof. + +Open Local Scope error_monad_scope. Section TRANSLATION. Variable prog: Csharpminor.program. Variable tprog: program. -Hypothesis TRANSL: transl_program prog = Some tprog. +Hypothesis TRANSL: transl_program prog = OK tprog. Let ge : Csharpminor.genv := Genv.globalenv prog. Let tge: genv := Genv.globalenv tprog. Let gce : compilenv := build_global_compilenv prog. Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intro. unfold ge, tge. - apply Genv.find_symbol_transf_partial2 with (transl_fundef gce) transl_globvar. - exact TRANSL. -Qed. +Proof (Genv.find_symbol_transf_partial2 (transl_fundef gce) transl_globvar _ TRANSL). Lemma function_ptr_translated: forall (b: block) (f: Csharpminor.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, - Genv.find_funct_ptr tge b = Some tf /\ transl_fundef gce f = Some tf. -Proof. - intros. - generalize - (Genv.find_funct_ptr_transf_partial2 (transl_fundef gce) transl_globvar TRANSL H). - case (transl_fundef gce f). - intros tf [A B]. exists tf. tauto. - intros [A B]. elim B. reflexivity. -Qed. + 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). + 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 = Some tf. -Proof. - intros. - generalize - (Genv.find_funct_transf_partial2 (transl_fundef gce) transl_globvar TRANSL H). - case (transl_fundef gce f). - intros tf [A B]. exists tf. tauto. - intros [A B]. elim B. reflexivity. -Qed. + 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). Lemma sig_preserved: forall f tf, - transl_fundef gce f = Some tf -> + transl_fundef gce f = OK tf -> Cminor.funsig tf = Csharpminor.funsig f. Proof. intros until tf; destruct f; simpl. unfold transl_function. destruct (build_compilenv gce f). - case (zle z Int.max_signed); try congruence. - intro. case (transl_stmt c (Csharpminor.fn_body f)); simpl; try congruence. - intros. inversion H. reflexivity. - intro. inversion H; reflexivity. + case (zle z Int.max_signed); simpl; try congruence. + intros. monadInv H. monadInv EQ. reflexivity. + intro. inv H. reflexivity. Qed. Definition global_compilenv_match (ce: compilenv) (gv: gvarenv) : Prop := @@ -510,15 +492,12 @@ Lemma load_from_alloc_is_undef: alloc m1 0 (size_chunk chunk) = (m2, b) -> load chunk m2 b 0 = Some Vundef. Proof. - intros. - assert (valid_block m2 b). eapply valid_new_block; eauto. - assert (low_bound m2 b <= 0). - generalize (low_bound_alloc _ _ b _ _ _ H). rewrite zeq_true. omega. - assert (0 + size_chunk chunk <= high_bound m2 b). - generalize (high_bound_alloc _ _ b _ _ _ H). rewrite zeq_true. omega. - elim (load_in_bounds _ _ _ _ H0 H1 H2). intros v LOAD. - assert (v = Vundef). eapply load_alloc_same; eauto. - congruence. + intros. + assert (exists v, load chunk m2 b 0 = Some v). + apply valid_access_load. + eapply valid_access_alloc_same; eauto; omega. + destruct H0 as [v LOAD]. rewrite LOAD. decEq. + eapply load_alloc_same; eauto. Qed. Lemma match_env_alloc_same: @@ -577,14 +556,20 @@ Proof. contradiction. (* other vars *) generalize (me_vars0 id0); intros. - inversion H6; econstructor; eauto. - unfold e2; rewrite PTree.gso; auto. - unfold f2, extend_inject, eq_block; rewrite zeq_false; auto. - generalize (me_bounded0 _ _ _ H8). unfold block in *; omega. - unfold e2; rewrite PTree.gso; eauto. - unfold e2; rewrite PTree.gso; eauto. - unfold e2; rewrite PTree.gso; eauto. - unfold e2; rewrite PTree.gso; eauto. + inversion H6. + 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 _ _ _ H8). 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 *) @@ -629,9 +614,15 @@ Proof. inversion H2. constructor; auto. (* me_vars *) intros. generalize (me_vars0 id); intro. - inversion H5; econstructor; eauto. - unfold f2, extend_inject, eq_block. rewrite zeq_false. auto. - generalize (me_bounded0 _ _ _ H7). unfold block in *; omega. + 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. @@ -726,9 +717,10 @@ Proof. (* me_vars *) intros. generalize (me_vars0 id); intro. inversion H5. (* var_local *) - econstructor; eauto. + eapply match_var_local with (v := v); eauto. + eapply load_alloc_other; eauto. generalize (me_bounded0 _ _ _ H7). intro. - unfold f2, extend_inject. case (eq_block b0 b); intro. + unfold f2, extend_inject. case (zeq b0 b); intro. subst b0. rewrite BEQ in H12. omegaContradiction. auto. (* var_stack_scalar *) @@ -740,12 +732,12 @@ Proof. (* var_global_array *) econstructor; eauto. (* me_bounded *) - intros until delta. unfold f2, extend_inject. case (eq_block b0 b); intro. + 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 (eq_block b0 b); intros. + 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. @@ -804,16 +796,7 @@ Qed. (** * Correctness of Cminor construction functions *) -Hint Resolve eval_negint eval_negfloat eval_absfloat eval_intoffloat - eval_floatofint eval_floatofintu eval_notint eval_notbool - eval_cast8signed eval_cast8unsigned eval_cast16signed - eval_cast16unsigned eval_singleoffloat eval_add eval_add_ptr - eval_add_ptr_2 eval_sub eval_sub_ptr_int eval_sub_ptr_ptr - eval_mul eval_divs eval_mods eval_divu eval_modu - eval_and eval_or eval_xor eval_shl eval_shr eval_shru - eval_addf eval_subf eval_mulf eval_divf - eval_cmp eval_cmp_null_r eval_cmp_null_l eval_cmp_ptr - eval_cmpu eval_cmpf: evalexpr. +Hint Resolve eval_Econst eval_Eunop eval_Ebinop eval_Eload: evalexpr. Remark val_inject_val_of_bool: forall f b, val_inject f (Val.of_bool b) (Val.of_bool b). @@ -821,151 +804,146 @@ Proof. intros; destruct b; unfold Val.of_bool, Vtrue, Vfalse; constructor. Qed. +Remark val_inject_bool_of_val: + forall f v b tv, + val_inject f v tv -> Val.bool_of_val v b -> Val.bool_of_val tv b. +Proof. + intros. inv H; inv H0; constructor; auto. +Qed. + +Remark val_inject_eval_compare_null: + forall f c i v, + eval_compare_null c i = Some v -> + val_inject f v v. +Proof. + unfold eval_compare_null; intros. + destruct (Int.eq i Int.zero). + destruct c; inv H; unfold Vfalse, Vtrue; constructor. + discriminate. +Qed. + Ltac TrivialOp := match goal with - | [ |- exists x, _ /\ val_inject _ (Vint ?x) _ ] => + | [ |- exists y, _ /\ val_inject _ (Vint ?x) _ ] => exists (Vint x); split; [eauto with evalexpr | constructor] - | [ |- exists x, _ /\ val_inject _ (Vfloat ?x) _ ] => + | [ |- exists y, _ /\ val_inject _ (Vfloat ?x) _ ] => exists (Vfloat x); split; [eauto with evalexpr | constructor] - | [ |- exists x, _ /\ val_inject _ (Val.of_bool ?x) _ ] => + | [ |- exists y, _ /\ val_inject _ (Val.of_bool ?x) _ ] => exists (Val.of_bool x); split; [eauto with evalexpr | apply val_inject_val_of_bool] + | [ |- exists y, Some ?x = Some y /\ val_inject _ _ _ ] => + exists x; split; [auto | econstructor; eauto] | _ => idtac end. -Remark eval_compare_null_inv: - forall c i v, - Csharpminor.eval_compare_null c i = Some v -> - i = Int.zero /\ (c = Ceq /\ v = Vfalse \/ c = Cne /\ v = Vtrue). +(** Correctness of [transl_constant]. *) + +Lemma transl_constant_correct: + forall f sp cst v, + Csharpminor.eval_constant cst = Some v -> + exists tv, + eval_constant tge sp (transl_constant cst) = Some tv + /\ val_inject f v tv. Proof. - intros until v. unfold Csharpminor.eval_compare_null. - predSpec Int.eq Int.eq_spec i Int.zero. - case c; intro EQ; simplify_eq EQ; intro; subst v; tauto. - congruence. + destruct cst; simpl; intros; inv H; TrivialOp. Qed. -(** Correctness of [make_op]. The generated Cminor code evaluates - to a value that matches the result value of the Csharpminor operation, - provided arguments match pairwise ([val_list_inject f] hypothesis). *) +(** Compatibility of [eval_unop] with respect to [val_inject]. *) -Lemma make_op_correct: - forall al a op vl m2 v sp le te tm1 t tm2 tvl f, - make_op op al = Some a -> - Csharpminor.eval_operation op vl m2 = Some v -> - eval_exprlist tge (Vptr sp Int.zero) le te tm1 al t tm2 tvl -> - val_list_inject f vl tvl -> - mem_inject f m2 tm2 -> +Lemma eval_unop_compat: + forall f op v1 tv1 v, + eval_unop op v1 = Some v -> + val_inject f v1 tv1 -> exists tv, - eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 tv + eval_unop op tv1 = Some tv /\ val_inject f v tv. Proof. - intros. - destruct al as [ | a1 al]; - [idtac | destruct al as [ | a2 al]; - [idtac | destruct al as [ | a3 al]]]; - simpl in H; try discriminate. - (* Constant operators *) - inversion H1. subst sp0 le0 e m tm1 tvl. - inversion H2. subst vl. - destruct op; simplify_eq H; intro; subst a; - simpl in H0; injection H0; intro; subst v. - (* intconst *) - TrivialOp. econstructor. constructor. reflexivity. - (* floatconst *) - TrivialOp. econstructor. constructor. reflexivity. - (* Unary operators *) - inversion H1; clear H1; subst. - inversion H11; clear H11; subst. - rewrite E0_right. - inversion H2; clear H2; subst. inversion H8; clear H8; subst. - destruct op; simplify_eq H; intro; subst a; - simpl in H0; destruct v1; simplify_eq H0; intro; subst v; - inversion H7; subst v0; - TrivialOp. - change (Vint (Int.cast8unsigned i)) with (Val.cast8unsigned (Vint i)). eauto with evalexpr. - change (Vint (Int.cast8signed i)) with (Val.cast8signed (Vint i)). eauto with evalexpr. - change (Vint (Int.cast16unsigned i)) with (Val.cast16unsigned (Vint i)). eauto with evalexpr. - change (Vint (Int.cast16signed i)) with (Val.cast16signed (Vint i)). eauto with evalexpr. - replace (Int.eq i Int.zero) with (negb (negb (Int.eq i Int.zero))). - eapply eval_notbool. eauto. - generalize (Int.eq_spec i Int.zero). destruct (Int.eq i Int.zero); intro; simpl. - rewrite H1; constructor. constructor; auto. - apply negb_elim. - unfold Vfalse; TrivialOp. change (Vint Int.zero) with (Val.of_bool (negb true)). - eapply eval_notbool. eauto. constructor. - change (Vfloat (Float.singleoffloat f0)) with (Val.singleoffloat (Vfloat f0)). eauto with evalexpr. - (* Binary operations *) - inversion H1; clear H1; subst. inversion H11; clear H11; subst. - inversion H12; clear H12; subst. rewrite E0_right. - inversion H2; clear H2; subst. inversion H9; clear H9; subst. - inversion H10; clear H10; subst. - destruct op; simplify_eq H; intro; subst a; - simpl in H0; destruct v2; destruct v3; simplify_eq H0; intro; try subst v; - inversion H7; inversion H8; subst v0; subst v1; - TrivialOp. - (* add int ptr *) - exists (Vptr b2 (Int.add ofs2 i)); split. - eauto with evalexpr. apply val_inject_ptr with x. auto. - subst ofs2. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - (* add ptr int *) - exists (Vptr b2 (Int.add ofs2 i0)); split. - eauto with evalexpr. apply val_inject_ptr with x. auto. - subst ofs2. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - (* sub ptr int *) - exists (Vptr b2 (Int.sub ofs2 i0)); split. - eauto with evalexpr. apply val_inject_ptr with x. auto. - subst ofs2. apply Int.sub_add_l. - (* sub ptr ptr *) - destruct (eq_block b b0); simplify_eq H0; intro; subst v; subst b0. - assert (b4 = b2). congruence. subst b4. - exists (Vint (Int.sub ofs3 ofs2)); split. - eauto with evalexpr. - subst ofs2 ofs3. replace x0 with x. rewrite Int.sub_shifted. constructor. - congruence. - (* divs *) - generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; - simplify_eq H0; intro; subst v. TrivialOp. - (* divu *) - generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; - simplify_eq H0; intro; subst v. TrivialOp. - (* mods *) - generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; - simplify_eq H0; intro; subst v. TrivialOp. - (* modu *) - generalize (Int.eq_spec i0 Int.zero); destruct (Int.eq i0 Int.zero); intro; - simplify_eq H0; intro; subst v. TrivialOp. - (* shl *) - caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; - simplify_eq H0; intro; subst v. TrivialOp. - (* shr *) - caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; - simplify_eq H0; intro; subst v. TrivialOp. - (* shru *) - caseEq (Int.ltu i0 (Int.repr 32)); intro EQ; rewrite EQ in H0; - simplify_eq H0; intro; subst v. TrivialOp. - (* cmp int ptr *) - elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i. - exists v; split. eauto with evalexpr. - elim H12; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor. - (* cmp ptr int *) - elim (eval_compare_null_inv _ _ _ H0); intros; subst i1 i0. - exists v; split. eauto with evalexpr. - elim H12; intros [A B]; subst v; unfold Vtrue, Vfalse; constructor. + destruct op; simpl; intros. + inv H; inv H0; simpl; TrivialOp. + inv H; inv H0; simpl; TrivialOp. + inv H; inv H0; simpl; TrivialOp. + inv H; inv H0; simpl; TrivialOp. + inv H0; inv H. TrivialOp. + inv H0; inv H. TrivialOp. unfold Vfalse; TrivialOp. + inv H0; inv H; TrivialOp. + inv H0; inv H; TrivialOp. + inv H0; inv H; TrivialOp. + inv H; inv H0; simpl; TrivialOp. + inv H0; inv H; TrivialOp. + inv H0; inv H; TrivialOp. + inv H0; inv H; TrivialOp. +Qed. + +(** Compatibility of [eval_binop] with respect to [val_inject]. *) + +Lemma eval_binop_compat: + forall f op v1 tv1 v2 tv2 v m tm, + eval_binop op v1 v2 m = Some v -> + val_inject f v1 tv1 -> + val_inject f v2 tv2 -> + mem_inject f m tm -> + exists tv, + eval_binop op tv1 tv2 tm = Some tv + /\ val_inject f v tv. +Proof. + destruct op; simpl; intros. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + apply Int.sub_add_l. + 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. + 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. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + destruct (Int.eq i0 Int.zero); inv H1. TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + destruct (Int.eq i0 Int.zero); inv H1. TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + destruct (Int.eq i0 Int.zero); inv H1. TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + destruct (Int.ltu i0 (Int.repr 32)); inv H1. TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. + 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 m2 b (Int.signed i) && valid_pointer m2 b0 (Int.signed i0)); - intro EQ; rewrite EQ in H0; try discriminate. - destruct (eq_block b b0); simplify_eq H0; intro; subst v b0. - assert (b4 = b2); [congruence|subst b4]. - assert (x0 = x); [congruence|subst x0]. + caseEq (valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b0 (Int.signed ofs0)); + intro EQ; rewrite EQ in H4; try discriminate. + destruct (eq_block b1 b0); inv H4. + assert (b3 = b2) by congruence. subst b3. + assert (x0 = x) by congruence. subst x0. elim (andb_prop _ _ EQ); intros. - exists (Val.of_bool (Int.cmp c ofs3 ofs2)); split. - eauto with evalexpr. - subst ofs2 ofs3. rewrite Int.translate_cmp. - apply val_inject_val_of_bool. + exists (Val.of_bool (Int.cmp c ofs1 ofs0)); split. + exploit (Mem.valid_pointer_inject f m tm b0 ofs0); eauto. + intro VP; rewrite VP; clear VP. + exploit (Mem.valid_pointer_inject f m tm b0 ofs1); eauto. + intro VP; rewrite VP; clear VP. + 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. + apply val_inject_val_of_bool. + (* *) + inv H0; try discriminate; inv H1; inv H; TrivialOp. + inv H0; try discriminate; inv H1; inv H; TrivialOp. Qed. (** Correctness of [make_cast]. Note that the resulting Cminor value is @@ -980,35 +958,28 @@ Lemma make_cast_correct: te tm1 (make_cast chunk a) t tm2 tv' /\ val_inject f (Val.load_result chunk v) tv'. Proof. - intros. destruct chunk. + intros. destruct chunk; simpl make_cast. exists (Val.cast8signed tv). - split. apply eval_cast8signed; auto. - inversion H0; simpl; constructor. + split. eauto with evalexpr. inversion H0; simpl; constructor. exists (Val.cast8unsigned tv). - split. apply eval_cast8unsigned; auto. - inversion H0; simpl; constructor. + split. eauto with evalexpr. inversion H0; simpl; constructor. exists (Val.cast16signed tv). - split. apply eval_cast16signed; auto. - inversion H0; simpl; constructor. + split. eauto with evalexpr. inversion H0; simpl; constructor. exists (Val.cast16unsigned tv). - split. apply eval_cast16unsigned; auto. - inversion H0; simpl; constructor. + split. eauto with evalexpr. inversion H0; simpl; constructor. - exists tv. - split. simpl; auto. - inversion H0; simpl; econstructor; eauto. + exists tv. + split. auto. inversion H0; simpl; econstructor; eauto. exists (Val.singleoffloat tv). - split. apply eval_singleoffloat; auto. - inversion H0; simpl; constructor. + split. eauto with evalexpr. inversion H0; simpl; constructor. - exists tv. - split. simpl; auto. - inversion H0; simpl; constructor. + exists tv. + split. auto. inversion H0; simpl; econstructor; eauto. Qed. Lemma make_stackaddr_correct: @@ -1018,7 +989,7 @@ Lemma make_stackaddr_correct: E0 tm (Vptr sp (Int.repr ofs)). Proof. intros; unfold make_stackaddr. - eapply eval_Eop. econstructor. simpl. decEq. decEq. + econstructor. simpl. decEq. decEq. rewrite Int.add_commut. apply Int.add_zero. Qed. @@ -1030,22 +1001,10 @@ Lemma make_globaladdr_correct: E0 tm (Vptr b Int.zero). Proof. intros; unfold make_globaladdr. - eapply eval_Eop. econstructor. simpl. rewrite H. auto. + econstructor. simpl. rewrite H. auto. Qed. -(** Correctness of [make_load] and [make_store]. *) - -Lemma make_load_correct: - forall sp le te tm1 a t tm2 va chunk v, - eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 va -> - Mem.loadv chunk tm2 va = Some v -> - eval_expr tge (Vptr sp Int.zero) le - te tm1 (make_load chunk a) - t tm2 v. -Proof. - intros; unfold make_load. - eapply eval_load; eauto. -Qed. +(** Correctness of [make_store]. *) Lemma store_arg_content_inject: forall f sp le te tm1 a t tm2 v va chunk, @@ -1053,25 +1012,23 @@ Lemma store_arg_content_inject: val_inject f v va -> exists vb, eval_expr tge (Vptr sp Int.zero) le te tm1 (store_arg chunk a) t tm2 vb - /\ val_content_inject f (mem_chunk chunk) v vb. + /\ val_content_inject f chunk v vb. Proof. intros. assert (exists vb, eval_expr tge (Vptr sp Int.zero) le te tm1 a t tm2 vb - /\ val_content_inject f (mem_chunk chunk) v vb). + /\ val_content_inject f chunk v vb). exists va; split. assumption. constructor. assumption. - inversion H; clear H; subst; simpl; trivial. - inversion H2; clear H2; subst; trivial. - inversion H4; clear H4; subst; trivial. - rewrite E0_right. rewrite E0_right in H1. - destruct op; trivial; destruct chunk; trivial; - exists v0; (split; [auto| - simpl in H3; inversion H3; clear H3; subst va; - destruct v0; simpl in H0; inversion H0; subst; try (constructor; constructor)]). - apply val_content_inject_8. apply Int.cast8_unsigned_signed. - apply val_content_inject_8. apply Int.cast8_unsigned_idem. - apply val_content_inject_16. apply Int.cast16_unsigned_signed. - apply val_content_inject_16. apply Int.cast16_unsigned_idem. + destruct a; simpl store_arg; trivial; + destruct u; trivial; + destruct chunk; trivial; + inv H; simpl in H12; inv H12; + econstructor; (split; [eauto|idtac]); + destruct v1; simpl in H0; inv H0; try (constructor; constructor). + apply val_content_inject_8. auto. apply Int.cast8_unsigned_idem. + apply val_content_inject_8; auto. apply Int.cast8_unsigned_signed. + apply val_content_inject_16; auto. apply Int.cast16_unsigned_idem. + apply val_content_inject_16; auto. apply Int.cast16_unsigned_signed. apply val_content_inject_32. apply Float.singleoffloat_idem. Qed. @@ -1098,13 +1055,11 @@ Proof. intros [tv [EVAL VCINJ]]. exploit storev_mapped_inject_1; eauto. intros [tm4 [STORE MEMINJ]]. - exploit eval_store. eexact H. eexact EVAL. eauto. - intro EVALSTORE. exists tm4. - split. apply exec_Sexpr with tv. auto. + split. apply exec_Sexpr with tv. eapply eval_Estore; eauto. split. auto. unfold storev in STORE; destruct tvaddr; try discriminate. - exploit store_inv; eauto. simpl. tauto. + eapply nextblock_store; eauto. Qed. (** Correctness of the variable accessors [var_get], [var_set] @@ -1112,7 +1067,7 @@ Qed. Lemma var_get_correct: forall cenv id a f e te sp lo hi m cs tm b chunk v le, - var_get cenv id = Some a -> + 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 -> eval_var_ref prog e id b chunk -> @@ -1138,7 +1093,7 @@ Proof. unfold loadv. eexact H3. intros [tv [LOAD INJ]]. exists tv; split. - eapply make_load_correct; eauto. eapply make_stackaddr_correct; eauto. + econstructor; eauto. eapply make_stackaddr_correct; eauto. auto. (* var_global_scalar *) inversion H2; [congruence|subst]. @@ -1151,14 +1106,14 @@ Proof. generalize (loadv_inject _ _ _ _ _ _ _ H1 H12 H13). intros [tv [LOAD INJ]]. exists tv; split. - eapply make_load_correct; eauto. eapply make_globaladdr_correct; eauto. + econstructor; eauto. eapply make_globaladdr_correct; eauto. auto. Qed. Lemma var_addr_correct: forall cenv id a f e te sp lo hi m cs tm b le, match_callstack f (mkframe cenv e te sp lo hi :: cs) m.(nextblock) tm.(nextblock) m -> - var_addr cenv id = Some a -> + var_addr cenv id = OK a -> eval_var_addr prog e id b -> exists tv, eval_expr tge (Vptr sp Int.zero) le te tm a E0 tm tv /\ @@ -1196,7 +1151,7 @@ Qed. Lemma var_set_correct: forall cenv id rhs a f e te sp lo hi m2 cs tm2 tm1 tv b chunk v m3 t, - var_set cenv id rhs = Some a -> + var_set cenv id rhs = OK a -> match_callstack f (mkframe cenv e te sp lo hi :: cs) m2.(nextblock) tm2.(nextblock) m2 -> eval_expr tge (Vptr sp Int.zero) nil te tm1 rhs t tm2 tv -> val_inject f v tv -> @@ -1210,7 +1165,7 @@ Lemma var_set_correct: Proof. unfold var_set; intros. assert (NEXTBLOCK: nextblock m3 = nextblock m2). - exploit store_inv; eauto. simpl; tauto. + eapply nextblock_store; eauto. inversion H0. subst. assert (match_var f id e m2 te sp cenv!!id). inversion H19; auto. inversion H6; subst; rewrite <- H7 in H; inversion H; subst; clear H. @@ -1337,7 +1292,7 @@ Proof. unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. rewrite <- H1. omega. intros until delta; unfold f1, extend_inject, eq_block. - rewrite (high_bound_alloc _ _ b _ _ _ H). + rewrite (high_bound_alloc _ _ _ _ _ H b). case (zeq b b1); intros. inversion H3. unfold sizeof; rewrite LV. omega. generalize (BOUND _ _ H3). omega. @@ -1350,7 +1305,7 @@ Proof. exploit IHalloc_variables; eauto. unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. intros until delta; unfold f1, extend_inject, eq_block. - rewrite (high_bound_alloc _ _ b _ _ _ H). + rewrite (high_bound_alloc _ _ _ _ _ H b). case (zeq b b1); intros. discriminate. eapply BOUND; eauto. intros [f' [INCR2 [MINJ2 MATCH2]]]. @@ -1373,7 +1328,7 @@ Proof. unfold f1; rewrite <- H2; eapply match_callstack_alloc_left; eauto. rewrite <- H1. omega. intros until delta; unfold f1, extend_inject, eq_block. - rewrite (high_bound_alloc _ _ b _ _ _ H). + rewrite (high_bound_alloc _ _ _ _ _ H b). case (zeq b b1); intros. inversion H6. unfold sizeof; rewrite LV. omega. generalize (BOUND _ _ H6). omega. @@ -1439,10 +1394,9 @@ Proof. intros. assert (SP: sp = nextblock tm). injection H2; auto. unfold build_compilenv in H. - eapply match_callstack_alloc_variables_rec with (sz' := sz); eauto. - eapply valid_new_block; eauto. - rewrite (low_bound_alloc _ _ sp _ _ _ H2). apply zeq_true. - rewrite (high_bound_alloc _ _ sp _ _ _ H2). apply zeq_true. + 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. @@ -1460,15 +1414,15 @@ Proof. (* me_inj *) intros until lv2. unfold Csharpminor.empty_env; rewrite PTree.gempty; congruence. (* me_inv *) - intros. exploit mi_mappedblocks; eauto. intros [A B]. + intros. exploit mi_mappedblocks; eauto. intro A. elim (fresh_block_alloc _ _ _ _ _ H2 A). (* me_incr *) - intros. exploit mi_mappedblocks; eauto. intros [A B]. + intros. exploit mi_mappedblocks; eauto. intro A. rewrite SP; auto. rewrite SP; auto. eapply alloc_right_inject; eauto. omega. - intros. exploit mi_mappedblocks; eauto. intros [A B]. + intros. exploit mi_mappedblocks; eauto. unfold valid_block; intro. unfold block in SP; omegaContradiction. (* defined *) intros. unfold te. apply set_locals_params_defined. @@ -1569,7 +1523,7 @@ Proof. inversion H18. inversion NOREPET. subst hd tl. assert (NEXT: nextblock m1 = nextblock m). - exploit store_inv; eauto. simpl; tauto. + eapply nextblock_store; eauto. generalize (me_vars0 id). intro. inversion H2; subst. (* cenv!!id = Var_local chunk *) assert (b0 = b). congruence. subst b0. @@ -1724,43 +1678,6 @@ Qed. (** * Semantic preservation for the translation *) -(** These tactics simplify hypotheses of the form [f ... = Some x]. *) - -Ltac monadSimpl1 := - match goal with - | [ |- (bind _ _ ?F ?G = Some ?X) -> _ ] => - unfold bind at 1; - generalize (refl_equal F); - pattern F at -1 in |- *; - case F; - [ (let EQ := fresh "EQ" in - (intro; intro EQ; - try monadSimpl1)) - | intros; discriminate ] - | [ |- (None = Some _) -> _ ] => - intro; discriminate - | [ |- (Some _ = Some _) -> _ ] => - let h := fresh "H" in - (intro h; injection h; intro; clear h) - end. - -Ltac monadSimpl := - match goal with - | [ |- (bind _ _ ?F ?G = Some ?X) -> _ ] => monadSimpl1 - | [ |- (None = Some _) -> _ ] => monadSimpl1 - | [ |- (Some _ = Some _) -> _ ] => monadSimpl1 - | [ |- (?F _ _ _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 - | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 - | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 - | [ |- (?F _ _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 - | [ |- (?F _ _ _ = Some _) -> _ ] => simpl F; monadSimpl1 - | [ |- (?F _ _ = Some _) -> _ ] => simpl F; monadSimpl1 - | [ |- (?F _ = Some _) -> _ ] => simpl F; monadSimpl1 - end. - -Ltac monadInv H := - generalize H; monadSimpl. - (** The proof of semantic preservation uses simulation diagrams of the following form: << @@ -1790,7 +1707,7 @@ Ltac monadInv H := Definition eval_expr_prop (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (a: Csharpminor.expr) (t: trace) (m2: mem) (v: val) : Prop := forall cenv ta f1 tle te tm1 sp lo hi cs - (TR: transl_expr cenv a = Some ta) + (TR: transl_expr cenv a = OK ta) (LINJ: val_list_inject f1 le tle) (MINJ: mem_inject f1 m1 tm1) (MATCH: match_callstack f1 @@ -1808,7 +1725,7 @@ Definition eval_expr_prop Definition eval_exprlist_prop (le: Csharpminor.letenv) (e: Csharpminor.env) (m1: mem) (al: Csharpminor.exprlist) (t: trace) (m2: mem) (vl: list val) : Prop := forall cenv tal f1 tle te tm1 sp lo hi cs - (TR: transl_exprlist cenv al = Some tal) + (TR: transl_exprlist cenv al = OK tal) (LINJ: val_list_inject f1 le tle) (MINJ: mem_inject f1 m1 tm1) (MATCH: match_callstack f1 @@ -1826,7 +1743,7 @@ Definition eval_exprlist_prop Definition eval_funcall_prop (m1: mem) (fn: Csharpminor.fundef) (args: list val) (t: trace) (m2: mem) (res: val) : Prop := forall tfn f1 tm1 cs targs - (TR: transl_fundef gce fn = Some tfn) + (TR: transl_fundef gce fn = OK tfn) (MINJ: mem_inject f1 m1 tm1) (MATCH: match_callstack f1 cs m1.(nextblock) tm1.(nextblock) m1) (ARGSINJ: val_list_inject f1 args targs), @@ -1852,7 +1769,7 @@ Inductive outcome_inject (f: meminj) : Csharpminor.outcome -> outcome -> Prop := Definition exec_stmt_prop (e: Csharpminor.env) (m1: mem) (s: Csharpminor.stmt) (t: trace) (m2: mem) (out: Csharpminor.outcome): Prop := forall cenv ts f1 te1 tm1 sp lo hi cs - (TR: transl_stmt cenv s = Some ts) + (TR: transl_stmt cenv s = OK ts) (MINJ: mem_inject f1 m1 tm1) (MATCH: match_callstack f1 (mkframe cenv e te1 sp lo hi :: cs) @@ -1897,21 +1814,61 @@ Proof. exists f1; exists tm1; exists tv. intuition eauto. Qed. -Lemma transl_expr_Eop_correct: - forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) - (op : Csharpminor.operation) (al : Csharpminor.exprlist) - (t: trace) (m1 : mem) (vl : list val) (v : val), - Csharpminor.eval_exprlist prog le e m al t m1 vl -> - eval_exprlist_prop le e m al t m1 vl -> - Csharpminor.eval_operation op vl m1 = Some v -> - eval_expr_prop le e m (Csharpminor.Eop op al) t m1 v. -Proof. - intros; red; intros. monadInv TR; intro EQ0. +Lemma transl_expr_Econst_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (cst : Csharpminor.constant) (v : val), + Csharpminor.eval_constant cst = Some v -> + eval_expr_prop le e m (Csharpminor.Econst cst) E0 m v. +Proof. + intros; red; intros; monadInv TR. + exploit transl_constant_correct; eauto. + intros [tv [EVAL VINJ]]. + exists f1; exists tm1; exists tv. intuition eauto. + constructor; eauto. +Qed. + +Lemma transl_expr_Eunop_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (op : unary_operation) (a : Csharpminor.expr) (t : trace) + (m1 : mem) (v1 v : val), + Csharpminor.eval_expr prog le e m a t m1 v1 -> + eval_expr_prop le e m a t m1 v1 -> + Csharpminor.eval_unop op v1 = Some v -> + eval_expr_prop le e m (Csharpminor.Eunop op a) t m1 v. +Proof. + intros; red; intros. monadInv TR. exploit H0; eauto. intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. - exploit make_op_correct; eauto. - intros [tv [EVAL2 VINJ2]]. - exists f2; exists tm2; exists tv. intuition. + exploit eval_unop_compat; eauto. intros [tv [EVAL VINJ]]. + exists f2; exists tm2; exists tv; intuition. + econstructor; eauto. +Qed. + +Lemma transl_expr_Ebinop_correct: + forall (le : Csharpminor.letenv) (e : Csharpminor.env) (m : mem) + (op : binary_operation) (a1 a2 : Csharpminor.expr) (t1 : trace) + (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem) (v2 : val) + (t : trace) (v : val), + Csharpminor.eval_expr prog le e m a1 t1 m1 v1 -> + eval_expr_prop le e m a1 t1 m1 v1 -> + Csharpminor.eval_expr prog le e m1 a2 t2 m2 v2 -> + eval_expr_prop le e m1 a2 t2 m2 v2 -> + Csharpminor.eval_binop op v1 v2 m2 = Some v -> + t = t1 ** t2 -> + eval_expr_prop le e m (Csharpminor.Ebinop op a1 a2) t m2 v. +Proof. + intros; red; intros. monadInv TR. + exploit H0; eauto. + intros [f2 [tm2 [tvl [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. + exploit H2. + eauto. eapply val_list_inject_incr; eauto. eauto. eauto. + intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]. + exploit eval_binop_compat. + eauto. eapply val_inject_incr; eauto. eauto. eauto. + intros [tv [EVAL VINJ]]. + exists f3; exists tm3; exists tv; intuition. + econstructor; eauto. + eapply inject_incr_trans; eauto. Qed. Lemma transl_expr_Eload_correct: @@ -1931,7 +1888,7 @@ Proof. intros [tv [TLOAD VINJ]]. exists f2; exists tm2; exists tv. intuition. - subst ta. eapply make_load_correct; eauto. + econstructor; eauto. Qed. Lemma transl_expr_Ecall_correct: @@ -1951,7 +1908,7 @@ Lemma transl_expr_Ecall_correct: t = t1 ** t2 ** t3 -> eval_expr_prop le e m (Csharpminor.Ecall sig a bl) t m3 vres. Proof. - intros;red;intros. monadInv TR. subst ta. + intros;red;intros. monadInv TR. exploit H0; eauto. intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR1 MATCH1]]]]]]]. exploit H2. @@ -1960,18 +1917,18 @@ Proof. assert (tv1 = vf). elim (Genv.find_funct_inv H3). intros bf VF. rewrite VF in H3. rewrite Genv.find_funct_find_funct_ptr in H3. - generalize (Genv.find_funct_ptr_inv H3). intro. + generalize (Genv.find_funct_ptr_negative H3). intro. assert (match_globalenvs f2). eapply match_callstack_match_globalenvs; eauto. - generalize (mg_functions _ H9 _ H8). intro. + generalize (mg_functions _ H7 _ H4). intro. rewrite VF in VINJ1. inversion VINJ1. subst vf. decEq. congruence. - subst ofs2. replace x with 0. reflexivity. congruence. + subst ofs2. replace x1 with 0. reflexivity. congruence. subst tv1. elim (functions_translated _ _ H3). intros tf [FIND TRF]. exploit H6; eauto. intros [f4 [tm4 [tres [EVAL3 [VINJ3 [MINJ3 [INCR3 MATCH3]]]]]]]. exists f4; exists tm4; exists tres. intuition. eapply eval_Ecall; eauto. - rewrite <- H4. apply sig_preserved; auto. + apply sig_preserved; auto. apply inject_incr_trans with f2; auto. apply inject_incr_trans with f3; auto. Qed. @@ -1996,8 +1953,8 @@ Proof. intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]. exists f3; exists tm3; exists tv2. intuition. - rewrite <- H6. subst t; eapply eval_conditionalexpr_true; eauto. - inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply eval_Econdition with (b1 := true); eauto. + eapply val_inject_bool_of_val; eauto. apply Val.bool_of_true_val; eauto. eapply inject_incr_trans; eauto. Qed. @@ -2021,8 +1978,8 @@ Proof. intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]. exists f3; exists tm3; exists tv2. intuition. - rewrite <- H6. subst t; eapply eval_conditionalexpr_false; eauto. - inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply eval_Econdition with (b1 := false); eauto. + eapply val_inject_bool_of_val; eauto. apply Val.bool_of_false_val; eauto. eapply inject_incr_trans; eauto. Qed. @@ -2047,7 +2004,7 @@ Proof. intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ2 [INCR2 MATCH2]]]]]]]. exists f3; exists tm3; exists tv2. intuition. - subst ta; eapply eval_Elet; eauto. + eapply eval_Elet; eauto. eapply inject_incr_trans; eauto. Qed. @@ -2072,7 +2029,7 @@ Proof. exploit val_list_inject_nth; eauto. intros [tv [A B]]. exists f1; exists tm1; exists tv. intuition. - subst ta. eapply eval_Eletvar; auto. + eapply eval_Eletvar; auto. Qed. Lemma transl_expr_Ealloc_correct: @@ -2095,7 +2052,7 @@ Proof. intros [MINJ3 INCR3]. exists (extend_inject b (Some (tb, 0)) f2); exists tm3; exists (Vptr tb Int.zero). - split. subst ta; econstructor; eauto. + split. econstructor; eauto. split. econstructor. unfold extend_inject, eq_block. rewrite zeq_true. reflexivity. reflexivity. split. assumption. @@ -2109,7 +2066,7 @@ Lemma transl_exprlist_Enil_correct: Proof. intros; red; intros. monadInv TR. exists f1; exists tm1; exists (@nil val). - intuition. subst tal; constructor. + intuition. constructor. Qed. Lemma transl_exprlist_Econs_correct: @@ -2131,7 +2088,7 @@ Proof. eauto. eapply val_list_inject_incr; eauto. eauto. eauto. intros [f3 [tm3 [tv2 [EVAL2 [VINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]. exists f3; exists tm3; exists (tv1 :: tv2). - intuition. subst tal; econstructor; eauto. + intuition. econstructor; eauto. constructor. eapply val_inject_incr; eauto. auto. eapply inject_incr_trans; eauto. Qed. @@ -2149,15 +2106,11 @@ Lemma transl_funcall_internal_correct: eval_funcall_prop m (Internal f) vargs t (free_list m3 lb) vres. Proof. intros; red. intros tfn f1 tm; intros. - generalize TR; clear TR. - unfold transl_fundef, transf_partial_fundef. - caseEq (transl_function gce f); try congruence. - intros tf TR EQ. inversion EQ; clear EQ; subst tfn. - unfold transl_function in TR. + monadInv TR. generalize EQ. + unfold transl_function. caseEq (build_compilenv gce f); intros cenv stacksize CENV. - rewrite CENV in TR. - destruct (zle stacksize Int.max_signed); try discriminate. - monadInv TR. clear TR. + destruct (zle stacksize Int.max_signed); try congruence. + intro TR. monadInv TR. caseEq (alloc tm 0 stacksize). intros tm1 sp ALLOC. exploit function_entry_ok; eauto. intros [f2 [te2 [tm2 [STOREPARAM [MINJ2 [INCR12 [MATCH2 BLOCKS]]]]]]]. @@ -2177,9 +2130,11 @@ Proof. exists v2; split. auto. subst vres; auto. contradiction. destruct H5 as [tvres [TOUT VINJRES]]. + assert (outcome_free_mem tout tm3 sp = Mem.free tm3 sp). + inversion OUTINJ; auto. exists f3; exists (Mem.free tm3 sp); exists tvres. (* execution *) - split. rewrite <- H6; econstructor; simpl; eauto. + split. rewrite <- H5. econstructor; simpl; eauto. apply exec_Sseq_continue with E0 te2 tm2 t. exact STOREPARAM. eexact EXECBODY. @@ -2195,7 +2150,7 @@ Proof. (* match_callstack *) assert (forall bl mm, nextblock (free_list mm bl) = nextblock mm). induction bl; intros. reflexivity. simpl. auto. - unfold free; simpl nextblock. rewrite H5. + unfold free; simpl nextblock. rewrite H6. eapply match_callstack_freelist; eauto. intros. elim (BLOCKS b); intros B1 B2. generalize (B2 H7). omega. Qed. @@ -2206,8 +2161,7 @@ Lemma transl_funcall_external_correct: event_match ef vargs t vres -> eval_funcall_prop m (External ef) vargs t m vres. Proof. - intros; red; intros. - simpl in TR. inversion TR; clear TR; subst tfn. + intros; red; intros. monadInv TR. exploit event_match_inject; eauto. intros [A B]. exists f1; exists tm1; exists vres; intuition. constructor; auto. @@ -2219,7 +2173,7 @@ Lemma transl_stmt_Sskip_correct: Proof. intros; red; intros. monadInv TR. exists f1; exists te1; exists tm1; exists Out_normal. - intuition. subst ts; constructor. constructor. + intuition. constructor. constructor. Qed. Lemma transl_stmt_Sexpr_correct: @@ -2233,7 +2187,7 @@ Proof. exploit H0; eauto. intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]. exists f2; exists te1; exists tm2; exists Out_normal. - intuition. subst ts. econstructor; eauto. + intuition. econstructor; eauto. constructor. Qed. @@ -2247,7 +2201,7 @@ Lemma transl_stmt_Sassign_correct: store chunk m1 b 0 v = Some m2 -> exec_stmt_prop e m (Csharpminor.Sassign id a) t m2 Csharpminor.Out_normal. Proof. - intros; red; intros. monadInv TR; intro EQ0. + intros; red; intros. monadInv TR. exploit H0; eauto. intros [f2 [tm2 [tv1 [EVAL1 [VINJ1 [MINJ1 [INCR12 MATCH1]]]]]]]. exploit var_set_correct; eauto. @@ -2282,15 +2236,15 @@ Proof. eapply val_inject_incr; eauto. eauto. intros [tm4 [EVAL [MINJ4 NEXTBLOCK]]]. exists f3; exists te1; exists tm4; exists Out_normal. - rewrite <- H6. subst t3. intuition. + intuition. constructor. eapply inject_incr_trans; eauto. assert (val_inject f3 v1 tv1). eapply val_inject_incr; eauto. unfold storev in H3; destruct v1; try discriminate. inversion H4. rewrite NEXTBLOCK. replace (nextblock m3) with (nextblock m2). - eapply match_callstack_mapped; eauto. congruence. - exploit store_inv; eauto. simpl; symmetry; tauto. + eapply match_callstack_mapped; eauto. congruence. + symmetry. eapply nextblock_store; eauto. Qed. Lemma transl_stmt_Sseq_continue_correct: @@ -2309,7 +2263,7 @@ Proof. exploit H2; eauto. intros [f3 [te3 [tm3 [tout2 [EXEC2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. exists f3; exists te3; exists tm3; exists tout2. - intuition. subst ts; eapply exec_Sseq_continue; eauto. + intuition. eapply exec_Sseq_continue; eauto. inversion OINJ1. subst tout1. auto. eapply inject_incr_trans; eauto. Qed. @@ -2326,7 +2280,7 @@ Proof. exploit H0; eauto. intros [f2 [te2 [tm2 [tout1 [EXEC1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. exists f2; exists te2; exists tm2; exists tout1. - intuition. subst ts; eapply exec_Sseq_stop; eauto. + intuition. eapply exec_Sseq_stop; eauto. inversion OINJ1; subst out tout1; congruence. Qed. @@ -2350,8 +2304,8 @@ Proof. intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]]. exists f3; exists te3; exists tm3; exists tout. intuition. - subst ts t. eapply exec_ifthenelse_true; eauto. - inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply exec_Sifthenelse with (b1 := true); eauto. + eapply val_inject_bool_of_val; eauto. apply Val.bool_of_true_val; auto. eapply inject_incr_trans; eauto. Qed. @@ -2375,8 +2329,8 @@ Proof. intros [f3 [te3 [tm3 [tout [EVAL2 [OINJ [MINJ3 [INCR3 MATCH3]]]]]]]]. exists f3; exists te3; exists tm3; exists tout. intuition. - subst ts t. eapply exec_ifthenelse_false; eauto. - inversion VINJ1; subst v1 tv1; simpl in H1; simpl; contradiction || auto. + eapply exec_Sifthenelse with (b1 := false); eauto. + eapply val_inject_bool_of_val; eauto. apply Val.bool_of_false_val; auto. eapply inject_incr_trans; eauto. Qed. @@ -2391,14 +2345,14 @@ Lemma transl_stmt_Sloop_loop_correct: t = t1 ** t2 -> exec_stmt_prop e m (Csharpminor.Sloop sl) t m2 out. Proof. - intros; red; intros. monadInv TR. + intros; red; intros. generalize TR; intro TR'; monadInv TR'. exploit H0; eauto. intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. exploit H2; eauto. intros [f3 [te3 [tm3 [tout2 [EVAL2 [OINJ2 [MINJ3 [INCR3 MATCH3]]]]]]]]. exists f3; exists te3; exists tm3; exists tout2. intuition. - subst ts. eapply exec_Sloop_loop; eauto. + eapply exec_Sloop_loop; eauto. inversion OINJ1; subst tout1; eauto. eapply inject_incr_trans; eauto. Qed. @@ -2415,7 +2369,7 @@ Proof. exploit H0; eauto. intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. exists f2; exists te2; exists tm2; exists tout1. - intuition. subst ts; eapply exec_Sloop_stop; eauto. + intuition. eapply exec_Sloop_stop; eauto. inversion OINJ1; subst out tout1; congruence. Qed. @@ -2431,7 +2385,7 @@ Proof. exploit H0; eauto. intros [f2 [te2 [tm2 [tout1 [EVAL1 [OINJ1 [MINJ2 [INCR2 MATCH2]]]]]]]]. exists f2; exists te2; exists tm2; exists (outcome_block tout1). - intuition. subst ts; eapply exec_Sblock; eauto. + intuition. eapply exec_Sblock; eauto. inversion OINJ1; subst out tout1; simpl. constructor. destruct n; constructor. @@ -2445,7 +2399,7 @@ Lemma transl_stmt_Sexit_correct: Proof. intros; red; intros. monadInv TR. exists f1; exists te1; exists tm1; exists (Out_exit n). - intuition. subst ts; constructor. constructor. + intuition. constructor. constructor. Qed. Lemma transl_stmt_Sswitch_correct: @@ -2462,7 +2416,7 @@ Proof. intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]. exists f2; exists te1; exists tm2; exists (Out_exit (switch_target n default cases)). intuition. - subst ts. constructor. inversion VINJ1. subst tv1. assumption. + constructor. inversion VINJ1. subst tv1. assumption. constructor. Qed. @@ -2473,7 +2427,7 @@ Lemma transl_stmt_Sreturn_none_correct: Proof. intros; red; intros. monadInv TR. exists f1; exists te1; exists tm1; exists (Out_return None). - intuition. subst ts; constructor. constructor. + intuition. constructor. constructor. Qed. Lemma transl_stmt_Sreturn_some_correct: @@ -2488,7 +2442,7 @@ Proof. exploit H0; eauto. intros [f2 [tm2 [tv1 [EVAL [VINJ1 [MINJ2 [INCR MATCH2]]]]]]]. exists f2; exists te1; exists tm2; exists (Out_return (Some tv1)). - intuition. subst ts; econstructor; eauto. constructor; auto. + intuition. econstructor; eauto. constructor; auto. Qed. (** We conclude by an induction over the structure of the Csharpminor @@ -2499,7 +2453,7 @@ Lemma transl_function_correct: Csharpminor.eval_funcall prog m1 f vargs t m2 vres -> eval_funcall_prop m1 f vargs t m2 vres. Proof - (eval_funcall_ind4 prog + (Csharpminor.eval_funcall_ind4 prog eval_expr_prop eval_exprlist_prop eval_funcall_prop @@ -2507,7 +2461,9 @@ Proof transl_expr_Evar_correct transl_expr_Eaddrof_correct - transl_expr_Eop_correct + transl_expr_Econst_correct + transl_expr_Eunop_correct + transl_expr_Ebinop_correct transl_expr_Eload_correct transl_expr_Ecall_correct transl_expr_Econdition_true_correct @@ -2545,11 +2501,9 @@ Lemma match_globalenvs_init: match_globalenvs f. Proof. intros. constructor. - (* globalvars *) - (* symbols *) intros. split. unfold f. rewrite zlt_true. auto. unfold m. - eapply Genv.find_symbol_inv; eauto. + eapply Genv.find_symbol_not_fresh; eauto. rewrite <- H. apply symbols_preserved. intros. unfold f. rewrite zlt_true. auto. generalize (nextblock_pos m). omega. @@ -2566,20 +2520,10 @@ Proof. intros t n [b [fn [m [FINDS [FINDF [SIG EVAL]]]]]]. elim (function_ptr_translated _ _ FINDF). intros tfn [TFIND TR]. set (m0 := Genv.init_mem prog) in *. - set (f := fun b => if zlt b m0.(nextblock) then Some(b, 0) else None). + set (f := meminj_init m0). assert (MINJ0: mem_inject f m0 m0). - unfold f; constructor; intros. - apply zlt_false; auto. - destruct (zlt b0 (nextblock m0)); try discriminate. - inversion H; subst b' delta. - split. auto. - constructor. compute. split; congruence. left; auto. - intros; omega. - generalize (Genv.initmem_block_init prog b0). fold m0. intros [idata EQ]. - rewrite EQ. simpl. apply Mem.contents_init_data_inject. - destruct (zlt b1 (nextblock m0)); try discriminate. - destruct (zlt b2 (nextblock m0)); try discriminate. - left; congruence. + unfold f; apply init_inject. + unfold m0; apply Genv.initmem_inject_neutral. assert (MATCH0: match_callstack f nil m0.(nextblock) m0.(nextblock) m0). constructor. unfold f; apply match_globalenvs_init. fold ge in EVAL. diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v index 4cc8555..e24430c 100644 --- a/cfrontend/Csem.v +++ b/cfrontend/Csem.v @@ -1,6 +1,7 @@ (** * Dynamic semantics for the Clight language *) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import Integers. Require Import Floats. @@ -559,7 +560,7 @@ with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop := | eval_Efield_struct: forall e m a t m1 l ofs id fList i ty delta, eval_lvalue e m a t m1 l ofs -> typeof a = Tstruct id fList -> - field_offset i fList = Some delta -> + field_offset i fList = OK delta -> eval_lvalue e m (Expr (Efield a i) ty) t m1 l (Int.add ofs (Int.repr delta)) | eval_Efield_union: forall e m a t m1 l ofs id fList i ty, diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index f1d22d7..729814e 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -9,6 +9,7 @@ Require Import Values. Require Import Mem. Require Import Events. Require Import Globalenvs. +Require Cminor. (** Abstract syntax *) @@ -24,52 +25,21 @@ Require Import Globalenvs. Unlike in Cminor (the next intermediate language of the back-end), Csharpminor local variables reside in memory, and their address can be taken using [Eaddrof] expressions. +*) + +Inductive constant : Set := + | Ointconst: int -> constant (**r integer constant *) + | Ofloatconst: float -> constant. (**r floating-point constant *) - Another difference with Cminor is that Csharpminor is entirely - processor-neutral. In particular, Csharpminor uses a standard set of - operations: it does not reflect processor-specific operations nor - addressing modes. *) - -Inductive operation : Set := - | Ointconst: int -> operation (**r integer constant *) - | Ofloatconst: float -> operation (**r floating-point constant *) - | Ocast8unsigned: operation (**r 8-bit zero extension *) - | Ocast8signed: operation (**r 8-bit sign extension *) - | Ocast16unsigned: operation (**r 16-bit zero extension *) - | Ocast16signed: operation (**r 16-bit sign extension *) - | Onotbool: operation (**r boolean negation *) - | Onotint: operation (**r bitwise complement *) - | Oadd: operation (**r integer addition *) - | Osub: operation (**r integer subtraction *) - | Omul: operation (**r integer multiplication *) - | Odiv: operation (**r integer signed division *) - | Odivu: operation (**r integer unsigned division *) - | Omod: operation (**r integer signed modulus *) - | Omodu: operation (**r integer unsigned modulus *) - | Oand: operation (**r bitwise ``and'' *) - | Oor: operation (**r bitwise ``or'' *) - | Oxor: operation (**r bitwise ``xor'' *) - | Oshl: operation (**r left shift *) - | Oshr: operation (**r right signed shift *) - | Oshru: operation (**r right unsigned shift *) - | Onegf: operation (**r float opposite *) - | Oabsf: operation (**r float absolute value *) - | Oaddf: operation (**r float addition *) - | Osubf: operation (**r float subtraction *) - | Omulf: operation (**r float multiplication *) - | Odivf: operation (**r float division *) - | Osingleoffloat: operation (**r float truncation *) - | Ointoffloat: operation (**r integer to float *) - | Ofloatofint: operation (**r float to signed integer *) - | Ofloatofintu: operation (**r float to unsigned integer *) - | Ocmp: comparison -> operation (**r integer signed comparison *) - | Ocmpu: comparison -> operation (**r integer unsigned comparison *) - | Ocmpf: comparison -> operation. (**r float comparison *) +Definition unary_operation : Set := Cminor.unary_operation. +Definition binary_operation : Set := Cminor.binary_operation. Inductive expr : Set := | Evar : ident -> expr (**r reading a scalar variable *) | Eaddrof : ident -> expr (**r taking the address of a variable *) - | Eop : operation -> exprlist -> expr (**r arithmetic operation *) + | Econst : constant -> expr + | Eunop : unary_operation -> expr -> expr + | Ebinop : binary_operation -> expr -> expr -> expr | Eload : memory_chunk -> expr -> expr (**r memory read *) | Ecall : signature -> expr -> exprlist -> expr (**r function call *) | Econdition : expr -> expr -> expr -> expr (**r conditional expression *) @@ -202,78 +172,15 @@ Definition global_var_env (p: program): gvarenv := (** Evaluation of operator applications. *) -Definition eval_compare_null (c: comparison) (n: int) : option val := - if Int.eq n Int.zero - then match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end - else None. - -Definition eval_operation (op: operation) (vl: list val) (m: mem): option val := - match op, vl with - | Ointconst n, nil => Some (Vint n) - | Ofloatconst n, nil => Some (Vfloat n) - | Ocast8unsigned, Vint n1 :: nil => Some (Vint (Int.cast8unsigned n1)) - | Ocast8signed, Vint n1 :: nil => Some (Vint (Int.cast8signed n1)) - | Ocast16unsigned, Vint n1 :: nil => Some (Vint (Int.cast16unsigned n1)) - | Ocast16signed, Vint n1 :: nil => Some (Vint (Int.cast16signed n1)) - | Onotbool, Vint n1 :: nil => Some (Val.of_bool (Int.eq n1 Int.zero)) - | Onotbool, Vptr b1 n1 :: nil => Some (Vfalse) - | Onotint, Vint n1 :: nil => Some (Vint (Int.not n1)) - | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2)) - | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1)) - | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2)) - | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2)) - | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2)) - | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None - | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2)) - | Odiv, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2)) - | Odivu, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) - | Omod, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2)) - | Omodu, Vint n1 :: Vint n2 :: nil => - if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) - | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2)) - | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2)) - | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2)) - | Oshl, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None - | Oshr, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None - | Oshru, Vint n1 :: Vint n2 :: nil => - if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None - | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) - | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1)) - | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2)) - | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2)) - | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2)) - | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2)) - | Osingleoffloat, Vfloat f1 :: nil => - Some (Vfloat (Float.singleoffloat f1)) - | Ointoffloat, Vfloat f1 :: nil => - Some (Vint (Float.intoffloat f1)) - | Ofloatofint, Vint n1 :: nil => - Some (Vfloat (Float.floatofint n1)) - | Ofloatofintu, Vint n1 :: nil => - Some (Vfloat (Float.floatofintu n1)) - | Ocmp c, Vint n1 :: Vint n2 :: nil => - Some (Val.of_bool(Int.cmp c n1 n2)) - | Ocmp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => - if valid_pointer m b1 (Int.signed n1) - && valid_pointer m b2 (Int.signed n2) then - if eq_block b1 b2 then Some(Val.of_bool(Int.cmp c n1 n2)) else None - else - None - | Ocmp c, Vptr b1 n1 :: Vint n2 :: nil => eval_compare_null c n2 - | Ocmp c, Vint n1 :: Vptr b2 n2 :: nil => eval_compare_null c n1 - | Ocmpu c, Vint n1 :: Vint n2 :: nil => - Some (Val.of_bool(Int.cmpu c n1 n2)) - | Ocmpf c, Vfloat f1 :: Vfloat f2 :: nil => - Some (Val.of_bool (Float.cmp c f1 f2)) - | _, _ => None +Definition eval_constant (cst: constant) : option val := + match cst with + | Ointconst n => Some (Vint n) + | Ofloatconst n => Some (Vfloat n) end. +Definition eval_unop := Cminor.eval_unop. +Definition eval_binop := Cminor.eval_binop. + (** Allocation of local variables at function entry. Each variable is bound to the reference to a fresh block of the appropriate size. *) @@ -361,11 +268,22 @@ Inductive eval_expr: forall le e m id b, eval_var_addr e id b -> eval_expr le e m (Eaddrof id) E0 m (Vptr b Int.zero) - | eval_Eop: - forall le e m op al t m1 vl v, - eval_exprlist le e m al t m1 vl -> - eval_operation op vl m1 = Some v -> - eval_expr le e m (Eop op al) t m1 v + | eval_Econst: + forall le e m cst v, + eval_constant cst = Some v -> + eval_expr le e m (Econst cst) E0 m v + | eval_Eunop: + forall le e m op a t m1 v1 v, + eval_expr le e m a t m1 v1 -> + eval_unop op v1 = Some v -> + eval_expr le e m (Eunop op a) t m1 v + | eval_Ebinop: + forall le e m op a1 a2 t1 m1 v1 t2 m2 v2 t v, + eval_expr le e m a1 t1 m1 v1 -> + eval_expr le e m1 a2 t2 m2 v2 -> + eval_binop op v1 v2 m2 = Some v -> + t = t1 ** t2 -> + eval_expr le e m (Ebinop op a1 a2) t m2 v | eval_Eload: forall le e m chunk a t m1 v1 v, eval_expr le e m a t m1 v1 -> diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v index 664c6fc..5ab685d 100644 --- a/cfrontend/Cshmgen.v +++ b/cfrontend/Cshmgen.v @@ -1,19 +1,14 @@ Require Import Coqlib. +Require Import Errors. Require Import Integers. Require Import Floats. Require Import AST. Require Import Csyntax. +Require Import Cminor. Require Import Csharpminor. -(** The error monad *) - -Definition bind (A B: Set) (f: option A) (g: A -> option B) := - match f with None => None | Some x => g x end. - -Implicit Arguments bind [A B]. - -Notation "'do' X <- A ; B" := (bind A (fun X => B)) - (at level 200, X ident, A at level 100, B at level 200). +Open Local Scope string_scope. +Open Local Scope error_monad_scope. (** ** Operations on C types *) @@ -22,28 +17,28 @@ Definition signature_of_function (f: Csyntax.function) : signature := (typlist_of_typelist (type_of_params (Csyntax.fn_params f))) (opttyp_of_type (Csyntax.fn_return f)). -Definition chunk_of_type (ty: type): option memory_chunk := +Definition chunk_of_type (ty: type): res memory_chunk := match access_mode ty with - | By_value chunk => Some chunk - | _ => None + | By_value chunk => OK chunk + | _ => Error (msg "Cshmgen.chunk_of_type") end. -Definition var_kind_of_type (ty: type): option var_kind := +Definition var_kind_of_type (ty: type): res var_kind := match ty with - | Tint I8 Signed => Some(Vscalar Mint8signed) - | Tint I8 Unsigned => Some(Vscalar Mint8unsigned) - | Tint I16 Signed => Some(Vscalar Mint16signed) - | Tint I16 Unsigned => Some(Vscalar Mint16unsigned) - | Tint I32 _ => Some(Vscalar Mint32) - | Tfloat F32 => Some(Vscalar Mfloat32) - | Tfloat F64 => Some(Vscalar Mfloat64) - | Tvoid => None - | Tpointer _ => Some(Vscalar Mint32) - | Tarray _ _ => Some(Varray (Csyntax.sizeof ty)) - | Tfunction _ _ => None - | Tstruct _ fList => Some(Varray (Csyntax.sizeof ty)) - | Tunion _ fList => Some(Varray (Csyntax.sizeof ty)) - | Tcomp_ptr _ => Some(Vscalar Mint32) + | Tint I8 Signed => OK(Vscalar Mint8signed) + | Tint I8 Unsigned => OK(Vscalar Mint8unsigned) + | Tint I16 Signed => OK(Vscalar Mint16signed) + | Tint I16 Unsigned => OK(Vscalar Mint16unsigned) + | Tint I32 _ => OK(Vscalar Mint32) + | Tfloat F32 => OK(Vscalar Mfloat32) + | Tfloat F64 => OK(Vscalar Mfloat64) + | Tvoid => Error (msg "Cshmgen.var_kind_of_type(void)") + | Tpointer _ => OK(Vscalar Mint32) + | Tarray _ _ => OK(Varray (Csyntax.sizeof ty)) + | Tfunction _ _ => Error (msg "Cshmgen.var_kind_of_type(function)") + | Tstruct _ fList => OK(Varray (Csyntax.sizeof ty)) + | Tunion _ fList => OK(Varray (Csyntax.sizeof ty)) + | Tcomp_ptr _ => OK(Vscalar Mint32) end. (** ** Csharpminor constructors *) @@ -60,19 +55,14 @@ end. denoting a case where the operation is not defined at the given types. *) -Definition make_intconst (n: int) := Eop (Ointconst n) Enil. - -Definition make_floatconst (f: float) := Eop (Ofloatconst f) Enil. - -Definition make_unop (op: operation) (e: expr) := Eop op (Econs e Enil). +Definition make_intconst (n: int) := Econst (Ointconst n). -Definition make_binop (op: operation) (e1 e2: expr) := - Eop op (Econs e1 (Econs e2 Enil)). +Definition make_floatconst (f: float) := Econst (Ofloatconst f). Definition make_floatofint (e: expr) (sg: signedness) := match sg with - | Signed => make_unop Ofloatofint e - | Unsigned => make_unop Ofloatofintu e + | Signed => Eunop Ofloatofint e + | Unsigned => Eunop Ofloatofintu e end. (* [make_boolean e ty] returns a Csharpminor expression that evaluates @@ -84,98 +74,98 @@ Definition make_floatofint (e: expr) (sg: signedness) := *) Definition make_boolean (e: expr) (ty: type) := match ty with - | Tfloat _ => make_binop (Ocmpf Cne) e (make_floatconst Float.zero) + | Tfloat _ => Ebinop (Ocmpf Cne) e (make_floatconst Float.zero) | _ => e end. Definition make_neg (e: expr) (ty: type) := match ty with - | Tint _ _ => Some (make_binop Osub (make_intconst Int.zero) e) - | Tfloat _ => Some (make_unop Onegf e) - | _ => None + | Tint _ _ => OK (Eunop Onegint e) + | Tfloat _ => OK (Eunop Onegf e) + | _ => Error (msg "Cshmgen.make_neg") end. Definition make_notbool (e: expr) (ty: type) := match ty with - | Tfloat _ => make_binop (Ocmpf Ceq) e (make_floatconst Float.zero) - | _ => make_unop Onotbool e + | Tfloat _ => Ebinop (Ocmpf Ceq) e (make_floatconst Float.zero) + | _ => Eunop Onotbool e end. Definition make_notint (e: expr) (ty: type) := - make_unop Onotint e. + Eunop Onotint e. Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_add ty1 ty2 with - | add_case_ii => Some (make_binop Oadd e1 e2) - | add_case_ff => Some (make_binop Oaddf e1 e2) + | add_case_ii => OK (Ebinop Oadd e1 e2) + | add_case_ff => OK (Ebinop Oaddf e1 e2) | add_case_pi ty => let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in - Some (make_binop Oadd e1 (make_binop Omul n e2)) - | add_default => None + OK (Ebinop Oadd e1 (Ebinop Omul n e2)) + | add_default => Error (msg "Cshmgen.make_add") end. Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_sub ty1 ty2 with - | sub_case_ii => Some (make_binop Osub e1 e2) - | sub_case_ff => Some (make_binop Osubf e1 e2) + | sub_case_ii => OK (Ebinop Osub e1 e2) + | sub_case_ff => OK (Ebinop Osubf e1 e2) | sub_case_pi ty => let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in - Some (make_binop Osub e1 (make_binop Omul n e2)) + OK (Ebinop Osub e1 (Ebinop Omul n e2)) | sub_case_pp ty => let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in - Some (make_binop Odivu (make_binop Osub e1 e2) n) - | sub_default => None + OK (Ebinop Odivu (Ebinop Osub e1 e2) n) + | sub_default => Error (msg "Cshmgen.make_sub") end. Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_mul ty1 ty2 with - | mul_case_ii => Some (make_binop Omul e1 e2) - | mul_case_ff => Some (make_binop Omulf e1 e2) - | mul_default => None + | mul_case_ii => OK (Ebinop Omul e1 e2) + | mul_case_ff => OK (Ebinop Omulf e1 e2) + | mul_default => Error (msg "Cshmgen.make_mul") end. Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_div ty1 ty2 with - | div_case_I32unsi => Some (make_binop Odivu e1 e2) - | div_case_ii => Some (make_binop Odiv e1 e2) - | div_case_ff => Some (make_binop Odivf e1 e2) - | div_default => None + | div_case_I32unsi => OK (Ebinop Odivu e1 e2) + | div_case_ii => OK (Ebinop Odiv e1 e2) + | div_case_ff => OK (Ebinop Odivf e1 e2) + | div_default => Error (msg "Cshmgen.make_div") end. Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_mod ty1 ty2 with - | mod_case_I32unsi => Some (make_binop Omodu e1 e2) - | mod_case_ii=> Some (make_binop Omod e1 e2) - | mod_default => None + | mod_case_I32unsi => OK (Ebinop Omodu e1 e2) + | mod_case_ii=> OK (Ebinop Omod e1 e2) + | mod_default => Error (msg "Cshmgen.make_mod") end. Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - Some(make_binop Oand e1 e2). + OK(Ebinop Oand e1 e2). Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - Some(make_binop Oor e1 e2). + OK(Ebinop Oor e1 e2). Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - Some(make_binop Oxor e1 e2). + OK(Ebinop Oxor e1 e2). Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) := - Some(make_binop Oshl e1 e2). + OK(Ebinop Oshl e1 e2). Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_shr ty1 ty2 with - | shr_case_I32unsi => Some (make_binop Oshru e1 e2) - | shr_case_ii=> Some (make_binop Oshr e1 e2) - | shr_default => None + | shr_case_I32unsi => OK (Ebinop Oshru e1 e2) + | shr_case_ii=> OK (Ebinop Oshr e1 e2) + | shr_default => Error (msg "Cshmgen.make_shr") end. Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) := match classify_cmp ty1 ty2 with - | cmp_case_I32unsi => Some (make_binop (Ocmpu c) e1 e2) - | cmp_case_ii => Some (make_binop (Ocmp c) e1 e2) - | cmp_case_ff => Some (make_binop (Ocmpf c) e1 e2) - | cmp_case_pi => Some (make_binop (Ocmp c) e1 e2) - | cmp_case_pp => Some (make_binop (Ocmp c) e1 e2) - | cmp_default => None + | cmp_case_I32unsi => OK (Ebinop (Ocmpu c) e1 e2) + | cmp_case_ii => OK (Ebinop (Ocmp c) e1 e2) + | cmp_case_ff => OK (Ebinop (Ocmpf c) e1 e2) + | cmp_case_pi => OK (Ebinop (Ocmp c) e1 e2) + | cmp_case_pp => OK (Ebinop (Ocmp c) e1 e2) + | cmp_default => Error (msg "Cshmgen.make_shr") end. Definition make_andbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) := @@ -206,17 +196,17 @@ Definition make_orbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) := Definition make_cast1 (from to: type) (e: expr) := match from, to with | Tint _ uns, Tfloat _ => make_floatofint e uns - | Tfloat _, Tint _ _ => make_unop Ointoffloat e + | Tfloat _, Tint _ _ => Eunop Ointoffloat e | _, _ => e end. Definition make_cast2 (from to: type) (e: expr) := match to with - | Tint I8 Signed => make_unop Ocast8signed e - | Tint I8 Unsigned => make_unop Ocast8unsigned e - | Tint I16 Signed => make_unop Ocast16signed e - | Tint I16 Unsigned => make_unop Ocast16unsigned e - | Tfloat F32 => make_unop Osingleoffloat e + | Tint I8 Signed => Eunop Ocast8signed e + | Tint I8 Unsigned => Eunop Ocast8unsigned e + | Tint I16 Signed => Eunop Ocast16signed e + | Tint I16 Unsigned => Eunop Ocast16unsigned e + | Tfloat F32 => Eunop Osingleoffloat e | _ => e end. @@ -231,9 +221,9 @@ Definition make_cast (from to: type) (e: expr) := Definition make_load (addr: expr) (ty_res: type) := match (access_mode ty_res) with - | By_value chunk => Some (Eload chunk addr) - | By_reference => Some addr - | By_nothing => None + | By_value chunk => OK (Eload chunk addr) + | By_reference => OK addr + | By_nothing => Error (msg "Cshmgen.make_load") end. (* [make_store addr ty_res rhs ty_rhs] stores the value of the @@ -243,8 +233,8 @@ Definition make_load (addr: expr) (ty_res: type) := Definition make_store (addr: expr) (ty: type) (rhs: expr) := match access_mode ty with - | By_value chunk => Some (Sstore chunk addr rhs) - | _ => None + | By_value chunk => OK (Sstore chunk addr rhs) + | _ => Error (msg "Cshmgen.make_store") end. (** ** Reading and writing variables *) @@ -258,9 +248,9 @@ Definition make_store (addr: expr) (ty: type) (rhs: expr) := Definition var_get (id: ident) (ty: type) := match access_mode ty with - | By_value chunk => Some (Evar id) - | By_reference => Some (Eaddrof id) - | _ => None + | By_value chunk => OK (Evar id) + | By_reference => OK (Eaddrof id) + | _ => Error (MSG "Cshmgen.var_get " :: CTX id :: nil) end. (* [var_set id ty rhs] stores the value of the Csharpminor @@ -269,21 +259,22 @@ Definition var_get (id: ident) (ty: type) := Definition var_set (id: ident) (ty: type) (rhs: expr) := match access_mode ty with - | By_value chunk => Some (Sassign id rhs) - | _ => None + | By_value chunk => OK (Sassign id rhs) + | _ => Error (MSG "Cshmgen.var_set " :: CTX id :: nil) end. (** ** Translation of operators *) -Definition transl_unop (op: unary_operation) (a: expr) (ta: type) : option expr := +Definition transl_unop (op: Csyntax.unary_operation) (a: expr) (ta: type) : res expr := match op with - | Csyntax.Onotbool => Some(make_notbool a ta) - | Csyntax.Onotint => Some(make_notint a ta) + | Csyntax.Onotbool => OK(make_notbool a ta) + | Csyntax.Onotint => OK(make_notint a ta) | Csyntax.Oneg => make_neg a ta end. -Definition transl_binop (op: binary_operation) (a: expr) (ta: type) - (b: expr) (tb: type) : option expr := +Definition transl_binop (op: Csyntax.binary_operation) + (a: expr) (ta: type) + (b: expr) (tb: type) : res expr := match op with | Csyntax.Oadd => make_add a ta b tb | Csyntax.Osub => make_sub a ta b tb @@ -315,12 +306,12 @@ Definition transl_binop (op: binary_operation) (a: expr) (ta: type) a || b ---> a ? 1 : (b ? 1 : 0) *) -Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := +Fixpoint transl_expr (a: Csyntax.expr) {struct a} : res expr := match a with | Expr (Csyntax.Econst_int n) _ => - Some(make_intconst n) + OK(make_intconst n) | Expr (Csyntax.Econst_float n) _ => - Some(make_floatconst n) + OK(make_floatconst n) | Expr (Csyntax.Evar id) ty => var_get id ty | Expr (Csyntax.Ederef b) _ => @@ -337,7 +328,7 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := transl_binop op tb (typeof b) tc (typeof c) | Expr (Csyntax.Ecast ty b) _ => do tb <- transl_expr b; - Some (make_cast (typeof b) ty tb) + OK (make_cast (typeof b) ty tb) | Expr (Csyntax.Eindex b c) ty => do tb <- transl_expr b; do tc <- transl_expr c; @@ -348,31 +339,33 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := | fun_case_f args res => do tb <- transl_expr b; do tcl <- transl_exprlist cl; - Some(Ecall (signature_of_type args res) tb tcl) - | _ => None + OK(Ecall (signature_of_type args res) tb tcl) + | _ => + Error(msg "Cshmgen.transl_expr(call)") end | Expr (Csyntax.Eandbool b c) _ => do tb <- transl_expr b; do tc <- transl_expr c; - Some(make_andbool tb (typeof b) tc (typeof c)) + OK(make_andbool tb (typeof b) tc (typeof c)) | Expr (Csyntax.Eorbool b c) _ => do tb <- transl_expr b; do tc <- transl_expr c; - Some(make_orbool tb (typeof b) tc (typeof c)) + OK(make_orbool tb (typeof b) tc (typeof c)) | Expr (Csyntax.Esizeof ty) _ => - Some(make_intconst (Int.repr (Csyntax.sizeof ty))) + OK(make_intconst (Int.repr (Csyntax.sizeof ty))) | Expr (Csyntax.Efield b i) ty => match typeof b with | Tstruct _ fld => do tb <- transl_lvalue b; do ofs <- field_offset i fld; make_load - (make_binop Oadd tb (make_intconst (Int.repr ofs))) + (Ebinop Oadd tb (make_intconst (Int.repr ofs))) ty | Tunion _ fld => do tb <- transl_lvalue b; make_load tb ty - | _ => None + | _ => + Error(msg "Cshmgen.transl_expr(field)") end end @@ -381,10 +374,10 @@ Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr := where the value of [a] is stored. *) -with transl_lvalue (a: Csyntax.expr) {struct a} : option expr := +with transl_lvalue (a: Csyntax.expr) {struct a} : res expr := match a with | Expr (Csyntax.Evar id) _ => - Some (Eaddrof id) + OK (Eaddrof id) | Expr (Csyntax.Ederef b) _ => transl_expr b | Expr (Csyntax.Eindex b c) _ => @@ -396,25 +389,27 @@ with transl_lvalue (a: Csyntax.expr) {struct a} : option expr := | Tstruct _ fld => do tb <- transl_lvalue b; do ofs <- field_offset i fld; - Some (make_binop Oadd tb (make_intconst (Int.repr ofs))) + OK (Ebinop Oadd tb (make_intconst (Int.repr ofs))) | Tunion _ fld => transl_lvalue b - | _ => None + | _ => + Error(msg "Cshmgen.transl_lvalue(field)") end - | _ => None + | _ => + Error(msg "Cshmgen.transl_lvalue") end (* [transl_exprlist al] returns a list of Csharpminor expressions that compute the values of the list [al] of Csyntax expressions. Used for function applications. *) -with transl_exprlist (al: Csyntax.exprlist): option exprlist := +with transl_exprlist (al: Csyntax.exprlist): res exprlist := match al with - | Csyntax.Enil => Some Enil + | Csyntax.Enil => OK Enil | Csyntax.Econs a1 a2 => do ta1 <- transl_expr a1; do ta2 <- transl_exprlist a2; - Some (Econs ta1 ta2) + OK (Econs ta1 ta2) end. (** ** Translation of statements *) @@ -431,9 +426,9 @@ Definition is_variable (e: Csyntax.expr) : option ident := value of the CabsCoq expression [e] and performs an [exit 0] if [e] evaluates to false. *) -Definition exit_if_false (e: Csyntax.expr) : option stmt := +Definition exit_if_false (e: Csyntax.expr) : res stmt := do te <- transl_expr e; - Some(Sifthenelse + OK(Sifthenelse (make_boolean te (typeof e)) Sskip (Sexit 0%nat)). @@ -497,13 +492,13 @@ Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int | LScase ni _ rem => (ni, k) :: switch_table rem (k+1) end. -Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : option stmt := +Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : res stmt := match s with | Csyntax.Sskip => - Some Sskip + OK Sskip | Csyntax.Sexpr e => do te <- transl_expr e; - Some (Sexpr te) + OK (Sexpr te) | Csyntax.Sassign b c => match (is_variable b) with | Some id => @@ -517,35 +512,35 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : o | Csyntax.Ssequence s1 s2 => do ts1 <- transl_statement nbrk ncnt s1; do ts2 <- transl_statement nbrk ncnt s2; - Some (Sseq ts1 ts2) + OK (Sseq ts1 ts2) | Csyntax.Sifthenelse e s1 s2 => do te <- transl_expr e; do ts1 <- transl_statement nbrk ncnt s1; do ts2 <- transl_statement nbrk ncnt s2; - Some (Sifthenelse (make_boolean te (typeof e)) ts1 ts2) + OK (Sifthenelse (make_boolean te (typeof e)) ts1 ts2) | Csyntax.Swhile e s1 => do te <- exit_if_false e; do ts1 <- transl_statement 1%nat 0%nat s1; - Some (Sblock (Sloop (Sseq te (Sblock ts1)))) + OK (Sblock (Sloop (Sseq te (Sblock ts1)))) | Csyntax.Sdowhile e s1 => do te <- exit_if_false e; do ts1 <- transl_statement 1%nat 0%nat s1; - Some (Sblock (Sloop (Sseq (Sblock ts1) te))) + OK (Sblock (Sloop (Sseq (Sblock ts1) te))) | Csyntax.Sfor e1 e2 e3 s1 => do te1 <- transl_statement nbrk ncnt e1; do te2 <- exit_if_false e2; do te3 <- transl_statement nbrk ncnt e3; do ts1 <- transl_statement 1%nat 0%nat s1; - Some (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))) + OK (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3))))) | Csyntax.Sbreak => - Some (Sexit nbrk) + OK (Sexit nbrk) | Csyntax.Scontinue => - Some (Sexit ncnt) + OK (Sexit ncnt) | Csyntax.Sreturn (Some e) => do te <- transl_expr e; - Some (Sreturn (Some te)) + OK (Sreturn (Some te)) | Csyntax.Sreturn None => - Some (Sreturn None) + OK (Sreturn None) | Csyntax.Sswitch e sl => let cases := switch_table sl 0 in let ncases := List.length cases in @@ -554,11 +549,11 @@ Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : o end with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt) - {struct sl}: option stmt := + {struct sl}: res stmt := match sl with | LSdefault s => do ts <- transl_statement nbrk ncnt s; - Some (Sblock (Sseq body ts)) + OK (Sblock (Sseq body ts)) | LScase _ s rem => do ts <- transl_statement nbrk ncnt s; transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts)) @@ -566,28 +561,31 @@ with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt) (*** Translation of functions *) +Definition prefix_var_name (id: ident) : errmsg := + MSG "In local variable " :: CTX id :: MSG ":\n" :: nil. + Definition transl_params (l: list (ident * type)) := - AST.map_partial chunk_of_type l. + AST.map_partial prefix_var_name chunk_of_type l. Definition transl_vars (l: list (ident * type)) := - AST.map_partial var_kind_of_type l. + AST.map_partial prefix_var_name var_kind_of_type l. -Definition transl_function (f: Csyntax.function) : option function := +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); - Some (mkfunction (signature_of_function f) tparams tvars tbody). + OK (mkfunction (signature_of_function f) tparams tvars tbody). -Definition transl_fundef (f: Csyntax.fundef) : option fundef := +Definition transl_fundef (f: Csyntax.fundef) : res fundef := match f with | Csyntax.Internal g => - do tg <- transl_function g; Some(AST.Internal tg) + do tg <- transl_function g; OK(AST.Internal tg) | Csyntax.External id args res => - Some(AST.External (external_function id args res)) + OK(AST.External (external_function id args res)) end. (** ** Translation of programs *) Definition transl_globvar (ty: type) := var_kind_of_type ty. -Definition transl_program (p: Csyntax.program) : option program := +Definition transl_program (p: Csyntax.program) : res program := transform_partial_program2 transl_fundef transl_globvar p. diff --git a/cfrontend/Cshmgenproof1.v b/cfrontend/Cshmgenproof1.v index bee0782..7ffd156 100644 --- a/cfrontend/Cshmgenproof1.v +++ b/cfrontend/Cshmgenproof1.v @@ -1,6 +1,7 @@ (** * Correctness of the C front end, part 1: syntactic properties *) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import Integers. Require Import Floats. @@ -12,64 +13,28 @@ Require Import Globalenvs. Require Import Csyntax. Require Import Csem. Require Import Ctyping. +Require Import Cminor. Require Import Csharpminor. Require Import Cshmgen. -(** Monadic simplification *) - -Ltac monadSimpl1 := - match goal with - | [ |- (bind ?F ?G = Some ?X) -> _ ] => - unfold bind at 1; - generalize (refl_equal F); - pattern F at -1 in |- *; - case F; - [ (let EQ := fresh "EQ" in - (intro; intro EQ; try monadSimpl1)) - | intro; intro; discriminate ] - | [ |- (None = Some _) -> _ ] => - intro; discriminate - | [ |- (Some _ = Some _) -> _ ] => - let h := fresh "H" in - (intro h; injection h; intro; clear h) - | [ |- (_ = Some _) -> _ ] => - let EQ := fresh "EQ" in intro EQ - end. - -Ltac monadSimpl := - match goal with - | [ |- (bind ?F ?G = Some ?X) -> _ ] => monadSimpl1 - | [ |- (None = Some _) -> _ ] => monadSimpl1 - | [ |- (Some _ = Some _) -> _ ] => monadSimpl1 - | [ |- (?F _ _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1 - | [ |- (?F _ _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1 - | [ |- (?F _ _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1 - | [ |- (?F _ _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1 - | [ |- (?F _ _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1 - | [ |- (?F _ = Some _) -> _ ] => unfold F; fold F; monadSimpl1 - end. - -Ltac monadInv H := - generalize H; monadSimpl. - (** Operations on types *) Lemma transl_fundef_sig1: forall f tf args res, - transl_fundef f = Some tf -> + transl_fundef f = OK tf -> classify_fun (type_of_fundef f) = fun_case_f args res -> funsig tf = signature_of_type args res. Proof. intros. destruct f; monadInv H. - monadInv EQ. rewrite <- H2. rewrite <- H3. simpl. + monadInv EQ. simpl. simpl in H0. inversion H0. reflexivity. - rewrite <- H2. simpl. + simpl. simpl in H0. congruence. Qed. Lemma transl_fundef_sig2: forall f tf args res, - transl_fundef f = Some tf -> + transl_fundef f = OK tf -> type_of_fundef f = Tfunction args res -> funsig tf = signature_of_type args res. Proof. @@ -80,7 +45,7 @@ Qed. Lemma var_kind_by_value: forall ty chunk, access_mode ty = By_value chunk -> - var_kind_of_type ty = Some(Vscalar chunk). + var_kind_of_type ty = OK(Vscalar chunk). Proof. intros ty chunk; destruct ty; simpl; try congruence. destruct i; try congruence; destruct s; congruence. @@ -89,7 +54,7 @@ Qed. Lemma sizeof_var_kind_of_type: forall ty vk, - var_kind_of_type ty = Some vk -> + var_kind_of_type ty = OK vk -> Csharpminor.sizeof vk = Csyntax.sizeof ty. Proof. intros ty vk. @@ -103,35 +68,35 @@ Qed. (** ** Some properties of the translation functions *) Lemma map_partial_names: - forall (A B: Set) (f: A -> option B) + forall (A B: Set) (f: A -> res B) (l: list (ident * A)) (tl: list (ident * B)), - map_partial f l = Some tl -> + map_partial prefix_var_name f l = OK tl -> List.map (@fst ident B) tl = List.map (@fst ident A) l. Proof. induction l; simpl. intros. inversion H. reflexivity. intro tl. destruct a as [id x]. destruct (f x); try congruence. - caseEq (map_partial f l); intros; try congruence. - inversion H0; subst tl. simpl. decEq. auto. + caseEq (map_partial prefix_var_name f l); simpl; intros; try congruence. + inv H0. simpl. decEq. auto. Qed. Lemma map_partial_append: - forall (A B: Set) (f: A -> option B) + forall (A B: Set) (f: A -> res B) (l1 l2: list (ident * A)) (tl1 tl2: list (ident * B)), - map_partial f l1 = Some tl1 -> - map_partial f l2 = Some tl2 -> - map_partial f (l1 ++ l2) = Some (tl1 ++ tl2). + map_partial prefix_var_name f l1 = OK tl1 -> + map_partial prefix_var_name f l2 = OK tl2 -> + map_partial prefix_var_name f (l1 ++ l2) = OK (tl1 ++ tl2). Proof. induction l1; intros until tl2; simpl. intros. inversion H. simpl; auto. destruct a as [id x]. destruct (f x); try congruence. - caseEq (map_partial f l1); intros; try congruence. - inversion H0. rewrite (IHl1 _ _ _ H H1). auto. + caseEq (map_partial prefix_var_name f l1); simpl; intros; try congruence. + inv H0. rewrite (IHl1 _ _ _ H H1). auto. Qed. Lemma transl_params_names: forall vars tvars, - transl_params vars = Some tvars -> + transl_params vars = OK tvars -> List.map (@fst ident memory_chunk) tvars = Ctyping.var_names vars. Proof. exact (map_partial_names _ _ chunk_of_type). @@ -139,7 +104,7 @@ Qed. Lemma transl_vars_names: forall vars tvars, - transl_vars vars = Some tvars -> + transl_vars vars = OK tvars -> List.map (@fst ident var_kind) tvars = Ctyping.var_names vars. Proof. exact (map_partial_names _ _ var_kind_of_type). @@ -148,8 +113,8 @@ Qed. Lemma transl_names_norepet: forall params vars sg tparams tvars body, list_norepet (var_names params ++ var_names vars) -> - transl_params params = Some tparams -> - transl_vars vars = Some tvars -> + transl_params params = OK tparams -> + transl_vars vars = OK tvars -> let f := Csharpminor.mkfunction sg tparams tvars body in list_norepet (fn_params_names f ++ fn_vars_names f). Proof. @@ -161,35 +126,35 @@ Qed. Lemma transl_vars_append: forall l1 l2 tl1 tl2, - transl_vars l1 = Some tl1 -> transl_vars l2 = Some tl2 -> - transl_vars (l1 ++ l2) = Some (tl1 ++ tl2). + transl_vars l1 = OK tl1 -> transl_vars l2 = OK tl2 -> + transl_vars (l1 ++ l2) = OK (tl1 ++ tl2). Proof. exact (map_partial_append _ _ var_kind_of_type). Qed. Lemma transl_params_vars: forall params tparams, - transl_params params = Some tparams -> + transl_params params = OK tparams -> transl_vars params = - Some (List.map (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) tparams). + OK (List.map (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) tparams). Proof. induction params; intro tparams; simpl. intros. inversion H. reflexivity. destruct a as [id x]. unfold chunk_of_type. caseEq (access_mode x); try congruence. intros chunk AM. - caseEq (transl_params params); intros; try congruence. - inversion H0. + caseEq (transl_params params); simpl; intros; try congruence. + inv H0. rewrite (var_kind_by_value _ _ AM). rewrite (IHparams _ H). reflexivity. Qed. Lemma transl_fn_variables: forall params vars sg tparams tvars body, - transl_params params = Some tparams -> - transl_vars vars = Some tvars -> + transl_params params = OK tparams -> + transl_vars vars = OK tvars -> let f := Csharpminor.mkfunction sg tparams tvars body in - transl_vars (params ++ vars) = Some (fn_variables f). + transl_vars (params ++ vars) = OK (fn_variables f). Proof. intros. generalize (transl_params_vars _ _ H); intro. @@ -212,35 +177,36 @@ Qed. Lemma transl_expr_lvalue: forall ge e m1 a ty t m2 loc ofs ta, Csem.eval_lvalue ge e m1 (Expr a ty) t m2 loc ofs -> - transl_expr (Expr a ty) = Some ta -> - (exists id, a = Csyntax.Evar id /\ var_get id ty = Some ta) \/ - (exists tb, transl_lvalue (Expr a ty) = Some tb /\ - make_load tb ty = Some ta). + transl_expr (Expr a ty) = OK ta -> + (exists id, a = Csyntax.Evar id /\ var_get id ty = OK ta) \/ + (exists tb, transl_lvalue (Expr a ty) = OK tb /\ + make_load tb ty = OK ta). Proof. intros. inversion H; subst; clear H; simpl in H0. left; exists id; auto. left; exists id; auto. - monadInv H0. right. exists e0; split; auto. - simpl. monadInv H0. right. exists e2; split; auto. - simpl. rewrite H6 in H0. rewrite H6. - monadInv H0. right. - exists (make_binop Oadd e0 (make_intconst (Int.repr z))). split; auto. - simpl. rewrite H10 in H0. rewrite H10. - monadInv H0. right. - exists e0; auto. + monadInv H0. right. exists x; split; auto. + simpl. monadInv H0. right. exists x1; split; auto. + simpl. rewrite EQ; rewrite EQ1. simpl. auto. + rewrite H6 in H0. monadInv H0. right. + exists (Ebinop Oadd x (make_intconst (Int.repr x0))). split; auto. + simpl. rewrite H6. rewrite EQ. rewrite EQ1. auto. + rewrite H10 in H0. monadInv H0. right. + exists x; split; auto. + simpl. rewrite H10. auto. Qed. Lemma transl_stmt_Sfor_start: forall nbrk ncnt s1 e2 s3 s4 ts, - transl_statement nbrk ncnt (Sfor s1 e2 s3 s4) = Some ts -> + transl_statement nbrk ncnt (Sfor s1 e2 s3 s4) = OK ts -> exists ts1, exists ts2, ts = Sseq ts1 ts2 - /\ transl_statement nbrk ncnt s1 = Some ts1 - /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = Some (Sseq Sskip ts2). + /\ transl_statement nbrk ncnt s1 = OK ts1 + /\ transl_statement nbrk ncnt (Sfor Csyntax.Sskip e2 s3 s4) = OK (Sseq Sskip ts2). Proof. - intros. monadInv H. simpl. - exists s; exists (Sblock (Sloop (Sseq s0 (Sseq (Sblock s5) s2)))). - intuition. + intros. monadInv H. econstructor; econstructor. + split. reflexivity. split. auto. simpl. + rewrite EQ1; rewrite EQ0; rewrite EQ2; auto. Qed. (** Properties related to switch constructs *) diff --git a/cfrontend/Cshmgenproof2.v b/cfrontend/Cshmgenproof2.v index 0458bd5..8e2ce30 100644 --- a/cfrontend/Cshmgenproof2.v +++ b/cfrontend/Cshmgenproof2.v @@ -1,6 +1,7 @@ (** * Correctness of the C front end, part 2: Csharpminor construction functions *) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import Integers. Require Import Floats. @@ -12,6 +13,7 @@ Require Import Globalenvs. Require Import Csyntax. Require Import Csem. Require Import Ctyping. +Require Import Cminor. Require Import Csharpminor. Require Import Cshmgen. Require Import Cshmgenproof1. @@ -25,14 +27,14 @@ Variable tprog: Csharpminor.program. Lemma transl_lblstmts_exit: forall e m1 t m2 sl body n tsl nbrk ncnt, exec_stmt tprog e m1 body t m2 (Out_exit (lblstmts_length sl + n)) -> - transl_lblstmts nbrk ncnt sl body = Some tsl -> + transl_lblstmts nbrk ncnt sl body = OK tsl -> exec_stmt tprog e m1 tsl t m2 (outcome_block (Out_exit n)). Proof. induction sl; intros. simpl in H; simpl in H0; monadInv H0. - rewrite <- H2. constructor. apply exec_Sseq_stop. auto. congruence. + constructor. apply exec_Sseq_stop. auto. congruence. simpl in H; simpl in H0; monadInv H0. - eapply IHsl with (body := Sblock (Sseq body s0)); eauto. + eapply IHsl with (body := Sblock (Sseq body x)); eauto. change (Out_exit (lblstmts_length sl + n)) with (outcome_block (Out_exit (S (lblstmts_length sl + n)))). constructor. apply exec_Sseq_stop. auto. congruence. @@ -41,15 +43,15 @@ Qed. Lemma transl_lblstmts_return: forall e m1 t m2 sl body optv tsl nbrk ncnt, exec_stmt tprog e m1 body t m2 (Out_return optv) -> - transl_lblstmts nbrk ncnt sl body = Some tsl -> + transl_lblstmts nbrk ncnt sl body = OK tsl -> exec_stmt tprog e m1 tsl t m2 (Out_return optv). Proof. induction sl; intros. simpl in H; simpl in H0; monadInv H0. - rewrite <- H2. change (Out_return optv) with (outcome_block (Out_return optv)). + change (Out_return optv) with (outcome_block (Out_return optv)). constructor. apply exec_Sseq_stop. auto. congruence. simpl in H; simpl in H0; monadInv H0. - eapply IHsl with (body := Sblock (Sseq body s0)); eauto. + eapply IHsl with (body := Sblock (Sseq body x)); eauto. change (Out_return optv) with (outcome_block (Out_return optv)). constructor. apply exec_Sseq_stop. auto. congruence. Qed. @@ -61,41 +63,18 @@ Lemma make_intconst_correct: forall n le e m1, Csharpminor.eval_expr tprog le e m1 (make_intconst n) E0 m1 (Vint n). Proof. - intros. unfold make_intconst. econstructor. constructor. reflexivity. + intros. unfold make_intconst. econstructor. constructor. Qed. Lemma make_floatconst_correct: forall n le e m1, Csharpminor.eval_expr tprog le e m1 (make_floatconst n) E0 m1 (Vfloat n). Proof. - intros. unfold make_floatconst. econstructor. constructor. reflexivity. -Qed. - -Lemma make_unop_correct: - forall op le e m1 a ta m2 va v, - Csharpminor.eval_expr tprog le e m1 a ta m2 va -> - eval_operation op (va :: nil) m2 = Some v -> - Csharpminor.eval_expr tprog le e m1 (make_unop op a) ta m2 v. -Proof. - intros. unfold make_unop. econstructor. econstructor. eauto. constructor. - traceEq. auto. -Qed. - -Lemma make_binop_correct: - forall op le e m1 a ta m2 va b tb m3 vb t v, - Csharpminor.eval_expr tprog le e m1 a ta m2 va -> - Csharpminor.eval_expr tprog le e m2 b tb m3 vb -> - eval_operation op (va :: vb :: nil) m3 = Some v -> - t = ta ** tb -> - Csharpminor.eval_expr tprog le e m1 (make_binop op a b) t m3 v. -Proof. - intros. unfold make_binop. - econstructor. econstructor. eauto. econstructor. eauto. constructor. - reflexivity. traceEq. auto. + intros. unfold make_floatconst. econstructor. constructor. Qed. Hint Resolve make_intconst_correct make_floatconst_correct - make_unop_correct make_binop_correct: cshm. + eval_Eunop eval_Ebinop: cshm. Hint Extern 2 (@eq trace _ _) => traceEq: cshm. Remark Vtrue_is_true: Val.is_true Vtrue. @@ -120,7 +99,7 @@ Proof. destruct ty; simpl; try (exists v; intuition; inversion VTRUE; simpl; auto; fail). exists Vtrue; split. - eapply make_binop_correct; eauto with cshm. + econstructor; eauto with cshm. inversion VTRUE; simpl. replace (Float.cmp Cne f0 Float.zero) with (negb (Float.cmp Ceq f0 Float.zero)). rewrite Float.eq_zero_false. reflexivity. auto. @@ -140,7 +119,7 @@ Proof. destruct ty; simpl; try (exists v; intuition; inversion VFALSE; simpl; auto; fail). exists Vfalse; split. - eapply make_binop_correct; eauto with cshm. + econstructor; eauto with cshm. inversion VFALSE; simpl. replace (Float.cmp Cne Float.zero Float.zero) with (negb (Float.cmp Ceq Float.zero Float.zero)). rewrite Float.eq_zero_true. reflexivity. @@ -151,13 +130,13 @@ Qed. Lemma make_neg_correct: forall a tya c ta va v le e m1 m2, sem_neg va tya = Some v -> - make_neg a tya = Some c -> + make_neg a tya = OK c -> eval_expr tprog le e m1 a ta m2 va -> eval_expr tprog le e m1 c ta m2 v. Proof. intros until m2; intro SEM. unfold make_neg. functional inversion SEM; intros. - inversion H4. eapply make_binop_correct; eauto with cshm. + inversion H4. econstructor; eauto with cshm. inversion H4. eauto with cshm. Qed. @@ -186,21 +165,21 @@ Proof. Qed. Definition binary_constructor_correct - (make: expr -> type -> expr -> type -> option expr) + (make: expr -> type -> expr -> type -> res expr) (sem: val -> type -> val -> type -> option val): Prop := forall a tya b tyb c ta va tb vb v le e m1 m2 m3, sem va tya vb tyb = Some v -> - make a tya b tyb = Some c -> + make a tya b tyb = OK c -> eval_expr tprog le e m1 a ta m2 va -> eval_expr tprog le e m2 b tb m3 vb -> eval_expr tprog le e m1 c (ta ** tb) m3 v. Definition binary_constructor_correct' - (make: expr -> type -> expr -> type -> option expr) + (make: expr -> type -> expr -> type -> res expr) (sem: val -> val -> option val): Prop := forall a tya b tyb c ta va tb vb v le e m1 m2 m3, sem va vb = Some v -> - make a tya b tyb = Some c -> + make a tya b tyb = OK c -> eval_expr tprog le e m1 a ta m2 va -> eval_expr tprog le e m2 b tb m3 vb -> eval_expr tprog le e m1 c (ta ** tb) m3 v. @@ -212,8 +191,8 @@ Proof. inversion H7. eauto with cshm. inversion H7. eauto with cshm. inversion H7. - eapply make_binop_correct. eauto. - eapply make_binop_correct. eauto with cshm. eauto. + econstructor. eauto. + econstructor. eauto with cshm. eauto. simpl. reflexivity. reflexivity. simpl. reflexivity. traceEq. Qed. @@ -223,12 +202,12 @@ Proof. red; intros until m3. intro SEM. unfold make_sub. functional inversion SEM; rewrite H0; intros; inversion H7; eauto with cshm. - eapply make_binop_correct. eauto. - eapply make_binop_correct. eauto with cshm. eauto. + econstructor. eauto. + econstructor. eauto with cshm. eauto. simpl. reflexivity. reflexivity. simpl. reflexivity. traceEq. - inversion H9. eapply make_binop_correct. - eapply make_binop_correct; eauto. + inversion H9. econstructor. + econstructor; eauto. simpl. unfold eq_block; rewrite H3. reflexivity. eauto with cshm. simpl. rewrite H8. reflexivity. traceEq. Qed. @@ -244,9 +223,9 @@ Lemma make_div_correct: binary_constructor_correct make_div sem_div. Proof. red; intros until m3. intro SEM. unfold make_div. functional inversion SEM; rewrite H0; intros. - inversion H8. eapply make_binop_correct; eauto with cshm. + inversion H8. econstructor; eauto with cshm. simpl. rewrite H7; auto. - inversion H8. eapply make_binop_correct; eauto with cshm. + inversion H8. econstructor; eauto with cshm. simpl. rewrite H7; auto. inversion H7; eauto with cshm. Qed. @@ -254,9 +233,9 @@ Qed. Lemma make_mod_correct: binary_constructor_correct make_mod sem_mod. red; intros until m3. intro SEM. unfold make_mod. functional inversion SEM; rewrite H0; intros. - inversion H8. eapply make_binop_correct; eauto with cshm. + inversion H8. econstructor; eauto with cshm. simpl. rewrite H7; auto. - inversion H8. eapply make_binop_correct; eauto with cshm. + inversion H8. econstructor; eauto with cshm. simpl. rewrite H7; auto. Qed. @@ -285,7 +264,7 @@ Lemma make_shl_correct: binary_constructor_correct' make_shl sem_shl. Proof. red; intros until m3. intro SEM. unfold make_shl. functional inversion SEM. intros. inversion H5. - eapply make_binop_correct; eauto with cshm. + econstructor; eauto with cshm. simpl. rewrite H4. auto. Qed. @@ -293,16 +272,16 @@ Lemma make_shr_correct: binary_constructor_correct make_shr sem_shr. Proof. red; intros until m3. intro SEM. unfold make_shr. functional inversion SEM; intros; rewrite H0 in H8; inversion H8. - eapply make_binop_correct; eauto with cshm. + econstructor; eauto with cshm. simpl; rewrite H7; auto. - eapply make_binop_correct; eauto with cshm. + econstructor; eauto with cshm. simpl; rewrite H7; auto. Qed. Lemma make_cmp_correct: forall cmp a tya b tyb c ta va tb vb v le e m1 m2 m3, sem_cmp cmp va tya vb tyb m3 = Some v -> - make_cmp cmp a tya b tyb = Some c -> + make_cmp cmp a tya b tyb = OK c -> eval_expr tprog le e m1 a ta m2 va -> eval_expr tprog le e m2 b tb m3 vb -> eval_expr tprog le e m1 c (ta ** tb) m3 v. @@ -312,16 +291,16 @@ Proof. inversion H8. eauto with cshm. inversion H8. eauto with cshm. inversion H8. eauto with cshm. - inversion H9. eapply make_binop_correct; eauto with cshm. + inversion H9. econstructor; eauto with cshm. simpl. functional inversion H; subst; unfold eval_compare_null; rewrite H8; auto. - inversion H10. eapply make_binop_correct; eauto with cshm. + inversion H10. econstructor; eauto with cshm. simpl. rewrite H3. unfold eq_block; rewrite H9. auto. Qed. Lemma transl_unop_correct: forall op a tya c ta va v le e m1 m2, - transl_unop op a tya = Some c -> + transl_unop op a tya = OK c -> sem_unary_operation op va tya = Some v -> eval_expr tprog le e m1 a ta m2 va -> eval_expr tprog le e m1 c ta m2 v. @@ -334,7 +313,7 @@ Qed. Lemma transl_binop_correct: forall op a tya b tyb c ta va tb vb v le e m1 m2 m3, - transl_binop op a tya b tyb = Some c -> + transl_binop op a tya b tyb = OK c -> sem_binary_operation op va tya vb tyb m3 = Some v -> eval_expr tprog le e m1 a ta m2 va -> eval_expr tprog le e m2 b tb m3 vb -> @@ -365,7 +344,7 @@ Lemma make_cast_correct: cast v ty1 ty2 v' -> eval_expr tprog le e m1 (make_cast ty1 ty2 a) t m2 v'. Proof. - unfold make_cast, make_cast1, make_cast2, make_unop. + unfold make_cast, make_cast1, make_cast2. intros until v'; intros EVAL CAST. inversion CAST; clear CAST; subst. (* cast_int_int *) @@ -373,7 +352,7 @@ Proof. (* cast_float_int *) destruct sz2; destruct si2; repeat econstructor; eauto with cshm; simpl; auto. (* cast_int_float *) - destruct sz2; destruct si1; unfold make_floatofint, make_unop; repeat econstructor; eauto with cshm; simpl; auto. + destruct sz2; destruct si1; unfold make_floatofint; repeat econstructor; eauto with cshm; simpl; auto. (* cast_float_float *) destruct sz2; repeat econstructor; eauto with cshm. (* neutral, ptr *) @@ -384,7 +363,7 @@ Qed. Lemma make_load_correct: forall addr ty code b ofs v le e m1 t m2, - make_load addr ty = Some code -> + make_load addr ty = OK code -> eval_expr tprog le e m1 addr t m2 (Vptr b ofs) -> load_value_of_type ty m2 b ofs = Some v -> eval_expr tprog le e m1 code t m2 v. @@ -400,7 +379,7 @@ Qed. Lemma make_store_correct: forall addr ty rhs code e m1 t1 m2 b ofs t2 m3 v m4, - make_store addr ty rhs = Some code -> + make_store addr ty rhs = OK code -> eval_expr tprog nil e m1 addr t1 m2 (Vptr b ofs) -> eval_expr tprog nil e m2 rhs t2 m3 v -> store_value_of_type ty m3 b ofs v = Some m4 -> diff --git a/cfrontend/Cshmgenproof3.v b/cfrontend/Cshmgenproof3.v index 497286b..c8b9caf 100644 --- a/cfrontend/Cshmgenproof3.v +++ b/cfrontend/Cshmgenproof3.v @@ -1,6 +1,7 @@ (** * Correctness of the C front end, part 3: semantic preservation *) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import Integers. Require Import Floats. @@ -12,6 +13,7 @@ Require Import Globalenvs. Require Import Csyntax. Require Import Csem. Require Import Ctyping. +Require Import Cminor. Require Import Csharpminor. Require Import Cshmgen. Require Import Cshmgenproof1. @@ -22,40 +24,26 @@ Section CORRECTNESS. Variable prog: Csyntax.program. Variable tprog: Csharpminor.program. Hypothesis WTPROG: wt_program prog. -Hypothesis TRANSL: transl_program prog = Some tprog. +Hypothesis TRANSL: transl_program prog = OK tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Lemma symbols_preserved: forall s, Genv.find_symbol tge s = Genv.find_symbol ge s. -Proof. - intros. unfold ge, tge. - apply Genv.find_symbol_transf_partial2 with transl_fundef transl_globvar. - auto. -Qed. +Proof (Genv.find_symbol_transf_partial2 transl_fundef transl_globvar _ TRANSL). 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 = Some tf. -Proof. - intros. - generalize (Genv.find_funct_transf_partial2 transl_fundef transl_globvar TRANSL H). - intros [A B]. - destruct (transl_fundef f). exists f0; split. assumption. auto. congruence. -Qed. + 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). 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 = Some tf. -Proof. - intros. - generalize (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar TRANSL H). - intros [A B]. - destruct (transl_fundef f). exists f0; split. assumption. auto. congruence. -Qed. + 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). Lemma functions_well_typed: forall v f, @@ -119,7 +107,7 @@ Proof. Qed. Lemma match_var_kind_of_type: - forall ty vk, var_kind_of_type ty = Some vk -> match_var_kind ty vk. + forall ty vk, var_kind_of_type ty = OK vk -> match_var_kind ty vk. Proof. intros; red. caseEq (access_mode ty); auto. @@ -131,7 +119,7 @@ Lemma match_env_alloc_variables: Csem.alloc_variables e1 m1 vars e2 m2 lb -> forall tyenv te1 tvars, match_env tyenv e1 te1 -> - transl_vars vars = Some tvars -> + transl_vars vars = OK tvars -> exists te2, Csharpminor.alloc_variables te1 m1 tvars te2 m2 lb /\ match_env (Ctyping.add_vars tyenv vars) e2 te2. @@ -140,8 +128,8 @@ Proof. simpl in H0. inversion H0; subst; clear H0. exists te1; split. constructor. simpl. auto. generalize H2. simpl. - caseEq (var_kind_of_type ty); [intros vk VK | congruence]. - caseEq (transl_vars vars); [intros tvrs TVARS | congruence]. + caseEq (var_kind_of_type ty); simpl; [intros vk VK | congruence]. + 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). @@ -168,14 +156,14 @@ Lemma bind_parameters_match_rec: forall tyenv te tvars, (forall id ty, In (id, ty) vars -> tyenv!id = Some ty) -> match_env tyenv e te -> - transl_params vars = Some tvars -> + transl_params vars = OK tvars -> Csharpminor.bind_parameters te m1 tvars vals m2. Proof. induction 1; intros. simpl in H1. inversion H1. constructor. generalize H4; clear H4; simpl. - caseEq (chunk_of_type ty); [intros chunk CHK | congruence]. - caseEq (transl_params params); [intros tparams TPARAMS | congruence]. + caseEq (chunk_of_type ty); simpl; [intros chunk CHK | congruence]. + caseEq (transl_params params); simpl; [intros tparams TPARAMS | congruence]. intro EQ; inversion EQ; clear EQ; subst tvars. generalize CHK. unfold chunk_of_type. caseEq (access_mode ty); intros; try discriminate. @@ -215,7 +203,7 @@ Lemma bind_parameters_match: Csem.bind_parameters e m1 params vals m2 -> list_norepet (var_names params ++ var_names vars) -> match_env (Ctyping.add_vars tyenv (params ++ vars)) e te -> - transl_params params = Some tvars -> + transl_params params = OK tvars -> Csharpminor.bind_parameters te m1 tvars vals m2. Proof. intros. @@ -273,14 +261,14 @@ Qed. Lemma add_global_var_match_globalenv: forall vars tenv gv tvars, match_globalenv tenv gv -> - map_partial transl_globvar vars = Some tvars -> + map_partial AST.prefix_var_name transl_globvar vars = OK tvars -> match_globalenv (add_global_vars tenv vars) (globvarenv gv tvars). Proof. induction vars; simpl. intros. inversion H0. assumption. destruct a as [[id init] ty]. intros until tvars; intro. - caseEq (transl_globvar ty); try congruence. intros vk VK. - caseEq (map_partial transl_globvar vars); try congruence. intros tvars' EQ1 EQ2. + caseEq (transl_globvar ty); simpl; try congruence. intros vk VK. + caseEq (map_partial AST.prefix_var_name transl_globvar vars); simpl; try congruence. intros tvars' EQ1 EQ2. inversion EQ2; clear EQ2. simpl. apply IHvars; auto. red. intros until chunk. repeat rewrite PTree.gsspec. @@ -299,7 +287,7 @@ Proof. unfold global_typenv. apply add_global_var_match_globalenv. apply add_global_funs_match_global_env. - unfold transl_program in TRANSL. functional inversion TRANSL. auto. + unfold transl_program in TRANSL. monadInv TRANSL. auto. Qed. (** ** Variable accessors *) @@ -309,7 +297,7 @@ Lemma var_get_correct: Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) E0 m loc ofs -> load_value_of_type ty m loc ofs = Some v -> wt_expr tyenv (Expr (Csyntax.Evar id) ty) -> - var_get id ty = Some code -> + var_get id ty = OK code -> match_env tyenv e te -> eval_expr tprog le te m code E0 m v. Proof. @@ -356,7 +344,7 @@ Lemma var_set_correct: Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) t1 m1 loc ofs -> store_value_of_type ty m2 loc ofs v = Some m3 -> wt_expr tyenv (Expr (Csyntax.Evar id) ty) -> - var_set id ty rhs = Some code -> + var_set id ty rhs = OK code -> match_env tyenv e te -> eval_expr tprog nil te m1 rhs t2 m2 v -> exec_stmt tprog te m code (t1 ** t2) m3 Out_normal. @@ -394,7 +382,7 @@ Definition eval_expr_prop (e: Csem.env) (m1: mem) (a: Csyntax.expr) (t: trace) (m2: mem) (v: val) : Prop := forall tyenv ta te tle (WT: wt_expr tyenv a) - (TR: transl_expr a = Some ta) + (TR: transl_expr a = OK ta) (MENV: match_env tyenv e te), Csharpminor.eval_expr tprog tle te m1 ta t m2 v. @@ -403,7 +391,7 @@ Definition eval_lvalue_prop (m2: mem) (b: block) (ofs: int) : Prop := forall tyenv ta te tle (WT: wt_expr tyenv a) - (TR: transl_lvalue a = Some ta) + (TR: transl_lvalue a = OK ta) (MENV: match_env tyenv e te), Csharpminor.eval_expr tprog tle te m1 ta t m2 (Vptr b ofs). @@ -412,7 +400,7 @@ Definition eval_exprlist_prop (m2: mem) (vl: list val) : Prop := forall tyenv tal te tle (WT: wt_exprlist tyenv al) - (TR: transl_exprlist al = Some tal) + (TR: transl_exprlist al = OK tal) (MENV: match_env tyenv e te), Csharpminor.eval_exprlist tprog tle te m1 tal t m2 vl. @@ -429,7 +417,7 @@ Definition exec_stmt_prop (m2: mem) (out: Csem.outcome) : Prop := forall tyenv nbrk ncnt ts te (WT: wt_stmt tyenv s) - (TR: transl_statement nbrk ncnt s = Some ts) + (TR: transl_statement nbrk ncnt s = OK ts) (MENV: match_env tyenv e te), Csharpminor.exec_stmt tprog te m1 ts t m2 (transl_outcome nbrk ncnt out). @@ -440,7 +428,7 @@ Definition exec_lblstmts_prop (WT: wt_lblstmts tyenv s) (TR: transl_lblstmts (lblstmts_length s) (1 + lblstmts_length s + ncnt) - s body = Some ts) + s body = OK ts) (MENV: match_env tyenv e te) (BODY: Csharpminor.exec_stmt tprog te m0 body t0 m1 Out_normal), Csharpminor.exec_stmt tprog te m0 ts (t0 ** t) m2 @@ -451,7 +439,7 @@ Definition eval_funcall_prop (t: trace) (m2: mem) (res: val) : Prop := forall tf (WT: wt_fundef (global_typenv prog) f) - (TR: transl_fundef f = Some tf), + (TR: transl_fundef f = OK tf), Csharpminor.eval_funcall tprog m1 tf params t m2 res. (* @@ -465,7 +453,7 @@ Lemma transl_Econst_int_correct: eval_expr_prop e m (Expr (Econst_int i) ty) E0 m (Vint i)). Proof. intros; red; intros. - monadInv TR. subst ta. apply make_intconst_correct. + monadInv TR. apply make_intconst_correct. Qed. Lemma transl_Econst_float_correct: @@ -473,7 +461,7 @@ Lemma transl_Econst_float_correct: eval_expr_prop e m (Expr (Econst_float f0) ty) E0 m (Vfloat f0)). Proof. intros; red; intros. - monadInv TR. subst ta. apply make_floatconst_correct. + monadInv TR. apply make_floatconst_correct. Qed. Lemma transl_Elvalue_correct: @@ -512,16 +500,16 @@ Lemma transl_Esizeof_correct: eval_expr_prop e m (Expr (Esizeof ty') ty) E0 m (Vint (Int.repr (Csyntax.sizeof ty')))). Proof. - intros; red; intros. monadInv TR. subst ta. apply make_intconst_correct. + intros; red; intros. monadInv TR. apply make_intconst_correct. Qed. Lemma transl_Eunop_correct: - (forall (e : Csem.env) (m : mem) (op : unary_operation) + (forall (e : Csem.env) (m : mem) (op : Csyntax.unary_operation) (a : Csyntax.expr) (ty : type) (t : trace) (m1 : mem) (v1 v : val), Csem.eval_expr ge e m a t m1 v1 -> eval_expr_prop e m a t m1 v1 -> sem_unary_operation op v1 (typeof a) = Some v -> - eval_expr_prop e m (Expr (Eunop op a) ty) t m1 v). + eval_expr_prop e m (Expr (Csyntax.Eunop op a) ty) t m1 v). Proof. intros; red; intros. inversion WT; clear WT; subst. @@ -530,7 +518,7 @@ Proof. Qed. Lemma transl_Ebinop_correct: - (forall (e : Csem.env) (m : mem) (op : binary_operation) + (forall (e : Csem.env) (m : mem) (op : Csyntax.binary_operation) (a1 a2 : Csyntax.expr) (ty : type) (t1 : trace) (m1 : mem) (v1 : val) (t2 : trace) (m2 : mem) (v2 v : val), Csem.eval_expr ge e m a1 t1 m1 v1 -> @@ -538,7 +526,7 @@ Lemma transl_Ebinop_correct: Csem.eval_expr ge e m1 a2 t2 m2 v2 -> eval_expr_prop e m1 a2 t2 m2 v2 -> sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m2 = Some v -> - eval_expr_prop e m (Expr (Ebinop op a1 a2) ty) (t1 ** t2) m2 v). + eval_expr_prop e m (Expr (Csyntax.Ebinop op a1 a2) ty) (t1 ** t2) m2 v). Proof. intros; red; intros. inversion WT; clear WT; subst. @@ -555,7 +543,7 @@ Lemma transl_Eorbool_1_correct: eval_expr_prop e m (Expr (Eorbool a1 a2) ty) t m1 Vtrue). Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. - rewrite <- H3; unfold make_orbool. + unfold make_orbool. exploit make_boolean_correct_true; eauto. intros [vb [EVAL ISTRUE]]. eapply eval_Econdition_true; eauto. unfold Vtrue; apply make_intconst_correct. traceEq. @@ -574,7 +562,7 @@ Lemma transl_Eorbool_2_correct: eval_expr_prop e m (Expr (Eorbool a1 a2) ty) (t1 ** t2) m2 v). Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. - rewrite <- H6; unfold make_orbool. + unfold make_orbool. exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]]. eapply eval_Econdition_false; eauto. inversion H4; subst. @@ -595,7 +583,7 @@ Lemma transl_Eandbool_1_correct: eval_expr_prop e m (Expr (Eandbool a1 a2) ty) t m1 Vfalse). Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. - rewrite <- H3; unfold make_andbool. + unfold make_andbool. exploit make_boolean_correct_false; eauto. intros [vb [EVAL ISFALSE]]. eapply eval_Econdition_false; eauto. unfold Vfalse; apply make_intconst_correct. traceEq. @@ -614,7 +602,7 @@ Lemma transl_Eandbool_2_correct: eval_expr_prop e m (Expr (Eandbool a1 a2) ty) (t1 ** t2) m2 v). Proof. intros; red; intros. inversion WT; clear WT; subst. monadInv TR. - rewrite <- H6; unfold make_andbool. + unfold make_andbool. exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]]. eapply eval_Econdition_true; eauto. inversion H4; subst. @@ -634,7 +622,7 @@ Lemma transl_Ecast_correct: cast v1 (typeof a) ty v -> eval_expr_prop e m (Expr (Ecast ty a) ty) t m1 v). Proof. - intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta. + intros; red; intros. inversion WT; clear WT; subst. monadInv TR. eapply make_cast_correct; eauto. Qed. @@ -660,7 +648,7 @@ Proof. caseEq (classify_fun (typeof a)). 2: intros; rewrite H7 in TR; discriminate. intros targs tres EQ. rewrite EQ in TR. - monadInv TR. clear TR. subst ta. + monadInv TR. rewrite <- H4 in EQ. exploit functions_translated; eauto. intros [tf [FIND TRL]]. econstructor. @@ -679,7 +667,7 @@ Lemma transl_Evar_local_correct: e ! id = Some l -> eval_lvalue_prop e m (Expr (Csyntax.Evar id) ty) E0 m l Int.zero). Proof. - intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta. + intros; red; intros. inversion WT; clear WT; subst. monadInv TR. exploit (me_local _ _ _ MENV); eauto. intros [vk [A B]]. econstructor. eapply eval_var_addr_local. eauto. Qed. @@ -691,7 +679,7 @@ Lemma transl_Evar_global_correct: Genv.find_symbol ge id = Some l -> eval_lvalue_prop e m (Expr (Csyntax.Evar id) ty) E0 m l Int.zero). Proof. - intros; red; intros. inversion WT; clear WT; subst. monadInv TR. subst ta. + intros; red; intros. inversion WT; clear WT; subst. monadInv TR. exploit (me_global _ _ _ MENV); eauto. intros [A B]. econstructor. eapply eval_var_addr_global. eauto. rewrite symbols_preserved. auto. @@ -730,13 +718,13 @@ Lemma transl_Efield_struct_correct: eval_lvalue ge e m a t m1 l ofs -> eval_lvalue_prop e m a t m1 l ofs -> typeof a = Tstruct id fList -> - field_offset i fList = Some delta -> + field_offset i fList = OK delta -> eval_lvalue_prop e m (Expr (Efield a i) ty) t m1 l (Int.add ofs (Int.repr delta))). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR. rewrite H1 in TR. monadInv TR. - rewrite <- H5. eapply make_binop_correct; eauto. + econstructor; eauto. apply make_intconst_correct. simpl. congruence. traceEq. Qed. @@ -758,7 +746,7 @@ Lemma transl_Enil_correct: (forall (e : Csem.env) (m : mem), eval_exprlist_prop e m Csyntax.Enil E0 m nil). Proof. - intros; red; intros. monadInv TR. subst tal. constructor. + intros; red; intros. monadInv TR. constructor. Qed. Lemma transl_Econs_correct: @@ -772,14 +760,14 @@ Lemma transl_Econs_correct: eval_exprlist_prop e m (Csyntax.Econs a bl) (t1 ** t2) m2 (v :: vl)). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst tal. econstructor; eauto. + econstructor; eauto. Qed. Lemma transl_Sskip_correct: (forall (e : Csem.env) (m : mem), exec_stmt_prop e m Csyntax.Sskip E0 m Csem.Out_normal). Proof. - intros; red; intros. monadInv TR. subst ts. simpl. constructor. + intros; red; intros. monadInv TR. simpl. constructor. Qed. Lemma transl_Sexpr_correct: @@ -790,8 +778,7 @@ Lemma transl_Sexpr_correct: exec_stmt_prop e m (Csyntax.Sexpr a) t m1 Csem.Out_normal). Proof. intros; red; intros; simpl. inversion WT; clear WT; subst. - monadInv TR. subst ts. - econstructor; eauto. + monadInv TR. econstructor; eauto. Qed. Lemma transl_Sassign_correct: @@ -831,7 +818,7 @@ Lemma transl_Ssequence_1_correct: exec_stmt_prop e m (Ssequence s1 s2) (t1 ** t2) m2 out). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. red in H0; simpl in H0. eapply exec_Sseq_continue; eauto. + red in H0; simpl in H0. eapply exec_Sseq_continue; eauto. Qed. Lemma transl_Ssequence_2_correct: @@ -843,7 +830,7 @@ Lemma transl_Ssequence_2_correct: exec_stmt_prop e m (Ssequence s1 s2) t1 m1 out). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. eapply exec_Sseq_stop; eauto. + eapply exec_Sseq_stop; eauto. destruct out; simpl; congruence. Qed. @@ -860,7 +847,7 @@ Lemma transl_Sifthenelse_true_correct: Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]]. - subst ts. eapply exec_Sifthenelse_true; eauto. + eapply exec_Sifthenelse_true; eauto. Qed. Lemma transl_Sifthenelse_false_correct: @@ -876,7 +863,7 @@ Lemma transl_Sifthenelse_false_correct: Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]]. - subst ts. eapply exec_Sifthenelse_false; eauto. + eapply exec_Sifthenelse_false; eauto. Qed. Lemma transl_Sreturn_none_correct: @@ -884,7 +871,7 @@ Lemma transl_Sreturn_none_correct: exec_stmt_prop e m (Csyntax.Sreturn None) E0 m (Csem.Out_return None)). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. apply exec_Sreturn_none. + simpl. apply exec_Sreturn_none. Qed. Lemma transl_Sreturn_some_correct: @@ -896,7 +883,7 @@ Lemma transl_Sreturn_some_correct: (Csem.Out_return (Some v))). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. eapply exec_Sreturn_some; eauto. + simpl. eapply exec_Sreturn_some; eauto. Qed. Lemma transl_Sbreak_correct: @@ -904,7 +891,7 @@ Lemma transl_Sbreak_correct: exec_stmt_prop e m Sbreak E0 m Out_break). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. apply exec_Sexit. + simpl. apply exec_Sexit. Qed. Lemma transl_Scontinue_correct: @@ -912,19 +899,19 @@ Lemma transl_Scontinue_correct: exec_stmt_prop e m Scontinue E0 m Out_continue). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. apply exec_Sexit. + simpl. apply exec_Sexit. Qed. Lemma exit_if_false_true: forall a ts e m1 t m2 v tyenv te, - exit_if_false a = Some ts -> + exit_if_false a = OK ts -> eval_expr_prop e m1 a t m2 v -> match_env tyenv e te -> wt_expr tyenv a -> is_true v (typeof a) -> exec_stmt tprog te m1 ts t m2 Out_normal. Proof. - intros. monadInv H. rewrite <- H5. + intros. monadInv H. exploit make_boolean_correct_true. eapply H0; eauto. eauto. intros [vb [EVAL ISTRUE]]. eapply exec_Sifthenelse_true with (v1 := vb); eauto. @@ -933,14 +920,14 @@ Qed. Lemma exit_if_false_false: forall a ts e m1 t m2 v tyenv te, - exit_if_false a = Some ts -> + exit_if_false a = OK ts -> eval_expr_prop e m1 a t m2 v -> match_env tyenv e te -> wt_expr tyenv a -> is_false v (typeof a) -> exec_stmt tprog te m1 ts t m2 (Out_exit 0). Proof. - intros. monadInv H. rewrite <- H5. + intros. monadInv H. exploit make_boolean_correct_false. eapply H0; eauto. eauto. intros [vb [EVAL ISFALSE]]. eapply exec_Sifthenelse_false with (v1 := vb); eauto. @@ -956,7 +943,7 @@ Lemma transl_Swhile_false_correct: exec_stmt_prop e m (Swhile a s) t m1 Csem.Out_normal). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. + simpl. change Out_normal with (outcome_block (Out_exit 0)). apply exec_Sblock. apply exec_Sloop_stop. apply exec_Sseq_stop. eapply exit_if_false_false; eauto. congruence. congruence. @@ -992,7 +979,7 @@ Lemma transl_Swhile_stop_correct: exec_stmt_prop e m (Swhile a s) (t1 ** t2) m2 out). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. rewrite (transl_out_break_or_return _ _ nbrk ncnt H4). + rewrite (transl_out_break_or_return _ _ nbrk ncnt H4). apply exec_Sblock. apply exec_Sloop_stop. eapply exec_Sseq_continue. eapply exit_if_false_true; eauto. @@ -1017,7 +1004,6 @@ Proof. intros; red; intros. exploit H6; eauto. intro NEXTITER. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. inversion NEXTITER; subst. apply exec_Sblock. eapply exec_Sloop_loop. eapply exec_Sseq_continue. @@ -1041,7 +1027,7 @@ Lemma transl_Sdowhile_false_correct: exec_stmt_prop e m (Sdowhile a s) (t1 ** t2) m2 Csem.Out_normal). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. + simpl. change Out_normal with (outcome_block (Out_exit 0)). apply exec_Sblock. apply exec_Sloop_stop. eapply exec_Sseq_continue. rewrite (transl_out_normal_or_continue out1 H1). @@ -1058,7 +1044,7 @@ Lemma transl_Sdowhile_stop_correct: exec_stmt_prop e m (Sdowhile a s) t m1 out). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. + simpl. assert (outcome_block (transl_outcome 1 0 out1) <> Out_normal). inversion H1; simpl; congruence. rewrite (transl_out_break_or_return _ _ nbrk ncnt H1). @@ -1084,7 +1070,6 @@ Proof. intros; red; intros. exploit H6; eauto. intro NEXTITER. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. inversion NEXTITER; subst. apply exec_Sblock. eapply exec_Sloop_loop. eapply exec_Sseq_continue. @@ -1129,7 +1114,7 @@ Lemma transl_Sfor_false_correct: exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) t m1 Csem.Out_normal). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. + simpl. eapply exec_Sseq_continue. apply exec_Sskip. change Out_normal with (outcome_block (Out_exit 0)). apply exec_Sblock. apply exec_Sloop_stop. @@ -1150,7 +1135,7 @@ Lemma transl_Sfor_stop_correct: exec_stmt_prop e m (Sfor Csyntax.Sskip a2 a3 s) (t1 ** t2) m2 out). Proof. intros; red; intros. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. simpl. + simpl. assert (outcome_block (transl_outcome 1 0 out2) <> Out_normal). inversion H4; simpl; congruence. rewrite (transl_out_break_or_return _ _ nbrk ncnt H4). @@ -1181,7 +1166,6 @@ Proof. intros; red; intros. exploit H8; eauto. intro NEXTITER. inversion WT; clear WT; subst. simpl in TR; monadInv TR. - subst ts. inversion NEXTITER; subst. inversion H11; subst. inversion H18; subst. @@ -1205,7 +1189,7 @@ Lemma transl_lblstmts_switch: transl_lblstmts (lblstmts_length sl) (S (lblstmts_length sl + ncnt)) - sl (Sblock body) = Some ts -> + sl (Sblock body) = OK ts -> wt_lblstmts tyenv sl -> match_env tyenv e te -> exec_lblstmts_prop e m1 (select_switch n sl) t2 m2 out -> @@ -1226,7 +1210,7 @@ Proof. (* next case selected *) inversion H1; clear H1; subst. simpl in H0; monadInv H0. - eapply IHsl with (body := Sseq (Sblock body) s0); eauto. + eapply IHsl with (body := Sseq (Sblock body) x); eauto. apply exec_Sseq_stop. change (Out_exit (switch_target n (lblstmts_length sl) (switch_table sl 0))) with (outcome_block (Out_exit (S (switch_target n (lblstmts_length sl) (switch_table sl 0))))). @@ -1247,7 +1231,7 @@ Lemma transl_Sswitch_correct: Proof. intros; red; intros. inversion WT; clear WT; subst. - simpl in TR. monadInv TR; clear TR. + simpl in TR. monadInv TR. rewrite length_switch_table in EQ0. replace (ncnt + lblstmts_length sl + 1)%nat with (S (lblstmts_length sl + ncnt))%nat in EQ0 by omega. @@ -1265,7 +1249,6 @@ Proof. intros; red; intros. inversion WT; subst. simpl in TR. monadInv TR. - rewrite <- H3. replace (transl_outcome nbrk ncnt (outcome_switch out)) with (outcome_block (transl_outcome 0 (S ncnt) out)). constructor. @@ -1286,8 +1269,8 @@ Lemma transl_LScase_fallthrough_correct: Proof. intros; red; intros. inversion WT; subst. - simpl in TR. monadInv TR; clear TR. - assert (exec_stmt tprog te m0 (Sblock (Sseq body s0)) + monadInv TR. + assert (exec_stmt tprog te m0 (Sblock (Sseq body x)) (t0 ** t1) m1 Out_normal). change Out_normal with (outcome_block (transl_outcome (S (lblstmts_length ls)) @@ -1311,19 +1294,19 @@ Lemma transl_LScase_stop_correct: Proof. intros; red; intros. inversion WT; subst. - simpl in TR. monadInv TR; clear TR. + monadInv TR. exploit H0; eauto. intro EXEC. destruct out; simpl; simpl in EXEC. (* out = Out_break *) change Out_normal with (outcome_block (Out_exit 0)). - eapply transl_lblstmts_exit with (body := Sblock (Sseq body s0)); eauto. + eapply transl_lblstmts_exit with (body := Sblock (Sseq body x)); eauto. rewrite plus_0_r. change (Out_exit (lblstmts_length ls)) with (outcome_block (Out_exit (S (lblstmts_length ls)))). constructor. eapply exec_Sseq_continue; eauto. (* out = Out_continue *) change (Out_exit ncnt) with (outcome_block (Out_exit (S ncnt))). - eapply transl_lblstmts_exit with (body := Sblock (Sseq body s0)); eauto. + eapply transl_lblstmts_exit with (body := Sblock (Sseq body x)); eauto. replace (Out_exit (lblstmts_length ls + S ncnt)) with (outcome_block (Out_exit (S (S (lblstmts_length ls + ncnt))))). constructor. eapply exec_Sseq_continue; eauto. @@ -1331,7 +1314,7 @@ Proof. (* out = Out_normal *) congruence. (* out = Out_return *) - eapply transl_lblstmts_return with (body := Sblock (Sseq body s0)); eauto. + eapply transl_lblstmts_return with (body := Sblock (Sseq body x)); eauto. change (Out_return o) with (outcome_block (Out_return o)). constructor. eapply exec_Sseq_continue; eauto. @@ -1366,13 +1349,13 @@ Proof. inversion WT; clear WT; subst. inversion H6; clear H6; subst. (* Exploitation of translation hypothesis *) - monadInv TR. subst tf. clear TR. - monadInv EQ. clear EQ. subst f0. + monadInv TR. + monadInv EQ. (* Allocation of variables *) exploit match_env_alloc_variables; eauto. apply match_globalenv_match_env_empty. apply match_global_typenv. - eexact (transl_fn_variables _ _ (signature_of_function f) _ _ s EQ0 EQ1). + eexact (transl_fn_variables _ _ (signature_of_function f) _ _ x2 EQ0 EQ). intros [te [ALLOCVARS MATCHENV]]. (* Execution *) econstructor; simpl. @@ -1395,7 +1378,7 @@ Lemma transl_funcall_external_correct: eval_funcall_prop m (External id targs tres) vargs t m vres). Proof. intros; red; intros. - monadInv TR. subst tf. constructor. auto. + monadInv TR. constructor. auto. Qed. Theorem transl_funcall_correct: @@ -1467,7 +1450,7 @@ End CORRECTNESS. Theorem transl_program_correct: forall prog tprog t r, - transl_program prog = Some tprog -> + transl_program prog = OK tprog -> Ctyping.wt_program prog -> Csem.exec_program prog t r -> Csharpminor.exec_program tprog t r. diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v index f9463e6..6a5fcf3 100644 --- a/cfrontend/Csyntax.v +++ b/cfrontend/Csyntax.v @@ -1,6 +1,7 @@ (** * Abstract syntax for the Clight language *) Require Import Coqlib. +Require Import Errors. Require Import Integers. Require Import Floats. Require Import AST. @@ -251,17 +252,19 @@ Qed. (** Byte offset for a field in a struct. *) +Open Local Scope string_scope. + Fixpoint field_offset_rec (id: ident) (fld: fieldlist) (pos: Z) - {struct fld} : option Z := + {struct fld} : res Z := match fld with - | Fnil => None + | Fnil => Error (MSG "Unknown field " :: CTX id :: nil) | Fcons id' t fld' => if ident_eq id id' - then Some (align pos (alignof t)) + then OK (align pos (alignof t)) else field_offset_rec id fld' (align pos (alignof t) + sizeof t) end. -Definition field_offset (id: ident) (fld: fieldlist) : option Z := +Definition field_offset (id: ident) (fld: fieldlist) : res Z := field_offset_rec id fld 0. (* Describe how a variable of the given type must be accessed: -- cgit v1.2.3