source: src/ERTL/ERTL_semantics.ma

Last change on this file was 3371, checked in by piccolo, 6 years ago

Modified RTLsemantics and ERTLsemantics. Now the pop frame will set
to undef the carry bit and all RegisterCallerSaved? exept those used to
pass the return value of a function.

Added an overflow check in ERTL_semantics

File size: 9.3 KB
Line 
1include "joint/semanticsUtils.ma".
2include "ERTL/ERTL.ma". (* CSC: syntax.ma in RTLabs *)
3include alias "common/Identifiers.ma".
4
5definition ertl_reg_env ≝ register_env beval × hw_register_env.
6
7definition ps_reg_store: ? → ? → ? → res ? ≝
8 λr,v.λlocal_env : ertl_reg_env.
9  let res ≝ reg_store r v (\fst local_env) in
10  OK … 〈res, \snd local_env〉.
11
12definition ps_reg_retrieve ≝
13 λlocal_env:ertl_reg_env. reg_retrieve … (\fst local_env).
14
15definition hw_reg_store ≝
16 λr,v.λlocal_env:ertl_reg_env.
17  OK … 〈\fst local_env,hwreg_store r v (\snd local_env)〉.
18
19definition hw_reg_retrieve ≝
20 λlocal_env:ertl_reg_env.λreg.
21  OK … (hwreg_retrieve … (\snd local_env) reg).
22
23
24definition ps_arg_retrieve : ertl_reg_env → argument ? → res beval ≝
25  λlocal_env,a.
26  match a with
27  [ Reg r ⇒ ps_reg_retrieve local_env r
28  | Imm b ⇒ return BVByte b
29  ].
30
31definition get_hwsp : ertl_reg_env → res xpointer ≝
32 λst.hwreg_retrieve_sp (\snd st).
33
34definition set_hwsp : ertl_reg_env → xpointer → ertl_reg_env ≝
35 λst,sp.〈\fst st, hwreg_store_sp (\snd st) sp〉.
36 
37record ERTL_frame : Type[0] ≝
38{ psd_reg_env : register_env beval
39; funct_pc : program_counter
40; funct_sp : xpointer (* just for correctness *)
41}.
42
43definition ERTL_state : sem_state_params ≝
44  mk_sem_state_params
45 (* framesT ≝ *) (list (ERTL_frame))
46 (* empty_framesT ≝ *) [ ]
47 (* regsT ≝ *) ertl_reg_env
48 (* empty_regsT ≝ *) (λsp.〈empty_map …, init_hw_register_env sp〉)
49 (*load_sp ≝ *) get_hwsp
50 (*save_sp ≝ *) set_hwsp.
51 
52(* when the stack is unique, the stack block is already present in the state
53   that we are analysing.
54   If the ptr's block is not it, we suppose
55   it's pointing to a global and we accept it. *)
56definition ERTL_validate_pointer : ∀F. ∀globals. genv_gen F globals →
57  ident → state ERTL_state → pointer → res unit ≝
58λF,globals,ge,curr_id,st,ptr.
59! sp ← sp … st ;
60if eq_block (pblock ptr) (pblock sp) then
61  let off ≝
62    λsp : pointer.Z_of_unsigned_bitvector … (offv (poff ptr)) -
63        Z_of_unsigned_bitvector … (offv (poff sp)) in
64  ! bl ← opt_to_res … [MSG BadFunction; CTX … curr_id]
65    (! bl ← find_symbol … ge curr_id ; code_block_of_block bl) ;
66  ! 〈ign, f〉 ← fetch_internal_function … ge bl ;
67  ! ss ← opt_to_res ? [MSG BadFunction; CTX … curr_id ] (stack_sizes … ge curr_id) ;
68  let o' ≝ off sp in
69  if (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
70     Zltb o' (minus ss (get_joint_if_params_stacksize … ge f))) ∨
71    Zleb ss o' then
72    Error … (msg BadPointer)
73  else
74    ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
75    m_fold ??? (λfr.λ_.
76      ! 〈ign, f〉 ← fetch_internal_function … ge (pc_block (funct_pc fr)) ;
77      let o' ≝ off (funct_sp fr) in
78      if Zleb (get_joint_if_local_stacksize … ge f) o' ∧
79         Zltb o' (minus ss (get_joint_if_params_stacksize … ge f)) then
80        Error … (msg BadPointer)
81      else return it) frms it
82else return it.
83
84(* we ignore need_spilled_no as we never move framesize based values around in the
85   translation *)
86definition ertl_eval_move ≝ λenv.λpr : move_dst × move_src.
87      ! v ←
88        match \snd pr with
89        [ Reg src ⇒
90          match src with
91          [ PSD r ⇒ ps_reg_retrieve env r
92          | HDW r ⇒ hw_reg_retrieve env r
93          ]
94        | Imm b ⇒ return BVByte b ] ;
95      match \fst pr with
96      [ PSD r ⇒ ps_reg_store r v env
97      | HDW r ⇒ hw_reg_store r v env
98      ].
99
100definition ertl_allocate_local ≝
101  λreg.λlenv : ertl_reg_env.
102  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
103
104definition ertl_save_frame:
105 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
106 λ_.λ_.λst.
107  ! st' ← push_ra … st (pc … st) ;
108  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
109  ! sp ← sp … st ;
110  return
111  (set_frms ERTL_state
112  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc ? st) sp) :: frms)
113    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
114
115(* Paolo: maybe insert a check that stack pointer is restored after return? *)
116definition ertl_pop_frame:
117 ∀F. ∀globals. genv_gen F globals → ident →  state ERTL_state →
118   res (state ERTL_state × program_counter) ≝
119 λF,globals,ge,id,st.
120 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
121 match frms with
122 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
123 | cons hd tl ⇒
124    let st' ≝ set_regs ERTL_state 〈(psd_reg_env hd), \snd (regs … st)〉
125       (set_frms ERTL_state tl st) in
126    ! 〈st'', pc〉 ← pop_ra … st' ;
127    if eq_program_counter (funct_pc hd) pc then
128      ! sp ← sp … st'' ;
129      ! framesize ← opt_to_res ? (msg FunctionNotFound) (stack_sizes … ge id);
130      let framesize : Byte ≝ bitvector_of_nat 8 framesize in
131      let newsp ≝ shift_pointer … sp framesize in
132      let cs_regs : hw_register_env ≝
133        foldl ?? (λregs,r.hwreg_store r BVundef regs) (\snd (regs …st''))
134          (filter ? (λr.all … (λx.¬ eq_Register r x) RegisterRets)  RegisterCallerSaved)
135       in
136      OK … 〈set_sp ? newsp (set_regs ERTL_state 〈\fst (regs … st''),cs_regs〉
137                            (set_carry ? BBundef st'')), pc〉
138    else Error ? [MSG BlockInFramesCorrupted]
139 ].
140@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
141
142(*CSC: XXXX, for external functions only*)
143axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
144axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
145(* I think there should be a list beval in place of list val here
146  λvals.λ_.λst.
147  (* set all RegisterRets to 0 *)
148  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
149  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
150  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
151  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
152  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
153
154(*CSC: here we should use helper_def_store from Joint/semantics.ma,
155  but it is not visible *)
156definition ps_reg_store_status : register → beval → state ERTL_state →
157  res (state ERTL_state) ≝
158 λdst,v,st.
159  let env ≝ regs … st in
160  ! env' ← ps_reg_store dst v env ;
161  return set_regs ERTL_state env' st.
162
163include alias "arithmetics/nat.ma".
164
165definition ertl_setup_call : ℕ → state ERTL_state → res (state ERTL_state) ≝
166λframesize,st.
167  ! sp ← sp … st ;
168  if leb (S (framesize + (stack_usage … st))) (2^16) then
169   let framesize : Byte ≝ bitvector_of_nat 8 framesize in
170   let newsp ≝ neg_shift_pointer … sp framesize in
171   return set_sp … newsp st
172  else
173   Error … [MSG StackOverflow].
174@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
175 
176definition eval_ertl_seq:
177 ∀F. ∀globals. genv_gen F globals →
178  ertl_seq → ident → state ERTL_state →
179   res (state ERTL_state) ≝
180 λF,globals,ge,stm,id,st.
181 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
182 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
183   match stm with
184   [ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st].
185   
186(*
187definition eval_ertl_seq:
188 ∀F. ∀globals. genv_gen F globals →
189  ertl_seq → ident → state ERTL_state →
190   res (state ERTL_state) ≝
191 λF,globals,ge,stm,id,st.
192 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
193 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
194  match stm with
195   [ ertl_new_frame ⇒
196      ! sp ← sp … st ;
197      let newsp ≝ neg_shift_pointer … sp framesize in
198      return set_sp … newsp st
199   | ertl_del_frame ⇒
200      ! sp ← sp … st ;
201      let newsp ≝ shift_pointer … sp framesize in
202      return set_sp … newsp st
203   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
204   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  *)
205
206definition ERTL_sem_uns ≝ 
207λF. mk_sem_unserialized_params ERTL ?
208  (* st_pars            ≝ *) ERTL_state
209  (* acca_store_        ≝ *) ps_reg_store
210  (* acca_retrieve_     ≝ *) ps_reg_retrieve
211  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
212  (* accb_store_        ≝ *) ps_reg_store
213  (* accb_retrieve_     ≝ *) ps_reg_retrieve
214  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
215  (* dpl_store_         ≝ *) ps_reg_store
216  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
217  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
218  (* dph_store_         ≝ *) ps_reg_store
219  (* dph_retrieve_      ≝ *) ps_reg_retrieve
220  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
221  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
222  (* pair_reg_move_     ≝ *) ertl_eval_move
223  (* save_frame         ≝ *) ertl_save_frame
224  (* setup_call         ≝ *) (λn.λ_.λ_.λst.ertl_setup_call n st)
225  (* fetch_external_args≝ *) ertl_fetch_external_args
226  (* set_result         ≝ *) ertl_set_result
227  (* call_args_for_main ≝ *) 0
228  (* call_dest_for_main ≝ *) it
229  (* read_result        ≝ *) (λ_.λ_.λ_.
230     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
231  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
232  (* pop_frame          ≝ *) (λglobals,ge,id.λ_.λst.ertl_pop_frame F globals ge id st)
233  (* validate_pointer   ≝ *) (ERTL_validate_pointer …).
234
235definition ERTL_semantics ≝
236  mk_sem_graph_params ERTL ERTL_sem_uns ERTL_premain.
Note: See TracBrowser for help on using the repository browser.