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