Changeset 1999


Ignore:
Timestamp:
May 25, 2012, 10:45:15 AM (5 years ago)
Author:
campbell
Message:

Make back-end use the main global envs.

Location:
src
Files:
1 deleted
7 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/semantics.ma

    r1451 r1999  
    117117  block → call_args rtl_sem_params → IO io_out io_in (trace×(state rtl_sem_params)) ≝
    118118 λglobals,ge,st,b,args.
    119   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
     119  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ge b);
    120120    match fd with
    121121    [ Internal fn ⇒
     
    125125      let l' ≝ joint_if_entry … fn in
    126126      ! st ← next … (rtl_sem_params1 …) l' (set_regs rtl_sem_params regs st) ;
    127        ret ? 〈 E0, st〉
     127       return 〈 E0, st〉
    128128    | External fn ⇒ ?(*
    129129      ! params ← fetch_external_args … fn st;
     
    154154      ! st ← greg_store rtl_sem_params dreg2 dph st ;
    155155      ! st ← next … (rtl_sem_params1 globals) l st ;
    156        ret ? 〈E0, st〉
     156       return 〈E0, st〉
    157157   | rtl_st_ext_call_ptr r1 r2 args dest ⇒
    158       ! b ← block_of_register_pair r1 r2 st ;
    159       ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) ;
     158      ! b ← block_of_register_pair r1 r2 st : IO ??? ;
     159      ! ra ← succ_pc … (rtl_more_sem_params1 globals) l (pc … st) : IO ??? ;
    160160      eval_call_block … (mk_sem_params1 … (rtl_more_sem_params1 globals))
    161161       ge st b args dest ra
    162162   | rtl_st_ext_tailcall_id id args ⇒
    163       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     163      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    164164      eval_tail_call_block … ge st b args
    165165   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
    166       ! b ← block_of_register_pair r1 r2 st ;
     166      ! b ← block_of_register_pair r1 r2 st : IO ???;
    167167      eval_tail_call_block … ge st b args
    168168   ].
  • src/RTL/semantics_paolo.ma

    r1643 r1999  
    170170   match stm with
    171171   [ rtl_st_ext_tailcall_id id args ⇒
    172       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
     172      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ge id) : IO ???;
    173173      eval_tail_call_block … ge st b args
    174174   | rtl_st_ext_tailcall_ptr r1 r2 args ⇒
  • src/RTLabs/semantics.ma

    r1988 r1999  
    133133(*
    134134  | St_tailcall_id id args ⇒ λH.
    135       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    136       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     135      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ge id);
     136      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ge b);
    137137      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    138138      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    139139  | St_tailcall_ptr frs args ⇒ λH.
    140140      ! fv ← reg_retrieve (locals f) frs;
    141       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
     141      ! fd ← opt_to_res … (msg BadFunction) (find_funct ge fv);
    142142      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    143143      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
  • src/common/Globalenvs.ma

    r1994 r1999  
    196196  \fst (globalenv_allocmem F V i p).
    197197
     198(* Return the global environment for the given program with no data initialisation. *)
     199definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝
     200λF,p.
     201  \fst (globalenv_allocmem F nat (λn.[Init_space n]) p).
     202
    198203(* Return the initial memory state for the given program. *)
    199204definition init_mem: ∀F,V. (V → list init_data) → program F V → res mem ≝
     
    201206  let 〈g,m〉 ≝ globalenv_allocmem F V i p in
    202207  init_globals ? V i g m (prog_vars ?? p).
     208
     209(* Setup memory when data initialisation is not required (has the benefit
     210   of being total. *)
     211definition alloc_mem: ∀F. program F nat → mem ≝
     212λF,p.
     213  \snd (globalenv_allocmem F nat (λn. [Init_space n]) p).
    203214
    204215(* Return the function description associated with the given address, if any. *)
  • src/joint/semantics.ma

    r1601 r1999  
    11include "basics/lists/list.ma".
    2 include "joint/BEGlobalenvs.ma".
     2include "common/Globalenvs.ma".
    33include "common/IO.ma".
    44include "common/SmallstepExec.ma".
     5include "joint/BEMem.ma".
    56include "joint/Joint.ma".
    67include "ASM/I8051bis.ma".
     
    5253*)
    5354
    54 definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
     55definition genv ≝ λglobals.λp:params globals. genv_t (joint_function globals p).
    5556
    5657record more_sem_params1 (globals: list ident) (p: params globals) : Type[1] ≝
     
    220221  block → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    221222 λglobals,p,ge,st,b,args,dest,ra.
    222   ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr ?? ge b);
     223  ! fd ← opt_to_res … [MSG BadPointer] (find_funct_ptr … ge b) : IO ???;
    223224    match fd with
    224225    [ Internal fn ⇒
     
    230231      ! newpc ← address_of_label … ge pointer_in_fn l' ;
    231232      let st ≝ set_pc … newpc st in
    232        ret ? 〈 E0, st〉
     233       return 〈 E0, st〉
    233234    | External fn ⇒
    234       ! params ← fetch_external_args … fn st;
    235       ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     235      ! params ← fetch_external_args … fn st : IO ???;
     236      ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???;
    236237      ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    237238      (* CSC: XXX bug here; I think I should split it into Byte-long
     
    241242      ! st ← set_result … vs st;
    242243      let st ≝ set_pc … ra st in
    243         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
     244        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), st〉
    244245     ].
    245246% qed.
     
    249250  ident → call_args p → call_dest p → address → IO io_out io_in (trace×(state p)) ≝
    250251 λglobals,p,ge,st,id,args,dest,ra.
    251   ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
     252  ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id) : IO ???;
    252253  eval_call_block … ge st b args dest ra.
    253  
     254
    254255definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
    255256 λglobals,p,ge,st.
    256   ! s ← fetch_statement … ge st;
    257   match s with
     257  ! s ← fetch_statement … ge st : IO ???;
     258  match s return λ_. IO ??? with
    258259    [ GOTO l ⇒
    259260       ! st ← goto … p ge l st ;
    260        ret ? 〈E0, st〉
     261       return 〈E0, st〉
    261262    | sequential seq l ⇒
    262       match seq with
     263      match seq return λ_. IO ??? with
    263264      [ extension c ⇒ exec_extended … p ge c l st
    264265      | COST_LABEL cl ⇒
    265266         ! st ← next … p l st ;
    266          ret ? 〈Echarge cl, st〉
     267         return 〈Echarge cl, st〉
    267268      | COMMENT c ⇒
    268269         ! st ← next … p l st ;
    269          ret ? 〈E0, st〉
     270         return 〈E0, st〉
    270271      | INT dest v ⇒
    271272         ! st ← greg_store p dest (BVByte v) st;
    272273         ! st ← next … p l st ;
    273           ret ? 〈E0, st〉
     274          return 〈E0, st〉
    274275      | LOAD dst addrl addrh ⇒
    275276        ! vaddrh ← dph_retrieve … st addrh;
     
    279280        ! st ← acca_store p … dst v st;
    280281        ! st ← next … p l st ;
    281           ret ? 〈E0, st〉
     282          return 〈E0, st〉
    282283      | STORE addrl addrh src ⇒
    283284        ! vaddrh ← dph_retrieve … st addrh;
     
    288289        let st ≝ set_m … m' st in
    289290        ! st ← next … p l st ;
    290           ret ? 〈E0, st〉
     291          return 〈E0, st〉
    291292      | COND src ltrue ⇒
    292293        ! v ← acca_retrieve … st src;
     
    294295        if b then
    295296         ! st ← goto … p ge ltrue st ;
    296          ret ? 〈E0, st〉
     297         return 〈E0, st〉
    297298        else
    298299         ! st ← next … p l st ;
    299          ret ? 〈E0, st〉
     300         return 〈E0, st〉
    300301      | ADDRESS ident prf ldest hdest ⇒
    301         ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ?? ge ident);
     302        ! addr ← opt_to_res ? [MSG MissingSymbol; CTX … ident] (find_symbol ge ident);
    302303        ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset);
    303304        ! st ← dpl_store p ldest laddr st;
    304305        ! st ← dph_store p hdest haddr st;
    305306        ! st ← next … p l st ;
    306           ret ? 〈E0, st〉
     307          return 〈E0, st〉
    307308      | OP1 op dacc_a sacc_a ⇒
    308309        ! v ← acca_retrieve … st sacc_a;
     
    311312        ! st ← acca_store p dacc_a v' st;
    312313        ! st ← next … p l st ;
    313           ret ? 〈E0, st〉
     314          return 〈E0, st〉
    314315      | OP2 op dacc_a sacc_a src ⇒
    315316        ! v1 ← acca_retrieve … st sacc_a;
     
    324325          let st ≝ set_carry … carry st in
    325326        ! st ← next … p l st ;
    326           ret ? 〈E0, st〉
     327          return 〈E0, st〉
    327328      | CLEAR_CARRY ⇒
    328329        ! st ← next … p l (set_carry … BVfalse st) ;
    329          ret ? 〈E0, st〉
     330         return 〈E0, st〉
    330331      | SET_CARRY ⇒
    331332        ! st ← next … p l (set_carry … BVtrue st) ;
    332          ret ? 〈E0, st〉
     333         return 〈E0, st〉
    333334      | OPACCS op dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    334335        ! v1 ← acca_retrieve … st sacc_a_reg;
     
    342343        ! st ← accb_store p dacc_b_reg v2' st;
    343344        ! st ← next … p l st ;
    344           ret ? 〈E0, st〉
     345          return 〈E0, st〉
    345346      | POP dst ⇒
    346347        ! 〈st,v〉 ← pop … st;
    347348        ! st ← acca_store p dst v st;
    348349        ! st ← next … p l st ;
    349           ret ? 〈E0, st〉
     350          return 〈E0, st〉
    350351      | PUSH src ⇒
    351352        ! v ← acca_retrieve … st src;
    352353        ! st ← push … st v;
    353354        ! st ← next … p l st ;
    354           ret ? 〈E0, st〉
     355          return 〈E0, st〉
    355356      | MOVE dst_src ⇒
    356357        ! st ← pair_reg_move … st dst_src ;
    357358        ! st ← next … p l st ;
    358           ret ? 〈E0, st〉
     359          return 〈E0, st〉
    359360      | CALL_ID id args dest ⇒
    360         ! ra ← succ_pc … p l (pc … st) ;         
     361        ! ra ← succ_pc … p l (pc … st) : IO ???;         
    361362          eval_call_id … p ge st id args dest ra ]
    362363    | RETURN ⇒
    363364      ! 〈st,ra〉 ← fetch_ra … st;
    364365      ! st ← pop_frame … ge st;
    365         ret ? 〈E0,set_pc … ra st〉].
     366        return 〈E0,set_pc … ra st〉].
    366367cases addr //
    367368qed.
     
    402403 let ptr ≝ mk_pointer Code b ? (mk_offset 0) in
    403404 let addr ≝ address_of_code_pointer ptr in
    404   (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv Genv … p)).
     405  (λp. mk_evaluation_parameters (prog_var_names … p) (mk_sem_params2 … (sparams p)) addr (globalenv_noinit … p)).
    405406% qed.
    406407
     
    412413  let sem_globals ≝ make_global pars sparams p in
    413414  let ge ≝ genv2 sem_globals in
    414   let m ≝ init_mem Genv … p in
     415  let m ≝ alloc_mem … p in
    415416  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    416417  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
  • src/joint/semantics_blocks.ma

    r1949 r1999  
    189189[ #id #args #dest #H whd in H;
    190190  #st change with (! x ← ? ; ?) in match (eval_step ?????);
    191   elim (find_symbol ????) in H ⊢ %; [//]
     191  elim (find_symbol ???) in H ⊢ %; [//]
    192192  #b >m_return_bind  >m_return_bind
    193193  change with (! x ← ? ; ?) in match (eval_call_block ?????????);
    194   elim (find_funct_ptr ????) [//]
     194  elim (find_funct_ptr ???) [//]
    195195  #fd >m_return_bind  >m_return_bind
    196196  elim fd #fn normalize nodelta *
  • src/joint/semantics_paolo.ma

    r1976 r1999  
    11include "basics/lists/list.ma".
    2 include "joint/BEGlobalenvs.ma".
     2include "common/Globalenvs.ma".
    33include "common/IO.ma".
    44include "common/SmallstepExec.ma".
     5include "joint/BEMem.ma".
    56include "joint/Joint_paolo.ma".
    67include "ASM/I8051bis.ma".
     
    1112   only the head is kept (or Undef if the list is empty) ??? *)
    1213
    13 definition genv ≝ λglobals.λp:params. genv_t Genv (joint_function globals p).
     14definition genv ≝ λglobals.λp:params. genv_t (joint_function globals p).
    1415definition cpointer ≝ Σp.ptype p = Code.
    1516definition xpointer ≝ Σp.ptype p = XData.
     
    233234    IO io_out io_in ((step_flow p globals lbls)×(state p')) ≝
    234235 λglobals,p,p',lbls,ge,st,b,args,dest.
    235   ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge b) : IO ? io_in ?);
     236  ! fd ← (opt_to_res ? [MSG BadPointer] (find_funct_ptr ge b) : IO ? io_in ?);
    236237    match fd with
    237238    [ Internal fn ⇒
     
    450451      return 〈Proceed ???, st〉
    451452  | ADDRESS ident prf ldest hdest ⇒
    452     let addr ≝ opt_safe ? (find_symbol ?? ge ident) ? in
     453    let addr ≝ opt_safe ? (find_symbol ge ident) ? in
    453454    ! 〈laddr,haddr〉 ← address_of_pointer (mk_pointer (block_region addr) addr ? zero_offset) ;
    454455    ! st' ← dpl_store … ldest laddr st;
     
    502503    return 〈Proceed ???, st〉
    503504  | CALL_ID id args dest ⇒
    504     ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id) : IO ???;
     505    ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ge id) : IO ???;
    505506    eval_call_block … ge st b args dest
    506507  ].
     
    645646    (mk_sem_params … pars)
    646647    ptr
    647     (globalenv Genv … p)
     648    (globalenv_noinit … p)
    648649  ).
    649650% qed.
     
    657658  let sem_globals ≝ make_global pars p in
    658659  let ge ≝ genv2 sem_globals in
    659   let m ≝ init_mem Genv … p in
     660  let m ≝ alloc_mem … p in
    660661  let 〈m,spb〉 ≝ alloc … m 0 external_ram_size XData in
    661662  let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in
     
    668669  let st0' ≝ set_frms ? (save_frame … (exit sem_globals) (call_dest_for_main … pars) st0) st0 in
    669670  let st_pc0 ≝ mk_state_pc ? st0' dummy_pc in
    670   ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ?? ge main) ;
    671   ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ?? ge main_block) ;
     671  ! main_block ← opt_to_res … [MSG MissingSymbol; CTX ? main] (find_symbol ge main) ;
     672  ! main_fd ← opt_to_res ? [MSG BadPointer] (find_funct_ptr ge main_block) ;
    672673  match main_fd with
    673674  [ Internal fn ⇒
Note: See TracChangeset for help on using the changeset viewer.