source: src/RTL/RTL_semantics.ma @ 2958

Last change on this file since 2958 was 2958, checked in by sacerdot, 7 years ago

Error message implemented.

File size: 10.9 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
107definition rtl_setup_call_separate_overflow :
108 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
109  λstacksize,formal_arg_regs,actual_arg_regs,st.
110  (* using nats is highly inefficient... *)
111  if leb (S (stacksize + stack_usage … st)) (2^16) then
112    rtl_setup_call_separate stacksize formal_arg_regs actual_arg_regs st
113  else Error … [MSG StackOverflow].
114
115definition rtl_setup_call_unique :
116 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
117  λstacksize,formal_arg_regs,actual_arg_regs,st.
118  ! sp ← sp … st ; (* always succeeds in RTL *)
119  let newsp ≝ neg_shift_pointer … sp (bitvector_of_nat 8 stacksize) in
120  do new_regs ←
121   mfold_left2 …
122    (λlenv,dest,src.
123      do v ← rtl_arg_retrieve … (regs ? st) src ;
124      OK … (reg_sp_store dest v lenv))
125    (OK … (reg_sp_empty newsp)) formal_arg_regs actual_arg_regs ;
126  OK …
127   (set_regs RTL_state_params new_regs st).
128@(pi2 … sp) qed.
129
130definition RTL_state_pc ≝ state_pc RTL_state_params.
131
132unification hint 0 ≔ ⊢ RTL_state ≡ state RTL_state_params.
133unification hint 0 ≔ ⊢ RTL_state_pc ≡ state_pc RTL_state_params.
134
135definition rtl_save_frame ≝ λretregs.λst : RTL_state_pc.
136 ! frms ← opt_to_res … [MSG … FrameErrorOnPush] (st_frms … st) ;
137 let frame ≝ mk_frame retregs (pc ? st) (carry ? st) (regs ? st) :: frms in
138  OK … (set_frms RTL_state_params frame st).
139
140(*CSC: XXXX, for external functions only*)
141axiom rtl_fetch_external_args: external_function → RTL_state → list psd_argument → res (list val).
142axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
143
144definition rtl_reg_store ≝ λr,v,st.
145  let mem ≝ reg_sp_store r v (regs RTL_state_params st) in
146  set_regs RTL_state_params mem st.
147
148definition rtl_reg_retrieve ≝ λst,l.reg_sp_retrieve (regs RTL_state_params st) l.
149
150definition rtl_read_result :
151 list register → RTL_state → res (list beval) ≝
152 λrets,st.
153 m_list_map … (rtl_reg_retrieve st) rets.
154
155(*CSC: we could use a dependent type here: the list of return values should have
156  the same length of the list of return registers that store the values. This
157  saves the OutOfBounds exception *)
158definition rtl_pop_frame_separate:
159 list register → RTL_state →
160  res (RTL_state × program_counter) ≝
161 λret,st.
162 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
163 match frms with
164  [ nil ⇒ Error ? [MSG EmptyStack]
165  | cons hd tl ⇒
166    ! ret_vals ← rtl_read_result … ret st ;
167    (* Paolo: no more OutOfBounds exception, but is it right? should be for
168       compiled programs *)
169    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
170    ! sp ← sp … st ;  (* always succeeds in RTL *)
171    let st ≝ set_frms RTL_state_params tl
172        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
173          (set_carry RTL_state_params (fr_carry hd)
174            (set_m … (free … (m … st) (pblock sp)) st))) in
175    let pc ≝ fr_pc hd in
176    let st ≝ foldl …
177      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
178      st reg_vals in
179    return 〈st, pc〉
180  ].
181
182(* as the stack pointer is reobtained from the frame, there is no need
183   to shift it back into position. We still need to avoid freeing
184   the memory *)
185definition rtl_pop_frame_unique:
186 list register → RTL_state →
187  res (RTL_state × program_counter) ≝
188 λret,st.
189 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
190 match frms with
191  [ nil ⇒ Error ? [MSG EmptyStack]
192  | cons hd tl ⇒
193    ! ret_vals ← rtl_read_result … ret st ;
194    (* Paolo: no more OutOfBounds exception, but is it right? should be for
195       compiled programs *)
196    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
197    ! sp ← sp … st ;  (* always succeeds in RTL *)
198    let st ≝ set_frms RTL_state_params tl
199        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
200          (set_carry RTL_state_params (fr_carry hd) st)) in
201    let pc ≝ fr_pc hd in
202    let st ≝ foldl …
203      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
204      st reg_vals in
205    return 〈st, pc〉
206  ].
207
208definition block_of_register_pair: register → register → RTL_state → res block ≝
209 λr1,r2,st.
210 do v1 ← rtl_reg_retrieve st r1 ;
211 do v2 ← rtl_reg_retrieve st r2 ;
212 do ptr ← pointer_of_address 〈v1,v2〉 ;
213 OK … (pblock ptr). 
214
215definition eval_rtl_seq:
216  rtl_seq → ident → RTL_state →
217   res RTL_state ≝
218 λstm,curr_fn,st.
219  match stm with
220   [ rtl_stack_address dreg1 dreg2  ⇒
221      ! sp ← sp ? st ; (* always succeeds in RTL *)
222      let 〈dpl,dph〉 ≝ beval_pair_of_pointer sp in
223      let st ≝ rtl_reg_store dreg1 dpl st in
224      return rtl_reg_store dreg2 dph st
225   ].
226
227(* for a store living in res *)
228definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
229
230definition RTL_semantics_separate ≝
231  mk_sem_graph_params RTL
232    (λF.mk_sem_unserialized_params RTL F
233      RTL_state_params
234      reg_res_store reg_sp_retrieve rtl_arg_retrieve
235      reg_res_store reg_sp_retrieve rtl_arg_retrieve
236      reg_res_store reg_sp_retrieve rtl_arg_retrieve
237      reg_res_store reg_sp_retrieve rtl_arg_retrieve
238      rtl_arg_retrieve
239      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
240        ! v ← rtl_arg_retrieve env src ;
241        return reg_sp_store dest v env)
242      (λ_.rtl_save_frame)
243      rtl_setup_call_separate
244      rtl_fetch_external_args
245      rtl_set_result
246      [ ]
247      [an_identifier … one ; an_identifier … (p0 one) ;
248       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
249      (λ_.λ_.rtl_read_result) 
250      (λ_.λ_.eval_rtl_seq)
251      (λ_.λ_.λ_.rtl_pop_frame_separate))
252    RTL_premain.
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      [an_identifier … one ; an_identifier … (p0 one) ;
272       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
273      (λ_.λ_.rtl_read_result) 
274      (λ_.λ_.eval_rtl_seq)
275      (λ_.λ_.λ_.rtl_pop_frame_separate))
276    RTL_premain.
277
278definition RTL_semantics_unique ≝
279  mk_sem_graph_params RTL
280    (λF.mk_sem_unserialized_params RTL F
281      RTL_state_params
282      reg_res_store reg_sp_retrieve rtl_arg_retrieve
283      reg_res_store reg_sp_retrieve rtl_arg_retrieve
284      reg_res_store reg_sp_retrieve rtl_arg_retrieve
285      reg_res_store reg_sp_retrieve rtl_arg_retrieve
286      rtl_arg_retrieve
287      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
288        ! v ← rtl_arg_retrieve env src ;
289        return reg_sp_store dest v env)
290      (λ_.rtl_save_frame)
291      rtl_setup_call_unique
292      rtl_fetch_external_args
293      rtl_set_result
294      [ ]
295      [an_identifier … one ; an_identifier … (p0 one) ;
296       an_identifier … (p1 one) ; an_identifier … (p0 (p0 one)) ]
297      (λ_.λ_.rtl_read_result) 
298      (λ_.λ_.eval_rtl_seq)
299      (λ_.λ_.λ_.rtl_pop_frame_unique))
300    RTL_premain.
301     
Note: See TracBrowser for help on using the repository browser.