source: src/joint/semanticsUtils.ma @ 2757

Last change on this file since 2757 was 2708, checked in by tranquil, 7 years ago

fixed linearise and LINToASM
LINToASM has now correct transformation of idents and labels to Identifier

File size: 21.6 KB
Line 
1include "joint/joint_semantics.ma".
2include alias "common/Identifiers.ma".
3include "utilities/hide.ma".
4include "ASM/BitVectorTrie.ma".
5include "joint/TranslateUtils.ma".
6include "common/ExtraMonads.ma".
7include "common/extraGlobalenvs.ma".
8
9record hw_register_env : Type[0] ≝
10  { reg_env : BitVectorTrie beval 6
11  ; other_bit : bebit
12  }.
13
14definition empty_hw_register_env: hw_register_env ≝
15  mk_hw_register_env (Stub …) BBundef.
16
17include alias "ASM/BitVectorTrie.ma".
18
19definition hwreg_retrieve: hw_register_env → Register → beval ≝
20 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
21
22definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
23 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
24  (other_bit env).
25
26definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
27λv,env.mk_hw_register_env (reg_env env) v.
28
29definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
30λenv.
31let spl ≝ hwreg_retrieve env RegisterSPL in
32let sph ≝ hwreg_retrieve env RegisterSPH in
33! ptr ← pointer_of_address 〈spl, sph〉 ;
34match ptype ptr return λx.ptype ptr = x → res xpointer with
35[ XData ⇒ λprf.return «ptr, prf»
36| _ ⇒ λ_.Error … [MSG BadPointer]
37] (refl …).
38
39definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
40λenv,sp.
41let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
42hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
43
44(*** Store/retrieve on pseudo-registers ***)
45include alias "common/Identifiers.ma".
46
47record reg_sp : Type[0] ≝
48{ reg_sp_env :> identifier_map RegisterTag beval
49; stackp : xpointer
50}.
51
52definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v.
53
54definition reg_retrieve : register_env beval → register → res beval ≝
55 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
56
57definition reg_sp_store ≝ λreg,v,locals.
58! locals' ← reg_store reg v (reg_sp_env locals) ;
59return mk_reg_sp locals' (stackp locals).
60
61definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals.
62
63(*** Store/retrieve on hardware registers ***)
64
65definition init_hw_register_env: xpointer → hw_register_env ≝
66 λsp.hwreg_store_sp empty_hw_register_env sp.
67
68(******************************** GRAPHS **************************************)
69
70record sem_graph_params : Type[1] ≝
71{ sgp_pars : unserialized_params
72; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
73}.
74
75definition sem_graph_params_to_graph_params :
76  ∀pars : sem_graph_params.graph_params ≝
77  λpars.mk_graph_params (sgp_pars pars).
78
79coercion graph_params_from_sem_graph_params nocomposites :
80  ∀pars : sem_graph_params.
81  graph_params ≝ sem_graph_params_to_graph_params
82  on _pars : sem_graph_params to graph_params.
83
84definition sem_graph_params_to_sem_params :
85  ∀pars : sem_graph_params.
86  sem_params ≝
87  λpars.
88  mk_sem_params
89    (pars : graph_params)
90    (sgp_sup pars ?)
91    (word_of_identifier ?)
92    (an_identifier ?)
93    ? (refl …).
94* #p % qed.
95
96coercion sem_params_from_sem_graph_params :
97  ∀pars : sem_graph_params.
98  sem_params ≝ sem_graph_params_to_sem_params
99  on _pars : sem_graph_params to sem_params.
100
101
102(******************************** LINEAR **************************************)
103
104lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
105@pos_elim [%]
106#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
107
108record sem_lin_params : Type[1] ≝
109{ slp_pars : unserialized_params
110; slp_sup : ∀F.sem_unserialized_params slp_pars F
111}.
112
113definition sem_lin_params_to_lin_params :
114  ∀pars : sem_lin_params.lin_params ≝
115  λpars.mk_lin_params (slp_pars pars).
116
117coercion lin_params_from_sem_lin_params nocomposites :
118  ∀pars : sem_lin_params.
119  lin_params ≝ sem_lin_params_to_lin_params
120  on _pars : sem_lin_params to lin_params.
121
122definition sem_lin_params_to_sem_params :
123  ∀pars : sem_lin_params.
124  sem_params ≝
125  λpars.
126  mk_sem_params
127    (pars : lin_params)
128    (slp_sup pars ?)
129    succ_pos_of_nat
130    (λp.pred (nat_of_pos p))
131    ??.
132[ #n >nat_succ_pos %
133| @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
134] qed.
135
136coercion sem_params_from_sem_lin_params :
137  ∀pars : sem_lin_params.
138  sem_params ≝ sem_lin_params_to_sem_params
139  on _pars : sem_lin_params to sem_params.
140
141
142lemma fetch_statement_eq : ∀p:sem_params.∀g.
143  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
144  ∀i,fn,s.
145  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
146  let pt ≝ point_of_pc … ptr in
147  stmt_at … (joint_if_code … fn) pt = Some ? s →
148  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
149#p #g #ge #ptr #i #f #s #EQ1 #EQ2
150whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
151>EQ2 %
152qed.
153
154lemma fetch_statement_inv : ∀p:sem_params.∀g.
155  ∀ge : genv_t (joint_function p g).∀ptr : program_counter.
156  ∀i,fn,s.
157  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
158  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
159  let pt ≝ point_of_pc p ptr in
160  stmt_at … (joint_if_code … fn) pt = Some ? s.
161#p #g #ge #ptr #i #fn #s #H
162elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
163elim (bind_inversion ????? H) #s' * #H
164lapply (opt_eq_from_res ???? H) -H #EQ2
165whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
166qed.
167
168definition pm_P : ∀A,B.∀P : A → B → Prop.positive_map A → positive_map B → Prop ≝
169λA,B,P,mA,mB.
170∀p.
171match lookup_opt … p mA with
172[ Some a ⇒
173  match lookup_opt … p mB with
174  [ Some b ⇒ P a b
175  | _ ⇒ False
176  ]
177| _ ⇒ match lookup_opt … p mB with
178  [ Some _ ⇒ False
179  | _ ⇒ True
180  ]
181].
182
183definition match_funct_map :
184  ∀M : matching.
185  ∀vars.positive_map (m_A M vars) → positive_map (m_B M vars) → Prop ≝
186  λM,vars.pm_P … (match_fundef M ?).
187
188lemma pm_P_insert :
189  ∀A,B,P.
190  ∀p,a1,a2,m1,m2.P a1 a2 → pm_P A B P m1 m2 →
191  pm_P … P (insert … p a1 m1) (insert … p a2 m2).
192#A #B #P #p #a1 #a2 #m1 #m2 #Pa1a2 #Pm1m2
193#p'
194@(eqb_elim p' p) #H destruct
195[ >lookup_opt_insert_hit >lookup_opt_insert_hit @Pa1a2
196| >(lookup_opt_insert_miss … a1 … H) >(lookup_opt_insert_miss … a2 … H)
197  @Pm1m2
198]
199qed.
200
201lemma pm_P_set_None :
202  ∀A,B,P.
203  ∀p,m1,m2.pm_P A B P m1 m2 →
204  pm_P … P (pm_set … p (None ?) m1) (pm_set … p (None ?) m2).
205#A #B #P #p #m1 #m2 #Pm1m2
206#p'
207@(eqb_elim p' p) #H destruct
208[ >lookup_opt_pm_set_hit >lookup_opt_pm_set_hit %
209| >(lookup_opt_pm_set_miss … H) >(lookup_opt_pm_set_miss … H)
210  @Pm1m2
211]
212qed.
213
214record match_genv_t (M : matching)
215  (vars : list ident)
216  (ge1 : genv_t (m_A M vars)) (ge2 : genv_t (m_B M vars)) : Prop ≝
217{ symbols_eq : symbols … ge1 = symbols … ge2
218; nextfunction_eq : nextfunction … ge1 = nextfunction … ge2
219; functions_match : pm_P … (match_fundef M ?) (functions … ge1) (functions … ge2)
220}.
221
222lemma add_globals_match :
223  ∀M : matching.∀initV,initW.
224  ∀vars1,vars2.
225  ∀vars.
226(*  let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in
227  let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *)
228  ∀env_mem1 : genv_t (m_A M vars) × mem.
229  ∀env_mem2 : genv_t (m_B M vars) × mem.
230  All2 (ident×region×(m_V M)) (ident×region×(m_W M))
231      (match_var_entry M) vars1 vars2 →
232  nextblock … (\snd env_mem1) = nextblock … (\snd env_mem2) →
233  match_genv_t M vars
234    (\fst env_mem1) (\fst env_mem2) →
235  match_genv_t M vars
236    (\fst (add_globals … initV env_mem1 vars1))
237    (\fst (add_globals … initW env_mem2 vars2)).
238#M #init1 #init2 #vars1
239elim vars1 -vars1 [2: ** #id1 #r1 #v1 #tl1 #IH ]
240* [2,4: ** #id2 #r2 #v2 #tl2 ]
241#vars * #env1 #mem1 * #env2 #mem2 *
242[2: #_ #H @H ]
243#H inversion H #id' #r' #v1' #v2' #P #EQ1 #EQ2 #_ destruct -H #H
244#EQnxtbl #G @(IH tl2 … H)
245cases mem1 in EQnxtbl; -mem1 #mem1 #nbl1 #prf1
246cases mem2 -mem2 #mem2 #nbl2 #prf2 #EQ destruct
247[ % ]
248normalize nodelta %
249whd in match add_symbol;
250whd in match drop_fn; normalize nodelta
251[ >(symbols_eq … G) %
252| @(nextfunction_eq … G)
253| >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta
254  [2: ** [2,3: #p] normalize nodelta ]
255  try @pm_P_set_None
256  @(functions_match … G)
257]
258qed.
259
260lemma add_functs_match :
261  ∀M : matching.
262  ∀vars.
263  ∀functs1,functs2.
264(*  let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in
265  let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *)
266  ∀env1 : genv_t (m_A M vars).
267  ∀env2 : genv_t (m_B M vars).
268  All2 …
269    (match_funct_entry M vars vars) functs1 functs2 →
270  match_genv_t M vars env1 env2 →
271  match_genv_t M vars
272    (add_functs … env1 functs1)
273    (add_functs … env2 functs2).
274#M #vars #functs1 elim functs1 -functs1 [2: * #id1 #f1 #tl1 #IH ]
275* [2,4: * #id2 #f2 #tl2 ]
276#env1 #env2 *
277[2: #H @H ]
278#H
279cut (id1 = id2 ∧ match_fundef M … f1 f2)
280[ @(match_funct_entry_inv M ??????? H) #v #i #f1 #f2 #H %{H} % ]
281* #EQ destruct #Pf1f2 #Ptl1tl2 #G
282lapply (IH … Ptl1tl2 G) -G #G
283%
284whd in
285  match (add_functs ?? (? :: tl1));
286whd in
287  match (add_functs ?? (? :: tl2));
288change with (add_functs ?? tl1) in match (foldr ???? tl1);
289change with (add_functs ?? tl2) in match (foldr ???? tl2);
290whd in match drop_fn; normalize nodelta
291[ >(nextfunction_eq … G)  >(symbols_eq … G) %
292| >(nextfunction_eq … G) %
293| >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta
294  [2: ** [2,3: #p] normalize nodelta ]
295  >(nextfunction_eq … G)
296  @(pm_P_insert … Pf1f2)
297  try @pm_P_set_None @(functions_match … G)
298]
299qed.
300
301lemma globalenv_match:
302    ∀M:matching.∀initV,initW.
303     (∀v,w. match_var_entry M v w →
304      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
305    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
306    ∀MATCH:match_program … M p p'.
307    match_genv_t M ? (globalenv … initV p)
308      (globalenv … initW p' ⌈prog_var_names … p' ↦ prog_var_names … p⌉).
309[2: @sym_eq @(matching_vars … (mp_vars … MATCH)) ]
310* #A #B #V #W #Pf #Pv #iV #iW #init_eq
311* #vars1 #functs1 #main1
312* #vars2 #functs2 #main2
313*
314whd in match prog_var_names;
315normalize nodelta;
316#Mvars #Mfns #EQmain destruct
317lapply (sym_eq ????)
318#E
319lapply Mfns lapply functs2 -functs2
320whd in match globalenv; whd in match globalenv_allocmem;
321whd in match prog_var_names in E ⊢ %;
322normalize nodelta in E ⊢ %;
323>E normalize nodelta #functs2 #Mfns
324@add_globals_match [ assumption | % ]
325@add_functs_match [ assumption ]
326% try % #p %
327qed.
328
329lemma symbols_transf:
330 ∀A,B,V,init.∀prog_in : program A V.
331 ∀trans : ∀vars.A vars → B vars.
332 let prog_out ≝ transform_program … prog_in trans in
333 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).
334#A #B #V #iV #p #tf whd
335lapply (transform_program_match … tf p)
336#MATCH
337>(symbols_eq … (globalenv_match … MATCH))
338[2: @iV |3: #v #w * // ]
339lapply (sym_eq ????)
340whd in match (prog_var_names ???); whd in match (prog_vars B ??);
341#E >(K ?? E) normalize nodelta %
342qed.
343
344
345lemma functions_transf:
346 ∀A,B,V,init.∀prog_in : program A V.
347 ∀trans : ∀vars.A vars → B vars.
348 let prog_out ≝ transform_program … prog_in trans in
349 ∀p.lookup_opt … p (functions … (globalenv … init prog_out)) =
350 option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))).
351#A #B #V #iV #p #tf #n
352lapply (transform_program_match … tf p)
353#MATCH
354whd in match globalenv; whd in match globalenv_allocmem;
355normalize nodelta
356lapply (functions_match … (globalenv_match … MATCH) n)
357[ @iV | @iV | #v #w * // ]
358lapply (sym_eq ????)
359whd in match (prog_var_names ???); whd in match (prog_vars B ??);
360#E >(K ?? E) normalize nodelta
361cases (lookup_opt ???) [2: #x ] normalize nodelta
362cases (lookup_opt ???) [2,4: #y ] normalize nodelta
363[ #EQ <EQ % |*: * % ]
364qed.
365
366lemma symbol_for_block_transf :
367 ∀A,B,V,init.∀prog_in : program A V.
368 ∀trans : ∀vars.A vars → B vars.
369 let prog_out ≝ transform_program … prog_in trans in
370 ∀bl.
371 symbol_for_block … (globalenv … init prog_out) bl =
372 symbol_for_block … (globalenv … init prog_in) bl.
373#A #B #V #iV #p #tf whd
374#bl
375whd in match symbol_for_block; normalize nodelta
376>(symbols_transf … tf) %
377qed.
378
379include alias "common/Pointers.ma".
380
381lemma fetch_function_transf :
382 ∀A,B,V,init.∀prog_in : program A V.
383 ∀trans : ∀vars.A vars → B vars.
384 let prog_out ≝ transform_program … prog_in trans in
385 ∀bl.
386 fetch_function … (globalenv … init prog_out) bl =
387 ! 〈i, f〉 ← fetch_function … (globalenv … init prog_in) bl ;
388 return 〈i, trans … f〉.
389#A #B #V #init #prog_in #trans #bl
390whd in match fetch_function; normalize nodelta
391>(symbol_for_block_transf A B V init prog_in trans)
392cases (symbol_for_block ???) [ % ] #id >m_return_bind >m_return_bind
393whd in match find_funct_ptr; normalize nodelta
394whd in match (block_region (pi1 ?? bl));
395cases (block_id (pi1 ?? bl)) [2,3: #p] normalize nodelta try %
396>(functions_transf A B V init prog_in trans p)
397cases (lookup_opt ???) //
398qed.
399
400lemma fetch_internal_function_transf :
401 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
402 ∀trans : ∀vars.A vars → B vars.
403 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
404 ∀bl.
405 fetch_internal_function … (globalenv_noinit … prog_out) bl =
406 ! 〈i, f〉 ← fetch_internal_function … (globalenv_noinit … prog_in) bl ;
407 return 〈i, trans … f〉.
408#A #B #prog #trans #bl
409 whd in match fetch_internal_function; normalize nodelta
410>(fetch_function_transf … prog)
411cases (fetch_function ???)
412[ * #id * #f % | #e % ]
413qed.
414
415include alias "utilities/binary/positive.ma".
416
417lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop.
418(∀m.(∀p.lookup_opt A p m = None ?) → P m) →
419(∀m,p,v.P m → lookup_opt A p m = None ? → P (insert A p v m)) →
420∀m.P m.
421#A #P #H1 #H2 #m lapply H2 lapply H1 lapply P -P elim m -m
422[ #P #H1 #_ @H1 #p % ]
423#o #l #r #IHl #IHr #P #H1 #H2
424@IHl #l'
425[ #empty_l' @IHr #r'
426  [ #empty_r' cases o [ @H1 * try #p normalize // ]
427    #v change with (P (insert ? one v (pm_node ? (None ?) ??)))
428    @H2 [ @H1 * try #p normalize // | % ]
429  ]
430]
431#p #v #H #G
432[ change with (P (insert ? (p1 p) v (pm_node ? ???)))
433| change with (P (insert ? (p0 p) v (pm_node ? ???)))
434] @H2 assumption
435qed.
436
437include alias "basics/logic.ma".
438include alias "common/PositiveMap.ma".
439
440lemma swap_neg : ∀A,B : Prop.(A → B) → ¬B → ¬A.
441#A #B #impl * #Bf % #At @Bf @impl @At qed-.
442
443definition b_graph_transform_program_props ≝
444  λsrc,dst : sem_graph_params.
445  λdata,prog_in.
446  λinit_regs : block → list register.
447  λf_lbls : block → label → option (list label).
448  λf_regs : block → label → option (list register).
449   let prog_out ≝ b_graph_transform_program src dst data prog_in in
450   let src_genv ≝ globalenv_noinit ? prog_in in
451   let dst_genv ≝ globalenv_noinit ? prog_out in
452  ∀bl,def_in.
453  find_funct_ptr … src_genv bl = return (Internal ? def_in) →
454  ∃init_data,def_out.
455  find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
456  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
457  b_graph_translate_props src dst ? init_data (init_regs bl)
458    def_in def_out (f_lbls bl) (f_regs bl).
459 
460lemma make_b_graph_transform_program_props :
461 ∀src,dst:sem_graph_params.
462 ∀data : ∀globals.joint_closed_internal_function src globals →
463  bind_new register (b_graph_translate_data src dst globals).
464 ∀prog_in : joint_program src.
465 let prog_out ≝ b_graph_transform_program … data prog_in in
466 let src_genv ≝ globalenv_noinit ? prog_in in
467 let dst_genv ≝ globalenv_noinit ? prog_out in
468 ∃init_regs : block → list register.
469 ∃f_lbls : block → label → option (list label).
470 ∃f_regs : block → label → option (list register).
471 b_graph_transform_program_props src dst data prog_in init_regs f_lbls f_regs.
472#src #dst #data #prog_in
473whd in match b_graph_transform_program_props; normalize nodelta
474letin prog_out ≝ (b_graph_transform_program … data prog_in)
475letin src_genv ≝ (globalenv_noinit ? prog_in)
476letin dst_genv ≝ (globalenv_noinit ? prog_out)
477cut (∀p.lookup_opt ? p (functions ? dst_genv) =
478     option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f))
479      (lookup_opt ? p (functions ? src_genv)))
480[ @functions_transf ]
481cases dst_genv #functs2 #nextf2 #symbols2 #H2
482cases src_genv #functs1 #nextf1 #symbols1 #H1
483lapply H2 lapply H1 lapply functs2
484@(pm_map_add_ind … functs1) -functs1 -functs2 #functs1
485[ #functs1_empty | #p #f #IH #p_not_in ]
486#functs2 #H1 #H2 #transf
487[ %{(λ_.[ ])} %{(λ_.λ_.None ?)} %{(λ_.λ_.None ?)}
488  #bl #def_in #ABS @⊥ lapply ABS -ABS
489  whd in match find_funct_ptr;
490  normalize nodelta
491  whd in match (block_region bl);
492  cases (block_id bl) normalize nodelta
493  [2,3: #p [2: >functs1_empty ]]
494  normalize #ABS destruct
495]
496cases (IH (pm_set … p (None ?) functs2) ???)
497[2: @hide_prf #b #G @(H1 b ?) @(swap_neg … G) -G @(eqb_elim b p)
498  [ #EQ destruct >lookup_opt_insert_hit #ABS destruct ]
499  #NEQ >(lookup_opt_insert_miss ? f b p … NEQ) #H @H
500|3: @hide_prf #b #G @(H2 b ?) @(swap_neg … G) -G @(eqb_elim b p)
501  [ #EQ destruct >lookup_opt_pm_set_hit #_ % ]
502  #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) #H @H
503|4: #b @(eqb_elim b p)
504  [ #EQ destruct >lookup_opt_pm_set_hit >p_not_in % ]
505  #NEQ >(lookup_opt_pm_set_miss … b p … NEQ) >transf
506  >(lookup_opt_insert_miss ? f b p … NEQ) %
507]
508-IH cases f in H1 transf; -f #f #H1 #transf
509#init_regs * #f_lbls * #f_regs #props
510[ (* internal *)
511  letin upd ≝ (λA : Type[0].λf : block → A.
512    λid.λv,id'.
513    if eq_block id id' then v else f id')
514  cases (pi2 ?? (b_graph_translate … (data … f) f))
515  #loc_data * #loc_init_regs * #loc_f_lbls * #loc_f_regs *
516  #inst_loc_data #loc_props
517  letin bl ≝ (mk_block (neg p))
518  %{(upd … init_regs bl loc_init_regs)}
519  %{(upd … f_lbls bl loc_f_lbls)}
520  %{(upd … f_regs bl loc_f_regs)}
521| (* external, nothing changes *)
522  %{init_regs}
523  %{f_lbls}
524  %{f_regs}
525]
526* #p' #def_in
527whd in match find_funct_ptr; normalize nodelta
528whd in match (block_region (mk_block p'));
529cases p' -p' [2,3,5,6: #p' ] normalize nodelta
530[1,3,5,6: #ABS normalize in ABS; destruct]
531@(eqb_elim p' p) #pp' destruct
532[1,3: >lookup_opt_insert_hit whd in ⊢ (??%%→?); #EQ destruct(EQ)
533  %{loc_data} %
534  [2: % [ % ]
535    [ >transf >lookup_opt_insert_hit %
536    |*: >eq_block_b_b assumption
537    ]
538  |]
539|*: >(lookup_opt_insert_miss ???? functs1 … pp')
540  [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta]
541  #EQ lapply (props (mk_block (neg p')) def_in EQ)
542  whd in match find_funct_ptr; normalize nodelta
543  >(lookup_opt_pm_set_miss … functs2 … pp') #H @H
544]
545qed.
546
547lemma b_graph_transform_program_fetch_internal_function :
548 ∀src,dst:sem_graph_params.
549 ∀data : ∀globals.joint_closed_internal_function src globals →
550  bind_new register (b_graph_translate_data src dst globals).
551 ∀prog_in : joint_program src.
552 ∀init_regs : block → list register.
553 ∀f_lbls : block → label → option (list label).
554 ∀f_regs : block → label → option (list register).
555 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
556 let prog_out ≝ b_graph_transform_program … data prog_in in
557 let src_genv ≝ globalenv_noinit ? prog_in in
558 let dst_genv ≝ globalenv_noinit ? prog_out in
559 ∀bl,id,def_in.
560 fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
561 ∃init_data,def_out.
562 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
563 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
564 b_graph_translate_props src dst ? init_data (init_regs bl)
565    def_in def_out (f_lbls bl) (f_regs bl).
566#src #dst #data #prog_in
567#init_regs #f_lbls #f_regs #props
568#bl #id #def_in
569#H @('bind_inversion H) * #id' * #def_in' -H
570normalize nodelta #H whd in ⊢ (??%%→?); #EQ destruct
571@('bind_inversion (opt_eq_from_res … H)) -H #id' #EQ1
572#H @('bind_inversion H) -H #def_in' #H
573whd in ⊢ (??%%→?); #EQ destruct
574cases (props … H)
575#loc_data * #def_out ** #H1 #H2 #H3
576%{loc_data} %{def_out}
577%{H3} %{H2}
578whd in match fetch_internal_function;
579whd in match fetch_function; normalize nodelta
580>symbol_for_block_transf >EQ1 >m_return_bind
581>H1 %
582qed.
583
584lemma b_graph_transform_program_fetch_statement :
585 ∀src,dst:sem_graph_params.
586 ∀data : ∀globals.joint_closed_internal_function src globals →
587  bind_new register (b_graph_translate_data src dst globals).
588 ∀prog_in : joint_program src.
589 ∀init_regs : block → list register.
590 ∀f_lbls : block → label → option (list label).
591 ∀f_regs : block → label → option (list register).
592 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
593 let prog_out ≝ b_graph_transform_program … data prog_in in
594 let src_genv ≝ globalenv_noinit ? prog_in in
595 let dst_genv ≝ globalenv_noinit ? prog_out in
596 ∀pc,id,def_in,s.
597 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
598 ∃init_data,def_out.
599 let bl ≝ pc_block pc in
600 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
601 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
602 let l ≝ point_of_pc dst pc in
603 ∃lbls,regs.
604 f_lbls bl l = Some ? lbls ∧
605 f_regs bl l = Some ? regs ∧
606  match s with
607  [ sequential s' nxt ⇒
608    let block ≝
609      if eq_identifier … (joint_if_entry … def_in) l then
610        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
611      else
612        f_step … init_data l s' in
613    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
614  | final s' ⇒
615    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
616  | FCOND abs _ _ _ ⇒ Ⓧabs
617  ].
618#src #dst #data #prog_in
619#init_regs #f_lbls #f_regs #props
620#pc #id #def_in #s
621#H @('bind_inversion H) * #id' #def_in' -H
622#EQfif
623#H @('bind_inversion H) -H #s
624#H lapply (opt_eq_from_res ???? H) -H
625#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
626cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
627#a * #b ** #H1 #H2 #H3 %{a} %{b} %
628[ %{H1 H2} | @(multi_fetch_ok … H3 … EQstmt_at) ]
629qed.
Note: See TracBrowser for help on using the repository browser.