Changeset 1250 for src/ERTL


Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (9 years ago)
Author:
sacerdot
Message:
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
Location:
src/ERTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1249 r1250  
    44include "ERTL/build.ma".
    55include "ERTL/uses.ma".
    6 include "ERTL/Interference.ma".
    76include "ASM/Arithmetic.ma".
    87
     
    365364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (to_acc RegisterDPL)) l) in
    366365        〈joint_st_sequential (ltl_params globals) globals (joint_instr_address … globals lbl prf it it) l, graph, luniv〉
     366    | joint_instr_extension ext ⇒
     367      match ext with
     368      [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
     369      | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
     370      | ertl_st_ext_frame_size r l ⇒
     371        let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
     372          〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
     373      ]
    367374    ]
    368375  | joint_st_return ⇒ 〈joint_st_return … globals, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    369376  | joint_st_goto l ⇒ 〈joint_st_goto … globals l, graph, joint_if_luniverse globals (ertl_params globals) int_fun〉
    370   | joint_st_extension ext ⇒
    371     match ext with
    372     [ ertl_st_ext_new_frame l ⇒ newframe globals int_fun graph l
    373     | ertl_st_ext_del_frame l ⇒ delframe globals int_fun graph l
    374     | ertl_st_ext_frame_size r l ⇒
    375       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph r l in
    376         〈joint_st_sequential (ltl_params globals) globals (joint_instr_int … globals hdw (bitvector_of_nat ? (stacksize globals int_fun))) l, graph, luniv〉
    377     ]
    378377  ].
    379378
  • src/ERTL/liveness.ma

    r1249 r1250  
    1111    [ joint_instr_cond acc_a_reg lbl_true ⇒
    1212        set_insert … lbl_true (set_singleton … l)
    13     | _ ⇒ set_singleton … l
    14     ]
    15   | joint_st_extension ext ⇒
    16     match ext with
    17     [ ertl_st_ext_new_frame l ⇒ set_singleton … l
    18     | ertl_st_ext_del_frame l ⇒ set_singleton … l
    19     | ertl_st_ext_frame_size r l ⇒ set_singleton … l
    20     ]
     13    | _ ⇒ set_singleton … l ]
    2114  | joint_st_goto l ⇒ set_singleton … l
    22   | joint_st_return ⇒ set_empty
     15  | joint_st_return ⇒ set_empty ?
    2316  ].
    2417
     
    116109      | hardware h ⇒ lattice_hsingleton h
    117110      ]
    118     ]
     111    | joint_instr_extension ext ⇒
     112      match ext with
     113      [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     114      | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
     115      | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r]]
    119116  | joint_st_return ⇒ lattice_bottom
    120   | joint_st_extension ext ⇒
    121     match ext with
    122     [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    123     | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    124     | ertl_st_ext_frame_size r l ⇒ lattice_psingleton r
    125     ]
    126117  | joint_st_goto l ⇒ lattice_bottom
    127118  ].
     
    165156      | hardware h ⇒ lattice_hsingleton h
    166157      ]
    167     ]
    168   | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    169   | joint_st_goto l ⇒ lattice_bottom
    170   | joint_st_extension ext ⇒
     158  | joint_instr_extension ext ⇒
    171159    match ext with
    172160    [ ertl_st_ext_new_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    173161    | ertl_st_ext_del_frame l ⇒ lattice_join (lattice_hsingleton RegisterSPL) (lattice_hsingleton RegisterSPH)
    174     | ertl_st_ext_frame_size r l ⇒ lattice_bottom
    175     ]
     162    | ertl_st_ext_frame_size r l ⇒ lattice_bottom]]
     163  | joint_st_return ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
     164  | joint_st_goto l ⇒ lattice_bottom
    176165  ].
    177166
     
    245234          None ?
    246235        else
    247           Some ? l
    248       ]
    249     ]
     236          Some ? l]
     237    | joint_instr_extension ext ⇒
     238      match ext with
     239      [ ertl_st_ext_new_frame l ⇒ None ?
     240      | ertl_st_ext_del_frame l ⇒ None ?
     241      | ertl_st_ext_frame_size r l ⇒
     242        if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
     243           set_member ? eq_Register RegisterCarry hliveafter then
     244          None ?
     245        else
     246          Some ? l]]
    250247  | joint_st_goto l ⇒ None ?
    251248  | joint_st_return ⇒ None ?
    252   | joint_st_extension ext ⇒
    253     match ext with
    254     [ ertl_st_ext_new_frame l ⇒ None ?
    255     | ertl_st_ext_del_frame l ⇒ None ?
    256     | ertl_st_ext_frame_size r l ⇒
    257       if set_member ? (eq_identifier RegisterTag) r pliveafter ∨
    258          set_member ? eq_Register RegisterCarry hliveafter then
    259         None ?
    260       else
    261         Some ? l
    262     ]
    263249  ].
    264250
  • src/ERTL/uses.ma

    r1249 r1250  
    11include "ERTL/ERTL.ma".
    2 
    32include "utilities/adt/table_adt.ma".
    43
     
    3332        match reg2 with
    3433        [ pseudo p ⇒ count p uses
    35         | hardware h2 ⇒ uses
    36         ]
    37       ]
     34        | hardware h2 ⇒ uses]]
    3835    | joint_instr_clear_carry ⇒ uses
    3936    | joint_instr_set_carry ⇒ uses
     
    4946    | joint_instr_store srcr r1 r2 ⇒ count r1 (count r2 (count srcr uses))
    5047    | joint_instr_cond srcr l2 ⇒ count srcr uses
    51     ]
     48    | joint_instr_extension ext ⇒
     49      match ext with
     50      [ ertl_st_ext_new_frame l ⇒ uses
     51      | ertl_st_ext_del_frame l ⇒ uses
     52      | ertl_st_ext_frame_size r l ⇒ count r uses]]
    5253  | joint_st_return ⇒ uses
    5354  | joint_st_goto l ⇒ uses
    54   | joint_st_extension ext ⇒
    55     match ext with
    56     [ ertl_st_ext_new_frame l ⇒ uses
    57     | ertl_st_ext_del_frame l ⇒ uses
    58     | ertl_st_ext_frame_size r l ⇒ count r uses
    59     ]
    6055  ].
    6156
Note: See TracChangeset for help on using the changeset viewer.