-
Notifications
You must be signed in to change notification settings - Fork 5
/
IdSimClightIdInv.v
156 lines (135 loc) · 4.96 KB
/
IdSimClightIdInv.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
Require Import Program.
Require Import Sem SimProg Skeleton Mod ModSem SimMod SimModSem SimSymb SimMem Sound SimSymb.
Require Import Cop Ctypes ClightC.
Require Import AsmC.
Require SimMemInjInvC.
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 Conventions1C.
Require Import MatchSimModSem.
Require Import IntegersC.
Require Import Coq.Logic.PropExtensionality.
Require Import CtypingC.
Require Import CopC.
Require Import MatchSimModSem.
Require Import Conventions1C.
Require Import ClightStepInj.
Require Import IdSimExtra IdSimInvExtra IdSimClightExtra.
Require Import mktac.
Set Implicit Arguments.
Local Opaque Z.mul Z.add Z.sub Z.div.
Section INJINV.
Variable P: SimMemInjInv.memblk_invariant.
Local Instance SimMemP: SimMem.class := SimMemInjInvC.SimMemInjInv SimMemInjInv.top_inv P.
Local Instance SimSymbP: SimSymb.class SimMemP := SimMemInjInvC.SimSymbIdInv P.
Local Existing Instance SoundTop.Top.
Inductive match_states_clight_inv
: unit -> Clight.state -> Clight.state -> SimMem.t -> Prop :=
| match_states_clight_intro
st_src st_tgt j m_src m_tgt sm0
(MWFSRC: m_src = sm0.(SimMem.src))
(MWFTGT: m_tgt = sm0.(SimMem.tgt))
(MWFINJ: j = sm0.(SimMemInjInv.minj).(SimMemInj.inj))
(MATCHST: match_states_clight_internal st_src st_tgt j m_src m_tgt)
(MWF: SimMem.wf sm0)
:
match_states_clight_inv
tt st_src st_tgt sm0
.
Lemma clight_inj_inv_id
(clight: Clight.program)
(WF: Sk.wf (module2 clight))
:
exists mp,
(<<SIM: ModPair.sim mp>>)
/\ (<<SRC: mp.(ModPair.src) = (module2 clight)>>)
/\ (<<TGT: mp.(ModPair.tgt) = (module2 clight)>>)
.
Proof.
eexists (ModPair.mk _ _ _); s. instantiate (3:= (SimMemInjInvC.mk bot1 _ _)).
esplits; eauto.
econs; ss; i.
{ econs; ss; i; clarify. }
eapply match_states_sim with (match_states := match_states_clight_inv); ss.
- apply unit_ord_wf.
- eapply SoundTop.sound_state_local_preservation.
- i. ss. exploit SimSymbIdInv_match_globals.
{ inv SIMSKENV. ss. eauto. } intros GEMATCH.
inv INITTGT. inv SAFESRC. inv SIMARGS; ss. inv H. ss.
exploit match_globals_find_funct; eauto.
i. clarify.
esplits; eauto.
+ econs; eauto.
+ refl.
+ econs; eauto. econs; eauto.
{ inv TYP. inv TYP0. eapply inject_list_typify_list; eauto. }
econs.
- i. ss. exploit SimSymbIdInv_match_globals.
{ inv SIMSKENV. ss. eauto. } intros GEMATCH.
des. inv SAFESRC. inv SIMARGS; ss. esplits. econs; ss.
+ eapply match_globals_find_funct; eauto.
+ inv TYP. econs; eauto.
erewrite <- inject_list_length; eauto.
- i. ss. inv MATCH; eauto.
- i. ss. clear SOUND. inv CALLSRC. inv MATCH. inv MATCHST. inv SIMSKENV. ss.
esplits; eauto.
+ econs; ss; eauto.
* eapply SimSymbIdInv_find_None; eauto.
ii. clarify. ss. des. clarify.
* des. clear EXTERNAL.
unfold Genv.find_funct, Genv.find_funct_ptr in *. des_ifs_safe.
inv INJ. inv SIMSKELINK. inv INJECT. exploit IMAGE; eauto.
{ left. eapply Genv.genv_defs_range; eauto. }
{ i. des. clarify. inv SIMSKENV. des_ifs. esplits; eauto. }
+ econs; ss.
+ refl.
+ instantiate (1:=top4). ss.
- i. ss. clear SOUND HISTORY.
exists (SimMemInjInvC.unlift' sm_arg sm_ret).
inv AFTERSRC. inv MATCH. inv MATCHST.
esplits; eauto.
+ econs; eauto. inv SIMRET; ss.
+ inv SIMRET; ss. econs; eauto. econs; eauto.
{ eapply inject_typify; et. }
ss. eapply match_cont_incr; try eassumption.
inv MLE. inv MLE1. inv MLE0. inv MLE. etrans; eauto.
+ refl.
- i. ss. inv FINALSRC. inv MATCH. inv MATCHST. inv CONT.
esplits; eauto.
+ econs.
+ econs; eauto.
+ refl.
- left. i. split.
+ eapply modsem2_receptive.
+ ii. inv MATCH. destruct sm0 as [sm0 mem_inv_src mem_inv_tgt].
cinv MWF. cinv WF0. ss.
exploit clight_step_preserve_injection2; try eassumption.
{ instantiate (1:=cgenv skenv_link_tgt clight). ss. }
{ eapply function_entry2_inject. ss. }
{ inv SIMSKENV. ss.
exploit SimMemInjInvC.skenv_inject_symbols_inject; eauto. }
{ inv SIMSKENV. ss. exploit SimSymbIdInv_match_globals; eauto. } i. des.
exploit SimMemInjC.parallel_gen; eauto. i. des.
hexploit SimMemInjInv.le_inj_wf_wf; eauto.
{ eapply SimMemInjInv.private_unchanged_on_invariant; eauto.
- ii. exploit INVRANGETGT; eauto. i. des. inv MWF. eapply Plt_Ple_trans; eauto.
- eapply Mem.unchanged_on_implies; eauto.
i. exploit INVRANGETGT; eauto. i. des. eauto. } intros MWFINV0.
esplits; eauto.
* left. apply plus_one. econs; ss; eauto.
eapply modsem2_determinate.
* instantiate (1:=SimMemInjInv.mk _ _ _). econs; ss; eauto.
* econs; ss; eauto.
Unshelve. apply 0.
Qed.
End INJINV.