source: src/joint/Traces.ma @ 2946

Last change on this file since 2946 was 2946, checked in by tranquil, 7 years ago

main novelties:

  • there is an in-built stack_usage nat in joint states, at the base of the new division of RTL's semantics (with separate stacks, with separate stacks but with an artificial overflow error, with a unique stack)
  • a premain is added semantically to the global env, so initial cost label and main call and return are observed
  • proper initialization is now in LINToASM (to be sure, endianess should be checked ;-)

The update breaks proofs of back end atm. compiler.ma should be okay, but I have not had time to complete its compilation.

File size: 9.5 KB
Line 
1include "joint/semanticsUtils.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
43lemma lookup_remove_elim : ∀tag,A.∀P : option A → Prop.
44∀m,i,j.
45(i = j → P (None ?)) →
46(i ≠ j → P (lookup tag A m i)) →
47P (lookup tag A (remove tag A m j) i).
48#tag #A #P #m #i #j #H1 #H2
49@(eq_identifier_elim … i j) #H destruct
50[ >lookup_remove_hit @H1 % | >lookup_remove_miss try @H2 assumption ]
51qed.
52
53definition make_global : prog_params → evaluation_params
54
55λpars.
56let p ≝ prog pars in
57let spars ≝ prog_spars pars in
58let genv ≝ joint_globalenv spars p in
59let get_pc_lbl ≝ λid,lbl.
60  ! bl ← block_of_funct_id … spars genv id ;
61  pc_of_label … genv bl lbl in
62mk_evaluation_params
63  (prog_var_names … p)
64  spars
65  (mk_genv_gen ?? genv ? (stack_sizes pars) get_pc_lbl)
66 (* (prog_io pars) *).
67#s #H
68elim (find_symbol_exists … (λx.x) … p s ?)
69[ #bl #EQ %
70  whd in match genv; whd in match find_symbol; whd in match drop_fn; normalize nodelta
71  @lookup_add_elim #H
72  [2: @lookup_remove_elim [ #EQ >EQ in H; * #ABS cases (ABS ?) % ]
73    #_ change with (find_symbol ? (globalenv … (λx.x) p) s = ? → ?) >EQ ]
74  #ABS destruct(ABS) ]
75@Exists_append_r
76@(Exists_mp … H) //
77qed.
78
79coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
80≝ make_global on _p : prog_params to evaluation_params.
81
82definition make_initial_state :
83 ∀pars: prog_params.state_pc pars ≝
84λpars.let p ≝ prog pars in
85  let sem_globals : evaluation_params ≝ pars in
86  let ge ≝ ev_genv sem_globals in
87  (* this is going to change shortly: globals will not reside in globalenv anymore *)
88  let m0 ≝ \snd (globalenv_allocmem … (λx.x) p) in
89  let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in
90  let globals_size ≝ globals_stacksize … p in
91  (* stack pointer should start at 2^16 - |globals|, right?
92     first call to main shuold bring it to 2^16 - |globals| - |main stack|
93     Also, on words 2^16 - |globals| = - |globals| *)
94  let spp : xpointer ≝
95    «mk_pointer spb (mk_offset (bitvector_of_Z 16 (-globals_size))),
96     pi2 … spb» in
97(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
98  let main ≝ prog_main … p in
99  let st ≝ mk_state pars (Some ? (empty_framesT …)) empty_is (BBbit false) (empty_regsT … spp) m globals_size in
100  mk_state_pc ? (set_sp … spp st) init_pc (null_pc one).
101cases m0 in H; #m1 #m2 #m3 #H
102whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥
103@(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by Zlt_to_Zle_to_Zlt/
104qed.
105
106definition joint_classify_step :
107  ∀p : evaluation_params.joint_step p (globals … p) → status_class ≝
108  λp,stmt.
109  match stmt with
110  [ CALL f args dest ⇒ cl_call
111  | COND _ _ ⇒ cl_jump
112  | _ ⇒ cl_other
113  ].
114
115definition joint_classify_final :
116  ∀p : evaluation_params.joint_fin_step p → status_class ≝
117  λp,stmt.
118  match stmt with
119  [ GOTO _ ⇒ cl_other
120  | RETURN ⇒ cl_return
121  | TAILCALL _ f args ⇒ cl_tailcall
122  ].
123
124definition joint_classify :
125  ∀p : evaluation_params.state_pc p → status_class ≝
126  λp,st.
127  match fetch_statement … (ev_genv p) (pc … st) with
128  [ OK i_fn_s ⇒
129    match \snd i_fn_s with
130    [ sequential s _ ⇒ joint_classify_step p s
131    | final s ⇒ joint_classify_final p s
132    | FCOND _ _ _ _ ⇒ cl_jump
133    ]
134  | _ ⇒ cl_other
135  ].
136
137lemma joint_classify_call : ∀p : evaluation_params.∀st.
138  joint_classify p st = cl_call →
139  ∃i_f,f',args,dest,next.
140  fetch_statement … (ev_genv p) (pc … st) =
141    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉.
142#p #st
143whd in match joint_classify; normalize nodelta
144inversion (fetch_statement … (ev_genv p) (pc … st))
145[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
146* #i_f *
147[2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
148  normalize nodelta normalize in ⊢ (%→?); #ABS destruct
149]
150* [ #c | #f' #args #dest | #a #lbl | #s ] #nxt #fetch normalize nodelta
151normalize in ⊢ (%→?); #EQ destruct
152%[|%[|%[|%[|%[| %]]]]]
153qed.
154
155definition joint_after_ret : ∀p:evaluation_params.
156  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
157λp,s1,s2.
158match fetch_statement … (ev_genv p) (pc … s1) with
159[ OK x ⇒
160  match \snd x with
161  [ sequential s next ⇒
162    last_pop … s2 = pc … s1 ∧
163    pc … s2 = succ_pc p (pc … s1) next
164  | _ ⇒ False (* never happens *)
165  ]
166| _ ⇒ False (* never happens *)
167].
168
169definition joint_call_ident : ∀p:evaluation_params.
170  state_pc p → ident ≝
171(* this is a definition without a dummy ident :
172λp,st.
173match ?
174return λx.
175  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
176  match s with
177  [ sequential s next ⇒
178    match s with
179    [ CALL f' args dest ⇒ function_of_call … (ev_genv p) st f'
180    | _ ⇒ Error … [ ]
181    ]
182  | _ ⇒ Error … [ ]
183  ] = x → ? with
184[ OK v ⇒ λ_.v
185| Error e ⇒ λABS.⊥
186] (refl …).
187@hide_prf
188elim (joint_classify_call … (pi2 … st))
189#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
190lapply ABS -ABS
191>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
192qed. *)
193(* with a dummy ident (which is never used as seen above in the commented script)
194   I think handling of the function is easier *)
195λp,st.
196let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
197match fetch_statement … (ev_genv p) (pc … st) with
198[ OK x ⇒
199  match \snd x with
200  [ sequential s next ⇒
201    match s with
202    [ CALL f' args dest ⇒
203      match
204        (! bl ← block_of_call … (ev_genv p) f' st;
205         fetch_internal_function … (ev_genv p) bl) with
206      [ OK i_f ⇒ \fst i_f
207      | _ ⇒ dummy
208      ]
209    | _ ⇒ dummy
210    ]
211  | _ ⇒ dummy
212  ]
213| _ ⇒ dummy
214].
215
216definition joint_tailcall_ident : ∀p:evaluation_params.
217  state_pc p → ident ≝
218λp,st.
219let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
220match fetch_statement … (ev_genv p) (pc … st) with
221[ OK x ⇒
222  match \snd x with
223  [ final s ⇒
224    match s with
225    [ TAILCALL _ f' args ⇒
226      match
227        (! bl ← block_of_call … (ev_genv p) f' st;
228         fetch_internal_function … (ev_genv p) bl) with
229      [ OK i_f ⇒ \fst i_f
230      | _ ⇒ dummy
231      ]
232    | _ ⇒ dummy
233    ]
234  | _ ⇒ dummy
235  ]
236| _ ⇒ dummy
237].
238
239definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
240*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
241[ #EQ destruct % #H %
242| * #NEQ % #ABS destruct elim (NEQ ?) %
243]
244qed.
245
246(*
247let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
248  match c with
249  [ Value x ⇒ OK … x
250  | Interact o f ⇒
251    ! i ← env o ;
252    io_evaluate O I X env (f i)
253  | Wrong e ⇒ Error … e
254  ].
255*)
256
257definition cost_label_of_stmt :
258  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
259  λp,s.match s with
260  [ sequential s _ ⇒
261    match s with
262    [  COST_LABEL lbl ⇒ Some ? lbl
263    | _ ⇒ None ?
264    ]
265  | _ ⇒ None ?
266  ].
267
268definition joint_label_of_pc ≝
269  λp : evaluation_params.
270    (λpc.
271      match fetch_statement … (ev_genv p) pc with
272      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
273      | _ ⇒ None ?
274      ]).
275
276(* the prime is to render obsolete old definition of exit_pc, remove when all is corrected *)
277definition exit_pc' : program_counter ≝
278mk_program_counter «mk_block (-1), refl …» (p1 one).
279
280definition joint_final: ∀p: sem_params.∀globals.
281  genv p globals → state_pc p → option int ≝
282 λp,globals,ge,st.
283 if eq_program_counter (pc … st) exit_pc' then
284   let ret ≝ call_dest_for_main ?? p in
285   res_to_opt … (! vals ← read_result … ge ret st ;
286               Word_of_list_beval vals)
287 else None ?.
288
289definition joint_abstract_status :
290 ∀p : prog_params.
291 abstract_status ≝
292 λp.
293 mk_abstract_status
294   (* as_status ≝ *) (state_pc p)
295   (* as_execute ≝ *)
296    (λs1,s2.eval_state … (ev_genv p) s1 = return s2)
297   (* (* as_init ≝ *) (make_initial_state p) *)
298   (* as_pc ≝ *) pcDeq
299   (* as_pc_of ≝ *) (pc …)
300   (* as_classify ≝ *) (joint_classify p)
301   (* as_label_of_pc ≝ *) (joint_label_of_pc p)
302   (* as_after_return ≝ *) (joint_after_ret p)
303   (* as_result ≝ *) (joint_final p  (globals ?) (ev_genv p))
304   (* as_call_ident ≝ *) (λst.joint_call_ident p st)
305   (* as_tailcall_ident ≝ *) (λst.joint_tailcall_ident p st).
306
307(* alternative definition with integrated prog_params constructor *)
308definition joint_status :
309 ∀p : sem_params.
310 joint_program p → (ident → option ℕ) → abstract_status ≝
311λp,prog,stacksizes.joint_abstract_status (mk_prog_params p prog stacksizes).
Note: See TracBrowser for help on using the repository browser.