source: src/RTL/semantics_paolo.ma @ 1921

Last change on this file since 1921 was 1643, checked in by tranquil, 9 years ago
  • some changes in everything
  • separated extensions in sequential and final, to accomodate tailcalls
  • finished RTL's semantics
File size: 6.8 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: address
9 ; fr_sp: pointer
10 ; fr_carry: beval
11 ; fr_regs: register_env beval
12 }.
13
14definition rtl_sem_state_params : 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 : rtl_argument.
22  match a with
23  [ Reg r ⇒ reg_retrieve env r
24  | Imm b ⇒ return (BVByte 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_sem_state_params → res ((state rtl_sem_state_params) × address) ≝
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_locals :
39 list register → register_env beval → register_env beval ≝
40 λlocals,env.
41  foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
42
43
44definition rtl_setup_call:
45 nat → list register → list rtl_argument → state rtl_sem_state_params → res (state rtl_sem_state_params) ≝
46  λstacksize,formal_arg_regs,actual_arg_regs,st.
47  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
48  do new_regs ←
49   mfold_left2 …
50    (λlenv,dest,src.
51      do v ← rtl_arg_retrieve … (regs ? st) src ;
52      OK … (add … lenv dest v))
53    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
54  OK …
55   (set_regs rtl_sem_state_params new_regs
56    (set_m … mem
57     (set_sp … (mk_pointer XData b ? (mk_offset 0)) st))).
58cases b * #r #off #E >E %
59qed.
60
61definition rtl_save_frame ≝ λl.λretregs.λst : state rtl_sem_state_params.
62  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
63  set_frms rtl_sem_state_params frame st. 
64
65(*CSC: XXXX, for external functions only*)
66axiom rtl_fetch_external_args: external_function → state rtl_sem_state_params → res (list val).
67axiom rtl_set_result: list val → state rtl_sem_state_params → res (state rtl_sem_state_params).
68
69definition rtl_msu_params :
70  more_sem_unserialized_params rtl_uns_params ≝
71 mk_more_sem_unserialized_params rtl_uns_params rtl_sem_state_params
72    reg_store reg_retrieve rtl_arg_retrieve
73    reg_store reg_retrieve rtl_arg_retrieve
74    reg_store reg_retrieve rtl_arg_retrieve
75    reg_store reg_retrieve rtl_arg_retrieve
76    rtl_arg_retrieve
77    (λenv,p. let 〈dest,src〉 ≝ p in
78      ! v ← rtl_arg_retrieve env src ;
79      reg_store dest v env)
80    rtl_fetch_ra
81    rtl_init_locals
82    rtl_save_frame
83    rtl_setup_call
84    rtl_fetch_external_args
85    rtl_set_result
86    [ ] [ ] (*dummy*).
87
88(* alias *)
89definition rtl_reg_store : register→beval→state rtl_sem_state_params→
90    res (state rtl_sem_state_params) ≝ acca_store ? rtl_msu_params.
91definition rtl_reg_retrieve : state rtl_sem_state_params→register→res beval ≝
92    acca_retrieve ? rtl_msu_params.
93
94definition rtl_read_result :
95 ∀globals. genv globals rtl_params → state rtl_sem_state_params → res (list beval) ≝
96 λglobals,ge,st.
97  ! p ← code_pointer_of_address (pc … st) ;
98  ! fn ← fetch_function … ge p ;
99  m_mmap … (rtl_reg_retrieve st) (joint_if_result … fn).
100
101(*CSC: we could use a dependent type here: the list of return values should have
102  the same length of the list of return registers that store the values. This
103  saves the OutOfBounds exception *)
104definition rtl_pop_frame:
105 ∀globals. genv globals rtl_params → state rtl_sem_state_params →
106  res (state rtl_sem_state_params) ≝
107 λglobals,ge,st.
108  do ret_vals ← rtl_read_result … ge st ;
109  match st_frms ? st with
110  [ nil ⇒ Error ? [MSG EmptyStack]
111  | cons hd tl ⇒
112     do st ←
113      mfold_left_i …
114       (λi.λst.λreg.
115         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
116         rtl_reg_store reg v st)
117       (OK … st) (fr_ret_regs hd) ;
118     OK …
119      (set_frms rtl_sem_state_params tl
120        (set_regs rtl_sem_state_params (fr_regs hd)
121         (set_sp … (fr_sp hd)
122          (set_carry … (fr_carry hd)
123           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
124
125
126(* This code is quite similar to eval_call_block: can we factorize it out? *)
127definition eval_tail_call_block:
128 ∀globals.genv globals rtl_params → state rtl_sem_state_params →
129  block → call_args rtl_uns_params → IO io_out io_in (trace×(state rtl_sem_state_params)) ≝
130 λglobals,ge,st,b,args.
131  ! 〈next, tr, st〉 ← eval_call_block_preamble ? rtl_params rtl_msu_params ge st b args (None ?) ;
132  match next with
133  [ None ⇒ (* Paolo: external tailcall, copied from evaluation of return, is it right? *)
134    ! 〈st,ra〉 ← fetch_ra … st ;
135    ! st ← rtl_pop_frame … ge st;
136    return 〈tr,st〉
137  | Some lbl ⇒
138    return 〈tr,st〉
139  ].
140
141definition block_of_register_pair: register → register → state rtl_sem_state_params → res block ≝
142 λr1,r2,st.
143 do v1 ← rtl_reg_retrieve st r1 ;
144 do v2 ← rtl_reg_retrieve st r2 ;
145 do ptr ← pointer_of_address 〈v1,v2〉 ;
146 OK … (pblock ptr). 
147
148definition rtl_exec_extended:
149 ∀globals. genv globals rtl_params →
150  rtl_instruction_extension → state rtl_sem_state_params → address →
151   IO io_out io_in ((option (label)) × trace × (state rtl_sem_state_params)) ≝
152 λglobals,ge,stm,st,next_addr.
153  match stm with
154   [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
155      let sp ≝ sp ? st in
156      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
157      ! st ← rtl_reg_store dreg1 dpl st ;
158      ! st ← rtl_reg_store dreg2 dph st ;
159      return 〈None label,E0, st〉
160   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
161     ! b ← block_of_register_pair r1 r2 st : IO ???;
162     eval_call_block_preamble ? rtl_params rtl_msu_params
163                              ge st b args (Some ? 〈dest,next_addr〉) ].
164
165definition rtl_exec_fin_extended:
166 ∀globals. genv globals rtl_params →
167  rtl_statement_extension → state rtl_sem_state_params →
168   IO io_out io_in (trace × (state rtl_sem_state_params)) ≝
169   λglobals,ge,stm,st.
170   match stm with
171   [ rtl_st_ext_tailcall_id id args ⇒
172      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
173      eval_tail_call_block … ge st b args
174   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
175      ! b ← block_of_register_pair r1 r2 st : IO ???;
176      eval_tail_call_block … ge st b args
177   ].
178
179definition rtl_msg_params : more_sem_genv_params rtl_params ≝
180  mk_more_sem_genv_params rtl_params rtl_msu_params
181    rtl_read_result
182    rtl_exec_extended
183    rtl_exec_fin_extended
184    rtl_pop_frame.
185
186
187
188definition rtl_sem_params : sem_params ≝ make_sem_graph_params … rtl_msg_params.
189
190definition rtl_fullexec ≝ joint_fullexec … rtl_sem_params.
Note: See TracBrowser for help on using the repository browser.