Changeset 887 for src/RTLabs


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
Location:
src/RTLabs
Files:
2 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))〉
  • src/RTLabs/syntax.ma

    r878 r887  
    1010include "common/Graphs.ma".
    1111
    12 (* XXX: ASTish stuff *)
    13 
    14 definition immediate : Type[0] ≝ int.
    15 
    16 (* Addressing modes *)
    17 
    18 inductive addressing : Type[0] ≝
    19 | Aindexed  : immediate → addressing         (* r1 + offset *)
    20 | Aindexed2 : addressing                     (* r1 + r2 *)
    21 | Aglobal   : ident → immediate → addressing (* global + offset *)
    22 | Abased    : ident → immediate → addressing (* global + offset + r1 *)
    23 | Ainstack  : immediate → addressing         (* stack + offset *)
    24 .
    25 
    26 definition addr_mode_args : addressing → nat ≝
    27 λa. match a with
    28 [ Aindexed _  ⇒ 1
    29 | Aindexed2   ⇒ 2
    30 | Aglobal _ _ ⇒ 0
    31 | Abased _ _  ⇒ 1
    32 | Ainstack _  ⇒ 0
    33 ].
    34 
    35 definition addr ≝ λm.Vector register (addr_mode_args m).
    36 
    3712(* Statements, including the label of successor(s). *)
    3813
     
    4318| St_op1 : unary_operation → register → register → label → statement
    4419| St_op2 : binary_operation → register → register → register → label → statement
    45 | St_load : memory_chunk → ∀m:addressing. addr m → register → label → statement
    46 | St_store : memory_chunk → ∀m:addressing. addr m → register → label → statement
     20| St_load : memory_chunk → register → register → label → statement
     21| St_store : memory_chunk → register → register → label → statement
    4722| St_call_id : ident → list register → option register → label → statement
    4823| St_call_ptr : register → list register → option register → label → statement
     
    6035{ f_labgen    : universe LabelTag
    6136; f_reggen    : universe RegisterTag
    62 ; f_sig       : signature
    63 ; f_result    : option register
    64 ; f_params    : list register
    65 ; f_locals    : list register
    66 ; f_ptrs      : list register
     37; f_result    : option (register × typ)
     38; f_params    : list (register × typ)
     39; f_locals    : list (register × typ)
    6740; f_stacksize : nat
    6841; f_graph     : graph statement
Note: See TracChangeset for help on using the changeset viewer.