source: src/RTL/RTL_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: 13.5 KB
Line 
1include "joint/semanticsUtils.ma".
2include "RTL/RTL.ma". (* CSC: syntax.ma in RTLabs *)
3include alias "common/Identifiers.ma".
4include alias "ASM/Util.ma".
5
6(* we design here three different semantics of RTL, which differ on how stack
7   is treated.
8   
9   1) the first, RTL_semantics_separate, allocates a new stack for each
10      function call, behaving like RTLabs. Each separate stack is finite
11      (offsets are bounded by 2^16), but the number of stacks is unbounded
12   2) the second, RTL_semantics_separate_overflow, behaves like the previous one,
13      but is defined to fail on stack overflow. The idea is that we use the
14      hypothesis of not stack overflowing to pass from RTL_semantics_separate to
15      RTL_semantics_separate_overflow, without having to trasnform the states in
16      any way
17   3) the third, RTL_semantics_unique, behaves like ERTL and later languages:
18      the stack is unique (allocation happens once in make_initial_state, see
19      joint/Traces.ma). However the proof that allows passing from
20      RTL_semantics_separate_overflow to RTL_semantics_unique should not
21      rely on any hypothesis about stack usage
22
23*)
24 
25record reg_sp : Type[0] ≝
26{ reg_sp_env :> identifier_map RegisterTag beval
27; stackp : xpointer
28}.
29
30definition reg_sp_store ≝ λreg,v,locals.
31let locals' ≝ reg_store reg v (reg_sp_env locals) in
32mk_reg_sp locals' (stackp locals).
33
34definition reg_sp_retrieve ≝ λlocals : reg_sp.reg_retrieve locals.
35
36definition reg_sp_empty ≝ mk_reg_sp (empty_map …).
37(*** Store/retrieve on hardware registers ***)
38
39record frame: Type[0] ≝
40 { fr_ret_regs: list register
41 ; fr_pc: program_counter
42 ; fr_carry: bebit
43 ; fr_regs: reg_sp
44 }.
45
46definition RTL_state_params : sem_state_params ≝
47  mk_sem_state_params
48    (list frame)
49    [ ]
50    reg_sp
51    reg_sp_empty
52    (λenv.OK … (stackp env))
53    (λenv.mk_reg_sp env (* coercion*)).
54
55(* in separate stacks, when a pointer has the same block that a stack pointer
56   in frame, either it is correct or we can immediately fire an error.
57   If the ptr's block is not any of the stack pointer blocks, we suppose
58   it's pointing to a global and we accept it. *)
59definition RTL_separate_validate_pointer : ∀F. ∀globals. genv_gen F globals →
60  ident → state RTL_state_params → pointer → res unit ≝
61λF,globals,ge,curr_id,st,ptr.
62! bl ← opt_to_res … [MSG BadFunction; CTX … curr_id]
63  (! bl ← find_symbol … ge curr_id ; code_block_of_block bl) ;
64! 〈ign, f〉 ← fetch_internal_function … ge bl ;
65if eq_block (pblock ptr) (pblock (stackp (regs … st))) ∧
66  leb (get_joint_if_local_stacksize … ge f)
67    (nat_of_bitvector … (offv (poff ptr))) then
68  Error … (msg BadPointer)
69else
70  ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
71  m_fold ??? (λfr.λ_.
72    ! 〈ign, f〉 ← fetch_internal_function … ge (pc_block (fr_pc fr)) ;
73    if eq_block (pblock ptr) (pblock (stackp (fr_regs fr))) ∧
74      leb (get_joint_if_local_stacksize … ge f)
75        (nat_of_bitvector … (offv (poff ptr))) then
76       Error … (msg BadPointer)
77    else return it) frms it.
78 
79(* when the stack is unique, the stack block is already present in the state
80   that we are analysing.
81   If the ptr's block is not it, we suppose
82   it's pointing to a global and we accept it. *)
83definition RTL_unique_validate_pointer : ∀F. ∀globals. genv_gen F globals →
84  ident → state RTL_state_params → pointer → res unit ≝
85λF,globals,ge,curr_id,st,ptr.
86let sp ≝ stackp (regs … st) in
87if eq_block (pblock ptr) (pblock sp) then
88  let off ≝
89    λsp : pointer.Z_of_unsigned_bitvector … (offv (poff ptr)) -
90        Z_of_unsigned_bitvector … (offv (poff sp)) in
91  ! bl ← opt_to_res … [MSG BadFunction; CTX … curr_id]
92    (! bl ← find_symbol … ge curr_id ; code_block_of_block bl) ;
93  ! 〈ign, f〉 ← fetch_internal_function … ge bl ;
94  let o' ≝ off sp in
95  if Zltb o' 0 ∨ Zleb (get_joint_if_local_stacksize … ge f) o' then
96    Error … (msg BadPointer)
97  else
98    ! frms ← opt_to_res ? (msg FrameErrorOnPop) (st_frms ? st) ;
99    m_fold ??? (λfr.λ_.
100      ! 〈ign, f〉 ← fetch_internal_function … ge (pc_block (fr_pc fr)) ;
101      let o' ≝ off (stackp (fr_regs fr)) in
102      if Zltb o' 0 ∨ Zleb (get_joint_if_local_stacksize … ge f) o' then
103         Error … (msg BadPointer)
104      else return it) frms it
105else return it.
106
107definition RTL_state ≝ state RTL_state_params.
108
109unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
110
111definition rtl_arg_retrieve : reg_sp → psd_argument → res beval ≝
112  λenv.λa : psd_argument.
113  match a with
114  [ Reg r ⇒ reg_retrieve env r
115  | Imm b ⇒ OK … (BVByte b)
116  ].
117
118(*CSC: could we use here a dependent type to avoid the Error case? *)
119definition rtl_fetch_ra:
120 RTL_state → res (RTL_state × program_counter) ≝
121 λst.
122 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
123   match frms with
124  [ nil ⇒ Error ? [MSG EmptyStack]
125  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉
126  ].
127
128definition rtl_init_local :
129 register → reg_sp → reg_sp ≝
130 λlocal.reg_sp_store … local BVundef.
131
132lemma Zlt_to_not_Zle : ∀z1,z2 : Z.z1 < z2 → z2 ≰ z1.
133#z1 #z2 #H % #G
134lapply (Zlt_to_Zle_to_Zlt … H G) #ABS @(absurd ? ABS ?) @irreflexive_Zlt
135qed.
136
137definition rtl_setup_call_separate :
138 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
139  λstacksize,formal_arg_regs,actual_arg_regs,st.
140  let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
141  let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
142  do new_regs ←
143   mfold_left2 …
144    (λlenv,dest,src.
145      do v ← rtl_arg_retrieve … (regs ? st) src ;
146      OK … (reg_sp_store dest v lenv))
147    (OK … (reg_sp_empty sp)) formal_arg_regs actual_arg_regs ;
148  OK …
149   (set_regs RTL_state_params new_regs
150    (set_m … mem st)).
151@hide_prf
152whd in match sp; -sp
153cases (m ??) in E; #m #next #prf
154whd in ⊢ (???%→?); #EQ destruct
155whd in ⊢ (??%?); @Zleb_elim_Type0 [2: #_ %]
156#abs cases (absurd ? abs ?) @Zlt_to_not_Zle assumption
157qed.
158
159definition rtl_setup_call_separate_overflow :
160 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
161  λstacksize,formal_arg_regs,actual_arg_regs,st.
162  (* using nats is highly inefficient... *)
163  if leb (S (stacksize + stack_usage … st)) (2^16) then
164    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
165  else Error … [MSG StackOverflow].
166
167definition rtl_setup_call_unique :
168 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
169  λstacksize,formal_arg_regs,actual_arg_regs,st.
170  ! sp ← sp … st ; (* always succeeds in RTL *)
171  let newsp ≝ neg_shift_pointer … sp (bitvector_of_nat 8 stacksize) in
172  do new_regs ←
173   mfold_left2 …
174    (λlenv,dest,src.
175      do v ← rtl_arg_retrieve … (regs ? st) src ;
176      OK … (reg_sp_store dest v lenv))
177    (OK … (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs ;
178  OK …
179   (set_regs RTL_state_params new_regs st).
180@(pi2 … sp) qed.
181
182definition RTL_state_pc ≝ state_pc RTL_state_params.
183
184unification hint 0 ≔ ⊢ RTL_state ≡ state RTL_state_params.
185unification hint 0 ≔ ⊢ RTL_state_pc ≡ state_pc RTL_state_params.
186
187definition rtl_save_frame ≝ λretregs.λst : RTL_state_pc.
188 ! frms ← opt_to_res … [MSG … FrameErrorOnPush] (st_frms … st) ;
189 let frame ≝ mk_frame retregs (pc ? st) (carry ? st) (regs ? st) :: frms in
190  OK … (set_frms RTL_state_params frame st).
191
192(*CSC: XXXX, for external functions only*)
193axiom rtl_fetch_external_args: external_function → RTL_state → list psd_argument → res (list val).
194axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
195
196definition rtl_reg_store ≝ λr,v,st.
197  let mem ≝ reg_sp_store r v (regs RTL_state_params st) in
198  set_regs RTL_state_params mem st.
199
200definition rtl_reg_retrieve ≝ λst,l.reg_sp_retrieve (regs RTL_state_params st) l.
201
202definition rtl_read_result :
203 list register → RTL_state → res (list beval) ≝
204 λrets,st.
205 m_list_map … (rtl_reg_retrieve st) rets.
206
207(*CSC: we could use a dependent type here: the list of return values should have
208  the same length of the list of return registers that store the values. This
209  saves the OutOfBounds exception *)
210definition rtl_pop_frame_separate:
211 list register → RTL_state →
212  res (RTL_state × program_counter) ≝
213 λret,st.
214 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
215 match frms with
216  [ nil ⇒ Error ? [MSG EmptyStack]
217  | cons hd tl ⇒
218    ! ret_vals ← rtl_read_result … ret st ;
219    (* Paolo: no more OutOfBounds exception, but is it right? should be for
220       compiled programs *)
221    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
222    ! sp ← sp … st ;  (* always succeeds in RTL *)
223    let st ≝ set_frms RTL_state_params tl
224        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
225          (set_carry RTL_state_params (fr_carry hd)
226            (set_m … (free … (m … st) (pblock sp)) st))) in
227    let pc ≝ fr_pc hd in
228    let st ≝ foldl …
229      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
230      st reg_vals in
231    return 〈st, pc〉
232  ].
233
234(* as the stack pointer is reobtained from the frame, there is no need
235   to shift it back into position. We still need to avoid freeing
236   the memory *)
237definition rtl_pop_frame_unique:
238 list register → RTL_state →
239  res (RTL_state × program_counter) ≝
240 λret,st.
241 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
242 match frms with
243  [ nil ⇒ Error ? [MSG EmptyStack]
244  | cons hd tl ⇒
245    ! ret_vals ← rtl_read_result … ret st ;
246    (* Paolo: no more OutOfBounds exception, but is it right? should be for
247       compiled programs *)
248    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
249    ! sp ← sp … st ;  (* always succeeds in RTL *)
250    let st ≝ set_frms RTL_state_params tl
251        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
252          (set_carry RTL_state_params (fr_carry hd) st)) in
253    let pc ≝ fr_pc hd in
254    let st ≝ foldl …
255      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
256      st reg_vals in
257    return 〈st, pc〉
258  ].
259
260definition block_of_register_pair: register → register → RTL_state → res block ≝
261 λr1,r2,st.
262 do v1 ← rtl_reg_retrieve st r1 ;
263 do v2 ← rtl_reg_retrieve st r2 ;
264 do ptr ← pointer_of_address 〈v1,v2〉 ;
265 OK … (pblock ptr). 
266
267definition eval_rtl_seq:
268  rtl_seq → ident → RTL_state →
269   res RTL_state ≝
270 λstm,curr_fn,st.
271  match stm with
272   [ rtl_stack_address dreg1 dreg2  ⇒
273      ! sp ← sp ? st ; (* always succeeds in RTL *)
274      let 〈dpl,dph〉 ≝ beval_pair_of_pointer sp in
275      let st ≝ rtl_reg_store dreg1 dpl st in
276      return rtl_reg_store dreg2 dph st
277   ].
278
279(* for a store living in res *)
280definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
281
282definition RTL_semantics_separate ≝
283  mk_sem_graph_params RTL
284    (λF.mk_sem_unserialized_params RTL F
285      RTL_state_params
286      reg_res_store reg_sp_retrieve rtl_arg_retrieve
287      reg_res_store reg_sp_retrieve rtl_arg_retrieve
288      reg_res_store reg_sp_retrieve rtl_arg_retrieve
289      reg_res_store reg_sp_retrieve rtl_arg_retrieve
290      rtl_arg_retrieve
291      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
292        ! v ← rtl_arg_retrieve env src ;
293        return reg_sp_store dest v env)
294      (λ_.rtl_save_frame)
295      rtl_setup_call_separate
296      rtl_fetch_external_args
297      rtl_set_result
298      [ ]
299      [an_identifier … one ; an_identifier … (p0 one) ;
300       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
301      (λ_.λ_.rtl_read_result) 
302      (λ_.λ_.eval_rtl_seq)
303      (λ_.λ_.λ_.rtl_pop_frame_separate)
304      (RTL_separate_validate_pointer …))
305    RTL_premain.
306
307definition RTL_semantics_separate_overflow ≝
308  mk_sem_graph_params RTL
309    (λF.mk_sem_unserialized_params RTL F
310      RTL_state_params
311      reg_res_store reg_sp_retrieve rtl_arg_retrieve
312      reg_res_store reg_sp_retrieve rtl_arg_retrieve
313      reg_res_store reg_sp_retrieve rtl_arg_retrieve
314      reg_res_store reg_sp_retrieve rtl_arg_retrieve
315      rtl_arg_retrieve
316      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
317        ! v ← rtl_arg_retrieve env src ;
318        return reg_sp_store dest v env)
319      (λ_.rtl_save_frame)
320      rtl_setup_call_separate_overflow
321      rtl_fetch_external_args
322      rtl_set_result
323      [ ]
324      [an_identifier … one ; an_identifier … (p0 one) ;
325       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
326      (λ_.λ_.rtl_read_result) 
327      (λ_.λ_.eval_rtl_seq)
328      (λ_.λ_.λ_.rtl_pop_frame_separate)
329      (RTL_separate_validate_pointer …))
330    RTL_premain.
331
332definition RTL_semantics_unique ≝
333  mk_sem_graph_params RTL
334    (λF.mk_sem_unserialized_params RTL F
335      RTL_state_params
336      reg_res_store reg_sp_retrieve rtl_arg_retrieve
337      reg_res_store reg_sp_retrieve rtl_arg_retrieve
338      reg_res_store reg_sp_retrieve rtl_arg_retrieve
339      reg_res_store reg_sp_retrieve rtl_arg_retrieve
340      rtl_arg_retrieve
341      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
342        ! v ← rtl_arg_retrieve env src ;
343        return reg_sp_store dest v env)
344      (λ_.rtl_save_frame)
345      rtl_setup_call_unique
346      rtl_fetch_external_args
347      rtl_set_result
348      [ ]
349      [an_identifier … one ; an_identifier … (p0 one) ;
350       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
351      (λ_.λ_.rtl_read_result) 
352      (λ_.λ_.eval_rtl_seq)
353      (λ_.λ_.λ_.rtl_pop_frame_unique)
354      (RTL_unique_validate_pointer …))
355    RTL_premain.
Note: See TracBrowser for help on using the repository browser.