Ignore:
Timestamp:
Sep 3, 2011, 4:17:48 AM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semantics.ma

    r1174 r1176  
    1 
    2 (* XXX NB: I haven't checked all of these semantics against the prototype
    3            compilers yet! *)
    4 
    51include "utilities/lists.ma".
    6 
    7 include "common/Errors.ma".
    82include "common/Globalenvs.ma".
    93include "common/IO.ma".
    104include "common/SmallstepExec.ma".
    11 
    125include "joint/Joint.ma".
    136(*
     
    4639*)
    4740(* CSC: ??? *)
    48 axiom address_of_label: mem → label → address.
    49 axiom address_chunks_of_label: mem → label → Byte × Byte.
    50 (*
     41axiom address_of_label: ∀p. mem → next p → address.
     42axiom address_chunks_of_label: ∀p. mem → next p → Byte × Byte.
    5143axiom label_of_address_chunks: Byte → Byte → label.
    52 *)
    5344axiom address_of_address_chunks: Byte → Byte → address.
    5445(*
    5546axiom address_chunks_of_address: address → Byte × Byte. (* CSC: only to shift the hwsp *)
    5647*)
     48(*
    5749axiom mRegisterMap: Type[0]. (* CSC: use the one in I8051? *)
    5850axiom hwreg_retrieve : mRegisterMap → Register → res val.
    5951axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    60 (*
    61 definition genv ≝ λglobals. (genv_t Genv) (fundef (ltl_internal_function globals)).
    62 *)
    63 (* CSC: frame reduced to this
    64 definition frame: Type[0] ≝ unit.
    6552*)
    6653
     
    6956 ; framesT: Type[0]
    7057 ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
     58 
    7159 ; pop_frame_: framesT → res framesT
    7260 ; save_frame_: framesT → regsT → framesT
     
    9381 }.
    9482
     83definition genv ≝ λglobals,pre,p. (genv_t Genv) (joint_function globals pre p).
     84
     85record sem_params2 (globals: list ident): Type[1] ≝
     86 { sparams:> sem_params
     87 ; pre_sem_params:> sem_params_ sparams globals
     88 ; exec_extended: genv … pre_sem_params → extend_statements sparams → state sparams → IO io_out io_in (trace × (state sparams))
     89 }.
     90
    9591definition set_m: ∀p. mem → state p → state p ≝
    9692 λp,m,st. mk_state p (st_frms … st) (pc … st) (sp … st) (carry … st) (regs … st) m.
     
    112108
    113109(* CSC: was build_state in RTL *)
    114 definition goto: ∀p. label → state p → state p ≝
    115  λp,l,st. set_pc … (address_of_label (m … st) l) st.
     110definition goto: ∀p:sem_params. next p → state p → state p ≝
     111 λp,l,st. set_pc … (address_of_label (m … st) l) st.
    116112
    117113definition greg_store: ∀p:sem_params. generic_reg p → val → state p → res (state p) ≝
     
    194190   (λv. bind ?? (Byte_of_val v) (λv. OK ? 〈st,v〉)).
    195191
    196 definition save_ra : ∀p. state p → label → res (state p) ≝
     192definition save_ra : ∀p. state p → next p → res (state p) ≝
    197193 λp,st,l.
    198   let 〈addrl,addrh〉 ≝ address_chunks_of_label (m … st) l in
     194  let 〈addrl,addrh〉 ≝ address_chunks_of_label (m … st) l in
    199195  (* No monadic notation here *)
    200196  bind ?? (push … st addrl) (λst.push … st addrh).
    201197
    202 (*
    203 (*CSC: unused now
    204 definition fetch_ra : state → res (state × label) ≝
    205  λst.
     198definition fetch_ra : ∀p.state p → res (state p × label) ≝
     199 λp,st.
    206200  (* No monadic notation here *)
    207   bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
    208   bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
    209    OK ? 〈st, label_of_address_chunks addrl addrh〉)). *)
    210 *)
     201  bind ?? (pop st) (λres. let 〈st,addrh〉 ≝ res in
     202  bind ?? (pop st) (λres. let 〈st,addrl〉 ≝ res in
     203   OK ? 〈st, label_of_address_chunks addrl addrh〉)).
     204
    211205(*CSC: To be implemented *)
    212 
    213 (*
    214 axiom fetch_statement: ∀globals: list ident. state → res (ltl_statement globals). (* CSC *)
     206axiom fetch_statement: ∀p.∀globals: list ident. state p → res (joint_statement p globals).
     207(*
    215208axiom fetch_function: ∀globals: list ident. state → res (ltl_internal_function globals). (* CSC *)
    216209*)
    217210
     211(*
    218212definition init_locals : ∀p.list register → regsT p ≝
    219213foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
     214*)
    220215
    221216(*
     
    235230axiom BadFunction : String.
    236231
    237 (*
    238232(*CSC: to be implemented *)
    239 axiom fetch_external_args: external_function → state → res (list val).(* ≝
     233axiom fetch_external_args: ∀p. external_function → state p → res (list val). (* ≝
    240234 λfn,st.
    241235  let registerno ≝ ? fn in
     
    244238    (λr. hwreg_retrieve (regs st) r) (prefix … registersno RegisterParameters);
    245239  (* CSC: HERE WE NEED TO RETRIEVE THE REMAINING REGISTERS FROM THE STACK! *)
    246   ?.*)
     240  ?.
     241*)
     242
    247243
    248244(*CSC: to be implemented; fails if the first list is longer *)
     
    253249
    254250(* CSC: the list should be a vector or have an upper bounded length *)
    255 definition set_result: list val → state → res state ≝
    256  λvs,st.
     251(*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX *)
     252axiom set_result: ∀p. list val → state p → res (state p).
     253(* λp,vs,st.
    257254  (* CSC: monadic notation not used *)
    258255  bind ?? (
    259256   fold_left2_first_not_longer …
    260     (λregs,v,reg. hwreg_store reg v regs) (regs st) vs RegisterRets)
    261   (λregs.OK ? (set_regs regs st)).
    262 
     257    (λregs,v,reg. hwreg_store reg v regs) (regs … st) vs RegisterRets)
     258  (λregs.OK ? (set_regs … regs st)).
     259*)
     260
     261(*
    263262definition fetch_result: state → nat → res (list val) ≝
    264263 λst,registersno.
     
    295294*)
    296295
    297 definition eval_statement : ∀p:sem_params.∀globals: list ident. ?(*(genv globals)*) → state p → joint_statement … p globals → IO io_out io_in (trace × (state p)) ≝
    298   λp,globals. λge,st,s.
    299 (* CSC: fixme
    300   ! s ← fetch_statement globals st;
    301 *)
     296(*CSC: move elsewhere *)
     297definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
     298 λA,P,c. match c with [ dp w _ ⇒ w ].
     299coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
     300
     301definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv … (pre_sem_params … p) → state p → IO io_out io_in (trace × (state p)) ≝
     302  λglobals,p. λge,st.
     303  ! s ← fetch_statement p globals st;
    302304  match s with
    303305    [ joint_st_goto l ⇒ ret ? 〈E0, goto … l st〉
     
    342344        ! v1 ← acca_retrieve … st acc_a;
    343345        ! v1 ← Byte_of_val v1;
    344         ! v2 ← greg_retrieve … src;
     346        ! v2 ← greg_retrieve … st src;
    345347        ! v2 ← Byte_of_val v2;
    346348        ! carry ← eval_bool_of_val (carry … st);
     
    374376      | joint_instr_move dst_src ⇒
    375377          ret ? 〈E0, goto … l (pair_reg_move … st dst_src)〉
    376       | joint_instr_call_id id argsno ⇒ (* CSC: only the number of args kept, no return reg *)
     378      | joint_instr_call_id id argsno ⇒
    377379        ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    378380        ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    379381          match fd with
    380382          [ Internal fn ⇒
    381             ! st ← save_ra st l;
     383            ! st ← save_ra st l;
    382384              let st ≝ save_frame … st in
    383               let regs ≝ init_locals … (ertl_if_locals globals fn) in
    384               let l' ≝ ertl_if_entry globals fn in
    385               ret ? 〈 E0, goto … l' (set_regs … regs st)〉
     385              (*CSC: XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
     386              let regs ≝ init_locals … (ertl_if_locals globals fn) in *) let regs ≝ regs … st in
     387              let l' ≝ joint_if_entry … fn in
     388             ret ? 〈 E0, goto … l' (set_regs … regs st)〉
    386389          | External fn ⇒
    387             ! params ← fetch_external_args fn st;
     390            ! params ← fetch_external_args fn st;
    388391            ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    389392            ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     
    391394               components; instead I am making a singleton out of it *)
    392395              let vs ≝ [mk_val ? evres] in
    393             ! st ← set_result vs st;
    394               ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     396            ! st ← set_result vs st;
     397              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
    395398          ]
    396399      ]
     
    401404        let pc ≝ address_of_address_chunks pcl pch in
    402405        ret ? 〈E0,set_pc … pc st〉
    403     | _ ⇒ ?
     406    | joint_st_extension c ⇒ exec_extended … p ge c st
    404407    ].
    405      
    406 axiom WrongReturnValueType: String.
    407408
    408409definition is_final: list ident → label → nat → state → option ((*CSC: why not res*) int) ≝
     
    412413  λst.
    413414 (* CSC: monadic notation missing here *)
    414   match fetch_statement globals st with
     415  match fetch_statement p globals st with
    415416  [ Error _ ⇒ None ?
    416417  | OK s ⇒
    417418    match s with
    418     [ ertl_st_lift_pre pre ⇒
    419       match pre with
    420419      [ joint_st_return ⇒
    421420        match fetch_ra st with
     
    435434      | _ ⇒ None ?
    436435      ]
    437     | _ ⇒ None ?
    438     ]
    439436  ].
    440437
Note: See TracChangeset for help on using the changeset viewer.