source: src/joint/Traces.ma @ 2470

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

completely separated program counters from code pointers in joint languages: the advantage is program counters with an unbounded offset in Pos

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