source: src/joint/semantics_paolo.ma @ 1641

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