source: src/ERTL/semantics.ma @ 2563

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

Repairing ERTL: show stopper found.

File size: 7.5 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
119definition eval_ertl_seq:
120 ∀globals. genv ERTL globals →
121  ertl_seq → ident → joint_internal_function ERTL globals → state ERTL_state →
122   IO io_out io_in (state ERTL_state) ≝
123 λglobals,ge,stm,id,curr_fn,st.
124 let framesize : Byte ≝ bitvector_of_nat 8 (joint_if_stacksize … curr_fn) in
125  match stm with
126   [ ertl_new_frame ⇒
127      ! sp ← get_hwsp st ;
128      let newsp ≝ shift_pointer … sp framesize in
129      return set_hwsp newsp st
130   | ertl_del_frame ⇒
131      ! sp ← get_hwsp st ;
132      let newsp ≝ shift_pointer … sp framesize in
133      return set_hwsp newsp st
134   | ertl_frame_size dst ⇒
135      let env ≝ regs … st in
136      ! env' ← ps_reg_store dst (BVByte framesize) env ;
137      let env'' ≝ 〈add_need_spilled_no dst (\fst env'), \snd env'〉 in
138      return set_regs ERTL_state env'' st
139   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed. 
140
141definition ertl_post_op2 ≝
142  λop,dst,arg1,arg2,st.
143  let local_env ≝ regs ERTL_state st in
144  let f ≝ λarg,st.match arg with
145     [ Reg r ⇒
146       if r ∈ need_spilled_no (\fst local_env) then
147         set_regs ERTL_state 〈add_need_spilled_no dst (\fst local_env),\snd local_env〉 st
148       else
149         st
150     | _ ⇒ st
151     ] in
152  match op with
153  [ Add ⇒ f arg1 (f arg2 st) (* won't happen both *)
154  | Addc ⇒ f arg1 (f arg2 st) (* we have to think about what should we do with carry bit *)
155  | Sub ⇒ f arg1 st
156  | _ ⇒ st].
157         
158definition ERTL_semantics ≝
159  make_sem_graph_params ERTL
160  (λF. mk_sem_unserialized_params ??
161  (* st_pars            ≝ *) ERTL_state
162  (* acca_store_        ≝ *) ps_reg_store
163  (* acca_retrieve_     ≝ *) ps_reg_retrieve
164  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
165  (* accb_store_        ≝ *) ps_reg_store
166  (* accb_retrieve_     ≝ *) ps_reg_retrieve
167  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
168  (* dpl_store_         ≝ *) ps_reg_store
169  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
170  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
171  (* dph_store_         ≝ *) ps_reg_store
172  (* dph_retrieve_      ≝ *) ps_reg_retrieve
173  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
174  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
175  (* pair_reg_move_     ≝ *) ertl_eval_move
176(*  (* fetch_ra           ≝ *) ?(*(pop_ra …)*) *)
177  (* allocate_local     ≝ *) ertl_allocate_local
178  (* save_frame         ≝ *) ertl_save_frame
179  (* setup_call         ≝ *) (λ_.λ_.λ_.λst.return st)
180  (* fetch_external_args≝ *) ertl_fetch_external_args
181  (* set_result         ≝ *) ertl_set_result
182  (* call_args_for_main ≝ *) 0
183  (* call_dest_for_main ≝ *) it
184  (* read_result        ≝ *) (λ_.λ_.λ_.
185     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
186  (* eval_ext_seq       ≝ *) ?(*eval_ertl_seq*)
187(*  (* eval_ext_tailcall  ≝ *) (λ_.λ_.λabs.match abs in void with [ ])
188  (* eval_ext_call      ≝ *) (λ_.λ_.λabs.match abs in void with [ ]) *)
189  (* pop_frame          ≝ *) ?(*(λ_.λ_.?(*return st_no_pc ? st*))*)
190(*  (* post_op2           ≝ *) (λ_.λ_.ertl_post_op2)) *)).
191[ (* pop_frame *) cases daemon (* Handle last-popped correctly *)
192| @eval_ertl_seq (* Handle type of call *)
193]
Note: See TracBrowser for help on using the repository browser.