Changeset 2286 for src/RTL/semantics.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r2176 r2286  
    66record frame: Type[0] ≝
    77 { fr_ret_regs: list register
    8  ; fr_pc: address
    9  ; fr_sp: pointer
    10  ; fr_carry: beval
     8 ; fr_pc: cpointer
     9 ; fr_sp: xpointer
     10 ; fr_carry: bebit
    1111 ; fr_regs: register_env beval
    1212 }.
    1313
    14 definition rtl_more_sem_params: more_sem_params rtl_params_ :=
    15  mk_more_sem_params rtl_params_
    16   (list frame) [] (register_env beval) (λ_.empty_map …) [] [](*dummy*)
    17    reg_store reg_retrieve reg_store reg_retrieve reg_store reg_retrieve
    18     reg_store reg_retrieve reg_store reg_retrieve
    19      (λlocals,dest_src.
    20        do v ← reg_retrieve locals (\snd dest_src) ;
    21        reg_store (\fst dest_src) v locals).
    22 definition rtl_sem_params: sem_params ≝ mk_sem_params … rtl_more_sem_params.
    23 
    24 definition rtl_init_locals :
    25  list register → register_env beval → register_env beval ≝
    26  λlocals,env.
    27   foldl ?? (λlenv,reg. add … lenv reg BVundef) env locals.
     14definition RTL_state : sem_state_params ≝
     15  mk_sem_state_params
     16    (list frame)
     17    [ ]
     18    (register_env beval)
     19    (λ_.empty_map …).
     20
     21definition rtl_arg_retrieve : ?→?→res ? ≝ λenv.λa : psd_argument.
     22  match a with
     23  [ Reg r ⇒ reg_retrieve env r
     24  | Imm b ⇒ return b
     25  ].
    2826
    2927(*CSC: could we use here a dependent type to avoid the Error case? *)
     
    3230
    3331definition rtl_fetch_ra:
    34  state … rtl_sem_params → res ((state … rtl_sem_params) × address) ≝
     32 RTL_state → res (RTL_state × cpointer) ≝
    3533 λst.
    3634  match st_frms ? st with
     
    3836  | cons hd tl ⇒ OK … 〈st, fr_pc hd〉 ].
    3937
    40 definition rtl_result_regs:
    41  ∀globals. genv … (rtl_params globals) → state rtl_sem_params → res (list register) ≝
    42  λglobals,ge,st.
    43   do fn ← graph_fetch_function … globals ge st ;
    44   OK … (joint_if_result … fn).
    45 
    46 (*CSC: we could use a dependent type here: the list of return values should have
    47   the same length of the list of return registers that store the values. This
    48   saves the OutOfBounds exception *)
    49 definition rtl_pop_frame:
    50  ∀globals. genv … (rtl_params globals) → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    51  λglobals,ge,st.
    52   do ret_regs ← rtl_result_regs … ge st ;
    53   do ret_vals ← mmap … (λreg.greg_retrieve rtl_sem_params st reg) ret_regs ;
    54   match st_frms ? st with
    55   [ nil ⇒ Error ? [MSG EmptyStack]
    56   | cons hd tl ⇒
    57      do st ←
    58       mfold_left_i ??
    59        (λi.λst.λreg.
    60          do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
    61          greg_store rtl_sem_params reg v st)
    62        (OK … st) (fr_ret_regs hd) ;
    63      OK …
    64       (set_frms rtl_sem_params tl
    65         (set_regs rtl_sem_params (fr_regs hd)
    66          (set_sp … (fr_sp hd)
    67           (set_carry … (fr_carry hd)
    68            (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    69 
    70 definition rtl_call_function:
    71  nat → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
     38definition rtl_init_local :
     39 register → register_env beval → register_env beval ≝
     40 λlocal,env.add … env local BVundef.
     41
     42definition rtl_setup_call:
     43 nat → list register → list psd_argument → RTL_state → res RTL_state ≝
    7244  λstacksize,formal_arg_regs,actual_arg_regs,st.
    7345  let 〈mem,b〉 ≝ alloc … (m … st) 0 stacksize XData in
     
    7547   mfold_left2 …
    7648    (λlenv,dest,src.
    77       do v ← greg_retrieve … st src ;
     49      do v ← rtl_arg_retrieve … (regs ? st) src ;
    7850      OK … (add … lenv dest v))
    7951    (OK … (empty_map …)) formal_arg_regs actual_arg_regs ;
    8052  OK …
    81    (set_regs rtl_sem_params new_regs
     53   (set_regs RTL_state new_regs
    8254    (set_m … mem
    83      (set_sp … (mk_pointer b (mk_offset 0)) st))).
    84 (*cases b * #r #off #E >E %
    85 qed.*)
    86 
    87 definition rtl_save_frame:
    88  address → nat → list register → list register → list register → state … rtl_sem_params → res (state … rtl_sem_params) ≝
    89  λl,stacksize,formal_arg_regs,actual_arg_regs,retregs,st.
    90   let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs … st) :: (st_frms … st) in
    91   let st ≝ set_frms rtl_sem_params frame st in
    92   rtl_call_function stacksize formal_arg_regs actual_arg_regs st.
     55     (set_sp … (mk_pointer b (mk_offset (bv_zero …))) st))).
     56cases b * #r #off #E >E %
     57qed.
     58
     59definition rtl_save_frame ≝ λl.λretregs.λst : RTL_state.
     60  let frame ≝ mk_frame retregs l (sp … st) (carry … st) (regs ? st) :: (st_frms … st) in
     61  OK … (set_frms RTL_state frame st).
    9362
    9463(*CSC: XXXX, for external functions only*)
    95 axiom rtl_fetch_external_args: external_function → state rtl_sem_params → res (list val).
    96 axiom rtl_set_result: list val → state rtl_sem_params → res (state rtl_sem_params).
    97 
    98 definition rtl_more_sem_params1: ∀globals. more_sem_params1 … (rtl_params globals) ≝
    99  λglobals.
    100   mk_more_sem_params1 … rtl_more_sem_params graph_succ_p (graph_pointer_of_label …)
    101    (graph_fetch_statement …) rtl_fetch_ra (rtl_result_regs …)
    102    rtl_init_locals rtl_save_frame (rtl_pop_frame …)
    103    rtl_fetch_external_args rtl_set_result.
    104 definition rtl_sem_params1: ∀globals. sem_params1 … globals ≝
    105  λglobals. mk_sem_params1 … (rtl_more_sem_params1 globals).
    106 
    107 definition block_of_register_pair: register → register → state rtl_sem_params → res block ≝
    108  λr1,r2,st.
    109  do v1 ← greg_retrieve rtl_sem_params st r1 ;
    110  do v2 ← greg_retrieve rtl_sem_params st r2 ;
    111  do ptr ← pointer_of_address 〈v1,v2〉 ;
    112  OK … (pblock ptr). 
     64axiom rtl_fetch_external_args: external_function → RTL_state → res (list val).
     65axiom rtl_set_result: list val → list register → RTL_state → res RTL_state.
     66
     67definition rtl_reg_store ≝ λr,v,st.! mem ← reg_store r v (regs RTL_state st) ; return set_regs RTL_state mem st.
     68definition rtl_reg_retrieve ≝ λst.reg_retrieve (regs RTL_state st).
     69
     70definition rtl_read_result :
     71 ∀globals.genv RTL globals → list register → RTL_state → res (list beval) ≝
     72 λglobals,ge,rets,st.
     73 m_list_map … (rtl_reg_retrieve st) rets.
     74
     75(*CSC: we could use a dependent type here: the list of return values should have
     76  the same length of the list of return registers that store the values. This
     77  saves the OutOfBounds exception *)
     78definition rtl_pop_frame:
     79 ∀globals. genv RTL globals → joint_internal_function RTL globals → RTL_state →
     80  res RTL_state ≝
     81 λglobals,ge,curr_fn,st.
     82  let ret ≝ joint_if_result … curr_fn in
     83  do ret_vals ← rtl_read_result … ge ret st ;
     84  match st_frms ? st with
     85  [ nil ⇒ Error ? [MSG EmptyStack]
     86  | cons hd tl ⇒
     87     do st ←
     88      mfold_left_i …
     89       (λi.λst.λreg.
     90         do v ← opt_to_res ? [MSG OutOfBounds] (nth_opt … i ret_vals) ;
     91         rtl_reg_store reg v st)
     92       (OK … st) (fr_ret_regs hd) ;
     93     OK …
     94      (set_frms RTL_state tl
     95        (set_regs RTL_state (fr_regs hd)
     96         (set_sp … (fr_sp hd)
     97          (set_carry … (fr_carry hd)
     98           (set_m … (free … (m … st) (pblock (sp … st))) st)))))].
    11399
    114100(* This code is quite similar to eval_call_block: can we factorize it out? *)
    115 definition eval_tail_call_block:
    116  ∀globals.genv … (rtl_params globals) → state rtl_sem_params →
    117   block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
    118  λglobals,ge,st,b,args.
    119   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b);
     101definition eval_tailcall_block:
     102 ∀globals.genv RTL globals → RTL_state →
     103  block → call_args RTL →
     104  (* this is where the result of the current function should be stored *)
     105  call_dest RTL →
     106  IO io_out io_in
     107    ((fin_step_flow RTL (joint_internal_function RTL globals) Call)×RTL_state) ≝
     108 λglobals,ge,st,b,args,ret.
     109  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
    120110    match fd with
    121     [ Internal fn ⇒
    122       let st ≝ set_m … (free … (m … st) (pblock (sp … st))) st in
    123       ! st ← rtl_call_function (joint_if_stacksize … fn) (joint_if_params … fn) args st ;
    124       let regs ≝ rtl_init_locals … (joint_if_locals … fn) (regs … st) in
    125       let l' ≝ joint_if_entry … fn in
    126       ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
    127        return 〈 E0, st〉
    128     | External fn ⇒ ?(*
    129       ! params ← fetch_external_args … fn st;
    130       ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     111    [ Internal fd ⇒
     112      return 〈FTailInit ?? (block_id b) fd args, st〉
     113    | External fn ⇒
     114      ! params ← rtl_fetch_external_args … fn st : IO ???;
     115      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    131116      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    132117      (* CSC: XXX bug here; I think I should split it into Byte-long
    133118         components; instead I am making a singleton out of it. To be
    134119         fixed once we fully implement external functions. *)
    135         let vs ≝ [mk_val ? evres] in
    136       ! st ← set_result … vs st;
    137       let st ≝ set_pc … ra st in
    138         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉 *)
    139      ].
    140 cases daemon (*CSC: XXX tailcall to external function not implemented yet;
    141                     it needs alls other functions on external calls *)
    142 qed.
    143 
    144 definition rtl_exec_extended:
    145  ∀globals. genv globals (rtl_params globals) →
    146   rtl_statement_extension → label → state rtl_sem_params →
    147    IO io_out io_in (trace × (state rtl_sem_params)) ≝
    148  λglobals,ge,stm,l,st.
     120      let vs ≝ [mk_val ? evres] in
     121      ! st ← rtl_set_result … vs ret st : IO ???;
     122      return 〈FEnd2 ??, st〉
     123    ].
     124
     125definition block_of_register_pair: register → register → RTL_state → res block ≝
     126 λr1,r2,st.
     127 do v1 ← rtl_reg_retrieve st r1 ;
     128 do v2 ← rtl_reg_retrieve st r2 ;
     129 do ptr ← pointer_of_address 〈v1,v2〉 ;
     130 OK … (pblock ptr). 
     131
     132definition eval_rtl_seq:
     133 ∀globals. genv RTL globals →
     134  rtl_seq → joint_internal_function RTL globals → RTL_state →
     135   IO io_out io_in RTL_state ≝
     136 λglobals,ge,stm,curr_fn,st.
    149137  match stm with
    150    [ rtl_st_ext_stack_address dreg1 dreg2  ⇒
     138   [ rtl_stack_address dreg1 dreg2  ⇒
    151139      let sp ≝ sp ? st in
    152140      ! 〈dpl,dph〉 ← beval_pair_of_pointer sp ;
    153       ! st ← greg_store rtl_sem_params dreg1 dpl st ;
    154       ! st ← greg_store rtl_sem_params dreg2 dph st ;
    155       ! st ← next … (rtl_sem_params1 globals) l st ;
    156        return 〈E0, st〉
    157    | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    158       ! b ← block_of_register_pair r1 r2 st : IO ??? ;
    159       ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) : IO ??? ;
    160       eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
    161        ge st b args dest ra
    162    | rtl_st_ext_tailcall_id id args ⇒
     141      ! st ← rtl_reg_store dreg1 dpl st ;
     142      rtl_reg_store dreg2 dph st
     143   ].
     144
     145definition eval_rtl_call:
     146 ∀globals. genv RTL globals →
     147  rtl_call → RTL_state →
     148   IO io_out io_in ((step_flow RTL ? Call)×RTL_state) ≝
     149 λglobals,ge,stm,st.
     150  match stm with
     151  [ rtl_call_ptr r1 r2 args dest ⇒
     152    ! b ← block_of_register_pair r1 r2 st : IO ???;
     153    ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ? ge b) : IO ? io_in ?);
     154    match fd with
     155    [ Internal fd ⇒
     156      return 〈Init ?? (block_id b) fd args dest, st〉
     157    | External fn ⇒
     158      ! params ← rtl_fetch_external_args … fn st : IO ???;
     159      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
     160      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     161      (* CSC: XXX bug here; I think I should split it into Byte-long
     162         components; instead I am making a singleton out of it. To be
     163         fixed once we fully implement external functions. *)
     164      let vs ≝ [mk_val ? evres] in
     165      ! st ← rtl_set_result … vs dest st : IO ???;
     166      return 〈Proceed ???, st〉
     167    ]
     168  ].
     169
     170definition eval_rtl_tailcall:
     171 ∀globals. genv RTL globals →
     172  rtl_tailcall → joint_internal_function RTL globals → RTL_state →
     173   IO io_out io_in ((fin_step_flow RTL ? Call)×RTL_state) ≝
     174   λglobals,ge,stm,curr_fn,st.
     175   let ret ≝ joint_if_result … curr_fn in
     176   match stm with
     177   [ rtl_tailcall_id id args ⇒
    163178      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    164       eval_tail_call_block … ge st b args
    165    | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
     179      eval_tailcall_block … ge st b args ret
     180   | rtl_tailcall_ptr r1 r2 args ⇒
    166181      ! b ← block_of_register_pair r1 r2 st : IO ???;
    167       eval_tail_call_block … ge st b args
     182      eval_tailcall_block … ge st b args ret
    168183   ].
    169184
    170 definition rtl_more_sem_params2: ∀globals. more_sem_params2 … (rtl_params globals) ≝
    171  λglobals. mk_more_sem_params2 … (rtl_more_sem_params1 globals) (rtl_exec_extended …).
    172 
    173 definition rtl_fullexec ≝
    174  joint_fullexec … (λp. rtl_more_sem_params2 (prog_var_names … p)).
     185definition RTL_semantics ≝
     186  make_sem_graph_params RTL
     187    (mk_more_sem_unserialized_params ??
     188      RTL_state
     189      reg_store reg_retrieve rtl_arg_retrieve
     190      reg_store reg_retrieve rtl_arg_retrieve
     191      reg_store reg_retrieve rtl_arg_retrieve
     192      reg_store reg_retrieve rtl_arg_retrieve
     193      rtl_arg_retrieve
     194      (λenv,p. let 〈dest,src〉 ≝ p in
     195        ! v ← rtl_arg_retrieve env src ;
     196        reg_store dest v env)
     197      rtl_fetch_ra
     198      rtl_init_local
     199      rtl_save_frame
     200      rtl_setup_call
     201      rtl_fetch_external_args
     202      rtl_set_result
     203      [ ] [ ]
     204      rtl_read_result
     205      eval_rtl_seq
     206      eval_rtl_tailcall
     207      eval_rtl_call
     208      rtl_pop_frame
     209      (λ_.λ_.λ_.λ_.λ_.λ_.λst.st)).
Note: See TracChangeset for help on using the changeset viewer.