source: src/ERTL/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.2 KB
Line 
1include "joint/semanticsUtils_paolo.ma".
2include "ERTL/ERTL_paolo.ma". (* CSC: syntax.ma in RTLabs *)
3include alias "common/Identifiers.ma".
4
5record ertl_psd_env : Type[0] ≝
6  { psd_regs : register_env beval
7  (* this tells what pseudo-registers should have their value corrected by spilled_no *)
8  ; need_spilled_no : identifier_set RegisterTag
9  }.
10
11definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
12definition add_need_spilled_no ≝
13  λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
14definition rm_need_spilled_no ≝
15  λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
16
17definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
18
19definition ps_reg_store ≝
20 λr,v.λlocal_env : ertl_reg_env.
21  do res ← reg_store r v (psd_regs (\fst local_env)) ;
22  let psd_env ≝ set_psd_regs res (\fst local_env) in
23  OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.
24
25definition ps_reg_retrieve ≝
26 λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
27
28definition hw_reg_store ≝
29 λr,v.λlocal_env:ertl_reg_env.
30  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
31
32definition hw_reg_retrieve ≝
33 λlocal_env:ertl_reg_env.λreg.
34  OK … (hwreg_retrieve … (\snd local_env) reg).
35
36definition ps_arg_retrieve ≝
37  λlocal_env,a.
38  match a with
39  [ Reg r ⇒ ps_reg_retrieve local_env r
40  | Imm b ⇒ return b
41  ].
42
43definition ERTL_state : sem_state_params ≝
44  mk_sem_state_params
45 (* framesT ≝ *) (list ertl_psd_env)
46 (* empty_framesT ≝ *) [ ]
47 (* regsT ≝ *) ertl_reg_env
48 (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉).
49
50(* we ignore need_spilled_no as we never move framesize based values around in the
51   translation *)
52definition ertl_eval_move ≝ λenv,pr.
53      ! v ←
54        match \snd pr with
55        [ Reg src ⇒
56          match src with
57          [ PSD r ⇒ ps_reg_retrieve env r
58          | HDW r ⇒ hw_reg_retrieve env r
59          ]
60        | Imm bv ⇒ return bv ] ;
61      match \fst pr with
62      [ PSD r ⇒ ps_reg_store r v env
63      | HDW r ⇒ hw_reg_store r v env
64      ].
65
66definition ertl_allocate_local ≝
67  λreg.λlenv : ertl_reg_env.
68  〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
69
70definition ertl_save_frame:
71 cpointer → unit → state … ERTL_state → res (state … ERTL_state) ≝
72 λpc.λ_.λst.
73  do st ← save_ra … st pc ;
74  OK …
75   (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
76    (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
77
78(*CSC: XXXX, for external functions only*)
79axiom ertl_fetch_external_args: external_function → state ERTL_state → res (list val).
80axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
81(* I think there should be a list beval in place of list val here
82  λvals.λ_.λst.
83  (* set all RegisterRets to 0 *)
84  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
85  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
86  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
87  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
88  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
89
90definition xdata_pointer_of_address: address → res xpointer ≝
91λp.let 〈v1,v2〉 ≝ p in
92! p ← pointer_of_bevals [v1;v2] ;
93match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
94[ XData ⇒ λE.OK ? (mk_Sig … p E)
95| _ ⇒ λ_.Error … [MSG BadPointer]
96] (refl …).
97
98definition address_of_xdata_pointer: xpointer → address ≝
99λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
100
101definition get_hwsp : ERTL_state → res xpointer ≝
102 λst.
103  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
104  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
105  xdata_pointer_of_address 〈spl,sph〉.
106
107definition set_hwsp : xpointer → ERTL_state → ERTL_state ≝
108 λsp,st.
109  let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
110  let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
111  let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
112  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
113
114definition eval_ertl_seq:
115 ∀globals. genv ERTL globals →
116  ertl_seq → joint_internal_function ERTL globals → ERTL_state →
117   IO io_out io_in ERTL_state ≝
118 λglobals,ge,stm,curr_fn,st.
119 let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
120  match stm with
121   [ ertl_new_frame ⇒
122      ! sp ← get_hwsp st ;
123      let newsp ≝ shift_pointer … sp framesize in
124      return set_hwsp newsp st
125   | ertl_del_frame ⇒
126      ! sp ← get_hwsp st ;
127      let newsp ≝ shift_pointer … sp framesize in
128      return set_hwsp newsp st
129   | ertl_frame_size dst ⇒
130      let env ≝ regs … st in
131      ! env' ← ps_reg_store dst (BVByte framesize) env ;
132      let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
133      return set_regs ERTL_state env'' st
134   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
135
136definition ertl_post_op2 ≝
137  λop,dst,arg1,arg2,st.
138  let local_env ≝ regs ERTL_state st in
139  let f ≝ λarg,st.match arg with
140     [ Reg r ⇒
141       if r ∈ need_spilled_no (\fst local_env) then
142         set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
143       else
144         st
145     | _ ⇒ st
146     ] in
147  match op with
148  [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
149  | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
150  | Sub ⇒ f arg1 st
151  | _ ⇒ st].
152         
153
154definition ERTL_semantics ≝
155  make_sem_graph_params ERTL
156  (mk_more_sem_unserialized_params ??
157  (* st_pars            ≝ *) ERTL_state
158  (* acca_store_        ≝ *) ps_reg_store
159  (* acca_retrieve_     ≝ *) ps_reg_retrieve
160  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
161  (* accb_store_        ≝ *) ps_reg_store
162  (* accb_retrieve_     ≝ *) ps_reg_retrieve
163  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
164  (* dpl_store_         ≝ *) ps_reg_store
165  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
166  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
167  (* dph_store_         ≝ *) ps_reg_store
168  (* dph_retrieve_      ≝ *) ps_reg_retrieve
169  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
170  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
171  (* pair_reg_move_     ≝ *) ertl_eval_move
172  (* fetch_ra           ≝ *) (load_ra …)
173  (* allocate_local     ≝ *) ertl_allocate_local
174  (* save_frame         ≝ *) ertl_save_frame
175  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
176  (* fetch_external_args≝ *) ertl_fetch_external_args
177  (* set_result         ≝ *) ertl_set_result
178  (* call_args_for_main ≝ *) 0
179  (* call_dest_for_main ≝ *) it
180  (* read_result        ≝ *) (λ_.λ_.λ_.
181     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
182  (* eval_ext_seq       ≝ *) eval_ertl_seq
183  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
184  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
185  (* pop_frame          ≝ *) (λ_.λ_.λ_.λst.return st)
186  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)).
Note: See TracBrowser for help on using the repository browser.