Correctness of the translation from Clight to C#minor.
Require Import Coqlib Errors Maps Integers Floats.
Require Import AST Linking.
Require Import Values Events Memory Globalenvs Smallstep.
Require Import Ctypes Cop Clight Cminor Csharpminor.
Require Import Cshmgen.
Relational specification of the transformation
Inductive match_fundef (
p:
Clight.program) :
Clight.fundef ->
Csharpminor.fundef ->
Prop :=
|
match_fundef_internal:
forall f tf,
transl_function p.(
prog_comp_env)
f =
OK tf ->
match_fundef p (
Ctypes.Internal f) (
AST.Internal tf)
|
match_fundef_external:
forall ef args res cc,
ef_sig ef =
signature_of_type args res cc ->
match_fundef p (
Ctypes.External ef args res cc) (
AST.External ef).
Definition match_varinfo (
v:
type) (
tv:
unit) :=
True.
Definition match_prog (
p:
Clight.program) (
tp:
Csharpminor.program) :
Prop :=
match_program_gen match_fundef match_varinfo p p tp.
Lemma transf_program_match:
forall p tp,
transl_program p =
OK tp ->
match_prog p tp.
Proof.
Properties of operations over types
Remark transl_params_types:
forall params,
map typ_of_type (
map snd params) =
typlist_of_typelist (
type_of_params params).
Proof.
induction params; simpl. auto. destruct a as [id ty]; simpl. f_equal; auto.
Qed.
Lemma transl_fundef_sig1:
forall ce f tf args res cc,
match_fundef ce f tf ->
classify_fun (
type_of_fundef f) =
fun_case_f args res cc ->
funsig tf =
signature_of_type args res cc.
Proof.
Lemma transl_fundef_sig2:
forall ce f tf args res cc,
match_fundef ce f tf ->
type_of_fundef f =
Tfunction args res cc ->
funsig tf =
signature_of_type args res cc.
Proof.
Lemma transl_sizeof:
forall (
cunit prog:
Clight.program)
t sz,
linkorder cunit prog ->
sizeof cunit.(
prog_comp_env)
t =
OK sz ->
sz =
Ctypes.sizeof prog.(
prog_comp_env)
t.
Proof.
Lemma transl_alignof:
forall (
cunit prog:
Clight.program)
t al,
linkorder cunit prog ->
alignof cunit.(
prog_comp_env)
t =
OK al ->
al =
Ctypes.alignof prog.(
prog_comp_env)
t.
Proof.
Lemma transl_alignof_blockcopy:
forall (
cunit prog:
Clight.program)
t sz,
linkorder cunit prog ->
sizeof cunit.(
prog_comp_env)
t =
OK sz ->
sz =
Ctypes.sizeof prog.(
prog_comp_env)
t /\
alignof_blockcopy cunit.(
prog_comp_env)
t =
alignof_blockcopy prog.(
prog_comp_env)
t.
Proof.
Lemma field_offset_stable:
forall (
cunit prog:
Clight.program)
id co f,
linkorder cunit prog ->
cunit.(
prog_comp_env)!
id =
Some co ->
prog.(
prog_comp_env)!
id =
Some co /\
field_offset prog.(
prog_comp_env)
f (
co_members co) =
field_offset cunit.(
prog_comp_env)
f (
co_members co).
Proof.
Section WITHEXTERNALCALLS.
Context `{
external_calls_prf:
ExternalCalls}.
Variable fn_stack_requirements :
ident ->
Z.
Properties of the translation functions
Transformation of expressions and statements.
Lemma transl_expr_lvalue:
forall ge e le m a loc ofs ce ta,
Clight.eval_lvalue ge e le m a loc ofs ->
transl_expr ce a =
OK ta ->
(
exists tb,
transl_lvalue ce a =
OK tb /\
make_load tb (
typeof a) =
OK ta).
Proof.
intros until ta;
intros EVAL TR.
inv EVAL;
simpl in TR.
var local *)
exists (
Eaddrof id);
auto.
var global *)
exists (
Eaddrof id);
auto.
deref *)
monadInv TR.
exists x;
auto.
field struct *)
monadInv TR.
exists x0;
split;
auto.
simpl;
rewrite EQ;
auto.
field union *)
monadInv TR.
exists x0;
split;
auto.
simpl;
rewrite EQ;
auto.
Qed.
Properties of labeled statements
Lemma transl_lbl_stmt_1:
forall ce tyret nbrk ncnt n sl tsl,
transl_lbl_stmt ce tyret nbrk ncnt sl =
OK tsl ->
transl_lbl_stmt ce tyret nbrk ncnt (
Clight.select_switch n sl) =
OK (
select_switch n tsl).
Proof.
Lemma transl_lbl_stmt_2:
forall ce tyret nbrk ncnt sl tsl,
transl_lbl_stmt ce tyret nbrk ncnt sl =
OK tsl ->
transl_statement ce tyret nbrk ncnt (
seq_of_labeled_statement sl) =
OK (
seq_of_lbl_stmt tsl).
Proof.
induction sl; intros.
monadInv H. auto.
monadInv H. simpl. rewrite EQ; simpl. rewrite (IHsl _ EQ1). simpl. auto.
Qed.
Correctness of Csharpminor construction functions
Section CONSTRUCTORS.
Variables cunit prog:
Clight.program.
Hypothesis LINK:
linkorder cunit prog.
Variable ge:
genv.
Lemma make_intconst_correct:
forall n e le m,
eval_expr ge e le m (
make_intconst n) (
Vint n).
Proof.
Lemma make_floatconst_correct:
forall n e le m,
eval_expr ge e le m (
make_floatconst n) (
Vfloat n).
Proof.
Lemma make_singleconst_correct:
forall n e le m,
eval_expr ge e le m (
make_singleconst n) (
Vsingle n).
Proof.
Lemma make_longconst_correct:
forall n e le m,
eval_expr ge e le m (
make_longconst n) (
Vlong n).
Proof.
Lemma make_ptrofsconst_correct:
forall n e le m,
eval_expr ge e le m (
make_ptrofsconst n) (
Vptrofs (
Ptrofs.repr n)).
Proof.
Lemma make_singleoffloat_correct:
forall a n e le m,
eval_expr ge e le m a (
Vfloat n) ->
eval_expr ge e le m (
make_singleoffloat a) (
Vsingle (
Float.to_single n)).
Proof.
intros. econstructor. eauto. auto.
Qed.
Lemma make_floatofsingle_correct:
forall a n e le m,
eval_expr ge e le m a (
Vsingle n) ->
eval_expr ge e le m (
make_floatofsingle a) (
Vfloat (
Float.of_single n)).
Proof.
intros. econstructor. eauto. auto.
Qed.
Lemma make_floatofint_correct:
forall a n sg e le m,
eval_expr ge e le m a (
Vint n) ->
eval_expr ge e le m (
make_floatofint a sg) (
Vfloat(
cast_int_float sg n)).
Proof.
Hint Resolve make_intconst_correct make_floatconst_correct make_longconst_correct
make_singleconst_correct make_singleoffloat_correct make_floatofsingle_correct
make_floatofint_correct:
cshm.
Hint Constructors eval_expr eval_exprlist:
cshm.
Hint Extern 2 (@
eq trace _ _) =>
traceEq:
cshm.
Lemma make_cmpu_ne_zero_correct:
forall e le m a n,
eval_expr ge e le m a (
Vint n) ->
eval_expr ge e le m (
make_cmpu_ne_zero a) (
Vint (
if Int.eq n Int.zero then Int.zero else Int.one)).
Proof.
Lemma make_cmpu_ne_zero_correct_ptr:
forall e le m a b i,
eval_expr ge e le m a (
Vptr b i) ->
Archi.ptr64 =
false ->
Mem.weak_valid_pointer m b (
Ptrofs.unsigned i) =
true ->
eval_expr ge e le m (
make_cmpu_ne_zero a)
Vone.
Proof.
Lemma make_cast_int_correct:
forall e le m a n sz si,
eval_expr ge e le m a (
Vint n) ->
eval_expr ge e le m (
make_cast_int a sz si) (
Vint (
cast_int_int sz si n)).
Proof.
Lemma make_longofint_correct:
forall e le m a n si,
eval_expr ge e le m a (
Vint n) ->
eval_expr ge e le m (
make_longofint a si) (
Vlong (
cast_int_long si n)).
Proof.
Hint Resolve make_cast_int_correct make_longofint_correct:
cshm.
Ltac InvEval :=
match goal with
| [
H:
None =
Some _ |-
_ ] =>
discriminate
| [
H:
Some _ =
Some _ |-
_ ] =>
inv H;
InvEval
| [
H:
match ?
x with Some _ =>
_ |
None =>
_ end =
Some _ |-
_ ] =>
destruct x eqn:?;
InvEval
| [
H:
match ?
x with true =>
_ |
false =>
_ end =
Some _ |-
_ ] =>
destruct x eqn:?;
InvEval
|
_ =>
idtac
end.
Lemma make_cast_correct:
forall e le m a b v ty1 ty2 v',
make_cast ty1 ty2 a =
OK b ->
eval_expr ge e le m a v ->
sem_cast v ty1 ty2 m =
Some v' ->
eval_expr ge e le m b v'.
Proof.
intros.
unfold make_cast,
sem_cast in *;
destruct (
classify_cast ty1 ty2);
inv H;
destruct v;
InvEval;
eauto with cshm.
-
unfold make_singleofint,
cast_int_float.
destruct si1;
eauto with cshm.
-
apply make_cast_int_correct.
unfold cast_float_int in Heqo.
unfold make_intoffloat.
destruct si2;
econstructor;
eauto;
simpl;
rewrite Heqo;
auto.
-
apply make_cast_int_correct.
unfold cast_single_int in Heqo.
unfold make_intofsingle.
destruct si2;
econstructor;
eauto with cshm;
simpl;
rewrite Heqo;
auto.
-
unfold make_floatoflong,
cast_long_float.
destruct si1;
eauto with cshm.
-
unfold make_singleoflong,
cast_long_single.
destruct si1;
eauto with cshm.
-
unfold cast_float_long in Heqo.
unfold make_longoffloat.
destruct si2;
econstructor;
eauto;
simpl;
rewrite Heqo;
auto.
-
unfold cast_single_long in Heqo.
unfold make_longofsingle.
destruct si2;
econstructor;
eauto with cshm;
simpl;
rewrite Heqo;
auto.
-
apply make_cmpu_ne_zero_correct;
auto.
-
eapply make_cmpu_ne_zero_correct_ptr;
eauto.
-
econstructor;
eauto with cshm.
simpl.
unfold Val.cmplu,
Val.cmplu_bool,
Int64.cmpu.
destruct (
Int64.eq i Int64.zero);
auto.
-
econstructor;
eauto with cshm.
simpl.
unfold Val.cmplu,
Val.cmplu_bool.
rewrite Cop.weak_valid_pointer_eq in Heqb1.
unfold Mem.weak_valid_pointer in Heqb1.
rewrite Heqb0,
Heqb1.
rewrite Int64.eq_true.
reflexivity.
-
econstructor;
eauto with cshm.
simpl.
unfold Val.cmpf,
Val.cmpf_bool.
rewrite Float.cmp_ne_eq.
destruct (
Float.cmp Ceq f Float.zero);
auto.
-
econstructor;
eauto with cshm.
simpl.
unfold Val.cmpfs,
Val.cmpfs_bool.
rewrite Float32.cmp_ne_eq.
destruct (
Float32.cmp Ceq f Float32.zero);
auto.
-
destruct (
ident_eq id1 id2);
inv H1;
auto.
-
destruct (
ident_eq id1 id2);
inv H1;
auto.
Qed.
Lemma make_boolean_correct:
forall e le m a v ty b,
eval_expr ge e le m a v ->
bool_val v ty m =
Some b ->
exists vb,
eval_expr ge e le m (
make_boolean a ty)
vb
/\
Val.bool_of_val vb b.
Proof.
Lemma make_neg_correct:
forall a tya c va v e le m,
sem_neg va tya =
Some v ->
make_neg a tya =
OK c ->
eval_expr ge e le m a va ->
eval_expr ge e le m c v.
Proof.
unfold sem_neg,
make_neg;
intros until m;
intros SEM MAKE EV1;
destruct (
classify_neg tya);
inv MAKE;
destruct va;
inv SEM;
eauto with cshm.
Qed.
Lemma make_absfloat_correct:
forall a tya c va v e le m,
sem_absfloat va tya =
Some v ->
make_absfloat a tya =
OK c ->
eval_expr ge e le m a va ->
eval_expr ge e le m c v.
Proof.
unfold sem_absfloat,
make_absfloat;
intros until m;
intros SEM MAKE EV1;
destruct (
classify_neg tya);
inv MAKE;
destruct va;
inv SEM;
eauto with cshm.
unfold make_floatoflong,
cast_long_float.
destruct s.
econstructor.
econstructor;
simpl;
eauto.
simpl;
eauto.
simpl;
eauto.
econstructor.
econstructor;
simpl;
eauto.
simpl;
eauto.
simpl;
eauto.
Qed.
Lemma make_notbool_correct:
forall a tya c va v e le m,
sem_notbool va tya m =
Some v ->
make_notbool a tya =
OK c ->
eval_expr ge e le m a va ->
eval_expr ge e le m c v.
Proof.
unfold sem_notbool,
bool_val,
make_notbool;
intros until m;
intros SEM MAKE EV1.
destruct (
classify_bool tya);
inv MAKE;
destruct va;
simpl in SEM;
InvEval.
-
econstructor;
eauto with cshm.
simpl.
unfold Val.cmpu,
Val.cmpu_bool,
Int.cmpu.
destruct (
Int.eq i Int.zero);
auto.
-
destruct Archi.ptr64 eqn:
SF;
inv SEM.
rewrite Cop.weak_valid_pointer_eq in H0.
destruct (
Mem.weak_valid_pointer m b (
Ptrofs.unsigned i))
eqn:
V;
simpl in H0;
inv H0.
econstructor;
eauto with cshm.
simpl.
unfold Val.cmpu,
Val.cmpu_bool.
unfold Mem.weak_valid_pointer in V.
rewrite SF,
V,
Int.eq_true.
auto.
-
econstructor;
eauto with cshm.
simpl.
unfold Val.cmplu,
Val.cmplu_bool,
Int64.cmpu.
destruct (
Int64.eq i Int64.zero);
auto.
-
destruct Archi.ptr64 eqn:
SF;
inv SEM.
rewrite Cop.weak_valid_pointer_eq in H0.
destruct (
Mem.weak_valid_pointer m b (
Ptrofs.unsigned i))
eqn:
V;
simpl in H0;
inv H0.
econstructor;
eauto with cshm.
simpl.
unfold Val.cmplu,
Val.cmplu_bool.
unfold Mem.weak_valid_pointer in V.
rewrite SF,
V,
Int64.eq_true.
auto.
-
econstructor;
eauto with cshm.
simpl.
unfold Val.cmpf,
Val.cmpf_bool.
destruct (
Float.cmp Ceq f Float.zero);
auto.
-
econstructor;
eauto with cshm.
simpl.
unfold Val.cmpfs,
Val.cmpfs_bool.
destruct (
Float32.cmp Ceq f Float32.zero);
auto.
Qed.
Lemma make_notint_correct:
forall a tya c va v e le m,
sem_notint va tya =
Some v ->
make_notint a tya =
OK c ->
eval_expr ge e le m a va ->
eval_expr ge e le m c v.
Proof.
Definition binary_constructor_correct
(
make:
expr ->
type ->
expr ->
type ->
res expr)
(
sem:
val ->
type ->
val ->
type ->
mem ->
option val):
Prop :=
forall a tya b tyb c va vb v e le m,
sem va tya vb tyb m =
Some v ->
make a tya b tyb =
OK c ->
eval_expr ge e le m a va ->
eval_expr ge e le m b vb ->
eval_expr ge e le m c v.
Definition shift_constructor_correct
(
make:
expr ->
type ->
expr ->
type ->
res expr)
(
sem:
val ->
type ->
val ->
type ->
option val):
Prop :=
forall a tya b tyb c va vb v e le m,
sem va tya vb tyb =
Some v ->
make a tya b tyb =
OK c ->
eval_expr ge e le m a va ->
eval_expr ge e le m b vb ->
eval_expr ge e le m c v.
Section MAKE_BIN.
Variable sem_int:
signedness ->
int ->
int ->
option val.
Variable sem_long:
signedness ->
int64 ->
int64 ->
option val.
Variable sem_float:
float ->
float ->
option val.
Variable sem_single:
float32 ->
float32 ->
option val.
Variables iop iopu fop sop lop lopu:
binary_operation.
Hypothesis iop_ok:
forall x y m,
eval_binop iop (
Vint x) (
Vint y)
m =
sem_int Signed x y.
Hypothesis iopu_ok:
forall x y m,
eval_binop iopu (
Vint x) (
Vint y)
m =
sem_int Unsigned x y.
Hypothesis lop_ok:
forall x y m,
eval_binop lop (
Vlong x) (
Vlong y)
m =
sem_long Signed x y.
Hypothesis lopu_ok:
forall x y m,
eval_binop lopu (
Vlong x) (
Vlong y)
m =
sem_long Unsigned x y.
Hypothesis fop_ok:
forall x y m,
eval_binop fop (
Vfloat x) (
Vfloat y)
m =
sem_float x y.
Hypothesis sop_ok:
forall x y m,
eval_binop sop (
Vsingle x) (
Vsingle y)
m =
sem_single x y.
Lemma make_binarith_correct:
binary_constructor_correct
(
make_binarith iop iopu fop sop lop lopu)
(
sem_binarith sem_int sem_long sem_float sem_single).
Proof.
red;
unfold make_binarith,
sem_binarith;
intros until m;
intros SEM MAKE EV1 EV2.
set (
cls :=
classify_binarith tya tyb)
in *.
set (
ty :=
binarith_type cls)
in *.
monadInv MAKE.
destruct (
sem_cast va tya ty m)
as [
va'|]
eqn:
Ca;
try discriminate.
destruct (
sem_cast vb tyb ty m)
as [
vb'|]
eqn:
Cb;
try discriminate.
exploit make_cast_correct.
eexact EQ.
eauto.
eauto.
intros EV1'.
exploit make_cast_correct.
eexact EQ1.
eauto.
eauto.
intros EV2'.
destruct cls;
inv EQ2;
destruct va';
try discriminate;
destruct vb';
try discriminate.
-
destruct s;
inv H0;
econstructor;
eauto with cshm.
rewrite iop_ok;
auto.
rewrite iopu_ok;
auto.
-
destruct s;
inv H0;
econstructor;
eauto with cshm.
rewrite lop_ok;
auto.
rewrite lopu_ok;
auto.
-
erewrite <-
fop_ok in SEM;
eauto with cshm.
-
erewrite <-
sop_ok in SEM;
eauto with cshm.
Qed.
Lemma make_binarith_int_correct:
binary_constructor_correct
(
make_binarith_int iop iopu lop lopu)
(
sem_binarith sem_int sem_long (
fun x y =>
None) (
fun x y =>
None)).
Proof.
red;
unfold make_binarith_int,
sem_binarith;
intros until m;
intros SEM MAKE EV1 EV2.
set (
cls :=
classify_binarith tya tyb)
in *.
set (
ty :=
binarith_type cls)
in *.
monadInv MAKE.
destruct (
sem_cast va tya ty m)
as [
va'|]
eqn:
Ca;
try discriminate.
destruct (
sem_cast vb tyb ty m)
as [
vb'|]
eqn:
Cb;
try discriminate.
exploit make_cast_correct.
eexact EQ.
eauto.
eauto.
intros EV1'.
exploit make_cast_correct.
eexact EQ1.
eauto.
eauto.
intros EV2'.
destruct cls;
inv EQ2;
destruct va';
try discriminate;
destruct vb';
try discriminate.
-
destruct s;
inv H0;
econstructor;
eauto with cshm.
rewrite iop_ok;
auto.
rewrite iopu_ok;
auto.
-
destruct s;
inv H0;
econstructor;
eauto with cshm.
rewrite lop_ok;
auto.
rewrite lopu_ok;
auto.
Qed.
End MAKE_BIN.
Hint Extern 2 (@
eq (
option val)
_ _) => (
simpl;
reflexivity) :
cshm.
Lemma make_add_correct:
binary_constructor_correct (
make_add cunit.(
prog_comp_env)) (
sem_add prog.(
prog_comp_env)).
Proof.
Lemma make_sub_correct:
binary_constructor_correct (
make_sub cunit.(
prog_comp_env)) (
sem_sub prog.(
prog_comp_env)).
Proof.
Lemma make_mul_correct:
binary_constructor_correct make_mul sem_mul.
Proof.
Lemma make_div_correct:
binary_constructor_correct make_div sem_div.
Proof.
Lemma make_mod_correct:
binary_constructor_correct make_mod sem_mod.
Proof.
Lemma make_and_correct:
binary_constructor_correct make_and sem_and.
Proof.
Lemma make_or_correct:
binary_constructor_correct make_or sem_or.
Proof.
Lemma make_xor_correct:
binary_constructor_correct make_xor sem_xor.
Proof.
Ltac comput val :=
let x :=
fresh in set val as x in *;
vm_compute in x;
subst x.
Remark small_shift_amount_1:
forall i,
Int64.ltu i Int64.iwordsize =
true ->
Int.ltu (
Int64.loword i)
Int64.iwordsize' =
true
/\
Int64.unsigned i =
Int.unsigned (
Int64.loword i).
Proof.
Remark small_shift_amount_2:
forall i,
Int64.ltu i (
Int64.repr 32) =
true ->
Int.ltu (
Int64.loword i)
Int.iwordsize =
true.
Proof.
Lemma small_shift_amount_3:
forall i,
Int.ltu i Int64.iwordsize' =
true ->
Int64.unsigned (
Int64.repr (
Int.unsigned i)) =
Int.unsigned i.
Proof.
Lemma make_shl_correct:
shift_constructor_correct make_shl sem_shl.
Proof.
Lemma make_shr_correct:
shift_constructor_correct make_shr sem_shr.
Proof.
Lemma make_cmp_ptr_correct:
forall cmp e le m a va b vb v,
cmp_ptr (
valid_pointer :=
Mem.valid_pointer)
m cmp va vb =
Some v ->
eval_expr ge e le m a va ->
eval_expr ge e le m b vb ->
eval_expr ge e le m (
make_cmp_ptr cmp a b)
v.
Proof.
Remark make_ptrofs_of_int_correct:
forall e le m a i si,
eval_expr ge e le m a (
Vint i) ->
eval_expr ge e le m (
if Archi.ptr64 then make_longofint a si else a) (
Vptrofs (
ptrofs_of_int si i)).
Proof.
Remark make_ptrofs_of_int64_correct:
forall e le m a i,
eval_expr ge e le m a (
Vlong i) ->
eval_expr ge e le m (
if Archi.ptr64 then a else Eunop Ointoflong a) (
Vptrofs (
Ptrofs.of_int64 i)).
Proof.
Lemma make_cmp_correct:
forall cmp,
binary_constructor_correct (
make_cmp cmp) (
sem_cmp cmp).
Proof.
Lemma transl_unop_correct:
forall op a tya c va v e le m,
transl_unop op a tya =
OK c ->
sem_unary_operation op va tya m =
Some v ->
eval_expr ge e le m a va ->
eval_expr ge e le m c v.
Proof.
Lemma transl_binop_correct:
forall op a tya b tyb c va vb v e le m,
transl_binop cunit.(
prog_comp_env)
op a tya b tyb =
OK c ->
sem_binary_operation prog.(
prog_comp_env)
op va tya vb tyb m =
Some v ->
eval_expr ge e le m a va ->
eval_expr ge e le m b vb ->
eval_expr ge e le m c v.
Proof.
Lemma make_load_correct:
forall addr ty code b ofs v e le m,
make_load addr ty =
OK code ->
eval_expr ge e le m addr (
Vptr b ofs) ->
deref_loc ty m b ofs v ->
eval_expr ge e le m code v.
Proof.
unfold make_load;
intros until m;
intros MKLOAD EVEXP DEREF.
inv DEREF.
scalar *)
rewrite H in MKLOAD.
inv MKLOAD.
apply eval_Eload with (
Vptr b ofs);
auto.
by reference *)
rewrite H in MKLOAD.
inv MKLOAD.
auto.
by copy *)
rewrite H in MKLOAD.
inv MKLOAD.
auto.
Qed.
Lemma make_memcpy_correct:
forall (
SGE_NEXTBLOCK:
Genv.genv_next ge =
Genv.genv_next (
Clight.globalenv prog)),
forall f dst src ty k e le m b ofs v m'
s,
eval_expr ge e le m dst (
Vptr b ofs) ->
eval_expr ge e le m src v ->
assign_loc (
Clight.globalenv prog)
ty m b ofs v m' ->
access_mode ty =
By_copy ->
make_memcpy cunit.(
prog_comp_env)
dst src ty =
OK s ->
forall (
STACK_TOP_NO_INFO:
forall b,
is_stack_top (
Mem.stack m)
b ->
forall fi,
get_frame_info (
Mem.stack m)
b =
Some fi ->
forall o,
frame_perm fi o =
Public),
(
step fn_stack_requirements)
ge (
State f s k e le m)
E0 (
State f Sskip k e le m').
Proof.
Lemma make_store_correct:
forall (
SGE_NEXTBLOCK:
Genv.genv_next ge =
Genv.genv_next (
Clight.globalenv prog)),
forall addr ty rhs code e le m b ofs v m'
f k,
make_store cunit.(
prog_comp_env)
addr ty rhs =
OK code ->
eval_expr ge e le m addr (
Vptr b ofs) ->
eval_expr ge e le m rhs v ->
assign_loc (
Clight.globalenv prog)
ty m b ofs v m' ->
forall (
STACK_TOP_NO_INFO:
forall b,
is_stack_top (
Mem.stack m)
b ->
forall fi,
get_frame_info (
Mem.stack m)
b =
Some fi ->
forall o,
frame_perm fi o =
Public),
(
step fn_stack_requirements)
ge (
State f code k e le m)
E0 (
State f Sskip k e le m').
Proof.
unfold make_store.
intros until k;
intros MKSTORE EV1 EV2 ASSIGN.
inversion ASSIGN;
subst.
nonvolatile scalar *)
rewrite H in MKSTORE;
inv MKSTORE.
econstructor;
eauto.
by copy *)
rewrite H in MKSTORE.
eapply make_memcpy_correct with (
b :=
b) (
v :=
Vptr b'
ofs');
eauto.
Qed.
End CONSTRUCTORS.
Basic preservation invariants
Section CORRECTNESS.
Variable prog:
Clight.program.
Variable tprog:
Csharpminor.program.
Hypothesis TRANSL:
match_prog prog tprog.
Let ge :=
globalenv prog.
Let tge :=
Genv.globalenv tprog.
Lemma symbols_preserved:
forall s,
Genv.find_symbol tge s =
Genv.find_symbol ge s.
Proof (
Genv.find_symbol_match TRANSL).
Lemma genv_next_preserved:
Genv.genv_next tge =
Genv.genv_next ge.
Proof (
Genv.genv_next_match TRANSL).
Lemma senv_preserved:
Senv.equiv ge tge.
Proof (
Genv.senv_match TRANSL).
Lemma function_ptr_translated:
forall v f,
Genv.find_funct_ptr ge v =
Some f ->
exists cu tf,
Genv.find_funct_ptr tge v =
Some tf /\
match_fundef cu f tf /\
linkorder cu prog.
Proof (
Genv.find_funct_ptr_match TRANSL).
Lemma functions_translated:
forall v f,
Genv.find_funct ge v =
Some f ->
exists cu tf,
Genv.find_funct tge v =
Some tf /\
match_fundef cu f tf /\
linkorder cu prog.
Proof (
Genv.find_funct_match TRANSL).
Matching between environments
In this section, we define a matching relation between
a Clight local environment and a Csharpminor local environment.
Record match_env (
e:
Clight.env) (
te:
Csharpminor.env) :
Prop :=
mk_match_env {
me_local:
forall id b ty,
e!
id =
Some (
b,
ty) ->
te!
id =
Some(
b,
Ctypes.sizeof ge ty);
me_local_inv:
forall id b sz,
te!
id =
Some (
b,
sz) ->
exists ty,
e!
id =
Some(
b,
ty)
}.
Lemma match_env_globals:
forall e te id,
match_env e te ->
e!
id =
None ->
te!
id =
None.
Proof.
intros.
destruct (
te!
id)
as [[
b sz] | ]
eqn:?;
auto.
exploit me_local_inv;
eauto.
intros [
ty EQ].
congruence.
Qed.
Lemma match_env_same_blocks:
forall e te,
match_env e te ->
blocks_of_env te =
Clight.blocks_of_env ge e.
Proof.
Lemma match_env_free_blocks:
forall e te m m',
match_env e te ->
Mem.free_list m (
Clight.blocks_of_env ge e) =
Some m' ->
Mem.free_list m (
blocks_of_env te) =
Some m'.
Proof.
Lemma match_env_empty:
match_env Clight.empty_env Csharpminor.empty_env.
Proof.
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 cunit,
linkorder cunit prog ->
forall e1 m1 vars e2 m2,
Clight.alloc_variables ge e1 m1 vars e2 m2 ->
forall tvars te1,
mmap (
transl_var cunit.(
prog_comp_env))
vars =
OK tvars ->
match_env e1 te1 ->
exists te2,
Csharpminor.alloc_variables te1 m1 tvars te2 m2
/\
match_env e2 te2.
Proof.
induction 2;
simpl;
intros.
-
inv H0.
exists te1;
split.
constructor.
auto.
-
monadInv H2.
monadInv EQ.
simpl in *.
exploit transl_sizeof.
eexact H.
eauto.
intros SZ;
rewrite SZ.
exploit (
IHalloc_variables x0 (
PTree.set id (
b1,
Ctypes.sizeof ge ty)
te1)).
auto.
constructor.
me_local *)
intros until ty0.
repeat rewrite PTree.gsspec.
destruct (
peq id0 id);
intros.
congruence.
eapply me_local;
eauto.
me_local_inv *)
intros until sz.
repeat rewrite PTree.gsspec.
destruct (
peq id0 id);
intros.
exists ty;
congruence.
eapply me_local_inv;
eauto.
intros [
te2 [
ALLOC MENV]].
exists te2;
split.
econstructor;
eauto.
auto.
Qed.
Lemma create_undef_temps_match:
forall temps,
create_undef_temps (
map fst temps) =
Clight.create_undef_temps temps.
Proof.
induction temps; simpl. auto.
destruct a as [id ty]. simpl. decEq. auto.
Qed.
Lemma bind_parameter_temps_match:
forall vars vals le1 le2,
Clight.bind_parameter_temps vars vals le1 =
Some le2 ->
bind_parameters (
map fst vars)
vals le1 =
Some le2.
Proof.
induction vars; simpl; intros.
destruct vals; inv H. auto.
destruct a as [id ty]. destruct vals; try discriminate. auto.
Qed.
Lemma transl_vars_names:
forall ce vars tvars,
mmap (
transl_var ce)
vars =
OK tvars ->
map fst tvars =
var_names vars.
Proof.
intros.
exploit mmap_inversion;
eauto.
generalize vars tvars.
induction 1;
simpl.
-
auto.
-
monadInv H0.
simpl;
congruence.
Qed.
Proof of semantic preservation
Semantic preservation for expressions
The proof of semantic preservation for the translation of expressions
relies on simulation diagrams of the following form:
e, le, m, a ------------------- te, le, m, ta
| |
| |
| |
v v
e, le, m, v ------------------- te, le, 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.
.
Variable cunit:
Clight.program.
Hypothesis LINK:
linkorder cunit prog.
Variable e:
Clight.env.
Variable le:
temp_env.
Variable m:
mem.
Variable te:
Csharpminor.env.
Hypothesis MENV:
match_env e te.
Lemma transl_expr_lvalue_correct:
(
forall a v,
Clight.eval_expr ge e le m a v ->
forall ta (
TR:
transl_expr cunit.(
prog_comp_env)
a =
OK ta) ,
Csharpminor.eval_expr tge te le m ta v)
/\(
forall a b ofs,
Clight.eval_lvalue ge e le m a b ofs ->
forall ta (
TR:
transl_lvalue cunit.(
prog_comp_env)
a =
OK ta),
Csharpminor.eval_expr tge te le m ta (
Vptr b ofs)).
Proof.
Lemma transl_expr_correct:
forall a v,
Clight.eval_expr ge e le m a v ->
forall ta,
transl_expr cunit.(
prog_comp_env)
a =
OK ta ->
Csharpminor.eval_expr tge te le m ta v.
Proof (
proj1 transl_expr_lvalue_correct).
Lemma transl_lvalue_correct:
forall a b ofs,
Clight.eval_lvalue ge e le m a b ofs ->
forall ta,
transl_lvalue cunit.(
prog_comp_env)
a =
OK ta ->
Csharpminor.eval_expr tge te le m ta (
Vptr b ofs).
Proof (
proj2 transl_expr_lvalue_correct).
Lemma transl_arglist_correct:
forall al tyl vl,
Clight.eval_exprlist ge e le m al tyl vl ->
forall tal,
transl_arglist cunit.(
prog_comp_env)
al tyl =
OK tal ->
Csharpminor.eval_exprlist tge te le m tal vl.
Proof.
Lemma typlist_of_arglist_eq:
forall al tyl vl,
Clight.eval_exprlist ge e le m al tyl vl ->
typlist_of_arglist al tyl =
typlist_of_typelist tyl.
Proof.
induction 1; simpl.
auto.
f_equal; auto.
Qed.
End EXPR.
Semantic preservation for statements
The simulation diagram for the translation of statements and functions
is a "plus" diagram of the form
I
S1 ------- R1
| |
t | + | t
v v
S2 ------- R2
I I
The invariant
I is the
match_states predicate that we now define.
:
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 le m,
match_transl (
Sblock ts)
tk ts'
tk' ->
star (
step fn_stack_requirements)
tge (
State f ts'
tk'
te le m)
E0 (
State f ts (
Kblock tk)
te le m).
Proof.
Inductive match_cont:
composite_env ->
type ->
nat ->
nat ->
Clight.cont ->
Csharpminor.cont ->
Prop :=
|
match_Kstop:
forall ce tyret nbrk ncnt,
match_cont tyret ce nbrk ncnt Clight.Kstop Kstop
|
match_Kseq:
forall ce tyret nbrk ncnt s k ts tk,
transl_statement ce tyret nbrk ncnt s =
OK ts ->
match_cont ce tyret nbrk ncnt k tk ->
match_cont ce tyret nbrk ncnt
(
Clight.Kseq s k)
(
Kseq ts tk)
|
match_Kloop1:
forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
transl_statement ce tyret 1%
nat 0%
nat s1 =
OK ts1 ->
transl_statement ce tyret 0%
nat (
S ncnt)
s2 =
OK ts2 ->
match_cont ce tyret nbrk ncnt k tk ->
match_cont ce tyret 1%
nat 0%
nat
(
Clight.Kloop1 s1 s2 k)
(
Kblock (
Kseq ts2 (
Kseq (
Sloop (
Sseq (
Sblock ts1)
ts2)) (
Kblock tk))))
|
match_Kloop2:
forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
transl_statement ce tyret 1%
nat 0%
nat s1 =
OK ts1 ->
transl_statement ce tyret 0%
nat (
S ncnt)
s2 =
OK ts2 ->
match_cont ce tyret nbrk ncnt k tk ->
match_cont ce tyret 0%
nat (
S ncnt)
(
Clight.Kloop2 s1 s2 k)
(
Kseq (
Sloop (
Sseq (
Sblock ts1)
ts2)) (
Kblock tk))
|
match_Kswitch:
forall ce tyret nbrk ncnt k tk,
match_cont ce tyret nbrk ncnt k tk ->
match_cont ce tyret 0%
nat (
S ncnt)
(
Clight.Kswitch k)
(
Kblock tk)
|
match_Kcall:
forall ce tyret nbrk ncnt nbrk'
ncnt'
f e k id tf te le tk cu,
linkorder cu prog ->
transl_function cu.(
prog_comp_env)
f =
OK tf ->
match_env e te ->
match_cont cu.(
prog_comp_env) (
Clight.fn_return f)
nbrk'
ncnt'
k tk ->
match_cont ce tyret nbrk ncnt
(
Clight.Kcall id f e le k)
(
Kcall id tf te le tk).
Fixpoint nostackinfo (
adt:
stack) (
k:
cont) :
Prop :=
match k with
Kstop =>
True
|
Kseq _ k
|
Kblock k =>
nostackinfo adt k
|
Kcall oi f e te k =>
match adt with
| (
f,
_)::
r =>
nostackinfo r k /\
forall a ,
f =
Some a ->
Forall (
fun bfi =>
forall o,
frame_perm (
snd bfi)
o =
Public) (
frame_adt_blocks a)
|
_ =>
False
end
end.
Inductive match_states:
Clight.state ->
Csharpminor.state ->
Prop :=
|
match_state:
forall f nbrk ncnt s k e le m tf ts tk te ts'
tk'
cu
(
LINK:
linkorder cu prog)
(
TRF:
transl_function cu.(
prog_comp_env)
f =
OK tf)
(
TR:
transl_statement cu.(
prog_comp_env) (
Clight.fn_return f)
nbrk ncnt s =
OK ts)
(
MTR:
match_transl ts tk ts'
tk')
(
MENV:
match_env e te)
(
MK:
match_cont cu.(
prog_comp_env) (
Clight.fn_return f)
nbrk ncnt k tk)
(
TOPNOINFO:
nostackinfo (
Mem.stack m) (
Kcall None tf te le tk)),
match_states (
Clight.State f s k e le m)
(
State tf ts'
tk'
te le m)
|
match_callstate:
forall fd args k m tfd tk targs tres cconv cu ce sz
(
LINK:
linkorder cu prog)
(
TR:
match_fundef cu fd tfd)
(
MK:
match_cont ce Tvoid 0%
nat 0%
nat k tk)
(
ISCC:
Clight.is_call_cont k)
(
HDNIL:
top_tframe_tc (
Mem.stack m))
(
TOPNOINFO:
nostackinfo (
tl (
Mem.stack m))
tk)
(
TY:
type_of_fundef fd =
Tfunction targs tres cconv),
match_states (
Clight.Callstate fd args k m sz)
(
Callstate tfd args tk m sz)
|
match_returnstate:
forall res k m tk ce
(
MK:
match_cont ce Tvoid 0%
nat 0%
nat k tk)
(
TOPNOINFO:
nostackinfo (
tl (
Mem.stack m))
tk),
match_states (
Clight.Returnstate res k m)
(
Returnstate res tk m).
Remark match_states_skip:
forall f e le te nbrk ncnt k tf tk m cu,
linkorder cu prog ->
transl_function cu.(
prog_comp_env)
f =
OK tf ->
match_env e te ->
match_cont cu.(
prog_comp_env) (
Clight.fn_return f)
nbrk ncnt k tk ->
nostackinfo ((
Mem.stack m)) (
Kcall None tf te le tk) ->
match_states (
Clight.State f Clight.Sskip k e le m) (
State tf Sskip tk te le m).
Proof.
intros. econstructor; eauto. simpl; reflexivity. constructor.
Qed.
Commutation between label resolution and compilation
Section FIND_LABEL.
Variable ce:
composite_env.
Variable lbl:
label.
Variable tyret:
type.
Lemma transl_find_label:
forall s nbrk ncnt k ts tk
(
TR:
transl_statement ce tyret nbrk ncnt s =
OK ts)
(
MC:
match_cont ce tyret nbrk ncnt k tk),
match Clight.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 ce tyret nbrk'
ncnt'
s' =
OK ts'
/\
match_cont ce tyret nbrk'
ncnt'
k'
tk'
end
with transl_find_label_ls:
forall ls nbrk ncnt k tls tk
(
TR:
transl_lbl_stmt ce tyret nbrk ncnt ls =
OK tls)
(
MC:
match_cont ce tyret nbrk ncnt k tk),
match Clight.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 ce tyret nbrk'
ncnt'
s' =
OK ts'
/\
match_cont ce tyret nbrk'
ncnt'
k'
tk'
end.
Proof.
*
intro s;
case s;
intros;
try (
monadInv TR);
simpl.
-
auto.
-
unfold make_store,
make_memcpy in EQ3.
destruct (
access_mode (
typeof e));
monadInv EQ3;
auto.
-
auto.
-
simpl in TR.
destruct (
classify_fun (
typeof e));
monadInv TR.
auto.
-
auto.
-
exploit (
transl_find_label s0 nbrk ncnt (
Clight.Kseq s1 k));
eauto.
constructor;
eauto.
destruct (
Clight.find_label lbl s0 (
Clight.Kseq s1 k))
as [[
s'
k'] | ].
intros [
ts' [
tk' [
nbrk' [
ncnt' [
A [
B C]]]]]].
rewrite A.
exists ts';
exists tk';
exists nbrk';
exists ncnt';
auto.
intro.
rewrite H.
eapply transl_find_label;
eauto.
-
exploit (
transl_find_label s0);
eauto.
destruct (
Clight.find_label lbl s0 k)
as [[
s'
k'] | ].
intros [
ts' [
tk' [
nbrk' [
ncnt' [
A [
B C]]]]]].
rewrite A.
exists ts';
exists tk';
exists nbrk';
exists ncnt';
auto.
intro.
rewrite H.
eapply transl_find_label;
eauto.
-
exploit (
transl_find_label s0 1%
nat 0%
nat (
Kloop1 s0 s1 k));
eauto.
econstructor;
eauto.
destruct (
Clight.find_label lbl s0 (
Kloop1 s0 s1 k))
as [[
s'
k'] | ].
intros [
ts' [
tk' [
nbrk' [
ncnt' [
A [
B C]]]]]].
rewrite A.
exists ts';
exists tk';
exists nbrk';
exists ncnt';
auto.
intro.
rewrite H.
eapply transl_find_label;
eauto.
econstructor;
eauto.
-
auto.
-
auto.
-
simpl in TR.
destruct o;
monadInv TR.
auto.
auto.
-
assert (
exists b,
ts =
Sblock (
Sswitch b x x0)).
{
destruct (
classify_switch (
typeof e));
inv EQ2;
econstructor;
eauto. }
destruct H as [
b EQ3];
rewrite EQ3;
simpl.
eapply transl_find_label_ls with (
k :=
Clight.Kswitch k);
eauto.
econstructor;
eauto.
-
destruct (
ident_eq lbl l).
exists x;
exists tk;
exists nbrk;
exists ncnt;
auto.
eapply transl_find_label;
eauto.
-
auto.
*
intro ls;
case ls;
intros;
monadInv TR;
simpl.
-
auto.
-
exploit (
transl_find_label s nbrk ncnt (
Clight.Kseq (
seq_of_labeled_statement l)
k));
eauto.
econstructor;
eauto.
apply transl_lbl_stmt_2;
eauto.
destruct (
Clight.find_label lbl s (
Clight.Kseq (
seq_of_labeled_statement l)
k))
as [[
s'
k'] | ].
intros [
ts' [
tk' [
nbrk' [
ncnt' [
A [
B C]]]]]].
rewrite A.
exists ts';
exists tk';
exists nbrk';
exists ncnt';
auto.
intro.
rewrite H.
eapply transl_find_label_ls;
eauto.
Qed.
.
Properties of call continuations
Lemma match_cont_call_cont:
forall ce'
tyret'
nbrk'
ncnt'
ce tyret nbrk ncnt k tk,
match_cont ce tyret nbrk ncnt k tk ->
match_cont ce'
tyret'
nbrk'
ncnt' (
Clight.call_cont k) (
call_cont tk).
Proof.
induction 1; simpl; auto.
constructor.
econstructor; eauto.
Qed.
Lemma match_cont_is_call_cont:
forall ce tyret nbrk ncnt k tk ce'
tyret'
nbrk'
ncnt',
match_cont ce tyret nbrk ncnt k tk ->
Clight.is_call_cont k ->
match_cont ce'
tyret'
nbrk'
ncnt'
k tk /\
is_call_cont tk.
Proof.
intros. inv H; simpl in H0; try contradiction; simpl.
split; auto; constructor.
split; auto; econstructor; eauto.
Qed.
Lemma assign_loc_stack:
forall ty m b o v m',
assign_loc ge ty m b o v m' ->
Mem.stack m' =
Mem.stack m.
Proof.
Lemma nostackinfo_call_cont:
forall l k,
nostackinfo l k ->
nostackinfo l (
call_cont k).
Proof.
induction k; simpl; intros; eauto.
Qed.
Lemma find_label_nostackinfo:
forall lbl x tk'
ts'
tk''
l,
find_label lbl x tk' =
Some (
ts',
tk'') ->
nostackinfo l tk' ->
nostackinfo l tk''
with
find_label_ls_nostackinfo:
forall lbl x tk'
ts'
tk''
l,
find_label_ls lbl x tk' =
Some (
ts',
tk'') ->
nostackinfo l tk' ->
nostackinfo l tk''
.
Proof.
-
destruct x;
simpl;
intros;
try intuition congruence.
+
destruct (
find_label lbl x1 (
Kseq x2 tk'))
eqn:?.
inv H.
eapply find_label_nostackinfo in Heqo.
eauto.
simpl;
auto.
eapply find_label_nostackinfo in H;
eauto.
+
destruct (
find_label lbl x1 tk')
eqn:?.
inv H.
eapply find_label_nostackinfo in Heqo.
eauto.
simpl;
auto.
eapply find_label_nostackinfo in H;
eauto.
+
destruct (
find_label lbl x (
Kseq (
Sloop x)
tk'))
eqn:?.
inv H.
eapply find_label_nostackinfo in Heqo.
eauto.
simpl;
auto.
inv H.
+
destruct (
find_label lbl x (
Kblock tk'))
eqn:?.
inv H.
eapply find_label_nostackinfo in Heqo.
eauto.
simpl;
auto.
inv H.
+
eapply find_label_ls_nostackinfo in H;
eauto.
+
destruct (
ident_eq lbl l);
auto.
inv H.
auto.
eapply find_label_nostackinfo in H0;
eauto.
-
destruct x;
simpl;
intros;
try intuition congruence.
destruct (
find_label lbl s (
Kseq (
seq_of_lbl_stmt x)
tk'))
eqn:?.
inv H.
eapply find_label_nostackinfo in Heqo0.
eauto.
simpl;
auto.
eapply find_label_ls_nostackinfo in H;
eauto.
Qed.
:
forall e m l e'
m',
Clight.alloc_variables ge e m l e'
m' ->
Mem.stack m' =
Mem.stack m.
Proof.
The simulation proof
Lemma transl_step:
forall S1 t S2,
Clight.step2 fn_stack_requirements ge S1 t S2 ->
forall T1,
match_states S1 T1 ->
exists T2,
plus (
step fn_stack_requirements)
tge T1 t T2 /\
match_states S2 T2.
Proof.
Lemma transl_initial_states:
forall S,
Clight.initial_state fn_stack_requirements prog S ->
exists R,
initial_state fn_stack_requirements tprog R /\
match_states S R.
Proof.
Lemma transl_final_states:
forall S R r,
match_states S R ->
Clight.final_state S r ->
final_state R r.
Proof.
intros. inv H0. inv H. inv MK. constructor.
Qed.
Theorem transl_program_correct:
forward_simulation (
Clight.semantics2 fn_stack_requirements prog) (
Csharpminor.semantics fn_stack_requirements tprog).
Proof.
End CORRECTNESS.
End WITHEXTERNALCALLS.
Commutation with linking
Instance TransfCshmgenLink :
TransfLink match_prog.
Proof.