Ignore:
Timestamp:
Apr 12, 2011, 12:32:33 PM (9 years ago)
Author:
campbell
Message:

Track some of the changes to the prototype in RTLabs.

Just one register in each place now, f_ptrs is present but not checked.
The changes to memory quantities have been glossed over for now.
A new difference from the prototype: return registers are optional.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs-sem.ma

    r744 r750  
    1414record frame : Type[0] ≝
    1515{ func   : internal_function
    16 ; locals : register_env split_val
     16; locals : register_env val
    1717; next   : label
    1818; sp     : block
    19 ; retdst : registers (* XXX: not optional? *)
     19; retdst : option register
    2020}.
    2121
     
    3232   ∀  fd : fundef internal_function.
    3333   ∀args : list val.
    34    ∀ dst : registers.
     34   ∀ dst : option register.
    3535   ∀ stk : list frame.
    3636   ∀   m : mem.
     
    3838| Returnstate :
    3939   ∀ rtv : val.
    40    ∀ dst : registers.
     40   ∀ dst : option register.
    4141   ∀ stk : list frame.
    4242   ∀   m : mem.
     
    4949
    5050definition reg_store ≝
    51 λrs,v,locals. match rs with [ dp n regs ⇒
    52   do vs ← break n v;
    53   OK ? (fold_right2_i ??? (λ_.λr,v,lcls. add RegisterTag ? lcls r v) locals n regs vs)
    54 ].
    55 
    56 let rec params_store (rs:list registers) (vs:list val) (locals : register_env split_val) : res (register_env split_val) ≝
     51λreg,v,locals.
     52  OK ? (add RegisterTag val locals reg v)
     53.
     54
     55let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    5756match rs with
    5857[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? ]
     
    6261] ].
    6362
    64 definition reg_retrieve : register_env ? → registers → res val ≝
    65 λlocals,rs. match rs with [ dp n regs ⇒
    66   do vs ← fold_right_i ??? (λm,r,vs. do vs' ← vs; do v ← opt_to_res … (lookup ?? locals r); OK ? (v:::vs')) (OK ? [[ ]]) regs;
    67   merge n vs
    68 ].
     63definition reg_retrieve : register_env ? → register → res val ≝
     64λlocals,reg. opt_to_res … (lookup ?? locals reg).
    6965
    7066(* TODO: maybe should make immediate = int or offset; val seems like a cheat here - not a real runtime value *)
    7167
    72 definition eval_addr : genv → frame → ∀m:addressing. Vector registers (addr_mode_args m) → res val ≝
    73 λge,f,m. match m return λm'.Vector registers (addr_mode_args m') → ? with
     68definition eval_addr : genv → frame → ∀m:addressing. Vector register (addr_mode_args m) → res val ≝
     69λge,f,m. match m return λm'.Vector register (addr_mode_args m') → ? with
    7470[ Aindexed i ⇒ λargs.
    7571    do v ← reg_retrieve (locals f) ((args !!! 0) ?);
     
    115111  [ St_skip l ⇒ ret ? 〈E0, build_state f fs m l〉
    116112  | St_cost cl l ⇒ ret ? 〈Echarge cl, build_state f fs m l〉
    117   | St_const rs cst l ⇒
     113  | St_const r cst l ⇒
    118114      ! v ← opt_to_res … (eval_constant (find_symbol … ge) (sp f) cst);
    119       ! locals ← reg_store rs v (locals f);
     115      ! locals ← reg_store r v (locals f);
    120116      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    121117  | St_op1 op dst src l ⇒
     
    178174      ret ? 〈E0, build_state f fs m (if b then ltrue else lfalse)〉
    179175
    180   | St_jumptable rs ls ⇒
    181       ! v ← reg_retrieve (locals f) rs;
     176  | St_jumptable r ls ⇒
     177      ! v ← reg_retrieve (locals f) r;
    182178      match v with
    183179      [ Vint i ⇒
     
    207203    [ nil ⇒ Error ? (* Already in final state *)
    208204    | cons f fs' ⇒
    209         ! locals ← reg_store dst v (locals f);
     205        ! locals ← match dst with [ None ⇒ OK ? (locals f)
     206                                  | Some d ⇒ reg_store d v (locals f) ];
    210207        ret ? 〈E0, State (mk_frame (func f) locals (next f) (sp f) (retdst f)) fs' m〉
    211208    ]
     
    229226  do b ← opt_to_res ? (find_symbol ? ? ge (prog_main ?? p));
    230227  do f ← opt_to_res ? (find_funct_ptr ? ? ge b);
    231   OK ? 〈ge,Callstate f (nil ?) (dp ??? [[ ]]) (nil ?) m〉.
     228  OK ? 〈ge,Callstate f (nil ?) (None ?) (nil ?) m〉.
    232229
    233230definition RTLabs_fullexec : fullexec io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.