source: src/joint/semantics_paolo.ma @ 1908

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

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

File size: 28.9 KB
Line 
1include "basics/lists/list.ma".
2include "joint/BEGlobalenvs.ma".
3include "common/IO.ma".
4include "common/SmallstepExec.ma".
5include "joint/Joint_paolo.ma".
6include "ASM/I8051bis.ma".
7
8(* CSC: external functions never fail (??) and always return something of the
9   size of one register, both in the frontend and in the backend.
10   Is this reasonable??? In OCaml it always return a list, but in the frontend
11   only the head is kept (or Undef if the list is empty) ??? *)
12
13definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p).
14definition cpointer ≝ Σp.ptype p = Code.
15definition xpointer ≝ Σp.ptype p = XData.
16unification hint 0 ≔ ⊢ cpointer ≡ Sig pointer (λp.ptype p = Code).
17unification hint 0 ≔ ⊢ xpointer ≡ Sig pointer (λp.ptype p = XData).
18
19record sem_state_params : Type[1] ≝
20 { framesT: Type[0]
21 ; empty_framesT: framesT
22 ; regsT : Type[0]
23 ; empty_regsT: xpointer → regsT (* Stack pointer *)
24 }.
25 
26record state (semp: sem_state_params): Type[0] ≝
27 { st_frms: framesT semp
28 ; sp: xpointer
29 ; isp: xpointer
30 ; carry: beval
31 ; regs: regsT semp
32 ; m: bemem
33 }.
34
35record state_pc (semp : sem_state_params) : Type[0] ≝
36  { st_no_pc :> state semp
37  ; pc : cpointer
38  }.
39
40definition set_m: ∀p. bemem → state p → state p ≝
41 λp,m,st. mk_state p (st_frms ?…st) (sp … st) (isp … st) (carry … st) (regs … st) m.
42
43definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
44 λp,regs,st. mk_state p (st_frms … st) (sp … st) (isp … st) (carry … st) regs (m … st).
45
46definition set_sp: ∀p. ? → state p → state p ≝
47 λp,sp,st. mk_state … (st_frms … st) sp (isp … st) (carry … st) (regs … st) (m … st).
48
49definition set_isp: ∀p. ? → state p → state p ≝
50 λp,isp,st. mk_state … (st_frms … st) (sp … st) isp (carry … st) (regs … st) (m … st).
51
52definition set_carry: ∀p. beval → state p → state p ≝
53 λp,carry,st. mk_state … (st_frms … st) (sp … st) (isp … st) carry (regs … st) (m … st).
54
55definition set_pc: ∀p. ? → state_pc p → state_pc p ≝
56 λp,pc,st. mk_state_pc … (st_no_pc … st) pc.
57
58definition set_no_pc: ∀p. ? → state_pc p → state_pc p ≝
59 λp,s,st. mk_state_pc … s (pc … st).
60
61definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
62 λp,frms,st. mk_state … frms (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
63
64axiom BadProgramCounter : String.
65(* this can replace graph_fetch function and lin_fetch_function *)
66definition fetch_function:
67 ∀pars : params.
68 ∀globals.
69  genv globals pars →
70  cpointer →
71  res (joint_internal_function … pars) ≝
72 λpars,globals,ge,p.
73  let b ≝ pblock p in
74  do def ← opt_to_res ? [MSG BadProgramCounter] (find_funct_ptr … ge b) ;
75  match def with
76  [ Internal def' ⇒ OK … def'
77  | External _ ⇒ Error … [MSG BadProgramCounter]].
78
79inductive step_flow (p : params) (globals : list ident) : Type[0] ≝
80  | Redirect : label → step_flow p globals (* used for goto-like flow alteration *)
81  | Init     : Z → joint_internal_function globals p → call_args p → call_dest p → step_flow p globals (* call a function with given id, then proceed *)
82  | Proceed  : step_flow p globals. (* go to implicit successor *)
83
84inductive stmt_flow (p : params) (globals : list ident) : Type[0] ≝
85  | SRedirect : label → stmt_flow p globals
86  | SProceed : succ p → stmt_flow p globals
87  | SInit     : Z → joint_internal_function globals p → call_args p → call_dest p → succ p → stmt_flow p globals
88  | STailInit : Z → joint_internal_function globals p → call_args p → stmt_flow p globals
89  | SEnd  : stmt_flow p globals. (* end flow *)
90
91
92record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
93  { st_pars :> sem_state_params
94  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
95  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
96  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
97  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
98  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
99  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
100  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
101  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
102  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
103  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
104  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
105  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
106  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
107  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
108  ; fetch_ra: state st_pars → res ((state st_pars) × cpointer)
109
110  ; allocate_local : localsT uns_pars → regsT st_pars → regsT st_pars
111  (* Paolo: save_frame separated from call_setup to factorize tailcall code *)
112  ; save_frame: cpointer → call_dest uns_pars → state st_pars → framesT st_pars
113   (*CSC: setup_call returns a res only because we can call a function with the wrong number and
114     type of arguments. To be fixed using a dependent type *)
115  ; setup_call : nat → paramsT … uns_pars → call_args uns_pars →
116      state st_pars → res (state st_pars)
117  ; fetch_external_args: external_function → state st_pars →
118      res (list val)
119  ; set_result: list val → state st_pars → res (state st_pars)
120  ; call_args_for_main: call_args uns_pars
121  ; call_dest_for_main: call_dest uns_pars
122 }.
123
124
125definition helper_def_retrieve :
126  ∀X : ? → ? → Type[0].
127  (∀up.∀p:more_sem_unserialized_params up. regsT p → X up p → res beval) →
128  ∀up.∀p : more_sem_unserialized_params up.state p → X up p → res beval ≝
129    λX,f,up,p,st.f ? p (regs … st).
130
131definition helper_def_store :
132  ∀X : ? → ? → Type[0].
133  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
134  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
135  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return set_regs … r st.
136
137definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
138definition acca_store ≝ helper_def_store ? acca_store_.
139definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
140definition accb_store ≝ helper_def_store ? accb_store_.
141definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
142definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
143definition dpl_store ≝ helper_def_store ? dpl_store_.
144definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
145definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
146definition dph_store ≝ helper_def_store ? dph_store_.
147definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
148definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
149definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
150definition pair_reg_move : ?→?→?→?→?  ≝
151  λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
152    ! r ← pair_reg_move_ ? p (regs ? st) pm;
153    return set_regs ? r st.
154
155 
156axiom BadPointer : String.
157 
158(* this is preamble to all calls (including tail ones). The optional argument in
159   input tells the function whether it has to save the frame for internal
160   calls.
161   the first element of the triple is the entry point of the function if
162   it is an internal one, or false in case of an external one.
163   The actual update of the pc is left to later, as it depends on
164   serialization and on whether the call is a tail one. *)
165definition eval_call_block:
166 ∀globals.∀p : params.∀p':more_sem_unserialized_params p.
167  genv globals p → state p' → block → call_args p → call_dest p →
168    IO io_out io_in ((step_flow p globals)×trace×(state p')) ≝
169 λglobals,p,p',ge,st,b,args,dest.
170  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
171    match fd with
172    [ Internal fn ⇒
173      return 〈Init … (block_id b) fn args dest, E0, st〉
174    | External fn ⇒
175      ! params ← fetch_external_args … p' fn st : IO ???;
176      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
177      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
178      (* CSC: XXX bug here; I think I should split it into Byte-long
179         components; instead I am making a singleton out of it. To be
180         fixed once we fully implement external functions. *)
181      let vs ≝ [mk_val ? evres] in
182      ! st ← set_result … p' vs st : IO ???;
183      return 〈Proceed ??, Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
184      ].
185
186axiom FailedStore: String.
187
188definition push: ∀p.state p → beval → res (state p) ≝
189 λp,st,v.
190  let isp' ≝ isp ? st in
191  do m ← opt_to_res ? (msg FailedStore) (bestorev (m … st) isp' v);
192  let isp'' ≝ shift_pointer … isp' [[false;false;false;false;false;false;false;true]] in
193  return set_m … m (set_isp … isp'' st).
194  normalize elim (isp p st) //
195qed.
196
197definition pop: ∀p. state p → res ((state p ) × beval) ≝
198 λp,st.
199  let isp' ≝ isp ? st in
200  let isp'' ≝ neg_shift_pointer ? isp' [[false;false;false;false;false;false;false;true]] in
201  let ist ≝ set_isp … isp'' st in
202  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp'');
203  OK ? 〈ist,v〉.
204  normalize elim (isp p st) //
205qed.
206 
207definition save_ra : ∀p. state p → cpointer → res (state p) ≝
208 λp,st,l.
209  let 〈addrl,addrh〉 ≝ address_of_code_pointer l in
210  ! st' ← push … st addrl;
211  push … st' addrh.
212
213definition load_ra : ∀p.state p → res ((state p) × cpointer) ≝
214 λp,st.
215  do 〈st',addrh〉 ← pop … st;
216  do 〈st'',addrl〉 ← pop … st';
217  do pr ← code_pointer_of_address 〈addrh, addrl〉;
218  return 〈st'', pr〉.
219
220definition flow_no_seq : ∀p,g.stmt_flow p g → Prop ≝ λp,g,flow.
221  match flow with
222  [ SProceed _ ⇒ False
223  | SInit _ _ _ _ _ ⇒ False
224  | _ ⇒ True
225  ].
226
227(* parameters that need full params to have type of functions,
228   but are still independent of serialization *)
229record more_sem_genv_params (pp : params) : Type[1] ≝
230  { msu_pars :> more_sem_unserialized_params pp
231  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
232  (* change of pc must be left to *_flow execution *)
233  ; exec_extended: ∀globals.genv globals pp → ext_step pp →
234      state msu_pars →
235      IO io_out io_in ((step_flow pp globals)× trace × (state msu_pars))
236  ; exec_fin_extended: ∀globals.genv globals pp → ext_fin_stmt pp →
237      state msu_pars →
238      IO io_out io_in ((Σs.flow_no_seq pp globals s)× trace × (state msu_pars))
239  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
240  }.
241
242(* parameters that are defined by serialization *)
243record more_sem_params (pp : params) : Type[1] ≝
244  { msg_pars :> more_sem_genv_params pp
245  ; offset_of_point : code_point pp → offset
246  ; point_of_offset : offset → option (code_point pp)
247  ; point_of_offset_of_point : ∀pt.point_of_offset (offset_of_point pt) = Some ? pt
248  ; offset_of_point_of_offset : ∀o.opt_All ? (eq ? o) (! pt ← point_of_offset o ; return offset_of_point pt)
249  }.
250
251definition pointer_of_point : ∀p.more_sem_params p →
252  cpointer→ code_point p → cpointer ≝
253  λp,msp,ptr,pt.
254    mk_pointer Code (pblock ptr) ? (offset_of_point p msp pt).
255[ elim ptr #ptr' #EQ <EQ @pok
256| %] qed.
257
258axiom BadOffsetForCodePoint : String.
259
260definition point_of_pointer :
261  ∀p.more_sem_params p → cpointer → res (code_point p) ≝
262  λp,msp,ptr.opt_to_res … (msg BadOffsetForCodePoint)
263    (point_of_offset p msp (poff ptr)).
264
265lemma point_of_pointer_of_point :
266  ∀p,msp.∀ptr : cpointer.∀pt.point_of_pointer p msp (pointer_of_point p msp ptr pt) = return pt.
267#p #msp #ptr #pt normalize
268>point_of_offset_of_point %
269qed.
270
271lemma pointer_of_point_block :
272  ∀p,msp,ptr,pt.pblock (pointer_of_point p msp ptr pt) = pblock ptr.
273/ by refl/
274qed.
275
276lemma pointer_of_point_uses_block :
277  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.pblock ptr1 = pblock ptr2 → pointer_of_point p msp ptr1 pt = pointer_of_point p msp ptr2 pt.
278#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
279        ** #ty2 #bl2 #H2 #o2 #EQ2
280#pt #EQ3 destruct normalize //
281qed.
282
283lemma pointer_of_point_of_pointer :
284  ∀p,msp.∀ptr1,ptr2 : cpointer.∀pt.
285    pblock ptr1 = pblock ptr2 → point_of_pointer p msp ptr1 = OK … pt →
286    pointer_of_point p msp ptr2 pt = ptr1.
287#p #msp ** #ty1 #bl1 #H1 #o1 #EQ1
288        ** #ty2 #bl2 #H2 #o2 #EQ2 #pt #EQ
289destruct
290lapply (offset_of_point_of_offset p msp o1)
291normalize
292elim (point_of_offset ???) normalize [* #ABS destruct(ABS)]
293#pt' #EQ #EQ' destruct %
294qed.
295
296
297axiom ProgramCounterOutOfCode : String.
298axiom PointNotFound : String.
299axiom LabelNotFound : String.
300
301definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals.
302  genv globals p → cpointer → res (joint_statement p globals) ≝
303  λp,msp,globals,ge,ptr.
304  ! pt ← point_of_pointer ? msp ptr ;
305  ! fn ← fetch_function … ge ptr ;
306  opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt).
307
308definition pointer_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals.
309  genv globals p → cpointer → label → res cpointer ≝
310  λp,msp,globals,ge,ptr,lbl.
311  ! fn ← fetch_function … ge ptr ;
312  ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl]
313            (point_of_label … (joint_if_code … fn) lbl) ;
314  return pointer_of_point ? msp ptr pt.
315
316definition succ_pc : ∀p : params.∀ msp : more_sem_params p.
317  cpointer → succ p → res cpointer ≝
318  λp,msp,ptr,nxt.
319  ! curr ← point_of_pointer p msp ptr ;
320  return pointer_of_point p msp ptr (point_of_succ p curr nxt). 
321
322record sem_params : Type[1] ≝
323  { spp :> params
324  ; more_sem_pars :> more_sem_params spp
325  }.
326
327(* definition address_of_label: ∀globals. ∀p:sem_params.
328  genv globals p → pointer → label → res address ≝
329 λglobals,p,ge,ptr,l.
330  do newptr ← pointer_of_label … p ? ge … ptr l ;
331  OK … (address_of_code_pointer newptr). *)
332
333definition goto: ∀globals. ∀p:sem_params.
334  genv globals p → label → state_pc p → res (state_pc p) ≝
335 λglobals,p,ge,l,st.
336  ! newpc ← pointer_of_label ? p … ge (pc … st) l ;
337  return set_pc … newpc st.
338
339(*
340definition empty_state: ∀p. more_sem_params p → state p ≝
341 mk_state … (empty_framesT …)
342*)
343
344definition next : ∀p : sem_params.succ p → state_pc p → res (state_pc p) ≝
345 λp,l,st.
346 ! nw ← succ_pc ? p … (pc ? st) l ;
347 return set_pc … nw st.
348
349axiom MissingSymbol : String.
350axiom FailedLoad : String.
351axiom BadFunction : String.
352axiom SuccessorNotProvided : String.
353
354(* the optional point must be given only for calls *)
355definition eval_step :
356 ∀globals.∀p:sem_params. genv globals p → state p →
357  joint_step p globals →
358  IO io_out io_in ((step_flow p globals)×trace×(state p)) ≝
359 λglobals,p,ge,st,seq.
360  match seq with
361  [ extension c ⇒
362    exec_extended … ge c st
363  | COST_LABEL cl ⇒
364    return 〈Proceed ??, Echarge cl, st〉
365  | COMMENT c ⇒
366    return 〈Proceed ??, E0, st〉
367  | LOAD dst addrl addrh ⇒
368    ! vaddrh ← dph_arg_retrieve … st addrh ;
369    ! vaddrl ← dpl_arg_retrieve … st addrl;
370    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
371    ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
372    ! st ← acca_store p … dst v st ;
373    return 〈Proceed ??, E0, st〉
374  | STORE addrl addrh src ⇒
375    ! vaddrh ← dph_arg_retrieve … st addrh;
376    ! vaddrl ← dpl_arg_retrieve … st addrl;
377    ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
378    ! v ← acca_arg_retrieve … st src;
379    ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
380    return 〈Proceed ??, E0, set_m … m' st〉
381  | COND src ltrue ⇒
382    ! v ← acca_retrieve … st src;
383    ! b ← bool_of_beval v;
384    if b then
385      return 〈Redirect ?? ltrue, E0, st〉
386    else
387      return 〈Proceed ??, E0, st〉
388  | ADDRESS ident prf ldest hdest ⇒
389    let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
390    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
391    ! st' ← dpl_store … ldest laddr st;
392    ! st'' ← dph_store … hdest haddr st';
393    return 〈Proceed ??, E0, st''〉
394  | OP1 op dacc_a sacc_a ⇒
395    ! v ← acca_retrieve … st sacc_a;
396    ! v ← Byte_of_val v;
397    let v' ≝ BVByte (op1 eval op v) in
398    ! st ← acca_store … dacc_a v' st;
399    return 〈Proceed ??, E0, st〉
400  | OP2 op dacc_a sacc_a src ⇒
401    ! v1 ← acca_arg_retrieve … st sacc_a;
402    ! v1 ← Byte_of_val v1;
403    ! v2 ← snd_arg_retrieve … st src;
404    ! v2 ← Byte_of_val v2;
405    ! carry ← bool_of_beval (carry … st);
406      let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
407      let v' ≝ BVByte v' in
408      let carry ≝ beval_of_bool carry in
409    ! st' ← acca_store … dacc_a v' st;
410      let st'' ≝ set_carry … carry st' in
411    return 〈Proceed ??, E0, st''〉
412  | CLEAR_CARRY ⇒
413    let st' ≝ set_carry … BVfalse st in
414    return 〈Proceed ??, E0, st'〉
415  | SET_CARRY ⇒
416    let st' ≝ set_carry … BVtrue st in
417    return 〈Proceed ??, E0, st'〉
418  | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
419    ! v1 ← acca_arg_retrieve … st sacc_a_reg;
420    ! v1 ← Byte_of_val v1;
421    ! v2 ← accb_arg_retrieve … st sacc_b_reg;
422    ! v2 ← Byte_of_val v2;
423    let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
424    let v1' ≝ BVByte v1' in
425    let v2' ≝ BVByte v2' in
426    ! st' ← acca_store … dacc_a_reg v1' st;
427    ! st'' ← accb_store … dacc_b_reg v2' st';
428    return 〈Proceed ??, E0, st''〉
429  | POP dst ⇒
430    ! 〈st',v〉 ← pop p st;
431    ! st'' ← acca_store p p dst v st';
432    return 〈Proceed ??, E0, st''〉
433  | PUSH src ⇒
434    ! v ← acca_arg_retrieve … st src;
435    ! st ← push … st v;
436    return 〈Proceed ??, E0, st〉
437  | MOVE dst_src ⇒
438    ! st ← pair_reg_move … st dst_src ;
439    return 〈Proceed ??, E0, st〉
440  | CALL_ID id args dest ⇒
441    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
442    eval_call_block … ge st b args dest
443  ].
444  [ cases addr //
445  | (* TODO: to prove *)
446    elim daemon
447  ] qed.
448
449definition eval_step_flow :
450 ∀globals.∀p:sem_params.step_flow p globals →
451  succ p → stmt_flow p globals ≝
452 λglobals,p,cmd,nxt.
453 match cmd with
454 [ Redirect l ⇒ SRedirect … l
455 | Init id fn args dest ⇒ SInit … id fn args dest nxt
456 | Proceed ⇒ SProceed … nxt
457 ].
458
459definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
460  state p → joint_statement … p globals →
461  IO io_out io_in ((stmt_flow p globals) × trace × (state p)) ≝
462 λglobals,p,ge,st,s.
463  match s with
464    [ GOTO l ⇒ return 〈SRedirect … l, E0, (st : state ?)〉
465    | RETURN ⇒ return 〈SEnd ??, E0, (st : state ?) 〉
466    | sequential seq l ⇒
467      ! 〈flow, tr, st〉 ← eval_step … ge st seq ;
468      return 〈eval_step_flow … flow l, tr, st〉
469    | extension_fin c ⇒
470      ! 〈flow, tr, st〉 ← exec_fin_extended … ge c st ;
471      return 〈pi1 … flow, tr, st〉
472    ].
473
474definition eval_statement_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
475  state p → (Σs : joint_statement … p globals.no_seq … s) →
476  IO io_out io_in ((Σf.flow_no_seq p globals f) × trace × (state p)) ≝
477 λglobals,p,ge,st,s_sig.
478  match s_sig with
479  [ mk_Sig s s_prf ⇒
480    match s return λx.no_seq p globals x → ? with
481    [ GOTO l ⇒ λ_.return 〈«SRedirect … l,?», E0, (st : state ?)〉
482    | RETURN ⇒ λ_.return 〈«SEnd ??,?», E0, (st : state ?) 〉
483    | sequential seq l ⇒ Ⓧ
484    | extension_fin c ⇒ λ_.exec_fin_extended … ge c st
485    ] s_prf
486  ]. % qed.
487
488let rec rel_io O I A B (P : A → B → Prop) (v1 : IO O I A)
489  (v2 : IO O I B) on v1 : Prop ≝
490  match v1 with
491  [ Value x ⇒
492    match v2 with
493    [ Value y ⇒
494      P x y
495    | _ ⇒ False
496    ]
497  | Wrong _ ⇒
498    match v2 with
499    [ Wrong _ ⇒ True
500    | _ ⇒ False
501    ]
502  | Interact o1 f1 ⇒
503    match v2 with
504    [ Interact o2 f2 ⇒
505      ∃prf:o1 = o2.∀i.rel_io … P (f1 i) (f2 ?)
506    | _ ⇒ False
507    ]
508  ]. <prf @i qed.
509
510definition IORel ≝ λO,I.
511  mk_MonadRel (IOMonad O I) (IOMonad O I)
512    (rel_io O I) ???.
513[//
514|#X #Y #Z #W #relin #relout #m elim m
515  [ #o #f #IH * [#o' #f' | #v | #e] * #EQ destruct(EQ) #G
516    #f1 #f2 #G' whd %{(refl …)} #i
517    @(IH … (G i) f1 f2 G')
518  | #v * [#o #f * | #v' | #e *]
519    #Pvv' #f #g #H normalize @H @Pvv'
520  | #e1 * [#o #f * | #v' *| #e2] * #f #g #_ %
521  ]
522| #X #Y #P #Q #H #m elim m [#o #f #IH | #v | #e] *
523  [1,4,7: #o' #f' [2,3: *]
524    normalize * #prf destruct(prf) normalize #G
525    % [%] normalize #i @IH @G
526  |2,5,8: #v' [1,3: *]
527    @H
528  |*: #e' [1,2: *] //
529  ]
530]
531qed.
532
533lemma IORel_refl : ∀O,I,X,rel.reflexive X rel →
534  reflexive ? (m_rel ?? (IORel O I) ?? rel).
535#O #I #X #rel #H #m elim m
536[ #o #f #IH whd %[%] #i normalize @IH
537| #v @H
538| #e %
539]
540qed.
541
542lemma IORel_transitive : ∀O,I,X,Y,Z,rel1,rel2,rel3.
543  (∀x : X.∀y : Y.∀z : Z.rel1 x y → rel2 y z → rel3 x z) →
544  ∀m,n,o.
545  m_rel ?? (IORel O I) … rel1 m n →
546  m_rel ?? (IORel O I) … rel2 n o →
547  m_rel ?? (IORel O I) … rel3 m o.
548#O #I #X #Y #Z #rel1 #rel2 #rel3 #H #m elim m
549[ #o #f #IH * [#o' #f' * [#o'' #f'' | #v #_ * | #e #_ * ] | #v #x * | #e #x * ]
550  normalize * #EQ #H1 * #EQ' #H2 destruct %[%] normalize #i @(IH ? (f' i)) //
551| #v * [#o #f #x * | #v' * [#o #f #_ * | #v'' |#e #_ *] | #e #x *]
552  @H
553| #e * [#o #f #x * | #v #x * | #e' * [#o #f #_ * | #v #_ * | #e'']] //
554]
555qed.
556
557lemma mr_bind' : ∀M1,M2.∀Rel : MonadRel M1 M2.
558  ∀X,Y,Z,W,relin,relout,m,n.m_rel ?? Rel X Y relin m n →
559  ∀f,g.(∀x,y.relin x y → m_rel ?? Rel Z W relout (f x) (g y)) →
560                  m_rel ?? Rel ?? relout (! x ← m ; f x) (! y ← n ; g y).
561#M1 #M2 #Rel #X #Y #Z #W #relin #relout #m #n #H #f #g #G
562@(mr_bind … H) @G qed.
563
564lemma m_bind_ext_eq' : ∀M : MonadProps.∀X,Y.∀m1,m2 : monad M X.∀f1,f2 : X → monad M Y.
565  m1 = m2 → (∀x.f1 x = f2 x) → ! x ← m1 ; f1 x = ! x ← m2 ; f2 x.
566#M #X #Y #m1 #m2 #f1 #f2 #EQ >EQ @m_bind_ext_eq
567qed.
568
569lemma eval_statement_no_seq_to_normal : ∀globals,p,ge,st,s1,s2.
570  pi1 ?? s1 = s2 →
571  m_rel ?? (IORel ??) ??
572    (λx,y.pi1 ?? (\fst (\fst x)) = \fst (\fst y) ∧
573      \snd (\fst x) = \snd (\fst y) ∧ \snd x = \snd y)
574    (eval_statement_no_seq globals p ge st s1)
575    (eval_statement globals p ge st s2).
576#globals #p #ge #st * * [#s #n | #lbl || #c ]*
577#s2 #EQ destruct(EQ)
578whd in match eval_statement;
579whd in match eval_statement_no_seq;
580normalize nodelta
581[1,2: @(mr_return … (IORel ??)) /3 by pair_destruct, conj/]
582<(m_bind_return … (exec_fin_extended ??????)) in ⊢ (???????%?);
583@(mr_bind … (IORel ??)) [@eq | @IORel_refl // |
584#x #y #EQ destruct(EQ) cases y ** #a #prf #b #c whd /3 by pair_destruct, conj/
585qed.
586
587definition do_call : ∀globals: list ident.∀p:sem_params. genv globals p →
588  state p → Z → joint_internal_function globals p → call_args p →
589  res (state_pc p) ≝
590  λglobals,p,ge,st,id,fn,args.
591    ! st' ← setup_call … (joint_if_stacksize … fn) (joint_if_params … fn)
592              args st ;
593    let regs ≝ foldr ?? (allocate_local p p) (regs … st) (joint_if_locals … fn) in
594    let l' ≝ joint_if_entry … fn in
595    let st' ≝ set_regs p regs st in
596    let pointer_in_fn ≝ mk_pointer Code (mk_block Code id) ? (mk_offset 0) in
597    let pc ≝ pointer_of_point ? p … pointer_in_fn l' in
598    return mk_state_pc ? st' pc. % qed.
599
600definition eval_stmt_flow : ∀globals: list ident.∀p:sem_params. genv globals p →
601  state_pc p → stmt_flow p globals → IO io_out io_in (state_pc p) ≝
602  λglobals,p,ge,st,flow.
603  match flow with
604  [ SRedirect l ⇒ goto … ge l st
605  | SProceed nxt ⇒ next ? nxt st
606  | SInit id fn args dest nxt ⇒
607    ! ra ← succ_pc ? p … (pc … st) nxt ;
608    let st' ≝ set_no_pc … (set_frms … (save_frame … ra dest st) st) st in
609    do_call ?? ge st' id fn args
610  | STailInit id fn args ⇒
611    do_call … ge st id fn args
612  | SEnd ⇒
613    ! 〈st,ra〉 ← fetch_ra … st ;
614    ! st' ← pop_frame … ge st;
615    return mk_state_pc ? st' ra
616  ].
617
618definition eval_stmt_flow_no_seq : ∀globals: list ident.∀p:sem_params. genv globals p →
619  state p → Z → (Σf:stmt_flow p globals.flow_no_seq … f) →
620    IO io_out io_in (state_pc p) ≝
621  λglobals,p,ge,st,id,flow_sig.
622  match flow_sig with
623  [ mk_Sig flow prf ⇒
624    match flow return λx.flow_no_seq p globals x → ? with
625    [ SRedirect l ⇒ λ_.
626      ! newpc ← pointer_of_label ? p … ge
627        (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) l ;
628      return mk_state_pc … st newpc
629    | STailInit id fn args ⇒ λ_.
630      do_call … ge st id fn args
631    | SEnd ⇒ λ_.
632      ! 〈st,ra〉 ← fetch_ra … st ;
633      ! st' ← pop_frame … ge st;
634      return mk_state_pc ? st' ra
635    | _ ⇒ Ⓧ
636    ] prf
637  ]. % qed.
638
639lemma pointer_of_label_eq_with_id :
640∀g.∀p : sem_params.∀ge : genv g p.∀ptr1,ptr2 : cpointer.∀lbl.
641  block_id (pblock ptr1) = block_id (pblock ptr2) →
642  pointer_of_label ? p ? ge ptr1 lbl = pointer_of_label ? p ? ge ptr2 lbl.
643#g #p #ge
644** #ty1 * #r1 #id1 #H1 inversion H1 [#s || #s] #id #EQ1 #EQ2 #EQ3 #o #EQ4 destruct
645** #ty2 * #r2 #id2 #H2 inversion H2
646[1,3: #s] #id2' #EQ5 #EQ6 #EQ7 #o2 #EQ8 #lbl #EQ9 destruct %
647qed.
648
649
650lemma eval_stmt_flow_no_seq_to_normal : ∀g.∀p : sem_params.∀ge.∀st : state_pc p.
651  ∀id.∀s1 : Σs.flow_no_seq p g s.∀s2.
652  pi1 … s1 = s2 → block_id (pblock (pc … st)) = id →
653    (eval_stmt_flow_no_seq g p ge st id s1) =
654    (eval_stmt_flow g p ge st s2).
655#g#p#ge#st#id'
656**[#lbl|#nxt*|#id#fn#args#dest#n*|#id#fn#args]*
657#s2 #EQ #EQ' destruct(EQ)
658whd in match eval_stmt_flow_no_seq; normalize nodelta
659whd in match eval_stmt_flow; normalize nodelta
660[2,3: %]
661whd in match goto; normalize nodelta
662whd in match set_pc; normalize nodelta
663>pointer_of_label_eq_with_id [% | >EQ' % |]
664qed.
665
666definition eval_state : ∀globals: list ident.∀p:sem_params. genv globals p →
667  state_pc p → IO io_out io_in (trace × (state_pc p)) ≝
668  λglobals,p,ge,st.
669  ! s ← fetch_statement ? p … ge (pc … st) : IO ???;
670  ! 〈flow, tr, st_npc〉 ← eval_statement … ge st s;
671  let st ≝ set_no_pc … st_npc st in
672  ! st ← eval_stmt_flow … ge st flow;
673  return 〈tr, st〉.
674
675definition is_final: ∀globals:list ident. ∀p: sem_params.
676  genv globals p → cpointer → state_pc p → option int ≝
677 λglobals,p,ge,exit,st.res_to_opt ? (
678  do s ← fetch_statement ? p … ge (pc … st);
679  match s with
680   [ RETURN ⇒
681      do 〈st,ra〉 ← fetch_ra … st;
682      if eq_pointer ra exit then
683       do vals ← read_result … ge st ;
684       Word_of_list_beval vals
685      else
686       Error ? [ ]
687   | _ ⇒ Error ? [ ]]).
688 
689record evaluation_parameters : Type[1] ≝
690 { globals: list ident
691 ; sparams:> sem_params
692 ; exit: cpointer
693 ; genv2: genv globals sparams
694 }.
695
696definition joint_exec: trans_system io_out io_in ≝
697  mk_trans_system … evaluation_parameters (λG. state_pc G)
698   (λG.is_final (globals G) G (genv2 G) (exit G))
699   (λG.eval_state (globals G) G (genv2 G)).
700
701definition make_global :
702 ∀pars: sem_params.
703  joint_program pars → evaluation_parameters
704
705 λpars.
706 (* Invariant: a -1 block is unused in common/Globalenvs *)
707 let b ≝ mk_block Code (-1) in
708 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
709  (λp. mk_evaluation_parameters
710    (prog_var_names … p)
711    (mk_sem_params … pars)
712    ptr
713    (globalenv Genv … p)
714  ).
715% qed.
716
717axiom ExternalMain: String.
718
719definition make_initial_state :
720 ∀pars: sem_params.
721 ∀p: joint_program … pars. res (state_pc pars) ≝
722λpars,p.
723  let sem_globals ≝ make_global pars p in
724  let ge ≝ genv2 sem_globals in
725  let m ≝ init_mem Genv … p in
726  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
727  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
728  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
729  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
730  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
731  let main ≝ prog_main … p in
732  let st0 ≝ mk_state pars (empty_framesT …) spp ispp BVfalse (empty_regsT … spp) m in
733  (* use exit sem_globals as ra and call_dest_for_main as dest *)
734  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
735  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
736  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ?? ge main) ;
737  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge main_block) ;
738  match main_fd with
739  [ Internal fn ⇒
740    do_call ?? ge st_pc0 (block_id main_block) fn (call_args_for_main … pars)
741  | External _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
742  ]. [5: cases ispb * |6: cases spb * ] (* without try it fails! *) try //
743qed.
744
745definition joint_fullexec :
746 ∀pars:sem_params.fullexec io_out io_in ≝
747 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
Note: See TracBrowser for help on using the repository browser.