Changeset 1186


Ignore:
Timestamp:
Sep 5, 2011, 5:08:14 PM (8 years ago)
Author:
sacerdot
Message:

Spurious code removed.
joint_fullexec implemented up to make_initial_state and exit symbol/registersno
for main function.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1182 r1186  
    3232axiom val_of_address: address → val. (* CSC: only to shift the sp *)
    3333axiom address_of_val: val → address. (* CSC: only to shift the sp *)
    34 (*
    35 axiom addr_sub: address → nat → address.
    36 axiom addr_add: address → nat → address.
    37 *)
    3834(* CSC: ??? *)
    3935axiom address_of_label: mem → label → address.
     
    4137axiom label_of_address_chunks: Byte → Byte → label.
    4238axiom address_of_address_chunks: Byte → Byte → address.
    43 (*
    44 axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    45 *)
    46 (*
    47 axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    48 axiom hwreg_retrieve : mRegisterMap → Register → res val.
    49 axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    50 *)
    5139
    5240record sem_params: Type[1] ≝
     
    6856 ; dph_retrieve_: regsT → dph_reg p → res val
    6957 ; pair_reg_move_: regsT → pair_reg p → regsT
     58 
     59 ; init_locals : localsT p → regsT
    7060 }.
    7161
     
    8474 { sparams:> sem_params
    8575 ; pre_sem_params:> sem_params_ sparams globals
     76 
     77 ; fetch_statement: state sparams → res (joint_statement sparams globals)
     78 ; fetch_external_args: external_function → state sparams → res (list val)
     79 ; set_result: list val → state sparams → res (state sparams)
     80 ; fetch_result: state sparams → nat → res (list val)
     81
    8682 ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
    8783 }.
     
    178174    OK ? (set_m ? m (set_sp … sp st))).
    179175
    180 
    181176definition pop: ∀p. state p → res (state p × Byte) ≝
    182177 λp,st.
     
    201196   OK ? 〈st, label_of_address_chunks addrl addrh〉)).
    202197
    203 (*CSC: To be implemented *)
    204 axiom fetch_statement: ∀p.∀globals: list ident. state p → res (joint_statement p globals).
    205 (*
    206 axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
    207 *)
    208 
    209 (*
    210 definition init_locals : ∀p.list register → regsT p ≝
    211 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
    212 *)
    213 
    214 (*
    215 definition reg_store ≝
    216 λreg,v,locals. update RegisterTag val locals reg v.
    217 
    218 axiom BadRegister : String.
    219 
    220 definition reg_retrieve : register_env val → register → res val ≝
    221 λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
    222 *)
    223 
    224198axiom MissingSymbol : String.
    225 
    226199axiom FailedLoad : String.
    227 
    228200axiom BadFunction : String.
    229 
    230 (*CSC: to be implemented *)
    231 axiom fetch_external_args: ∀p. external_function → state p → res (list val). (* ≝
    232  λfn,st.
    233   let registerno ≝ ? fn in
    234   ! vs ←
    235    mmap …
    236     (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
    237   (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
    238   ?.
    239 *)
    240 
    241 
    242 (*CSC: to be implemented; fails if the first list is longer *)
    243 axiom fold_left2_first_not_longer:
    244  ∀A,B,C:Type[0]. ∀f:(C → A → B → res C).
    245   ∀acc:C. ∀l1:list A. ∀l2: list B.
    246    res C.
    247 
    248 (* CSC: the list should be a vector or have an upper bounded length *)
    249 (*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
    250 axiom set_result: ∀p. list val → state p → res (state p).
    251 (* λp,vs,st.
    252   (* CSC: monadic notation not used *)
    253   bind ?? (
    254    fold_left2_first_not_longer …
    255     (λregs,v,reg. hwreg_store reg v regs) (regs … st) vs RegisterRets)
    256   (λregs.OK ? (set_regs … regs st)).
    257 *)
    258 
    259 (*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
    260 axiom fetch_result: ∀p. state p → nat → res (list val).
    261 (*
    262 definition fetch_result: state → nat → res (list val) ≝
    263  λst,registersno.
    264   let retregs ≝ prefix … registersno RegisterRets in
    265   mmap … (λr. hwreg_retrieve (regs st) r) retregs.
    266 
    267 definition framesize: list ident → state → res nat ≝
    268   λglobals: list ident.
    269   λst.
    270   (* CSC: monadic notation missing here *)
    271     bind ?? (fetch_function globals st) (λf.
    272     OK ? (ltl_if_stacksize globals f)).
    273 
    274 definition get_hwsp : state → res address ≝
    275  λst.
    276   (* CSC: monadic notation missing here *)
    277   bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λspl.
    278   (* CSC: monadic notation missing here *)
    279   bind ?? (Byte_of_val spl) (λspl.
    280   (* CSC: monadic notation missing here *)
    281   bind ?? (hwreg_retrieve (regs st) RegisterSPL) (λsph.
    282   (* CSC: monadic notation missing here *)
    283   bind ?? (Byte_of_val sph) (λsph.
    284   OK ? (address_of_address_chunks spl sph))))).
    285 
    286 definition set_hwsp : address → state → res state ≝
    287  λsp,st.
    288   let 〈spl,sph〉 ≝ address_chunks_of_address sp in
    289   (* CSC: monadic notation missing here *) 
    290   bind ?? (hwreg_store RegisterSPL (val_of_Byte spl) (regs st)) (λregs.
    291   (* CSC: monadic notation missing here *) 
    292   bind ?? (hwreg_store RegisterSPL (val_of_Byte sph) regs) (λregs.
    293   OK ? (set_regs regs st))).
    294 *)
    295201
    296202(*CSC: move elsewhere *)
     
    301207definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv … (pre_sem_params … p) → state p → IO io_out io_in (trace × (state p)) ≝
    302208  λglobals,p. λge,st.
    303   ! s ← fetch_statement p globals st;
     209  ! s ← fetch_statement globals p st;
    304210  match s with
    305211    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
     
    383289            ! st ← save_ra … st l;
    384290              let st ≝ save_frame … st in
    385               (*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
    386               let regs ≝ init_locals … (ertl_if_locals globals fn) in *) let regs ≝ regs … st in
     291              let regs ≝ init_locals p (joint_if_locals … fn) in
    387292              let l' ≝ joint_if_entry … fn in
    388293             ret ? 〈 E0, goto … l' (set_regs … regs st)〉
     
    407312    ].
    408313
    409 definition is_final: ∀p. list ident → label → nat → state p → option ((*CSC: why not res*) int) ≝
    410   λp.λglobals: list ident.
     314definition is_final: ∀globals:list ident. ∀p: sem_params2 globals. label → nat → state p → option ((*CSC: why not res*) int) ≝
     315  λglobals: list ident.
     316  λp.
    411317  λexit.
    412318  λregistersno.
    413319  λst.
    414320 (* CSC: monadic notation missing here *)
    415   match fetch_statement … globals st with
     321  match fetch_statement … st with
    416322  [ Error _ ⇒ None ?
    417323  | OK s ⇒
     
    440346  λexit.
    441347  λregistersno.
    442   mk_execstep ? ? ? ? (is_final p globals exit registersno) (m p) (eval_statement globals p).
    443 
    444 (* CSC: XXX the program type does not fit with the globalenv and init_mem
    445 definition make_initial_state : rtl_program → res (genv × state)
     348  mk_execstep ? ? ? ? (is_final globals p exit registersno) (m p) (eval_statement globals p).
     349
     350(* CSC: XXX the program type does not fit with the globalenv and init_mem *)
     351axiom make_initial_state : ∀globals:list ident.∀sparams: sem_params2 globals. joint_program … (pre_sem_params … sparams) → res ((genv … (pre_sem_params … sparams)) × (state sparams)).(*
    446352λp.
    447353  do ge ← globalenv Genv ?? p;
     
    451357  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    452358  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
    453 
    454 definition RTL_fullexec : fullexec io_out io_in ≝
    455   mk_fullexec … RTL_exec ? make_initial_state.
    456359*)
     360
     361definition joint_fullexec :
     362 ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
     363 λglobals,p,program.
     364  let exit ≝ ? in
     365  let registersno ≝ ? in
     366  mk_fullexec ?? (joint_exec ? p exit registersno) ? (make_initial_state … p).
Note: See TracChangeset for help on using the changeset viewer.