summaryrefslogtreecommitdiff
path: root/cfrontend
diff options
context:
space:
mode:
authorGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-08-04 07:27:50 +0000
committerGravatar xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>2007-08-04 07:27:50 +0000
commit355b4abcee015c3fae9ac5653c25259e104a886c (patch)
treecfdb5b17f36b815bb358699cf420f64eba9dfe25 /cfrontend
parent22ff08b38616ceef336f5f974d4edc4d37d955e8 (diff)
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
Diffstat (limited to 'cfrontend')
-rw-r--r--cfrontend/Cminorgen.v221
-rw-r--r--cfrontend/Cminorgenproof.v694
-rw-r--r--cfrontend/Csem.v3
-rw-r--r--cfrontend/Csharpminor.v150
-rw-r--r--cfrontend/Cshmgen.v276
-rw-r--r--cfrontend/Cshmgenproof1.v134
-rw-r--r--cfrontend/Cshmgenproof2.v103
-rw-r--r--cfrontend/Cshmgenproof3.v179
-rw-r--r--cfrontend/Csyntax.v11
9 files changed, 755 insertions, 1016 deletions
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: