Changeset 2796 for src/RTL


Ignore:
Timestamp:
Mar 7, 2013, 12:10:42 PM (7 years ago)
Author:
tranquil
Message:
  • added global notation for existence in Type[1] (\exists[1] x.P)
  • in Arithmetic, reimplemented efficient nat_to_bitvector, but still commented out
  • in joint_semantics, moved out and around some parameters in primitive semantics functions
  • fixed all back end semantics
  • added skeleton files for single passes correctness proofs
Location:
src/RTL
Files:
1 added
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL_semantics.ma

    r2645 r2796  
    66record frame: Type[0] ≝
    77 { fr_ret_regs: list register
    8  ; fr_pc: cpointer
    9  ; fr_sp: xpointer
     8 ; fr_pc: program_counter
    109 ; fr_carry: bebit
    11  ; fr_regs: register_env beval
     10 ; fr_regs: reg_sp
    1211 }.
    1312
    14 definition RTL_state : sem_state_params ≝
     13definition RTL_state_params : sem_state_params ≝
    1514  mk_sem_state_params
    1615    (list frame)
    1716    [ ]
    18     (register_env beval)
    19     (λ_.empty_map …).
     17    reg_sp
     18    reg_sp_init
     19    (λenv.OK … (stackp env))
     20    (λenv.mk_reg_sp env (* coercion*)).
    2021
    21 definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
     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.
    2228  match a with
    2329  [ Reg r ⇒ reg_retrieve env r
    24   | Imm b ⇒ return b
     30  | Imm b ⇒ OK … (BVByte b)
    2531  ].
    2632
    2733(*CSC: could we use here a dependent type to avoid the Error case? *)
    28 
    2934definition rtl_fetch_ra:
    30  RTL_state → res (RTL_state × cpointer) ≝
     35 RTL_state → res (RTL_state × program_counter) ≝
    3136 λst.
    32   match st_frms ? st with
     37 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
     38   match frms with
    3339  [ nil ⇒ Error ? [MSG EmptyStack]
    34   | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
     40  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉
     41  ].
    3542
    3643definition rtl_init_local :
    37  register → register_env beval → register_env beval
    38  λlocal,env.add … env local BVundef.
     44 register → reg_sp → reg_sp
     45 λlocal.reg_sp_store … local BVundef.
    3946
    4047definition rtl_setup_call:
    4148 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
    4249  λstacksize,formal_arg_regs,actual_arg_regs,st.
    43   let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
     50  (* paolo: this will need to be changed: we want a unified stack in the whole backend *)
     51  let 〈mem,b〉 as E ≝ alloc … (m … st) 0 stacksize in
     52  let sp ≝ mk_pointer b (mk_offset (bv_zero …)) in
    4453  do new_regs ←
    4554   mfold_left2 …
    4655    (λlenv,dest,src.
    4756      do v ← rtl_arg_retrieve … (regs ? st) src ;
    48       OK … (add … lenv dest v))
    49     (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
     57      OK … (reg_sp_store dest v lenv))
     58    (OK … (reg_sp_init sp)) formal_arg_regs actual_arg_regs ;
    5059  OK …
    51    (set_regs RTL_state new_regs
    52     (set_m … mem
    53      (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
    54 cases b * #r #off #E >E %
     60   (set_regs RTL_state_params new_regs
     61    (set_m … mem st)).
     62cases daemon (* will probably change anyway *)
    5563qed.
    5664
    57 definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state.
    58   let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
    59   OK … (set_frms RTL_state frame st).
     65definition RTL_state_pc ≝ state_pc RTL_state_params.
     66
     67unification hint 0 ≔ ⊢ RTL_state ≡ state RTL_state_params.
     68unification hint 0 ≔ ⊢ RTL_state_pc ≡ state_pc RTL_state_params.
     69
     70definition rtl_save_frame ≝ λretregs.λst : RTL_state_pc.
     71 ! frms ← opt_to_res … [MSG … FrameErrorOnPush] (st_frms … st) ;
     72 let frame ≝ mk_frame retregs (pc ? st) (carry ? st) (regs ? st) :: frms in
     73  OK … (set_frms RTL_state_params frame st).
    6074
    6175(*CSC: XXXX, for external functions only*)
    62 axiom rtl_fetch_external_args: external_function → RTL_state → res (list val).
     76axiom rtl_fetch_external_args: external_function → RTL_state → list psd_argument → res (list val).
    6377axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
    6478
    65 definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
    66 definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
     79definition rtl_reg_store ≝ λr,v,st.
     80  let mem ≝ reg_sp_store r v (regs RTL_state_params st) in
     81  set_regs RTL_state_params mem st.
     82
     83definition rtl_reg_retrieve ≝ λst,l.reg_sp_retrieve (regs RTL_state_params st) l.
    6784
    6885definition rtl_read_result :
    69  ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
    70  λglobals,ge,rets,st.
     86 list register → RTL_state → res (list beval) ≝
     87 λrets,st.
    7188 m_list_map … (rtl_reg_retrieve st) rets.
    7289
     
    7592  saves the OutOfBounds exception *)
    7693definition rtl_pop_frame:
    77  ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state →
    78   res RTL_state ≝
    79  λglobals,ge,curr_fn,st.
    80   let ret ≝ joint_if_result … curr_fn in
    81   do ret_vals ← rtl_read_result … ge ret st ;
    82   match st_frms ? st with
     94 list register → RTL_state →
     95  res (RTL_state × program_counter) ≝
     96 λret,st.
     97 ! frms ← opt_to_res … [MSG … FrameErrorOnPop] (st_frms … st) ;
     98 match frms with
    8399  [ nil ⇒ Error ? [MSG EmptyStack]
    84100  | cons hd tl ⇒
    85      do st ←
    86       mfold_left_i …
    87        (λi.λst.λreg.
    88          do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
    89          rtl_reg_store reg v st)
    90        (OK … st) (fr_ret_regs hd) ;
    91      OK …
    92       (set_frms RTL_state tl
    93         (set_regs RTL_state (fr_regs hd)
    94          (set_sp … (fr_sp hd)
    95           (set_carry … (fr_carry hd)
    96            (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    97 
    98 (* This code is quite similar to eval_call_block: can we factorize it out? *)
    99 definition eval_tailcall_block:
    100  ∀globals.genv RTL globals → RTL_state →
    101   block → call_args RTL →
    102   (* this is where the result of the current function should be stored *)
    103   call_dest RTL →
    104   IO io_out io_in
    105     ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
    106  λglobals,ge,st,b,args,ret.
    107   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    108     match fd with
    109     [ Internal fd ⇒
    110       return 〈FTailInit ?? (block_id b) fd args, st〉
    111     | External fn ⇒
    112       ! params ← rtl_fetch_external_args … fn st : IO ???;
    113       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    114       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    115       (* CSC: XXX bug here; I think I should split it into Byte-long
    116          components; instead I am making a singleton out of it. To be
    117          fixed once we fully implement external functions. *)
    118       let vs ≝ [mk_val ? evres] in
    119       ! st ← rtl_set_result … vs ret st : IO ???;
    120       return 〈FEnd2 ??, st〉
    121     ].
     101    ! ret_vals ← rtl_read_result … ret st ;
     102    (* Paolo: no more OutOfBounds exception, but is it right? should be for
     103       compiled programs *)
     104    let reg_vals ≝ zip_pottier … (fr_ret_regs hd) ret_vals in
     105    let st ≝ foldl …
     106      (λst,reg_val.rtl_reg_store (\fst reg_val) (\snd reg_val) st)
     107      st reg_vals in
     108    ! sp ← sp … st ;  (* always succeeds in RTL *)
     109    let st ≝ set_frms RTL_state_params tl
     110        (set_regs RTL_state_params (fr_regs hd)
     111          (set_carry RTL_state_params (fr_carry hd)
     112            (set_m … (free … (m … st) (pblock sp)) st))) in
     113    let pc ≝ fr_pc hd in
     114    return 〈st, pc〉
     115  ].
    122116
    123117definition block_of_register_pair: register → register → RTL_state → res block ≝
     
    129123
    130124definition eval_rtl_seq:
    131  ∀globals. genv RTL globals →
    132   rtl_seq → joint_internal_function RTL globals → RTL_state →
    133    IO io_out io_in RTL_state ≝
    134  λglobals,ge,stm,curr_fn,st.
     125  rtl_seq → ident → RTL_state →
     126   res RTL_state ≝
     127 λstm,curr_fn,st.
    135128  match stm with
    136129   [ rtl_stack_address dreg1 dreg2  ⇒
    137       let sp ≝ sp ? st in
    138       ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
    139       ! st ← rtl_reg_store dreg1 dpl st ;
    140       rtl_reg_store dreg2 dph st
     130      ! sp ← sp ? st ; (* always succeeds in RTL *)
     131      let 〈dpl,dph〉 ≝ beval_pair_of_pointer sp in
     132      let st ≝ rtl_reg_store dreg1 dpl st in
     133      return rtl_reg_store dreg2 dph st
    141134   ].
    142135
    143 definition eval_rtl_call:
    144  ∀globals. genv RTL globals →
    145   rtl_call → RTL_state →
    146    IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
    147  λglobals,ge,stm,st.
    148   match stm with
    149   [ rtl_call_ptr r1 r2 args dest ⇒
    150     ! b ← block_of_register_pair r1 r2 st : IO ???;
    151     ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    152     match fd with
    153     [ Internal fd ⇒
    154       return 〈Init ?? (block_id b) fd args dest, st〉
    155     | External fn ⇒
    156       ! params ← rtl_fetch_external_args … fn st : IO ???;
    157       ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    158       ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    159       (* CSC: XXX bug here; I think I should split it into Byte-long
    160          components; instead I am making a singleton out of it. To be
    161          fixed once we fully implement external functions. *)
    162       let vs ≝ [mk_val ? evres] in
    163       ! st ← rtl_set_result … vs dest st : IO ???;
    164       return 〈Proceed ???, st〉
    165     ]
    166   ].
    167 
    168 definition eval_rtl_tailcall:
    169  ∀globals. genv RTL globals →
    170   rtl_tailcall → joint_internal_function RTL globals → RTL_state →
    171    IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
    172    λglobals,ge,stm,curr_fn,st.
    173    let ret ≝ joint_if_result … curr_fn in
    174    match stm with
    175    [ rtl_tailcall_id id args ⇒
    176       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    177       eval_tailcall_block … ge st b args ret
    178    | rtl_tailcall_ptr r1 r2 args ⇒
    179       ! b ← block_of_register_pair r1 r2 st : IO ???;
    180       eval_tailcall_block … ge st b args ret
    181    ].
     136(* for a store living in res *)
     137definition reg_res_store ≝ λr,v,s.OK ? (reg_sp_store r v s).
    182138
    183139definition RTL_semantics ≝
    184   make_sem_graph_params RTL
    185     (mk_more_sem_unserialized_params ??
    186       RTL_state
    187       reg_store reg_retrieve rtl_arg_retrieve
    188       reg_store reg_retrieve rtl_arg_retrieve
    189       reg_store reg_retrieve rtl_arg_retrieve
    190       reg_store reg_retrieve rtl_arg_retrieve
     140  mk_sem_graph_params RTL
     141    (λF.mk_sem_unserialized_params RTL F
     142      RTL_state_params
     143      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     144      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     145      reg_res_store reg_sp_retrieve rtl_arg_retrieve
     146      reg_res_store reg_sp_retrieve rtl_arg_retrieve
    191147      rtl_arg_retrieve
    192       (λenv,p. let 〈dest,src〉 ≝ p in
     148      (λenv : reg_sp.λp. let 〈dest,src〉 ≝ p in
    193149        ! v ← rtl_arg_retrieve env src ;
    194         reg_store dest v env)
    195       rtl_fetch_ra
    196       rtl_init_local
    197       rtl_save_frame
     150        return reg_sp_store dest v env)
     151      (λ_.rtl_save_frame)
    198152      rtl_setup_call
    199153      rtl_fetch_external_args
    200154      rtl_set_result
    201155      [ ] [ ]
    202       rtl_read_result
    203       eval_rtl_seq
    204       eval_rtl_tailcall
    205       eval_rtl_call
    206       rtl_pop_frame
    207       (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).
     156      (λ_.λ_.rtl_read_result) 
     157      (λ_.λ_.eval_rtl_seq)
     158      (λ_.λ_.λ_.rtl_pop_frame)).
Note: See TracChangeset for help on using the changeset viewer.