source: src/joint/Traces.ma @ 2886

Last change on this file since 2886 was 2824, checked in by tranquil, 7 years ago
  • moved sum on lists notation to extranat
  • used sum on lists to define portion of stack occupied by globals
  • corrected probable bug in joint semantics, where initial state would not move stack pointer past globals before setting up main
File size: 9.1 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
11record prog_params : Type[1] ≝
12 { prog_spars : sem_params
13 ; prog : joint_program prog_spars
14 ; stack_sizes : ident → option ℕ
15(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
16 }.
17
18lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l.
19#A #B #f #P #l elim l -l [*]
20#hd #tl #IH *
21[ #Phd %1{Phd}
22| #Ptl %2{(IH Ptl)}
23]
24qed.
25
26lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x.
27#A #P #l elim l -l [*] #hd #tl #IH *
28[ #Phd %{hd} %{Phd} %1 %
29| #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1}
30]
31qed.
32
33lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l.
34#A #P #l elim l -l [ #x *] #hd #tl #IH #x *
35[ #EQ >EQ #H %1{H}
36| #Intl #Px %2{(IH … Intl Px)}
37]
38qed.
39
40lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l.
41#A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed.
42
43definition make_global : prog_params → evaluation_params
44
45λpars.
46let p ≝ prog pars in
47let spars ≝ prog_spars pars in
48let genv ≝ globalenv_noinit ? p in
49let get_pc_lbl ≝ λid,lbl.
50  ! bl ← block_of_funct_id … spars genv id ;
51  pc_of_label … genv bl lbl in
52mk_evaluation_params
53  (prog_var_names … p)
54  spars
55  (mk_genv_gen ?? genv ? (stack_sizes pars) get_pc_lbl)
56 (* (prog_io pars) *).
57#s #H
58elim (find_symbol_exists … p s ?)
59[ #bl #EQ >EQ % #ABS destruct(ABS)|*:]
60@Exists_append_r
61@(Exists_mp … H) //
62qed.
63
64coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
65≝ make_global on _p : prog_params to evaluation_params.
66
67definition make_initial_state :
68 ∀pars: prog_params.res (state_pc pars) ≝
69λpars.let p ≝ prog pars in
70  let sem_globals : evaluation_params ≝ pars in
71  let ge ≝ ev_genv sem_globals in
72  let m0 ≝ alloc_mem … p in
73  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
74  let globals_size ≝ globals_stacksize … p in
75  (* stack pointer should start at 2^16 - |globals|, right?
76     first call to main shuold bring it to 2^16 - |globals| - |main stack|
77     Also, on words 2^16 - |globals| = - |globals| *)
78  let spp : xpointer ≝
79    «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-globals_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 (Some ? (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) 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 ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
99@(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by Zlt_to_Zle_to_Zlt/
100qed.
101
102definition joint_classify_step :
103  ∀p : evaluation_params.joint_step p (globals … p) → status_class ≝
104  λp,stmt.
105  match stmt with
106  [ CALL f args dest ⇒ cl_call
107  | COND _ _ ⇒ cl_jump
108  | _ ⇒ cl_other
109  ].
110
111definition joint_classify_final :
112  ∀p : evaluation_params.joint_fin_step p → status_class ≝
113  λp,stmt.
114  match stmt with
115  [ GOTO _ ⇒ cl_other
116  | RETURN ⇒ cl_return
117  | TAILCALL _ f args ⇒ cl_tailcall
118  ].
119
120definition joint_classify :
121  ∀p : evaluation_params.state_pc p → status_class ≝
122  λp,st.
123  match fetch_statement … (ev_genv p) (pc … st) with
124  [ OK i_fn_s ⇒
125    match \snd i_fn_s with
126    [ sequential s _ ⇒ joint_classify_step p s
127    | final s ⇒ joint_classify_final p s
128    | FCOND _ _ _ _ ⇒ cl_jump
129    ]
130  | _ ⇒ cl_other
131  ].
132
133lemma joint_classify_call : ∀p : evaluation_params.∀st.
134  joint_classify p st = cl_call →
135  ∃i_f,f',args,dest,next.
136  fetch_statement … (ev_genv p) (pc … st) =
137    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉.
138#p #st
139whd in match joint_classify; normalize nodelta
140inversion (fetch_statement … (ev_genv p) (pc … st))
141[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
142* #i_f *
143[2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
144  normalize nodelta normalize in ⊢ (%→?); #ABS destruct
145]
146* [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch normalize nodelta
147normalize in ⊢ (%→?); #EQ destruct
148%[|%[|%[|%[|%[| %]]]]]
149qed.
150
151definition joint_after_ret : ∀p:evaluation_params.
152  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
153λp,s1,s2.
154match fetch_statement … (ev_genv p) (pc … s1) with
155[ OK x ⇒
156  match \snd x with
157  [ sequential s next ⇒
158    last_pop … s2 = pc … s1 ∧
159    pc … s2 = succ_pc p (pc … s1) next
160  | _ ⇒ False (* never happens *)
161  ]
162| _ ⇒ False (* never happens *)
163].
164
165definition joint_call_ident : ∀p:evaluation_params.
166  state_pc p → ident ≝
167(* this is a definition without a dummy ident :
168λp,st.
169match ?
170return λx.
171  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
172  match s with
173  [ sequential s next ⇒
174    match s with
175    [ step_seq s ⇒
176      match s with
177      [ CALL f' args dest ⇒
178        function_of_call … (ev_genv p) st f'
179      | _ ⇒ Error … [ ]
180      ]
181    | _ ⇒ Error … [ ]
182    ]
183  | _ ⇒ Error … [ ]
184  ] = x → ? with
185[ OK v ⇒ λ_.v
186| Error e ⇒ λABS.⊥
187] (refl …).
188@hide_prf
189elim (joint_classify_call … (pi2 … st))
190#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
191lapply ABS -ABS
192>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
193qed. *)
194(* with a dummy ident (which is never used as seen above in the commented script)
195   I think handling of the function is easier *)
196λp,st.
197let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
198match fetch_statement … (ev_genv p) (pc … st) with
199[ OK x ⇒
200  match \snd x with
201  [ sequential s next ⇒
202    match s with
203    [ step_seq s ⇒
204      match s with
205      [ CALL f' args dest ⇒
206        match
207          (! bl ← block_of_call … (ev_genv p) f' st;
208           fetch_internal_function … (ev_genv p) bl) with
209        [ OK i_f ⇒ \fst i_f
210        | _ ⇒ dummy
211        ]
212      | _ ⇒ dummy
213      ]
214    | _ ⇒ dummy
215    ]
216  | _ ⇒ dummy
217  ]
218| _ ⇒ dummy
219].
220
221definition joint_tailcall_ident : ∀p:evaluation_params.
222  state_pc p → ident ≝
223λp,st.
224let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
225match fetch_statement … (ev_genv p) (pc … st) with
226[ OK x ⇒
227  match \snd x with
228  [ final s ⇒
229    match s with
230    [ TAILCALL _ f' args ⇒
231      match
232        (! bl ← block_of_call … (ev_genv p) f' st;
233         fetch_internal_function … (ev_genv p) bl) with
234      [ OK i_f ⇒ \fst i_f
235      | _ ⇒ dummy
236      ]
237    | _ ⇒ dummy
238    ]
239  | _ ⇒ dummy
240  ]
241| _ ⇒ dummy
242].
243
244definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
245*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
246[ #EQ destruct % #H %
247| * #NEQ % #ABS destruct elim (NEQ ?) %
248]
249qed.
250
251(*
252let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
253  match c with
254  [ Value x ⇒ OK … x
255  | Interact o f ⇒
256    ! i ← env o ;
257    io_evaluate O I X env (f i)
258  | Wrong e ⇒ Error … e
259  ].
260*)
261
262definition cost_label_of_stmt :
263  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
264  λp,s.match s with
265  [ sequential s _ ⇒
266    match s with
267    [  COST_LABEL lbl ⇒ Some ? lbl
268    | _ ⇒ None ?
269    ]
270  | _ ⇒ None ?
271  ].
272
273definition joint_label_of_pc ≝
274  λp : evaluation_params.
275    (λpc.
276      match fetch_statement … (ev_genv p) pc with
277      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
278      | _ ⇒ None ?
279      ]).
280
281definition joint_abstract_status :
282 ∀p : prog_params.
283 abstract_status ≝
284 λp.
285 mk_abstract_status
286   (* as_status ≝ *) (state_pc p)
287   (* as_execute ≝ *)
288    (λs1,s2.eval_state … (ev_genv p) s1 = return s2)
289   (* (* as_init ≝ *) (make_initial_state p) *)
290   (* as_pc ≝ *) pcDeq
291   (* as_pc_of ≝ *) (pc …)
292   (* as_classify ≝ *) (joint_classify p)
293   (* as_label_of_pc ≝ *) (joint_label_of_pc p)
294   (* as_after_return ≝ *) (joint_after_ret p)
295   (* as_result ≝ *) (is_final p  (globals ?) (ev_genv p) exit_pc)
296   (* as_call_ident ≝ *) (λst.joint_call_ident p st)
297   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).
298
299(* alternative definition with integrated prog_params constructor *)
300definition joint_status :
301 ∀p : sem_params.
302 joint_program p → (ident → option ℕ) → abstract_status ≝
303λp,prog,stacksizes.joint_abstract_status (mk_prog_params p prog stacksizes).
Note: See TracBrowser for help on using the repository browser.