Changeset 782 for src


Ignore:
Timestamp:
Apr 28, 2011, 5:36:33 PM (9 years ago)
Author:
mulligan
Message:

More work on rtl-ertl pass from today, plus resolved conflict.

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorTrie.ma

    r779 r782  
    88| Node: ∀n: nat. BitVectorTrie A n → BitVectorTrie A n → BitVectorTrie A (S n)
    99| Stub: ∀n: nat. BitVectorTrie A n.
     10
     11axiom fold:
     12 ∀A, B: Type[0].
     13 ∀n: nat.
     14 ∀f: BitVector n → A → B → B.
     15 ∀t: BitVectorTrie A n.
     16 ∀b: B.
     17   B.
    1018
    1119let rec lookup_opt (A: Type[0]) (n: nat)
  • src/ASM/Util.ma

    r777 r782  
    22include "basics/types.ma".
    33include "arithmetics/nat.ma".
     4 
     5lemma eq_rect_Type0_r :
     6  ∀A: Type[0].
     7  ∀a:A.
     8  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
     9  #A #a #P #H #x #p
     10  generalize in match H
     11  generalize in match P
     12  cases p
     13  //
     14qed.
     15 
     16let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝
     17  match n return λo. o < length A l → A with
     18  [ O ⇒
     19    match l return λm. 0 < length A m → A with
     20    [ nil ⇒ λabsd1. ?
     21    | cons hd tl ⇒ λprf1. hd
     22    ]
     23  | S n' ⇒
     24    match l return λm. S n' < length A m → A with
     25    [ nil ⇒ λabsd2. ?
     26    | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
     27    ]
     28  ] ?.
     29  [ 1:
     30    @ p
     31  | 4:
     32    normalize in prf2
     33    normalize
     34    @ le_S_S_to_le
     35    assumption
     36  | 2:
     37    normalize in absd1;
     38    cases (not_le_Sn_O O)
     39    # H
     40    elim (H absd1)
     41  | 3:
     42    normalize in absd2;
     43    cases (not_le_Sn_O (S n'))
     44    # H
     45    elim (H absd2)
     46  ]
     47qed.
    448 
    549let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
     
    128172
    129173definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
    130 
    131 lemma eq_rect_Type0_r :
    132   ∀A: Type[0].
    133   ∀a:A.
    134   ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
    135   #A #a #P #H #x #p
    136   generalize in match H
    137   generalize in match P
    138   cases p
    139   //
    140 qed.
    141 
    142174
    143175notation "hvbox(t⌈o ↦ h⌉)"
  • src/ERTL/ERTL.ma

    r777 r782  
    2121  | ertl_st_pop: register → label → ertl_statement
    2222  | 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
     23  | ertl_st_addr_h: register → ident → label → ertl_statement
     24  | ertl_st_addr_l: register → ident → label → ertl_statement
    2525  | ertl_st_int: register → Byte → label → ertl_statement
    2626  | ertl_st_move: register → register → label → ertl_statement
     
    3131  | ertl_st_load: register → register → register → label → ertl_statement
    3232  | ertl_st_store: register → register → register → label → ertl_statement
    33   | ertl_st_call_id: label → Byte → label → ertl_statement
     33  | ertl_st_call_id: ident → Byte → label → ertl_statement
    3434  | ertl_st_cond_acc: register → label → label → ertl_statement
    3535  | ertl_st_return: registers → ertl_statement.
     
    4343  ertl_if_params: nat;
    4444  ertl_if_locals: registers;
     45  ertl_if_stacksize: nat;
    4546  ertl_if_graph: ertl_statement_graph;
    4647  ertl_if_entry: label;
     
    5152  # E
    5253  cases E
    53   # H1 # H2 # H3 # H4 # H5 # H6 # H7
     54  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
    5455  @ H3
    5556qed.
    5657
     58definition ertl_if_stacksize: ertl_internal_function → nat.
     59  # E
     60  cases E
     61  # H1 # H2 # H3 # H4 # H5 # H6 # H7 # H8
     62  @ H5
     63qed.
     64
    5765inductive ertl_function: Type[0] ≝
    58   | ertl_fu_internal: ertl_internal_function → ertl_function
    59   | ertl_fu_external: external_function → ertl_function.
     66  | ertl_f_internal: ertl_internal_function → ertl_function
     67  | ertl_f_external: external_function → ertl_function.
    6068 
    6169record ertl_program: Type[0] ≝
  • src/RTL/RTL.ma

    r756 r782  
    1010inductive rtl_statement: Type[0] ≝
    1111  | rtl_st_skip: label → rtl_statement
    12   | rtl_st_cost: costlabel → rtl_statement
     12  | rtl_st_cost: costlabel → label → rtl_statement
    1313  | rtl_st_addr: register → register → ident → label → rtl_statement
    14   | rtl_st_stack_Addr: register → register → label → rtl_statement
     14  | rtl_st_stack_addr: register → register → label → rtl_statement
    1515  | rtl_st_int: register → Byte → label → rtl_statement
    1616  | rtl_st_move: register → register → label → rtl_statement
     
    2525  | rtl_st_tailcall_id: ident → registers → rtl_statement
    2626  | rtl_st_tailcall_ptr: register → register → registers → rtl_statement
    27   | rtl_st_condacc: register → label → label → rtl_statement
     27  | rtl_st_cond_acc: register → label → label → rtl_statement
    2828  | rtl_st_return: registers → rtl_statement.
    2929 
  • src/RTL/RTLtoERTL.ma

    r777 r782  
    11include "RTL/RTL.ma".
    22include "ERTL/ERTL.ma".
    3 include "ASM/RegisterSet.ma".
     3include "utilities/RegisterSet.ma".
    44
    55definition change_exit_label ≝
     
    1010  let ertl_if_params' ≝ ertl_if_params p in
    1111  let ertl_if_locals' ≝ ertl_if_locals p in
     12  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    1213  let ertl_if_graph' ≝ ertl_if_graph p in
    1314  let ertl_if_entry' ≝ ertl_if_entry p in
    1415  let ertl_if_exit' ≝ l in
    1516    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    16                               ertl_if_params' ertl_if_locals'
     17                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    1718                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    1819
     
    2425  let ertl_if_params' ≝ ertl_if_params p in
    2526  let ertl_if_locals' ≝ ertl_if_locals p in
     27  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    2628  let ertl_if_graph' ≝ ertl_if_graph p in
    2729  let ertl_if_entry' ≝ l in
    2830  let ertl_if_exit' ≝ ertl_if_exit p in
    2931    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    30                               ertl_if_params' ertl_if_locals'
     32                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    3133                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    3234                             
     
    3941  let ertl_if_params' ≝ ertl_if_params p in
    4042  let ertl_if_locals' ≝ ertl_if_locals p in
     43  let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    4144  let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
    4245  let ertl_if_entry' ≝ ertl_if_entry p in
    4346  let ertl_if_exit' ≝ ertl_if_exit p in
    4447    mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    45                               ertl_if_params' ertl_if_locals'
     48                              ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    4649                              ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    4750                             
     
    330333    ]
    331334  ].
    332    
     335 
     336axiom add_pro_and_epilogue:
     337  ∀rs: register_set.
     338  ∀params: list register.
     339  ∀ret_args: list register.
     340  ∀def: ertl_internal_function.
     341    option ertl_internal_function.
     342   
     343(*
     344  dpm: address callee_saved problem   
    333345definition add_pro_and_epilogue ≝
    334346  λrs: register_set.
     
    337349  λdef.
    338350  let 〈def, sra〉 ≝ fresh_regs def 2 in
    339   let sral ≝ nth ? 0 sra in
    340   let srah ≝ nth sra 1 in
     351  let sral ≝ safe_nth ? 0 sra ? in
     352  let srah ≝ safe_nth ? 1 sra ? in
    341353  let 〈def, sregs〉 ≝ allocate_regs callee_saved def in
    342354  let def ≝ add_prologue params sral srah sregs def in
    343355  let def ≝ add_epilogue ret_args sral srah sregs def in
    344     def.
     356    def. 
     357*)
     358
     359definition set_params_hdw ≝
     360  λparams.
     361  match length ? params with
     362  [ O ⇒ Some ? [ get_params_hdw_internal ]
     363  | _ ⇒
     364    match zip ? ? params parameters with
     365    [ None ⇒ None ?
     366    | Some zipped_params ⇒ Some ? (restore_hdws zipped_params)
     367    ]
     368  ].
     369 
     370definition set_param_stack ≝
     371  λoff: nat.
     372  λsrcr.
     373  λstart_lbl, dest_lbl: label.
     374  λdef.
     375  let 〈def, addr1〉 ≝ fresh_reg def in
     376  let 〈def, addr2〉 ≝ fresh_reg def in
     377  let 〈def, tmpr〉 ≝ fresh_reg def in
     378  let 〈int_offset, ignore〉 ≝ add_8_with_carry (bitvector_of_nat ? off) int_size false in
     379    adds_graph [
     380      ertl_st_int addr2 int_offset start_lbl;
     381      ertl_st_get_hdw tmpr RegisterSPL start_lbl;
     382      ertl_st_clear_carry start_lbl;
     383      ertl_st_op2 Sub addr1 tmpr addr1 start_lbl;
     384      ertl_st_get_hdw tmpr RegisterSPH start_lbl;
     385      ertl_st_int addr2 (bitvector_of_nat ? 0) start_lbl;
     386      ertl_st_op2 Sub addr2 tmpr addr2 start_lbl;
     387      ertl_st_store addr1 addr2 srcr start_lbl
     388    ] start_lbl dest_lbl def.
     389
     390definition set_params_stack ≝
     391  λparams.
     392  match length ? params with
     393  [ O ⇒ [ get_params_hdw_internal ]
     394  | _ ⇒ mapi ? ? set_param_stack params
     395 
     396  ].
     397 
     398definition set_params ≝
     399  λparams.
     400  let n ≝ min (length ? params) (length ? parameters) in
     401  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
     402    match set_params_hdw hdw_params with
     403    [ None ⇒ None ?
     404    | Some hdw_params' ⇒ Some ? (hdw_params' @ (set_params_stack stack_params))
     405    ].
     406   
     407definition fetch_result ≝
     408  λret_regs.
     409  λstart_lbl.
     410  match ret_regs with
     411  [ nil ⇒ adds_graph [ertl_st_skip start_lbl] start_lbl
     412  | cons hd tl ⇒
     413    match tl with
     414    [ nil ⇒
     415      adds_graph [
     416        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
     417        ertl_st_get_hdw hd RegisterST0 start_lbl
     418      ] start_lbl
     419    | cons hd' tl' ⇒
     420      adds_graph [
     421        ertl_st_hdw_to_hdw RegisterST0 RegisterDPL start_lbl;
     422        ertl_st_hdw_to_hdw RegisterST1 RegisterDPH start_lbl;
     423        ertl_st_get_hdw hd RegisterST0 start_lbl;
     424        ertl_st_get_hdw hd' RegisterST1 start_lbl
     425      ] start_lbl
     426    ]
     427  ].
     428 
     429definition translate_call_id ≝
     430  λf.
     431  λargs.
     432  λret_regs.
     433  λstart_lbl, dest_lbl: label.
     434  λdef.
     435  let nb_args ≝ bitvector_of_nat ? (length ? args) in
     436  match set_params args with
     437  [ None ⇒ None ?
     438  | Some params_args ⇒
     439    add_translates (
     440      params_args @ [
     441        adds_graph [ ertl_st_call_id f nb_args start_lbl ] ;
     442        fetch_result ret_regs
     443      ]) start_lbl dest_lbl def
     444  ].
     445 
     446definition translate_stmt ≝
     447  λlbl: label.
     448  λstmt: rtl_statement.
     449  λdef: ertl_internal_function.
     450  match stmt with
     451  [ rtl_st_skip lbl' ⇒
     452    Some ? (add_graph lbl (ertl_st_skip lbl') def)
     453  | rtl_st_cost cost_lbl lbl' ⇒
     454    Some ? (add_graph lbl (ertl_st_cost cost_lbl lbl') def)
     455  | rtl_st_addr r1 r2 x lbl' ⇒
     456    adds_graph [
     457      ertl_st_addr_l r1 x lbl;
     458      ertl_st_addr_h r2 x lbl
     459    ] lbl lbl' def
     460  | rtl_st_stack_addr r1 r2 lbl' ⇒
     461    adds_graph [
     462      ertl_st_get_hdw r1 RegisterSPL lbl;
     463      ertl_st_get_hdw r2 RegisterSPH lbl
     464    ] lbl lbl' def
     465  | rtl_st_int r i lbl' ⇒
     466    Some ? (add_graph lbl (ertl_st_int r i lbl') def)
     467  | rtl_st_move r1 r2 lbl' ⇒
     468    Some ? (add_graph lbl (ertl_st_move r1 r2 lbl') def)
     469  | rtl_st_opaccs opaccs d s1 s2 lbl' ⇒
     470    Some ? (add_graph lbl (ertl_st_opaccs opaccs d s1 s2 lbl') def)
     471  | rtl_st_op1 op1 d s lbl' ⇒
     472    Some ? (add_graph lbl (ertl_st_op1 op1 d s lbl') def)
     473  | rtl_st_op2 op2 d s1 s2 lbl' ⇒
     474    Some ? (add_graph lbl (ertl_st_op2 op2 d s1 s2 lbl') def)
     475  | rtl_st_clear_carry lbl' ⇒
     476    Some ? (add_graph lbl (ertl_st_clear_carry lbl') def)
     477  | rtl_st_load d a1 a2 lbl' ⇒
     478    Some ? (add_graph lbl (ertl_st_load d a1 a2 lbl') def)
     479  | rtl_st_store a1 a2 s lbl' ⇒
     480    Some ? (add_graph lbl (ertl_st_store a1 a2 s lbl') def)
     481  | rtl_st_call_id f args ret_regs lbl' ⇒
     482    translate_call_id f args ret_regs lbl lbl' def
     483  | rtl_st_call_ptr r1 r2 regs1 regs2 lbl ⇒ None ? (* dpm: todo *)
     484  | rtl_st_cond_acc src lbl_true lbl_false ⇒
     485    Some ? (add_graph lbl (ertl_st_cond_acc src lbl_true lbl_false) def)
     486  | rtl_st_return ret_regs ⇒
     487    Some ? (add_graph lbl (ertl_st_return ret_regs) def)
     488  | rtl_st_tailcall_id ident regs ⇒ None ? (* dpm: impossible *)
     489  | rtl_st_tailcall_ptr r1 r2 regs ⇒ None ? (* dpm: impossible *)
     490  ].
     491
     492(* dpm: this should not be option, fix *)
     493axiom map_fold:
     494  ∀A, B: Type[0].
     495  ∀f: label → A → B → option B.
     496  ∀m: rtl_statement_graph.
     497  ∀b: B.
     498    B.
     499   
     500definition translate_internal ≝
     501  λdef.
     502  let nb_params ≝ length ? (rtl_if_params def) in
     503  let added_stacksize ≝ max 0 (nb_params - (length ? parameters)) in
     504  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
     505  let def' ≝
     506    mk_ertl_internal_function
     507      (rtl_if_luniverse def) (rtl_if_runiverse def)
     508      nb_params new_locals ((rtl_if_stacksize def) + added_stacksize)
     509      (empty_map ? ?) (rtl_if_entry def) (rtl_if_exit def) in
     510  let def' ≝ map_fold ? ? translate_stmt (rtl_if_graph def) def' in
     511  let def' ≝ add_pro_and_epilogue register_list_set (rtl_if_params def) (rtl_if_result def) def' in
     512    def'.
     513   
     514definition translate_funct ≝
     515  λid_def: ident × ?.
     516  let 〈id, def〉 ≝ id_def in
     517  let def' ≝
     518    match def with
     519    [ rtl_f_internal def ⇒
     520      match translate_internal def with
     521      [ None ⇒ None ?
     522      | Some internal_def ⇒ Some ? (ertl_f_internal internal_def)
     523      ]
     524    | rtl_f_external def ⇒ Some ? (ertl_f_external def)
     525    ] in
     526  〈id, def'〉.
     527
     528definition generate ≝
     529  λstmt.
     530  λdef.
     531  let entry ≝ fresh_label def in
     532  match entry with
     533  [ None ⇒ None ?
     534  | Some entry ⇒
     535    let def ≝ add_graph entry stmt def in
     536      Some ? (change_entry_label entry def)
     537  ].
     538 
  • src/common/Identifiers.ma

    r779 r782  
    6262  an_id_map : BitVectorTrie A 16 → identifier_map tag A.
    6363 
    64  
    6564definition empty_map : ∀tag:String. ∀A. identifier_map tag A ≝
    6665  λtag,A. an_id_map tag A (Stub A 16).
  • src/utilities/RegisterSet.ma

    r778 r782  
    1010  rs_insert: register → rs_set → rs_set;
    1111  rs_exists: register → rs_set → bool;
    12   rs_union: rs_set → rs_set → rs_set
     12  rs_union: rs_set → rs_set → rs_set;
     13  rs_to_list: rs_set → list register;
     14  rs_from_list: list register → rs_set
    1315}.
    1416
     
    4446    nub_by ? (eq_identifier ?) (r @ s).
    4547 
     48definition rs_list_set_from_list ≝
     49  λr: list register.
     50    nub_by ? (eq_identifier ?) r.
     51 
    4652definition register_list_set: register_set ≝
    4753  mk_register_set (list register) rs_list_set_empty
    4854                  rs_list_set_singleton rs_list_set_fold
    4955                  rs_list_set_insert rs_list_set_exists
    50                   rs_list_set_union.
     56                  rs_list_set_union
     57                  (λx. x) rs_list_set_from_list.
Note: See TracChangeset for help on using the changeset viewer.