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
RevLine 
[2563]1include "joint/semanticsUtils.ma".
[1302]2include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
[1359]3include alias "common/Identifiers.ma".
[1130]4
[2590]5definition ertl_reg_env ≝ register_env beval × hw_register_env.
[2286]6
[2563]7definition ps_reg_store: ? → ? → ? → res ? ≝
[2286]8 λr,v.λlocal_env : ertl_reg_env.
[2796]9  let res ≝ reg_store r v (\fst local_env) in
[2590]10  OK … 〈res, \snd local_env〉.
[1130]11
[1302]12definition ps_reg_retrieve ≝
[2590]13 λlocal_env:ertl_reg_env. reg_retrieve … (\fst local_env).
[1130]14
[1302]15definition hw_reg_store ≝
[2286]16 λr,v.λlocal_env:ertl_reg_env.
[1415]17  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
[1130]18
[1302]19definition hw_reg_retrieve ≝
[2286]20 λlocal_env:ertl_reg_env.λreg.
[1415]21  OK … (hwreg_retrieve … (\snd local_env) reg).
[1302]22
[2563]23
24definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
[2286]25  λlocal_env,a.
26  match a with
27  [ Reg r ⇒ ps_reg_retrieve local_env r
[2563]28  | Imm b ⇒ return BVByte b
[2286]29  ].
[1302]30
[2590]31definition get_hwsp : ertl_reg_env → res xpointer ≝
32 λst.hwreg_retrieve_sp (\snd st).
[2563]33
[2590]34definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
35 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.
[3259]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}.
[2563]42
[2286]43definition ERTL_state : sem_state_params ≝
44  mk_sem_state_params
[3259]45 (* framesT ≝ *) (list (ERTL_frame))
[2286]46 (* empty_framesT ≝ *) [ ]
47 (* regsT ≝ *) ertl_reg_env
[2946]48 (* empty_regsT ≝ *) (λsp.〈empty_map …, init_hw_register_env sp〉)
[2590]49 (*load_sp ≝ *) get_hwsp
50 (*save_sp ≝ *) set_hwsp.
[1313]51
[2286]52(* we ignore need_spilled_no as we never move framesize based values around in the
53   translation *)
[3259]54definition ertl_eval_move ≝ λenv.λpr : move_dst × move_src.
[2286]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          ]
[2563]62        | Imm b ⇒ return BVByte b ] ;
[2286]63      match \fst pr with
64      [ PSD r ⇒ ps_reg_store r v env
65      | HDW r ⇒ hw_reg_store r v env
66      ].
[1318]67
[2286]68definition ertl_allocate_local ≝
69  λreg.λlenv : ertl_reg_env.
[2590]70  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
[2286]71
[1377]72definition ertl_save_frame:
[2783]73 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
74 λ_.λ_.λst.
75  ! st' ← push_ra … st (pc … st) ;
[2801]76  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
[3259]77  let callee_val ≝ map … (λr.hwreg_retrieve (\snd (regs …  st')) r)
78                    RegisterCalleeSaved in
[2783]79  return
80  (set_frms ERTL_state
[3259]81  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st))
82      «callee_val,length_map … ») :: frms)
[2783]83    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
[1318]84
[3259]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
[2783]94definition ertl_pop_frame:
[3259]95 ∀F. ∀globals. genv_gen F globals → ident →  state ERTL_state →
[2783]96   res (state ERTL_state × program_counter) ≝
[3259]97 λF,globals,ge,id,st.
[2783]98 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
99 match frms with
100 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
101 | cons hd tl ⇒
[3259]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]
[2783]114 ].
[3259]115@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
[2783]116
[1302]117(*CSC: XXXX, for external functions only*)
[2563]118axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
[2286]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).*)
[1302]128
[2566]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 ;
[2590]136  return set_regs ERTL_state env' st.
[2566]137
[3259]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 
[2286]149definition eval_ertl_seq:
[2564]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.
[2807]154 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
[2564]155 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
[3259]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
[1327]167  match stm with
[2286]168   [ ertl_new_frame ⇒
[2590]169      ! sp ← sp … st ;
[2823]170      let newsp ≝ neg_shift_pointer … sp framesize in
[2590]171      return set_sp … newsp st
[2286]172   | ertl_del_frame ⇒
[2590]173      ! sp ← sp … st ;
[2286]174      let newsp ≝ shift_pointer … sp framesize in
[2590]175      return set_sp … newsp st
[2566]176   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
[3259]177   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  *)
[2666]178
179definition ERTL_sem_uns ≝ 
180λF. mk_sem_unserialized_params ERTL ?
[2286]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
[3259]197  (* setup_call         ≝ *) (λgl,ge.λ_.λ_.λ_.λid,st.ertl_setup_call F gl ge id st)
[2286]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)
[2796]204  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
[3259]205  (* pop_frame          ≝ *) (λglobals,ge,id.λ_.λst.ertl_pop_frame F globals ge id st).
[2674]206
[2666]207definition ERTL_semantics ≝
[2946]208  mk_sem_graph_params ERTL ERTL_sem_uns ERTL_premain.
Note: See TracBrowser for help on using the repository browser.