Changeset 756


Ignore:
Timestamp:
Apr 15, 2011, 5:47:32 PM (9 years ago)
Author:
mulligan
Message:

Made a start on RTL. Renaming in ERTL and below to move closer to Brian's naming convention and datatypes.

Location:
src
Files:
1 added
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/Build.ma

    r733 r756  
    1 include "ERTL/ERTL.ma".
    21
    3 definition build ≝
    4   λint_fun: ERTLInternalFunction.
    5     let liveafter ≝ analyze int_fun in
    6     let graph ≝ create
    72
  • src/ERTL/ERTL.ma

    r753 r756  
    33include "utilities/IdentifierTools.ma".
    44include "common/Graphs.ma".
     5include "common/CostLabel.ma".
     6include "common/Registers.ma".
    57
    6 inductive AbstractRegister: Type[0] ≝
    7   mkAbstractRegister: Word → AbstractRegister.
     8inductive abstract_register: Type[0] ≝
     9  mk_abstract_register: Word → abstract_register.
    810
    9 definition AbstractRegisters ≝ list AbstractRegister.
     11definition abstract_registers ≝ list abstract_register.
    1012
    11 inductive ERTLStatement: Type[0] ≝
    12   | ERTL_St_Skip: Identifier → ERTLStatement
    13   | ERTL_St_Comment: String → Identifier → ERTLStatement
    14   | ERTL_St_Cost: Identifier → Identifier → ERTLStatement
    15   | ERTL_St_Get_Hdw: Register → AbstractRegister → Identifier → ERTLStatement
    16   | ERTL_St_Set_Hdw: AbstractRegister → Register → Identifier → ERTLStatement
    17   | ERTL_St_Hdw_To_Hdw: Register → Register → Identifier → ERTLStatement
    18   | ERTL_St_NewFrame: Identifier → ERTLStatement
    19   | ERTL_St_DelFrame: Identifier → ERTLStatement
    20   | ERTL_St_FrameSize: AbstractRegister → Identifier → ERTLStatement
    21   | ERTL_St_Pop: AbstractRegister → Identifier → ERTLStatement
    22   | ERTL_St_Push: AbstractRegister → Identifier → ERTLStatement
    23   | ERTL_St_AddrH: AbstractRegister → Identifier → Identifier → ERTLStatement
    24   | ERTL_St_AddrL: AbstractRegister → Identifier → Identifier → ERTLStatement
    25   | ERTL_St_Int: AbstractRegister → Byte → Identifier → ERTLStatement
    26   | ERTL_St_Move: AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    27   | ERTL_St_Opaccs: OpAccs → AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    28   | ERTL_St_Op1: Op1 → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    29   | ERTL_St_Op2: Op2 → AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    30   | ERTL_St_ClearCarry: Identifier → ERTLStatement
    31   | ERTL_St_Load: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    32   | ERTL_St_Store: AbstractRegister → AbstractRegister → AbstractRegister → Identifier → ERTLStatement
    33   | ERTL_St_Call_Id: Identifier → Byte → Identifier → ERTLStatement
    34   | ERTL_St_CondAcc: AbstractRegister → Identifier → Identifier → ERTLStatement
    35   | ERTL_St_Return: AbstractRegisters → ERTLStatement.
     13definition registers ≝ list register.
    3614
    37 definition ERTLStatementGraph ≝ graph ERTLStatement.
     15inductive ertl_statement: Type[0] ≝
     16  | ertl_st_skip: ident → ertl_statement
     17  | ertl_st_comment: String → ident → ertl_statement
     18  | ertl_st_cost: costlabel → ident → ertl_statement
     19  | ertl_st_get_hdw: register → abstract_register → ident → ertl_statement
     20  | ertl_st_set_hdw: abstract_register → register → ident → ertl_statement
     21  | ertl_st_hdw_to_hdw: register → register → ident → ertl_statement
     22  | ertl_st_new_frame: ident → ertl_statement
     23  | ertl_st_del_frame: ident → ertl_statement
     24  | ertl_st_frame_size: abstract_register → ident → ertl_statement
     25  | ertl_st_pop: abstract_register → ident → ertl_statement
     26  | ertl_st_push: abstract_register → ident → ertl_statement
     27  | ertl_st_addr_h: abstract_register → ident → ident → ertl_statement
     28  | ertl_st_addr_l: abstract_register → ident → ident → ertl_statement
     29  | ertl_st_int: abstract_register → Byte → ident → ertl_statement
     30  | ertl_st_move: abstract_register → abstract_register → ident → ertl_statement
     31  | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → ident → ertl_statement
     32  | ertl_st_op1: Op1 → abstract_register → abstract_register → ident → ertl_statement
     33  | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → ident → ertl_statement
     34  | ertl_st_clear_carry: ident → ertl_statement
     35  | ertl_st_load: abstract_register → abstract_register → abstract_register → ident → ertl_statement
     36  | ertl_st_store: abstract_register → abstract_register → abstract_register → ident → ertl_statement
     37  | ertl_st_call_id: ident → Byte → ident → ertl_statement
     38  | ertl_st_cond_acc: abstract_register → ident → ident → ertl_statement
     39  | ertl_st_return: abstract_registers → ertl_statement.
    3840
    39 record ERTLInternalFunction: Type[0] ≝
     41definition ertl_statement_graph ≝ graph ertl_statement.
     42
     43record ertl_internal_function: Type[0] ≝
    4044{
    41   ERTL_IF_LUniverse: Universe;
    42   ERTL_IF_RUniverse: Universe;
    43   ERTL_IF_Params: Byte;
    44   ERTL_IF_Locals: BitVectorTrieSet 16;
    45   ERTL_IF_Graph: ERTLStatementGraph;
    46   ERTL_IF_Entry: Identifier;
    47   ERTL_IF_Exit: Identifier
     45  ertl_if_luniverse: universe LabelTag;
     46  ertl_if_runiverse: universe RegisterTag;
     47  ertl_if_params: nat;
     48  ertl_if_locals: registers;
     49  ertl_if_graph: ertl_statement_graph;
     50  ertl_if_entry: ident;
     51  ertl_if_exit: ident
    4852}.
    4953
    50 inductive ERTLFunction: Type[0] ≝
    51   | ERTL_Fu_Internal: ERTLInternalFunction → ERTLFunction
    52   | ERTL_Fu_External: ExternalFunction → ERTLFunction.
     54inductive ertl_function: Type[0] ≝
     55  | ertl_fu_internal: ertl_internal_function → ertl_function
     56  | ertl_fu_external: external_function → ertl_function.
    5357 
    54 record ERTLProgram: Type[0] ≝
     58record ertl_program: Type[0] ≝
    5559{
    56   ERTL_Pr_Vars: list (Identifier × nat);
    57   ERTL_Pr_Funcs: list (Identifier × ERTLFunction);
    58   ERTL_Pr_Main: option Identifier
     60  ertl_pr_vars: list (ident × nat);
     61  ertl_pr_funcs: list (ident × ertl_function);
     62  ertl_pr_main: option ident
    5963}.
    6064
    61 definition ERTL_Pr_Vars: ERTLProgram → list (Identifier × nat).
     65definition ertl_pr_vars: ertl_program → list (ident × nat).
    6266  # E
    6367  cases E
  • src/ERTL/Liveness.ma

    r746 r756  
    11include "ERTL/ERTL.ma".
    22
    3 definition set_singleton ≝
    4   λl: Identifier.
    5     set_insert ? l (set_empty ?).
    6 
    73definition statement_successors ≝
    8   λstmt: ERTLStatement.
     4  λstmt: ertl_statement.
    95  match stmt with
    10   [ ERTL_St_Return _ ⇒ set_empty ?
    11   | ERTL_St_Skip l ⇒ set_singleton l
    12   | ERTL_St_Comment comment l ⇒ set_singleton l
    13   | ERTL_St_Cost cost l ⇒ set_singleton l
    14   | ERTL_St_Set_Hdw r1 r2 l ⇒ set_singleton l
    15   | ERTL_St_Get_Hdw r1 r2 l ⇒ set_singleton l
    16   | ERTL_St_Hdw_To_Hdw r1 r2 l ⇒ set_singleton l
    17   | ERTL_St_NewFrame l ⇒ set_singleton l
    18   | ERTL_St_DelFrame l ⇒ set_singleton l
    19   | ERTL_St_FrameSize r l ⇒ set_singleton l
    20   | ERTL_St_Push r l ⇒ set_singleton l
    21   | ERTL_St_Pop r l ⇒ set_singleton l
    22   | ERTL_St_AddrH r l1 l2 ⇒ set_singleton l2
    23   | ERTL_St_AddrL r l1 l2 ⇒ set_singleton l2
    24   | ERTL_St_Int r v l ⇒ set_singleton l
    25   | ERTL_St_Move r1 r2 l ⇒ set_singleton l
    26   | ERTL_St_Opaccs opaccs r1 r2 r3 l ⇒ set_singleton l
    27   | ERTL_St_Op2 op2 r1 r2 r3 l ⇒ set_singleton l
    28   | ERTL_St_Op1 op1 r1 r2 l ⇒ set_singleton l
    29   | ERTL_St_ClearCarry l ⇒ set_singleton l
    30   | ERTL_St_Load r1 r2 r3 l ⇒ set_singleton l
    31   | ERTL_St_Store r1 r2 r3 l ⇒ set_singleton l
    32   | ERTL_St_Call_Id id v l ⇒ set_singleton l
    33   | ERTL_St_CondAcc _ l1 l2 ⇒ set_union ? (set_singleton l1) (set_singleton l2)
     6  [ ertl_st_return _ ⇒ [ ]
     7  | ertl_st_skip l ⇒ [ l ]
     8  | ertl_st_comment comment l ⇒ [ l ]
     9  | ertl_st_cost cost l ⇒ [ l ]
     10  | ertl_st_set_hdw r1 r2 l ⇒ [ l ]
     11  | ertl_st_get_hdw r1 r2 l ⇒ [ l ]
     12  | ertl_st_hdw_to_hdw r1 r2 l ⇒ [ l ]
     13  | ertl_st_new_frame l ⇒ [ l ]
     14  | ertl_st_del_frame l ⇒ [ l ]
     15  | ertl_st_frame_size r l ⇒ [ l ]
     16  | ertl_st_push r l ⇒ [ l ]
     17  | ertl_st_pop r l ⇒ [ l ]
     18  | ertl_st_addr_h r l1 l2 ⇒ [ l2 ]
     19  | ertl_st_addr_l r l1 l2 ⇒ [ l2 ]
     20  | ertl_st_int r v l ⇒ [ l ]
     21  | ertl_st_move r1 r2 l ⇒ [ l ]
     22  | ertl_st_opaccs opaccs r1 r2 r3 l ⇒ [ l ]
     23  | ertl_st_op2 op2 r1 r2 r3 l ⇒ [ l ]
     24  | ertl_st_op1 op1 r1 r2 l ⇒ [ l ]
     25  | ertl_st_clear_carry l ⇒ [ l ]
     26  | ertl_st_load r1 r2 r3 l ⇒ [ l ]
     27  | ertl_st_store r1 r2 r3 l ⇒ [ l ]
     28  | ertl_st_call_id id v l ⇒ [ l ]
     29  | ertl_st_cond_acc _ l1 l2 ⇒ [ l1 ] @ [ l2 ]
    3430  ].
     31 
     32(* dpm: this needs sorting out!  just what exactly is a register? *)
    3533
    3634definition set_of_list ≝
  • src/ERTL/Uses.ma

    r746 r756  
    33include "ASM/Arithmetic.ma".
    44include "ASM/I8051.ma".
     5include "common/Registers.ma".
    56
    67definition count ≝
    7   λregister.
     8  λr: register.
    89  λuses.
    910    let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
     
    1112     
    1213definition examine_statement ≝
    13   λstatement: ERTLStatement.
     14  λstatement: ertl_statement.
    1415  λuses.
    1516  match statement with
    16   [ ERTL_St_Skip _ ⇒ uses
    17   | ERTL_St_Comment _ _ ⇒ uses
    18   | ERTL_St_Cost _ _ ⇒ uses
    19   | ERTL_St_Hdw_To_Hdw _ _ _ ⇒ uses
    20   | ERTL_St_NewFrame _ ⇒ uses
    21   | ERTL_St_DelFrame _ ⇒ uses
    22   | ERTL_St_ClearCarry _ ⇒ uses
    23   | ERTL_St_Call_Id _ _ _ ⇒ uses
    24   | ERTL_St_Return _ ⇒ uses
    25   | ERTL_St_Get_Hdw r _ _ ⇒ count (word_of_register r) uses
    26   | ERTL_St_Set_Hdw _ r _ ⇒ count (word_of_register r) uses
    27   | ERTL_St_FrameSize ar _ ⇒
     17  [ ertl_st_skip _ ⇒ uses
     18  | ertl_st_comment _ _ ⇒ uses
     19  | ertl_st_cost _ _ ⇒ uses
     20  | ertl_st_hdw_to_hdw _ _ _ ⇒ uses
     21  | ertl_st_new_frame _ ⇒ uses
     22  | ertl_st_del_frame _ ⇒ uses
     23  | ertl_st_clear_carry _ ⇒ uses
     24  | ertl_st_call_id _ _ _ ⇒ uses
     25  | ertl_st_return _ ⇒ uses
     26  | ertl_st_get_hdw r _ _ ⇒ count (word_of_register r) uses
     27  | ertl_st_set_hdw _ r _ ⇒ count (word_of_register r) uses
     28  | ertl_st_frame_size ar _ ⇒
    2829    match ar with [
    29       mkAbstractRegister r ⇒
     30      mk_abstract_register r ⇒
    3031        (* dpm: shift the abstract registers above the physical registers *)
    3132        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    3233          count offset uses
    3334    ]
    34   | ERTL_St_Pop ar _ ⇒
     35  | ertl_st_pop ar _ ⇒
    3536    match ar with [
    36       mkAbstractRegister r ⇒
     37      mk_abstract_register r ⇒
    3738        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    3839          count offset uses
    3940    ]
    40   | ERTL_St_Push ar _ ⇒
     41  | ertl_st_push ar _ ⇒
    4142    match ar with [
    42       mkAbstractRegister r ⇒
     43      mk_abstract_register r ⇒
    4344        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    4445          count offset uses
    4546    ]
    46   | ERTL_St_Int ar _ _ ⇒
     47  | ertl_st_int ar _ _ ⇒
    4748    match ar with [
    48       mkAbstractRegister r ⇒
     49      mk_abstract_register r ⇒
    4950        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    5051          count offset uses
    5152    ]
    52   | ERTL_St_AddrH ar _ _ ⇒
     53  | ertl_st_addr_h ar _ _ ⇒
    5354    match ar with [
    54       mkAbstractRegister r ⇒
     55      mk_abstract_register r ⇒
    5556        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    5657          count offset uses
    5758    ]
    58   | ERTL_St_AddrL ar _ _ ⇒
     59  | ertl_st_addr_l ar _ _ ⇒
    5960    match ar with [
    60       mkAbstractRegister r ⇒
     61      mk_abstract_register r ⇒
    6162        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    6263          count offset uses
    6364    ]
    64   | ERTL_St_CondAcc ar _ _ ⇒
     65  | ertl_st_cond_acc ar _ _ ⇒
    6566    match ar with [
    66       mkAbstractRegister r ⇒
     67      mk_abstract_register r ⇒
    6768        let 〈offset, ignore〉 ≝ add_n_with_carry ? r (bitvector_of_nat ? physical_register_count) false ? in
    6869          count offset uses
    6970    ]
    70   | ERTL_St_Move ar1 ar2 _ ⇒
     71  | ertl_st_move ar1 ar2 _ ⇒
    7172    match ar1 with [
    72       mkAbstractRegister r1 ⇒
     73      mk_abstract_register r1 ⇒
    7374      match ar2 with [
    74         mkAbstractRegister r2 ⇒
     75        mk_abstract_register r2 ⇒
    7576          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    7677          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    7879      ]
    7980    ]
    80   | ERTL_St_Op1 op1 ar1 ar2 _ ⇒
     81  | ertl_st_op1 op1 ar1 ar2 _ ⇒
    8182    match ar1 with [
    82       mkAbstractRegister r1 ⇒
     83      mk_abstract_register r1 ⇒
    8384      match ar2 with [
    84         mkAbstractRegister r2 ⇒
     85        mk_abstract_register r2 ⇒
    8586          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    8687          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    8889      ]
    8990    ]
    90   | ERTL_St_Op2 op2 ar1 ar2 ar3 _ ⇒
     91  | ertl_st_op2 op2 ar1 ar2 ar3 _ ⇒
    9192    match ar1 with [
    92       mkAbstractRegister r1 ⇒
     93      mk_abstract_register r1 ⇒
    9394      match ar2 with [
    94         mkAbstractRegister r2 ⇒
     95        mk_abstract_register r2 ⇒
    9596        match ar3 with [
    96           mkAbstractRegister r3 ⇒
     97          mk_abstract_register r3 ⇒
    9798          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    9899          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    102103      ]
    103104    ]
    104   | ERTL_St_Opaccs opaccs ar1 ar2 ar3 _ ⇒
     105  | ertl_st_opaccs opaccs ar1 ar2 ar3 _ ⇒
    105106    match ar1 with [
    106       mkAbstractRegister r1 ⇒
     107      mk_abstract_register r1 ⇒
    107108      match ar2 with [
    108         mkAbstractRegister r2 ⇒
     109        mk_abstract_register r2 ⇒
    109110        match ar3 with [
    110           mkAbstractRegister r3 ⇒
     111          mk_abstract_register r3 ⇒
    111112          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    112113          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    116117      ]
    117118    ]
    118   | ERTL_St_Load ar1 ar2 ar3 _ ⇒
     119  | ertl_st_load ar1 ar2 ar3 _ ⇒
    119120    match ar1 with [
    120       mkAbstractRegister r1 ⇒
     121      mk_abstract_register r1 ⇒
    121122      match ar2 with [
    122         mkAbstractRegister r2 ⇒
     123        mk_abstract_register r2 ⇒
    123124        match ar3 with [
    124           mkAbstractRegister r3 ⇒
     125          mk_abstract_register r3 ⇒
    125126          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    126127          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
     
    130131      ]
    131132    ]
    132   | ERTL_St_Store ar1 ar2 ar3 _ ⇒
     133  | ertl_st_store ar1 ar2 ar3 _ ⇒
    133134    match ar1 with [
    134       mkAbstractRegister r1 ⇒
     135      mk_abstract_register r1 ⇒
    135136      match ar2 with [
    136         mkAbstractRegister r2 ⇒
     137        mk_abstract_register r2 ⇒
    137138        match ar3 with [
    138           mkAbstractRegister r3 ⇒
     139          mk_abstract_register r3 ⇒
    139140          let 〈offset1, ignore〉 ≝ add_n_with_carry ? r1 (bitvector_of_nat ? physical_register_count) false ? in
    140141          let 〈offset2, ignore〉 ≝ add_n_with_carry ? r2 (bitvector_of_nat ? physical_register_count) false ? in
  • src/RTL/RTL.ma

    r754 r756  
    4444}.
    4545
     46definition rtl_if_stacksize: rtl_internal_function → nat.
     47  # R
     48  cases R
     49  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8 # H9 # H10
     50  @ H7
     51qed.
     52
    4653inductive rtl_function_definition: Type[0] ≝
    4754  | rtl_f_internal: rtl_internal_function → rtl_function_definition
     
    5461  rtl_pr_main: option ident
    5562}.
    56 }.
Note: See TracChangeset for help on using the changeset viewer.