1 | include "joint/semanticsUtils.ma". |
---|
2 | include "common/StructuredTraces.ma". |
---|
3 | |
---|
4 | record evaluation_params (p : sem_params) : Type[0] ≝ |
---|
5 | { globals : list ident |
---|
6 | ; ev_genv :> genv p globals |
---|
7 | }. |
---|
8 | |
---|
9 | record prog_params : Type[1] ≝ |
---|
10 | { prog_spars :> sem_params |
---|
11 | ; prog : joint_program prog_spars |
---|
12 | ; stack_sizes : ident → option ℕ |
---|
13 | (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) |
---|
14 | }. |
---|
15 | |
---|
16 | definition joint_make_global : ∀p : prog_params.evaluation_params (prog_spars p) ≝ |
---|
17 | λp.mk_evaluation_params ? |
---|
18 | (prog_names … (prog p)) |
---|
19 | (joint_globalenv p (prog p) (stack_sizes p)). |
---|
20 | |
---|
21 | coercion joint_make_global : ∀p : prog_params.evaluation_params (prog_spars p) ≝ |
---|
22 | joint_make_global on p : prog_params to evaluation_params ?. |
---|
23 | |
---|
24 | definition make_initial_state : |
---|
25 | ∀pars: prog_params.res (state_pc pars) ≝ |
---|
26 | λpars.let p ≝ prog pars in |
---|
27 | let ge ≝ ev_genv pars in |
---|
28 | (* this is going to change shortly: globals will not reside in globalenv anymore *) |
---|
29 | ! m0 ← init_mem … (λx.x) p ; |
---|
30 | let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in |
---|
31 | let globals_size ≝ globals_stacksize … p in |
---|
32 | (* stack pointer should start at 2^16 - |globals|, right? |
---|
33 | first call to main shuold bring it to 2^16 - |globals| - |main stack| |
---|
34 | Also, on words 2^16 - |globals| = - |globals| *) |
---|
35 | (* mcu8051ide disallows byte FFFFh of XDATA... bug or feature? *) |
---|
36 | let spp : xpointer ≝ |
---|
37 | «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-S (globals_size)))), |
---|
38 | pi2 … spb» in |
---|
39 | (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) |
---|
40 | let main ≝ prog_main … p in |
---|
41 | let st ≝ mk_state pars |
---|
42 | (* frames ≝ *)(Some ? (empty_framesT …)) |
---|
43 | (* internal_stack ≝ *) empty_is |
---|
44 | (* carry ≝ *)(BBbit false) |
---|
45 | (* regs ≝ *)(empty_regsT … spp) |
---|
46 | (* mem ≝ *)m |
---|
47 | (* stack_usage ≝ *)0 in |
---|
48 | return |
---|
49 | mk_state_pc ? |
---|
50 | (* state_no_pc ≝ *)(set_sp … spp st) |
---|
51 | (* pc ≝ *)init_pc |
---|
52 | (* last_pop ≝ *)(null_pc one). |
---|
53 | @hide_prf |
---|
54 | cases m0 in H; #m1 #m2 #m3 #H |
---|
55 | whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥ |
---|
56 | @(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by Zlt_to_Zle_to_Zlt/ |
---|
57 | qed. |
---|
58 | |
---|
59 | definition joint_classify_step : |
---|
60 | ∀p,globals.joint_step p globals → status_class ≝ |
---|
61 | λp,g,stmt. |
---|
62 | match stmt with |
---|
63 | [ CALL f args dest ⇒ cl_call |
---|
64 | | COND _ _ ⇒ cl_jump |
---|
65 | | _ ⇒ cl_other |
---|
66 | ]. |
---|
67 | |
---|
68 | definition joint_classify_final : |
---|
69 | ∀p.joint_fin_step p → status_class ≝ |
---|
70 | λp,stmt. |
---|
71 | match stmt with |
---|
72 | [ GOTO _ ⇒ cl_other |
---|
73 | | RETURN ⇒ cl_return |
---|
74 | | TAILCALL _ f args ⇒ cl_tailcall |
---|
75 | ]. |
---|
76 | |
---|
77 | definition joint_classify : |
---|
78 | ∀p.∀pars : evaluation_params p.state_pc p → status_class ≝ |
---|
79 | λp,pars,st. |
---|
80 | match fetch_statement … (ev_genv … pars) (pc … st) with |
---|
81 | [ OK i_fn_s ⇒ |
---|
82 | match \snd i_fn_s with |
---|
83 | [ sequential s _ ⇒ joint_classify_step … s |
---|
84 | | final s ⇒ joint_classify_final … s |
---|
85 | | FCOND _ _ _ _ ⇒ cl_jump |
---|
86 | ] |
---|
87 | | _ ⇒ cl_other |
---|
88 | ]. |
---|
89 | |
---|
90 | lemma joint_classify_call : ∀p,pars,st. |
---|
91 | joint_classify p pars st = cl_call → |
---|
92 | ∃i_f,f',args,dest,next. |
---|
93 | fetch_statement … (ev_genv … pars) (pc … st) = |
---|
94 | OK ? 〈i_f, sequential … (CALL … f' args dest) next〉. |
---|
95 | #p #pars #st |
---|
96 | whd in match joint_classify; normalize nodelta |
---|
97 | inversion (fetch_statement ????) |
---|
98 | [2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] |
---|
99 | * #i_f * |
---|
100 | [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_ |
---|
101 | normalize nodelta normalize in ⊢ (%→?); #ABS destruct |
---|
102 | ] |
---|
103 | * [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch normalize nodelta |
---|
104 | normalize in ⊢ (%→?); #EQ destruct |
---|
105 | %[|%[|%[|%[|%[| %]]]]] |
---|
106 | qed. |
---|
107 | |
---|
108 | definition joint_after_ret : ∀p : sem_params.∀pars. |
---|
109 | (Σs : state_pc p.joint_classify p pars s = cl_call) → state_pc p → Prop ≝ |
---|
110 | λp,pars,s1,s2. |
---|
111 | match fetch_statement … (ev_genv … pars) (pc … s1) with |
---|
112 | [ OK x ⇒ |
---|
113 | match \snd x with |
---|
114 | [ sequential s next ⇒ |
---|
115 | last_pop … s2 = pc … s1 ∧ |
---|
116 | pc … s2 = succ_pc p (pc … s1) next |
---|
117 | | _ ⇒ False (* never happens *) |
---|
118 | ] |
---|
119 | | _ ⇒ False (* never happens *) |
---|
120 | ]. |
---|
121 | |
---|
122 | definition joint_call_ident : ∀p : sem_params.∀pars. |
---|
123 | state_pc p → ident ≝ |
---|
124 | (* this is a definition without a dummy ident : |
---|
125 | λp,st. |
---|
126 | match ? |
---|
127 | return λx. |
---|
128 | !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ; |
---|
129 | match s with |
---|
130 | [ sequential s next ⇒ |
---|
131 | match s with |
---|
132 | [ CALL f' args dest ⇒ function_of_call … (ev_genv p) st f' |
---|
133 | | _ ⇒ Error … [ ] |
---|
134 | ] |
---|
135 | | _ ⇒ Error … [ ] |
---|
136 | ] = x → ? with |
---|
137 | [ OK v ⇒ λ_.v |
---|
138 | | Error e ⇒ λABS.⊥ |
---|
139 | ] (refl …). |
---|
140 | @hide_prf |
---|
141 | elim (joint_classify_call … (pi2 … st)) |
---|
142 | #f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3 |
---|
143 | lapply ABS -ABS |
---|
144 | >EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS) |
---|
145 | qed. *) |
---|
146 | (* with a dummy ident (which is never used as seen above in the commented script) |
---|
147 | I think handling of the function is easier *) |
---|
148 | λp,pars,st. |
---|
149 | let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) |
---|
150 | match fetch_statement … (ev_genv … pars) (pc … st) with |
---|
151 | [ OK x ⇒ |
---|
152 | match \snd x with |
---|
153 | [ sequential s next ⇒ |
---|
154 | match s with |
---|
155 | [ CALL f' args dest ⇒ |
---|
156 | match |
---|
157 | (! bl ← block_of_call … (ev_genv … pars) f' st; |
---|
158 | fetch_internal_function … (ev_genv … pars) bl) with |
---|
159 | [ OK i_f ⇒ \fst i_f |
---|
160 | | _ ⇒ dummy |
---|
161 | ] |
---|
162 | | _ ⇒ dummy |
---|
163 | ] |
---|
164 | | _ ⇒ dummy |
---|
165 | ] |
---|
166 | | _ ⇒ dummy |
---|
167 | ]. |
---|
168 | |
---|
169 | definition joint_tailcall_ident : ∀p:sem_params.∀pars. |
---|
170 | state_pc p → ident ≝ |
---|
171 | λp,pars,st. |
---|
172 | let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) |
---|
173 | match fetch_statement … (ev_genv … pars) (pc … st) with |
---|
174 | [ OK x ⇒ |
---|
175 | match \snd x with |
---|
176 | [ final s ⇒ |
---|
177 | match s with |
---|
178 | [ TAILCALL _ f' args ⇒ |
---|
179 | match |
---|
180 | (! bl ← block_of_call … (ev_genv … pars) f' st; |
---|
181 | fetch_internal_function … (ev_genv … pars) bl) with |
---|
182 | [ OK i_f ⇒ \fst i_f |
---|
183 | | _ ⇒ dummy |
---|
184 | ] |
---|
185 | | _ ⇒ dummy |
---|
186 | ] |
---|
187 | | _ ⇒ dummy |
---|
188 | ] |
---|
189 | | _ ⇒ dummy |
---|
190 | ]. |
---|
191 | |
---|
192 | definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?. |
---|
193 | *#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim |
---|
194 | [ #EQ destruct % #H % |
---|
195 | | * #NEQ % #ABS destruct elim (NEQ ?) % |
---|
196 | ] |
---|
197 | qed. |
---|
198 | |
---|
199 | (* |
---|
200 | let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝ |
---|
201 | match c with |
---|
202 | [ Value x ⇒ OK … x |
---|
203 | | Interact o f ⇒ |
---|
204 | ! i ← env o ; |
---|
205 | io_evaluate O I X env (f i) |
---|
206 | | Wrong e ⇒ Error … e |
---|
207 | ]. |
---|
208 | *) |
---|
209 | |
---|
210 | definition cost_label_of_stmt : |
---|
211 | ∀p,globals.joint_statement p globals → option costlabel ≝ |
---|
212 | λp,g,s.match s with |
---|
213 | [ sequential s _ ⇒ |
---|
214 | match s with |
---|
215 | [ COST_LABEL lbl ⇒ Some ? lbl |
---|
216 | | _ ⇒ None ? |
---|
217 | ] |
---|
218 | | _ ⇒ None ? |
---|
219 | ]. |
---|
220 | |
---|
221 | definition joint_label_of_pc ≝ |
---|
222 | λp,pars. |
---|
223 | (λpc. |
---|
224 | match fetch_statement … (ev_genv p pars) pc with |
---|
225 | [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt) |
---|
226 | | _ ⇒ None ? |
---|
227 | ]). |
---|
228 | |
---|
229 | (* the prime is to render obsolete old definition of exit_pc, remove when all is corrected *) |
---|
230 | definition exit_pc' : program_counter ≝ |
---|
231 | mk_program_counter «mk_block (-1), refl …» (p1 one). |
---|
232 | |
---|
233 | definition joint_final: ∀p: sem_params.∀pars. |
---|
234 | state_pc p → option int ≝ |
---|
235 | λp,pars,st. |
---|
236 | let ge ≝ ev_genv p pars in |
---|
237 | if eq_program_counter (pc … st) exit_pc' then |
---|
238 | let ret ≝ call_dest_for_main ?? p in |
---|
239 | match (! vals ← read_result … ge ret st ; |
---|
240 | Word_of_list_beval vals) |
---|
241 | with |
---|
242 | [ OK v ⇒ Some ? v |
---|
243 | | Error _ ⇒ Some … (maximum ?) ] |
---|
244 | else None ?. |
---|
245 | |
---|
246 | definition joint_abstract_status : |
---|
247 | ∀p : prog_params. |
---|
248 | abstract_status ≝ |
---|
249 | λp. |
---|
250 | mk_abstract_status |
---|
251 | (* as_status ≝ *) (state_pc p) |
---|
252 | (* as_execute ≝ *) |
---|
253 | (λs1,s2.eval_state … (ev_genv … p) s1 = return s2) |
---|
254 | (* (* as_init ≝ *) (make_initial_state p) *) |
---|
255 | (* as_pc ≝ *) pcDeq |
---|
256 | (* as_pc_of ≝ *) (pc …) |
---|
257 | (* as_classify ≝ *) (joint_classify … p) |
---|
258 | (* as_label_of_pc ≝ *) (joint_label_of_pc … p) |
---|
259 | (* as_after_return ≝ *) (joint_after_ret … p) |
---|
260 | (* as_result ≝ *) (joint_final … p) |
---|
261 | (* as_call_ident ≝ *) (λst.joint_call_ident … p st) |
---|
262 | (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident … p st). |
---|
263 | |
---|
264 | (* alternative definition with integrated prog_params constructor *) |
---|
265 | definition joint_status : |
---|
266 | ∀p : sem_params. |
---|
267 | joint_program p → (ident → option ℕ) → abstract_status ≝ |
---|
268 | λp,prog,stacksizes.joint_abstract_status (mk_prog_params p prog stacksizes). |
---|