source: src/RTL/RTL_semantics.ma @ 2860

Last change on this file since 2860 was 2823, checked in by tranquil, 7 years ago
  • corrected bug in ERTL semantics (both delframe and newframe did the same operation on the stack pointer...)
  • split RTL semantics in two (one with multiple stack spaces per call, one with only one for all)
  • joint_if_entry is not required anymore to be in the code (as it is covered by entry_costed in good_if)
  • temporarily replaced the two biggest proofs of linearise by daemons
File size: 8.2 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
6record frame: Type[0] ≝
7 { fr_ret_regs: list register
8 ; fr_pc: program_counter
9 ; fr_carry: bebit
10 ; fr_regs: reg_sp
11 }.
12
13definition RTL_state_params : sem_state_params ≝
14  mk_sem_state_params
15    (list frame)
16    [ ]
17    reg_sp
18    reg_sp_init
19    (λenv.OK … (stackp env))
20    (λenv.mk_reg_sp env (* coercion*)).
21
22definition RTL_state ≝ state RTL_state_params.
23
24unification hint 0 ≔ X ⊢ register_env X ≡ identifier_map RegisterTag X.
25
26definition rtl_arg_retrieve : reg_sp → psd_argument → res beval ≝
27  λenv.λa : psd_argument.
28  match a with
29  [ Reg r ⇒ reg_retrieve env r
30  | Imm b ⇒ OK … (BVByte b)
31  ].
32
33(*CSC: could we use here a dependent type to avoid the Error case? *)
34definition rtl_fetch_ra:
35 RTL_state → res (RTL_state × program_counter) ≝
36 λst.
37 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
38   match frms with
39  [ nil ⇒ Error ? [MSG EmptyStack]
40  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉
41  ].
42
43definition rtl_init_local :
44 register → reg_sp → reg_sp ≝
45 λlocal.reg_sp_store … local BVundef.
46
47lemma Zlt_to_not_Zle : ∀z1,z2 : Z.z1 < z2 → z2 ≰ z1.
48#z1 #z2 #H % #G
49lapply (Zlt_to_Zle_to_Zlt … H G) #ABS @(absurd ? ABS ?) @irreflexive_Zlt
50qed.
51
52definition rtl_setup_call_separate :
53 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
54  λstacksize,formal_arg_regs,actual_arg_regs,st.
55  let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
56  let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
57  do new_regs ←
58   mfold_left2 …
59    (λlenv,dest,src.
60      do v ← rtl_arg_retrieve … (regs ? st) src ;
61      OK … (reg_sp_store dest v lenv))
62    (OK … (reg_sp_init sp)) formal_arg_regs actual_arg_regs ;
63  OK …
64   (set_regs RTL_state_params new_regs
65    (set_m … mem st)).
66@hide_prf
67whd in match sp; -sp
68cases (m ??) in E; #m #next #prf
69whd in ⊢ (???%→?); #EQ destruct
70whd in ⊢ (??%?); @Zleb_elim_Type0 [2: #_ %]
71#abs cases (absurd ? abs ?) @Zlt_to_not_Zle assumption
72qed.
73
74definition rtl_setup_call_unique :
75 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
76  λstacksize,formal_arg_regs,actual_arg_regs,st.
77  (* paolo: this will need to be changed: we want a unified stack in the whole backend *)
78  ! sp ← sp … st ; (* always succeeds in RTL *)
79  let newsp ≝ neg_shift_pointer … sp (bitvector_of_nat 8 stacksize) in
80  do new_regs ←
81   mfold_left2 …
82    (λlenv,dest,src.
83      do v ← rtl_arg_retrieve … (regs ? st) src ;
84      OK … (reg_sp_store dest v lenv))
85    (OK … (reg_sp_init newsp)) formal_arg_regs actual_arg_regs ;
86  OK …
87   (set_regs RTL_state_params new_regs st).
88@(pi2 … sp) qed.
89
90definition RTL_state_pc ≝ state_pc RTL_state_params.
91
92unification hint 0 ≔ ⊢ RTL_state ≡ state RTL_state_params.
93unification hint 0 ≔ ⊢ RTL_state_pc ≡ state_pc RTL_state_params.
94
95definition rtl_save_frame ≝ λretregs.λst : RTL_state_pc.
96 ! frms ← opt_to_res … [MSG … FrameErrorOnPush] (st_frms … st) ;
97 let frame ≝ mk_frame retregs (pc ? st) (carry ? st) (regs ? st) :: frms in
98  OK … (set_frms RTL_state_params frame st).
99
100(*CSC: XXXX, for external functions only*)
101axiom rtl_fetch_external_args: external_function → RTL_state → list psd_argument → res (list val).
102axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
103
104definition rtl_reg_store ≝ λr,v,st.
105  let mem ≝ reg_sp_store r v (regs RTL_state_params st) in
106  set_regs RTL_state_params mem st.
107
108definition rtl_reg_retrieve ≝ λst,l.reg_sp_retrieve (regs RTL_state_params st) l.
109
110definition rtl_read_result :
111 list register → RTL_state → res (list beval) ≝
112 λrets,st.
113 m_list_map … (rtl_reg_retrieve st) rets.
114
115(*CSC: we could use a dependent type here: the list of return values should have
116  the same length of the list of return registers that store the values. This
117  saves the OutOfBounds exception *)
118definition rtl_pop_frame_separate:
119 list register → RTL_state →
120  res (RTL_state × program_counter) ≝
121 λret,st.
122 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
123 match frms with
124  [ nil ⇒ Error ? [MSG EmptyStack]
125  | cons hd tl ⇒
126    ! ret_vals ← rtl_read_result … ret st ;
127    (* Paolo: no more OutOfBounds exception, but is it right? should be for
128       compiled programs *)
129    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
130    let st ≝ foldl …
131      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
132      st reg_vals in
133    ! sp ← sp … st ;  (* always succeeds in RTL *)
134    let st ≝ set_frms RTL_state_params tl
135        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
136          (set_carry RTL_state_params (fr_carry hd)
137            (set_m … (free … (m … st) (pblock sp)) st))) in
138    let pc ≝ fr_pc hd in
139    return 〈st, pc〉
140  ].
141
142(* as the stack pointer is reobtained from the frame, there is no need
143   to shift it back into position. We still need to avoid freeing
144   the memory *)
145definition rtl_pop_frame_unique:
146 list register → RTL_state →
147  res (RTL_state × program_counter) ≝
148 λret,st.
149 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
150 match frms with
151  [ nil ⇒ Error ? [MSG EmptyStack]
152  | cons hd tl ⇒
153    ! ret_vals ← rtl_read_result … ret st ;
154    (* Paolo: no more OutOfBounds exception, but is it right? should be for
155       compiled programs *)
156    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
157    let st ≝ foldl …
158      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
159      st reg_vals in
160    ! sp ← sp … st ;  (* always succeeds in RTL *)
161    let st ≝ set_frms RTL_state_params tl
162        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
163          (set_carry RTL_state_params (fr_carry hd) st)) in
164    let pc ≝ fr_pc hd in
165    return 〈st, pc〉
166  ].
167
168definition block_of_register_pair: register → register → RTL_state → res block ≝
169 λr1,r2,st.
170 do v1 ← rtl_reg_retrieve st r1 ;
171 do v2 ← rtl_reg_retrieve st r2 ;
172 do ptr ← pointer_of_address 〈v1,v2〉 ;
173 OK … (pblock ptr). 
174
175definition eval_rtl_seq:
176  rtl_seq → ident → RTL_state →
177   res RTL_state ≝
178 λstm,curr_fn,st.
179  match stm with
180   [ rtl_stack_address dreg1 dreg2  ⇒
181      ! sp ← sp ? st ; (* always succeeds in RTL *)
182      let 〈dpl,dph〉 ≝ beval_pair_of_pointer sp in
183      let st ≝ rtl_reg_store dreg1 dpl st in
184      return rtl_reg_store dreg2 dph st
185   ].
186
187(* for a store living in res *)
188definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
189
190(* two different semantics: one with separate stacks for each call,
191   the other with a unique one *)
192definition RTL_semantics_separate ≝
193  mk_sem_graph_params RTL
194    (λF.mk_sem_unserialized_params RTL F
195      RTL_state_params
196      reg_res_store reg_sp_retrieve rtl_arg_retrieve
197      reg_res_store reg_sp_retrieve rtl_arg_retrieve
198      reg_res_store reg_sp_retrieve rtl_arg_retrieve
199      reg_res_store reg_sp_retrieve rtl_arg_retrieve
200      rtl_arg_retrieve
201      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
202        ! v ← rtl_arg_retrieve env src ;
203        return reg_sp_store dest v env)
204      (λ_.rtl_save_frame)
205      rtl_setup_call_separate
206      rtl_fetch_external_args
207      rtl_set_result
208      [ ] [ ]
209      (λ_.λ_.rtl_read_result) 
210      (λ_.λ_.eval_rtl_seq)
211      (λ_.λ_.λ_.rtl_pop_frame_separate)).
212
213definition RTL_semantics_unique ≝
214  mk_sem_graph_params RTL
215    (λF.mk_sem_unserialized_params RTL F
216      RTL_state_params
217      reg_res_store reg_sp_retrieve rtl_arg_retrieve
218      reg_res_store reg_sp_retrieve rtl_arg_retrieve
219      reg_res_store reg_sp_retrieve rtl_arg_retrieve
220      reg_res_store reg_sp_retrieve rtl_arg_retrieve
221      rtl_arg_retrieve
222      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
223        ! v ← rtl_arg_retrieve env src ;
224        return reg_sp_store dest v env)
225      (λ_.rtl_save_frame)
226      rtl_setup_call_unique
227      rtl_fetch_external_args
228      rtl_set_result
229      [ ] [ ]
230      (λ_.λ_.rtl_read_result) 
231      (λ_.λ_.eval_rtl_seq)
232      (λ_.λ_.λ_.rtl_pop_frame_unique)).
233
234
Note: See TracBrowser for help on using the repository browser.