1 | include "joint/joint_semantics.ma". |
---|
2 | include alias "common/Identifiers.ma". |
---|
3 | include "utilities/hide.ma". |
---|
4 | include "ASM/BitVectorTrie.ma". |
---|
5 | include "joint/TranslateUtils.ma". |
---|
6 | |
---|
7 | record hw_register_env : Type[0] ≝ |
---|
8 | { reg_env : BitVectorTrie beval 6 |
---|
9 | ; other_bit : bebit |
---|
10 | }. |
---|
11 | |
---|
12 | definition empty_hw_register_env: hw_register_env ≝ |
---|
13 | mk_hw_register_env (Stub …) BBundef. |
---|
14 | |
---|
15 | include alias "ASM/BitVectorTrie.ma". |
---|
16 | |
---|
17 | definition hwreg_retrieve: hw_register_env → Register → beval ≝ |
---|
18 | λenv,r. lookup … (bitvector_of_register r) (reg_env env) BVundef. |
---|
19 | |
---|
20 | definition hwreg_store: Register → beval → hw_register_env → hw_register_env ≝ |
---|
21 | λr,v,env.mk_hw_register_env (insert … (bitvector_of_register r) v (reg_env env)) |
---|
22 | (other_bit env). |
---|
23 | |
---|
24 | definition hwreg_set_other : bebit → hw_register_env → hw_register_env ≝ |
---|
25 | λv,env.mk_hw_register_env (reg_env env) v. |
---|
26 | |
---|
27 | definition hwreg_retrieve_sp : hw_register_env → res xpointer ≝ |
---|
28 | λenv. |
---|
29 | let spl ≝ hwreg_retrieve env RegisterSPL in |
---|
30 | let sph ≝ hwreg_retrieve env RegisterSPH in |
---|
31 | ! ptr ← pointer_of_address 〈spl, sph〉 ; |
---|
32 | match ptype ptr return λx.ptype ptr = x → res xpointer with |
---|
33 | [ XData ⇒ λprf.return «ptr, prf» |
---|
34 | | _ ⇒ λ_.Error … [MSG BadPointer] |
---|
35 | ] (refl …). |
---|
36 | |
---|
37 | definition hwreg_store_sp : hw_register_env → xpointer → hw_register_env ≝ |
---|
38 | λenv,sp. |
---|
39 | let 〈spl, sph〉 ≝ beval_pair_of_pointer sp in |
---|
40 | hwreg_store RegisterSPH sph (hwreg_store RegisterSPL spl env). |
---|
41 | |
---|
42 | (*** Store/retrieve on pseudo-registers ***) |
---|
43 | include alias "common/Identifiers.ma". |
---|
44 | |
---|
45 | record reg_sp : Type[0] ≝ |
---|
46 | { reg_sp_env :> identifier_map RegisterTag beval |
---|
47 | ; stackp : xpointer |
---|
48 | }. |
---|
49 | |
---|
50 | definition reg_store ≝ λreg,v,locals. update RegisterTag beval locals reg v. |
---|
51 | |
---|
52 | definition reg_retrieve : register_env beval → register → res beval ≝ |
---|
53 | λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup … locals reg). |
---|
54 | |
---|
55 | definition reg_sp_store ≝ λreg,v,locals. |
---|
56 | ! locals' ← reg_store reg v (reg_sp_env locals) ; |
---|
57 | return mk_reg_sp locals' (stackp locals). |
---|
58 | |
---|
59 | definition reg_sp_retrieve ≝ λlocals.reg_retrieve locals. |
---|
60 | |
---|
61 | (*** Store/retrieve on hardware registers ***) |
---|
62 | |
---|
63 | definition init_hw_register_env: xpointer → hw_register_env ≝ |
---|
64 | λsp.hwreg_store_sp empty_hw_register_env sp. |
---|
65 | |
---|
66 | (******************************** GRAPHS **************************************) |
---|
67 | |
---|
68 | record sem_graph_params : Type[1] ≝ |
---|
69 | { sgp_pars : unserialized_params |
---|
70 | ; sgp_sup : ∀F.sem_unserialized_params sgp_pars F |
---|
71 | }. |
---|
72 | |
---|
73 | definition sem_graph_params_to_graph_params : |
---|
74 | ∀pars : sem_graph_params.graph_params ≝ |
---|
75 | λpars.mk_graph_params (sgp_pars pars). |
---|
76 | |
---|
77 | coercion graph_params_from_sem_graph_params nocomposites : |
---|
78 | ∀pars : sem_graph_params. |
---|
79 | graph_params ≝ sem_graph_params_to_graph_params |
---|
80 | on _pars : sem_graph_params to graph_params. |
---|
81 | |
---|
82 | definition sem_graph_params_to_sem_params : |
---|
83 | ∀pars : sem_graph_params. |
---|
84 | sem_params ≝ |
---|
85 | λpars. |
---|
86 | mk_sem_params |
---|
87 | (pars : graph_params) |
---|
88 | (sgp_sup pars ?) |
---|
89 | (word_of_identifier ?) |
---|
90 | (an_identifier ?) |
---|
91 | ? (refl …). |
---|
92 | * #p % qed. |
---|
93 | |
---|
94 | coercion sem_params_from_sem_graph_params : |
---|
95 | ∀pars : sem_graph_params. |
---|
96 | sem_params ≝ sem_graph_params_to_sem_params |
---|
97 | on _pars : sem_graph_params to sem_params. |
---|
98 | |
---|
99 | |
---|
100 | (******************************** LINEAR **************************************) |
---|
101 | |
---|
102 | lemma succ_pos_of_nat_of_pos : ∀p.succ_pos_of_nat (nat_of_pos p) = succ p. |
---|
103 | @pos_elim [%] |
---|
104 | #p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed. |
---|
105 | |
---|
106 | record sem_lin_params : Type[1] ≝ |
---|
107 | { slp_pars : unserialized_params |
---|
108 | ; slp_sup : ∀F.sem_unserialized_params slp_pars F |
---|
109 | }. |
---|
110 | |
---|
111 | definition sem_lin_params_to_lin_params : |
---|
112 | ∀pars : sem_lin_params.lin_params ≝ |
---|
113 | λpars.mk_lin_params (slp_pars pars). |
---|
114 | |
---|
115 | coercion lin_params_from_sem_lin_params nocomposites : |
---|
116 | ∀pars : sem_lin_params. |
---|
117 | lin_params ≝ sem_lin_params_to_lin_params |
---|
118 | on _pars : sem_lin_params to lin_params. |
---|
119 | |
---|
120 | definition sem_lin_params_to_sem_params : |
---|
121 | ∀pars : sem_lin_params. |
---|
122 | sem_params ≝ |
---|
123 | λpars. |
---|
124 | mk_sem_params |
---|
125 | (pars : lin_params) |
---|
126 | (slp_sup pars ?) |
---|
127 | succ_pos_of_nat |
---|
128 | (λp.pred (nat_of_pos p)) |
---|
129 | ??. |
---|
130 | [ #n >nat_succ_pos % |
---|
131 | | @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos |
---|
132 | ] qed. |
---|
133 | |
---|
134 | coercion sem_params_from_sem_lin_params : |
---|
135 | ∀pars : sem_lin_params. |
---|
136 | sem_params ≝ sem_lin_params_to_sem_params |
---|
137 | on _pars : sem_lin_params to sem_params. |
---|
138 | |
---|
139 | |
---|
140 | lemma fetch_statement_eq : ∀p:sem_params.∀g. |
---|
141 | ∀ge : genv_t (joint_function p g).∀ptr : program_counter. |
---|
142 | ∀i,fn,s. |
---|
143 | fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 → |
---|
144 | let pt ≝ point_of_pc … ptr in |
---|
145 | stmt_at … (joint_if_code … fn) pt = Some ? s → |
---|
146 | fetch_statement … ge ptr = OK … 〈i, fn, s〉. |
---|
147 | #p #g #ge #ptr #i #f #s #EQ1 #EQ2 |
---|
148 | whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind |
---|
149 | >EQ2 % |
---|
150 | qed. |
---|
151 | |
---|
152 | lemma fetch_statement_inv : ∀p:sem_params.∀g. |
---|
153 | ∀ge : genv_t (joint_function p g).∀ptr : program_counter. |
---|
154 | ∀i,fn,s. |
---|
155 | fetch_statement … ge ptr = OK … 〈i, fn, s〉 → |
---|
156 | fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧ |
---|
157 | let pt ≝ point_of_pc p ptr in |
---|
158 | stmt_at … (joint_if_code … fn) pt = Some ? s. |
---|
159 | #p #g #ge #ptr #i #fn #s #H |
---|
160 | elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H |
---|
161 | elim (bind_inversion ????? H) #s' * #H |
---|
162 | lapply (opt_eq_from_res ???? H) -H #EQ2 |
---|
163 | whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} |
---|
164 | qed. |
---|
165 | |
---|
166 | axiom b_graph_transform_program_props : |
---|
167 | ∀src,dst:sem_graph_params. |
---|
168 | ∀data : ∀globals.joint_closed_internal_function src globals → |
---|
169 | bind_new register (b_graph_translate_data src dst globals). |
---|
170 | ∀prog_in : joint_program src. |
---|
171 | let prog_out ≝ b_graph_transform_program … data prog_in in |
---|
172 | let src_genv ≝ globalenv_noinit ? prog_in in |
---|
173 | let dst_genv ≝ globalenv_noinit ? prog_out in |
---|
174 | ∃init_regs : ident → list register. |
---|
175 | ∃f_lbls : ident → label → option (list label). |
---|
176 | ∃f_regs : ident → label → option (list register). |
---|
177 | ∀bl,id,def_in. |
---|
178 | fetch_internal_function ? src_genv bl = return 〈id, def_in〉 → |
---|
179 | ∃init_data,def_out. |
---|
180 | fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧ |
---|
181 | bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧ |
---|
182 | b_graph_translate_props src dst ? init_data (init_regs id) |
---|
183 | def_in def_out (f_lbls id) (f_regs id). |
---|