source: src/ERTLptr/semantics.ma @ 2566

Last change on this file since 2566 was 2566, checked in by piccolo, 8 years ago

ERTL to ERTLptr pass implemented up to a few things to be
left to the infrastructure (marked with PAOLO)

File size: 7.5 KB
Line 
1include "joint/semanticsUtils.ma".
2include "ERTLptr/ERTLptr.ma". (* CSC: syntax.ma in RTLabs *)
3include "ERTL/semantics.ma".
4include "common/extraGlobalenvs.ma".
5include alias "common/Identifiers.ma".
6(*
7record ertl_psd_env : Type[0] ≝
8  { psd_regs : register_env beval
9  (* this tells what pseudo-registers should have their value corrected by spilled_no *)
10  ; need_spilled_no : identifier_set RegisterTag
11  }.
12
13definition set_psd_regs ≝ λx,env.mk_ertl_psd_env x (need_spilled_no env).
14definition add_need_spilled_no ≝
15  λr,env.mk_ertl_psd_env (psd_regs env) (add_set … (need_spilled_no env) r).
16definition rm_need_spilled_no ≝
17  λr,env.mk_ertl_psd_env (psd_regs env) (need_spilled_no env ∖  {(r)}).
18
19definition ertl_reg_env ≝ ertl_psd_env × hw_register_env.
20
21definition ps_reg_store: ? → ? → ? → res ? ≝
22 λr,v.λlocal_env : ertl_reg_env.
23  do res ← reg_store r v (psd_regs (\fst local_env)) ;
24  let psd_env ≝ set_psd_regs res (\fst local_env) in
25  OK … 〈rm_need_spilled_no r psd_env, \snd local_env〉.
26
27definition ps_reg_retrieve ≝
28 λlocal_env:ertl_reg_env. reg_retrieve … (psd_regs (\fst local_env)).
29
30definition hw_reg_store ≝
31 λr,v.λlocal_env:ertl_reg_env.
32  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
33
34definition hw_reg_retrieve ≝
35 λlocal_env:ertl_reg_env.λreg.
36  OK … (hwreg_retrieve … (\snd local_env) reg).
37
38
39definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
40  λlocal_env,a.
41  match a with
42  [ Reg r ⇒ ps_reg_retrieve local_env r
43  | Imm b ⇒ return BVByte b
44  ].
45
46
47
48definition ERTL_state : sem_state_params ≝
49  mk_sem_state_params
50 (* framesT ≝ *) (list ertl_psd_env)
51 (* empty_framesT ≝ *) [ ]
52 (* regsT ≝ *) ertl_reg_env
53 (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉)
54 (*load_sp ≝ *) ?
55  (*save_sp ≝ *) ?. cases daemon qed.
56
57(* we ignore need_spilled_no as we never move framesize based values around in the
58   translation *)
59definition ertl_eval_move ≝ λenv,pr.
60      ! v ←
61        match \snd pr with
62        [ Reg src ⇒
63          match src with
64          [ PSD r ⇒ ps_reg_retrieve env r
65          | HDW r ⇒ hw_reg_retrieve env r
66          ]
67        | Imm b ⇒ return BVByte b ] ;
68      match \fst pr with
69      [ PSD r ⇒ ps_reg_store r v env
70      | HDW r ⇒ hw_reg_store r v env
71      ].
72
73definition ertl_allocate_local ≝
74  λreg.λlenv : ertl_reg_env.
75  〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
76*)
77
78definition ertlptr_save_frame:
79 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
80 λk.λ_.λst.
81 do st ← match k with [ID ⇒ push_ra … st (pc … st) |
82 PTR ⇒ return (st_no_pc … st)] ; OK …
83   (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
84    (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
85
86(*
87(*CSC: XXXX, for external functions only*)
88axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
89axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
90(* I think there should be a list beval in place of list val here
91  λvals.λ_.λst.
92  (* set all RegisterRets to 0 *)
93  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
94  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
95  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
96  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
97  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
98
99definition xdata_pointer_of_address: address → res xpointer ≝
100λp.let 〈v1,v2〉 ≝ p in
101! p ← pointer_of_bevals [v1;v2] ;
102match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
103[ XData ⇒ λE.OK ? (mk_Sig … p E)
104| _ ⇒ λ_.Error … [MSG BadPointer]
105] (refl …).
106
107definition address_of_xdata_pointer: xpointer → address ≝
108λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
109
110definition get_hwsp : state ERTL_state → res xpointer ≝
111 λst.
112  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
113  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
114  xdata_pointer_of_address 〈spl,sph〉.
115
116definition set_hwsp : xpointer → state ERTL_state → state ERTL_state ≝
117 λsp,st.
118  let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
119  let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
120  let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
121  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
122
123axiom FunctionNotFound: errmsg.*)
124
125definition eval_ertlptr_seq:
126 ∀F. ∀globals. genv_gen F globals →
127  ertlptr_seq → ident → state ERTL_state →
128   res (state ERTL_state) ≝
129 λF,globals,ge,stm,id,st.
130  match stm with
131   [ ertlptr_ertl seq ⇒ eval_ertl_seq F globals ge seq id st
132   | LOW_ADDRESS r l ⇒  ! pc_lab ←  (pc_of_label ?? ? (block_of_funct … ge id) l);
133                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
134                        ps_reg_store_status r addrl st
135   | HIGH_ADDRESS r l ⇒ ! pc_lab ←  (pc_of_label ?? ? (block_of_funct … ge id) l);
136                        let 〈addrl,addrh〉 ≝  beval_pair_of_pc pc_lab in
137                        ps_reg_store_status r addrh st
138   ].
139 [3,8: (* PAOLO, HELP: we should pass ge, but the type is abstracted over F! *)
140       cases daemon
141 |4,5,9,10: cases daemon (* Closed by side effect for 3,8 *)
142 |1,6: (* PAOLO, HELP: this should be an hypothesis that needs to propagate
143          a long way and then be discarded in Joint/semantics.ma *)
144       cases daemon
145 |2,7: @block_of_funct_ident_is_code ]
146qed.
147
148(*
149definition ertl_post_op2 ≝
150  λop,dst,arg1,arg2,st.
151  let local_env ≝ regs ERTL_state st in
152  let f ≝ λarg,st.match arg with
153     [ Reg r ⇒
154       if r ∈ need_spilled_no (\fst local_env) then
155         set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
156       else
157         st
158     | _ ⇒ st
159     ] in
160  match op with
161  [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
162  | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
163  | Sub ⇒ f arg1 st
164  | _ ⇒ st].
165*)
166
167definition ERTLptr_semantics ≝
168  make_sem_graph_params ERTLptr
169  (λF. mk_sem_unserialized_params ??
170  (* st_pars            ≝ *) ERTL_state
171  (* acca_store_        ≝ *) ps_reg_store
172  (* acca_retrieve_     ≝ *) ps_reg_retrieve
173  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
174  (* accb_store_        ≝ *) ps_reg_store
175  (* accb_retrieve_     ≝ *) ps_reg_retrieve
176  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
177  (* dpl_store_         ≝ *) ps_reg_store
178  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
179  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
180  (* dph_store_         ≝ *) ps_reg_store
181  (* dph_retrieve_      ≝ *) ps_reg_retrieve
182  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
183  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
184  (* pair_reg_move_     ≝ *) ertl_eval_move
185  (* allocate_local     ≝ *) ertl_allocate_local
186  (* save_frame         ≝ *) ertlptr_save_frame
187  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
188  (* fetch_external_args≝ *) ertl_fetch_external_args
189  (* set_result         ≝ *) ertl_set_result
190  (* call_args_for_main ≝ *) 0
191  (* call_dest_for_main ≝ *) it
192  (* read_result        ≝ *) (λ_.λ_.λ_.
193     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
194  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertlptr_seq F gl ge stm id)
195  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
Note: See TracBrowser for help on using the repository browser.