source: src/joint/Traces.ma @ 2638

Last change on this file since 2638 was 2638, checked in by piccolo, 7 years ago

Back-end fixes for last Garnier's commit that removes the regions from
the blocks. Only part of the back-end has been fixed.

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