Changeset 2823


Ignore:
Timestamp:
Mar 8, 2013, 3:51:18 PM (6 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
Location:
src
Files:
6 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_semantics.ma

    r2807 r2823  
    122122   [ ertl_new_frame ⇒
    123123      ! sp ← sp … st ;
    124       let newsp ≝ shift_pointer … sp framesize in
     124      let newsp ≝ neg_shift_pointer … sp framesize in
    125125      return set_sp … newsp st
    126126   | ertl_del_frame ⇒
  • src/RTL/RTL_semantics.ma

    r2796 r2823  
    4545 λlocal.reg_sp_store … local BVundef.
    4646
    47 definition rtl_setup_call:
     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 :
    4853 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
    4954  λstacksize,formal_arg_regs,actual_arg_regs,st.
    50   (* paolo: this will need to be changed: we want a unified stack in the whole backend *)
    5155  let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
    5256  let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
     
    6064   (set_regs RTL_state_params new_regs
    6165    (set_m … mem st)).
    62 cases daemon (* will probably change anyway *)
     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
    6372qed.
     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.
    6489
    6590definition RTL_state_pc ≝ state_pc RTL_state_params.
     
    91116  the same length of the list of return registers that store the values. This
    92117  saves the OutOfBounds exception *)
    93 definition rtl_pop_frame:
     118definition rtl_pop_frame_separate:
    94119 list register → RTL_state →
    95120  res (RTL_state × program_counter) ≝
     
    108133    ! sp ← sp … st ;  (* always succeeds in RTL *)
    109134    let st ≝ set_frms RTL_state_params tl
    110         (set_regs RTL_state_params (fr_regs hd)
     135        (set_regs RTL_state_params (fr_regs hd) (* <- this resets the sp too *)
    111136          (set_carry RTL_state_params (fr_carry hd)
    112137            (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
    113164    let pc ≝ fr_pc hd in
    114165    return 〈st, pc〉
     
    137188definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
    138189
    139 definition RTL_semantics ≝
     190(* two different semantics: one with separate stacks for each call,
     191   the other with a unique one *)
     192definition RTL_semantics_separate ≝
    140193  mk_sem_graph_params RTL
    141194    (λF.mk_sem_unserialized_params RTL F
     
    150203        return reg_sp_store dest v env)
    151204      (λ_.rtl_save_frame)
    152       rtl_setup_call
     205      rtl_setup_call_separate
    153206      rtl_fetch_external_args
    154207      rtl_set_result
     
    156209      (λ_.λ_.rtl_read_result) 
    157210      (λ_.λ_.eval_rtl_seq)
    158       (λ_.λ_.λ_.rtl_pop_frame)).
     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
  • src/RTLabs/RTLabsToRTL.ma

    r2808 r2823  
    10341034  let luniverse' ≝ f_labgen def in
    10351035  let stack_size' ≝ f_stacksize def in
    1036   let entry' ≝ f_entry def in
     1036  let entry' ≝ pi1 … (f_entry def) in
    10371037  let init ≝ mk_joint_internal_function RTL globals
    10381038    luniverse' runiverse' [ ] [ ] stack_size' stack_size'
    1039     (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) (pi1 … entry') in
     1039    (add … (empty_map ? (joint_statement ??)) entry' (RETURN …)) entry' in
    10401040  let 〈init',lenv〉 as pr_eq ≝ initialize_locals_params_ret globals
    10411041    (f_locals def) (f_params def) (f_result def) init in
     
    10491049    ] (dpi2 … pr) in
    10501050  foldi … f_trans (f_graph def) init'.
    1051 [4: >graph_code_has_point @mem_set_add_id ] 
    10521051(* TODO *) cases daemon
    10531052qed.
  • src/joint/Joint.ma

    r2808 r2823  
    479479    (that are already on stack in the front end) *)
    480480  joint_if_code     : codeT p globals ;
    481   joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*;
     481  joint_if_entry : code_point p (* Paolo: condition entry ∈ code is ensured by good_if ;
    482482  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
    483483}.
     
    523523          Some … (sequential … (COST_LABEL … l) nxt)
    524524; entry_unused :
    525   let entry ≝ pi1 … (joint_if_entry … def) in
     525  let entry ≝ joint_if_entry … def in
    526526  let code ≝ joint_if_code … def in
    527527  forall_statements_i …
     
    555555       (joint_if_local_stacksize … int_fun)
    556556      graph entry (*exit*).
    557 
    558 definition set_joint_if_graph ≝
    559   λglobals.λpars : graph_params.
    560   λgraph.
    561   λp:joint_internal_function pars globals.
    562   λentry_prf.
    563   (*λexit_prf.*)
    564     set_joint_code globals pars p
    565       graph
    566       (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
    567       (*(mk_Sig … (joint_if_exit ?? p) exit_prf)*).
    568557
    569558definition set_luniverse ≝
     
    594583     (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
    595584     code
    596      (pi1 … (joint_if_entry … p))
     585     (joint_if_entry … p)
    597586     (*(pi1 … (joint_if_exit … p))*).
    598 >graph_code_has_point whd in match code; >mem_set_add
    599 @orb_Prop_r elim (joint_if_entry ???)
    600 #x #H <graph_code_has_point @H
    601 qed.
    602587
    603588definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
  • src/joint/TranslateUtils.ma

    r2808 r2823  
    502502; ss_def_out_eq :
    503503           joint_if_stacksize … def_out = init_stack_size … data
    504 ; entry_eq :
    505           pi1 … (joint_if_entry … def_out) = pi1 … (joint_if_entry … def_in)
     504; entry_eq : joint_if_entry … def_out = joint_if_entry … def_in
    506505; partition_lbls : partial_partition … f_lbls
    507506; partition_regs : partial_partition … f_regs
     
    573572    (joint_if_local_stacksize … def)
    574573    (add ?? (empty_map ? (joint_statement ??)) entry (RETURN …))
    575     («pi1 … entry, mem_set_add_id …») in
     574    entry in
    576575  let f : label → joint_statement (src_g_pars : params) globals →
    577576    joint_internal_function dst_g_pars globals → joint_internal_function dst_g_pars globals ≝
  • src/joint/linearise.ma

    r2808 r2823  
    237237    ] n_prf
    238238  ] (chop_ok ? (λx.x∈visited) visiting).
    239 (* cases daemon *)
     239cases daemon (*)
    240240whd
    241241[ (* base case, visiting is all visited *)
     
    518518|
    519519]
    520 (**)
     520*)
    521521qed.
    522522
     
    705705| >commutative_plus change with (? ≤ |g|) %
    706706]
    707 (* cases daemon *)
     707cases daemon (*)
    708708**
    709709#visited #required #generated normalize nodelta ****
     
    813813  ]
    814814]
    815 (**)
     815*)
    816816qed.
    817817
     
    846846  let code ≝ \fst code_sigma in
    847847  let sigma ≝ \snd code_sigma in
    848   let entry : Σpt.bool_to_Prop (code_has_point … code pt) ≝ «0, hide_prf ??» in
    849848  «〈«mk_joint_internal_function (mk_lin_params p) globals
    850849   (joint_if_luniverse ?? f_sig) (joint_if_runiverse ?? f_sig)
    851850   (joint_if_result ?? f_sig) (joint_if_params ?? f_sig)
    852851   (joint_if_stacksize ?? f_sig) (joint_if_local_stacksize ?? f_sig)
    853    code entry (* exit is dummy! *), hide_prf ??»,
     852   code 0 (* exit is dummy! *), hide_prf ??»,
    854853   sigma〉, proj1 ?? (pi2 ?? code_sigma)».
     854cases daemon (*)
    855855[2: whd in match code; cases code_sigma -code_sigma * #code #sigma
    856856  normalize nodelta *** #H3 #H4 #H5
     
    877877  ]
    878878]
     879*)
    879880qed.
    880881
Note: See TracChangeset for help on using the changeset viewer.