Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (9 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
3 edited
1 copied

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/RTL/RTL.ma

    r1109 r1153  
    1010  | rtl_st_skip: label → rtl_statement
    1111  | rtl_st_cost: costlabel → label → rtl_statement
     12                (* ldest, hdest, symbol, next *)
    1213  | rtl_st_addr: register → register → ident → label → rtl_statement
     14                (* ldest, hdest, next *)
    1315  | rtl_st_stack_addr: register → register → label → rtl_statement
    1416  | rtl_st_int: register → Byte → label → rtl_statement
     17                (* dest, src, next *)
    1518  | rtl_st_move: register → register → label → rtl_statement
    1619  | rtl_st_clear_carry: label → rtl_statement
     20                (* op, acc dest, bacc dest, acc src, bacc src, next *)
    1721  | rtl_st_opaccs: OpAccs → register → register → register → register → label → rtl_statement
     22                (* op, dest, src, next *)
    1823  | rtl_st_op1: Op1 → register → register → label → rtl_statement
     24                (* op, dest, src1, src2, next *)
    1925  | rtl_st_op2: Op2 → register → register → register → label → rtl_statement
    2026  | rtl_st_load: register → register → register → label → rtl_statement
  • Deliverables/D3.3/id-lookup-branch/RTL/RTLtoERTL.ma

    r1109 r1153  
    9797  | ertl_st_pop r _ ⇒ ertl_st_pop r l
    9898  | ertl_st_push r _ ⇒ ertl_st_push r l
    99   | ertl_st_addr_h r id _ ⇒ ertl_st_addr_h r id l
    100   | ertl_st_addr_l r id _ ⇒ ertl_st_addr_l r id l
     99  | ertl_st_addr r1 r2 x _ ⇒ ertl_st_addr r1 r2 x l
    101100  | ertl_st_int r i _ ⇒ ertl_st_int r i l
    102101  | ertl_st_move r1 r2 _ ⇒ ertl_st_move r1 r2 l
    103   | ertl_st_opaccs_a opaccs d s1 s2 _ ⇒ ertl_st_opaccs_a opaccs d s1 s2 l
    104   | ertl_st_opaccs_b opaccs d s1 s2 _ ⇒ ertl_st_opaccs_b opaccs d s1 s2 l
     102  | ertl_st_opaccs opaccs d1 d2 s1 s2 _ ⇒ ertl_st_opaccs opaccs d1 s1 s1 s2 l
    105103  | ertl_st_op1 op1 d s1 _ ⇒ ertl_st_op1 op1 d s1 l
    106104  | ertl_st_op2 op2 d s1 s2 _ ⇒ ertl_st_op2 op2 d s1 s2 l
     
    224222  [ nil ⇒ [get_params_hdw_internal]
    225223  | _ ⇒
    226     let l ≝ zip_pottier ? ? params parameters in
     224    let l ≝ zip_pottier ? ? params RegisterParams in
    227225      save_hdws l
    228226  ].
     
    260258definition get_params ≝
    261259  λparams.
    262   let n ≝ min (length ? params) (length ? parameters) in
     260  let n ≝ min (length ? params) (length ? RegisterParams) in
    263261  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    264262  let hdw_params ≝ get_params_hdw hdw_params in
     
    396394  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
    397395  | _ ⇒
    398     let l ≝ zip_pottier ? ? params parameters in
     396    let l ≝ zip_pottier ? ? params RegisterParams in
    399397      restore_hdws l
    400398  ].
     
    436434definition set_params ≝
    437435  λparams.
    438   let n ≝ min (|params|) (|parameters|) in
     436  let n ≝ min (|params|) (|RegisterParams|) in
    439437  let hdw_stack_params ≝ split ? params n ? in
    440438  let hdw_params ≝ \fst hdw_stack_params in
     
    477475    add_translates (
    478476      set_params args @ [
    479       adds_graph [ ertl_st_call_id f (bitvector_of_nat ? nb_args) start_lbl ];
     477      adds_graph [ ertl_st_call_id f nb_args start_lbl ];
    480478      fetch_result ret_regs
    481479      ]
     
    489487  [ rtl_st_skip lbl' ⇒ add_graph lbl (ertl_st_skip lbl') def
    490488  | rtl_st_cost cost_lbl lbl' ⇒ add_graph lbl (ertl_st_cost cost_lbl lbl') def
    491   | rtl_st_addr r1 r2 x lbl' ⇒
    492     adds_graph [
    493       ertl_st_addr_l r1 x lbl;
    494       ertl_st_addr_h r2 x lbl
    495     ] lbl lbl' def
     489  | rtl_st_addr r1 r2 x lbl' ⇒ add_graph lbl (ertl_st_addr r1 r2 x lbl') def
    496490  | rtl_st_stack_addr r1 r2 lbl' ⇒
    497491    adds_graph [
     
    502496  | rtl_st_move r1 r2 lbl' ⇒ add_graph lbl (ertl_st_move r1 r2 lbl') def
    503497  | rtl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl' ⇒
     498      add_graph lbl (ertl_st_opaccs op destr1 destr2 srcr1 srcr2 lbl) def
     499(* XXX: change from o'caml
    504500    adds_graph [
    505501      ertl_st_opaccs_a op destr1 srcr1 srcr2 lbl;
    506502      ertl_st_opaccs_b op destr2 srcr1 srcr2 lbl
    507503      ] lbl lbl' def
     504*)
    508505  | rtl_st_op1 op1 destr srcr lbl' ⇒
    509506    add_graph lbl (ertl_st_op1 op1 destr srcr lbl') def
     
    533530  λdef.
    534531  let nb_params ≝ |rtl_if_params def| in
    535   let added_stacksize ≝ max 0 (nb_params - |parameters|) in
     532  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
    536533  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
    537534  let entry' ≝ rtl_if_entry def in
     
    619616      | ertl_st_pop _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    620617      | ertl_st_push _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    621       | ertl_st_addr_h _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    622       | ertl_st_addr_l _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     618      | ertl_st_addr _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    623619      | ertl_st_int _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    624620      | ertl_st_move _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    625       | ertl_st_opaccs_a _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    626       | ertl_st_opaccs_b _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
     621      | ertl_st_opaccs _ _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    627622      | ertl_st_op1 _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
    628623      | ertl_st_op2 _ _ _ _ lbl ⇒ find_and_remove_first_cost_label_internal def lbl num_nodes'
Note: See TracChangeset for help on using the changeset viewer.