Ignore:
Timestamp:
Jun 6, 2011, 3:55:23 PM (9 years ago)
Author:
campbell
Message:

Start bringing RTLabs into line with the prototype compiler:

  • a coarse-grained type is associated with every register
  • the special addressing modes have been removed
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r879 r887  
    5050definition build_state ≝ λf.λfs.λm.λn. State (adv n f) fs m.
    5151
    52 definition init_locals : list register → register_env val ≝
    53 foldr ?? (λid,en. add RegisterTag val en id Vundef) (empty_map ??).
     52definition init_locals : list (register × typ) → register_env val ≝
     53foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
    5454
    5555definition reg_store ≝
     
    5959axiom WrongNumberOfParameters : String.
    6060
    61 let rec params_store (rs:list register) (vs:list val) (locals : register_env val) : res (register_env val) ≝
     61let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
    6262match rs with
    6363[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
    64 | cons r rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
     64| cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
     65  let 〈r,ty〉 ≝ rt in
    6566  let locals' ≝ add RegisterTag val locals r v in
    6667  params_store rst vst locals'
     
    7475axiom FailedOp : String.
    7576axiom MissingSymbol : String.
    76 
    77 (* TODO: maybe should make immediate = int or offset; val seems like a cheat here - not a real runtime value *)
    78 
    79 definition eval_addr : genv → frame → ∀m:addressing. Vector register (addr_mode_args m) → res val ≝
    80 λge,f,m. match m return λm'.Vector register (addr_mode_args m') → ? with
    81 [ Aindexed i ⇒ λargs.
    82     do v ← reg_retrieve (locals f) ((args !!! 0) ?);
    83     opt_to_res … (msg FailedOp) (ev_addp v (Vint i))
    84 | Aindexed2 ⇒ λargs.
    85     do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
    86     do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
    87     opt_to_res … (msg FailedOp) (ev_addp v1 v2)
    88 | Aglobal id off ⇒ λargs.
    89     do loc ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    90     OK ? (Vptr Any loc ? (shift_offset zero_offset off))
    91 | Abased id off ⇒ λargs.
    92     do loc ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol ?? ge id);
    93     do v ← reg_retrieve (locals f) ((args !!! 0) ?);
    94     opt_to_res … (msg FailedOp) (ev_addp (Vptr Any loc ? zero_offset) v)
    95 | Ainstack off ⇒ λargs.
    96     OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))
    97 ]
    98 . /2/ [ 1,2: cases loc | cases (sp f) ] // qed.
    99 
    10077
    10178axiom MissingStatement : String.
     
    132109      ! locals ← reg_store dst v' (locals f);
    133110      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    134   | St_load chunk mode args dst l ⇒
    135       ! vaddr ← eval_addr ge f mode args;
     111  | St_load chunk addr dst l ⇒
     112      ! vaddr ← reg_retrieve (locals f) addr;
    136113      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
    137114      ! locals ← reg_store dst v (locals f);
    138115      ret ? 〈E0, State (mk_frame (func f) locals l (sp f) (retdst f)) fs m〉
    139   | St_store chunk mode args src l ⇒
    140       ! vaddr ← eval_addr ge f mode args;
     116  | St_store chunk addr src l ⇒
     117      ! vaddr ← reg_retrieve (locals f) addr;
    141118      ! v ← reg_retrieve (locals f) src;
    142119      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
     
    191168      ! v ← match f_result (func f) with
    192169            [ None ⇒ ret ? (None ?)
    193             | Some r ⇒ ! v ← reg_retrieve (locals f) r; ret ? (Some ? v)
     170            | Some rt ⇒
     171                let 〈r,ty〉 ≝ rt in
     172                ! v ← reg_retrieve (locals f) r;
     173                ret ? (Some ? v)
    194174            ];
    195175      ret ? 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
Note: See TracChangeset for help on using the changeset viewer.