Changeset 1250


Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (8 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
Files:
9 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
  • src/LIN/LIN.ma

    r1246 r1250  
    1919definition lin_statement ≝ λglobals.(option label) × (pre_lin_statement globals).
    2020
    21 (*CSC: move elsewhere, also in joint/semantics.ma *)
    22 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    23  λA,P,c. match c with [ dp w _ ⇒ w ].
    24 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    25 
    2621definition lin_params: ∀globals. params globals ≝
    2722 λglobals.
  • src/LTL/LTLToLIN.ma

    r1246 r1250  
    88  λs: ltl_statement globals.
    99  match s with
    10   [ joint_st_return ⇒ joint_st_return
     10  [ joint_st_return ⇒ joint_st_return ??
    1111  | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
    12   | joint_st_goto l ⇒ joint_st_goto … l
    13   | joint_st_extension ext ⇒ joint_st_extension lin_params_ … ext
     12  | joint_st_goto l ⇒ joint_st_goto lin_params_ globals l
    1413  ].
    1514
     
    4948         | _ ⇒ visit globals g required visited' generated' l2 n']
    5049     | joint_st_return ⇒ 〈required, generated'〉
    51      | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n'
    52      | joint_st_extension ext ⇒ ⊥ ]]].
    53 [3: @ext
    54 |1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
     50     | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n']]].
     51[1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
    5552qed.
    5653
  • src/RTL/RTLtoERTL.ma

    r1245 r1250  
    33include "common/Identifiers.ma".
    44include "ERTL/ERTL.ma".
     5include "utilities/extralib.ma". (* CSC: Only for Sigma type projections *)
    56                     
    67definition add_graph ≝
    7   λl: label.
    8   λstmt.
    9   λp.
    10   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    11   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    12   let ertl_if_params' ≝ ertl_if_params p in
    13   let ertl_if_locals' ≝ ertl_if_locals p in
    14   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    15   let ertl_if_graph' ≝ add ? ? (ertl_if_graph p) l stmt in
    16   let ertl_if_entry' ≝ ertl_if_entry p in
    17   let ertl_if_exit' ≝ ertl_if_exit p in
    18     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    19                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    20                               ertl_if_graph' ? ?.
     8  λglobals.λl: label.λstmt.λp: joint_internal_function … (ertl_params globals).
     9   let code ≝ add … (joint_if_code … p) l stmt in
     10    mk_joint_internal_function … (ertl_params globals)
     11     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     12     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     13     code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)).
    2114  normalize nodelta;
    22   [1: generalize in match ertl_if_entry';
    23       #HYP
    24       cases HYP
    25       #LBL #LBL_PRF
    26       %
    27       [1: @LBL
    28       |2: @graph_add_lookup
    29           @LBL_PRF
    30       ]
    31   |2: generalize in match ertl_if_exit';
    32       #HYP
    33       cases HYP
    34       #LBL #LBL_PRF
    35       %
    36       [1: @LBL
    37       |2: @graph_add_lookup
    38           @LBL_PRF
    39       ]
    40   ]
     15  [ cases (joint_if_entry … p) | cases (joint_if_exit … p)]
     16  #LBL #LBL_PRF @graph_add_lookup @LBL_PRF
    4117qed.
    4218                           
    4319definition fresh_label ≝
    44   λdef.
    45     fresh LabelTag (ertl_if_luniverse def).
     20  λglobals.λdef: joint_internal_function … (ertl_params globals).
     21    fresh LabelTag (joint_if_luniverse … def).
    4622   
    4723definition change_label ≝
    48   λl.
    49   λe: ertl_statement.
     24  λglobals.λe: joint_statement ertl_params_ globals.λl.
    5025  match e with
    51   [ ertl_st_skip _ ⇒ ertl_st_skip l
     26  [ joint_st_goto _ ⇒ joint_st_goto … l
     27  | joint_st_return ⇒ joint_st_return …
     28  | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l
     29  | joint_st_extension ].
    5230  | ertl_st_comment s _ ⇒ ertl_st_comment s l
    5331  | ertl_st_cost c _ ⇒ ertl_st_cost c l
  • src/joint/Joint.ma

    r1246 r1250  
    4141  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    4242  | joint_instr_call_id: ident → nat → joint_instruction p globals
    43   | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
     43  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals
     44  | joint_instr_extension: extend_statements p → joint_instruction p globals.
    4445
    4546inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
    4647  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    4748  | joint_st_goto: label → joint_statement p globals
    48   | joint_st_return: joint_statement p globals
    49   | joint_st_extension: extend_statements p → joint_statement p globals.
     49  | joint_st_return: joint_statement p globals.
     50
    5051
    5152record params (globals: list ident): Type[1] ≝
  • src/joint/semantics.ma

    r1247 r1250  
    205205axiom FailedLoad : String.
    206206axiom BadFunction : String.
    207 
    208 (*CSC: move elsewhere, also in LIN.ma *)
    209 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    210  λA,P,c. match c with [ dp w _ ⇒ w ].
    211 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    212207
    213208definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
  • src/utilities/extralib.ma

    r891 r1250  
    721721| #m #H @(False_ind … H)
    722722] qed.
     723
     724(* Stuff about Sigma types *)
     725definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
     726 λA,P,c. match c with [ dp w _ ⇒ w ].
     727coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
Note: See TracChangeset for help on using the changeset viewer.