source: src/joint/Traces.ma @ 2952

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