source: src/joint/semanticsUtils.ma @ 3362

Last change on this file since 3362 was 3265, checked in by tranquil, 7 years ago

added validate_pointer filter
in Interference added that intereference only fires on non eliminable
statements

File size: 28.4 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
9definition reg_store ≝ λreg,v,locals.add RegisterTag beval locals reg v.
10
11definition reg_retrieve : register_env beval → register → res beval ≝
12 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg).
13
14record hw_register_env : Type[0] ≝
15  { reg_env : BitVectorTrie beval 6
16  ; other_bit : bebit
17  }.
18
19include alias "ASM/BitVectorTrie.ma".
20
21definition hwreg_retrieve: hw_register_env → Register → beval ≝
22 λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef.
23
24definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝
25 λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env))
26  (other_bit env).
27
28definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝
29λv,env.mk_hw_register_env (reg_env env) v.
30
31definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝
32λenv.
33let spl ≝ hwreg_retrieve env RegisterSPL in
34let sph ≝ hwreg_retrieve env RegisterSPH in
35! ptr ← pointer_of_address 〈spl, sph〉 ;
36match ptype ptr return λx.ptype ptr = x → res xpointer with
37[ XData ⇒ λprf.return «ptr, prf»
38| _ ⇒ λ_.Error … [MSG BadPointer]
39] (refl …).
40
41definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝
42λenv,sp.
43let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in
44hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env).
45
46definition init_hw_register_env: xpointer → hw_register_env ≝
47 hwreg_store_sp (mk_hw_register_env (Stub …) BBundef).
48
49(*** Store/retrieve on pseudo-registers ***)
50include alias "common/Identifiers.ma".
51
52unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
53
54(******************************** GRAPHS **************************************)
55
56record sem_graph_params : Type[1] ≝
57{ sgp_pars : uns_params
58; sgp_sup : ∀F.sem_unserialized_params sgp_pars F
59; graph_pre_main_generator :
60  ∀p : joint_program (mk_graph_params sgp_pars).
61  joint_closed_internal_function (mk_graph_params sgp_pars) (prog_names … p)
62}.
63
64
65definition sem_graph_params_to_graph_params :
66  ∀pars : sem_graph_params.graph_params ≝
67  λpars.mk_graph_params (sgp_pars pars).
68
69coercion graph_params_from_sem_graph_params nocomposites :
70  ∀pars : sem_graph_params.
71  graph_params ≝ sem_graph_params_to_graph_params
72  on _pars : sem_graph_params to graph_params.
73
74definition sem_graph_params_to_sem_params :
75  ∀pars : sem_graph_params.
76  sem_params ≝
77  λpars.
78  mk_sem_params
79    (mk_serialized_params
80      (pars : graph_params)
81      (sgp_sup pars ?)
82      (word_of_identifier ?)
83      (an_identifier ?)
84      ? (refl …))
85    (graph_pre_main_generator pars).
86* #p % qed.
87
88coercion sem_params_from_sem_graph_params :
89  ∀pars : sem_graph_params.
90  sem_params ≝ sem_graph_params_to_sem_params
91  on _pars : sem_graph_params to sem_params.
92
93
94(******************************** LINEAR **************************************)
95
96lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p.
97@pos_elim [%]
98#p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed.
99
100record sem_lin_params : Type[1] ≝
101{ slp_pars : uns_params
102; slp_sup : ∀F.sem_unserialized_params slp_pars F
103; lin_pre_main_generator :
104  ∀p : joint_program (mk_lin_params slp_pars).
105  joint_closed_internal_function (mk_lin_params slp_pars) (prog_names … p)
106}.
107
108definition sem_lin_params_to_lin_params :
109  ∀pars : sem_lin_params.lin_params ≝
110  λpars.mk_lin_params (slp_pars pars).
111
112coercion lin_params_from_sem_lin_params nocomposites :
113  ∀pars : sem_lin_params.
114  lin_params ≝ sem_lin_params_to_lin_params
115  on _pars : sem_lin_params to lin_params.
116
117definition sem_lin_params_to_sem_params :
118  ∀pars : sem_lin_params.
119  sem_params ≝
120  λpars.
121  mk_sem_params
122    (mk_serialized_params
123      (pars : lin_params)
124      (slp_sup pars ?)
125      succ_pos_of_nat
126      (λp.pred (nat_of_pos p))
127      ??)
128    (lin_pre_main_generator pars).
129[ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos
130| #n >nat_succ_pos %
131] qed.
132
133coercion sem_params_from_sem_lin_params :
134  ∀pars : sem_lin_params.
135  sem_params ≝ sem_lin_params_to_sem_params
136  on _pars : sem_lin_params to sem_params.
137
138(* TODO move elsewhere *)
139lemma lookup_opt_pm_set_elim : ∀A.∀P : option A → Prop.∀p,q,o,m.
140  (p = q → P o) →
141  (p ≠ q → P (lookup_opt A p m)) →
142  P (lookup_opt A p (pm_set A q o m)).
143#A #P #p #q
144@(eqb_elim p q) #H #o #m #H1 #H2
145[ >H >lookup_opt_pm_set_hit @H1 @H
146| >lookup_opt_pm_set_miss [ @H2 ] @H
147]
148qed.
149
150lemma lookup_add_elim : ∀tag,A.∀P : option A → Prop.∀m,i,j,x.
151  (i = j → P (Some ? x)) →
152  (i ≠ j → P (lookup tag A m j)) →
153  P (lookup tag A (add tag A m i x) j).
154#tag #A #P * #m * #p * #q #x
155#H1 #H2 whd in ⊢ (?%); normalize nodelta whd in match insert; normalize nodelta
156@lookup_opt_pm_set_elim #H destruct
157[ @H1 % | @H2 % #EQ destruct cases H #H @H % ]
158qed.
159
160lemma fetch_statement_eq : ∀p:sem_params.∀g.
161  ∀ge : genv p g.∀ptr : program_counter.
162  ∀i,fn,s.
163  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 →
164  let pt ≝ point_of_pc … ptr in
165  stmt_at … (joint_if_code … fn) pt = Some ? s →
166  fetch_statement … ge ptr = OK … 〈i, fn, s〉.
167#p #g #ge #ptr #i #f #s #EQ1 #EQ2
168whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind
169>EQ2 %
170qed.
171
172lemma fetch_statement_inv : ∀p:sem_params.∀g.
173  ∀ge : genv p g.∀ptr : program_counter.
174  ∀i,fn,s.
175  fetch_statement … ge ptr = OK … 〈i, fn, s〉 →
176  fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧
177  let pt ≝ point_of_pc p ptr in
178  stmt_at … (joint_if_code … fn) pt = Some ? s.
179#p #g #ge #ptr #i #fn #s #H
180elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H
181elim (bind_inversion ????? H) #s' * -H #H
182lapply (opt_eq_from_res ???? H) -H #EQ2
183whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
184qed.
185
186definition pm_P : ∀A,B.∀P : A → B → Prop.positive_map A → positive_map B → Prop ≝
187λA,B,P,mA,mB.
188∀p.
189match lookup_opt … p mA with
190[ Some a ⇒
191  match lookup_opt … p mB with
192  [ Some b ⇒ P a b
193  | _ ⇒ False
194  ]
195| _ ⇒ match lookup_opt … p mB with
196  [ Some _ ⇒ False
197  | _ ⇒ True
198  ]
199].
200
201definition match_funct_map :
202  ∀M : matching.
203  ∀vars.positive_map (m_A M vars) → positive_map (m_B M vars) → Prop ≝
204  λM,vars.pm_P … (match_fundef M ?).
205
206lemma pm_P_insert :
207  ∀A,B,P.
208  ∀p,a1,a2,m1,m2.P a1 a2 → pm_P A B P m1 m2 →
209  pm_P … P (insert … p a1 m1) (insert … p a2 m2).
210#A #B #P #p #a1 #a2 #m1 #m2 #Pa1a2 #Pm1m2
211#p'
212@(eqb_elim p' p) #H destruct
213[ >lookup_opt_insert_hit >lookup_opt_insert_hit @Pa1a2
214| >(lookup_opt_insert_miss … a1 … H) >(lookup_opt_insert_miss … a2 … H)
215  @Pm1m2
216]
217qed.
218
219lemma pm_P_set_None :
220  ∀A,B,P.
221  ∀p,m1,m2.pm_P A B P m1 m2 →
222  pm_P … P (pm_set … p (None ?) m1) (pm_set … p (None ?) m2).
223#A #B #P #p #m1 #m2 #Pm1m2
224#p'
225@(eqb_elim p' p) #H destruct
226[ >lookup_opt_pm_set_hit >lookup_opt_pm_set_hit %
227| >(lookup_opt_pm_set_miss … H) >(lookup_opt_pm_set_miss … H)
228  @Pm1m2
229]
230qed.
231
232record match_genv_t (M : matching)
233  (vars : list ident)
234  (ge1 : genv_t (m_A M vars)) (ge2 : genv_t (m_B M vars)) : Prop ≝
235{ symbols_eq : symbols … ge1 = symbols … ge2
236; nextfunction_eq : nextfunction … ge1 = nextfunction … ge2
237; functions_match : pm_P ?? (match_fundef M ?) (functions … ge1) (functions … ge2)
238}.
239
240lemma add_globals_match :
241  ∀M : matching.∀initV,initW.
242  ∀vars1,vars2.
243  ∀vars.
244(*  let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in
245  let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *)
246  ∀env_mem1 : genv_t (m_A M vars) × mem.
247  ∀env_mem2 : genv_t (m_B M vars) × mem.
248  All2 (ident×region×(m_V M)) (ident×region×(m_W M))
249      (match_var_entry M) vars1 vars2 →
250  nextblock … (\snd env_mem1) = nextblock … (\snd env_mem2) →
251  match_genv_t M vars
252    (\fst env_mem1) (\fst env_mem2) →
253  match_genv_t M vars
254    (\fst (add_globals … initV env_mem1 vars1))
255    (\fst (add_globals … initW env_mem2 vars2)).
256#M #init1 #init2 #vars1
257elim vars1 -vars1 [2: ** #id1 #r1 #v1 #tl1 #IH ]
258* [2,4: ** #id2 #r2 #v2 #tl2 ]
259#vars * #env1 #mem1 * #env2 #mem2 *
260[2: #_ #H @H ]
261#H inversion H #id' #r' #v1' #v2' #P #EQ1 #EQ2 #_ destruct -H #H
262#EQnxtbl #G @(IH tl2 … H)
263cases mem1 in EQnxtbl; -mem1 #mem1 #nbl1 #prf1
264cases mem2 -mem2 #mem2 #nbl2 #prf2 #EQ destruct
265[ % ]
266normalize nodelta %
267whd in match add_symbol;
268whd in match drop_fn; normalize nodelta
269[ >(symbols_eq … G) %
270| @(nextfunction_eq … G)
271| >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta
272  [2: ** [2,3: #p] normalize nodelta ]
273  try @pm_P_set_None
274  @(functions_match … G)
275]
276qed.
277
278lemma add_functs_match :
279  ∀M : matching.
280  ∀vars.
281  ∀functs1,functs2.
282(*  let vars1' ≝ map … (λx.\fst (\fst x)) vars1 in
283  let vars2' ≝ map … (λx.\fst (\fst x)) vars2 in *)
284  ∀env1 : genv_t (m_A M vars).
285  ∀env2 : genv_t (m_B M vars).
286  All2 …
287    (match_funct_entry M vars vars) functs1 functs2 →
288  match_genv_t M vars env1 env2 →
289  match_genv_t M vars
290    (add_functs … env1 functs1)
291    (add_functs … env2 functs2).
292#M #vars #functs1 elim functs1 -functs1 [2: * #id1 #f1 #tl1 #IH ]
293* [2,4: * #id2 #f2 #tl2 ]
294#env1 #env2 *
295[2: #H @H ]
296#H
297cut (id1 = id2 ∧ match_fundef M … f1 f2)
298[ @(match_funct_entry_inv M ??????? H) #v #i #f1 #f2 #H %{H} % ]
299* #EQ destruct #Pf1f2 #Ptl1tl2 #G
300lapply (IH … Ptl1tl2 G) -G #G
301%
302whd in
303  match (add_functs ?? (? :: tl1));
304whd in
305  match (add_functs ?? (? :: tl2));
306change with (add_functs ?? tl1) in match (foldr ???? tl1);
307change with (add_functs ?? tl2) in match (foldr ???? tl2);
308whd in match drop_fn; normalize nodelta
309[ >(nextfunction_eq … G)  >(symbols_eq … G) %
310| >(nextfunction_eq … G) %
311| >(symbols_eq … G) cases (lookup ? block ??) normalize nodelta
312  [2: ** [2,3: #p] normalize nodelta ]
313  >(nextfunction_eq … G)
314  @(pm_P_insert … Pf1f2)
315  try @pm_P_set_None @(functions_match … G)
316]
317qed.
318
319lemma globalenv_match:
320    ∀M:matching.∀initV,initW.
321     (∀v,w. match_var_entry M v w →
322      size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) →
323    ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M).
324    ∀MATCH:match_program … M p p'.
325    match_genv_t M ? (globalenv … initV p)
326      (globalenv … initW p' ⌈prog_var_names … p' ↦ prog_var_names … p⌉).
327[2: @sym_eq @(matching_vars … (mp_vars … MATCH)) ]
328* #A #B #V #W #Pf #Pv #iV #iW #init_eq
329* #vars1 #functs1 #main1
330* #vars2 #functs2 #main2
331*
332whd in match prog_var_names;
333normalize nodelta;
334#Mvars #Mfns #EQmain destruct
335lapply (sym_eq ????)
336#E
337lapply Mfns lapply functs2 -functs2
338whd in match globalenv; whd in match globalenv_allocmem;
339whd in match prog_var_names in E ⊢ %;
340normalize nodelta in E ⊢ %;
341>E normalize nodelta #functs2 #Mfns
342@add_globals_match [ assumption | % ]
343@add_functs_match [ assumption ]
344% try % #p %
345qed.
346
347lemma symbols_transf:
348 ∀A,B,V,init.∀prog_in : program A V.
349 ∀trans : ∀vars.A vars → B vars.
350 let prog_out ≝ transform_program … prog_in trans in
351 symbols … (globalenv … init prog_out) = symbols … (globalenv … init prog_in).
352#A #B #V #iV #p #tf whd
353lapply (transform_program_match … tf p)
354#MATCH
355>(symbols_eq … (globalenv_match … MATCH))
356[2: @iV |3: #v #w * // ]
357lapply (sym_eq ????)
358whd in match (prog_var_names ???); whd in match (prog_vars B ??);
359#E >(K ?? E) normalize nodelta %
360qed.
361
362lemma functions_transf:
363 ∀A,B,V,init.∀prog_in : program A V.
364 ∀trans : ∀vars.A vars → B vars.
365 let prog_out ≝ transform_program … prog_in trans in
366 ∀p.lookup_opt … p (functions … (globalenv … init prog_out)) =
367 option_map ?? (trans ?) (lookup_opt … p (functions … (globalenv … init prog_in))).
368#A #B #V #iV #p #tf #n
369lapply (transform_program_match … tf p)
370#MATCH
371whd in match globalenv; whd in match globalenv_allocmem;
372normalize nodelta
373lapply (functions_match … (globalenv_match … MATCH) n)
374[ @iV | @iV | #v #w * // ]
375lapply (sym_eq ????)
376whd in match (prog_var_names ???); whd in match (prog_vars B ??);
377#E >(K ?? E) normalize nodelta
378cases (lookup_opt ???) [2: #x ] normalize nodelta
379cases (lookup_opt ???) [2,4: #y ] normalize nodelta
380[ #EQ <EQ % |*: * % ]
381qed.
382
383lemma symbol_for_block_transf :
384 ∀A,B,V,init.∀prog_in : program A V.
385 ∀trans : ∀vars.A vars → B vars.
386 let prog_out ≝ transform_program … prog_in trans in
387 ∀bl.
388 symbol_for_block … (globalenv … init prog_out) bl =
389 symbol_for_block … (globalenv … init prog_in) bl.
390#A #B #V #iV #p #tf whd
391#bl
392whd in match symbol_for_block; normalize nodelta
393>(symbols_transf … tf) %
394qed.
395
396include alias "common/Pointers.ma".
397
398(* TODO move *)
399lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
400#A #P #Q #l #H elim l -l [2: #hd #tl #IH] * #G whd /3 by or_introl, or_intror/ qed.
401
402definition joint_globalenv :
403  ∀p : sem_params.∀pr:joint_program p.
404    (ident → option ℕ) → genv p (prog_names … pr) ≝
405λp,prog,stacksizes.
406let genv ≝ globalenv … (λx.x) prog in
407let pc_from_lbl ≝ λbl.λfn : joint_closed_internal_function p ?.λlbl.
408  ! pt ← point_of_label … (joint_if_code … fn) lbl ;
409  return mk_program_counter bl (offset_of_point … p pt) in
410mk_genv_gen ?? genv ? stacksizes (pre_main_generator … p prog) pc_from_lbl
411(joint_if_local_stacksize …) (joint_if_params_stacksize …).
412#s #H
413cases (find_symbol_exists ?? (λx.x) … prog s ?)
414[ #bl #EQ >EQ % #ABS destruct ]
415cases (Exists_append … H) -H #H
416[ @Exists_append_r | @Exists_append_l ]
417[ @(Exists_mp … H) @sym_eq ]
418cases prog in H; #functs * #vars #functs' #main #init_cost
419whd in match prog_funct_names; normalize nodelta #EQ
420>map_ext_eq [ >EQ @Exists_mp @sym_eq | // ] skip
421qed.
422
423lemma opt_to_res_bind : ∀X,Y,m,f,e.opt_to_res Y e (! x ← m ; f x) =
424  ! x ← opt_to_res X e m ; opt_to_res Y e (f x).
425#X #Y * [2: #x] #f #e % qed.
426
427lemma fetch_function_transf:
428 ∀src,dst : sem_params.∀prog_in : joint_program src.
429 ∀stacksizes,trans.
430 let prog_out ≝ transform_joint_program src dst trans prog_in in
431 ∀bl.
432 fetch_function … (joint_globalenv … prog_out stacksizes) bl =
433 if eqZb (block_id bl) (-1) then
434   return 〈pre_main_id, Internal ? (pre_main_generator … dst prog_out)〉
435 else
436   ! 〈id, f〉 ← fetch_function … (joint_globalenv … prog_in stacksizes) bl ;
437   return 〈id, transf_fundef ?? (trans ?) f〉.
438#src #dst #p #sizes #tf whd
439lapply (transform_program_match … (λvars.transf_fundef … (tf ?)) p)
440#MATCH
441whd in match fetch_function;
442whd in match joint_globalenv; normalize nodelta
443#bl @eqZb_elim #Hbl normalize nodelta [ % ]
444whd in match transform_joint_program;
445whd in match prog_names; normalize nodelta
446>symbol_for_block_transf
447>opt_to_res_bind >opt_to_res_bind in ⊢ (???%); >m_bind_bind
448@m_bind_ext_eq #id
449whd in match find_funct_ptr; normalize nodelta
450cases bl -bl ** [2,3: #p] normalize nodelta #_ try %
451lapply (functions_match … (globalenv_match … MATCH) p) try @(λx.x)
452[#v #w * //]
453lapply (sym_eq ????)
454whd in match prog_var_names; normalize nodelta
455#E >(K ?? E) -E normalize nodelta
456cases (lookup_opt ???) [2: #x ] normalize nodelta
457cases (lookup_opt ???) [2,4: #y ] normalize nodelta
458* %
459qed.
460
461lemma fetch_internal_function_transf :
462 ∀src,dst : sem_params.∀prog_in : joint_program src.
463 ∀stacksizes,trans.
464 let prog_out ≝ transform_joint_program src dst trans prog_in in
465 ∀bl.
466 fetch_internal_function … (joint_globalenv … prog_out stacksizes) bl =
467 if eqZb (block_id bl) (-1) then
468   return 〈pre_main_id, pre_main_generator … dst prog_out〉
469 else
470   ! 〈i, f〉 ← fetch_internal_function … (joint_globalenv … prog_in stacksizes) bl ;
471   return 〈i, trans … f〉.
472#src #dst #p #sizes #tf whd
473#bl whd in match fetch_internal_function; normalize nodelta
474>(fetch_function_transf … p)
475@eqZb_elim #Hbl [%] normalize nodelta >m_bind_bind >m_bind_bind
476@m_bind_ext_eq * #id * #f %
477qed.
478
479include alias "utilities/binary/positive.ma".
480
481lemma pm_map_add_ind : ∀A.∀P : positive_map A → Prop.
482(∀m.(∀p.lookup_opt A p m = None ?) → P m) →
483(∀m,p,v.P m → lookup_opt A p m = None ? → P (insert A p v m)) →
484∀m.P m.
485#A #P #H1 #H2 #m lapply H2 lapply H1 lapply P -P elim m -m
486[ #P #H1 #_ @H1 #p % ]
487#o #l #r #IHl #IHr #P #H1 #H2
488@IHl #l'
489[ #empty_l' @IHr #r'
490  [ #empty_r' cases o [ @H1 * try #p normalize // ]
491    #v change with (P (insert ? one v (pm_node ? (None ?) ??)))
492    @H2 [ @H1 * try #p normalize // | % ]
493  ]
494]
495#p #v #H #G
496[ change with (P (insert ? (p1 p) v (pm_node ? ???)))
497| change with (P (insert ? (p0 p) v (pm_node ? ???)))
498] @H2 assumption
499qed.
500
501include alias "basics/logic.ma".
502include alias "common/PositiveMap.ma".
503
504lemma swap_neg : ∀A,B : Prop.(A → B) → ¬B → ¬A.
505#A #B #impl * #Bf % #At @Bf @impl @At qed-.
506
507definition b_graph_transform_program_props ≝
508  λsrc,dst : sem_graph_params.
509  λstacksizes.
510  λdata,prog_in.
511  λinit_regs : block → list register.
512  λf_lbls : block → label → list label.
513  λf_regs : block → label → list register.
514   let prog_out ≝ b_graph_transform_program src dst data prog_in in
515   let src_genv ≝ joint_globalenv src prog_in stacksizes in
516   let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
517  ∀bl,def_in.
518  find_funct_ptr … src_genv bl = return (Internal ? def_in) →
519  ∃init_data,def_out.
520  find_funct_ptr … dst_genv bl = return (Internal ? def_out) ∧
521  bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
522  b_graph_translate_props src dst ? init_data
523    def_in def_out (f_lbls bl) (f_regs bl).
524
525lemma make_b_graph_transform_program_props :
526 ∀src,dst:sem_graph_params.
527 ∀stacksizes.
528 ∀data : ∀globals.joint_closed_internal_function src globals →
529  bound_b_graph_translate_data src dst globals.
530 ∀prog_in : joint_program src.
531 let prog_out ≝ b_graph_transform_program … data prog_in in
532 let src_genv ≝ joint_globalenv src prog_in stacksizes in
533 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
534 ∃init_regs : block → list register.
535 ∃f_lbls : block → label → list label.
536 ∃f_regs : block → label → list register.
537 b_graph_transform_program_props src dst stacksizes data prog_in init_regs f_lbls f_regs.
538cases daemon (* TOREDO
539#src #dst #data #prog_in
540whd in match b_graph_transform_program_props; normalize nodelta
541whd in match joint_globalenv; normalize nodelta
542letin prog_out ≝ (b_graph_transform_program … data prog_in)
543letin src_genv ≝ (globalenv … (λx.x) prog_in)
544letin dst_genv ≝ (globalenv … (λx.x) prog_out)
545cut (∀p.lookup_opt ? p (functions ? dst_genv) =
546     option_map ?? (transf_fundef … (λf.b_graph_translate … (data … f) f))
547      (lookup_opt ? p (functions ? src_genv)))
548[ @functions_transf ]
549cut (symbols ? dst_genv = symbols ? src_genv)
550[ @symbols_transf ]
551cases dst_genv #functs2 #nextf2 #symbols2 #H2
552cases src_genv #functs1 #nextf1 #symbols1 #H1 #EQ destruct
553lapply H2 lapply H1 lapply functs2
554@(pm_map_add_ind … functs1) -functs1 -functs2 #functs1
555[ #functs1_empty | #p #f #IH #p_not_in ]
556#functs2 #H1 #H2 #transf
557[ %{(λ_.[ ])} %{(λ_.λ_.[])} %{(λ_.λ_.[])}
558  #bl #def_in #ABS1 #ABS2 @⊥ lapply ABS2 -ABS2 lapply ABS1 -ABS1
559  whd in match find_funct_ptr;
560  whd in match find_symbol;
561  normalize nodelta
562  cases bl; * normalize nodelta
563  [2,3: #p ]
564  [1,3: #_ whd in ⊢ (???%→?); #EQ destruct ]
565  >lookup_add_hit
566  #H >lookup_opt_insert_miss
567  [2: @(swap_neg … H) #EQ >EQ % ]
568  whd in match drop_fn; normalize nodelta
569  cases (lookup … symbols1 pre_main_id)
570  normalize nodelta
571  [ >functs1_empty | ** [2,3: #p' ] normalize nodelta
572    [1,3: >functs1_empty
573    | @lookup_opt_pm_set_elim #H destruct
574      [2: >functs1_empty ]
575    ]
576  ] whd in ⊢ (???%→?); #EQ destruct
577]
578cases (IH (pm_set … p (None ?) functs2) ???)
579[|*: @hide_prf
580  [ #b #G @(H1 b ?) @(swap_neg … G) -G
581    whd in match insert; normalize nodelta
582    @lookup_opt_pm_set_elim
583    [ #EQ #ABS destruct ]
584    #NEQ #H @H
585  | #b #G @(H2 b ?) @(swap_neg … G) -G
586    @lookup_opt_pm_set_elim
587    [ #_ #_ % ]
588    #_ #H @H
589  | #b @lookup_opt_pm_set_elim
590    [ #EQ destruct >p_not_in % ]
591    #NEQ >transf
592    >(lookup_opt_insert_miss ? f b p … NEQ) %
593  ]
594]
595#init_regs * #f_lbls * #f_regs #props
596-IH cases f in H1 transf; -f #f #H1 #transf
597[ (* internal *)
598  letin upd ≝ (λA : Type[0].λf : block → A.
599    λid.λv,id'.
600    if eq_block id id' then v else f id')
601  cases (pi2 ?? (b_graph_translate … (data … f) f))
602  #loc_data * #loc_init_regs * #loc_f_lbls * #loc_f_regs *
603  #inst_loc_data #loc_props
604  letin bl ≝ (mk_block (neg p))
605  %{(upd … init_regs bl loc_init_regs)}
606  %{(upd … f_lbls bl loc_f_lbls)}
607  %{(upd … f_regs bl loc_f_regs)}
608| (* external, nothing changes *)
609  %{init_regs}
610  %{f_lbls}
611  %{f_regs}
612]
613* #p' #def_in
614whd in match find_funct_ptr; normalize nodelta
615whd in match (block_region (mk_block p'));
616cases p' -p' [2,3,5,6: #p' ] normalize nodelta
617[1,3,5,6: #_ #ABS normalize in ABS; destruct]
618whd in match find_symbol;
619whd in match insert; normalize nodelta
620#bl_prf
621@lookup_opt_pm_set_elim #pp' destruct
622[1,3: whd in ⊢ (??%%→?); #EQ destruct(EQ)
623  [ %{loc_data} %
624    [2: % [ % ]
625      [ >lookup_opt_insert_hit %
626      |*: >eq_block_b_b assumption
627      ]
628    |]
629|*: >(lookup_opt_insert_miss ???? functs1 … pp')
630  [ @eq_block_elim [ #EQ destruct cases (absurd ?? pp') % ] #_ normalize nodelta]
631  #EQ lapply (props (mk_block (neg p')) def_in EQ)
632  whd in match find_funct_ptr; normalize nodelta
633  >(lookup_opt_pm_set_miss … functs2 … pp') #H @H
634] *)
635qed.
636
637lemma if_elim' : ∀A : Type[0].∀P : A → Prop.∀b : bool.∀c1,c2 : A.
638  (b → P c1) → (¬(bool_to_Prop b) → P c2) → P (if b then c1 else c2).
639#A #P * /3 by Prop_notb/ qed.
640
641lemma b_graph_transform_program_fetch_internal_function :
642 ∀src,dst:sem_graph_params.
643 ∀stacksizes.
644 ∀data : ∀globals.joint_closed_internal_function src globals →
645  bound_b_graph_translate_data src dst globals.
646 ∀prog_in : joint_program src.
647 ∀init_regs : block → list register.
648 ∀f_lbls : block → label → list label.
649 ∀f_regs : block → label → list register.
650 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs →
651 let prog_out ≝ b_graph_transform_program … data prog_in in
652 let src_genv ≝ joint_globalenv src prog_in stacksizes in
653 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
654 ∀bl : Σbl.block_region … bl = Code.∀id,def_in.
655 if eqZb (block_id … bl) (-1) then
656   (fetch_internal_function … dst_genv bl =
657     return 〈pre_main_id, pre_main_generator … dst prog_out〉)
658 else
659   (fetch_internal_function … src_genv bl = return 〈id, def_in〉 →
660   ∃init_data,def_out.
661   fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
662   bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
663   b_graph_translate_props src dst ? init_data
664      def_in def_out (f_lbls bl) (f_regs bl)).
665#src #dst #stacksizes #data #prog_in
666#init_regs #f_lbls #f_regs #props
667#bl #id #def_in
668@if_elim' #Hbl
669[ whd in match fetch_internal_function; whd in match fetch_function;
670  normalize nodelta >Hbl % ]
671#H @('bind_inversion H) * #id' * #def_in' -H
672normalize nodelta [2: #_ whd in ⊢ (??%%→?); #ABS destruct ]
673whd in match fetch_function; normalize nodelta
674>Hbl normalize nodelta
675#H @('bind_inversion (opt_eq_from_res … H)) -H #id'' #EQ1
676#H @('bind_inversion H) -H #def_in'' #H
677whd in ⊢ (??%%→??%%→?); #EQ2 #EQ3 destruct
678cases (props … H)
679#loc_data * #def_out ** #H1 #H2 #H3
680%{loc_data} %{def_out}
681%{H3} %{H2}
682whd in match fetch_internal_function;
683whd in match fetch_function; normalize nodelta
684>Hbl normalize nodelta
685whd in match joint_globalenv; normalize nodelta
686whd in match prog_names; normalize nodelta
687>symbol_for_block_transf >EQ1 >m_return_bind
688>H1 %
689qed.
690
691lemma b_graph_transform_program_fetch_statement :
692 ∀src,dst:sem_graph_params.∀stacksizes.
693 ∀data : ∀globals.joint_closed_internal_function src globals →
694  bound_b_graph_translate_data src dst globals.
695 ∀prog_in : joint_program src.
696 ∀init_regs : block → list register.
697 ∀f_lbls : block → label → list label.
698 ∀f_regs : block → label → list register.
699 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs →
700 let prog_out ≝ b_graph_transform_program … data prog_in in
701 let src_genv ≝ joint_globalenv src prog_in stacksizes in
702 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
703 ∀pc,id,def_in,s.
704 if eqZb (block_id … (pc_block … pc)) (-1) then
705   (fetch_internal_function … dst_genv (pc_block … pc) =
706     return 〈pre_main_id, pre_main_generator … dst prog_out〉)
707 else
708   (fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
709   ∃init_data,def_out.
710   let bl ≝ pc_block pc in
711   fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
712   bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
713   let l ≝ point_of_pc dst pc in
714    let lbls ≝ f_lbls bl l in let regs ≝ f_regs bl l in
715    match s with
716    [ sequential s' nxt ⇒
717      let block ≝
718        if not_emptyb … (added_prologue … init_data) ∧
719           eq_identifier … (joint_if_entry … def_in) l then
720          bret … [ ]
721        else
722          f_step … init_data l s' in
723      l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
724    | final s' ⇒
725      l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
726    | FCOND abs _ _ _ ⇒ Ⓧabs
727    ]).
728#src #dst #stacksizes #data #prog_in
729#init_regs #f_lbls #f_regs #props
730#pc #id #def_in #s
731lapply (b_graph_transform_program_fetch_internal_function … props
732  (pc_block … pc) id def_in)
733@if_elim' #Hbl >Hbl normalize nodelta [ #H @H ] #G
734#H @('bind_inversion H) * #id' #def_in' -H
735#EQfif
736#H @('bind_inversion H) -H #s
737#H lapply (opt_eq_from_res ???? H) -H
738#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
739cases (G … EQfif)
740#a * #b ** #H1 #H2 #H3 %{a} %{b} %
741[ %{H1 H2}
742| @(multi_fetch_ok … H3 … EQstmt_at)
743]
744qed.
745
746lemma b_graph_transform_program_fetch_statement_plus :
747 ∀src,dst:sem_graph_params.∀stacksizes.
748 ∀data : ∀globals.joint_closed_internal_function src globals →
749  bound_b_graph_translate_data src dst globals.
750 ∀prog_in : joint_program src.
751 ∀init_regs : block → list register.
752 ∀f_lbls : block → label → list label.
753 ∀f_regs : block → label → list register.
754 b_graph_transform_program_props … stacksizes data prog_in init_regs f_lbls f_regs →
755 let prog_out ≝ b_graph_transform_program … data prog_in in
756 let src_genv ≝ joint_globalenv src prog_in stacksizes in
757 let dst_genv ≝ joint_globalenv dst prog_out stacksizes in
758 ∀pc,id,def_in,s.
759 if eqZb (block_id … (pc_block … pc)) (-1) then
760   (fetch_internal_function … dst_genv (pc_block … pc) =
761     return 〈pre_main_id, pre_main_generator … dst prog_out〉)
762 else
763   (fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
764   ∃init_data,def_out.
765   let bl ≝ pc_block pc in
766   fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
767   bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
768   let l ≝ point_of_pc dst pc in
769   let lbls ≝ f_lbls bl l in
770   let regs ≝ f_regs bl l in
771   partial_partition … (f_lbls bl) ∧
772   partial_partition … (f_regs bl) ∧
773   (∀l.All …
774      (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
775             fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧
776    (∀l.All …
777      (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
778             fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧
779   match s with
780    [ sequential s' nxt ⇒
781      let block ≝
782        if not_emptyb … (added_prologue … init_data) ∧
783           eq_identifier … (joint_if_entry … def_in) l then
784          bret … [ ]
785        else
786          f_step … init_data l s' in
787      l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
788    | final s' ⇒
789      l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
790    | FCOND abs _ _ _ ⇒ Ⓧabs
791    ]).
792#src #dst #stacksizes #data #prog_in
793#init_regs #f_lbls #f_regs #props
794#pc #id #def_in #s
795lapply (b_graph_transform_program_fetch_internal_function … props … (pc_block … pc) id def_in)
796@if_elim' #Hbl >Hbl normalize nodelta
797[ #H @H ] #G
798#H @('bind_inversion H) * #id' #def_in' -H
799#EQfif
800#H @('bind_inversion H) -H #s
801#H lapply (opt_eq_from_res ???? H) -H
802#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
803cases (G … EQfif)
804#a * #b ** #H1 #H2 #H3 %{a} %{b} %
805[ %{H1 H2}
806| %{(multi_fetch_ok … H3 … EQstmt_at)}
807  %{(freshness_regs … H3)}
808  %{(freshness_lbls … H3)}
809  %{(partition_regs … H3)}
810  @(partition_lbls … H3)
811]         
812qed.
Note: See TracBrowser for help on using the repository browser.