source: src/joint/Traces.ma @ 2457

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

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File size: 7.6 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: cpointer
8 ; ev_genv: genv sparams globals
9(* ; io_env : state sparams → ∀o:io_out.res (io_in o) *)
10 }.
11
12axiom is_internal_function_of_program :
13  ∀p:params.joint_program p → ident → Prop.
14
15axiom is_internal_function_of_program_ok :
16  ∀p.∀prog:joint_program p.∀i.is_internal_function ?? (globalenv_noinit ? prog) i →
17  is_internal_function_of_program p prog i.
18
19record prog_params : Type[1] ≝
20 { prog_spars : sem_params
21 ; prog : joint_program prog_spars
22 ; stack_sizes : (Σi.is_internal_function_of_program prog_spars prog i) → ℕ
23(* ; prog_io : state prog_spars → ∀o.res (io_in o) *)
24 }.
25
26definition make_global : prog_params → evaluation_params
27
28λpars.
29(* Invariant: a -1 block is unused in common/Globalenvs *)
30let b ≝ mk_block Code (-1) in
31let ptr ≝ mk_pointer b (mk_offset (bv_zero …)) in
32let p ≝ prog pars in
33mk_evaluation_params
34  (prog_var_names … p)
35  (prog_spars pars)
36  «ptr, refl …»
37  (mk_genv_gen ?? (globalenv_noinit ? p) ? (λi.stack_sizes pars «i, ?»))
38 (* (prog_io pars) *).
39[ @is_internal_function_of_program_ok @(pi2 … i)
40| (* TODO or TOBEFOUND *)
41  cases daemon
42]
43qed.
44
45coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params
46≝ make_global on _p : prog_params to evaluation_params.
47
48axiom BadMain : String.
49
50definition make_initial_state :
51 ∀pars: prog_params.res (state_pc pars) ≝
52λpars.let p ≝ prog pars in
53  let sem_globals : evaluation_params ≝ pars in
54  let ge ≝ ev_genv sem_globals in
55  let m ≝ alloc_mem … p in
56  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
57  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
58  let dummy_pc ≝ mk_pointer (mk_block Code (-1)) (mk_offset (bv_zero …)) in
59  let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in
60(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
61  let main ≝ prog_main … p in
62  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
63  let st0' ≝ set_sp … spp st0 in
64  (* use exit sem_globals as ra and call_dest_for_main as dest *)
65  ! st0'' ← save_frame ?? sem_globals (exit sem_globals) (call_dest_for_main … pars) st0 ;
66  let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in
67  ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … ge main) ;
68  match ? return λx.description_of_function … main = x → ? with
69  [ Internal fn ⇒ λprf.
70    let main : Σi : ident.is_internal_function ???? ≝ «main, ?» in
71    ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;
72    ! pc' ← eval_internal_call_pc … ge main ;
73    return mk_state_pc … st' pc'
74  | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
75  ] (refl …).
76  [ %
77  | @(description_of_internal_function … prf)
78  | cases spb normalize //
79  ]
80qed.
81
82definition joint_classify :
83  ∀p : evaluation_params.state_pc p → status_class ≝
84  λp,st.
85  match fetch_statement ? p … (ev_genv p) (pc … st) with
86  [ OK f_s ⇒
87    let 〈f, s〉 ≝ f_s in
88    match s with
89    [ sequential s _ ⇒
90      match s with
91      [ step_seq s ⇒
92        match s with
93        [ CALL f' args dest ⇒
94          match function_of_call ?? (ev_genv p) st f' with
95          [ OK fn ⇒
96            match description_of_function … fn with
97            [ Internal _ ⇒ cl_call
98            | External _ ⇒ cl_other
99            ]
100          | Error _ ⇒ cl_other
101          ]
102        | _ ⇒ cl_other
103        ]
104      | COND _ _ ⇒ cl_jump
105      ]
106    | final s ⇒
107      match s with
108      [ GOTO _ ⇒ cl_other
109      | RETURN ⇒ cl_return
110      | TAILCALL _ _ _ ⇒ cl_other (* this needs tailcalls implemented in structured traces *)
111      ]
112    ]
113  | Error _ ⇒ cl_other
114  ].
115
116lemma joint_classify_call : ∀p : evaluation_params.∀st.
117  joint_classify p st = cl_call →
118  ∃f,f',args,dest,next,fn,fd.
119  fetch_statement ? p … (ev_genv p) (pc … st) =
120    OK ? 〈f, sequential … (CALL … f' args dest) next〉 ∧
121  function_of_call … (ev_genv p) st f' = OK ? fn ∧
122  description_of_function … (ev_genv p) fn = Internal … fd.
123#p #st
124whd in match joint_classify; normalize nodelta
125lapply (refl … (fetch_statement ? p … (ev_genv p) (pc … st)))
126elim (fetch_statement ?????) in ⊢ (???%→%);
127[ * #f * [| * [ #lbl || #b #f #args ]]
128  [ * [| #a #lbl #next ]
129    [ *
130      [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b'
131      | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg
132      | #ext ] #next
133      [ normalize nodelta
134        lapply (refl … (function_of_call … (ev_genv p) st f'))
135        elim (function_of_call ?????) in ⊢ (???%→%);
136        [ #fn normalize nodelta
137          lapply (refl … (description_of_function … (ev_genv p) fn))
138          elim (description_of_function ????) in ⊢ (???%→%); #fd
139          #EQfd
140        | #e
141        ] #EQfn
142      ]
143    ]
144  ]
145| #e
146] #EQfetch
147[|*: #ABS normalize in ABS; destruct(ABS) ]
148normalize nodelta #_
149%{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} /3 by conj/
150qed.
151
152definition joint_call_ident : ∀p:evaluation_params.
153  (Σs : state_pc p.joint_classify p s = cl_call) → ident ≝
154λp,st.
155match ?
156return λx.
157  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
158  match s with
159  [ sequential s next ⇒
160    match s with
161    [ step_seq s ⇒
162      match s with
163      [ CALL f' args dest ⇒
164        function_of_call … (ev_genv p) st f'
165      | _ ⇒ Error … [ ]
166      ]
167    | _ ⇒ Error … [ ]
168    ]
169  | _ ⇒ Error … [ ]
170  ] = x → ? with
171[ OK v ⇒ λ_.v
172| Error e ⇒ λABS.⊥
173] (refl …).
174@hide_prf
175elim (joint_classify_call … (pi2 … st))
176#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
177lapply ABS -ABS
178>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
179qed.
180
181definition cpointerDeq ≝ mk_DeqSet cpointer eq_pointer ?.
182*#p1 #EQ1 * #p2 #EQ2 @eq_pointer_elim
183[ #EQ destruct % #H %
184| * #NEQ % #ABS destruct elim (NEQ ?) %
185]
186qed.
187
188(*
189let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
190  match c with
191  [ Value x ⇒ OK … x
192  | Interact o f ⇒
193    ! i ← env o ;
194    io_evaluate O I X env (f i)
195  | Wrong e ⇒ Error … e
196  ].
197*)
198
199definition cost_label_of_stmt :
200  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
201  λp,s.match s with
202  [ sequential s _ ⇒
203    match s with
204    [ step_seq s ⇒
205      match s with
206      [ COST_LABEL lbl ⇒ Some ? lbl
207      | _ ⇒ None ?
208      ]
209    | _ ⇒ None ?
210    ]
211  | _ ⇒ None ?
212  ].
213
214definition joint_abstract_status :
215 ∀p : evaluation_params.
216 abstract_status ≝
217 λp.
218 mk_abstract_status
219   (* as_status ≝ *) (state_pc p)
220   (* as_execute ≝ *)
221    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … p (ev_genv p) s1) = return s2)
222   (* as_pc ≝ *) cpointerDeq
223   (* as_pc_of ≝ *) (pc …)
224   (* as_classify ≝ *) (joint_classify p)
225   (* as_label_of_pc ≝ *)
226    (λpc.
227      match fetch_statement ? p … (ev_genv p) pc with
228      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
229      | _ ⇒ None ?
230      ])
231   (* as_after_return ≝ *)
232    (λs1,s2.
233      (* Paolo: considering sequential calls, tailcalls must be classified as cl_return *)
234      ∃fn,stp,nxt.fetch_statement ? p … (ev_genv p) (pc … s1) = return 〈fn,sequential ?? stp nxt〉 ∧
235      succ_pc p p (pc … s1) nxt = return pc … s2)
236   (* as_final ≝ *) (λs.is_final (globals ?) p (ev_genv p) (exit p) s ≠ None ?)
237   (* as_call_ident ≝ *) (joint_call_ident p).
Note: See TracBrowser for help on using the repository browser.