Library FminortoCminor_proof1
Require Import List.
Require Import Coqlib.
Require Import Coqlib2.
Require Import AST.
Require Import Globalenvs.
Require Import Maps.
Require Import Mml.
Require Import Mml_pre.
Require Import FSets.
Require Import FSetAVL.
Require Import Ordered.
Require Import Compare_dec.
Require Import EqNat.
Require Import Fminor.
Require Import Cminor.
Require Import Op.
Require Import Integers.
Require Import Cmconstr.
Require Import Values.
Require Import Cmconstrproof.
Require Import Mem.
Require Import FminortoCminor.
Require Import Switch.
Open Scope Z_scope.
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.
Fixpoint exprlist_size (l: exprlist) {struct l}:nat:=
match l with |Enil => O | (a:::m) => S (exprlist_size m) end.
Intermediate properties
Lemma same_size :
forall ge sp tle e tm1 l t tm2 lv,
eval_exprlist ge sp tle e tm1 l t tm2 lv ->
List.length lv = exprlist_size l.
Lemma set_1:
forall d v l e1,
set_loc_par d v l = Some e1 -> length d = length v.
Lemma sig_1:
forall A B p t,
length p = S ( length t) ->
map (fun _ : A => Tint) p =
Tint::map (fun _ : B => Tint) t.
Lemma root_get:
forall l r e,
~In r l -> PTree.get r (set_locals l e)= PTree.get r e.
Lemma max_signed_unsigned :
Int.max_signed < Int.max_unsigned.
Lemma min_signed_neg:
Int.min_signed < 0.
Lemma bounds_signed :
Int.min_signed <= 0 <= Int.max_signed.
Lemma max_sig_inf_mod:
Int.max_signed < modulus.
Lemma comp_max_signed_eq:
forall n m ,
0<=n < Int.max_signed ->
0<=m < Int.max_signed ->
Int.repr n = Int.repr m -> n =m.
Lemma comp_max_signed_neq:
forall n1 n2,
0<=n1 < Int.max_signed ->
0<=n2 < Int.max_signed ->
n1<>n2 ->
Int.repr n1 <> Int.repr n2.
Lemma comp_max_neq_inv:
forall n1 n2,
0<=n1 < Int.max_signed ->
0<=n2 < Int.max_signed ->
Int.repr n1 <> Int.repr n2 ->
n1<>n2.
Load and write of la list of n offset of 4 words
Fixpoint loadlist (m:mem) (b:block) (pos : Z) (nbr:nat) {struct nbr}: option (list val):=
match nbr with
| O => Some nil
| S k =>
do v<-load Mint32 m b pos;
do lv <-loadlist m b (pos+4) k;
Some (v::lv)
end.
Lemma loadlist_sm_sz :
forall n m b pos lv,
loadlist m b pos n = Some lv ->
length lv = n .
Lemma loadlist_nth:
forall lv m b k v n,
loadlist m b k (length lv) = Some lv ->
nth_error lv n = Some v ->
load Mint32 m b (k+(Z_of_nat n)*4) = Some v.
Lemma loadlist_incr:
forall nbr pos m b l m' ofs x chunk sp,
b<>sp ->
loadlist m b pos nbr = Some l ->
store chunk m sp ofs x = Some m' ->
loadlist m' b pos nbr = Some l.
Lemma load_same_loadlist:
forall m1 m2 b,
(forall delta , load Mint32 m1 b delta =
load Mint32 m2 b delta)->
forall m k, loadlist m1 b k m = loadlist m2 b k m.
Lemma loadlist_alloc_other:
forall k m b ofs l n1 n2 ma a
(LDL: loadlist m b ofs k = Some l)
(ALL: alloc m n1 n2 = (ma,a)),
loadlist ma b ofs k = Some l.
Lemma loadlist_store_other:
forall k m b ofs l spa ma j v
(LDL: loadlist m b ofs k = Some l)
(NEQ: b<>spa)
(ST: store Mint32 m spa j v = Some ma),
loadlist ma b ofs k = Some l.
Lemma loadlist_free:
forall k m b ofs l spa
(LDL: loadlist m b ofs k = Some l)
(NEQ: b<>spa) ,
loadlist (free m spa) b ofs k = Some l.
Fixpoint storelist (m:mem) (b:block) (ofs:Z)
(l : list val) {struct l}:option mem:=
match l with
| nil => Some m
| v::k =>
do m' <- store Mint32 m b ofs v;
storelist m' b (ofs+4) k
end.
Lemma storelist_store_once :
forall l m b b' ofs m' ofs' chunk,
storelist m b ofs l = Some m' ->
b'<>b \/ ofs' +(size_chunk chunk) <= ofs \/
ofs+ (Z_of_nat (length l))*4<= ofs' ->
load chunk m b' ofs' =
load chunk m' b' ofs'.
Lemma storelist_load :
forall n l m b ofs m' v ,
storelist m b ofs l = Some m' ->
nth_error l n = Some v ->
load Mint32 m' b (ofs+Z_of_nat n *4) = Some (Val.load_result Mint32 v).
Lemma list_in_ok :
forall l ao,
(forall a , In a (ao::l) -> (exists i , a= Vint i) \/(exists b , exists o, a= Vptr b o)) ->
(forall a , In a l -> (exists i, a=Vint i) \/ (exists b, exists o, a= Vptr b o)).
Lemma storelist_loadlist :
forall l m b ofs m' ,
(forall a, In a l -> (exists i,a= Vint i) \/ (exists b, exists o,a=Vptr b o) ) ->
storelist m b ofs l = Some m' ->
loadlist m' b ofs (length l)= Some l .
Lemma storelist_in_bounds:
forall l m b ofs,
valid_block m b ->
low_bound m b <= ofs ->
(ofs + ((Z_of_nat (length l))*4)) <= high_bound m b ->
exists tm , storelist m b ofs l = Some tm.
Lemma valid_block_storelist:
forall l m b ofs mf
(STL: storelist m b ofs l = Some mf),
forall z, valid_block m z ->valid_block mf z.
Lemma low_bound_storelist:
forall l m b ofs mf
(STL: storelist m b ofs l = Some mf),
forall z, low_bound mf z = low_bound m z.
Lemma high_bound_storelist:
forall l m b ofs mf
(STL: storelist m b ofs l = Some mf),
forall z, high_bound mf z = high_bound m z.
Lemma load_storelist_other:
forall l m b ofs mf
(STL: storelist m b ofs l = Some mf),
forall (chunk' : memory_chunk) (b' : block) (ofs' : Z),
b' <> b \/
ofs' + size_chunk chunk' <= ofs \/ ofs + (Z_of_nat (length l)*4) <= ofs' ->
load chunk' mf b' ofs' = load chunk' m b' ofs'.
Lemma loadlist_storelist_other:
forall cv k ma b cl ofs z0 n mf,
loadlist ma b ofs k = Some cl->
storelist ma z0 n cv = Some mf ->
b <>z0 ->
loadlist mf b ofs k = Some cl.
Local environment building for function call evaluation
Fixpoint set_params2 (lv:list val) (li : list ident) (e:env) {struct li}:env:=
match li,lv with
| id::lid,v::lv' =>
(set_params2 lv' lid (PTree.set id v e))
| _,_ => e
end .
Definition env_equiv (e1 e2:env):Prop:=
forall id , e1!id = e2!id.
Lemma equiv_refl:
forall e, env_equiv e e.
Lemma equiv_trans:
forall e1 e2 e3, env_equiv e1 e2 -> env_equiv e2 e3->
env_equiv e1 e3.
Lemma equiv_sym:
forall e e', env_equiv e e' -> env_equiv e' e.
Lemma set_set_equiv:
forall i i' v v' e ,
(i<>i') ->
env_equiv (PTree.set i v (PTree.set i' v' e))
(PTree.set i' v' (PTree.set i v e)) .
Lemma set_equiv:
forall a v e e' ,
env_equiv e e' ->
env_equiv (PTree.set a v e) (PTree.set a v e').
Lemma set_params2_env_equiv:
forall lv li e e' ,
length lv =length li->
env_equiv e e' ->
env_equiv (set_params2 lv li e) (set_params2 lv li e').
Lemma set_params_comm:
forall lv li a v e,
list_norepet (a::li) ->
length lv = length li ->
env_equiv
(set_params2 lv li (PTree.set a v e))
(PTree.set a v (set_params2 lv li e)).
Lemma set_params_set_params2_equiv:
forall li lv,
list_norepet li->
length li = length lv ->
env_equiv (set_params2 lv li (PTree.empty val) ) (set_params lv li) .
Lemma set_disjoint_prop:
forall l lx a e1 v,
list_disjoint lx l ->
(forall id : positive, In id lx -> a ! id = None) ->
set_loc_par l v a= Some e1 ->
forall id : positive, In id lx -> e1 ! id = None.
Pure expressions evaluation
Definition Eve := Events.E0.
Remark Eve_app:
Eve = Events.Eapp Eve Eve .
Definition Eval_expr (g:genv)
(sp:val) (e:env) (m:mem) (t:expr) (v:block):Prop:=
eval_expr g sp nil e m t Eve m (Vptr v Int.zero).
Inductive Eval_exprlist:
genv->val -> env -> mem -> exprlist -> list block -> Prop :=
| eval_Enil:
forall g sp e m,
eval_exprlist g sp nil e m Enil Eve m nil->
Eval_exprlist g sp e m Enil nil
| eval_Econs:
forall g sp e m a bl v vl,
Eval_expr g sp e m a v ->
Eval_exprlist g sp e m bl vl ->
Eval_exprlist g sp e m (Econs a bl) (v :: vl).
Lemma eval_Eval_conversion:
forall g sp e m tl vl, Eval_exprlist g sp e m tl vl ->
eval_exprlist g sp nil e m tl Eve m (map (fun x=> Vptr x Int.zero) vl).
Smart constructors evaluation
Lemma eval_intconst:
forall g sp e m z tle ,
eval_expr g sp tle e m (intconst z) Eve m (Vint (Int.repr z)).
Lemma eval_addrsymbol:
forall ge sp tle tm1 e s b ,
Genv.find_symbol ge s= Some b ->
eval_expr ge sp tle e tm1 (addrsymbol s) Eve tm1 (Vptr b Int.zero).
Lemma eval_addrstack :
forall ge sp tle tm1 e n addr , offset_sp sp n = Some addr ->
eval_expr ge sp tle e tm1 (addrstack n) Eve tm1 addr.
Lemma eval_addimm:
forall ge sp tle tm1 ce1 e n v1 v tm2,
eval_expr ge sp tle ce1 tm1 e Eve tm2 v1 ->
eval_operation ge sp Oadd (v1::(Vint (Int.repr n))::nil) tm2 = Some v ->
eval_expr ge sp tle ce1 tm1 (addimm e n) Eve tm2 v.
Lemma exec_Sstore:
forall ge sp e m1 m2 m3 m4 v1 v2 chunk a1 a2,
eval_expr ge sp nil e m1 a1 Eve m2 v1 ->
eval_expr ge sp nil e m2 a2 Eve m3 v2 ->
storev chunk m3 v1 v2 = Some m4 ->
exec_stmt ge sp e m1 (Sstore chunk a1 a2)
Eve e m4 Out_normal.
Lemma eval_Scall:
forall ge sp e m m0 m2 m1 id s f vf cf args vargs v,
eval_expr ge sp nil e m f Eve m0 vf ->
eval_exprlist ge sp nil e m0 args Eve m2 vargs ->
Genv.find_funct ge vf = Some cf ->funsig cf = s ->
eval_funcall ge m2 cf vargs Eve m1 v ->
exec_stmt ge sp e m (Scall id s f args ) Eve
(PTree.set id v e) m1 Out_normal.
Lemma match_body_length:
forall m , length (match_body m ) = m.
Lemma match_body_rec_target:
forall m n,
lt n m ->
nth_error (match_body m) n=
Some (Int.repr (Z_of_nat (m-(S n))), (m-(S n))%nat).
Lemma swith_match_body:
forall m n dft,
lt n m ->
(Z_of_nat m ) <Int.max_signed ->
(switch_target (Int.repr (Z_of_nat n)) dft
(match_body m)) = n.
Lemma eval_match_body_ok :
forall nb ge sp e m a m1 n ,
Z_of_nat nb < Int.max_signed -> lt n nb ->
eval_expr ge sp nil e m a Eve m1 (Vint (Int.repr (Z_of_nat n))) ->
exec_stmt ge sp e m
(Sswitch a (match_body nb ) nb) Eve e m1 (Out_exit n) .
Lemma exec_fold_return:
forall sl ge sp e a m m2 e1 out,
exec_stmt ge sp e m a Eve e1 m2 out ->
((exists v : val, out = Out_return (Some v)) \/
(exists v : val, out = Out_tailcall_return v)) ->
exec_stmt ge sp e m
(fold_bl_rec sl a ((length sl) - 1)) Eve e1 m2 out.
Lemma exec_fold_tail:
forall sl ge sp e m a m1 m2 n case e1 out ,
Z_of_nat (length sl) < Int.max_signed ->lt n (length sl) ->
exec_stmt ge sp e m a Eve e m1 (Out_exit n ) ->
nth_error sl n = Some case ->
exec_stmt ge sp e m1 case Eve e1 m2 out ->
(((exists v, out = Out_return (Some v)) \/
(exists v, out = Out_tailcall_return v) ) ->
exec_stmt ge sp e m (fold_bl_rec sl a (length sl -1) ) Eve e1 m2 out).
Lemma exec_fold_cont:
forall sl a0 ge sp e m e1 m2,
exec_stmt ge sp e m a0 Eve e1 m2 (Out_exit (length sl)) ->
exec_stmt ge sp e m
(fold_bl_rec sl a0 (length sl -1)) Eve e1 m2 Out_normal.
Lemma exec_fold:
forall sl ge sp e m a m1 m2 n case e1 out ,
Z_of_nat (length sl) < Int.max_signed ->lt n (length sl) ->
exec_stmt ge sp e m a Eve e m1 (Out_exit n ) ->
nth_error sl n = Some case ->
exec_stmt ge sp e m1 case Eve e1 m2 out ->
(out= Out_normal \/
((exists v, out = Out_return (Some v)) \/
(exists v, out = Out_tailcall_return v) )) ->
exec_stmt ge sp e m (fold_bl_rec sl a (length sl -1) )
Eve e1 m2 out.
Lemma exec_Smatch :
forall ge sp e m cstr m2 vctrs cases case out e1,
Z_of_nat (length cases) < Int.max_signed ->
eval_expr ge sp nil e m cstr Eve m (Vint (Int.repr (Z_of_nat vctrs))) ->
nth_error cases vctrs = Some case ->
exec_stmt ge sp e m case Eve e1 m2 out->
(out= Out_normal \/
((exists v, out = Out_return (Some v)) \/
(exists v, out = Out_tailcall_return v) )) ->
exec_stmt ge sp e m (Smatch cstr cases) Eve e1 m2 out .
Lemma exec_mkmatch :
forall ge sp e m cstr m2 vctrs cases case out e1,
Z_of_nat (length cases) < Int.max_signed ->
eval_expr ge sp nil e m cstr Eve m (Vint (Int.repr (Z_of_nat vctrs))) ->
nth_error cases vctrs = Some case ->
exec_stmt ge sp e m case Eve e1 m2 out ->
(out= Out_normal \/
((exists v, out = Out_return (Some v)) \/
(exists v, out = Out_tailcall_return v) )) ->
exec_stmt ge sp e m (mkmatch cstr cases) Eve e1 m2 out.
Definition int_of_nat (n:nat):=
Int.repr (Z_of_nat n).