Changeset 1163


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
Files:
6 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.
  • src/LIN/JointLTLLIN.ma

    r1161 r1163  
    88inductive joint_instruction
    99  (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])
    10   (dpl_reg: Type[0]) (dph_reg: Type[0]) (generic_reg: Type[0])
    11   (pair_reg: Type[0]): Type[0] ≝
    12   | joint_instr_comment: String → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    13   | joint_instr_cost_label: costlabel → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    14   | joint_instr_int: generic_reg → Byte → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    15   | joint_instr_pop: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    16   | joint_instr_push: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    17   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    18   | joint_instr_hdw_to_hdw: pair_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    19   | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    20   | joint_instr_op1: Op1 → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    21   | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    22   | joint_instr_clear_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    23   | joint_instr_set_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    24   | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    25   | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    26   | joint_instr_call_id: ident → nat → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    27   | joint_instr_cond: acc_a_reg → label → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg.
     10  (dpl_reg: Type[0]) (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]): Type[0] ≝
     11  | joint_instr_comment: String → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     12  | joint_instr_cost_label: costlabel → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     13  | joint_instr_int: generic_reg → Byte → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     14  | joint_instr_move: pair_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     15  | joint_instr_pop: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     16  | joint_instr_push: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     17  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     18  | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     19  | joint_instr_op1: Op1 → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     20  | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     21  | joint_instr_clear_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     22  | joint_instr_set_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     23  | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     24  | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     25  | joint_instr_call_id: ident → nat → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     26  | joint_instr_cond: acc_a_reg → label → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg.
    2827
    2928inductive joint_statement
    3029  (A: Type[0]) (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])
    31   (dpl_reg: Type[0]) (dph_reg: Type[0]) (generic_reg: Type[0]) (pair_reg: Type[0]): Type[0] ≝
    32   | joint_st_sequential: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg → A → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    33   | joint_st_goto: label → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
    34   | joint_st_return: joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg.
     30  (dpl_reg: Type[0]) (dph_reg: Type[0]) (pair_reg: Type[0]) (generic_reg: Type[0]): Type[0] ≝
     31  | joint_st_sequential: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg → A → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     32  | joint_st_goto: label → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg
     33  | joint_st_return: joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg pair_reg generic_reg.
  • src/LIN/LIN.ma

    r1132 r1163  
    11include "LIN/JointLTLLIN.ma".
    22 
    3 definition pre_lin_statement ≝ joint_statement unit.
     3definition pre_lin_statement ≝
     4  λglobals.
     5  joint_statement unit globals Register Register
     6                  Register Register Register
     7                  (Register × Register).
    48
    59definition lin_statement ≝
  • src/LTL/LTL.ma

    r1161 r1163  
    11include "common/Graphs.ma".
    22include "utilities/IdentifierTools.ma".
    3 include "LIN/LIN.ma".
     3include "LIN/JointLTLLIN.ma".
    44
    55definition ltl_statement ≝
    66  λglobals.
    7     joint_statement label globals .
     7    joint_statement label globals Register
     8                    Register Register Register
     9                    Register (Register × Register).
    810 
    911definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.