source: src/ERTL/ERTL_semantics.ma @ 3265

Last change on this file since 3265 was 3265, checked in by tranquil, 6 years ago

added validate_pointer filter
in Interference added that intereference only fires on non eliminable
statements

File size: 9.0 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_block : Σb:block.block_region b=Code
40; fr_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 Zltb o' 0 ∨
70    (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
71     Zltb o' (minus ss (get_joint_if_params_stacksize … ge f))) ∨
72    Zleb ss o' then
73    Error … (msg BadPointer)
74  else
75    ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
76    m_fold ??? (λfr.λ_.
77      ! 〈ign, f〉 ← fetch_internal_function … ge (funct_block fr) ;
78      let o' ≝ off (fr_sp fr) in
79      if Zltb o' 0 ∨
80        (Zleb (get_joint_if_local_stacksize … ge f) o' ∧
81         Zltb o' (minus ss (get_joint_if_params_stacksize … ge f))) ∨
82        Zleb ss o' then
83        Error … (msg BadPointer)
84      else return it) frms it
85else return it.
86
87(* we ignore need_spilled_no as we never move framesize based values around in the
88   translation *)
89definition ertl_eval_move ≝ λenv.λpr : move_dst × move_src.
90      ! v ←
91        match \snd pr with
92        [ Reg src ⇒
93          match src with
94          [ PSD r ⇒ ps_reg_retrieve env r
95          | HDW r ⇒ hw_reg_retrieve env r
96          ]
97        | Imm b ⇒ return BVByte b ] ;
98      match \fst pr with
99      [ PSD r ⇒ ps_reg_store r v env
100      | HDW r ⇒ hw_reg_store r v env
101      ].
102
103definition ertl_allocate_local ≝
104  λreg.λlenv : ertl_reg_env.
105  〈 add … (\fst lenv) reg BVundef, \snd lenv〉.
106
107definition ertl_save_frame:
108 call_kind → unit → state_pc ERTL_state → res (state … ERTL_state) ≝
109 λ_.λ_.λst.
110  ! st' ← push_ra … st (pc … st) ;
111  ! frms ← opt_to_res ? [MSG FrameErrorOnPush] (st_frms … st');
112  ! sp ← sp … st ;
113  return
114  (set_frms ERTL_state
115  ((mk_ERTL_frame (\fst (regs ERTL_state st')) (pc_block (pc ? st)) sp) :: frms)
116    (set_regs ERTL_state 〈empty_map …,\snd (regs … st')〉 st')).
117
118(* Paolo: maybe insert a check that stack pointer is restored after return? *)
119definition ertl_pop_frame:
120 ∀F. ∀globals. genv_gen F globals → ident →  state ERTL_state →
121   res (state ERTL_state × program_counter) ≝
122 λF,globals,ge,id,st.
123 ! frms ← opt_to_res ? [MSG FrameErrorOnPop] (st_frms … st);
124 match frms with
125 [ nil ⇒ Error ? [MSG FramesEmptyOnPop]
126 | cons hd tl ⇒
127    let st' ≝ set_regs ERTL_state 〈(psd_reg_env hd), \snd (regs … st)〉
128       (set_frms ERTL_state tl st) in
129    ! 〈st'', pc〉 ← pop_ra … st' ;
130    if eq_block (funct_block hd) (pc_block pc) then
131      ! sp ← sp … st'' ;
132      ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
133      let framesize : Byte ≝ bitvector_of_nat 8 framesize in
134      let newsp ≝ shift_pointer … sp framesize in
135      OK … 〈set_sp … newsp st'', pc〉
136    else Error ? [MSG BlockInFramesCorrupted]
137 ].
138@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
139
140(*CSC: XXXX, for external functions only*)
141axiom ertl_fetch_external_args: external_function → state ERTL_state → call_args ERTL → res (list val).
142axiom ertl_set_result : list val → unit → state ERTL_state → res (state ERTL_state).
143(* I think there should be a list beval in place of list val here
144  λvals.λ_.λst.
145  (* set all RegisterRets to 0 *)
146  let reset ≝ λenv,r.hwreg_store r (BVByte (bv_zero …)) env in
147  let env ≝ foldl … reset (\snd (regs … st)) RegisterRets in
148  let set_vals ≝ λenv,pr.hwreg_store (\fst pr) (\snd pr) env in ?.
149  let env' ≝ foldl … set_vals env (zip_pottier … RegisterRets vals) in
150  return (set_regs ERTL_state 〈\fst (regs … st), env'〉 st).*)
151
152(*CSC: here we should use helper_def_store from Joint/semantics.ma,
153  but it is not visible *)
154definition ps_reg_store_status : register → beval → state ERTL_state →
155  res (state ERTL_state) ≝
156 λdst,v,st.
157  let env ≝ regs … st in
158  ! env' ← ps_reg_store dst v env ;
159  return set_regs ERTL_state env' st.
160
161
162definition ertl_setup_call : ℕ → state ERTL_state → res (state ERTL_state) ≝
163λframesize,st.
164  ! sp ← sp … st ;
165  let framesize : Byte ≝ bitvector_of_nat 8 framesize in
166  let newsp ≝ neg_shift_pointer … sp framesize in
167  return set_sp … newsp st.
168@hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.
169 
170definition eval_ertl_seq:
171 ∀F. ∀globals. genv_gen F globals →
172  ertl_seq → ident → state ERTL_state →
173   res (state ERTL_state) ≝
174 λF,globals,ge,stm,id,st.
175 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
176 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
177   match stm with
178   [ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st].
179   
180(*
181definition eval_ertl_seq:
182 ∀F. ∀globals. genv_gen F globals →
183  ertl_seq → ident → state ERTL_state →
184   res (state ERTL_state) ≝
185 λF,globals,ge,stm,id,st.
186 ! framesize ← opt_to_res … (msg FunctionNotFound) (stack_sizes … ge id);
187 let framesize : Byte ≝ bitvector_of_nat 8 framesize in
188  match stm with
189   [ ertl_new_frame ⇒
190      ! sp ← sp … st ;
191      let newsp ≝ neg_shift_pointer … sp framesize in
192      return set_sp … newsp st
193   | ertl_del_frame ⇒
194      ! sp ← sp … st ;
195      let newsp ≝ shift_pointer … sp framesize in
196      return set_sp … newsp st
197   | ertl_frame_size dst ⇒ ps_reg_store_status dst (BVByte framesize) st
198   ]. @hide_prf whd in match newsp; cases sp #ptr #EQ <EQ % qed.  *)
199
200definition ERTL_sem_uns ≝ 
201λF. mk_sem_unserialized_params ERTL ?
202  (* st_pars            ≝ *) ERTL_state
203  (* acca_store_        ≝ *) ps_reg_store
204  (* acca_retrieve_     ≝ *) ps_reg_retrieve
205  (* acca_arg_retrieve_ ≝ *) ps_arg_retrieve
206  (* accb_store_        ≝ *) ps_reg_store
207  (* accb_retrieve_     ≝ *) ps_reg_retrieve
208  (* accb_arg_retrieve_ ≝ *) ps_arg_retrieve
209  (* dpl_store_         ≝ *) ps_reg_store
210  (* dpl_retrieve_      ≝ *) ps_reg_retrieve
211  (* dpl_arg_retrieve_  ≝ *) ps_arg_retrieve
212  (* dph_store_         ≝ *) ps_reg_store
213  (* dph_retrieve_      ≝ *) ps_reg_retrieve
214  (* dph_arg_retrieve_  ≝ *) ps_arg_retrieve
215  (* snd_arg_retrieve_  ≝ *) ps_arg_retrieve
216  (* pair_reg_move_     ≝ *) ertl_eval_move
217  (* save_frame         ≝ *) ertl_save_frame
218  (* setup_call         ≝ *) (λn.λ_.λ_.λst.ertl_setup_call n st)
219  (* fetch_external_args≝ *) ertl_fetch_external_args
220  (* set_result         ≝ *) ertl_set_result
221  (* call_args_for_main ≝ *) 0
222  (* call_dest_for_main ≝ *) it
223  (* read_result        ≝ *) (λ_.λ_.λ_.
224     λst.return map ?? (hwreg_retrieve (\snd (regs … st))) RegisterRets)
225  (* eval_ext_seq       ≝ *) (λgl,ge,stm,id.eval_ertl_seq F gl ge stm id)
226  (* pop_frame          ≝ *) (λglobals,ge,id.λ_.λst.ertl_pop_frame F globals ge id st)
227  (* validate_pointer   ≝ *) (ERTL_validate_pointer …).
228
229definition ERTL_semantics ≝
230  mk_sem_graph_params ERTL ERTL_sem_uns ERTL_premain.
Note: See TracBrowser for help on using the repository browser.