Library Cshmgenproof3
Require Import Coqlib.
Require Import Errors.
Require Import Maps.
Require Import Integers.
Require Import Floats.
Require Import AST.
Require Import Values.
Require Import Events.
Require Import Mem.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Csyntax.
Require Import Csem.
Require Import Ctyping.
Require Import Cminor.
Require Import Csharpminor.
Require Import Cshmgen.
Require Import Cshmgenproof1.
Require Import Cshmgenproof2.
Section CORRECTNESS.
Variable prog: Csyntax.program.
Variable tprog: Csharpminor.program.
Hypothesis WTPROG: wt_program prog.
Hypothesis TRANSL: transl_program prog = OK tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.
Let tgvare : gvarenv := global_var_env tprog.
Let tgve := (tge, tgvare).
Lemma symbols_preserved:
forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.
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 = 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 = OK tf.
Proof (Genv.find_funct_ptr_transf_partial2 transl_fundef transl_globvar TRANSL).
Lemma functions_well_typed:
forall v f,
Genv.find_funct ge v = Some f ->
wt_fundef (global_typenv prog) f.
Lemma function_ptr_well_typed:
forall b f,
Genv.find_funct_ptr ge b = Some f ->
wt_fundef (global_typenv prog) f.
Lemma sig_translated:
forall fd tfd targs tres,
classify_fun (type_of_fundef fd) = fun_case_f targs tres ->
transl_fundef fd = OK tfd ->
funsig tfd = signature_of_type targs tres.
In this section, we define a matching relation between
a Clight local environment and a Csharpminor local environment,
parameterized by an assignment of types to the Clight variables.
Definition match_var_kind (ty: type) (vk: var_kind) : Prop :=
match access_mode ty with
| By_value chunk => vk = Vscalar chunk
| _ => True
end.
Record match_env (tyenv: typenv) (e: Csem.env) (te: Csharpminor.env) : Prop :=
mk_match_env {
me_local:
forall id b,
e!id = Some b ->
exists vk, exists ty,
tyenv!id = Some ty
/\ match_var_kind ty vk
/\ te!id = Some (b, vk);
me_local_inv:
forall id b vk,
te!id = Some (b, vk) -> e!id = Some b;
me_global:
forall id ty,
e!id = None -> tyenv!id = Some ty ->
te!id = None /\
(forall chunk, access_mode ty = By_value chunk -> (global_var_env tprog)!id = Some (Vscalar chunk))
}.
Lemma match_env_same_blocks:
forall tyenv e te,
match_env tyenv e te ->
forall b, In b (Csem.blocks_of_env e) <-> In b (blocks_of_env te).
Remark free_list_charact:
forall l m,
free_list m l =
mkmem (fun b => if In_dec eq_block b l then empty_block 0 0 else m.(blocks) b)
m.(nextblock)
m.(nextblock_pos).
Lemma mem_free_list_same:
forall m l1 l2,
(forall b, In b l1 <-> In b l2) ->
free_list m l1 = free_list m l2.
Lemma match_env_free_blocks:
forall tyenv e te m,
match_env tyenv e te ->
Mem.free_list m (Csem.blocks_of_env e) = Mem.free_list m (blocks_of_env te).
Definition match_globalenv (tyenv: typenv) (gv: gvarenv): Prop :=
forall id ty chunk,
tyenv!id = Some ty -> access_mode ty = By_value chunk ->
gv!id = Some (Vscalar chunk).
Lemma match_globalenv_match_env_empty:
forall tyenv,
match_globalenv tyenv (global_var_env tprog) ->
match_env tyenv Csem.empty_env Csharpminor.empty_env.
Lemma match_var_kind_of_type:
forall ty vk, var_kind_of_type ty = OK vk -> match_var_kind ty vk.
The following lemmas establish the
match_env invariant at
the beginning of a function invocation, after allocation of
local variables and initialization of the parameters.
Lemma match_env_alloc_variables:
forall e1 m1 vars e2 m2,
Csem.alloc_variables e1 m1 vars e2 m2 ->
forall tyenv te1 tvars,
match_env tyenv e1 te1 ->
transl_vars vars = OK tvars ->
exists te2,
Csharpminor.alloc_variables te1 m1 tvars te2 m2
/\ match_env (Ctyping.add_vars tyenv vars) e2 te2.
Lemma bind_parameters_match_rec:
forall e m1 vars vals m2,
Csem.bind_parameters e m1 vars vals m2 ->
forall tyenv te tvars,
(forall id ty, In (id, ty) vars -> tyenv!id = Some ty) ->
match_env tyenv e te ->
transl_params vars = OK tvars ->
Csharpminor.bind_parameters te m1 tvars vals m2.
Lemma tyenv_add_vars_norepet:
forall vars tyenv,
list_norepet (var_names vars) ->
(forall id ty,
In (id, ty) vars -> (Ctyping.add_vars tyenv vars)!id = Some ty)
/\
(forall id,
~In id (var_names vars) -> (Ctyping.add_vars tyenv vars)!id = tyenv!id).
Lemma bind_parameters_match:
forall e m1 params vals vars m2 tyenv tvars te,
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 = OK tvars ->
Csharpminor.bind_parameters te m1 tvars vals m2.
The following lemmas establish the matching property
between the global environments constructed at the beginning
of program execution.
Definition globvarenv
(gv: gvarenv)
(vars: list (ident * list init_data * var_kind)) :=
List.fold_left
(fun gve x => match x with (id, init, k) => PTree.set id k gve end)
vars gv.
Definition type_not_by_value (ty: type) : Prop :=
match access_mode ty with
| By_value _ => False
| _ => True
end.
Lemma add_global_funs_charact:
forall fns tyenv,
(forall id ty, tyenv!id = Some ty -> type_not_by_value ty) ->
(forall id ty, (add_global_funs tyenv fns)!id = Some ty -> type_not_by_value ty).
Definition global_fun_typenv :=
add_global_funs (PTree.empty type) prog.(prog_funct).
Lemma add_global_funs_match_global_env:
match_globalenv global_fun_typenv (PTree.empty var_kind).
Lemma add_global_var_match_globalenv:
forall vars tenv gv tvars,
match_globalenv tenv gv ->
map_partial AST.prefix_var_name transl_globvar vars = OK tvars ->
match_globalenv (add_global_vars tenv vars) (globvarenv gv tvars).
Lemma match_global_typenv:
match_globalenv (global_typenv prog) (global_var_env tprog).
Correctness of the code generated by
var_get.
Lemma var_get_correct:
forall e m id ty loc ofs v tyenv code te,
Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) loc ofs ->
load_value_of_type ty m loc ofs = Some v ->
wt_expr tyenv (Expr (Csyntax.Evar id) ty) ->
var_get id ty = OK code ->
match_env tyenv e te ->
eval_expr tgve te m code v.
Correctness of the code generated by
var_set.
Lemma var_set_correct:
forall e m id ty loc ofs v m' tyenv code te rhs f k,
Csem.eval_lvalue ge e m (Expr (Csyntax.Evar id) ty) loc ofs ->
store_value_of_type ty m loc ofs v = Some m' ->
wt_expr tyenv (Expr (Csyntax.Evar id) ty) ->
var_set id ty rhs = OK code ->
match_env tyenv e te ->
eval_expr tgve te m rhs v ->
step tgve (State f code k te m) E0 (State f Sskip k te m').
Lemma call_dest_correct:
forall e m lhs loc ofs tyenv optid te,
Csem.eval_lvalue ge e m lhs loc ofs ->
wt_expr tyenv lhs ->
transl_lhs_call (Some lhs) = OK optid ->
match_env tyenv e te ->
exists id,
optid = Some id
/\ tyenv!id = Some (typeof lhs)
/\ ofs = Int.zero
/\ match access_mode (typeof lhs) with
| By_value chunk => eval_var_ref tgve te id loc chunk
| _ => True
end.
Lemma set_call_dest_correct:
forall ty m loc v m' tyenv e te id,
store_value_of_type ty m loc Int.zero v = Some m' ->
match access_mode ty with
| By_value chunk => eval_var_ref tgve te id loc chunk
| _ => True
end ->
match_env tyenv e te ->
tyenv!id = Some ty ->
exec_opt_assign tgve te m (Some id) v m'.
The proof of semantic preservation for the translation of expressions
relies on simulation diagrams of the following form:
Left: evaluation of r-value expression
We state these diagrams as the following properties, parameterized by the Clight evaluation.
e, m, a ------------------- te, m, ta
| |
| |
| |
v v
e, m, v ------------------- te, m, v
Left: evaluation of r-value expression
a in Clight.
Right: evaluation of its translation ta in Csharpminor.
Top (precondition): matching between environments e, te,
plus well-typedness of expression a.
Bottom (postcondition): the result values v
are identical in both evaluations.
We state these diagrams as the following properties, parameterized by the Clight evaluation.
Section EXPR.
Variable e: Csem.env.
Variable m: mem.
Variable te: Csharpminor.env.
Variable tyenv: typenv.
Hypothesis MENV: match_env tyenv e te.
Definition eval_expr_prop (a: Csyntax.expr) (v: val) : Prop :=
forall ta
(WT: wt_expr tyenv a)
(TR: transl_expr a = OK ta),
Csharpminor.eval_expr tgve te m ta v.
Definition eval_lvalue_prop (a: Csyntax.expr) (b: block) (ofs: int) : Prop :=
forall ta
(WT: wt_expr tyenv a)
(TR: transl_lvalue a = OK ta),
Csharpminor.eval_expr tgve te m ta (Vptr b ofs).
Definition eval_exprlist_prop (al: list Csyntax.expr) (vl: list val) : Prop :=
forall tal
(WT: wt_exprlist tyenv al)
(TR: transl_exprlist al = OK tal),
Csharpminor.eval_exprlist tgve te m tal vl.
Lemma transl_Econst_int_correct:
forall (i : int) (ty : type),
eval_expr_prop (Expr (Econst_int i) ty) (Vint i).
Lemma transl_Econst_float_correct:
forall (f0 : float) (ty : type),
eval_expr_prop (Expr (Econst_float f0) ty) (Vfloat f0).
Lemma transl_Elvalue_correct:
forall (a : expr_descr) (ty : type) (loc : block) (ofs : int)
(v : val),
eval_lvalue ge e m (Expr a ty) loc ofs ->
eval_lvalue_prop (Expr a ty) loc ofs ->
load_value_of_type ty m loc ofs = Some v ->
eval_expr_prop (Expr a ty) v.
Lemma transl_Eaddrof_correct:
forall (a : Csyntax.expr) (ty : type) (loc : block) (ofs : int),
eval_lvalue ge e m a loc ofs ->
eval_lvalue_prop a loc ofs ->
eval_expr_prop (Expr (Csyntax.Eaddrof a) ty) (Vptr loc ofs).
Lemma transl_Esizeof_correct:
forall ty' ty : type,
eval_expr_prop (Expr (Esizeof ty') ty)
(Vint (Int.repr (Csyntax.sizeof ty'))).
Lemma transl_Eunop_correct:
forall (op : Csyntax.unary_operation) (a : Csyntax.expr) (ty : type)
(v1 v : val),
Csem.eval_expr ge e m a v1 ->
eval_expr_prop a v1 ->
sem_unary_operation op v1 (typeof a) = Some v ->
eval_expr_prop (Expr (Csyntax.Eunop op a) ty) v.
Lemma transl_Ebinop_correct:
forall (op : Csyntax.binary_operation) (a1 a2 : Csyntax.expr)
(ty : type) (v1 v2 v : val),
Csem.eval_expr ge e m a1 v1 ->
eval_expr_prop a1 v1 ->
Csem.eval_expr ge e m a2 v2 ->
eval_expr_prop a2 v2 ->
sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m = Some v ->
eval_expr_prop (Expr (Csyntax.Ebinop op a1 a2) ty) v.
Lemma transl_Econdition_true_correct:
forall (a1 a2 a3 : Csyntax.expr) (ty : type) (v1 v2 : val),
Csem.eval_expr ge e m a1 v1 ->
eval_expr_prop a1 v1 ->
is_true v1 (typeof a1) ->
Csem.eval_expr ge e m a2 v2 ->
eval_expr_prop a2 v2 ->
eval_expr_prop (Expr (Csyntax.Econdition a1 a2 a3) ty) v2.
Lemma transl_Econdition_false_correct:
forall (a1 a2 a3 : Csyntax.expr) (ty : type) (v1 v3 : val),
Csem.eval_expr ge e m a1 v1 ->
eval_expr_prop a1 v1 ->
is_false v1 (typeof a1) ->
Csem.eval_expr ge e m a3 v3 ->
eval_expr_prop a3 v3 ->
eval_expr_prop (Expr (Csyntax.Econdition a1 a2 a3) ty) v3.
Lemma transl_Eorbool_1_correct:
forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val),
Csem.eval_expr ge e m a1 v1 ->
eval_expr_prop a1 v1 ->
is_true v1 (typeof a1) ->
eval_expr_prop (Expr (Eorbool a1 a2) ty) Vtrue.
Lemma transl_Eorbool_2_correct:
forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 v : val),
Csem.eval_expr ge e m a1 v1 ->
eval_expr_prop a1 v1 ->
is_false v1 (typeof a1) ->
Csem.eval_expr ge e m a2 v2 ->
eval_expr_prop a2 v2 ->
bool_of_val v2 (typeof a2) v ->
eval_expr_prop (Expr (Eorbool a1 a2) ty) v.
Lemma transl_Eandbool_1_correct:
forall (a1 a2 : Csyntax.expr) (ty : type) (v1 : val),
Csem.eval_expr ge e m a1 v1 ->
eval_expr_prop a1 v1 ->
is_false v1 (typeof a1) ->
eval_expr_prop (Expr (Eandbool a1 a2) ty) Vfalse.
Lemma transl_Eandbool_2_correct:
forall (a1 a2 : Csyntax.expr) (ty : type) (v1 v2 v : val),
Csem.eval_expr ge e m a1 v1 ->
eval_expr_prop a1 v1 ->
is_true v1 (typeof a1) ->
Csem.eval_expr ge e m a2 v2 ->
eval_expr_prop a2 v2 ->
bool_of_val v2 (typeof a2) v ->
eval_expr_prop (Expr (Eandbool a1 a2) ty) v.
Lemma transl_Ecast_correct:
forall (a : Csyntax.expr) (ty ty': type) (v1 v : val),
Csem.eval_expr ge e m a v1 ->
eval_expr_prop a v1 ->
cast v1 (typeof a) ty v -> eval_expr_prop (Expr (Ecast ty a) ty') v.
Lemma transl_Evar_local_correct:
forall (id : ident) (l : block) (ty : type),
e ! id = Some l ->
eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero.
Lemma transl_Evar_global_correct:
forall (id : ident) (l : block) (ty : type),
e ! id = None ->
Genv.find_symbol ge id = Some l ->
eval_lvalue_prop (Expr (Csyntax.Evar id) ty) l Int.zero.
Lemma transl_Ederef_correct:
forall (a : Csyntax.expr) (ty : type) (l : block) (ofs : int),
Csem.eval_expr ge e m a (Vptr l ofs) ->
eval_expr_prop a (Vptr l ofs) ->
eval_lvalue_prop (Expr (Ederef a) ty) l ofs.
Lemma transl_Efield_struct_correct:
forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block)
(ofs : int) (id : ident) (fList : fieldlist) (delta : Z),
eval_lvalue ge e m a l ofs ->
eval_lvalue_prop a l ofs ->
typeof a = Tstruct id fList ->
field_offset i fList = OK delta ->
eval_lvalue_prop (Expr (Efield a i) ty) l (Int.add ofs (Int.repr delta)).
Lemma transl_Efield_union_correct:
forall (a : Csyntax.expr) (i : ident) (ty : type) (l : block)
(ofs : int) (id : ident) (fList : fieldlist),
eval_lvalue ge e m a l ofs ->
eval_lvalue_prop a l ofs ->
typeof a = Tunion id fList ->
eval_lvalue_prop (Expr (Efield a i) ty) l ofs.
Lemma transl_expr_correct:
forall a v,
Csem.eval_expr ge e m a v ->
eval_expr_prop a v.
Proof
(eval_expr_ind2 ge e m eval_expr_prop eval_lvalue_prop
transl_Econst_int_correct
transl_Econst_float_correct
transl_Elvalue_correct
transl_Eaddrof_correct
transl_Esizeof_correct
transl_Eunop_correct
transl_Ebinop_correct
transl_Econdition_true_correct
transl_Econdition_false_correct
transl_Eorbool_1_correct
transl_Eorbool_2_correct
transl_Eandbool_1_correct
transl_Eandbool_2_correct
transl_Ecast_correct
transl_Evar_local_correct
transl_Evar_global_correct
transl_Ederef_correct
transl_Efield_struct_correct
transl_Efield_union_correct).
Lemma transl_lvalue_correct:
forall a blk ofs,
Csem.eval_lvalue ge e m a blk ofs ->
eval_lvalue_prop a blk ofs.
Proof
(eval_lvalue_ind2 ge e m eval_expr_prop eval_lvalue_prop
transl_Econst_int_correct
transl_Econst_float_correct
transl_Elvalue_correct
transl_Eaddrof_correct
transl_Esizeof_correct
transl_Eunop_correct
transl_Ebinop_correct
transl_Econdition_true_correct
transl_Econdition_false_correct
transl_Eorbool_1_correct
transl_Eorbool_2_correct
transl_Eandbool_1_correct
transl_Eandbool_2_correct
transl_Ecast_correct
transl_Evar_local_correct
transl_Evar_global_correct
transl_Ederef_correct
transl_Efield_struct_correct
transl_Efield_union_correct).
Lemma transl_exprlist_correct:
forall al vl,
Csem.eval_exprlist ge e m al vl ->
eval_exprlist_prop al vl.
End EXPR.
Lemma exit_if_false_true:
forall a ts e m v tyenv te f tk,
exit_if_false a = OK ts ->
Csem.eval_expr ge e m a v ->
is_true v (typeof a) ->
match_env tyenv e te ->
wt_expr tyenv a ->
step tgve (State f ts tk te m) E0 (State f Sskip tk te m).
Lemma exit_if_false_false:
forall a ts e m v tyenv te f tk,
exit_if_false a = OK ts ->
Csem.eval_expr ge e m a v ->
is_false v (typeof a) ->
match_env tyenv e te ->
wt_expr tyenv a ->
step tgve (State f ts tk te m) E0 (State f (Sexit 0) tk te m).
The simulation diagram for the translation of statements and functions
is a "plus" diagram of the form
The invariant
I
S1 ------- R1
| |
t | + | t
v v
S2 ------- R2
I I
The invariant
I is the match_states predicate that we now define.
Definition typenv_fun (f: Csyntax.function) :=
add_vars (global_typenv prog) (f.(Csyntax.fn_params) ++ f.(Csyntax.fn_vars)).
Inductive match_transl: stmt -> cont -> stmt -> cont -> Prop :=
| match_transl_0: forall ts tk,
match_transl ts tk ts tk
| match_transl_1: forall ts tk,
match_transl (Sblock ts) tk ts (Kblock tk).
Lemma match_transl_step:
forall ts tk ts' tk' f te m,
match_transl (Sblock ts) tk ts' tk' ->
star step tgve (State f ts' tk' te m) E0 (State f ts (Kblock tk) te m).
Inductive match_cont: typenv -> nat -> nat -> Csem.cont -> Csharpminor.cont -> Prop :=
| match_Kstop: forall tyenv nbrk ncnt,
match_cont tyenv nbrk ncnt Csem.Kstop Kstop
| match_Kseq: forall tyenv nbrk ncnt s k ts tk,
transl_statement nbrk ncnt s = OK ts ->
wt_stmt tyenv s ->
match_cont tyenv nbrk ncnt k tk ->
match_cont tyenv nbrk ncnt
(Csem.Kseq s k)
(Kseq ts tk)
| match_Kwhile: forall tyenv nbrk ncnt a s k ta ts tk,
exit_if_false a = OK ta ->
transl_statement 1%nat 0%nat s = OK ts ->
wt_expr tyenv a ->
wt_stmt tyenv s ->
match_cont tyenv nbrk ncnt k tk ->
match_cont tyenv 1%nat 0%nat
(Csem.Kwhile a s k)
(Kblock (Kseq (Sloop (Sseq ta (Sblock ts))) (Kblock tk)))
| match_Kdowhile: forall tyenv nbrk ncnt a s k ta ts tk,
exit_if_false a = OK ta ->
transl_statement 1%nat 0%nat s = OK ts ->
wt_expr tyenv a ->
wt_stmt tyenv s ->
match_cont tyenv nbrk ncnt k tk ->
match_cont tyenv 1%nat 0%nat
(Csem.Kdowhile a s k)
(Kblock (Kseq ta (Kseq (Sloop (Sseq (Sblock ts) ta)) (Kblock tk))))
| match_Kfor2: forall tyenv nbrk ncnt a2 a3 s k ta2 ta3 ts tk,
exit_if_false a2 = OK ta2 ->
transl_statement nbrk ncnt a3 = OK ta3 ->
transl_statement 1%nat 0%nat s = OK ts ->
wt_expr tyenv a2 -> wt_stmt tyenv a3 -> wt_stmt tyenv s ->
match_cont tyenv nbrk ncnt k tk ->
match_cont tyenv 1%nat 0%nat
(Csem.Kfor2 a2 a3 s k)
(Kblock (Kseq ta3 (Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk))))
| match_Kfor3: forall tyenv nbrk ncnt a2 a3 s k ta2 ta3 ts tk,
exit_if_false a2 = OK ta2 ->
transl_statement nbrk ncnt a3 = OK ta3 ->
transl_statement 1%nat 0%nat s = OK ts ->
wt_expr tyenv a2 -> wt_stmt tyenv a3 -> wt_stmt tyenv s ->
match_cont tyenv nbrk ncnt k tk ->
match_cont tyenv nbrk ncnt
(Csem.Kfor3 a2 a3 s k)
(Kseq (Sloop (Sseq ta2 (Sseq (Sblock ts) ta3))) (Kblock tk))
| match_Kswitch: forall tyenv nbrk ncnt k tk,
match_cont tyenv nbrk ncnt k tk ->
match_cont tyenv 0%nat (S ncnt)
(Csem.Kswitch k)
(Kblock tk)
| match_Kcall_none: forall tyenv nbrk ncnt nbrk' ncnt' f e k tf te tk,
transl_function f = OK tf ->
wt_stmt (typenv_fun f) f.(Csyntax.fn_body) ->
match_env (typenv_fun f) e te ->
match_cont (typenv_fun f) nbrk' ncnt' k tk ->
match_cont tyenv nbrk ncnt
(Csem.Kcall None f e k)
(Kcall None tf te tk)
| match_Kcall_some: forall tyenv nbrk ncnt nbrk' ncnt' loc ofs ty f e k id tf te tk,
transl_function f = OK tf ->
wt_stmt (typenv_fun f) f.(Csyntax.fn_body) ->
match_env (typenv_fun f) e te ->
ofs = Int.zero ->
(typenv_fun f)!id = Some ty ->
match access_mode ty with
| By_value chunk => eval_var_ref tgve te id loc chunk
| _ => True
end ->
match_cont (typenv_fun f) nbrk' ncnt' k tk ->
match_cont tyenv nbrk ncnt
(Csem.Kcall (Some(loc, ofs, ty)) f e k)
(Kcall (Some id) tf te tk).
Inductive match_states: Csem.state -> Csharpminor.state -> Prop :=
| match_state:
forall f nbrk ncnt s k e m tf ts tk te ts' tk'
(TRF: transl_function f = OK tf)
(TR: transl_statement nbrk ncnt s = OK ts)
(MTR: match_transl ts tk ts' tk')
(WTF: wt_stmt (typenv_fun f) f.(Csyntax.fn_body))
(WT: wt_stmt (typenv_fun f) s)
(MENV: match_env (typenv_fun f) e te)
(MK: match_cont (typenv_fun f) nbrk ncnt k tk),
match_states (Csem.State f s k e m)
(State tf ts' tk' te m)
| match_callstate:
forall fd args k m tfd tk
(TR: transl_fundef fd = OK tfd)
(WT: wt_fundef (global_typenv prog) fd)
(MK: match_cont (global_typenv prog) 0%nat 0%nat k tk)
(ISCC: Csem.is_call_cont k),
match_states (Csem.Callstate fd args k m)
(Callstate tfd args tk m)
| match_returnstate:
forall res k m tk
(MK: match_cont (global_typenv prog) 0%nat 0%nat k tk),
match_states (Csem.Returnstate res k m)
(Returnstate res tk m).
Remark match_states_skip:
forall f e te nbrk ncnt k tf tk m,
transl_function f = OK tf ->
wt_stmt (typenv_fun f) f.(Csyntax.fn_body) ->
match_env (typenv_fun f) e te ->
match_cont (typenv_fun f) nbrk ncnt k tk ->
match_states (Csem.State f Csyntax.Sskip k e m) (State tf Sskip tk te m).
Commutation between label resolution and compilation
Section FIND_LABEL.
Variable lbl: label.
Variable tyenv: typenv.
Remark exit_if_false_no_label:
forall a s, exit_if_false a = OK s -> forall k, find_label lbl s k = None.
Lemma transl_find_label:
forall s nbrk ncnt k ts tk
(WT: wt_stmt tyenv s)
(TR: transl_statement nbrk ncnt s = OK ts)
(MC: match_cont tyenv nbrk ncnt k tk),
match Csem.find_label lbl s k with
| None => find_label lbl ts tk = None
| Some (s', k') =>
exists ts', exists tk', exists nbrk', exists ncnt',
find_label lbl ts tk = Some (ts', tk')
/\ transl_statement nbrk' ncnt' s' = OK ts'
/\ match_cont tyenv nbrk' ncnt' k' tk'
/\ wt_stmt tyenv s'
end
with transl_find_label_ls:
forall ls nbrk ncnt k tls tk
(WT: wt_lblstmts tyenv ls)
(TR: transl_lbl_stmt nbrk ncnt ls = OK tls)
(MC: match_cont tyenv nbrk ncnt k tk),
match Csem.find_label_ls lbl ls k with
| None => find_label_ls lbl tls tk = None
| Some (s', k') =>
exists ts', exists tk', exists nbrk', exists ncnt',
find_label_ls lbl tls tk = Some (ts', tk')
/\ transl_statement nbrk' ncnt' s' = OK ts'
/\ match_cont tyenv nbrk' ncnt' k' tk'
/\ wt_stmt tyenv s'
end.
End FIND_LABEL.
Properties of call continuations
Lemma match_cont_call_cont:
forall nbrk' ncnt' tyenv' tyenv nbrk ncnt k tk,
match_cont tyenv nbrk ncnt k tk ->
match_cont tyenv' nbrk' ncnt' (Csem.call_cont k) (call_cont tk).
Lemma match_cont_is_call_cont:
forall typenv nbrk ncnt k tk typenv' nbrk' ncnt',
match_cont typenv nbrk ncnt k tk ->
Csem.is_call_cont k ->
match_cont typenv' nbrk' ncnt' k tk /\ is_call_cont tk.
The simulation proof
Lemma transl_step:
forall S1 t S2, Csem.step ge S1 t S2 ->
forall T1, match_states S1 T1 ->
exists T2, plus step tgve T1 t T2 /\ match_states S2 T2.
Lemma transl_initial_states:
forall S t S', Csem.initial_state prog S -> Csem.step ge S t S' ->
exists R, initial_state tprog R /\ match_states S R.
Lemma transl_final_states:
forall S R r,
match_states S R -> Csem.final_state S r -> final_state R r.
Theorem transl_program_correct:
forall (beh: program_behavior),
not_wrong beh -> Csem.exec_program prog beh ->
Csharpminor.exec_program tprog beh.
End CORRECTNESS.