Changeset 2823 for src/RTL

Timestamp:

Mar 8, 2013, 3:51:18 PM (8 years ago)

Author:

tranquil

Message:

• 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:

• src/RTL/RTL_semantics.ma (modified) (7 diffs)

src/RTL/RTL_semantics.ma

@@ -45 +45 @@
  λlocal.reg_sp_store … local BVundef.
 
-definition rtl_setup_call:
+lemma Zlt_to_not_Zle : ∀z1,z2 : Z.z1 < z2 → z2 ≰ z1.
+#z1 #z2 #H % #G
+lapply (Zlt_to_Zle_to_Zlt … H G) #ABS @(absurd ? ABS ?) @irreflexive_Zlt
+qed.
+
+definition rtl_setup_call_separate :
  nat → list register → list psd_argument → RTL_state → res RTL_state ≝
   λstacksize,formal_arg_regs,actual_arg_regs,st.
-  (* paolo: this will need to be changed: we want a unified stack in the whole backend *)
   let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
   let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
@@ -60 +64 @@
    (set_regs RTL_state_params new_regs
     (set_m … mem st)).
-cases daemon (* will probably change anyway *)
+@hide_prf
+whd in match sp; -sp
+cases (m ??) in E; #m #next #prf
+whd in ⊢ (???%→?); #EQ destruct
+whd in ⊢ (??%?); @Zleb_elim_Type0 [2: #_ %]
+#abs cases (absurd ? abs ?) @Zlt_to_not_Zle assumption
 qed.
+
+definition rtl_setup_call_unique :
+ nat → list register → list psd_argument → RTL_state → res RTL_state ≝
+  λstacksize,formal_arg_regs,actual_arg_regs,st.
+  (* paolo: this will need to be changed: we want a unified stack in the whole backend *)
+  ! sp ← sp … st ; (* always succeeds in RTL *)
+  let newsp ≝ neg_shift_pointer … sp (bitvector_of_nat 8 stacksize) in
+  do new_regs ←
+   mfold_left2 …
+    (λlenv,dest,src.
+      do v ← rtl_arg_retrieve … (regs ? st) src ;
+      OK … (reg_sp_store dest v lenv))
+    (OK … (reg_sp_init newsp)) formal_arg_regs actual_arg_regs ;
+  OK …
+   (set_regs RTL_state_params new_regs st).
+@(pi2 … sp) qed.
 
 definition RTL_state_pc ≝ state_pc RTL_state_params.
@@ -91 +116 @@
   the same length of the list of return registers that store the values. This
   saves the OutOfBounds exception *)
-definition rtl_pop_frame:
+definition rtl_pop_frame_separate:
  list register → RTL_state →
   res (RTL_state × program_counter) ≝
@@ -108 +133 @@
     ! sp ← sp … st ;  (* always succeeds in RTL *)
     let st ≝ set_frms RTL_state_params tl
-        (set_regs RTL_state_params (fr_regs hd)
+        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
           (set_carry RTL_state_params (fr_carry hd)
             (set_m … (free … (m … st) (pblock sp)) st))) in
+    let pc ≝ fr_pc hd in
+    return 〈st, pc〉
+  ].
+
+(* as the stack pointer is reobtained from the frame, there is no need
+   to shift it back into position. We still need to avoid freeing
+   the memory *)
+definition rtl_pop_frame_unique:
+ list register → RTL_state →
+  res (RTL_state × program_counter) ≝
+ λret,st.
+ ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
+ match frms with
+  [ nil ⇒ Error ? [MSG EmptyStack]
+  | cons hd tl ⇒
+    ! ret_vals ← rtl_read_result … ret st ;
+    (* Paolo: no more OutOfBounds exception, but is it right? should be for
+       compiled programs *)
+    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
+    let st ≝ foldl …
+      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
+      st reg_vals in
+    ! sp ← sp … st ;  (* always succeeds in RTL *)
+    let st ≝ set_frms RTL_state_params tl
+        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
+          (set_carry RTL_state_params (fr_carry hd) st)) in
     let pc ≝ fr_pc hd in
     return 〈st, pc〉
@@ -137 +188 @@
 definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
 
-definition RTL_semantics ≝
+(* two different semantics: one with separate stacks for each call,
+   the other with a unique one *)
+definition RTL_semantics_separate ≝
   mk_sem_graph_params RTL
     (λF.mk_sem_unserialized_params RTL F
@@ -150 +203 @@
         return reg_sp_store dest v env)
       (λ_.rtl_save_frame)
-      rtl_setup_call
+      rtl_setup_call_separate
       rtl_fetch_external_args
       rtl_set_result
@@ -156 +209 @@
       (λ_.λ_.rtl_read_result)  
       (λ_.λ_.eval_rtl_seq)
-      (λ_.λ_.λ_.rtl_pop_frame)).
+      (λ_.λ_.λ_.rtl_pop_frame_separate)).
+
+definition RTL_semantics_unique ≝
+  mk_sem_graph_params RTL
+    (λF.mk_sem_unserialized_params RTL F
+      RTL_state_params
+      reg_res_store reg_sp_retrieve rtl_arg_retrieve
+      reg_res_store reg_sp_retrieve rtl_arg_retrieve
+      reg_res_store reg_sp_retrieve rtl_arg_retrieve
+      reg_res_store reg_sp_retrieve rtl_arg_retrieve
+      rtl_arg_retrieve
+      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
+        ! v ← rtl_arg_retrieve env src ;
+        return reg_sp_store dest v env)
+      (λ_.rtl_save_frame)
+      rtl_setup_call_unique
+      rtl_fetch_external_args
+      rtl_set_result
+      [ ] [ ]
+      (λ_.λ_.rtl_read_result)  
+      (λ_.λ_.eval_rtl_seq)
+      (λ_.λ_.λ_.rtl_pop_frame_unique)).
+
+