source: src/ERTL/semantics.ma @ 2564

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

ERTL fully repaired, useless part of return value of pop_ra
removed.

File size: 7.2 KB
Line 
1include "joint/semanticsUtils.ma".
2include "ERTL/ERTL.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: ? → ? → ? → res ? ≝
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
36
37definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
38  λlocal_env,a.
39  match a with
40  [ Reg r ⇒ ps_reg_retrieve local_env r
41  | Imm b ⇒ return BVByte b
42  ].
43
44
45
46definition ERTL_state : sem_state_params ≝
47  mk_sem_state_params
48 (* framesT ≝ *) (list ertl_psd_env)
49 (* empty_framesT ≝ *) [ ]
50 (* regsT ≝ *) ertl_reg_env
51 (* empty_regsT ≝ *) (λsp.〈mk_ertl_psd_env (empty_map …) ∅,init_hw_register_env sp〉)
52 (*load_sp ≝ *) ?
53  (*save_sp ≝ *) ?. cases daemon qed.
54
55(* we ignore need_spilled_no as we never move framesize based values around in the
56   translation *)
57definition ertl_eval_move ≝ λenv,pr.
58      ! v ←
59        match \snd pr with
60        [ Reg src ⇒
61          match src with
62          [ PSD r ⇒ ps_reg_retrieve env r
63          | HDW r ⇒ hw_reg_retrieve env r
64          ]
65        | Imm b ⇒ return BVByte b ] ;
66      match \fst pr with
67      [ PSD r ⇒ ps_reg_store r v env
68      | HDW r ⇒ hw_reg_store r v env
69      ].
70
71definition ertl_allocate_local ≝
72  λreg.λlenv : ertl_reg_env.
73  〈set_psd_regs (add … (psd_regs (\fst lenv)) reg BVundef) (\fst lenv), \snd lenv〉.
74
75definition ertl_save_frame:
76 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
77 λ_.λ_.λst.
78  do st ← push_ra … st (pc … st) ;
79  OK …
80   (set_frms ERTL_state (\fst (regs ERTL_state st) :: (st_frms … st))
81    (set_regs ERTL_state 〈mk_ertl_psd_env (empty_map …) ∅,\snd (regs … st)〉 st)).
82
83(*CSC: XXXX, for external functions only*)
84axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
85axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
86(* I think there should be a list beval in place of list val here
87  λvals.λ_.λst.
88  (* set all RegisterRets to 0 *)
89  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
90  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
91  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
92  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
93  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
94
95definition xdata_pointer_of_address: address → res xpointer ≝
96λp.let 〈v1,v2〉 ≝ p in
97! p ← pointer_of_bevals [v1;v2] ;
98match ptype p return λpty. ptype p = pty → res (Σp:pointer. ptype p = XData) with
99[ XData ⇒ λE.OK ? (mk_Sig … p E)
100| _ ⇒ λ_.Error … [MSG BadPointer]
101] (refl …).
102
103definition address_of_xdata_pointer: xpointer → address ≝
104λp.list_to_pair … (bevals_of_pointer p) ?. % qed.
105
106definition get_hwsp : state ERTL_state → res xpointer ≝
107 λst.
108  let spl ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPL in
109  let sph ≝ hwreg_retrieve (\snd (regs … st)) RegisterSPH in
110  xdata_pointer_of_address 〈spl,sph〉.
111
112definition set_hwsp : xpointer → state ERTL_state → state ERTL_state ≝
113 λsp,st.
114  let 〈spl,sph〉 ≝ address_of_xdata_pointer sp in
115  let hwregs ≝ hwreg_store RegisterSPL spl (\snd (regs … st)) in
116  let hwregs ≝ hwreg_store RegisterSPH sph hwregs in
117  set_regs ERTL_state 〈\fst (regs … st),hwregs〉 st.
118
119axiom FunctionNotFound: errmsg.
120
121definition eval_ertl_seq:
122 ∀F. ∀globals. genv_gen F globals →
123  ertl_seq → ident → state ERTL_state →
124   res (state ERTL_state) ≝
125 λF,globals,ge,stm,id,st.
126 ! framesize ← opt_to_res … FunctionNotFound  (stack_sizes … ge id);
127 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
128  match stm with
129   [ ertl_new_frame ⇒
130      ! sp ← get_hwsp st ;
131      let newsp ≝ shift_pointer … sp framesize in
132      return set_hwsp newsp st
133   | ertl_del_frame ⇒
134      ! sp ← get_hwsp st ;
135      let newsp ≝ shift_pointer … sp framesize in
136      return set_hwsp newsp st
137   | ertl_frame_size dst ⇒
138      let env ≝ regs … st in
139      ! env' ← ps_reg_store dst (BVByte framesize) env ;
140      let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
141      return set_regs ERTL_state env'' st
142   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
143
144definition ertl_post_op2 ≝
145  λop,dst,arg1,arg2,st.
146  let local_env ≝ regs ERTL_state st in
147  let f ≝ λarg,st.match arg with
148     [ Reg r ⇒
149       if r ∈ need_spilled_no (\fst local_env) then
150         set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
151       else
152         st
153     | _ ⇒ st
154     ] in
155  match op with
156  [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
157  | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
158  | Sub ⇒ f arg1 st
159  | _ ⇒ st].
160         
161definition ERTL_semantics ≝
162  make_sem_graph_params ERTL
163  (λF. mk_sem_unserialized_params ??
164  (* st_pars            ≝ *) ERTL_state
165  (* acca_store_        ≝ *) ps_reg_store
166  (* acca_retrieve_     ≝ *) ps_reg_retrieve
167  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
168  (* accb_store_        ≝ *) ps_reg_store
169  (* accb_retrieve_     ≝ *) ps_reg_retrieve
170  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
171  (* dpl_store_         ≝ *) ps_reg_store
172  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
173  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
174  (* dph_store_         ≝ *) ps_reg_store
175  (* dph_retrieve_      ≝ *) ps_reg_retrieve
176  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
177  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
178  (* pair_reg_move_     ≝ *) ertl_eval_move
179  (* allocate_local     ≝ *) ertl_allocate_local
180  (* save_frame         ≝ *) ertl_save_frame
181  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
182  (* fetch_external_args≝ *) ertl_fetch_external_args
183  (* set_result         ≝ *) ertl_set_result
184  (* call_args_for_main ≝ *) 0
185  (* call_dest_for_main ≝ *) it
186  (* read_result        ≝ *) (λ_.λ_.λ_.
187     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
188  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.λ_.eval_ertl_seq F gl ge stm id)
189  (* pop_frame          ≝ *) (λ_.λ_.λ_.λ_.pop_ra …)).
Note: See TracBrowser for help on using the repository browser.