Changeset 1163 for src/ERTL


Ignore:
Timestamp:
Sep 1, 2011, 4:23:42 PM (8 years ago)
Author:
mulligan
Message:

even more streamlining and fixes to get things type checking

Location:
src/ERTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1161 r1163  
    99definition registers ≝ list register.
    1010
     11inductive move_registers: Type[0] ≝
     12  | pseudo: register → move_registers
     13  | hardware: Register → move_registers.
     14
    1115definition pre_ertl_statement ≝
    1216  λglobals: list ident.
    1317  joint_statement label globals register
    1418                  register register register
    15                   register (Register × Register).
     19                  (move_registers × move_registers) register.
    1620                 
    1721inductive ertl_statement (globals: list ident): Type[0] ≝
     
    1923  | ertl_st_new_frame: label → ertl_statement globals
    2024  | ertl_st_del_frame: label → ertl_statement globals
    21   | ertl_st_frame_size: register → label → ertl_statement globals
    22   | ertl_st_move: register → register → label → ertl_statement globals
    23   | ertl_st_get_hdw: register → Register → label → ertl_statement globals
    24   | ertl_st_set_hdw: Register → register → label → ertl_statement globals.
     25  | ertl_st_frame_size: register → label → ertl_statement globals.
    2526
    2627(*
  • src/ERTL/ERTLToLTL.ma

    r1161 r1163  
    3131  let 〈l, luniv〉 ≝ fresh_label globals luniv in
    3232  let graph ≝ add_graph globals l stmt graph in
    33     〈l, 〈graph, luniv〉〉.
     33    〈l, graph, luniv〉.
    3434
    3535definition num_locals ≝
    36   λint_fun.
    37     colour_locals + (ertl_if_stacksize int_fun).
     36  λglobals.
     37  λint_fun.
     38    colour_locals + (ertl_if_stacksize globals int_fun).
    3839
    3940definition stacksize ≝
    40   λint_fun.
    41     colour_locals + (ertl_if_stacksize int_fun).
     41  λglobals.
     42  λint_fun.
     43    colour_locals + (ertl_if_stacksize globals int_fun).
    4244
    4345definition adjust_off ≝
     46  λglobals.
    4447  λint_fun.
    4548  λoff.
    4649  let 〈ignore, int_off〉 ≝ half_add ? int_size off in
    47   let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals int_fun)) int_off false in
     50  let 〈sub, ignore〉 ≝ sub_8_with_carry (bitvector_of_nat ? (num_locals globals int_fun)) int_off false in
    4851    sub.
    4952
     53check
     54
    5055definition get_stack ≝
    51   λint_fun.
    52   λglobals.
     56  λglobals.
     57  λint_fun.
    5358  λgraph: graph (ltl_statement (globals)).
    5459  λr.
    5560  λoff.
    5661  λl.
    57     let off ≝ adjust_off int_fun off in
    58     let luniv ≝ ertl_if_luniverse int_fun in
    59     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals r) l) in
     62    let off ≝ adjust_off globals int_fun off in
     63    let luniv ≝ ertl_if_luniverse globals int_fun in
     64    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_hdw_to_hdw globals … 〈RegisterA, r〉) l) in
     65    ?.
     66   
    6067    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_load globals) l) in
    6168    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ? globals (joint_instr_from_acc globals RegisterDPH) l) in
  • src/ERTL/semantics.ma

    r1162 r1163  
    214214  OK ? (set_regs regs st))).
    215215
     216definition retrieve: state → move_registers → res val ≝
     217  λst.
     218  λr.
     219  match r with
     220  [ pseudo   src ⇒ reg_retrieve (locals st) src
     221  | hardware src ⇒ hwreg_retrieve (regs st) src
     222  ].
     223
     224definition store ≝
     225  λst.
     226  λv.
     227  λr.
     228  match r with
     229  [ pseudo   dst ⇒
     230    ! locals ← reg_store dst v (locals st);
     231      ret ? (set_locals locals st)
     232  | hardware dst ⇒
     233    ! regs ← hwreg_store dst v (regs st);
     234      ret ? (set_regs regs st)
     235  ].
     236
    216237definition eval_statement : ∀globals: list ident. (genv globals) → state → IO io_out io_in (trace × state) ≝
    217238  λglobals. λge,st.
     
    271292      | joint_instr_clear_carry ⇒ ret ? 〈E0, goto l (set_carry Vfalse st)〉
    272293      | joint_instr_set_carry ⇒ ret ? 〈E0, goto l (set_carry Vtrue st)〉
    273       | joint_instr_hdw_to_hdw dst_src ⇒
    274           let 〈dst, src〉 ≝ dst_src in
    275         ! v ← hwreg_retrieve (regs st) src;
    276         ! regs ← hwreg_store dst v (regs st);
    277           ret ? 〈E0, goto l (set_regs regs st)〉
    278294      | joint_instr_opaccs op acc_a_reg acc_b_reg ⇒
    279295        ! v1 ← reg_retrieve (locals st) acc_a_reg;
     
    295311        ! v ← Byte_of_val v;
    296312        ! st ← push st v;
     313          ret ? 〈E0, goto l st〉
     314      | joint_instr_move dst_src ⇒
     315        let 〈dst, src〉 ≝ dst_src in
     316        ! v ← retrieve st src;
     317        ! st ← store st v dst;
    297318          ret ? 〈E0, goto l st〉
    298319      (* CSC: changed, where the meat is *)
     
    316337            ! st ← set_result vs st;
    317338              ret ? 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), goto l st〉
     339          ]
    318340      ]
    319       | _ ⇒ ?
    320       ]
     341    (* CSC: changed, where the meat is *)
    321342    | joint_st_return ⇒
    322343      ! st ← pop_frame st;
     
    327348    | _ ⇒ ?
    328349    ]
    329   | ertl_st_get_hdw dst src l ⇒
    330      ! v ← hwreg_retrieve (regs st) src;
    331      ! locals ← reg_store dst v (locals st);
    332      ret ? 〈E0, goto l (set_locals locals st)〉
    333   | ertl_st_set_hdw dst src l ⇒
    334      ! v ← reg_retrieve (locals st) src;
    335      ! regs ← hwreg_store dst v (regs st);
    336      ret ? 〈E0, goto l (set_regs regs st)〉
    337   | ertl_st_new_frame _ ⇒ ?
    338   | ertl_st_del_frame _ ⇒ ?
    339   | ertl_st_frame_size _ _ ⇒ ?
    340   (*CSC: rtl_st_move is splitted into ertl_st_move, ertl_st_get_hdw,
    341          ertl_st_set_hdw, ertl_stl_hdw_to_hdw. Maybe one datatype would
    342          be more than enough... *)
    343   | ertl_st_move dst src l ⇒
    344      ! v ← reg_retrieve (locals st) src;
    345      ! locals ← reg_store dst v (locals st);
    346      ret ? 〈E0, goto l (set_locals locals st)〉
    347   ].
    348 
     350  | ertl_st_new_frame l ⇒
     351    ! v ← framesize globals st;
     352    ! sp ← get_hwsp st;
     353      let newsp ≝ addr_sub sp v in
     354    ! st ← set_hwsp newsp st;
     355      ret ? 〈E0,goto l st〉
     356  | ertl_st_del_frame l ⇒
     357    ! v ← framesize globals st;
     358    ! sp ← get_hwsp st;
     359      let newsp ≝ addr_add sp v in
     360    ! st ← set_hwsp newsp st;
     361      ret ? 〈E0,goto l st〉
     362  | ertl_st_frame_size dst l ⇒
     363    ! v ← framesize globals st;
     364    ! locals ← reg_store dst (val_of_nat v) (locals st);
     365      ret ? 〈E0, goto l (set_locals locals st)〉
    349366  (* CSC: Dropped:
    350367      - rtl_st_stackaddr (becomes two get_hdw)
    351368      - rtl_st_tailcall_id/rtl_st_tailcall_ptr (unimplemented ATM)
    352369      - rtl_st_call_ptr (unimplemented ATM) *)
    353   cases daemon
    354 qed.
     370  ].
    355371     
    356372axiom WrongReturnValueType: String.
Note: See TracChangeset for help on using the changeset viewer.