source: src/RTL/semantics_paolo.ma @ 2217

Last change on this file since 2217 was 2217, checked in by tranquil, 7 years ago
  • collapsed step_params, unserialized_params, funct_params and local_params into one (unserialized_params)
  • completed update of RTL, LTL and LIN semantics
File size: 7.3 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 state RTL_state → res ((state 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 → state RTL_state → res (state 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 : state 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 → state RTL_state → res (list val).
65axiom rtl_set_result: list val → list register → state RTL_state → res (state 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 → state 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 → list register → state RTL_state →
80  res (state RTL_state) ≝
81 λglobals,ge,ret,st.
82  do ret_vals ← rtl_read_result … ge ret st ;
83  match st_frms ? st with
84  [ nil ⇒ Error ? [MSG EmptyStack]
85  | cons hd tl ⇒
86     do st ←
87      mfold_left_i …
88       (λi.λst.λreg.
89         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
90         rtl_reg_store reg v st)
91       (OK … st) (fr_ret_regs hd) ;
92     OK …
93      (set_frms RTL_state tl
94        (set_regs RTL_state (fr_regs hd)
95         (set_sp … (fr_sp hd)
96          (set_carry … (fr_carry hd)
97           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
98
99(* This code is quite similar to eval_call_block: can we factorize it out? *)
100definition eval_tailcall_block:
101 ∀globals.genv RTL globals → state RTL_state →
102  block → call_args RTL →
103  (* this is where the result of the current function should be stored *)
104  call_dest RTL →
105  IO io_out io_in
106    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×(state RTL_state)) ≝
107 λglobals,ge,st,b,args,ret.
108  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
109    match fd with
110    [ Internal fd ⇒
111      return 〈FTailInit ?? (block_id b) fd args, st〉
112    | External fn ⇒
113      ! params ← rtl_fetch_external_args … fn st : IO ???;
114      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
115      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
116      (* CSC: XXX bug here; I think I should split it into Byte-long
117         components; instead I am making a singleton out of it. To be
118         fixed once we fully implement external functions. *)
119      let vs ≝ [mk_val ? evres] in
120      ! st ← rtl_set_result … vs ret st : IO ???;
121      return 〈FEnd2 ??, st〉
122    ].
123
124definition block_of_register_pair: register → register → state RTL_state → res block ≝
125 λr1,r2,st.
126 do v1 ← rtl_reg_retrieve st r1 ;
127 do v2 ← rtl_reg_retrieve st r2 ;
128 do ptr ← pointer_of_address 〈v1,v2〉 ;
129 OK … (pblock ptr). 
130
131definition eval_rtl_seq:
132 ∀globals. genv RTL globals →
133  rtl_seq → state RTL_state →
134   IO io_out io_in (state RTL_state) ≝
135 λglobals,ge,stm,st.
136  match stm with
137   [ rtl_stack_address dreg1 dreg2  ⇒
138      let sp ≝ sp ? st in
139      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
140      ! st ← rtl_reg_store dreg1 dpl st ;
141      rtl_reg_store dreg2 dph st
142   ].
143
144definition eval_rtl_call:
145 ∀globals. genv RTL globals →
146  rtl_call → state RTL_state →
147   IO io_out io_in ((step_flow RTL ? Call)×(state RTL_state)) ≝
148 λglobals,ge,stm,st.
149  match stm with
150  [ rtl_call_ptr r1 r2 args dest ⇒
151    ! b ← block_of_register_pair r1 r2 st : IO ???;
152    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
153    match fd with
154    [ Internal fd ⇒
155      return 〈Init ?? (block_id b) fd args dest, st〉
156    | External fn ⇒
157      ! params ← rtl_fetch_external_args … fn st : IO ???;
158      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
159      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
160      (* CSC: XXX bug here; I think I should split it into Byte-long
161         components; instead I am making a singleton out of it. To be
162         fixed once we fully implement external functions. *)
163      let vs ≝ [mk_val ? evres] in
164      ! st ← rtl_set_result … vs dest st : IO ???;
165      return 〈Proceed ???, st〉
166    ]
167  ].
168
169definition eval_rtl_tailcall:
170 ∀globals. genv RTL globals →
171  rtl_tailcall → call_dest RTL → state RTL_state →
172   IO io_out io_in ((fin_step_flow RTL ? Call)×(state RTL_state)) ≝
173   λglobals,ge,stm,ret,st.
174   match stm with
175   [ rtl_tailcall_id id args ⇒
176      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
177      eval_tailcall_block … ge st b args ret
178   | rtl_tailcall_ptr r1 r2 args ⇒
179      ! b ← block_of_register_pair r1 r2 st : IO ???;
180      eval_tailcall_block … ge st b args ret
181   ].
182
183definition RTL_semantics ≝
184  mk_more_sem_unserialized_params RTL (joint_internal_function RTL)
185    RTL_state
186    reg_store reg_retrieve rtl_arg_retrieve
187    reg_store reg_retrieve rtl_arg_retrieve
188    reg_store reg_retrieve rtl_arg_retrieve
189    reg_store reg_retrieve rtl_arg_retrieve
190    rtl_arg_retrieve
191    (λenv,p. let 〈dest,src〉 ≝ p in
192      ! v ← rtl_arg_retrieve env src ;
193      reg_store dest v env)
194    rtl_fetch_ra
195    rtl_init_local
196    rtl_save_frame
197    rtl_setup_call
198    rtl_fetch_external_args
199    rtl_set_result
200    [ ] [ ]
201    rtl_read_result
202    eval_rtl_seq
203    eval_rtl_tailcall
204    eval_rtl_call.
Note: See TracBrowser for help on using the repository browser.