source: src/joint/semantics_paolo.ma @ 1640

Last change on this file since 1640 was 1640, checked in by tranquil, 8 years ago
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File size: 18.1 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).
14
15record sem_state_params : Type[1] ≝
16 { regsT : Type[0]
17 ; framesT: Type[0]
18 ; empty_framesT: framesT
19 ; empty_regsT: address → regsT (* Stack pointer *)
20 }.
21 
22record state (semp: sem_state_params): Type[0] ≝
23 { st_frms: framesT semp
24 ; pc: address
25 ; sp: pointer
26 ; isp: pointer
27 ; carry: beval
28 ; regs: regsT semp
29 ; m: bemem
30 }.
31 
32definition set_m: ∀p. bemem → state p → state p ≝
33 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) m.
34
35definition set_regs: ∀p:sem_state_params. regsT p → state p → state p ≝
36 λp,regs,st. mk_state p (st_frms … st) (pc … st) (sp … st) (isp … st) (carry … st) regs (m … st).
37
38definition set_sp: ∀p. pointer → state p → state p ≝
39 λp,sp,st. mk_state … (st_frms … st) (pc … st) sp (isp … st) (carry … st) (regs … st) (m … st).
40
41definition set_isp: ∀p. pointer → state p → state p ≝
42 λp,isp,st. mk_state … (st_frms … st) (pc … st) (sp … st) isp (carry … st) (regs … st) (m … st).
43
44definition set_carry: ∀p. beval → state p → state p ≝
45 λp,carry,st. mk_state … (st_frms … st) (pc … st) (sp … st) (isp … st) carry (regs … st) (m … st).
46
47definition set_pc: ∀p. address → state p → state p ≝
48 λp,pc,st. mk_state … (st_frms … st) pc (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
49
50definition set_frms: ∀p:sem_state_params. framesT p → state p → state p ≝
51 λp,frms,st. mk_state … frms (pc … st) (sp … st) (isp … st) (carry … st) (regs … st) (m … st).
52
53
54
55record more_sem_unserialized_params (uns_pars : unserialized_params) : Type[1] ≝
56  { st_pars :> sem_state_params
57  ; acca_store_ : acc_a_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
58  ; acca_retrieve_ : regsT st_pars → acc_a_reg uns_pars → res beval
59  ; acca_arg_retrieve_ : regsT st_pars → acc_a_arg uns_pars → res beval
60  ; accb_store_ : acc_b_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
61  ; accb_retrieve_ : regsT st_pars → acc_b_reg uns_pars → res beval
62  ; accb_arg_retrieve_ : regsT st_pars → acc_b_arg uns_pars → res beval
63  ; dpl_store_ : dpl_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
64  ; dpl_retrieve_ : regsT st_pars → dpl_reg uns_pars → res beval
65  ; dpl_arg_retrieve_ : regsT st_pars → dpl_arg uns_pars → res beval
66  ; dph_store_ : dph_reg uns_pars → beval → regsT st_pars → res (regsT st_pars)
67  ; dph_retrieve_ : regsT st_pars → dph_reg uns_pars → res beval
68  ; dph_arg_retrieve_ : regsT st_pars → dph_arg uns_pars → res beval
69  ; snd_arg_retrieve_ : regsT st_pars → snd_arg uns_pars → res beval
70  ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars)
71  ; fetch_ra: state st_pars →
72      res ((state st_pars) × address)
73
74  ; init_locals : localsT uns_pars → regsT st_pars → regsT st_pars
75   (*CSC: save_frame returns a res only because we can call a function with the wrong number and
76     type of arguments. To be fixed using a dependent type *)
77  ; save_frame: address → nat → paramsT … uns_pars → call_args uns_pars → call_dest uns_pars →
78      state st_pars → res (state st_pars)
79  ; fetch_external_args: external_function → state st_pars →
80      res (list val)
81  ; set_result: list val → state st_pars →
82      res (state st_pars)
83  ; call_args_for_main: call_args uns_pars
84  ; call_dest_for_main: call_dest uns_pars
85 }.
86
87
88definition helper_def_retrieve :
89  ∀X : ? → ? → Type[0].
90  (∀up.∀p:more_sem_unserialized_params up. regsT p → X up p → res beval) →
91  ∀up.∀p : more_sem_unserialized_params up.state p → X up p → res beval ≝
92    λX,f,up,p,st.f ? p (regs … st).
93
94definition helper_def_store :
95  ∀X : ? → ? → Type[0].
96  (∀up.∀p : more_sem_unserialized_params up.X up p → beval → regsT p → res (regsT p)) →
97  ∀up.∀p : more_sem_unserialized_params up.X up p → beval → state p → res (state p) ≝
98  λX,f,up,p,x,v,st.! r ← f ? p x v (regs … st) ; return (set_regs … r st).
99
100(* all res are cast to IO to aid unification later *)
101definition acca_retrieve ≝ helper_def_retrieve ? acca_retrieve_.
102definition acca_store ≝ helper_def_store ? acca_store_.
103definition acca_arg_retrieve ≝ helper_def_retrieve ? acca_arg_retrieve_.
104definition accb_store ≝ helper_def_store ? accb_store_.
105definition accb_retrieve ≝ helper_def_retrieve ? accb_retrieve_.
106definition accb_arg_retrieve ≝ helper_def_retrieve ? accb_arg_retrieve_.
107definition dpl_store ≝ helper_def_store ? dpl_store_.
108definition dpl_retrieve ≝ helper_def_retrieve ? dpl_retrieve_.
109definition dpl_arg_retrieve ≝ helper_def_retrieve ? dpl_arg_retrieve_.
110definition dph_store ≝ helper_def_store ? dph_store_.
111definition dph_retrieve ≝ helper_def_retrieve ? dph_retrieve_.
112definition dph_arg_retrieve ≝ helper_def_retrieve ? dph_arg_retrieve_.
113definition snd_arg_retrieve ≝ helper_def_retrieve ? snd_arg_retrieve_.
114definition pair_reg_move : ?→?→?→?→res ? ≝
115  λup.λp : more_sem_unserialized_params up.λst : state p.λpm : pair_move up.
116    ! r ← pair_reg_move_ ? p (regs ? st) pm;
117    return (set_regs ? r st).
118
119record more_sem_params (pp : params) : Type[1] ≝
120  { msu_pars :> more_sem_unserialized_params pp
121  ; succ_pc: succ pp → address → res address
122  ; read_result: ∀globals.genv globals pp → state msu_pars → res (list beval)
123  ; exec_extended: ∀globals.genv globals pp → extend_statements pp →
124      state msu_pars → IO io_out io_in ((option label) × trace × (state msu_pars))
125
126  ; pointer_of_label: ∀globals.genv globals pp → pointer → label → res (Σp:pointer. ptype p = Code)
127
128  ; pop_frame: ∀globals.genv globals pp → state msu_pars → res (state msu_pars)
129 
130  ; fetch_statement: ∀globals.genv globals pp → state msu_pars → res (joint_statement pp globals)
131  }.
132
133record sem_params : Type[1] ≝
134  { spp :> params
135  ; more_sem_pars :> more_sem_params spp
136  }.
137
138definition address_of_label: ∀globals. ∀p:sem_params.
139  genv globals p → pointer → label → res address ≝
140 λglobals,p,ge,ptr,l.
141  do newptr ← pointer_of_label … p ? ge … ptr l ;
142  OK … (address_of_code_pointer newptr).
143
144definition goto: ∀globals. ∀p:sem_params.
145  genv globals p → label → state p → res (state p) ≝
146 λglobals,p,ge,l,st.
147  ! oldpc ← pointer_of_address (pc … st);
148  ! newpc ← address_of_label … ge oldpc l ;
149  OK (state p) (set_pc … newpc st).
150
151axiom FailedStore: String.
152
153definition push: ∀p. state p → beval → res (state p) ≝
154 λp,st,v.
155  let isp ≝ isp … st in
156  do m ← opt_to_res … (msg FailedStore) (bestorev (m … st) isp v);
157  let isp ≝ shift_pointer … isp [[false;false;false;false;false;false;false;true]] in
158  OK … (set_m … m (set_sp … isp st)).
159
160definition pop: ∀p. state p → res (state p × beval) ≝
161 λp,st.
162  let isp ≝ isp ? st in
163  let isp ≝ neg_shift_pointer ? isp [[false;false;false;false;false;false;false;true]] in
164  let ist ≝ set_sp … isp st in
165  do v ← opt_to_res ? (msg FailedStore) (beloadv (m ? st) isp);
166  OK ? 〈st,v〉.
167
168definition save_ra : ∀p. state p → address → res (state p) ≝
169 λp,st,l.
170  let 〈addrl,addrh〉 ≝ l in
171  do st ← push … st addrl;
172  push … st addrh.
173
174definition load_ra : ∀p.state p → res (state p × address) ≝
175 λp,st.
176  do 〈st,addrh〉 ← pop … st;
177  do 〈st,addrl〉 ← pop … st;
178  OK ? 〈st, 〈addrl,addrh〉〉.
179
180
181(*
182definition empty_state: ∀p. more_sem_params p → state p ≝
183 mk_state … (empty_framesT …)
184*)
185
186definition next: ∀p:sem_params. succ … p → state p → res (state p) ≝
187 λp,l,st.
188  ! l' ← succ_pc … p l (pc … st) ;
189  OK … (set_pc … l' st).
190
191axiom MissingSymbol : String.
192axiom FailedLoad : String.
193axiom BadFunction : String.
194axiom BadPointer : String.
195
196definition eval_call_block:
197 ∀globals.∀p:sem_params. genv globals p → state p →
198  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
199 λglobals,p,ge,st,b,args,dest,ra.
200  ! fd ← (opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
201    match fd with
202    [ Internal fn ⇒
203      ! st ← save_frame … ra (joint_if_stacksize … fn) (joint_if_params … fn) args dest st ;
204      let regs ≝ init_locals … (joint_if_locals … fn) (regs … st) in
205      let l' ≝ joint_if_entry … fn in
206      let st ≝ set_regs p regs st in
207      let pointer_in_fn ≝ mk_pointer Code (mk_block Code (block_id b)) ? (mk_offset 0) in
208      ! newpc ← address_of_label … ge pointer_in_fn l' ;
209      let st ≝ set_pc … newpc st in
210      return 〈 E0, st〉
211    | External fn ⇒
212      ! params ← fetch_external_args … p fn st : IO ???;
213      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
214      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
215      (* CSC: XXX bug here; I think I should split it into Byte-long
216         components; instead I am making a singleton out of it. To be
217         fixed once we fully implement external functions. *)
218      let vs ≝ [mk_val ? evres] in
219      ! st ← set_result … p vs st : IO ???;
220      let st ≝ set_pc … ra st in
221      return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
222      ].
223% qed.
224
225definition eval_call_id:
226 ∀globals.∀p:sem_params. genv globals p → state p →
227  ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
228 λglobals,p,ge,st,id,args,dest,ra.
229  ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
230  eval_call_block … ge st b args dest ra.
231
232
233(* defining because otherwise typechecker stalls *)
234definition eval_address : ∀globals.∀p : sem_params. genv globals p → state p →
235  ∀i : ident.member i (eq_identifier SymbolTag) globals
236     →dpl_reg p→dph_reg p→ succ p → res (trace × (state p)) ≝
237     λglobals,p,ge,st,ident,prf,ldest,hdest,l.
238     let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
239     ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
240     ! st ← dpl_store … ldest laddr st;
241     ! st ← dph_store … hdest haddr st;
242     ! st ← next … p l st ;
243     return 〈E0, st〉.
244  [ cases addr //
245  | (* TODO: to prove *)
246    elim daemon
247  ] qed.
248
249(* defining because otherwise typechecker stalls *)
250definition eval_pop : ∀globals.∀p : sem_params. genv globals p → state p →
251  acc_a_reg p → succ p → res (trace × (state p)) ≝
252  λglobals,p,ge,st,dst,l.
253        ! 〈st,v〉 ← pop p st;
254        ! st ← acca_store p p dst v st;
255        ! st ← next p l st ;
256        return 〈E0, st〉.
257
258(* defining because otherwise typechecker stalls *)
259definition eval_call_id_succ:
260 ∀globals.∀p:sem_params. genv globals p → state p →
261  ident → call_args p → call_dest p → succ p → IO io_out io_in (trace×(state p)) ≝
262 λglobals,p,ge,st,id,args,dest,l.
263   ! ra ← succ_pc … p l (pc … st) : IO ??? ;
264   eval_call_id … ge st id args dest ra.
265
266definition eval_statement : ∀globals: list ident.∀p:sem_params. genv globals p →
267  state p → IO io_out io_in (trace × (state p)) ≝
268 λglobals,p,ge,st.
269  ! s ← fetch_statement … ge st : IO ???;
270  match s return λ_.IO io_out io_in (trace × (state p)) with
271    [ GOTO l ⇒
272       ! st ← goto … ge l st ;
273       return 〈E0, st〉
274    | RETURN ⇒
275      ! p ← fetch_ra … st ;
276      let 〈st,ra〉 ≝ p in
277      ! st ← pop_frame … ge st;
278      return 〈E0,set_pc … ra st〉
279   | sequential seq l ⇒
280      match seq with
281      [ extension c ⇒
282        ! 〈lbl_opt, tr, st〉 ← exec_extended … ge c st ;
283        match lbl_opt with
284        [ Some lbl ⇒
285          ! st ← goto … ge lbl st ;
286          return 〈tr, st〉
287        | None ⇒
288          ! st ← next … l st ;
289          return 〈tr, st〉
290        ]       
291       | COST_LABEL cl ⇒
292         ! st ← next … p l st ;
293         return 〈Echarge cl, st〉
294      | COMMENT c ⇒
295         ! st ← next … p l st ;
296         return 〈E0, st〉
297      | LOAD dst addrl addrh ⇒
298        ! vaddrh ← dph_arg_retrieve … st addrh ;
299        ! vaddrl ← dpl_arg_retrieve … st addrl;
300        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
301        ! v ← opt_to_res … (msg FailedLoad) (beloadv (m … st) vaddr);
302        ! st ← acca_store p … dst v st ;
303        ! st ← next … p l st ;
304        return 〈E0, st〉
305      | STORE addrl addrh src ⇒
306        ! vaddrh ← dph_arg_retrieve … st addrh;
307        ! vaddrl ← dpl_arg_retrieve … st addrl;
308        ! vaddr ← pointer_of_address 〈vaddrl,vaddrh〉;
309        ! v ← acca_arg_retrieve … st src;
310        ! m' ← opt_to_res … (msg FailedStore) (bestorev (m … st) vaddr v);
311        let st ≝ set_m … m' st in
312        ! st ← next … p l st ;
313        return 〈E0, st〉
314      | COND src ltrue ⇒
315        ! v ← acca_retrieve … st src;
316        ! b ← bool_of_beval v;
317        if b then
318         ! st ← goto … p ge ltrue st ;
319         return 〈E0, st〉
320        else
321         ! st ← next … p l st ;
322         return 〈E0, st〉
323      | ADDRESS ident prf ldest hdest ⇒
324        eval_address … ge st ident prf ldest hdest l
325      | OP1 op dacc_a sacc_a ⇒
326        ! v ← acca_retrieve … st sacc_a;
327        ! v ← Byte_of_val v;
328        let v' ≝ BVByte (op1 eval op v) in
329        ! st ← acca_store … dacc_a v' st;
330        ! st ← next … l st ;
331        return 〈E0, st〉
332      | OP2 op dacc_a sacc_a src ⇒
333        ! v1 ← acca_arg_retrieve … st sacc_a;
334        ! v1 ← Byte_of_val v1;
335        ! v2 ← snd_arg_retrieve … st src;
336        ! v2 ← Byte_of_val v2;
337        ! carry ← bool_of_beval (carry … st);
338          let 〈v',carry〉 ≝ op2 eval carry op v1 v2 in
339          let v' ≝ BVByte v' in
340          let carry ≝ beval_of_bool carry in
341        ! st ← acca_store … dacc_a v' st;
342          let st ≝ set_carry … carry st in
343        ! st ← next … l st ;
344        return 〈E0, st〉
345      | CLEAR_CARRY ⇒
346        ! st ← next … l (set_carry … BVfalse st) ;
347        return 〈E0, st〉
348      | SET_CARRY ⇒
349        ! st ← next … l (set_carry … BVtrue st) ;
350        return 〈E0, st〉
351      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
352        ! v1 ← acca_arg_retrieve … st sacc_a_reg;
353        ! v1 ← Byte_of_val v1;
354        ! v2 ← accb_arg_retrieve … st sacc_b_reg;
355        ! v2 ← Byte_of_val v2;
356        let 〈v1',v2'〉 ≝ opaccs eval op v1 v2 in
357        let v1' ≝ BVByte v1' in
358        let v2' ≝ BVByte v2' in
359        ! st ← acca_store … dacc_a_reg v1' st;
360        ! st ← accb_store … dacc_b_reg v2' st;
361        ! st ← next … l st ;
362        return 〈E0, st〉
363      | POP dst ⇒
364        eval_pop … ge st dst l
365      | PUSH src ⇒
366        ! v ← acca_arg_retrieve … st src;
367        ! st ← push … st v;
368        ! st ← next … l st ;
369        return 〈E0, st〉
370      | MOVE dst_src ⇒
371        ! st ← pair_reg_move … st dst_src ;
372        ! st ← next … l st ;
373        return 〈E0, st〉
374      | CALL_ID id args dest ⇒
375        eval_call_id_succ … ge st id args dest l
376     ]
377   ].
378
379definition is_final: ∀globals:list ident. ∀p: sem_params.
380  genv globals p → address → state p → option int ≝
381 λglobals,p,ge,exit,st.res_to_opt ? (
382  do s ← fetch_statement … ge st;
383  match s with
384   [ RETURN ⇒
385      do 〈st,ra〉 ← fetch_ra … st;
386      if eq_address ra exit then
387       do vals ← read_result … ge st ;
388       Word_of_list_beval vals
389      else
390       Error ? [ ]
391   | _ ⇒ Error ? [ ]]).
392
393record evaluation_parameters : Type[1] ≝
394 { globals: list ident
395 ; sparams:> sem_params
396 ; exit: address
397 ; genv2: genv globals sparams
398 }.
399
400definition joint_exec: trans_system io_out io_in ≝
401  mk_trans_system … evaluation_parameters (λG. state G)
402   (λG.is_final (globals G) G (genv2 G) (exit G))
403   (λG.eval_statement (globals G) G (genv2 G)).
404
405definition make_global :
406 ∀pars: sem_params.
407  joint_program pars → evaluation_parameters
408
409 λpars.
410 (* Invariant: a -1 block is unused in common/Globalenvs *)
411 let b ≝ mk_block Code (-1) in
412 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
413 let addr ≝ address_of_code_pointer ptr in
414  (λp. mk_evaluation_parameters
415    (prog_var_names … p)
416    (mk_sem_params … pars)
417    addr
418    (globalenv Genv … p)
419  ).
420% qed.
421
422axiom ExternalMain: String.
423
424definition make_initial_state :
425 ∀pars: sem_params.
426 ∀p: joint_program … pars. res (state pars) ≝
427λpars,p.
428  let sem_globals ≝ make_global pars p in
429  let ge ≝ genv2 sem_globals in
430  let m ≝ init_mem Genv … p in
431  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
432  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
433  let dummy_pc ≝ mk_pointer Code (mk_block Code (-1)) ? (mk_offset 0) in
434  let spp ≝ mk_pointer XData spb ? (mk_offset external_ram_size) in
435  let ispp ≝ mk_pointer XData ispb ? (mk_offset 47) in
436  do sp ← address_of_pointer spp ;
437  let main ≝ prog_main … p in
438  let st0 ≝ mk_state … (empty_framesT …) sp ispp dummy_pc BVfalse (empty_regsT … sp) m in
439  let trace_state ≝
440   eval_call_id … pars ge st0 main (call_args_for_main … pars)
441    (call_dest_for_main … pars) (exit sem_globals) in
442  match trace_state with
443  [ Value tr_st ⇒ OK … (\snd tr_st) (* E0 trace thrown away *)
444  | Wrong msg ⇒ Error … msg
445  | Interact _ _ ⇒ Error … [MSG ExternalMain] (* External main not supported: why? *)
446  ].
447[3: % | cases ispb | cases spb] * #r #off #E >E %
448qed.
449
450definition joint_fullexec :
451 ∀pars:sem_params.fullexec io_out io_in ≝
452 λpars.mk_fullexec ??? joint_exec (make_global pars) (make_initial_state pars).
453 
454 
Note: See TracBrowser for help on using the repository browser.