source: src/ERTL/ERTL_semantics.ma @ 3259

Last change on this file since 3259 was 3259, checked in by piccolo, 7 years ago

changed ERTL semantics:
1) added manipulation of stack pointer directly in the semantics
2) added values of Callee Saved in frames

File size: 8.0 KB
Line 
1include "joint/semanticsUtils.ma".
2include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
3include alias "common/Identifiers.ma".
4
5definition ertl_reg_env ≝ register_env beval × hw_register_env.
6
7definition ps_reg_store: ? → ? → ? → res ? ≝
8 λr,v.λlocal_env : ertl_reg_env.
9  let res ≝ reg_store r v (\fst local_env) in
10  OK … 〈res, \snd local_env〉.
11
12definition ps_reg_retrieve ≝
13 λlocal_env:ertl_reg_env. reg_retrieve … (\fst local_env).
14
15definition hw_reg_store ≝
16 λr,v.λlocal_env:ertl_reg_env.
17  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
18
19definition hw_reg_retrieve ≝
20 λlocal_env:ertl_reg_env.λreg.
21  OK … (hwreg_retrieve … (\snd local_env) reg).
22
23
24definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
25  λlocal_env,a.
26  match a with
27  [ Reg r ⇒ ps_reg_retrieve local_env r
28  | Imm b ⇒ return BVByte b
29  ].
30
31definition get_hwsp : ertl_reg_env → res xpointer ≝
32 λst.hwreg_retrieve_sp (\snd st).
33
34definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
35 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.
36 
37record ERTL_frame : Type[0] ≝
38{ psd_reg_env : register_env beval
39; funct_block : Σb:block.block_region b=Code
40; callee_values : Σl : list beval. |l| = |RegisterCalleeSaved|
41}.
42
43definition ERTL_state : sem_state_params ≝
44  mk_sem_state_params
45 (* framesT ≝ *) (list (ERTL_frame))
46 (* empty_framesT ≝ *) [ ]
47 (* regsT ≝ *) ertl_reg_env
48 (* empty_regsT ≝ *) (λsp.〈empty_map …, init_hw_register_env sp〉)
49 (*load_sp ≝ *) get_hwsp
50 (*save_sp ≝ *) set_hwsp.
51
52(* we ignore need_spilled_no as we never move framesize based values around in the
53   translation *)
54definition ertl_eval_move ≝ λenv.λpr : move_dst × move_src.
55      ! v ←
56        match \snd pr with
57        [ Reg src ⇒
58          match src with
59          [ PSD r ⇒ ps_reg_retrieve env r
60          | HDW r ⇒ hw_reg_retrieve env r
61          ]
62        | Imm b ⇒ return BVByte b ] ;
63      match \fst pr with
64      [ PSD r ⇒ ps_reg_store r v env
65      | HDW r ⇒ hw_reg_store r v env
66      ].
67
68definition ertl_allocate_local ≝
69  λreg.λlenv : ertl_reg_env.
70  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
71
72definition ertl_save_frame:
73 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
74 λ_.λ_.λst.
75  ! st' ← push_ra … st (pc … st) ;
76  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
77  let callee_val ≝ map … (λr.hwreg_retrieve (\snd (regs …  st')) r)
78                    RegisterCalleeSaved in
79  return
80  (set_frms ERTL_state
81  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st))
82      «callee_val,length_map … ») :: frms)
83    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
84
85definition callee_values_ok : hw_register_env →
86   (Σl : list beval.|l| = |RegisterCalleeSaved|) → bool ≝
87λregs,l.
88foldl … andb true
89 (map2 … (λr : Register.λbv :beval.eq_beval (hwreg_retrieve regs r) bv)
90  RegisterCalleeSaved l ?).
91@hide_prf >(pi2 … l) % qed.
92
93
94definition ertl_pop_frame:
95 ∀F. ∀globals. genv_gen F globals → ident →  state ERTL_state →
96   res (state ERTL_state × program_counter) ≝
97 λF,globals,ge,id,st.
98 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
99 match frms with
100 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
101 | cons hd tl ⇒
102   if callee_values_ok (\snd (regs … st)) (callee_values hd) then
103    let st' ≝ set_regs ERTL_state 〈(psd_reg_env hd), \snd (regs … st)〉
104       (set_frms ERTL_state tl st) in
105    ! 〈st'', pc〉 ← pop_ra … st' ;
106    if eq_block (funct_block hd) (pc_block pc) then
107      ! sp ← sp … st'' ;
108      ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
109      let framesize : Byte ≝ bitvector_of_nat 8 framesize in
110      let newsp ≝ shift_pointer … sp framesize in
111      OK … 〈set_sp … newsp st'', pc〉
112    else Error ? [MSG BlockInFramesCorrupted]
113   else Error ? [MSG BadRegister]
114 ].
115@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
116
117(*CSC: XXXX, for external functions only*)
118axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
119axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
120(* I think there should be a list beval in place of list val here
121  λvals.λ_.λst.
122  (* set all RegisterRets to 0 *)
123  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
124  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
125  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
126  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
127  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
128
129(*CSC: here we should use helper_def_store from Joint/semantics.ma,
130  but it is not visible *)
131definition ps_reg_store_status : register → beval → state ERTL_state →
132  res (state ERTL_state) ≝
133 λdst,v,st.
134  let env ≝ regs … st in
135  ! env' ← ps_reg_store dst v env ;
136  return set_regs ERTL_state env' st.
137
138
139definition ertl_setup_call : ∀F. ∀globals. genv_gen F globals →
140ident → state ERTL_state → res (state ERTL_state) ≝
141λF,globals,ge,id,st.
142  ! sp ← sp … st ;
143  ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
144  let framesize : Byte ≝ bitvector_of_nat 8 framesize in
145  let newsp ≝ neg_shift_pointer … sp framesize in
146  return set_sp … newsp st.
147@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
148 
149definition eval_ertl_seq:
150 ∀F. ∀globals. genv_gen F globals →
151  ertl_seq → ident → state ERTL_state →
152   res (state ERTL_state) ≝
153 λF,globals,ge,stm,id,st.
154 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
155 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
156   match stm with
157   [ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st].
158   
159(*
160definition eval_ertl_seq:
161 ∀F. ∀globals. genv_gen F globals →
162  ertl_seq → ident → state ERTL_state →
163   res (state ERTL_state) ≝
164 λF,globals,ge,stm,id,st.
165 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
166 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
167  match stm with
168   [ ertl_new_frame ⇒
169      ! sp ← sp … st ;
170      let newsp ≝ neg_shift_pointer … sp framesize in
171      return set_sp … newsp st
172   | ertl_del_frame ⇒
173      ! sp ← sp … st ;
174      let newsp ≝ shift_pointer … sp framesize in
175      return set_sp … newsp st
176   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
177   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  *)
178
179definition ERTL_sem_uns ≝ 
180λF. mk_sem_unserialized_params ERTL ?
181  (* st_pars            ≝ *) ERTL_state
182  (* acca_store_        ≝ *) ps_reg_store
183  (* acca_retrieve_     ≝ *) ps_reg_retrieve
184  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
185  (* accb_store_        ≝ *) ps_reg_store
186  (* accb_retrieve_     ≝ *) ps_reg_retrieve
187  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
188  (* dpl_store_         ≝ *) ps_reg_store
189  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
190  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
191  (* dph_store_         ≝ *) ps_reg_store
192  (* dph_retrieve_      ≝ *) ps_reg_retrieve
193  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
194  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
195  (* pair_reg_move_     ≝ *) ertl_eval_move
196  (* save_frame         ≝ *) ertl_save_frame
197  (* setup_call         ≝ *) (λgl,ge.λ_.λ_.λ_.λid,st.ertl_setup_call F gl ge id st)
198  (* fetch_external_args≝ *) ertl_fetch_external_args
199  (* set_result         ≝ *) ertl_set_result
200  (* call_args_for_main ≝ *) 0
201  (* call_dest_for_main ≝ *) it
202  (* read_result        ≝ *) (λ_.λ_.λ_.
203     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
204  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
205  (* pop_frame          ≝ *) (λglobals,ge,id.λ_.λst.ertl_pop_frame F globals ge id st).
206
207definition ERTL_semantics ≝
208  mk_sem_graph_params ERTL ERTL_sem_uns ERTL_premain.
Note: See TracBrowser for help on using the repository browser.