source: src/joint/Traces.ma @ 2760

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

many things are still broken, but there is a partial backtrack on Structured traces's execute

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