Changeset 777 for src


Ignore:
Timestamp:
Apr 27, 2011, 5:25:26 PM (9 years ago)
Author:
mulligan
Message:

Lots of work on RTL to ERTL pass from today.

Location:
src
Files:
1 added
6 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/I8051.ma

    r757 r777  
    66include "ASM/Arithmetic.ma".
    77include "utilities/Compare.ma".
     8
     9definition int_size ≝ bitvector_of_nat 8 1.
     10definition ptr_size ≝ bitvector_of_nat 8 2.
     11definition alignment ≝ None.
    812
    913(* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
    … …  
    125129      ].
    126130
    127 definition eq_register: Register → Register → bool ≝
     131definition eq_Register: Register → Register → bool ≝
    128132  λr, s: Register.
    129133  let r_as_nat ≝ nat_of_register r in
    … …  
    178182  [ RegisterSST; RegisterST0; RegisterST1;
    179183    RegisterSPL; RegisterSPH ].
     184   
     185definition parameters: list Register ≝
     186  [ Register30; Register31; Register32; Register33;
     187    Register34; Register35; Register36; Register37 ].
    180188   
    181189record RegisterMap: Type[0] ≝

  • src/ASM/Util.ma

    r764 r777  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
     4 
     5let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
     6  match n with
     7  [ O ⇒
     8    match l with
     9    [ nil ⇒ [ ]
     10    | cons hd tl ⇒ l
     11    ]
     12  | S n ⇒
     13    match l with
     14    [ nil ⇒ [ ]
     15    | cons hd tl ⇒
     16      hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n
     17    ]
     18  ].
     19 
     20definition nub_by ≝
     21  λA: Type[0].
     22  λf: A → A → bool.
     23  λl: list A.
     24    nub_by_internal A f l (length ? l).
     25 
     26let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝
     27  match l with
     28  [ nil ⇒ false
     29  | cons hd tl ⇒ orb (eq a hd) (member A eq a tl)
     30  ].
     31 
     32let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝
     33  match n with
     34  [ O ⇒ [ ]
     35  | S n ⇒
     36    match l with
     37    [ nil ⇒ [ ]
     38    | cons hd tl ⇒ hd :: take A n tl
     39    ]
     40  ].
     41 
     42let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝
     43  match n with
     44  [ O ⇒ l
     45  | S n ⇒
     46    match l with
     47    [ nil ⇒ [ ]
     48    | cons hd tl ⇒ drop A n tl
     49    ]
     50  ].
     51 
     52definition list_split ≝
     53  λA: Type[0].
     54  λn: nat.
     55  λl: list A.
     56    〈take A n l, drop A n l〉.
     57 
     58let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B)
     59                      (l: list A) on l: list B ≝
     60  match l with
     61  [ nil ⇒ nil ?
     62  | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl)
     63  ]. 
     64
     65definition mapi ≝
     66  λA, B: Type[0].
     67  λf: nat → A → B.
     68  λl: list A.
     69    mapi_internal A B 0 f l.
     70
     71let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
     72  match l with
     73  [ nil ⇒ Some ? (nil (A × B))
     74  | cons hd tl ⇒
     75    match r with
     76    [ nil ⇒ None ?
     77    | cons hd' tl' ⇒
     78      match zip ? ? tl tl' with
     79      [ None ⇒ None ?
     80      | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail)
     81      ]
     82    ]
     83  ].
    484
    585let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝

  • src/ERTL/ERTL.ma

    r759 r777  
    66include "common/Registers.ma".
    77
    8 inductive abstract_register: Type[0] ≝
    9   mk_abstract_register: Word → abstract_register.
    10 
    11 definition abstract_registers ≝ list abstract_register.
    12 
     8definition hardware_register ≝ Register.
    139definition registers ≝ list register.
    1410
    … …  
    1713  | ertl_st_comment: String → label → ertl_statement
    1814  | ertl_st_cost: costlabel → label → ertl_statement
    19   | ertl_st_get_hdw: register → abstract_register → label → ertl_statement
    20   | ertl_st_set_hdw: abstract_register → register → label → ertl_statement
    21   | ertl_st_hdw_to_hdw: register → register → label → ertl_statement
     15  | ertl_st_get_hdw: register → hardware_register → label → ertl_statement
     16  | ertl_st_set_hdw: hardware_register → register → label → ertl_statement
     17  | ertl_st_hdw_to_hdw: hardware_register → hardware_register → label → ertl_statement
    2218  | ertl_st_new_frame: label → ertl_statement
    2319  | ertl_st_del_frame: label → ertl_statement
    24   | ertl_st_frame_size: abstract_register → label → ertl_statement
    25   | ertl_st_pop: abstract_register → label → ertl_statement
    26   | ertl_st_push: abstract_register → label → ertl_statement
    27   | ertl_st_addr_h: abstract_register → label → label → ertl_statement
    28   | ertl_st_addr_l: abstract_register → label → label → ertl_statement
    29   | ertl_st_int: abstract_register → Byte → label → ertl_statement
    30   | ertl_st_move: abstract_register → abstract_register → label → ertl_statement
    31   | ertl_st_opaccs: OpAccs → abstract_register → abstract_register → abstract_register → label → ertl_statement
    32   | ertl_st_op1: Op1 → abstract_register → abstract_register → label → ertl_statement
    33   | ertl_st_op2: Op2 → abstract_register → abstract_register → abstract_register → label → ertl_statement
     20  | ertl_st_frame_size: register → label → ertl_statement
     21  | ertl_st_pop: register → label → ertl_statement
     22  | ertl_st_push: register → label → ertl_statement
     23  | ertl_st_addr_h: register → label → label → ertl_statement
     24  | ertl_st_addr_l: register → label → label → ertl_statement
     25  | ertl_st_int: register → Byte → label → ertl_statement
     26  | ertl_st_move: register → register → label → ertl_statement
     27  | ertl_st_opaccs: OpAccs → register → register → register → label → ertl_statement
     28  | ertl_st_op1: Op1 → register → register → label → ertl_statement
     29  | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    3430  | ertl_st_clear_carry: label → ertl_statement
    35   | ertl_st_load: abstract_register → abstract_register → abstract_register → label → ertl_statement
    36   | ertl_st_store: abstract_register → abstract_register → abstract_register → label → ertl_statement
     31  | ertl_st_load: register → register → register → label → ertl_statement
     32  | ertl_st_store: register → register → register → label → ertl_statement
    3733  | ertl_st_call_id: label → Byte → label → ertl_statement
    38   | ertl_st_cond_acc: abstract_register → label → label → ertl_statement
    39   | ertl_st_return: abstract_registers → ertl_statement.
     34  | ertl_st_cond_acc: register → label → label → ertl_statement
     35  | ertl_st_return: registers → ertl_statement.
    4036
    4137definition ertl_statement_graph ≝ graph ertl_statement.

  • src/ERTL/Uses.ma

    r756 r777  
    99  λuses.
    1010    let l ≝ increment ? (lookup ? ? register uses (zero 16)) in
    11       insert ? 16 register l uses.
     11      insert ? 16 l uses.
    1212     
    1313definition examine_statement ≝

  • src/RTL/RTLtoERTL.ma

    r763 r777  
    11include "RTL/RTL.ma".
    22include "ERTL/ERTL.ma".
     3include "ASM/RegisterSet.ma".
    34
    45definition change_exit_label ≝
    … …  
    4748definition fresh_label ≝
    4849  λdef.
    49     fresh LabelTag (ertl_if_luniverse def).
     50    match fresh LabelTag (ertl_if_luniverse def) with
     51    [ OK lbl_univ ⇒ Some ? (\fst … lbl_univ)
     52    | Error ⇒ None ?
     53    ].
    5054   
    5155definition change_label ≝
    … …  
    8892      let tmp_lbl ≝ fresh_label def in
    8993      match tmp_lbl with
    90       [ OK o ⇒
    91         let 〈lbl, univ〉 ≝ o in
    92         let stmt ≝ change_label lbl hd in
     94      [ Some tmp_lbl ⇒
     95        let stmt ≝ change_label tmp_lbl hd in
    9396        let def ≝ add_graph start_lbl hd def in
    94           adds_graph tl lbl dest_lbl def
    95       | Error ⇒ None ?
     97          adds_graph tl tmp_lbl dest_lbl def
     98      | None ⇒ None ?
    9699      ]
    97100    ]
    98101  ].
    99102
    100 let rec add_translates (translate_list: list (label → label → ertl_internal_function → ertl_internal_function))
     103let rec add_translates (translate_list: list (label → label → ertl_internal_function → option ertl_internal_function))
    101104                       (start_lbl: label) (dest_lbl: label)
    102105                       (def: ertl_internal_function): option ertl_internal_function ≝
    … …  
    105108  | cons hd tl ⇒
    106109    match tl with
    107     [ nil ⇒ Some ? (hd start_lbl dest_lbl def)
     110    [ nil ⇒ hd start_lbl dest_lbl def
    108111    | _ ⇒
    109112      let tmp_lbl ≝ fresh_label def in
    110113      match tmp_lbl with
    111       [ OK o ⇒
    112         let 〈lbl, univ〉 ≝ o in
    113         let def ≝ hd start_lbl lbl def in
    114           add_translates tl lbl dest_lbl def
    115       | Error ⇒ None ?
     114      [ Some tmp_lbl ⇒
     115        match hd start_lbl tmp_lbl def with
     116        [ Some def ⇒ add_translates tl tmp_lbl dest_lbl def
     117        | None ⇒ None ?
     118        ]
     119      | None ⇒ None ?
    116120      ]
    117121    ]
    … …  
    129133  ].
    130134 
     135definition save_hdws_internal ≝
     136  λdestr_srcr: register × hardware_register.
     137  λstart_lbl: label.
     138    let 〈destr, srcr〉 ≝ destr_srcr in
     139      adds_graph [ ertl_st_get_hdw destr srcr start_lbl ] start_lbl.
     140 
    131141definition save_hdws ≝
    132   λ
     142  λl.
     143    map ? ? save_hdws_internal l.
     144   
     145definition restore_hdws_internal ≝
     146  λdestr_srcr: hardware_register × register.
     147  λstart_lbl: label.
     148    let 〈destr, srcr〉 ≝ destr_srcr in
     149    adds_graph [ ertl_st_set_hdw destr srcr start_lbl ] start_lbl.
     150   
     151definition swap_components ≝
     152  λA, B: Type[0].
     153  λp: A × B.
     154  let 〈l, r〉 ≝ p in
     155  〈r, l〉.
     156   
     157definition restore_hdws ≝
     158  λl.
     159    map ? ? restore_hdws_internal (map ? ? (swap_components ? ?) l).
     160
     161definition get_params_hdw_internal ≝
     162  λstart_lbl: label.
     163    adds_graph [ ertl_st_skip start_lbl ] start_lbl.
     164
     165definition get_params_hdw ≝
     166  λparams: list register.
     167  match length ? params with
     168  [ O ⇒ Some ? [ get_params_hdw_internal ]
     169  | _ ⇒
     170    match zip ? ? params parameters with
     171    [ None ⇒ None ?
     172    | Some l ⇒ Some ? (save_hdws l)
     173    ]
     174  ].
     175
     176definition get_param_stack ≝
     177  λoff: nat.
     178  λdestr.
     179  λstart_lbl, dest_lbl: label.
     180  λdef.
     181  let 〈def, addr1〉 ≝ fresh_reg def in
     182  let 〈def, addr2〉 ≝ fresh_reg def in
     183  let 〈def, tmpr〉 ≝ fresh_reg def in
     184  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
     185  adds_graph [
     186    ertl_st_frame_size addr1 start_lbl;
     187    ertl_st_int tmpr int_offset start_lbl;
     188    ertl_st_op2 Sub addr1 addr1 tmpr start_lbl;
     189    ertl_st_get_hdw tmpr RegisterSPL start_lbl;
     190    ertl_st_op2 Add addr1 addr1 tmpr start_lbl;
     191    ertl_st_int addr2 (bitvector_of_nat 8 0) start_lbl;
     192    ertl_st_get_hdw tmpr RegisterSPH start_lbl;
     193    ertl_st_op2 Addc addr2 addr2 tmpr start_lbl;
     194    ertl_st_load destr addr1 addr2 start_lbl
     195  ] start_lbl dest_lbl def.
     196 
     197definition get_params_stack_internal ≝
     198  λi.
     199  λr.
     200    get_param_stack i r.
     201 
     202definition get_params_stack ≝
     203  λparams.
     204  match length ? params with
     205  [ O ⇒ [ get_params_hdw_internal ]
     206  | _ ⇒ mapi ? ? get_params_stack_internal params
     207  ].
     208
     209definition get_params ≝
     210  λparams.
     211  let n ≝ min (length ? params) (length ? parameters) in
     212  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
     213  match get_params_hdw hdw_params with
     214  [ None ⇒ None ?
     215  | Some hdw_params ⇒ Some ? (hdw_params @ (get_params_stack stack_params))
     216  ].
     217 
     218definition add_prologue ≝
     219  λparams.
     220  λsral.
     221  λsrah.
     222  λsregs.
     223  λdef.
     224  let start_lbl ≝ ertl_if_entry def in
     225  let tmp_lbl ≝ fresh_label def in
     226  match tmp_lbl with
     227  [ None ⇒ None ?
     228  | Some tmp_lbl ⇒
     229    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
     230    let params ≝
     231      match get_params params with
     232      [ Some params ⇒ params
     233      | None ⇒ [ ] (* dpm: is this ok? *)
     234      ] in
     235    let def ≝
     236      add_translates (
     237        adds_graph [ ertl_st_new_frame start_lbl ] ::
     238        adds_graph [ ertl_st_pop sral start_lbl; ertl_st_pop srah start_lbl ] ::
     239        save_hdws sregs @
     240        params) start_lbl tmp_lbl def in
     241    match def with
     242    [ Some def ⇒
     243      match last_stmt with
     244      [ Some last_stmt ⇒ Some ? (add_graph tmp_lbl last_stmt def)
     245      | None ⇒ None ?
     246      ]
     247    | None ⇒ None ?
     248    ]
     249  ].
     250 
     251definition allocate_regs_internal ≝
     252  λr: register.
     253  λdef_sregs.
     254  let 〈def, sregs〉 ≝ def_sregs in
     255  let 〈def, r'〉 ≝ fresh_reg def in
     256    〈def, 〈r', r〉 :: sregs〉.
     257 
     258definition allocate_regs ≝
     259  λrs: register_set.
     260  λsaved: rs_set rs.
     261  λdef.
     262    rs_fold ? ? allocate_regs_internal saved 〈def, [ ]〉.
     263   
     264definition save_return_internal ≝
     265  λr.
     266  λstart_lbl.
     267  λdest_lbl.
     268  λdef.
     269  let 〈def, r_tmp〉 ≝ fresh_reg def in
     270  adds_graph [
     271    ertl_st_int r_tmp (bitvector_of_nat ? 0) start_lbl;
     272    ertl_st_set_hdw RegisterST0 r start_lbl;
     273    ertl_st_set_hdw RegisterST1 r_tmp start_lbl ] start_lbl dest_lbl def.
     274   
     275definition save_return_internal' ≝
     276  λr1, r2.
     277  λstart_lbl.
     278  adds_graph [
     279    ertl_st_set_hdw RegisterST0 r1 start_lbl;
     280    ertl_st_set_hdw RegisterST1 r2 start_lbl
     281  ] start_lbl.
     282   
     283definition save_return ≝
     284  λret_regs.
     285  match ret_regs with
     286  [ nil ⇒ [ get_params_hdw_internal ]
     287  | cons hd tl ⇒
     288    match tl with
     289    [ nil ⇒ [ save_return_internal hd ]
     290    | cons hd' tl' ⇒ [ save_return_internal' hd hd' ]
     291    ]
     292  ].
     293   
     294definition add_epilogue ≝
     295  λret_regs.
     296  λsral.
     297  λsrah.
     298  λsregs.
     299  λdef.
     300  let start_lbl ≝ ertl_if_exit def in
     301  let tmp_lbl ≝ fresh_label def in
     302  match tmp_lbl with
     303  [ None ⇒ None ?
     304  | Some tmp_lbl ⇒
     305    let last_stmt ≝ lookup ? ? (ertl_if_graph def) start_lbl in
     306    match last_stmt with
     307    [ None ⇒ None ?
     308    | Some last_stmt ⇒
     309      let def ≝
     310        add_translates (
     311          save_return ret_regs @
     312          restore_hdws sregs @
     313          [adds_graph [
     314            ertl_st_push srah start_lbl;
     315            ertl_st_push sral start_lbl
     316          ]] @
     317          [adds_graph [
     318            ertl_st_del_frame start_lbl
     319          ]] @
     320          [adds_graph [
     321            ertl_st_hdw_to_hdw RegisterDPL RegisterST0 start_lbl;
     322            ertl_st_hdw_to_hdw RegisterDPH RegisterST1 start_lbl
     323          ]]) start_lbl tmp_lbl def in
     324      match def with
     325      [ None ⇒ None ?
     326      | Some def ⇒
     327        let def ≝ add_graph tmp_lbl last_stmt def in
     328          Some ? (change_exit_label tmp_lbl def)
     329      ]
     330    ]
     331  ].
     332   
     333definition add_pro_and_epilogue ≝
     334  λrs: register_set.
     335  λparams.
     336  λret_args.
     337  λdef.
     338  let 〈def, sra〉 ≝ fresh_regs def 2 in
     339  let sral ≝ nth ? 0 sra in
     340  let srah ≝ nth sra 1 in
     341  let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
     342  let def ≝ add_prologue params sral srah sregs def in
     343  let def ≝ add_epilogue ret_args sral srah sregs def in
     344    def.

  • src/common/Registers.ma

    r757 r777  
    1818(* dpm: fix the Register/register mismatch *)
    1919axiom Register_of_register: register → Register.
     20axiom register_of_Register: Register → register.
Note: See TracChangeset for help on using the changeset viewer.