source: src/RTL/semantics.ma @ 1412

Last change on this file since 1412 was 1412, checked in by sacerdot, 10 years ago

Tailcalls (via ids or pointers) to internal functions implemented.
Tailcalls to external function left as a daemon.

File size: 7.2 KB
Line 
1include "joint/SemanticUtils.ma".
2include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
3include alias "common/Identifiers.ma".
4include alias "ASM/Util.ma".
5
6record frame: Type[0] ≝
7 { fr_ret_regs: list register
8 ; fr_pc: address
9 ; fr_sp: pointer
10 ; fr_carry: beval
11 ; fr_regs: register_env beval
12 }.
13
14definition rtl_more_sem_params: more_sem_params rtl_params_ :=
15 mk_more_sem_params rtl_params_
16  (list frame) [] (register_env beval) (empty_map …) [] [](*dummy*) graph_succ_p
17   reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
18    reg_store reg_retrieve reg_store reg_retrieve
19     (λlocals,dest_src.
20       do v ← reg_retrieve locals (\snd dest_src) ;
21       reg_store (\fst dest_src) v locals)
22     pointer_of_label.
23definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
24
25definition rtl_init_locals :
26 list register → register_env beval → register_env beval ≝
27 λlocals,env.
28  foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
29
30(*CSC: could we use here a dependent type to avoid the Error case? *)
31axiom EmptyStack: String.
32axiom OutOfBounds: String.
33
34definition rtl_fetch_ra:
35 state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
36 λst.
37  match st_frms ? st with
38  [ nil ⇒ Error ? [MSG EmptyStack]
39  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
40
41definition rtl_result_regs:
42 ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
43 λglobals,ge,st.
44  do fn ← graph_fetch_function … globals ge st ;
45  OK … (joint_if_result … fn).
46
47(*CSC: we could use a dependent type here: the list of return values should have
48  the same length of the list of return registers that store the values. This
49  saves the OutOfBounds exception *)
50definition rtl_pop_frame:
51 ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
52 λglobals,ge,st.
53  do ret_regs ← rtl_result_regs … ge st ;
54  do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
55  match st_frms ? st with
56  [ nil ⇒ Error ? [MSG EmptyStack]
57  | cons hd tl ⇒
58     do st ←
59      mfold_left_i ??
60       (λi.λst.λreg.
61         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
62         greg_store rtl_sem_params reg v st)
63       (OK … st) (fr_ret_regs hd) ;
64     OK …
65      (set_frms rtl_sem_params tl
66        (set_regs rtl_sem_params (fr_regs hd)
67         (set_sp … (fr_sp hd)
68          (set_carry … (fr_carry hd)
69           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
70
71definition rtl_call_function:
72 nat → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
73  λstacksize,formal_arg_regs,actual_arg_regs,st.
74  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
75  do new_regs ←
76   mfold_left2 …
77    (λlenv,dest,src.
78      do v ← greg_retrieve … st src ;
79      OK … (add … lenv dest v))
80    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
81  OK …
82   (set_regs rtl_sem_params new_regs
83    (set_m … mem
84     (set_sp … (mk_pointer XData b ? (mk_offset 0)) st))).
85cases b * #r #off #E >E %
86qed.
87
88definition rtl_save_frame:
89 address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
90 λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
91  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in
92  let st ≝ set_frms rtl_sem_params frame st in
93  rtl_call_function stacksize formal_arg_regs actual_arg_regs st.
94
95(*CSC: XXXX, for external functions only*)
96axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
97axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
98
99definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
100 λglobals.
101  mk_more_sem_params1 … rtl_more_sem_params
102   (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
103   rtl_init_locals rtl_save_frame (rtl_pop_frame …)
104   rtl_fetch_external_args rtl_set_result.
105
106definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
107 λr1,r2,st.
108 do v1 ← greg_retrieve rtl_sem_params st r1 ;
109 do v2 ← greg_retrieve rtl_sem_params st r2 ;
110 do ptr ← pointer_of_address 〈v1,v2〉 ;
111 OK … (pblock ptr). 
112
113(* This code is quite similar to eval_call_block: can we factorize it out? *)
114definition eval_tail_call_block:
115 ∀globals.genv … (rtl_params globals) → state rtl_sem_params →
116  block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
117 λglobals,ge,st,b,args.
118  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
119    match fd with
120    [ Internal fn ⇒
121      let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in
122      ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ;
123      let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
124      let l' ≝ joint_if_entry … fn in
125       ret ? 〈 E0, goto … l' (set_regs rtl_sem_params regs st)〉
126    | External fn ⇒ ?(*
127      ! params ← fetch_external_args … fn st;
128      ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
129      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
130      (* CSC: XXX bug here; I think I should split it into Byte-long
131         components; instead I am making a singleton out of it. To be
132         fixed once we fully implement external functions. *)
133        let vs ≝ [mk_val ? evres] in
134      ! st ← set_result … vs st;
135      let st ≝ set_pc … ra st in
136        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *)
137     ].
138cases daemon (*CSC: XXX tailcall to external function not implemented yet;
139                    it needs alls other functions on external calls *)
140qed.
141
142definition rtl_exec_extended:
143 ∀globals. genv globals (rtl_params globals) →
144  rtl_statement_extension → label → state rtl_sem_params →
145   IO io_out io_in (trace × (state rtl_sem_params)) ≝
146 λglobals,ge,stm,l,st.
147  match stm with
148   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
149      let sp ≝ sp ? st in
150      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
151      ! st ← greg_store rtl_sem_params dreg1 dpl st ;
152      ! st ← greg_store rtl_sem_params dreg2 dph st ;
153       ret ? 〈E0, goto … l st〉
154   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
155      ! b ← block_of_register_pair r1 r2 st ;
156      ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) ;
157      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
158       ge st b args dest ra
159   | rtl_st_ext_tailcall_id id args ⇒
160      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
161      eval_tail_call_block … ge st b args
162   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
163      ! b ← block_of_register_pair r1 r2 st ;
164      eval_tail_call_block … ge st b args
165   ].
166
167definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
168 λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
169
170definition rtl_fullexec ≝
171 joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
Note: See TracBrowser for help on using the repository browser.