1 | include "joint/semantics_paolo.ma". |
---|
2 | include alias "common/Identifiers.ma". |
---|
3 | |
---|
4 | (*** Store/retrieve on pseudo-registers ***) |
---|
5 | |
---|
6 | axiom BadRegister : String. |
---|
7 | |
---|
8 | definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v. |
---|
9 | |
---|
10 | definition reg_retrieve : register_env beval → register → res beval ≝ |
---|
11 | λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg). |
---|
12 | |
---|
13 | (*** Store/retrieve on hardware registers ***) |
---|
14 | |
---|
15 | definition init_hw_register_env: address → hw_register_env ≝ |
---|
16 | λaddr. |
---|
17 | let 〈dpl,dph〉 ≝ addr in |
---|
18 | let env ≝ hwreg_store RegisterDPH dph empty_hw_register_env in |
---|
19 | hwreg_store RegisterDPL dpl env. |
---|
20 | |
---|
21 | (******************************** GRAPHS **************************************) |
---|
22 | |
---|
23 | definition graph_pointer_of_label : cpointer → label → res cpointer ≝ |
---|
24 | λoldpc,l. |
---|
25 | return (mk_pointer Code |
---|
26 | (mk_block Code (block_id (pblock oldpc))) ? (mk_offset (pos (word_of_identifier … l))) : cpointer). |
---|
27 | % qed. |
---|
28 | |
---|
29 | definition graph_label_of_pointer: pointer → res label ≝ |
---|
30 | λp. OK … (an_identifier ? (match offv (poff p) with [ OZ ⇒ one | pos x ⇒ x | neg x ⇒ x ])). |
---|
31 | |
---|
32 | definition graph_fetch_statement: |
---|
33 | ∀pars : graph_params. |
---|
34 | ∀sem_pars : sem_state_params. |
---|
35 | ∀globals. |
---|
36 | genv globals pars → |
---|
37 | cpointer → |
---|
38 | res (joint_statement pars globals) ≝ |
---|
39 | λpars,sem_pars,globals,ge,p. |
---|
40 | do f ← fetch_function … ge p ; |
---|
41 | do l ← graph_label_of_pointer p; |
---|
42 | opt_to_res ? [MSG BadProgramCounter] (lookup ?? (joint_if_code … f) l). |
---|
43 | |
---|
44 | definition make_sem_graph_params : |
---|
45 | ∀pars : graph_params. |
---|
46 | ∀g_pars : more_sem_genv_params pars. |
---|
47 | sem_params ≝ |
---|
48 | λpars,g_pars. |
---|
49 | mk_sem_params |
---|
50 | pars |
---|
51 | (mk_more_sem_params |
---|
52 | pars |
---|
53 | g_pars |
---|
54 | graph_pointer_of_label |
---|
55 | (λ_.λ_.graph_pointer_of_label) |
---|
56 | (graph_fetch_statement ? g_pars) |
---|
57 | ). |
---|
58 | |
---|
59 | (******************************** LINEAR **************************************) |
---|
60 | check mk_pointer |
---|
61 | definition lin_succ_p: cpointer → unit → res cpointer := |
---|
62 | λptr.λ_.return «mk_pointer Code (pblock ptr) ? (mk_offset (offv (poff ptr) + 1)), ?». |
---|
63 | [%| cases ptr //] qed. |
---|
64 | |
---|
65 | axiom BadLabel: String. |
---|
66 | |
---|
67 | definition lin_pointer_of_label: |
---|
68 | ∀pars : lin_params. |
---|
69 | ∀globals. genv globals pars → cpointer → label → res cpointer ≝ |
---|
70 | λpars,globals,ge,old,l. |
---|
71 | do fn ← fetch_function … ge old ; |
---|
72 | do pos ← |
---|
73 | opt_to_res ? [MSG BadLabel] |
---|
74 | (position_of ? |
---|
75 | (λs. let 〈l',x〉 ≝ s in |
---|
76 | match l' with [ None ⇒ false | Some l'' ⇒ if eq_identifier … l l'' then true else false]) |
---|
77 | (joint_if_code … pars fn)) ; |
---|
78 | OK … (mk_Sig … (mk_pointer Code (mk_block Code (block_id (pblock old))) ? (mk_offset pos)) ?). |
---|
79 | % qed. |
---|
80 | |
---|
81 | definition lin_fetch_statement: |
---|
82 | ∀pars : lin_params. |
---|
83 | ∀sem_pars : sem_state_params. |
---|
84 | ∀globals. |
---|
85 | genv globals pars → cpointer → res (joint_statement pars globals) ≝ |
---|
86 | λpars,sem_pars,globals,ge,ppc. |
---|
87 | do fn ← fetch_function … ge ppc ; |
---|
88 | let off ≝ abs (offv (poff ppc)) in (* The offset should always be positive! *) |
---|
89 | do found ← opt_to_res ? [MSG BadProgramCounter] (nth_opt ? off (joint_if_code … fn)) ; |
---|
90 | return (\snd found). |
---|
91 | |
---|
92 | definition make_sem_lin_params : |
---|
93 | ∀pars : lin_params. |
---|
94 | ∀g_pars : more_sem_genv_params pars. |
---|
95 | sem_params ≝ |
---|
96 | λpars,g_pars. |
---|
97 | mk_sem_params |
---|
98 | pars |
---|
99 | (mk_more_sem_params |
---|
100 | pars |
---|
101 | g_pars |
---|
102 | lin_succ_p |
---|
103 | (lin_pointer_of_label ?) |
---|
104 | (lin_fetch_statement ? g_pars) |
---|
105 | ). |
---|
106 | |
---|
107 | definition step_unbranching : ∀p,globals.joint_step p globals → bool ≝ |
---|
108 | λp,globals,stp.match stp with |
---|
109 | [ COND _ _ ⇒ false |
---|
110 | | CALL_ID _ _ _ ⇒ false |
---|
111 | | extension c' ⇒ (* FIXME: does not care about calling extensions!! *) |
---|
112 | match ext_step_labels … c' with |
---|
113 | [ nil ⇒ true |
---|
114 | | _ ⇒ false |
---|
115 | ] |
---|
116 | | _ ⇒ true |
---|
117 | ]. |
---|
118 | |
---|
119 | definition is_not_seq : ∀p,globals.joint_statement p globals → bool ≝ |
---|
120 | λp,globals,stp.match stp with |
---|
121 | [ sequential _ _ ⇒ false |
---|
122 | | _ ⇒ true |
---|
123 | ]. |
---|
124 | |
---|
125 | inductive s_block (p : params) (globals : list ident) : Type[0] ≝ |
---|
126 | | Skip : s_block p globals |
---|
127 | | FinStep : (Σs.bool_to_Prop (¬step_unbranching p globals s)) → s_block p globals |
---|
128 | | FinStmt : (Σs.bool_to_Prop (is_not_seq p globals s)) → s_block p globals |
---|
129 | | Cons : (Σs.bool_to_Prop (step_unbranching p globals s)) → s_block p globals → s_block p globals. |
---|
130 | |
---|
131 | include "utilities/bind_new.ma". |
---|
132 | |
---|
133 | definition Block ≝ λp : params.λglobals.bind_new (localsT p) (s_block p globals). |
---|
134 | |
---|
135 | definition Bcons ≝ λp : params.λglobals. |
---|
136 | λs : Σs.bool_to_Prop (step_unbranching p globals s). |
---|
137 | λB : Block p globals. |
---|
138 | ! b ← B ; return Cons ?? s b. |
---|
139 | |
---|
140 | interpretation "block cons" 'vcons hd tl = (Bcons ??? hd tl). |
---|
141 | |
---|
142 | let rec is_unbranching p globals (b1 : s_block p globals) on b1 : bool ≝ |
---|
143 | match b1 with |
---|
144 | [ Skip ⇒ true |
---|
145 | | FinStep _ ⇒ false |
---|
146 | | FinStmt _ ⇒ false |
---|
147 | | Cons _ tl ⇒ is_unbranching ?? tl |
---|
148 | ]. |
---|
149 | |
---|
150 | let rec Is_unbranching p globals (b1 : Block p globals) on b1 : Prop ≝ |
---|
151 | match b1 with |
---|
152 | [ bret b ⇒ bool_to_Prop (is_unbranching … b) |
---|
153 | | bnew f ⇒ ∀x.Is_unbranching … (f x) |
---|
154 | ]. |
---|
155 | |
---|
156 | let rec s_block_append_aux p globals (b1 : s_block p globals) (b2 : s_block p globals) on b1 : is_unbranching … b1 → s_block p globals ≝ |
---|
157 | match b1 return λx.is_unbranching ?? x → ? with |
---|
158 | [ Skip ⇒ λ_.b2 |
---|
159 | | Cons x tl ⇒ λprf.Cons ?? x (s_block_append_aux ?? tl b2 prf) |
---|
160 | | _ ⇒ Ⓧ |
---|
161 | ]. |
---|
162 | |
---|
163 | definition s_block_append ≝ |
---|
164 | λp,globals.λb1 : Σb.bool_to_Prop (is_unbranching … b).λb2. |
---|
165 | match b1 with |
---|
166 | [ mk_Sig b1 prf ⇒ s_block_append_aux p globals b1 b2 prf ]. |
---|
167 | |
---|
168 | definition Is_to_is_unbr : ∀p,globals.(ΣB.Is_unbranching p globals B) → |
---|
169 | bind_new (localsT p) (Σb.bool_to_Prop (is_unbranching p globals b)) ≝ |
---|
170 | λp,globals. ?. |
---|
171 | * #b elim b -b |
---|
172 | [ #b #H @bret @b @H |
---|
173 | | #f #IH #H @bnew #x @(IH x) @H |
---|
174 | ] |
---|
175 | qed. |
---|
176 | |
---|
177 | lemma Is_to_is_unbr_OK : ∀p,globals,B.! b ← Is_to_is_unbr p globals B ; return pi1 … b = pi1 … B. |
---|
178 | #p #globals * #b elim b |
---|
179 | [ // |
---|
180 | | #f #IH #H @bnew_proper |
---|
181 | #x @IH |
---|
182 | ] |
---|
183 | qed. |
---|
184 | |
---|
185 | definition Block_append ≝ |
---|
186 | λp,globals.λB : Σb.Is_unbranching … b.λB'. |
---|
187 | ! b1 ← Is_to_is_unbr … B; |
---|
188 | ! b2 ← B'; |
---|
189 | return s_block_append p globals b1 b2. |
---|
190 | |
---|
191 | definition all_unbranching ≝ λp,globals.All ? (λs.bool_to_Prop (step_unbranching p globals s)). |
---|
192 | |
---|
193 | let rec step_list_to_s_block (p : params) globals (l : list (joint_step p globals)) on l : |
---|
194 | s_block p globals ≝ |
---|
195 | match l with |
---|
196 | [ nil ⇒ Skip ?? |
---|
197 | | cons hd tl ⇒ |
---|
198 | If step_unbranching … hd then with prf do |
---|
199 | Cons ?? hd (step_list_to_s_block ?? tl) |
---|
200 | else with prf do |
---|
201 | FinStep ?? hd |
---|
202 | ]. [assumption | >prf % ] qed. |
---|
203 | |
---|
204 | definition step_list_to_block : ∀R,p,g.? → Block R p g ≝ |
---|
205 | λR,p,globals,l.bret R ? (step_list_to_s_block p globals l). |
---|
206 | |
---|
207 | record sem_rel (p1 : sem_params) (p2 : sem_params) (globals : list ident) : Type[0] ≝ |
---|
208 | { function_rel : joint_function globals p1 → joint_function globals p2 → Prop |
---|
209 | ; genv_rel : genv globals p1 → genv globals p2 → Prop |
---|
210 | ; pc_rel : cpointer → cpointer → Prop |
---|
211 | ; st_rel : state p1 → state p2 → Prop |
---|
212 | ; stmt_rel : joint_statement p1 globals → Block |
---|
213 | (* TODO: state what do we need of genv_rel (like finding the same symbols and what relation to above rels ) *) |
---|
214 | ; st_to_pc_rel : ∀st1,st2.st_rel st1 st2 → pc_rel (pc ? st1) (pc ? st2) |
---|
215 | }. |
---|
216 | |
---|
217 | (* move *) |
---|
218 | definition beval_pair_of_xdata_pointer: (Σp:pointer. ptype p = XData) → beval × beval ≝ |
---|
219 | λp. match p return λp. ptype p = XData → ? with [ mk_pointer pty pbl pok poff ⇒ |
---|
220 | match pty return λpty. ? → pty = XData → ? with |
---|
221 | [ XData ⇒ λpok.λE. list_to_pair ? (bevals_of_pointer (mk_pointer XData pbl ? poff)) ? |
---|
222 | | _ ⇒ λpok'.λabs. ⊥] pok] ?. |
---|
223 | [@(pi2 … p) |6: // |7: %] destruct (abs) |
---|
224 | qed. |
---|
225 | |
---|
226 | definition safe_address_of_xdata_pointer: (Σp:pointer. ptype p = XData) → safe_address ≝ beval_pair_of_xdata_pointer. |
---|
227 | cases H -H * #r #b #H #o #EQ destruct(EQ) normalize lapply H |
---|
228 | lapply (pointer_compat_from_ind … H) -H cases b * #z * #H |
---|
229 | %{«mk_pointer ? (mk_block ? z) H o,I»} |
---|
230 | % [2,4: % [2,4: % [1,3: % [1,3: % ]] % |*:]|*:] |
---|
231 | qed. |
---|
232 | |
---|
233 | definition state_rel : ∀p1,p2.∀R : sem_rel p1 p2.good_state p1 → good_state p2 → Prop ≝ |
---|
234 | λp1,p2,R,st1,st2. |
---|
235 | frames_rel p1 p2 R (st_frms … st1) (st_frms … st2) ∧ |
---|
236 | pc_rel p1 p2 R (pc … st1) (pc … st2) ∧ |
---|
237 | sp_rel p1 p2 R |
---|
238 | (safe_address_of_xdata_pointer (sp … st1)) |
---|
239 | (safe_address_of_xdata_pointer (sp … st2)) ∧ |
---|
240 | isp_rel p1 p2 R |
---|
241 | (safe_address_of_xdata_pointer (isp … st1)) |
---|
242 | (safe_address_of_xdata_pointer (isp … st2)) ∧ |
---|
243 | sp_rel p1 p2 R |
---|
244 | (safe_address_of_xdata_pointer (sp … st1)) |
---|
245 | (safe_address_of_xdata_pointer (sp … st2)) ∧ |
---|
246 | carry … st1 = carry … st2 ∧ |
---|
247 | regs_rel p1 p2 R (regs … st1) (regs … st2) ∧ |
---|
248 | mem_rel p1 p2 R (m … st1) (m … st2). |
---|
249 | elim st1 -st1 #st1 ** #good_pc1 #good_sp1 #good_isp1 |
---|
250 | elim st2 -st2 #st2 ** #good_pc2 #good_sp2 #good_isp2 |
---|
251 | assumption |
---|
252 | qed. |
---|
253 | elim st2 |
---|
254 | -st1 -st2 #st2 ** #good_pc2 # ∧ |
---|
255 | frames_rel … R (st_frms … st1) (st_frms … st2) ∧ |
---|
256 | frames_rel … R (st_frms … st1) (st_frms … st2) ∧ |
---|
257 | frames_rel … R (st_frms … st1) (st_frms … st2) ∧ |
---|
258 | |
---|
259 | |
---|
260 | |
---|