Changeset 1137


Ignore:
Timestamp:
Aug 29, 2011, 6:27:16 PM (8 years ago)
Author:
sacerdot
Message:

More progress.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/semantics.ma

    r1130 r1137  
    7474 λpc,st. mk_state (st_frms st) pc (sp st) (locals st) (carry st) (regs st) (m st).
    7575
     76(* CSC: was build_state in RTL *)
    7677definition goto: label → state → state ≝
    7778 λl,st. set_pc (address_of_label (m st) l) st.
    7879
     80(* pushes the locals (i.e. the current frame) on top of the frames list *)
     81definition save_frame: state → state ≝
     82 λst. mk_state (locals st::st_frms st) (pc st) (sp st) (locals st) (carry st) (regs st) (m st).
     83
     84definition push: state → Byte → state ≝
     85 λst,v.
     86
     87definition pop: state → state × Byte ≝
     88 λst.
     89
     90definition save_ra : state → ? → state ≝
     91 λst,l.
     92  let 〈addrl,addrh〉 ≝ ? l in
     93  let st ≝ push st addrl in
     94  let st ≝ push st addrh in
     95   st.
     96
     97definition fetch_ra : state → state × ? ≝
     98 λst.
     99  let 〈st,addrh〉 ≝ pop st in
     100  let 〈st,addrl〉 ≝ pop st in
     101   〈st, ? addrl addrh〉.
     102
    79103(*CSC: To be implemented *)
    80104axiom fetch_statement: state → res ertl_statement.
    81105
    82 (*
    83 definition mem_of_state : state → mem ≝
    84 λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
    85 
    86 definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
    87 
    88 (* CSC: modified to take in input a list of registers (untyped) *)
    89106definition init_locals : list register → register_env val ≝
    90107foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
    91 *)
    92108
    93109definition reg_store ≝
     
    114130(*
    115131axiom FailedOp : String.
     132*)
    116133axiom MissingSymbol : String.
    117 
     134(*
    118135axiom MissingStatement : String.
    119136axiom FailedConstant : String. *)
    120137axiom FailedLoad : String.
    121138axiom FailedStore : String.
    122 (*axiom BadFunction : String.
    123 axiom BadJumpTable : String.
     139axiom BadFunction : String.
     140(*axiom BadJumpTable : String.
    124141axiom BadJumpValue : String.
    125142axiom FinalState : String.
     
    192209  | ertl_st_set_carry l ⇒
    193210    ret ? 〈E0, goto l (set_carry Vtrue st)〉
    194 
    195211     
    196212  (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
     
    214230     ret ? 〈E0, goto l (set_regs regs st)〉
    215231
    216   (* CSC: Dropped: rtl_st_stackaddr (becomes two get_hdw) *)
    217 
    218   | _ ⇒ ? ]
    219 (*
    220   | rtl_st_call_id id args dst l ⇒
     232  (* CSC: Dropped:
     233      - rtl_st_stackaddr (becomes two get_hdw)
     234      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
     235      - rtl_st_call_ptr (unimplemented ATM) *)
     236     
     237  (* CSC: changed, where the meat is *)
     238  | ertl_st_call_id id argsno l ⇒ (* CSC: only the number of args kept, no return reg *)
    221239      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    222240      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
     241      match fd with
     242      [ Internal fn ⇒
     243        let st ≝ save_ra st l in
     244        let st ≝ save_frame st in
     245        let locals ≝ init_locals (ertl_if_locals fn) in
     246        let pc ≝ ertl_if_entry fn in
     247         goto pc (set_locals locals st)
     248      | External fn ⇒ ? (*
     249        ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
     250        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
     251        (* CSC: return type changed from option to list *)
     252        ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉 *)
     253      ]
     254(*     
     255     
    223256      ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    224257      ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    225   | rtl_st_call_ptr lfrs hfrs args dst l ⇒ (* CSC: pairs of regs vs reg *)
    226       ! hfv ← reg_retrieve (locals f) hfrs;
    227       ! lfv ← reg_retrieve (locals f) lfrs;
    228       ! fv  ← smerge lfv hfv;
    229       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    230       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    231       ret ? 〈E0, Callstate fd vs dst (adv l f::fs) m〉
    232   | rtl_st_tailcall_id id args ⇒
    233       ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    234       ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr ?? ge b);
    235       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    236       ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
    237   | rtl_st_tailcall_ptr lfrs hfrs args ⇒ (* CSC: pairs of regs vs reg *)
    238       ! hfv ← reg_retrieve (locals f) hfrs;
    239       ! lfv ← reg_retrieve (locals f) lfrs;
    240       ! fv  ← smerge lfv hfv;
    241       ! fd ← opt_to_res … (msg BadFunction) (find_funct ?? ge fv);
    242       ! vs ← mmap ?? (reg_retrieve (locals f)) args;
    243       ret ? 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
     258*)   
     259
     260  | _ ⇒ ? ]
     261(*
    244262  | rtl_st_return ⇒
    245       (* CSC: rtl_if_result/f_result; list vs option *)
    246263      let dest ≝ rtl_if_result (func f) in
    247264      ! v ←  mmap … (reg_retrieve (locals f)) dest;
    248265      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    249266  ]
    250 | Callstate fd params dst fs m ⇒
    251     match fd with
    252     [ Internal fn ⇒
    253         ! locals ← params_store (rtl_if_params fn) params (init_locals (rtl_if_locals fn));
    254         let 〈m', sp〉 ≝ alloc m 0 (rtl_if_stacksize fn) Any in
    255         (* CSC: added carry *)
    256         ret ? 〈E0, State (mk_frame fn locals (rtl_if_entry fn) sp dst Vundef) fs m'〉
    257     | External fn ⇒
    258         ! evargs ← check_eventval_list params (sig_args (ef_sig fn));
    259         ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
    260         (* CSC: return type changed from option to list *)
    261         ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate [mk_val ? evres] dst fs m〉
    262     ]
    263267| Returnstate v dst fs m ⇒
    264268    match fs with
Note: See TracChangeset for help on using the changeset viewer.