Require Import Sem SimProg Skeleton Mod ModSem SimMod SimModSem SimSymb SimMem Sound SimSymb.
Require Import Simulation Ctypes Cop Ctyping Csyntax ClightC.
Require SimMemId SimMemExt SimMemInj.
Require SoundTop UnreachC.
Require SimSymbId SimSymbDrop.
Require Import CoqlibC.
Require Import ValuesC.
Require Import LinkingC.
Require Import MapsC.
Require Import AxiomsC.
Require Import Ord.
Require Import MemoryC.
Require Import SmallstepC.
Require Import Events.
Require Import Preservation.
Require Import Integers.
Require Import LocationsC Conventions.
Require Import MatchSimModSem.
Require Import mktac.
Require Import IntegersC.
Require Import IdSimExtra ClightStepInj.
Set Implicit Arguments.
Local Opaque Z.mul Z.add Z.sub Z.div.
Inductive match_states_ext_clight (
sm_arg:
SimMemExt.t')
:
unit ->
state ->
state ->
SimMemExt.t' ->
Prop :=
|
match_ext_State
fn stmt K_src K_tgt env_src env_tgt tenv_src tenv_tgt m_src m_tgt sm0
(
MWFSRC:
m_src =
sm0.(
SimMemExt.src))
(
MWFTGT:
m_tgt =
sm0.(
SimMemExt.tgt))
(
MWF:
Mem.extends m_src m_tgt)
(
ENV:
match_env inject_id env_src env_tgt)
(
TENV:
match_temp_env inject_id tenv_src tenv_tgt)
(
CONT:
match_cont inject_id K_src K_tgt):
match_states_ext_clight
sm_arg tt
(
State fn stmt K_src env_src tenv_src m_src)
(
State fn stmt K_tgt env_tgt tenv_tgt m_tgt)
sm0
|
match_ext_Callstate
fptr_src fptr_tgt ty args_src args_tgt K_src K_tgt m_src m_tgt sm0
(
MWFSRC:
m_src =
sm0.(
SimMemExt.src))
(
MWFTGT:
m_tgt =
sm0.(
SimMemExt.tgt))
(
MWF:
Mem.extends m_src m_tgt)
(
INJ:
Val.lessdef fptr_src fptr_tgt)
(
VALS:
Val.lessdef_list args_src args_tgt)
(
CONT:
match_cont inject_id K_src K_tgt):
match_states_ext_clight
sm_arg tt
(
Callstate fptr_src ty args_src K_src m_src)
(
Callstate fptr_tgt ty args_tgt K_tgt m_tgt)
sm0
|
match_ext_Returnstate
retv_src retv_tgt K_src K_tgt m_src m_tgt sm0
(
MWFSRC:
m_src =
sm0.(
SimMemExt.src))
(
MWFTGT:
m_tgt =
sm0.(
SimMemExt.tgt))
(
MWF:
Mem.extends m_src m_tgt)
(
INJ:
Val.lessdef retv_src retv_tgt)
(
CONT:
match_cont inject_id K_src K_tgt):
match_states_ext_clight
sm_arg tt
(
Returnstate retv_src K_src m_src)
(
Returnstate retv_tgt K_tgt m_tgt)
sm0.
Section CLIGHTEXT.
Variable se:
Senv.t.
Variable ge:
genv.
Definition function_entry_extends
(
function_entry:
genv ->
function ->
list val ->
mem ->
env ->
temp_env ->
mem ->
Prop) :=
forall fn vs_src vs_tgt m_src0 m_tgt0 en tenv_src m_src1
(
MWF:
Mem.extends m_src0 m_tgt0)
(
VALS:
Val.lessdef_list vs_src vs_tgt)
(
ENTRY:
function_entry ge fn vs_src m_src0 en tenv_src m_src1),
exists tenv_tgt m_tgt1,
(<<
MWF:
Mem.extends m_src1 m_tgt1>>) /\
(<<
TENV:
match_temp_env inject_id tenv_src tenv_tgt>>) /\
(<<
ENTRY:
function_entry ge fn vs_tgt m_tgt0 en tenv_tgt m_tgt1>>).
Variable function_entry:
genv ->
function ->
list val ->
mem ->
env ->
temp_env ->
mem ->
Prop.
Hypothesis FUNCTIONENTRY:
function_entry_extends function_entry.
Lemma alloc_variables_extends idl en_src0 en_tgt0 en_src1 m_src0 m_tgt0 m_src1
(
ALLOC:
alloc_variables ge en_src0 m_src0 idl en_src1 m_src1)
(
ENV:
match_env inject_id en_src0 en_tgt0)
(
MWF:
Mem.extends m_src0 m_tgt0):
exists m_tgt1 en_tgt1,
(<<
MWF:
Mem.extends m_src1 m_tgt1>>) /\
(<<
ENV:
match_env inject_id en_src1 en_tgt1>>) /\
(<<
ALLOC:
alloc_variables ge en_src0 m_tgt0 idl en_src1 m_tgt1>>).
Proof.
revert m_src0 m_src1 m_tgt0 en_src0 en_tgt0 en_src1 ALLOC ENV MWF.
induction idl.
-
i.
inv ALLOC.
esplits;
eauto.
econs;
eauto.
-
i.
inv ALLOC.
exploit Mem.alloc_extends;
eauto;
try refl.
i.
des.
exploit IHidl;
eauto.
{
instantiate (1:=
PTree.set id (
b1,
ty)
en_tgt0).
ii.
repeat rewrite PTree.gsspec.
des_ifs.
left.
esplits;
ss. }
i.
des.
esplits;
eauto.
econs;
eauto.
Qed.
Lemma assign_loc_extends ce ty m_src0 m_tgt0 v_src v_tgt m_src1 blk ofs
(
ASSIGN:
assign_loc ce ty m_src0 blk ofs v_src m_src1)
(
VAL:
Val.lessdef v_src v_tgt)
(
MWF:
Mem.extends m_src0 m_tgt0):
exists m_tgt1,
(<<
ASSIGN:
assign_loc ce ty m_tgt0 blk ofs v_tgt m_tgt1>>) /\
(<<
MWF:
Mem.extends m_src1 m_tgt1>>).
Proof.
Lemma match_env_inject_id en:
match_env inject_id en en.
Proof.
ii. destruct (en ! id) eqn:ENV; eauto. destruct p. left. esplits; ss.
Qed.
Lemma bind_parameters_extends e_src e_tgt m_src0 m_tgt0 idl vargs_src vargs_tgt m_src1
(
BIND:
bind_parameters ge e_src m_src0 idl vargs_src m_src1)
(
ENV:
match_env inject_id e_src e_tgt)
(
MWF:
Mem.extends m_src0 m_tgt0)
(
VALS:
Val.lessdef_list vargs_src vargs_tgt):
exists m_tgt1,
(<<
MWF:
Mem.extends m_src1 m_tgt1>>) /\
(<<
BIND:
bind_parameters ge e_tgt m_tgt0 idl vargs_tgt m_tgt1>>).
Proof.
revert m_src0 m_tgt0 ENV vargs_src vargs_tgt m_src1 MWF VALS BIND.
induction idl.
-
i.
inv BIND.
inv VALS.
esplits;
eauto.
econs.
-
i.
inv BIND.
inv VALS.
destruct (
ENV id);
des;
clarify.
unfold inject_id in *.
clarify.
exploit assign_loc_extends;
eauto.
i.
des.
clarify.
exploit IHidl;
try apply H6;
eauto.
i.
des.
esplits;
eauto.
econs;
eauto.
Qed.
Lemma function_entry2_extends:
function_entry_extends function_entry2.
Proof.
Lemma function_entry1_extends:
function_entry_extends function_entry1.
Proof.
Lemma bool_val_extends m_src m_tgt ty v_src v_tgt b
(
VAL:
Val.lessdef v_src v_tgt)
(
MWF:
Mem.extends m_src m_tgt)
(
BVAL:
bool_val v_src ty m_src =
Some b):
bool_val v_tgt ty m_tgt =
Some b.
Proof.
Lemma sem_unary_operation_extends m_src m_tgt op v_src0 v_tgt0 v_src1 ty
(
EXT:
Mem.extends m_src m_tgt)
(
VAL:
Val.lessdef v_src0 v_tgt0)
(
SEM:
sem_unary_operation op v_src0 ty m_src =
Some v_src1)
:
exists v_tgt1,
(<<
SEM:
sem_unary_operation op v_tgt0 ty m_tgt =
Some v_tgt1>>) /\
(<<
VAL:
Val.lessdef v_src1 v_tgt1>>).
Proof.
Lemma sem_binary_operation_extends ce m_src m_tgt op
v_src0 v_tgt0 v_src1 v_tgt1 v_src2 ty0 ty1
(
SEM:
sem_binary_operation ce op v_src0 ty0 v_src1 ty1 m_src =
Some v_src2)
(
EXT:
Mem.extends m_src m_tgt)
(
VAL0:
Val.lessdef v_src0 v_tgt0)
(
VAL1:
Val.lessdef v_src1 v_tgt1):
exists v_tgt2,
(<<
SEM:
sem_binary_operation ce op v_tgt0 ty0 v_tgt1 ty1 m_tgt =
Some v_tgt2>>) /\
(<<
VAL:
Val.lessdef v_src2 v_tgt2>>).
Proof.
Lemma sem_cast_extends m_src m_tgt v_src0 v_tgt0 v_src1 ty0 ty1
(
EXT:
Mem.extends m_src m_tgt)
(
VAL:
Val.lessdef v_src0 v_tgt0)
(
SEM:
sem_cast v_src0 ty0 ty1 m_src =
Some v_src1):
exists v_tgt1,
(<<
SEM:
sem_cast v_tgt0 ty0 ty1 m_tgt =
Some v_tgt1>>) /\
(<<
VAL:
Val.lessdef v_src1 v_tgt1>>).
Proof.
Lemma deref_loc_extends ty m_src m_tgt blk ofs v_src
(
DEREF:
deref_loc ty m_src blk ofs v_src)
(
EXT:
Mem.extends m_src m_tgt):
exists v_tgt,
(<<
DEREF:
deref_loc ty m_tgt blk ofs v_tgt>>) /\
(<<
VAL:
Val.lessdef v_src v_tgt>>).
Proof.
inv DEREF.
-
exploit Mem.loadv_extends;
eauto.
i.
des.
esplits;
eauto.
econs 1;
eauto.
-
esplits;
eauto.
econs 2;
eauto.
-
esplits;
eauto.
econs 3;
eauto.
Qed.
Lemma eval_expr_lvalue_extends en_src en_tgt tenv_src tenv_tgt m_src m_tgt
(
ENV:
match_env inject_id en_src en_tgt)
(
TENV:
match_temp_env inject_id tenv_src tenv_tgt)
(
EXT:
Mem.extends m_src m_tgt):
(
forall exp v_src
(
EVAL:
eval_expr ge en_src tenv_src m_src exp v_src),
exists v_tgt,
(<<
EVAL:
eval_expr ge en_tgt tenv_tgt m_tgt exp v_tgt>>) /\
(<<
LESS:
Val.lessdef v_src v_tgt>>)) /\
(
forall exp blk ofs
(
EVAL:
eval_lvalue ge en_src tenv_src m_src exp blk ofs),
eval_lvalue ge en_tgt tenv_tgt m_tgt exp blk ofs).
Proof.
apply eval_expr_lvalue_ind;
i;
try by (
esplits;
eauto;
econs;
eauto).
-
cinv (
TENV id);
rewrite H in *;
clarify.
erewrite val_inject_id in *.
esplits;
eauto.
econs 5;
eauto.
-
des.
exploit sem_unary_operation_extends;
eauto.
i.
des.
esplits;
eauto.
econs;
eauto.
-
des.
exploit sem_binary_operation_extends;
eauto.
i.
des.
esplits;
eauto.
econs;
eauto.
-
des.
exploit sem_cast_extends;
eauto.
i.
des.
esplits;
eauto.
econs;
eauto.
-
des.
exploit deref_loc_extends;
eauto.
i.
des.
esplits;
eauto.
econs 12;
eauto.
-
cinv (
ENV id);
des;
clarify.
unfold inject_id in *.
clarify.
econs;
eauto.
-
cinv (
ENV id);
des;
clarify.
econs 2;
eauto.
-
des.
cinv LESS.
econs;
eauto.
-
des.
cinv LESS.
econs;
eauto.
-
des.
cinv LESS.
econs;
eauto.
Qed.
Lemma eval_expr_extends en_src en_tgt tenv_src tenv_tgt m_src m_tgt
(
ENV:
match_env inject_id en_src en_tgt)
(
TENV:
match_temp_env inject_id tenv_src tenv_tgt)
(
EXT:
Mem.extends m_src m_tgt)
exp v_src
(
EVAL:
eval_expr ge en_src tenv_src m_src exp v_src):
exists v_tgt,
(<<
EVAL:
eval_expr ge en_tgt tenv_tgt m_tgt exp v_tgt>>) /\
(<<
LESS:
Val.lessdef v_src v_tgt>>).
Proof.
Lemma eval_exprlist_extends en_src en_tgt tenv_src tenv_tgt m_src m_tgt tys
(
ENV:
match_env inject_id en_src en_tgt)
(
TENV:
match_temp_env inject_id tenv_src tenv_tgt)
(
EXT:
Mem.extends m_src m_tgt)
exps vs_src
(
EVALS:
eval_exprlist ge en_src tenv_src m_src exps tys vs_src):
exists vs_tgt,
(<<
EVALS:
eval_exprlist ge en_tgt tenv_tgt m_tgt exps tys vs_tgt>>) /\
(<<
LESS:
Val.lessdef_list vs_src vs_tgt>>).
Proof.
revert tys vs_src EVALS TENV EXT.
induction exps;
i.
-
inv EVALS.
exists [].
esplits;
eauto.
econs;
eauto.
-
inv EVALS.
exploit IHexps;
eauto.
i.
des.
exploit eval_expr_extends;
eauto.
i.
des.
exploit sem_cast_extends;
eauto.
i.
des.
exists (
v_tgt1 ::
vs_tgt).
esplits;
eauto.
econs;
eauto.
Qed.
Lemma eval_lvalue_extends en_src en_tgt tenv_src tenv_tgt m_src m_tgt
(
ENV:
match_env inject_id en_src en_tgt)
(
TENV:
match_temp_env inject_id tenv_src tenv_tgt)
(
EXT:
Mem.extends m_src m_tgt)
exp blk ofs
(
EVAL:
eval_lvalue ge en_src tenv_src m_src exp blk ofs):
eval_lvalue ge en_tgt tenv_tgt m_tgt exp blk ofs.
Proof.
Lemma free_list_extends_parallel
m_src0 m_tgt0 locs m_src1
(
MWF:
Mem.extends m_src0 m_tgt0)
(
FREE:
Mem.free_list m_src0 locs =
Some m_src1):
exists m_tgt1,
(<<
MWF:
Mem.extends m_src1 m_tgt1>>) /\
(<<
FREE:
Mem.free_list m_tgt0 locs =
Some m_tgt1>>).
Proof.
revert m_src0 m_tgt0 m_src1 FREE MWF.
induction locs;
ss.
-
i.
clarify.
esplits;
eauto.
-
i.
des_ifs_safe.
exploit Mem.free_parallel_extends;
eauto.
i.
des.
exploit IHlocs;
eauto.
i.
des.
esplits;
eauto.
rewrite H.
rewrite FREE0.
eauto.
Qed.
Lemma blocks_of_env_ext_match e_src e_tgt
(
ENV:
match_env inject_id e_src e_tgt):
(
blocks_of_env ge e_src) = (
blocks_of_env ge e_tgt).
Proof.
exploit PTree.elements_canonical_order.
-
instantiate (1:= @
eq (
block *
type)).
instantiate (1:=
e_tgt).
instantiate (1:=
e_src).
i.
unfold inject_id in *.
destruct (
ENV i);
des;
clarify.
esplits;
eauto;
ss.
-
i.
unfold inject_id in *.
destruct (
ENV i);
des;
clarify.
esplits;
eauto.
-
intros ALL.
unfold blocks_of_env.
revert ALL.
generalize (
PTree.elements e_tgt).
generalize (
PTree.elements e_src).
induction l;
ss;
i.
+
inv ALL.
econs.
+
inv ALL.
ss.
destruct a,
b1.
ss.
des.
clarify.
des_ifs;
ss.
f_equal.
exploit IHl;
eauto.
Qed.
Lemma clight_step_preserve_extension
sm_arg u st_src0 st_tgt0 st_src1 sm0 tr
(
MATCH:
match_states_ext_clight sm_arg u st_src0 st_tgt0 sm0)
(
STEP:
step se ge (
function_entry ge)
st_src0 tr st_src1):
exists st_tgt1 sm1,
(<<
STEP:
step se ge (
function_entry ge)
st_tgt0 tr st_tgt1>>) /\
(<<
MATCH:
match_states_ext_clight sm_arg u st_src1 st_tgt1 sm1>>).
Proof.
End CLIGHTEXT.
Lemma match_states_clight_get_mem st_src st_tgt j m_src m_tgt
(
MATCH:
match_states_clight_internal st_src st_tgt j m_src m_tgt):
(<<
MSRC:
st_src.(
get_mem) =
m_src>>) /\ (<<
MTGT:
st_tgt.(
get_mem) =
m_tgt>>).
Proof.
inv MATCH; ss. Qed.
Definition flattize_inj (
j:
meminj):
meminj :=
fun blk =>
match j blk with
|
Some _ =>
Some (
blk, 0)
|
_ =>
None
end.
Lemma flattize_inj_val j v v_tgt
(
VAL:
Val.inject j v v_tgt):
Val.inject (
flattize_inj j)
v v.
Proof.
destruct v;
ss.
inv VAL.
unfold flattize_inj.
econs;
eauto.
-
rewrite H1.
eauto.
-
psimpl.
auto.
Qed.
Lemma flattize_inj_env j env_src env_tgt
(
ENV:
match_env j env_src env_tgt):
match_env (
flattize_inj j)
env_src env_src.
Proof.
ii.
specialize (
ENV id).
des.
-
left.
esplits;
eauto.
unfold flattize_inj.
des_ifs.
-
right.
eauto.
Qed.
Lemma flattize_inj_temp_env j tenv_src tenv_tgt
(
TENV:
match_temp_env j tenv_src tenv_tgt):
match_temp_env (
flattize_inj j)
tenv_src tenv_src.
Proof.
Lemma flattize_inj_cont j K_src K_tgt
(
TENV:
match_cont j K_src K_tgt):
match_cont (
flattize_inj j)
K_src K_src.
Proof.
Lemma flattiize_inj_states j st_src st_tgt m_src m_tgt
(
MATCH:
match_states_clight_internal st_src st_tgt j m_src m_tgt):
match_states_clight_internal st_src st_src (
flattize_inj j)
m_src m_src.
Proof.
Section CLIGHTSOUNDSTATE.
Variable skenv_link:
SkEnv.t.
Variable su:
Sound.t.
Inductive sound_state_clight:
state ->
Prop :=
|
match_states_clight_intro
st j m
(
WF:
Sound.wf su)
(
MEM:
UnreachC.mem'
su m)
(
INJ:
j =
UnreachC.to_inj su su.(
Unreach.nb))
(
SKE:
su.(
Unreach.ge_nb) =
skenv_link.(
Genv.genv_next))
(
SKLE:
Ple skenv_link.(
Genv.genv_next)
su.(
Unreach.nb))
(
MATCHST:
match_states_clight_internal st st j m m):
sound_state_clight st.
End CLIGHTSOUNDSTATE.
Require Import Program.
Section CLIGHTSOUND.
Variable skenv_link:
SkEnv.t.
Lemma clight_unreach_local_preservation clight:
exists sound_state, <<
PRSV:
local_preservation (
modsem2 skenv_link clight)
sound_state>>.
Proof.
End CLIGHTSOUND.