source: src/RTL/RTL_semantics.ma @ 2935

Last change on this file since 2935 was 2935, checked in by tranquil, 7 years ago

separation of RTL semantics in three different versions, and correction of a bug in pop_frame.

File size: 10.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
55definition RTL_state ≝ state RTL_state_params.
56
57unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
58
59definition rtl_arg_retrieve : reg_sp → psd_argument → res beval ≝
60  λenv.λa : psd_argument.
61  match a with
62  [ Reg r ⇒ reg_retrieve env r
63  | Imm b ⇒ OK … (BVByte b)
64  ].
65
66(*CSC: could we use here a dependent type to avoid the Error case? *)
67definition rtl_fetch_ra:
68 RTL_state → res (RTL_state × program_counter) ≝
69 λst.
70 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
71   match frms with
72  [ nil ⇒ Error ? [MSG EmptyStack]
73  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉
74  ].
75
76definition rtl_init_local :
77 register → reg_sp → reg_sp ≝
78 λlocal.reg_sp_store … local BVundef.
79
80lemma Zlt_to_not_Zle : ∀z1,z2 : Z.z1 < z2 → z2 ≰ z1.
81#z1 #z2 #H % #G
82lapply (Zlt_to_Zle_to_Zlt … H G) #ABS @(absurd ? ABS ?) @irreflexive_Zlt
83qed.
84
85definition rtl_setup_call_separate :
86 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
87  λstacksize,formal_arg_regs,actual_arg_regs,st.
88  let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
89  let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
90  do new_regs ←
91   mfold_left2 …
92    (λlenv,dest,src.
93      do v ← rtl_arg_retrieve … (regs ? st) src ;
94      OK … (reg_sp_store dest v lenv))
95    (OK … (reg_sp_empty sp)) formal_arg_regs actual_arg_regs ;
96  OK …
97   (set_regs RTL_state_params new_regs
98    (set_m … mem st)).
99@hide_prf
100whd in match sp; -sp
101cases (m ??) in E; #m #next #prf
102whd in ⊢ (???%→?); #EQ destruct
103whd in ⊢ (??%?); @Zleb_elim_Type0 [2: #_ %]
104#abs cases (absurd ? abs ?) @Zlt_to_not_Zle assumption
105qed.
106
107(* move *)
108axiom StackOverflow : ErrorMessage.
109
110definition rtl_setup_call_separate_overflow :
111 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
112  λstacksize,formal_arg_regs,actual_arg_regs,st.
113  (* using nats is highly inefficient... *)
114  if leb (S (stacksize + stack_usage … st)) (2^16) then
115    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
116  else Error … [MSG StackOverflow].
117
118definition rtl_setup_call_unique :
119 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
120  λstacksize,formal_arg_regs,actual_arg_regs,st.
121  ! sp ← sp … st ; (* always succeeds in RTL *)
122  let newsp ≝ neg_shift_pointer … sp (bitvector_of_nat 8 stacksize) in
123  do new_regs ←
124   mfold_left2 …
125    (λlenv,dest,src.
126      do v ← rtl_arg_retrieve … (regs ? st) src ;
127      OK … (reg_sp_store dest v lenv))
128    (OK … (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs ;
129  OK …
130   (set_regs RTL_state_params new_regs st).
131@(pi2 … sp) qed.
132
133definition RTL_state_pc ≝ state_pc RTL_state_params.
134
135unification hint 0 ≔ ⊢ RTL_state ≡ state RTL_state_params.
136unification hint 0 ≔ ⊢ RTL_state_pc ≡ state_pc RTL_state_params.
137
138definition rtl_save_frame ≝ λretregs.λst : RTL_state_pc.
139 ! frms ← opt_to_res … [MSG … FrameErrorOnPush] (st_frms … st) ;
140 let frame ≝ mk_frame retregs (pc ? st) (carry ? st) (regs ? st) :: frms in
141  OK … (set_frms RTL_state_params frame st).
142
143(*CSC: XXXX, for external functions only*)
144axiom rtl_fetch_external_args: external_function → RTL_state → list psd_argument → res (list val).
145axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
146
147definition rtl_reg_store ≝ λr,v,st.
148  let mem ≝ reg_sp_store r v (regs RTL_state_params st) in
149  set_regs RTL_state_params mem st.
150
151definition rtl_reg_retrieve ≝ λst,l.reg_sp_retrieve (regs RTL_state_params st) l.
152
153definition rtl_read_result :
154 list register → RTL_state → res (list beval) ≝
155 λrets,st.
156 m_list_map … (rtl_reg_retrieve st) rets.
157
158(*CSC: we could use a dependent type here: the list of return values should have
159  the same length of the list of return registers that store the values. This
160  saves the OutOfBounds exception *)
161definition rtl_pop_frame_separate:
162 list register → RTL_state →
163  res (RTL_state × program_counter) ≝
164 λret,st.
165 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
166 match frms with
167  [ nil ⇒ Error ? [MSG EmptyStack]
168  | cons hd tl ⇒
169    ! ret_vals ← rtl_read_result … ret st ;
170    (* Paolo: no more OutOfBounds exception, but is it right? should be for
171       compiled programs *)
172    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
173    ! sp ← sp … st ;  (* always succeeds in RTL *)
174    let st ≝ set_frms RTL_state_params tl
175        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
176          (set_carry RTL_state_params (fr_carry hd)
177            (set_m … (free … (m … st) (pblock sp)) st))) in
178    let pc ≝ fr_pc hd in
179    let st ≝ foldl …
180      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
181      st reg_vals in
182    return 〈st, pc〉
183  ].
184
185(* as the stack pointer is reobtained from the frame, there is no need
186   to shift it back into position. We still need to avoid freeing
187   the memory *)
188definition rtl_pop_frame_unique:
189 list register → RTL_state →
190  res (RTL_state × program_counter) ≝
191 λret,st.
192 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
193 match frms with
194  [ nil ⇒ Error ? [MSG EmptyStack]
195  | cons hd tl ⇒
196    ! ret_vals ← rtl_read_result … ret st ;
197    (* Paolo: no more OutOfBounds exception, but is it right? should be for
198       compiled programs *)
199    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
200    ! sp ← sp … st ;  (* always succeeds in RTL *)
201    let st ≝ set_frms RTL_state_params tl
202        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
203          (set_carry RTL_state_params (fr_carry hd) st)) in
204    let pc ≝ fr_pc hd in
205    let st ≝ foldl …
206      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
207      st reg_vals in
208    return 〈st, pc〉
209  ].
210
211definition block_of_register_pair: register → register → RTL_state → res block ≝
212 λr1,r2,st.
213 do v1 ← rtl_reg_retrieve st r1 ;
214 do v2 ← rtl_reg_retrieve st r2 ;
215 do ptr ← pointer_of_address 〈v1,v2〉 ;
216 OK … (pblock ptr). 
217
218definition eval_rtl_seq:
219  rtl_seq → ident → RTL_state →
220   res RTL_state ≝
221 λstm,curr_fn,st.
222  match stm with
223   [ rtl_stack_address dreg1 dreg2  ⇒
224      ! sp ← sp ? st ; (* always succeeds in RTL *)
225      let 〈dpl,dph〉 ≝ beval_pair_of_pointer sp in
226      let st ≝ rtl_reg_store dreg1 dpl st in
227      return rtl_reg_store dreg2 dph st
228   ].
229
230(* for a store living in res *)
231definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
232
233definition RTL_semantics_separate ≝
234  mk_sem_graph_params RTL
235    (λF.mk_sem_unserialized_params RTL F
236      RTL_state_params
237      reg_res_store reg_sp_retrieve rtl_arg_retrieve
238      reg_res_store reg_sp_retrieve rtl_arg_retrieve
239      reg_res_store reg_sp_retrieve rtl_arg_retrieve
240      reg_res_store reg_sp_retrieve rtl_arg_retrieve
241      rtl_arg_retrieve
242      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
243        ! v ← rtl_arg_retrieve env src ;
244        return reg_sp_store dest v env)
245      (λ_.rtl_save_frame)
246      rtl_setup_call_separate
247      rtl_fetch_external_args
248      rtl_set_result
249      [ ] [ ]
250      (λ_.λ_.rtl_read_result) 
251      (λ_.λ_.eval_rtl_seq)
252      (λ_.λ_.λ_.rtl_pop_frame_separate)).
253
254definition RTL_semantics_separate_overflow ≝
255  mk_sem_graph_params RTL
256    (λF.mk_sem_unserialized_params RTL F
257      RTL_state_params
258      reg_res_store reg_sp_retrieve rtl_arg_retrieve
259      reg_res_store reg_sp_retrieve rtl_arg_retrieve
260      reg_res_store reg_sp_retrieve rtl_arg_retrieve
261      reg_res_store reg_sp_retrieve rtl_arg_retrieve
262      rtl_arg_retrieve
263      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
264        ! v ← rtl_arg_retrieve env src ;
265        return reg_sp_store dest v env)
266      (λ_.rtl_save_frame)
267      rtl_setup_call_separate_overflow
268      rtl_fetch_external_args
269      rtl_set_result
270      [ ] [ ]
271      (λ_.λ_.rtl_read_result) 
272      (λ_.λ_.eval_rtl_seq)
273      (λ_.λ_.λ_.rtl_pop_frame_separate)).
274
275definition RTL_semantics_unique ≝
276  mk_sem_graph_params RTL
277    (λF.mk_sem_unserialized_params RTL F
278      RTL_state_params
279      reg_res_store reg_sp_retrieve rtl_arg_retrieve
280      reg_res_store reg_sp_retrieve rtl_arg_retrieve
281      reg_res_store reg_sp_retrieve rtl_arg_retrieve
282      reg_res_store reg_sp_retrieve rtl_arg_retrieve
283      rtl_arg_retrieve
284      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
285        ! v ← rtl_arg_retrieve env src ;
286        return reg_sp_store dest v env)
287      (λ_.rtl_save_frame)
288      rtl_setup_call_unique
289      rtl_fetch_external_args
290      rtl_set_result
291      [ ] [ ]
292      (λ_.λ_.rtl_read_result) 
293      (λ_.λ_.eval_rtl_seq)
294      (λ_.λ_.λ_.rtl_pop_frame_unique)).
Note: See TracBrowser for help on using the repository browser.