source: src/RTL/semantics_paolo.ma @ 2233

Last change on this file since 2233 was 2233, checked in by tranquil, 7 years ago
  • completed update of ERTL semantics
  • some minor changes in joint semantics
File size: 7.4 KB
Line 
1include "joint/semanticsUtils_paolo.ma".
2include "RTL/RTL_paolo.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: cpointer
9 ; fr_sp: xpointer
10 ; fr_carry: beval
11 ; fr_regs: register_env beval
12 }.
13
14definition RTL_state : sem_state_params ≝
15  mk_sem_state_params
16    (list frame)
17    [ ]
18    (register_env beval)
19    (λ_.empty_map …).
20
21definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
22  match a with
23  [ Reg r ⇒ reg_retrieve env r
24  | Imm b ⇒ return b
25  ].
26
27(*CSC: could we use here a dependent type to avoid the Error case? *)
28axiom EmptyStack: String.
29axiom OutOfBounds: String.
30
31definition rtl_fetch_ra:
32 RTL_state → res (RTL_state × cpointer) ≝
33 λst.
34  match st_frms ? st with
35  [ nil ⇒ Error ? [MSG EmptyStack]
36  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
37
38definition rtl_init_local :
39 register → register_env beval → register_env beval ≝
40 λlocal,env.add … env local BVundef.
41
42definition rtl_setup_call:
43 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
44  λstacksize,formal_arg_regs,actual_arg_regs,st.
45  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
46  do new_regs ←
47   mfold_left2 …
48    (λlenv,dest,src.
49      do v ← rtl_arg_retrieve … (regs ? st) src ;
50      OK … (add … lenv dest v))
51    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
52  OK …
53   (set_regs RTL_state new_regs
54    (set_m … mem
55     (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
56cases b * #r #off #E >E %
57qed.
58
59definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state.
60  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
61  OK … (set_frms RTL_state frame st).
62
63(*CSC: XXXX, for external functions only*)
64axiom rtl_fetch_external_args: external_function → RTL_state → res (list val).
65axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
66
67definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
68definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
69
70definition rtl_read_result :
71 ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
72 λglobals,ge,rets,st.
73 m_list_map … (rtl_reg_retrieve st) rets.
74
75(*CSC: we could use a dependent type here: the list of return values should have
76  the same length of the list of return registers that store the values. This
77  saves the OutOfBounds exception *)
78definition rtl_pop_frame:
79 ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state →
80  res RTL_state ≝
81 λglobals,ge,curr_fn,st.
82  let ret ≝ joint_if_result … curr_fn in
83  do ret_vals ← rtl_read_result … ge ret st ;
84  match st_frms ? st with
85  [ nil ⇒ Error ? [MSG EmptyStack]
86  | cons hd tl ⇒
87     do st ←
88      mfold_left_i …
89       (λi.λst.λreg.
90         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
91         rtl_reg_store reg v st)
92       (OK … st) (fr_ret_regs hd) ;
93     OK …
94      (set_frms RTL_state tl
95        (set_regs RTL_state (fr_regs hd)
96         (set_sp … (fr_sp hd)
97          (set_carry … (fr_carry hd)
98           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
99
100(* This code is quite similar to eval_call_block: can we factorize it out? *)
101definition eval_tailcall_block:
102 ∀globals.genv RTL globals → RTL_state →
103  block → call_args RTL →
104  (* this is where the result of the current function should be stored *)
105  call_dest RTL →
106  IO io_out io_in
107    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
108 λglobals,ge,st,b,args,ret.
109  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
110    match fd with
111    [ Internal fd ⇒
112      return 〈FTailInit ?? (block_id b) fd args, st〉
113    | External fn ⇒
114      ! params ← rtl_fetch_external_args … fn st : IO ???;
115      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
116      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
117      (* CSC: XXX bug here; I think I should split it into Byte-long
118         components; instead I am making a singleton out of it. To be
119         fixed once we fully implement external functions. *)
120      let vs ≝ [mk_val ? evres] in
121      ! st ← rtl_set_result … vs ret st : IO ???;
122      return 〈FEnd2 ??, st〉
123    ].
124
125definition block_of_register_pair: register → register → RTL_state → res block ≝
126 λr1,r2,st.
127 do v1 ← rtl_reg_retrieve st r1 ;
128 do v2 ← rtl_reg_retrieve st r2 ;
129 do ptr ← pointer_of_address 〈v1,v2〉 ;
130 OK … (pblock ptr). 
131
132definition eval_rtl_seq:
133 ∀globals. genv RTL globals →
134  rtl_seq → joint_internal_function RTL globals → RTL_state →
135   IO io_out io_in RTL_state ≝
136 λglobals,ge,stm,curr_fn,st.
137  match stm with
138   [ rtl_stack_address dreg1 dreg2  ⇒
139      let sp ≝ sp ? st in
140      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
141      ! st ← rtl_reg_store dreg1 dpl st ;
142      rtl_reg_store dreg2 dph st
143   ].
144
145definition eval_rtl_call:
146 ∀globals. genv RTL globals →
147  rtl_call → RTL_state →
148   IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
149 λglobals,ge,stm,st.
150  match stm with
151  [ rtl_call_ptr r1 r2 args dest ⇒
152    ! b ← block_of_register_pair r1 r2 st : IO ???;
153    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
154    match fd with
155    [ Internal fd ⇒
156      return 〈Init ?? (block_id b) fd args dest, st〉
157    | External fn ⇒
158      ! params ← rtl_fetch_external_args … fn st : IO ???;
159      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
160      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
161      (* CSC: XXX bug here; I think I should split it into Byte-long
162         components; instead I am making a singleton out of it. To be
163         fixed once we fully implement external functions. *)
164      let vs ≝ [mk_val ? evres] in
165      ! st ← rtl_set_result … vs dest st : IO ???;
166      return 〈Proceed ???, st〉
167    ]
168  ].
169
170definition eval_rtl_tailcall:
171 ∀globals. genv RTL globals →
172  rtl_tailcall → joint_internal_function RTL globals → RTL_state →
173   IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
174   λglobals,ge,stm,curr_fn,st.
175   let ret ≝ joint_if_result … curr_fn in
176   match stm with
177   [ rtl_tailcall_id id args ⇒
178      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
179      eval_tailcall_block … ge st b args ret
180   | rtl_tailcall_ptr r1 r2 args ⇒
181      ! b ← block_of_register_pair r1 r2 st : IO ???;
182      eval_tailcall_block … ge st b args ret
183   ].
184
185definition RTL_semantics ≝
186  make_sem_graph_params RTL
187    (mk_more_sem_unserialized_params ??
188      RTL_state
189      reg_store reg_retrieve rtl_arg_retrieve
190      reg_store reg_retrieve rtl_arg_retrieve
191      reg_store reg_retrieve rtl_arg_retrieve
192      reg_store reg_retrieve rtl_arg_retrieve
193      rtl_arg_retrieve
194      (λenv,p. let 〈dest,src〉 ≝ p in
195        ! v ← rtl_arg_retrieve env src ;
196        reg_store dest v env)
197      rtl_fetch_ra
198      rtl_init_local
199      rtl_save_frame
200      rtl_setup_call
201      rtl_fetch_external_args
202      rtl_set_result
203      [ ] [ ]
204      rtl_read_result
205      eval_rtl_seq
206      eval_rtl_tailcall
207      eval_rtl_call
208      rtl_pop_frame
209      (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).
Note: See TracBrowser for help on using the repository browser.