source: src/joint/Traces.ma @ 2553

Last change on this file since 2553 was 2553, checked in by tranquil, 8 years ago

as_classify changed to a partial function
added a status for tailcalls

File size: 11.3 KB
Line 
1include "joint/semantics.ma".
2include "common/StructuredTraces.ma".
3
4record evaluation_params : Type[1] ≝
5 { globals: list ident
6 ; sparams:> sem_params
7 ; exit: program_counter
8 ; ev_genv: genv sparams globals
9(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
10 }.
11 
12
13
14record prog_params : Type[1] ≝
15 { prog_spars : sem_params
16 ; prog : joint_program prog_spars
17 ; stack_sizes : ident → option ℕ
18(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
19 }.
20
21lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l.
22#A #B #f #P #l elim l -l [*]
23#hd #tl #IH *
24[ #Phd %1{Phd}
25| #Ptl %2{(IH Ptl)}
26]
27qed.
28
29lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x.
30#A #P #l elim l -l [*] #hd #tl #IH *
31[ #Phd %{hd} %{Phd} %1 %
32| #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1}
33]
34qed.
35
36lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l.
37#A #P #l elim l -l [ #x *] #hd #tl #IH #x *
38[ #EQ >EQ #H %1{H}
39| #Intl #Px %2{(IH … Intl Px)}
40]
41qed.
42
43lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
44#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
45
46definition make_global : prog_params → evaluation_params
47
48λpars.
49(* Invariant: a -1 block is unused in common/Globalenvs *)
50let b ≝ mk_block Code (-1) in
51let ptr ≝ mk_program_counter «b, refl …» one in
52let p ≝ prog pars in
53mk_evaluation_params
54  (prog_var_names … p)
55  (prog_spars pars)
56  ptr
57  (mk_genv_gen ?? (globalenv_noinit ? p) ? (stack_sizes pars))
58 (* (prog_io pars) *).
59#s #H
60elim (find_symbol_exists … p s ?)
61[ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
62@Exists_append_r
63@(Exists_mp … H) //
64qed.
65
66coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
67≝ make_global on _p : prog_params to evaluation_params.
68
69axiom BadMain : String.
70
71definition make_initial_state :
72 ∀pars: prog_params.res (state_pc pars) ≝
73λpars.let p ≝ prog pars in
74  let sem_globals : evaluation_params ≝ pars in
75  let ge ≝ ev_genv sem_globals in
76  let m ≝ alloc_mem … p in
77  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
78  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
79  let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
80  let spp : xpointer ≝
81    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
82     pi2 … spb» in
83(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
84  let main ≝ prog_main … p in
85  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
86  (* use exit sem_globals as ra and call_dest_for_main as dest *)
87  let st0' ≝ mk_state_pc … (set_sp … spp st0) (exit sem_globals) in
88  ! st0'' ← save_frame ?? sem_globals true (call_dest_for_main … pars) st0' ;
89  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
90  ! bl ← block_of_call … ge (inl … main) st_pc0;
91  ! 〈i, fn〉 ← fetch_function … ge bl ;
92  match fn with
93  [ Internal ifn ⇒
94    ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st_pc0 ;
95    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
96    return mk_state_pc … st' pc'
97  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
98  ].
99
100definition joint_classify_seq :
101  ∀p : evaluation_params.state p → joint_seq p (globals … p) → status_class ≝
102  λp,st,stmt.
103  match stmt with
104  [ CALL f args dest ⇒
105    match (! bl ← block_of_call … (ev_genv p) f st ;
106            fetch_function … (ev_genv p) bl) with
107    [ OK id_fn ⇒
108      match \snd id_fn with
109      [ Internal _ ⇒ cl_call
110      | External _ ⇒ cl_other
111      ]
112    | Error _ ⇒ cl_other
113    ]
114  | _ ⇒ cl_other
115  ].
116
117definition joint_classify_step :
118  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
119  λp,st,stmt.
120  match stmt with
121  [ step_seq s ⇒ joint_classify_seq p st s
122  | COND _ _ ⇒ cl_jump
123  ].
124
125definition joint_classify_final :
126  ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝
127  λp,st,stmt.
128  match stmt with
129  [ GOTO _ ⇒ cl_other
130  | RETURN ⇒ cl_return
131  | TAILCALL _ f args ⇒
132    match (! bl ← block_of_call … (ev_genv p) f st ;
133            fetch_function … (ev_genv p) bl) with
134    [ OK id_fn ⇒
135      match \snd id_fn with
136      [ Internal _ ⇒ cl_tailcall
137      | External _ ⇒ cl_return
138      ]
139    | Error _ ⇒ cl_other
140    ]
141  ].
142
143definition joint_classify :
144  ∀p : evaluation_params.state_pc p → option status_class ≝
145  λp,st.
146  ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
147  match s with
148  [ sequential s _ ⇒ Some ? (joint_classify_step p st s)
149  | final s ⇒ Some ? (joint_classify_final p st s)
150  | FCOND _ _ _ _ ⇒ Some ? cl_jump
151  ].
152
153definition no_call : ∀p,g.joint_seq p g → Prop ≝
154  λp,g,s.match s with
155  [ CALL _ _ _ ⇒ False
156  | _ ⇒ True
157  ].
158
159definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
160  λp,g,s.match s with
161  [ COST_LABEL _ ⇒ False
162  | _ ⇒ True
163  ].
164
165lemma no_call_advance : ∀p : evaluation_params.
166∀s,nxt.∀st : state_pc p.
167no_call p (globals p) s →
168eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st.
169#p * // #f #args #dest #nxt #st *
170qed.
171
172lemma no_call_other : ∀p : evaluation_params.∀st,s.
173no_call p (globals p) s →
174joint_classify_seq … st s = cl_other.
175#p #st * // #f #args #dest *
176qed.
177
178lemma cond_call_other :
179  ∀p,globals.∀P : joint_step p globals → Prop.
180  (∀a,lbltrue.P (COND … a lbltrue)) →
181  (∀f,args,dest.P (CALL … f args dest)) →
182  (∀s.no_call ?? s → P s) →
183  ∀s.P s.
184#p #globals #P #H1 #H2 #H3 * // * /2 by / qed.
185
186lemma joint_classify_call : ∀p : evaluation_params.∀st.
187  joint_classify p st = Some ? cl_call →
188  ∃i_f,f',args,dest,next,bl,i',fd'.
189  fetch_statement … (ev_genv p) (pc … st) =
190    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
191  block_of_call … (ev_genv p) f' st = OK ? bl ∧
192  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
193#p #st
194whd in match joint_classify; normalize nodelta
195inversion (fetch_statement … (ev_genv p) (pc … st))
196[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
197* #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
198>m_return_bind normalize nodelta
199  [3: whd in match joint_classify_final; normalize nodelta
200    generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
201    normalize nodelta ]
202  #ABS destruct(ABS) ]
203@cond_call_other [ #a #lbl | #f' #args #dest | #s #s_no_call ] #nxt #fetch >m_return_bind
204normalize nodelta
205[ normalize in ⊢ (%→?); #ABS destruct(ABS)
206|3: whd in match joint_classify_step;
207  normalize nodelta >(no_call_other … s_no_call) #ABS destruct(ABS)
208]
209whd in match joint_classify_step; whd in match joint_classify_seq;
210normalize nodelta
211inversion (block_of_call ?????)
212[ #bl #block_of_c  >m_return_bind
213  inversion (fetch_function ???)
214  [ * #i' *
215    [ #fd' #fetch' #_
216      %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
217      % [ %{block_of_c} % ]
218      whd in match fetch_internal_function; normalize nodelta
219      >fetch' %
220    ]
221  ]
222]
223#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
224qed.
225
226definition joint_after_ret : ∀p:evaluation_params.
227  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝
228λp,s1,s2.
229match fetch_statement … (ev_genv p) (pc … s1) with
230[ OK x ⇒
231  match \snd x with
232  [ sequential s next ⇒
233    pc … s2 = succ_pc p (pc … s1) next
234  | _ ⇒ False (* never happens *)
235  ]
236| _ ⇒ False (* never happens *)
237].
238
239definition joint_call_ident : ∀p:evaluation_params.
240  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝
241(* this is a definition without a dummy ident :
242λp,st.
243match ?
244return λx.
245  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
246  match s with
247  [ sequential s next ⇒
248    match s with
249    [ step_seq s ⇒
250      match s with
251      [ CALL f' args dest ⇒
252        function_of_call … (ev_genv p) st f'
253      | _ ⇒ Error … [ ]
254      ]
255    | _ ⇒ Error … [ ]
256    ]
257  | _ ⇒ Error … [ ]
258  ] = x → ? with
259[ OK v ⇒ λ_.v
260| Error e ⇒ λABS.⊥
261] (refl …).
262@hide_prf
263elim (joint_classify_call … (pi2 … st))
264#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
265lapply ABS -ABS
266>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
267qed. *)
268(* with a dummy ident (which is never used as seen above in the commented script)
269   I think handling of the function is easier *)
270λp,st.
271let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
272match fetch_statement … (ev_genv p) (pc … st) with
273[ OK x ⇒
274  match \snd x with
275  [ sequential s next ⇒
276    match s with
277    [ step_seq s ⇒
278      match s with
279      [ CALL f' args dest ⇒
280        match
281          (! bl ← block_of_call … (ev_genv p) f' st;
282           fetch_internal_function … (ev_genv p) bl) with
283        [ OK i_f ⇒ \fst i_f
284        | _ ⇒ dummy
285        ]
286      | _ ⇒ dummy
287      ]
288    | _ ⇒ dummy
289    ]
290  | _ ⇒ dummy
291  ]
292| _ ⇒ dummy
293].
294
295definition joint_tailcall_ident : ∀p:evaluation_params.
296  (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝
297λp,st.
298let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
299match fetch_statement … (ev_genv p) (pc … st) with
300[ OK x ⇒
301  match \snd x with
302  [ final s ⇒
303    match s with
304    [ TAILCALL _ f' args ⇒
305      match
306        (! bl ← block_of_call … (ev_genv p) f' st;
307         fetch_internal_function … (ev_genv p) bl) with
308      [ OK i_f ⇒ \fst i_f
309      | _ ⇒ dummy
310      ]
311    | _ ⇒ dummy
312    ]
313  | _ ⇒ dummy
314  ]
315| _ ⇒ dummy
316].
317
318definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
319*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
320[ #EQ destruct % #H %
321| * #NEQ % #ABS destruct elim (NEQ ?) %
322]
323qed.
324
325(*
326let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
327  match c with
328  [ Value x ⇒ OK … x
329  | Interact o f ⇒
330    ! i ← env o ;
331    io_evaluate O I X env (f i)
332  | Wrong e ⇒ Error … e
333  ].
334*)
335
336definition cost_label_of_stmt :
337  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
338  λp,s.match s with
339  [ sequential s _ ⇒
340    match s with
341    [ step_seq s ⇒
342      match s with
343      [ COST_LABEL lbl ⇒ Some ? lbl
344      | _ ⇒ None ?
345      ]
346    | _ ⇒ None ?
347    ]
348  | _ ⇒ None ?
349  ].
350
351
352lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
353no_cost_label p (globals p) s →
354cost_label_of_stmt … (sequential … s nxt) = None ?.
355#p * // #lbl #next *
356qed.
357
358definition joint_abstract_status :
359 ∀p : evaluation_params.
360 abstract_status ≝
361 λp.
362 mk_abstract_status
363   (* as_status ≝ *) (state_pc p)
364   (* as_execute ≝ *)
365    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
366   (* as_pc ≝ *) pcDeq
367   (* as_pc_of ≝ *) (pc …)
368   (* as_classify ≝ *) (joint_classify p)
369   (* as_label_of_pc ≝ *)
370    (λpc.
371      match fetch_statement … (ev_genv p) pc with
372      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
373      | _ ⇒ None ?
374      ])
375   (* as_after_return ≝ *) (joint_after_ret p)
376   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) (exit p) s ≠ None ?)
377   (* as_call_ident ≝ *) (joint_call_ident p)
378   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
Note: See TracBrowser for help on using the repository browser.