source: src/joint/Traces.ma @ 3007

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

Fixed cond and seq case in StatusSimulationHelper?

Added cost case in StatusSimulationHelper?

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