source: src/joint/Traces.ma @ 2473

Last change on this file since 2473 was 2473, checked in by tranquil, 8 years ago

put some generic stuff we need in the back end in extraGlobalenvs (with some axioms that are
in the commented section of Globalenvs)
linearise now has a full spec

File size: 8.8 KB
Line 
1include "joint/semantics.ma".
2include "common/StructuredTraces.ma".
3
4record evaluation_params : Type[1] ≝
5 { globals: list ident
6 ; sparams:> sem_params
7 ; exit: program_counter
8 ; ev_genv: genv sparams globals
9(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
10 }.
11 
12
13
14record prog_params : Type[1] ≝
15 { prog_spars : sem_params
16 ; prog : joint_program prog_spars
17 ; stack_sizes : (Σi.is_internal_function_of_program ?? prog i) → ℕ
18(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
19 }.
20
21lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l.
22#A #B #f #P #l elim l -l [*]
23#hd #tl #IH *
24[ #Phd %1{Phd}
25| #Ptl %2{(IH Ptl)}
26]
27qed.
28
29lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x.
30#A #P #l elim l -l [*] #hd #tl #IH *
31[ #Phd %{hd} %{Phd} %1 %
32| #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1}
33]
34qed.
35
36lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l.
37#A #P #l elim l -l [ #x *] #hd #tl #IH #x *
38[ #EQ >EQ #H %1{H}
39| #Intl #Px %2{(IH … Intl Px)}
40]
41qed.
42
43definition make_global : prog_params → evaluation_params
44
45λpars.
46(* Invariant: a -1 block is unused in common/Globalenvs *)
47let b ≝ mk_block Code (-1) in
48let ptr ≝ mk_program_counter «b, refl …» one in
49let p ≝ prog pars in
50mk_evaluation_params
51  (prog_var_names … p)
52  (prog_spars pars)
53  ptr
54  (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»))
55 (* (prog_io pars) *).
56[ @(is_internal_function_of_program_ok … (pi2 … i))
57| #s #H
58  lapply (map_Exists … H) -H #H
59  elim (Exists_In … H) -H ** #id #r #v * #id_in #EQ destruct(EQ)
60  elim (find_symbol_exists ??????? id_in)
61  [ #bl #EQ >EQ % #ABS destruct(ABS)|]
62]
63qed.
64
65coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
66≝ make_global on _p : prog_params to evaluation_params.
67
68axiom BadMain : String.
69
70definition make_initial_state :
71 ∀pars: prog_params.res (state_pc pars) ≝
72λpars.let p ≝ prog pars in
73  let sem_globals : evaluation_params ≝ pars in
74  let ge ≝ ev_genv sem_globals in
75  let m ≝ alloc_mem … p in
76  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
77  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
78  let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in
79  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
80(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
81  let main ≝ prog_main … p in
82  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
83  let st0' ≝ set_sp … spp st0 in
84  (* use exit sem_globals as ra and call_dest_for_main as dest *)
85  ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
86  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
87  ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
88  match ? return λx.description_of_function … main = x → ? with
89  [ Internal fn ⇒ λprf.
90    let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in
91    ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
92    let pc' ≝ eval_internal_call_pc … ge main in
93    return mk_state_pc … st' pc'
94  | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
95  ] (refl …).
96  [ @(description_of_internal_function … prf)
97  | cases spb normalize //
98  ]
99qed.
100
101definition joint_classify :
102  ∀p : evaluation_params.state_pc p → status_class ≝
103  λp,st.
104  match fetch_statement ? p … (ev_genv p) (pc … st) with
105  [ OK f_s ⇒
106    let 〈f, s〉 ≝ f_s in
107    match s with
108    [ sequential s _ ⇒
109      match s with
110      [ step_seq s ⇒
111        match s with
112        [ CALL f' args dest ⇒
113          match function_of_call ?? (ev_genv p) st f' with
114          [ OK fn ⇒
115            match description_of_function … fn with
116            [ Internal _ ⇒ cl_call
117            | External _ ⇒ cl_other
118            ]
119          | Error _ ⇒ cl_other
120          ]
121        | _ ⇒ cl_other
122        ]
123      | COND _ _ ⇒ cl_jump
124      ]
125    | final s ⇒
126      match s with
127      [ GOTO _ ⇒ cl_other
128      | RETURN ⇒ cl_return
129      | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
130      ]
131    ]
132  | Error _ ⇒ cl_other
133  ].
134
135lemma joint_classify_call : ∀p : evaluation_params.∀st.
136  joint_classify p st = cl_call →
137  ∃f,f',args,dest,next,fn,fd.
138  fetch_statement ? p … (ev_genv p) (pc … st) =
139    OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧
140  function_of_call … (ev_genv p) st f' = OK ? fn ∧
141  description_of_function … (ev_genv p) fn = Internal … fd.
142#p #st
143whd in match joint_classify; normalize nodelta
144lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st)))
145elim (fetch_statement ?????) in ⊢ (???%→%);
146[ * #f * [| * [ #lbl || #b #f #args ]]
147  [ * [| #a #lbl #next ]
148    [ *
149      [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b'
150      | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
151      | #ext ] #next
152      [ normalize nodelta
153        lapply (refl … (function_of_call … (ev_genv p) st f'))
154        elim (function_of_call ?????) in ⊢ (???%→%);
155        [ #fn normalize nodelta
156          lapply (refl … (description_of_function … (ev_genv p) fn))
157          elim (description_of_function ?? fn) in ⊢ (???%→%); #fd
158          #EQfd
159        | #e
160        ] #EQfn
161      ]
162    ]
163  ]
164| #e
165] #EQfetch
166[|*: #ABS normalize in ABS; destruct(ABS) ]
167normalize nodelta #_
168%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/
169qed.
170
171definition joint_after_ret : ∀p:evaluation_params.
172  (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝
173λp,s1,s2.
174match fetch_statement ? p … (ev_genv p) (pc … s1) with
175[ OK x ⇒
176  match \snd x with
177  [ sequential s next ⇒
178    pc … s2 = succ_pc p p (pc … s1) next
179  | _ ⇒ False (* never happens *)
180  ]
181| _ ⇒ False (* never happens *)
182].
183
184definition joint_call_ident : ∀p:evaluation_params.
185  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
186(* this is a definition without a dummy ident :
187λp,st.
188match ?
189return λx.
190  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
191  match s with
192  [ sequential s next ⇒
193    match s with
194    [ step_seq s ⇒
195      match s with
196      [ CALL f' args dest ⇒
197        function_of_call … (ev_genv p) st f'
198      | _ ⇒ Error … [ ]
199      ]
200    | _ ⇒ Error … [ ]
201    ]
202  | _ ⇒ Error … [ ]
203  ] = x → ? with
204[ OK v ⇒ λ_.v
205| Error e ⇒ λABS.⊥
206] (refl …).
207@hide_prf
208elim (joint_classify_call … (pi2 … st))
209#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
210lapply ABS -ABS
211>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
212qed. *)
213(* with a dummy ident (which is never used as seen above in the commented script)
214   I think handling of the function is easier *)
215λp,st.
216let dummy : ident ≝ an_identifier ? one in
217match fetch_statement ? p … (ev_genv p) (pc … st) with
218[ OK x ⇒
219  match \snd x with
220  [ sequential s next ⇒
221    match s with
222    [ step_seq s ⇒
223      match s with
224      [ CALL f' args dest ⇒
225        match function_of_call … (ev_genv p) st f' with
226        [ OK f ⇒ f
227        | _ ⇒ dummy
228        ]
229      | _ ⇒ dummy
230      ]
231    | _ ⇒ dummy
232    ]
233  | _ ⇒ dummy
234  ]
235| _ ⇒ dummy
236].
237
238definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
239*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
240[ #EQ destruct % #H %
241| * #NEQ % #ABS destruct elim (NEQ ?) %
242]
243qed.
244
245(*
246let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
247  match c with
248  [ Value x ⇒ OK … x
249  | Interact o f ⇒
250    ! i ← env o ;
251    io_evaluate O I X env (f i)
252  | Wrong e ⇒ Error … e
253  ].
254*)
255
256definition cost_label_of_stmt :
257  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
258  λp,s.match s with
259  [ sequential s _ ⇒
260    match s with
261    [ step_seq s ⇒
262      match s with
263      [ COST_LABEL lbl ⇒ Some ? lbl
264      | _ ⇒ None ?
265      ]
266    | _ ⇒ None ?
267    ]
268  | _ ⇒ None ?
269  ].
270
271definition joint_abstract_status :
272 ∀p : evaluation_params.
273 abstract_status ≝
274 λp.
275 mk_abstract_status
276   (* as_status ≝ *) (state_pc p)
277   (* as_execute ≝ *)
278    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
279   (* as_pc ≝ *) pcDeq
280   (* as_pc_of ≝ *) (pc …)
281   (* as_classify ≝ *) (joint_classify p)
282   (* as_label_of_pc ≝ *)
283    (λpc.
284      match fetch_statement ? p … (ev_genv p) pc with
285      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
286      | _ ⇒ None ?
287      ])
288   (* as_after_return ≝ *) (joint_after_ret p)
289   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
290   (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracBrowser for help on using the repository browser.