Require Import Coqlib Maps Errors Integers Floats .
Require Import AST Linking Memory .
Require Import Ctypes Cop Csyntax Clight SimplExpr .

Section SPEC .

Variable ce : composite_env .

Local Open Scope gensym_monad_scope.

Relational specification of the translation.

Translation of expressions

Definition final (dst: destination ) (a: expr ) : list statement :=
match dst with
| For_val => nil
| For_effects => nil
| For_set sd => do_set sd a
end.

Definition tr_is_bitfield_access (l: expr ) (bf: bitfield ) : Prop :=
match l with
| Efield r f _ =>
exists co ofs,
match typeof r with
| Tstruct id _ =>
ce !id = Some co /\ field_offset ce f (co_members co) = OK (ofs, bf)
| Tunion id _ =>
ce !id = Some co /\ union_field_offset ce f (co_members co) = OK (ofs, bf)
| _ => False
end
| _ => bf = Full
end.

Inductive tr_rvalof : type -> expr -> list statement -> expr -> list ident -> Prop :=
| tr_rvalof_nonvol : forall ty a tmp,
type_is_volatile ty = false ->
tr_rvalof ty a nil a tmp
| tr_rvalof_vol : forall ty a t bf tmp,
type_is_volatile ty = true -> In t tmp ->
tr_is_bitfield_access a bf ->
tr_rvalof ty a (make_set bf t a :: nil ) (Etempvar t ty) tmp.

Inductive tr_expr : temp_env -> destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop :=
| tr_var : forall le dst id ty tmp,
tr_expr le dst (Csyntax.Evar id ty)
(final dst (Evar id ty)) (Evar id ty) tmp
| tr_deref : forall le dst e1 ty sl1 a1 tmp,
tr_expr le For_val e1 sl1 a1 tmp ->
tr_expr le dst (Csyntax.Ederef e1 ty)
(sl1 ++ final dst (Ederef' a1 ty)) (Ederef' a1 ty) tmp
| tr_field : forall le dst e1 f ty sl1 a1 tmp,
tr_expr le For_val e1 sl1 a1 tmp ->
tr_expr le dst (Csyntax.Efield e1 f ty)
(sl1 ++ final dst (Efield a1 f ty)) (Efield a1 f ty) tmp
| tr_val_effect : forall le v ty any tmp,
tr_expr le For_effects (Csyntax.Eval v ty) nil any tmp
| tr_val_value : forall le v ty a tmp,
typeof a = ty ->
(forall tge e le' m,
(forall id, In id tmp -> le'!id = le!id) ->
eval_expr tge e le' m a v) ->
tr_expr le For_val (Csyntax.Eval v ty)
nil a tmp
| tr_val_set : forall le sd v ty a any tmp,
typeof a = ty ->
(forall tge e le' m,
(forall id, In id tmp -> le'!id = le!id) ->
eval_expr tge e le' m a v) ->
tr_expr le (For_set sd) (Csyntax.Eval v ty)
(do_set sd a) any tmp
| tr_sizeof : forall le dst ty' ty tmp,
tr_expr le dst (Csyntax.Esizeof ty' ty)
(final dst (Esizeof ty' ty))
(Esizeof ty' ty) tmp
| tr_alignof : forall le dst ty' ty tmp,
tr_expr le dst (Csyntax.Ealignof ty' ty)
(final dst (Ealignof ty' ty))
(Ealignof ty' ty) tmp
| tr_valof : forall le dst e1 ty tmp sl1 a1 tmp1 sl2 a2 tmp2,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_rvalof (Csyntax.typeof e1) a1 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp ->
tr_expr le dst (Csyntax.Evalof e1 ty)
(sl1 ++ sl2 ++ final dst a2)
a2 tmp
| tr_addrof : forall le dst e1 ty tmp sl1 a1,
tr_expr le For_val e1 sl1 a1 tmp ->
tr_expr le dst (Csyntax.Eaddrof e1 ty)
(sl1 ++ final dst (Eaddrof' a1 ty))
(Eaddrof' a1 ty) tmp
| tr_unop : forall le dst op e1 ty tmp sl1 a1,
tr_expr le For_val e1 sl1 a1 tmp ->
tr_expr le dst (Csyntax.Eunop op e1 ty)
(sl1 ++ final dst (Eunop op a1 ty))
(Eunop op a1 ty) tmp
| tr_binop : forall le dst op e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le For_val e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 -> incl tmp1 tmp -> incl tmp2 tmp ->
tr_expr le dst (Csyntax.Ebinop op e1 e2 ty)
(sl1 ++ sl2 ++ final dst (Ebinop op a1 a2 ty))
(Ebinop op a1 a2 ty) tmp
| tr_cast_effects : forall le e1 ty sl1 a1 any tmp,
tr_expr le For_effects e1 sl1 a1 tmp ->
tr_expr le For_effects (Csyntax.Ecast e1 ty)
sl1
any tmp
| tr_cast_val : forall le dst e1 ty sl1 a1 tmp,
tr_expr le For_val e1 sl1 a1 tmp ->
tr_expr le dst (Csyntax.Ecast e1 ty)
(sl1 ++ final dst (Ecast a1 ty))
(Ecast a1 ty) tmp
| tr_seqand_val : forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le (For_set (SDbase type_bool ty t)) e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
tr_expr le For_val (Csyntax.Eseqand e1 e2 ty)
(sl1 ++ makeif a1 (makeseq sl2)
(Sset t (Econst_int Int.zero ty)) :: nil )
(Etempvar t ty) tmp
| tr_seqand_effects : forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le For_effects e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp ->
tr_expr le For_effects (Csyntax.Eseqand e1 e2 ty)
(sl1 ++ makeif a1 (makeseq sl2) Sskip :: nil )
any tmp
| tr_seqand_set : forall le sd e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le (For_set (SDcons type_bool ty t sd)) e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
tr_expr le (For_set sd) (Csyntax.Eseqand e1 e2 ty)
(sl1 ++ makeif a1 (makeseq sl2)
(makeseq (do_set sd (Econst_int Int.zero ty))) :: nil )
any tmp
| tr_seqor_val : forall le e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le (For_set (SDbase type_bool ty t)) e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
tr_expr le For_val (Csyntax.Eseqor e1 e2 ty)
(sl1 ++ makeif a1 (Sset t (Econst_int Int.one ty))
(makeseq sl2) :: nil )
(Etempvar t ty) tmp
| tr_seqor_effects : forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le For_effects e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp ->
tr_expr le For_effects (Csyntax.Eseqor e1 e2 ty)
(sl1 ++ makeif a1 Sskip (makeseq sl2) :: nil )
any tmp
| tr_seqor_set : forall le sd e1 e2 ty sl1 a1 tmp1 t sl2 a2 tmp2 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le (For_set (SDcons type_bool ty t sd)) e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp -> In t tmp ->
tr_expr le (For_set sd) (Csyntax.Eseqor e1 e2 ty)
(sl1 ++ makeif a1 (makeseq (do_set sd (Econst_int Int.one ty)))
(makeseq sl2) :: nil )
any tmp
| tr_condition_val : forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le (For_set (SDbase ty ty t)) e2 sl2 a2 tmp2 ->
tr_expr le (For_set (SDbase ty ty t)) e3 sl3 a3 tmp3 ->
list_disjoint tmp1 tmp2 ->
list_disjoint tmp1 tmp3 ->
incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp ->
tr_expr le For_val (Csyntax.Econdition e1 e2 e3 ty)
(sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil )
(Etempvar t ty) tmp
| tr_condition_effects : forall le e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le For_effects e2 sl2 a2 tmp2 ->
tr_expr le For_effects e3 sl3 a3 tmp3 ->
list_disjoint tmp1 tmp2 ->
list_disjoint tmp1 tmp3 ->
incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
tr_expr le For_effects (Csyntax.Econdition e1 e2 e3 ty)
(sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil )
any tmp
| tr_condition_set : forall le sd t e1 e2 e3 ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le (For_set (SDcons ty ty t sd)) e2 sl2 a2 tmp2 ->
tr_expr le (For_set (SDcons ty ty t sd)) e3 sl3 a3 tmp3 ->
list_disjoint tmp1 tmp2 ->
list_disjoint tmp1 tmp3 ->
incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp -> In t tmp ->
tr_expr le (For_set sd) (Csyntax.Econdition e1 e2 e3 ty)
(sl1 ++ makeif a1 (makeseq sl2) (makeseq sl3) :: nil )
any tmp
| tr_assign_effects : forall le e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 bf any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le For_val e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp ->
tr_is_bitfield_access a1 bf ->
tr_expr le For_effects (Csyntax.Eassign e1 e2 ty)
(sl1 ++ sl2 ++ make_assign bf a1 a2 :: nil )
any tmp
| tr_assign_val : forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 t tmp ty1 ty2 bf,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le For_val e2 sl2 a2 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp ->
list_disjoint tmp1 tmp2 ->
In t tmp -> ~In t tmp1 -> ~In t tmp2 ->
ty1 = Csyntax.typeof e1 ->
ty2 = Csyntax.typeof e2 ->
tr_is_bitfield_access a1 bf ->
tr_expr le dst (Csyntax.Eassign e1 e2 ty)
(sl1 ++ sl2 ++
Sset t (Ecast a2 ty1) ::
make_assign bf a1 (Etempvar t ty1) ::
final dst (make_assign_value bf (Etempvar t ty1)))
(make_assign_value bf (Etempvar t ty1)) tmp
| tr_assignop_effects : forall le op e1 e2 tyres ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 bf sl3 a3 tmp3 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le For_val e2 sl2 a2 tmp2 ->
ty1 = Csyntax.typeof e1 ->
tr_rvalof ty1 a1 sl3 a3 tmp3 ->
list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 ->
incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
tr_is_bitfield_access a1 bf ->
tr_expr le For_effects (Csyntax.Eassignop op e1 e2 tyres ty)
(sl1 ++ sl2 ++ sl3 ++ make_assign bf a1 (Ebinop op a3 a2 tyres) :: nil )
any tmp
| tr_assignop_val : forall le dst op e1 e2 tyres ty sl1 a1 tmp1 sl2 a2 tmp2 sl3 a3 tmp3 t bf tmp ty1,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_expr le For_val e2 sl2 a2 tmp2 ->
tr_rvalof ty1 a1 sl3 a3 tmp3 ->
list_disjoint tmp1 tmp2 -> list_disjoint tmp1 tmp3 -> list_disjoint tmp2 tmp3 ->
incl tmp1 tmp -> incl tmp2 tmp -> incl tmp3 tmp ->
In t tmp -> ~In t tmp1 -> ~In t tmp2 -> ~In t tmp3 ->
ty1 = Csyntax.typeof e1 ->
tr_is_bitfield_access a1 bf ->
tr_expr le dst (Csyntax.Eassignop op e1 e2 tyres ty)
(sl1 ++ sl2 ++ sl3 ++
Sset t (Ecast (Ebinop op a3 a2 tyres) ty1) ::
make_assign bf a1 (Etempvar t ty1) ::
final dst (make_assign_value bf (Etempvar t ty1)))
(make_assign_value bf (Etempvar t ty1)) tmp
| tr_postincr_effects : forall le id e1 ty ty1 sl1 a1 tmp1 sl2 a2 tmp2 bf any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_rvalof ty1 a1 sl2 a2 tmp2 ->
ty1 = Csyntax.typeof e1 ->
incl tmp1 tmp -> incl tmp2 tmp ->
list_disjoint tmp1 tmp2 ->
tr_is_bitfield_access a1 bf ->
tr_expr le For_effects (Csyntax.Epostincr id e1 ty)
(sl1 ++ sl2 ++ make_assign bf a1 (transl_incrdecr id a2 ty1) :: nil )
any tmp
| tr_postincr_val : forall le dst id e1 ty sl1 a1 tmp1 bf t ty1 tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
incl tmp1 tmp -> In t tmp -> ~In t tmp1 ->
ty1 = Csyntax.typeof e1 ->
tr_is_bitfield_access a1 bf ->
tr_expr le dst (Csyntax.Epostincr id e1 ty)
(sl1 ++ make_set bf t a1 ::
make_assign bf a1 (transl_incrdecr id (Etempvar t ty1) ty1) ::
final dst (Etempvar t ty1))
(Etempvar t ty1) tmp
| tr_comma : forall le dst e1 e2 ty sl1 a1 tmp1 sl2 a2 tmp2 tmp,
tr_expr le For_effects e1 sl1 a1 tmp1 ->
tr_expr le dst e2 sl2 a2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp ->
tr_expr le dst (Csyntax.Ecomma e1 e2 ty) (sl1 ++ sl2) a2 tmp
| tr_call_effects : forall le e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 any tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_exprlist le el2 sl2 al2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp ->
tr_expr le For_effects (Csyntax.Ecall e1 el2 ty)
(sl1 ++ sl2 ++ Scall None a1 al2 :: nil )
any tmp
| tr_call_val : forall le dst e1 el2 ty sl1 a1 tmp1 sl2 al2 tmp2 t tmp,
dst <> For_effects ->
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_exprlist le el2 sl2 al2 tmp2 ->
list_disjoint tmp1 tmp2 -> In t tmp ->
incl tmp1 tmp -> incl tmp2 tmp ->
tr_expr le dst (Csyntax.Ecall e1 el2 ty)
(sl1 ++ sl2 ++ Scall (Some t) a1 al2 :: final dst (Etempvar t ty))
(Etempvar t ty) tmp
| tr_builtin_effects : forall le ef tyargs el ty sl al tmp1 any tmp,
tr_exprlist le el sl al tmp1 ->
incl tmp1 tmp ->
tr_expr le For_effects (Csyntax.Ebuiltin ef tyargs el ty)
(sl ++ Sbuiltin None ef tyargs al :: nil )
any tmp
| tr_builtin_val : forall le dst ef tyargs el ty sl al tmp1 t tmp,
dst <> For_effects ->
tr_exprlist le el sl al tmp1 ->
In t tmp -> incl tmp1 tmp ->
tr_expr le dst (Csyntax.Ebuiltin ef tyargs el ty)
(sl ++ Sbuiltin (Some t) ef tyargs al :: final dst (Etempvar t ty))
(Etempvar t ty) tmp
| tr_paren_val : forall le e1 tycast ty sl1 a1 t tmp,
tr_expr le (For_set (SDbase tycast ty t)) e1 sl1 a1 tmp ->
In t tmp ->
tr_expr le For_val (Csyntax.Eparen e1 tycast ty)
sl1
(Etempvar t ty) tmp
| tr_paren_effects : forall le e1 tycast ty sl1 a1 tmp any,
tr_expr le For_effects e1 sl1 a1 tmp ->
tr_expr le For_effects (Csyntax.Eparen e1 tycast ty) sl1 any tmp
| tr_paren_set : forall le t sd e1 tycast ty sl1 a1 tmp any,
tr_expr le (For_set (SDcons tycast ty t sd)) e1 sl1 a1 tmp ->
In t tmp ->
tr_expr le (For_set sd) (Csyntax.Eparen e1 tycast ty) sl1 any tmp

with tr_exprlist : temp_env -> Csyntax.exprlist -> list statement -> list expr -> list ident -> Prop :=
| tr_nil : forall le tmp,
tr_exprlist le Csyntax.Enil nil nil tmp
| tr_cons : forall le e1 el2 sl1 a1 tmp1 sl2 al2 tmp2 tmp,
tr_expr le For_val e1 sl1 a1 tmp1 ->
tr_exprlist le el2 sl2 al2 tmp2 ->
list_disjoint tmp1 tmp2 ->
incl tmp1 tmp -> incl tmp2 tmp ->
tr_exprlist le (Csyntax.Econs e1 el2) (sl1 ++ sl2) (a1 :: al2) tmp.

Scheme tr_expr_ind2 := Minimality for tr_expr Sort Prop
with tr_exprlist_ind2 := Minimality for tr_exprlist Sort Prop.
Combined Scheme tr_expr_exprlist from tr_expr_ind2 , tr_exprlist_ind2 .


Lemma tr_expr_invariant :
forall le dst r sl a tmps, tr_expr le dst r sl a tmps ->
forall le', (forall x, In x tmps -> le'!x = le!x) ->
tr_expr le' dst r sl a tmps
with tr_exprlist_invariant :
forall le rl sl al tmps, tr_exprlist le rl sl al tmps ->
forall le', (forall x, In x tmps -> le'!x = le!x) ->
tr_exprlist le' rl sl al tmps.

Lemma tr_rvalof_monotone :
forall ty a sl b tmps, tr_rvalof ty a sl b tmps ->
forall tmps', incl tmps tmps' -> tr_rvalof ty a sl b tmps'.

Lemma tr_expr_monotone :
forall le dst r sl a tmps, tr_expr le dst r sl a tmps ->
forall tmps', incl tmps tmps' -> tr_expr le dst r sl a tmps'
with tr_exprlist_monotone :
forall le rl sl al tmps, tr_exprlist le rl sl al tmps ->
forall tmps', incl tmps tmps' -> tr_exprlist le rl sl al tmps'.

Top-level translation

Section TR_TOP .

Variable ge : genv .
Variable e : env .
Variable le : temp_env .
Variable m : mem .

Inductive tr_top : destination -> Csyntax.expr -> list statement -> expr -> list ident -> Prop :=
| tr_top_val_val : forall v ty a tmp,
typeof a = ty -> eval_expr ge e le m a v ->
tr_top For_val (Csyntax.Eval v ty) nil a tmp
| tr_top_base : forall dst r sl a tmp,
tr_expr le dst r sl a tmp ->
tr_top dst r sl a tmp.

End TR_TOP .

Translation of statements

Inductive tr_expression : Csyntax.expr -> statement -> expr -> Prop :=
| tr_expression_intro : forall r sl a tmps,
(forall ge e le m, tr_top ge e le m For_val r sl a tmps) ->
tr_expression r (makeseq sl) a.

Inductive tr_expr_stmt : Csyntax.expr -> statement -> Prop :=
| tr_expr_stmt_intro : forall r sl a tmps,
(forall ge e le m, tr_top ge e le m For_effects r sl a tmps) ->
tr_expr_stmt r (makeseq sl).

Inductive tr_if : Csyntax.expr -> statement -> statement -> statement -> Prop :=
| tr_if_intro : forall r s1 s2 sl a tmps,
(forall ge e le m, tr_top ge e le m For_val r sl a tmps) ->
tr_if r s1 s2 (makeseq (sl ++ makeif a s1 s2 :: nil )).

Inductive tr_stmt : Csyntax.statement -> statement -> Prop :=
| tr_skip :
tr_stmt Csyntax.Sskip Sskip
| tr_do : forall r s,
tr_expr_stmt r s ->
tr_stmt (Csyntax.Sdo r) s
| tr_seq : forall s1 s2 ts1 ts2,
tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
tr_stmt (Csyntax.Ssequence s1 s2) (Ssequence ts1 ts2)
| tr_ifthenelse_empty : forall r s' a,
tr_expression r s' a ->
tr_stmt (Csyntax.Sifthenelse r Csyntax.Sskip Csyntax.Sskip ) (Ssequence s' Sskip )
| tr_ifthenelse : forall r s1 s2 s' a ts1 ts2,
tr_expression r s' a ->
tr_stmt s1 ts1 -> tr_stmt s2 ts2 ->
tr_stmt (Csyntax.Sifthenelse r s1 s2) (Ssequence s' (Sifthenelse a ts1 ts2))
| tr_while : forall r s1 s' ts1,
tr_if r Sskip Sbreak s' ->
tr_stmt s1 ts1 ->
tr_stmt (Csyntax.Swhile r s1)
(Sloop (Ssequence s' ts1) Sskip )
| tr_dowhile : forall r s1 s' ts1,
tr_if r Sskip Sbreak s' ->
tr_stmt s1 ts1 ->
tr_stmt (Csyntax.Sdowhile r s1)
(Sloop ts1 s')
| tr_for_1 : forall r s3 s4 s' ts3 ts4,
tr_if r Sskip Sbreak s' ->
tr_stmt s3 ts3 ->
tr_stmt s4 ts4 ->
tr_stmt (Csyntax.Sfor Csyntax.Sskip r s3 s4)
(Sloop (Ssequence s' ts4) ts3)
| tr_for_2 : forall s1 r s3 s4 s' ts1 ts3 ts4,
tr_if r Sskip Sbreak s' ->
s1 <> Csyntax.Sskip ->
tr_stmt s1 ts1 ->
tr_stmt s3 ts3 ->
tr_stmt s4 ts4 ->
tr_stmt (Csyntax.Sfor s1 r s3 s4)
(Ssequence ts1 (Sloop (Ssequence s' ts4) ts3))
| tr_break :
tr_stmt Csyntax.Sbreak Sbreak
| tr_continue :
tr_stmt Csyntax.Scontinue Scontinue
| tr_return_none :
tr_stmt (Csyntax.Sreturn None ) (Sreturn None )
| tr_return_some : forall r s' a,
tr_expression r s' a ->
tr_stmt (Csyntax.Sreturn (Some r)) (Ssequence s' (Sreturn (Some a)))
| tr_switch : forall r ls s' a tls,
tr_expression r s' a ->
tr_lblstmts ls tls ->
tr_stmt (Csyntax.Sswitch r ls) (Ssequence s' (Sswitch a tls))
| tr_label : forall lbl s ts,
tr_stmt s ts ->
tr_stmt (Csyntax.Slabel lbl s) (Slabel lbl ts)
| tr_goto : forall lbl,
tr_stmt (Csyntax.Sgoto lbl) (Sgoto lbl)

with tr_lblstmts : Csyntax.labeled_statements -> labeled_statements -> Prop :=
| tr_ls_nil :
tr_lblstmts Csyntax.LSnil LSnil
| tr_ls_cons : forall c s ls ts tls,
tr_stmt s ts ->
tr_lblstmts ls tls ->
tr_lblstmts (Csyntax.LScons c s ls) (LScons c ts tls).

Correctness proof with respect to the specification.

Properties of the monad

Remark bind_inversion :
forall (A B: Type) (f: mon A) (g: A -> mon B) (y: B) (z1 z3: generator ) I,
bind f g z1 = Res y z3 I ->
exists x, exists z2, exists I1, exists I2,
f z1 = Res x z2 I1 /\ g x z2 = Res y z3 I2.

Remark bind2_inversion :
forall (A B Csyntax: Type) (f: mon (A*B)) (g: A -> B -> mon Csyntax) (y: Csyntax) (z1 z3: generator ) I,
bind2 f g z1 = Res y z3 I ->
exists x1, exists x2, exists z2, exists I1, exists I2,
f z1 = Res (x1,x2) z2 I1 /\ g x1 x2 z2 = Res y z3 I2.

Ltac monadInv1 H :=
match type of H with
| (Res _ _ _ = Res _ _ _) =>
inversion H; clear H; try subst
| (@ret _ _ _ = Res _ _ _) =>
inversion H; clear H; try subst
| (@error _ _ _ = Res _ _ _) =>
inversion H
| (bind ?F ?G ?Z = Res ?X ?Z' ?I) =>
let x := fresh "x" in (
let z := fresh "z" in (
let I1 := fresh "I" in (
let I2 := fresh "I" in (
let EQ1 := fresh "EQ" in (
let EQ2 := fresh "EQ" in (
destruct (bind_inversion _ _ F G X Z Z' I H) as [x [z [I1 [I2 [EQ1 EQ2]]]]];
clear H;
try (monadInv1 EQ2)))))))
| (bind2 ?F ?G ?Z = Res ?X ?Z' ?I) =>
let x := fresh "x" in (
let y := fresh "y" in (
let z := fresh "z" in (
let I1 := fresh "I" in (
let I2 := fresh "I" in (
let EQ1 := fresh "EQ" in (
let EQ2 := fresh "EQ" in (
destruct (bind2_inversion _ _ _ F G X Z Z' I H) as [x [y [z [I1 [I2 [EQ1 EQ2]]]]]];
clear H;
try (monadInv1 EQ2))))))))
end.

Ltac monadInv H :=
match type of H with
| (@ret _ _ _ = Res _ _ _) => monadInv1 H
| (@error _ _ _ = Res _ _ _) => monadInv1 H
| (bind ?F ?G ?Z = Res ?X ?Z' ?I) => monadInv1 H
| (bind2 ?F ?G ?Z = Res ?X ?Z' ?I) => monadInv1 H
| (?F _ _ _ _ _ _ _ _ = Res _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
| (?F _ _ _ _ _ _ _ = Res _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
| (?F _ _ _ _ _ _ = Res _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
| (?F _ _ _ _ _ = Res _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
| (?F _ _ _ _ = Res _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
| (?F _ _ _ = Res _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
| (?F _ _ = Res _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
| (?F _ = Res _ _ _) =>
((progress simpl in H) || unfold F in H); monadInv1 H
end.

Freshness and separation properties.

Definition within (id: ident ) (g1 g2: generator ) : Prop :=
Ple (gen_next g1) id /\ Plt id (gen_next g2).

Lemma gensym_within :
forall ty g1 id g2 I,
gensym ty g1 = Res id g2 I -> within id g1 g2.

Lemma within_widen :
forall id g1 g2 g1' g2',
within id g1 g2 ->
Ple (gen_next g1') (gen_next g1) ->
Ple (gen_next g2) (gen_next g2') ->
within id g1' g2'.

Definition contained (l: list ident ) (g1 g2: generator ) : Prop :=
forall id, In id l -> within id g1 g2.

Lemma contained_nil :
forall g1 g2, contained nil g1 g2.

Lemma contained_widen :
forall l g1 g2 g1' g2',
contained l g1 g2 ->
Ple (gen_next g1') (gen_next g1) ->
Ple (gen_next g2) (gen_next g2') ->
contained l g1' g2'.

Lemma contained_cons :
forall id l g1 g2,
within id g1 g2 -> contained l g1 g2 -> contained (id :: l) g1 g2.

Lemma contained_app :
forall l1 l2 g1 g2,
contained l1 g1 g2 -> contained l2 g1 g2 -> contained (l1 ++ l2) g1 g2.

Lemma contained_disjoint :
forall g1 l1 g2 l2 g3,
contained l1 g1 g2 -> contained l2 g2 g3 -> list_disjoint l1 l2.

Lemma contained_notin :
forall g1 l g2 id g3,
contained l g1 g2 -> within id g2 g3 -> ~In id l.

Hint Resolve gensym_within within_widen contained_widen
contained_cons contained_app contained_disjoint
contained_notin contained_nil
incl_refl incl_tl incl_app incl_appl incl_appr incl_same_head incl_cons
in_eq in_cons in_or_app
Ple_trans Ple_refl: gensym.

Properties of destinations

Definition dest_below (dst: destination ) (g: generator ) : Prop :=
match dst with
| For_set sd => Plt (sd_temp sd) g.(gen_next )
| _ => True
end.

Lemma dest_below_le :
forall dst g1 g2,
dest_below dst g1 -> Ple g1.(gen_next ) g2.(gen_next ) -> dest_below dst g2.

Remark dest_for_val_below : forall g, dest_below For_val g.

Remark dest_for_effect_below : forall g, dest_below For_effects g.

Lemma dest_for_set_base_below : forall tmp tycast ty g1 g2,
within tmp g1 g2 -> dest_below (For_set (SDbase tycast ty tmp)) g2.

Hint Resolve dest_below_le dest_for_set_base_below : gensym.
Local Hint Resolve dest_for_val_below dest_for_effect_below : core.

Properties of temp_for_sd

Definition good_temp_for_sd (ty: type ) (tmp: ident ) (sd: set_destination ) (g1 g2 g3: generator ) : Prop :=
Plt (sd_temp sd) g1.(gen_next )
/\ Ple g1.(gen_next ) g2.(gen_next )
/\ Ple g2.(gen_next ) g3.(gen_next )
/\ if type_eq ty (sd_head_type sd) then tmp = sd_temp sd else within tmp g2 g3.

Lemma temp_for_sd_charact : forall ty tmp sd g1 g2 g3 I,
dest_below (For_set sd) g1 ->
temp_for_sd ty sd g2 = Res tmp g3 I ->
Ple g1.(gen_next ) g2.(gen_next ) ->
good_temp_for_sd ty tmp sd g1 g2 g3.

Lemma dest_for_set_cons_below : forall tycast ty tmp sd g1 g2 g3,
good_temp_for_sd ty tmp sd g1 g2 g3 ->
dest_below (For_set (SDcons tycast ty tmp sd)) g3.

Lemma sd_temp_notin :
forall sd g1 g2 l, dest_below (For_set sd) g1 -> contained l g1 g2 -> ~In (sd_temp sd) l.

Definition used_temp_for_sd (ty: type ) (tmp: ident ) (sd: set_destination ) : list ident :=
if type_eq ty (sd_head_type sd) then nil else tmp :: nil .

Lemma temp_for_sd_disj : forall tmp1 tmp2 ty t sd g1 g2 g3 g4,
good_temp_for_sd ty t sd g1 g2 g3 ->
contained tmp1 g1 g2 ->
contained tmp2 g3 g4 ->
list_disjoint tmp1 (t :: tmp2).

Lemma temp_for_sd_in : forall tmp ty t sd g1 g2 g3,
good_temp_for_sd ty t sd g1 g2 g3 ->
In t (sd_temp sd :: used_temp_for_sd ty t sd ++ tmp).

Lemma temp_for_sd_contained : forall ty t sd g1 g2 g3,
good_temp_for_sd ty t sd g1 g2 g3 ->
contained (used_temp_for_sd ty t sd) g2 g3.

Hint Resolve temp_for_sd_charact dest_for_set_cons_below
sd_temp_notin temp_for_sd_disj temp_for_sd_in temp_for_sd_contained: gensym.

Correctness of the translation functions

Lemma finish_meets_spec_1 :
forall dst sl a sl' a',
finish dst sl a = (sl', a') -> sl' = sl ++ final dst a.

Lemma finish_meets_spec_2 :
forall dst sl a sl' a',
finish dst sl a = (sl', a') -> a' = a.

Ltac UseFinish :=
match goal with
| [ H: finish _ _ _ = (_, _) |- _ ] =>
try (rewrite (finish_meets_spec_2 _ _ _ _ _ H));
try (rewrite (finish_meets_spec_1 _ _ _ _ _ H));
repeat rewrite app_ass
end.

Definition add_dest (dst: destination ) (tmps: list ident ) :=
match dst with
| For_set sd => sd_temp sd :: tmps
| _ => tmps
end.

Lemma add_dest_incl :
forall dst tmps, incl tmps (add_dest dst tmps).

Lemma tr_expr_add_dest :
forall le dst r sl a tmps,
tr_expr le dst r sl a tmps ->
tr_expr le dst r sl a (add_dest dst tmps).


Lemma is_bitfield_access_meets_spec : forall l g bf g' I,
is_bitfield_access ce l g = Res bf g' I ->
tr_is_bitfield_access l bf.

Lemma transl_valof_meets_spec :
forall ty a g sl b g' I,
transl_valof ce ty a g = Res (sl, b) g' I ->
exists tmps, tr_rvalof ty a sl b tmps /\ contained tmps g g'.

Scheme expr_ind2 := Induction for Csyntax.expr Sort Prop
with exprlist_ind2 := Induction for Csyntax.exprlist Sort Prop.
Combined Scheme expr_exprlist_ind from expr_ind2 , exprlist_ind2 .

Lemma transl_meets_spec :
(forall r dst g sl a g' I,
transl_expr ce dst r g = Res (sl, a) g' I ->
dest_below dst g ->
exists tmps, (forall le, tr_expr le dst r sl a (add_dest dst tmps)) /\ contained tmps g g')
/\
(forall rl g sl al g' I,
transl_exprlist ce rl g = Res (sl, al) g' I ->
exists tmps, (forall le, tr_exprlist le rl sl al tmps) /\ contained tmps g g').

Lemma transl_expr_meets_spec :
forall r dst g sl a g' I,
transl_expr ce dst r g = Res (sl, a) g' I ->
dest_below dst g ->
exists tmps, forall ge e le m, tr_top ge e le m dst r sl a tmps.

Lemma transl_expression_meets_spec :
forall r g s a g' I,
transl_expression ce r g = Res (s, a) g' I ->
tr_expression r s a.

Lemma transl_expr_stmt_meets_spec :
forall r g s g' I,
transl_expr_stmt ce r g = Res s g' I ->
tr_expr_stmt r s.

Lemma transl_if_meets_spec :
forall r s1 s2 g s g' I,
transl_if ce r s1 s2 g = Res s g' I ->
tr_if r s1 s2 s.

Lemma transl_stmt_meets_spec :
forall s g ts g' I, transl_stmt ce s g = Res ts g' I -> tr_stmt s ts
with transl_lblstmt_meets_spec :
forall s g ts g' I, transl_lblstmt ce s g = Res ts g' I -> tr_lblstmts s ts.


Inductive tr_function : Csyntax.function -> Clight.function -> Prop :=
| tr_function_intro : forall f tf,
tr_stmt f.(Csyntax.fn_body ) tf.(fn_body ) ->
fn_return tf = Csyntax.fn_return f ->
fn_callconv tf = Csyntax.fn_callconv f ->
fn_params tf = Csyntax.fn_params f ->
fn_vars tf = Csyntax.fn_vars f ->
tr_function f tf.

Lemma transl_function_spec :
forall f tf,
transl_function ce f = OK tf ->
tr_function f tf.

End SPEC .

Inductive tr_fundef (p: Csyntax.program ): Csyntax.fundef -> Clight.fundef -> Prop :=
| tr_internal : forall f tf,
tr_function p.(prog_comp_env ) f tf ->
tr_fundef p (Internal f) (Internal tf)
| tr_external : forall ef targs tres cconv,
tr_fundef p (External ef targs tres cconv) (External ef targs tres cconv).

Lemma transl_fundef_spec :
forall p fd tfd,
transl_fundef p.(prog_comp_env ) fd = OK tfd ->
tr_fundef p fd tfd.