source: src/joint/Traces.ma @ 2601

Last change on this file since 2601 was 2601, checked in by sacerdot, 7 years ago

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 10.1 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
69axiom BadMain : String.
70
71definition make_initial_state :
72 ∀pars: prog_params.res (state_pc pars) ≝
73λpars.let p ≝ prog pars in
74  let sem_globals : evaluation_params ≝ pars in
75  let ge ≝ ev_genv sem_globals in
76  let m ≝ alloc_mem … p in
77  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
78  let spp : xpointer ≝
79    «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)),
80     pi2 … spb» in
81(*  let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *)
82  let main ≝ prog_main … p in
83  let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in
84  (* use exit_pc as ra and call_dest_for_main as dest *)
85  let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in
86  ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) (prog_main … p) st0' ;
87  let st0'' ≝ set_no_pc … st0_no_pc st0' in
88  ! bl ← block_of_call … ge (inl … main) st0'';
89  ! 〈i, fn〉 ← fetch_function … ge bl ;
90  match fn with
91  [ Internal ifn ⇒
92    ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ;
93    let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in
94    return mk_state_pc … st' pc' exit_pc
95  | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *)
96  ].
97
98definition joint_classify_step :
99  ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
100  λp,st,stmt.
101  match stmt with
102  [ step_seq _ ⇒ cl_other
103  | CALL f args dest ⇒
104    match (! bl ← block_of_call … (ev_genv p) f st ;
105            fetch_function … (ev_genv p) bl) with
106    [ OK id_fn ⇒
107      match \snd id_fn with
108      [ Internal _ ⇒ cl_call
109      | External _ ⇒ cl_other
110      ]
111    | Error _ ⇒ cl_other
112    ]
113  | COND _ _ ⇒ cl_jump
114  ].
115
116definition joint_classify_final :
117  ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝
118  λp,st,stmt.
119  match stmt with
120  [ GOTO _ ⇒ cl_other
121  | RETURN ⇒ cl_return
122  | TAILCALL _ f args ⇒
123    match (! bl ← block_of_call … (ev_genv p) f st ;
124            fetch_function … (ev_genv p) bl) with
125    [ OK id_fn ⇒
126      match \snd id_fn with
127      [ Internal _ ⇒ cl_tailcall
128      | External _ ⇒ cl_return
129      ]
130    | Error _ ⇒ cl_other
131    ]
132  ].
133
134definition joint_classify :
135  ∀p : evaluation_params.state_pc p → option status_class ≝
136  λp,st.
137  ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
138  match s with
139  [ sequential s _ ⇒ Some ? (joint_classify_step p st s)
140  | final s ⇒ Some ? (joint_classify_final p st s)
141  | FCOND _ _ _ _ ⇒ Some ? cl_jump
142  ].
143
144definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝
145  λp,g,s.match s with
146  [ COST_LABEL _ ⇒ False
147  | _ ⇒ True
148  ].
149
150lemma joint_classify_call : ∀p : evaluation_params.∀st.
151  joint_classify p st = Some ? cl_call →
152  ∃i_f,f',args,dest,next,bl,i',fd'.
153  fetch_statement … (ev_genv p) (pc … st) =
154    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
155  block_of_call … (ev_genv p) f' st = OK ? bl ∧
156  fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
157#p #st
158whd in match joint_classify; normalize nodelta
159inversion (fetch_statement … (ev_genv p) (pc … st))
160[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
161* #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
162>m_return_bind normalize nodelta
163  [3: whd in match joint_classify_final; normalize nodelta
164    generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
165    normalize nodelta ]
166  #ABS destruct(ABS) ]
167* [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
168normalize nodelta
169[2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
170whd in match joint_classify_step;
171normalize nodelta
172inversion (block_of_call ?????)
173[ #bl #block_of_c  >m_return_bind
174  inversion (fetch_function ???)
175  [ * #i' *
176    [ #fd' #fetch' #_
177      %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
178      % [ %{block_of_c} % ]
179      whd in match fetch_internal_function; normalize nodelta
180      >fetch' %
181    ]
182  ]
183]
184#x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
185qed.
186
187definition joint_after_ret : ∀p:evaluation_params.
188  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝
189λp,s1,s2.
190match fetch_statement … (ev_genv p) (pc … s1) with
191[ OK x ⇒
192  match \snd x with
193  [ sequential s next ⇒
194    last_pop … s2 = pc … s1 ∧
195    pc … s2 = succ_pc p (pc … s1) next
196  | _ ⇒ False (* never happens *)
197  ]
198| _ ⇒ False (* never happens *)
199].
200
201definition joint_call_ident : ∀p:evaluation_params.
202  (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝
203(* this is a definition without a dummy ident :
204λp,st.
205match ?
206return λx.
207  !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ;
208  match s with
209  [ sequential s next ⇒
210    match s with
211    [ step_seq s ⇒
212      match s with
213      [ CALL f' args dest ⇒
214        function_of_call … (ev_genv p) st f'
215      | _ ⇒ Error … [ ]
216      ]
217    | _ ⇒ Error … [ ]
218    ]
219  | _ ⇒ Error … [ ]
220  ] = x → ? with
221[ OK v ⇒ λ_.v
222| Error e ⇒ λABS.⊥
223] (refl …).
224@hide_prf
225elim (joint_classify_call … (pi2 … st))
226#f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3
227lapply ABS -ABS
228>EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS)
229qed. *)
230(* with a dummy ident (which is never used as seen above in the commented script)
231   I think handling of the function is easier *)
232λp,st.
233let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
234match fetch_statement … (ev_genv p) (pc … st) with
235[ OK x ⇒
236  match \snd x with
237  [ sequential s next ⇒
238    match s with
239    [ step_seq s ⇒
240      match s with
241      [ CALL f' args dest ⇒
242        match
243          (! bl ← block_of_call … (ev_genv p) f' st;
244           fetch_internal_function … (ev_genv p) bl) with
245        [ OK i_f ⇒ \fst i_f
246        | _ ⇒ dummy
247        ]
248      | _ ⇒ dummy
249      ]
250    | _ ⇒ dummy
251    ]
252  | _ ⇒ dummy
253  ]
254| _ ⇒ dummy
255].
256
257definition joint_tailcall_ident : ∀p:evaluation_params.
258  (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝
259λp,st.
260let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *)
261match fetch_statement … (ev_genv p) (pc … st) with
262[ OK x ⇒
263  match \snd x with
264  [ final s ⇒
265    match s with
266    [ TAILCALL _ f' args ⇒
267      match
268        (! bl ← block_of_call … (ev_genv p) f' st;
269         fetch_internal_function … (ev_genv p) bl) with
270      [ OK i_f ⇒ \fst i_f
271      | _ ⇒ dummy
272      ]
273    | _ ⇒ dummy
274    ]
275  | _ ⇒ dummy
276  ]
277| _ ⇒ dummy
278].
279
280definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?.
281*#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim
282[ #EQ destruct % #H %
283| * #NEQ % #ABS destruct elim (NEQ ?) %
284]
285qed.
286
287(*
288let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝
289  match c with
290  [ Value x ⇒ OK … x
291  | Interact o f ⇒
292    ! i ← env o ;
293    io_evaluate O I X env (f i)
294  | Wrong e ⇒ Error … e
295  ].
296*)
297
298definition cost_label_of_stmt :
299  ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝
300  λp,s.match s with
301  [ sequential s _ ⇒
302    match s with
303    [ step_seq s ⇒
304      match s with
305      [ COST_LABEL lbl ⇒ Some ? lbl
306      | _ ⇒ None ?
307      ]
308    | _ ⇒ None ?
309    ]
310  | _ ⇒ None ?
311  ].
312
313
314lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt.
315no_cost_label p (globals p) s →
316cost_label_of_stmt … (sequential … s nxt) = None ?.
317#p * // #lbl #next *
318qed.
319
320definition joint_abstract_status :
321 ∀p : evaluation_params.
322 abstract_status ≝
323 λp.
324 mk_abstract_status
325   (* as_status ≝ *) (state_pc p)
326   (* as_execute ≝ *)
327    (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2)
328   (* as_pc ≝ *) pcDeq
329   (* as_pc_of ≝ *) (pc …)
330   (* as_classify ≝ *) (joint_classify p)
331   (* as_label_of_pc ≝ *)
332    (λpc.
333      match fetch_statement … (ev_genv p) pc with
334      [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt)
335      | _ ⇒ None ?
336      ])
337   (* as_after_return ≝ *) (joint_after_ret p)
338   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
339   (* as_call_ident ≝ *) (joint_call_ident p)
340   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
Note: See TracBrowser for help on using the repository browser.