Changeset 1281


Ignore:
Timestamp:
Sep 28, 2011, 11:08:37 PM (8 years ago)
Author:
sacerdot
Message:

Porting of all transformation to the joint syntax practically completed.
Some functions remain to be ported in RTLAbstoRTL, but it is just repetitive
coding.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r1275 r1281  
    33include "ERTL/spill.ma".
    44include "ASM/Arithmetic.ma".
    5 
    6 (* XXX: define an interference graph for a function and colour it, allowing
    7         the consultation of registers.
    8 definition initial_colouring ≝
    9   λglobals.
    10   λint_fun.
    11   let 〈ignore, graph〉 ≝ build globals int_fun in
    12   let coloured ≝ colour_initial graph in
    13     coloured.
    14 
    15 definition interference_lookup ≝
    16   λcoloured: initial_colouring.
    17   λr.
    18     colouring … coloured r.
    19 
    20 definition prepare_graph_for_second_colouring ≝
    21   λglobals: list ident.
    22   λcoloured: initial_colouring.
    23     let g ≝ the_graph decision coloured in
    24     let restricted ≝ ig_restrict g (λv.
    25       match colouring decision coloured v with
    26       [ decision_spill ⇒ true
    27       | decision_colour _ ⇒ false
    28       ]
    29     )
    30     in restricted.
    31 
    32 definition second_colouring ≝
    33   λglobals: list ident.
    34   λcoloured.
    35     let prepared ≝ prepare_graph_for_second_colouring globals coloured in
    36       colour_stack prepared.
    37 
    38 definition lookup ≝
    39   λinitial.
    40   λsecond.
    41   λr.
    42   match interference_lookup initial r with
    43   [ decision_colour _ ⇒ ?
    44   | decision_spill ⇒ ?
    45   ].
    46 *)
    475
    486definition fresh_label ≝
     
    397355    | joint_instr_opaccs opaccs dacc_a_reg dacc_b_reg sacc_a_reg sacc_b_reg ⇒
    398356      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    399       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    400       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_a_reg l fresh_lbl in
     357      let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph dacc_a_reg l fresh_lbl in
    401358      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    402       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in
    403       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    404       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    405       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    406       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    407       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc RegisterB)) fresh_lbl) in
    408       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    409       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    410       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    411       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … (joint_instr_move … (to_acc hdw)) l) fresh_lbl in
    412       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_goto … fresh_lbl) in
    413       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    414       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    415       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    416       let 〈hdw, l, graph, luniv〉 ≝ write globals int_fun valuation coloured_graph graph acc_b_reg l fresh_lbl in
    417       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (from_acc hdw)) l) in
    418       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_move … (to_acc RegisterB)) l) in
    419       let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it) l) in
    420       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    421       let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    422       let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    423       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in
     359      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … (joint_instr_opaccs … opaccs it it it it) l) in
     360      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     361      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
     362      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
     363      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_a_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in
    424364      let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential … globals (joint_instr_move … globals (from_acc RegisterB)) fresh_lbl) in
    425365      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    426366      let 〈fresh_lbl, luniv〉 ≝ fresh_label globals luniv in
    427367      let int_fun ≝ set_luniverse globals (ertl_params globals) int_fun luniv in
    428       let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph acc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in
     368      let 〈graph, luniv〉 ≝ read globals int_fun valuation coloured_graph graph sacc_b_reg (λhdw. joint_st_sequential … globals (joint_instr_move … globals (to_acc hdw)) l) fresh_lbl in
    429369        〈add_graph globals original_label (joint_st_goto … globals fresh_lbl) graph, luniv〉
    430370    ]
     
    522462
    523463definition ertl_to_ltl: ertl_program → ltl_program ≝
    524   λp.
    525     transform_program … p (transf_fundef … (translate_internal …)).
     464  λp.transform_program … p (transf_fundef … (translate_internal …)).
  • src/LIN/LIN.ma

    r1270 r1281  
    22include "utilities/lists.ma".
    33
    4 definition lin_params_: params_ ≝
    5  mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) unit.
     4definition lin_params__: params__ ≝
     5 mk_params__ unit unit unit unit registers_move Register nat unit False.
     6definition lin_params_ : params_ ≝ mk_params_ lin_params__ unit.
     7definition lin_params0 : params0 ≝ mk_params0 lin_params__ unit unit.
     8definition lin_params1 : params1 ≝ mk_params1 lin_params0 unit.
    69
    710definition pre_lin_statement ≝ joint_statement lin_params_.
     
    2124definition lin_params: ∀globals. params globals ≝
    2225 λglobals.
    23   mk_params globals lin_params_ (Σcode:list (lin_statement globals). well_formed_P … code)
     26  mk_params globals unit lin_params1 (Σcode:list (lin_statement globals). well_formed_P … code)
    2427   (λcode:Σcode.?. λl.
    2528    find ?? (λs. let 〈l',x〉 ≝ s in
  • src/LTL/LTL.ma

    r1280 r1281  
    11include "joint/Joint.ma".
    22
    3 definition ltl_params_: params_ ≝
    4  label_params__of_params__
    5   (mk_params__ unit unit unit unit registers_move Register nat unit False unit
    6     unit unit).
     3definition ltl_params__: params__ ≝
     4 (mk_params__ unit unit unit unit registers_move Register nat unit False).
     5definition ltl_params_ : params_ ≝ graph_params_ ltl_params__.
     6definition ltl_params0 : params0 ≝ mk_params0 ltl_params__ unit unit.
     7definition ltl_params1 : params1 ≝ mk_params1 ltl_params0 unit.
     8definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params1.
    79
    810definition ltl_statement ≝ joint_statement ltl_params_.
    911
    10 definition ltl_params: ∀globals. params globals ≝ graph_params ltl_params_.
    11 
    1212definition ltl_program ≝ joint_program ltl_params.
    1313
    14 definition ltl_internal_function ≝ λglobals. joint_internal_function globals (ltl_params globals).
     14definition ltl_internal_function ≝
     15 λglobals. joint_internal_function … (ltl_params globals).
  • src/RTLabs/RTLAbstoRTL.ma

    r1280 r1281  
    66include "joint/TranslateUtils.ma".
    77
    8 (*
    98let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
    109  match n with
    11   [ O ⇒ [ ]
    12   | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
    13   ].
    14 *)
     10  [ O ⇒ 〈[],runiverse〉
     11  | S n' ⇒
     12     let 〈r,runiverse〉 ≝ fresh … runiverse in
     13     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
     14      〈r::res,runiverse〉 ].
    1515
    1616definition choose_rest ≝
     
    8787  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
    8888
    89 (*
    9089definition initialize_local_env_internal ≝
    91   λruniverse.
    92   λlenv.
     90  λlenv_runiverse.
    9391  λr_sig.
     92  let 〈lenv,runiverse〉 ≝ lenv_runiverse in
    9493  let 〈r, sig〉 ≝ r_sig in
    9594  let size ≝ size_of_sig_type sig in
    96   let rs ≝ register_freshes runiverse size in
    97     add_local_env r rs lenv.
     95  let 〈rs,runiverse〉 ≝ register_freshes runiverse size in
     96    〈add_local_env r rs lenv,runiverse〉.
    9897
    9998definition initialize_local_env ≝
     
    107106    ]
    108107  in
    109     foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
    110 *)
     108    foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers.
    111109
    112110definition map_list_local_env_internal ≝
     
    219217    ] start_lbl dest_lbl def.
    220218
     219(*
    221220definition translate_cast_signed ≝
    222221  λglobals.
     
    10071006  ]
    10081007qed.
     1008*)
    10091009
    10101010definition translate_stmt ≝
    1011   λlenv.
     1011  λglobals.
     1012  λlenv: local_env.
    10121013  λlbl: label.
    10131014  λstmt.
    1014   λdef: rtl_internal_function.
     1015  λdef: joint_internal_function … (rtl_params globals).
    10151016  match stmt with
    1016   [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def
     1017  [ St_skip lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
     1018  | _ ⇒ ? ].
     1019(*
    10171020  | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
    10181021  | St_const destr cst lbl' ⇒
     
    10541057  |*: cases daemon (* TODO: proofs regarding lengths of lists, examine! *)
    10551058  ]
     1059*) cases daemon
    10561060qed.
    10571061
     
    10611065   skip instructions at these nodes. *)
    10621066definition translate_internal ≝
    1063   λdef.
     1067  λglobals,def.
    10641068  let runiverse ≝ f_reggen def in
    1065   let lenv ≝ initialize_local_env runiverse
     1069  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    10661070    (f_params def @ f_locals def) (f_result def) in
    10671071  let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
     
    10831087  let entry' ≝ f_entry def in
    10841088  let exit' ≝ f_exit def in
    1085   let graph' ≝ add ? ? (empty_map ? ?) entry' (rtl_st_skip entry') in
    1086   let graph' ≝ add ? ? graph' exit' (rtl_st_skip exit') in
     1089  let graph' ≝ add … (empty_map ? ?) entry' (joint_st_goto … entry') in
     1090  let graph' ≝ add … graph' exit' (joint_st_goto … exit') in
    10871091  let res ≝
    1088     mk_rtl_internal_function luniverse' runiverse' result' params'
    1089                          locals' stack_size' graph' ? ? in
    1090     foldi ? ? ? (translate_stmt lenv) (f_graph def) res.
    1091   [1: %
    1092       [1: @entry'
    1093       |2: normalize nodelta;
    1094           @graph_add_lookup
    1095           @graph_add
    1096       ]
    1097   |2: %
    1098       [1: @exit'
    1099       |2: normalize nodelta;
    1100           @graph_add
    1101       ]
    1102   ]
     1092    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
     1093     locals' stack_size' graph' ? ? in
     1094    foldi … (translate_stmt … lenv) (f_graph def) res.
     1095[ % [@entry' | @graph_add_lookup @graph_add]
     1096| % [@exit'  | @graph_add]]
    11031097qed.
    11041098
     
    11061100  because of CompCert heritage *)
    11071101definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝
    1108  λp. transform_program … p (transf_fundef … translate_internal).
     1102 λp. transform_program ??? p (transf_fundef … (translate_internal (prog_var_names …))).
  • src/joint/semantics.ma

    r1250 r1281  
    1717  eq_beval (\fst addr1) (\fst addr2) ∧ eq_beval (\snd addr1) (\snd addr2).
    1818
    19 record more_sem_params (p:params_): Type[1] ≝
     19record more_sem_params (p:params1): Type[1] ≝
    2020 { framesT: Type[0]
    21  ; regsT: Type[0] (* regs = pseudo-registers + hw registers *)
     21 ; regsT: Type[0]
    2222
    2323 ; succ_pc: succ p → address → address
     
    5555
    5656definition genv ≝ λglobals.λp:params globals. (genv_t Genv) (joint_function globals p).
    57 
    58 (*
    59 CSC: fetch_statement credo sia implementabile ⇒ globals non e' necessario ⇒ niente
    60 casino e posso back-trackare il cambiamento in SmallstepExec!!! Togliere del
    61 tutto il parametro a exec_extended.
    62 CSC: NO! RTL ha come exec_extended tail_call e (tail_)call_ptr che usa genv
    63 *)
    6457
    6558record more_sem_params2 (globals: list ident) (p: params globals) : Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.