Changeset 1280


Ignore:
Timestamp:
Sep 28, 2011, 2:43:37 AM (8 years ago)
Author:
sacerdot
Message:

Some progress in the porting of RTLAbstoRTL to the joint syntax:

1) common code with RTLtoERTL factorized out in joint/TranslateUtils.ma
2) this required yet another refactoring of the parameters in Joint.ma
3) RTLtoERTL ported to the new parameters; LTLtoLIN and LINtoASM are

probably broken but easily fixable a.t.m. RTLAbstoRTL still in progress,
but the difficult part is almost done.

Location:
src
Files:
1 added
6 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1270 r1280  
    1010  | ertl_st_ext_frame_size: register → ertl_statement_extension.
    1111
    12 definition ertl_params_: params_ ≝
    13  mk_params_
    14   (mk_params__ register register register register
    15     (move_registers × move_registers) register nat unit
    16       ertl_statement_extension unit (list register) nat) label.
     12definition ertl_params__: params__ ≝
     13 mk_params__ register register register register (move_registers × move_registers)
     14  register nat unit ertl_statement_extension.
     15definition ertl_params_: params_ ≝ graph_params_ ertl_params__.
     16definition ertl_params0: params0 ≝ mk_params0 ertl_params__ unit nat.
     17definition ertl_params1: params1 ≝ rtl_ertl_params1 ertl_params0.
     18definition ertl_params: ∀globals. params globals ≝ rtl_ertl_params ertl_params0.
    1719
    1820definition ertl_statement ≝ joint_statement ertl_params_.
    1921
    20 definition ertl_params: ∀globals. params globals ≝ graph_params ertl_params_.
    21 
    2222definition ertl_internal_function ≝
    23   λglobals.
    24     joint_internal_function globals (ertl_params globals).
     23  λglobals.joint_internal_function … (ertl_params globals).
    2524
    2625definition ertl_program ≝ joint_program ertl_params.
  • src/LTL/LTL.ma

    r1271 r1280  
    22
    33definition ltl_params_: params_ ≝
    4  mk_params_ (mk_params__ unit unit unit unit registers_move Register nat unit False unit unit unit) label.
     4 label_params__of_params__
     5  (mk_params__ unit unit unit unit registers_move Register nat unit False unit
     6    unit unit).
    57
    68definition ltl_statement ≝ joint_statement ltl_params_.
  • src/RTL/RTL.ma

    r1278 r1280  
    1010  | rtl_st_ext_tailcall_ptr: register → register → list register → rtl_statement_extension.
    1111
    12 definition rtl_params_: params_ ≝
    13  mk_params_
    14   (mk_params__ register register register register
    15     (register × register) register (list register) (list register)
    16       rtl_statement_extension (list register) (list register) (list register)) label.
     12definition rtl_params__: params__ ≝
     13 mk_params__ register register register register (register × register) register
     14  (list register) (list register) rtl_statement_extension.
     15definition rtl_params_: params_ ≝ graph_params_ rtl_params__.
     16definition rtl_params0: params0 ≝ mk_params0 rtl_params__ (list register) (list register).
     17definition rtl_params1: params1 ≝ rtl_ertl_params1 rtl_params0.
     18definition rtl_params: ∀globals. params globals ≝ rtl_ertl_params rtl_params0.
    1719
    1820definition rtl_statement ≝ joint_statement rtl_params_.
    1921
    20 definition rtl_params: ∀globals. params globals ≝ graph_params rtl_params_.
    21 
    2222definition rtl_internal_function ≝
    23   λglobals.
    24     joint_internal_function globals (rtl_params globals).
     23  λglobals. joint_internal_function … (rtl_params globals).
    2524
    2625definition rtl_program ≝ joint_program rtl_params.
     
    3534  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
    3635
    37 definition rtlntc_params_: params_ ≝
    38  mk_params_
    39   (mk_params__ register register register register
    40     (register × register) register (list register) (list register)
    41       rtlntc_statement_extension (list register) (list register) (list register)) label.
     36definition rtlntc_params__: params__ ≝
     37 mk_params__ register register register register (register × register) register
     38  (list register) (list register) rtlntc_statement_extension.
     39definition rtlntc_params_: params_ ≝ graph_params_ rtlntc_params__.
     40definition rtlntc_params0: params0 ≝ mk_params0 rtlntc_params__ (list register) (list register).
     41definition rtlntc_params1: params1 ≝ rtl_ertl_params1 rtlntc_params0.
     42definition rtlntc_params: ∀globals. params globals ≝ rtl_ertl_params rtlntc_params0.
    4243
    4344definition rtlntc_statement ≝ joint_statement rtlntc_params_.
    4445
    45 definition rtlntc_params: ∀globals. params globals ≝ graph_params rtlntc_params_.
    46 
    4746definition rtlntc_internal_function ≝
    48   λglobals.
    49     joint_internal_function globals (rtlntc_params globals).
     47  λglobals. joint_internal_function … (rtlntc_params globals).
    5048
    5149definition rtlntc_program ≝ joint_program rtlntc_params.
  • src/RTL/RTLtoERTL.ma

    r1278 r1280  
    33include "common/Identifiers.ma".
    44include "ERTL/ERTL.ma".
    5                            
    6 definition fresh_label ≝
    7   λglobals.λdef: joint_internal_function … (ertl_params globals).
    8     fresh LabelTag (joint_if_luniverse … def).
    9    
    10 definition change_label ≝
    11   λglobals.λe: joint_statement ertl_params_ globals.λl.
    12   match e with
    13   [ joint_st_goto _ ⇒ joint_st_goto … l
    14   | joint_st_return ⇒ joint_st_return ??
    15   | joint_st_sequential instr _ ⇒ joint_st_sequential … instr l].
    16 
    17 (*CSC: bad programming habit: the code below puts everywhere a fake
    18   label and then adds_graph fixes them *)
    19 (*CSC: the code is artificially fixed to work on ertl_statements, but
    20   it works on every graph_params *)
    21 (*CSC: this is just an instance of add_translates below! *)
    22 let rec adds_graph
    23   (globals: list ident)
    24   (stmt_list: list (ertl_statement globals)) (start_lbl: label)
    25   (dest_lbl: label) (def: ertl_internal_function globals)
    26     on stmt_list ≝
    27   match stmt_list with
    28   [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
    29   | cons stmt stmt_list ⇒
    30     match stmt_list with
    31     [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def
    32     | _ ⇒
    33       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    34       let stmt ≝ change_label … stmt tmp_lbl in
    35       let def ≝ add_graph … start_lbl stmt def in
    36         adds_graph globals stmt_list tmp_lbl dest_lbl def]].
    37 
    38 (*CSC: bad programming habit: the code below puts everywhere a fake
    39   label and then adds_graph fixes them *)
    40 (*CSC: the code is artificially fixed to work on ertl_statements, but
    41   it works on every graph_params *)
    42 let rec add_translates
    43   (globals: list ident) (translate_list: list ?) (start_lbl: label) (dest_lbl: label)
    44   (def: ertl_internal_function globals)
    45     on translate_list ≝
    46   match translate_list with
    47   [ nil ⇒ add_graph … start_lbl (joint_st_goto … dest_lbl) def
    48   | cons trans translate_list ⇒
    49     match translate_list with
    50     [ nil ⇒ trans start_lbl dest_lbl def
    51     | _ ⇒
    52       let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    53       let def ≝ trans start_lbl tmp_lbl def in
    54         add_translates globals translate_list tmp_lbl dest_lbl def]].
    55 
    56 definition fresh_reg:
    57  ∀globals. ertl_internal_function globals → (ertl_internal_function globals) × register ≝
    58   λglobals,def.
    59     let 〈r,runiverse〉 ≝ fresh … (joint_if_runiverse … def) in
    60      〈set_locals … (set_runiverse … def runiverse) (r::joint_if_locals … def), r〉.
    61 
    62 let rec fresh_regs (globals: list ident) (def: ertl_internal_function globals) (n: nat) on n ≝
    63   match n with
    64   [ O ⇒ 〈def, [ ]〉
    65   | S n' ⇒
    66     let 〈def', regs'〉 ≝ fresh_regs globals def n' in
    67     let 〈def', reg〉 ≝ fresh_reg … def' in
    68       〈def', reg :: regs'〉
    69   ].
    70  
    71 lemma fresh_regs_length:
    72  ∀globals.∀def: ertl_internal_function globals. ∀n: nat.
    73   |(\snd (fresh_regs … def n))| = n.
    74  #globals #def #n elim n
    75   [ %
    76   | #m whd in ⊢ (? → ??(??%)?) whd in ⊢ (? → ??(??match % with [ _ ⇒ ?])?)
    77     cases (fresh_regs globals def m) normalize nodelta
    78     #def' #regs #EQ change in EQ with (|regs| = m) <EQ
    79     change with
    80     (|let 〈a,b〉 ≝ let 〈x,y〉 ≝ let 〈r,runiverse〉 ≝ ? in ? in ? in ?| = ?)
    81     cases (fresh … (joint_if_runiverse … def')) normalize // ]
    82 qed.
    83 
    84 definition fresh_regs_strong:
    85  ∀globals. ertl_internal_function globals →
    86   ∀n: nat. Σregs: (ertl_internal_function globals) × (list register). |\snd regs| = n ≝
    87  λdef,n.fresh_regs def n. //
    88 qed.
     5include "joint/TranslateUtils.ma".
    896
    907definition save_hdws ≝
     
    9310   λdestr_srcr.λstart_lbl.
    9411    let 〈destr, srcr〉 ≝ destr_srcr in
    95      adds_graph globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
     12     adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
    9613  in
    9714   map ? ? save_hdws_internal l.
     
    10320    λstart_lbl: label.
    10421     let 〈srcr, destr〉 ≝ srcr_destr in
    105      adds_graph globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
     22     adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
    10623   in
    10724    map ? ? restore_hdws_internal l.
     
    11128  λparams: list register.
    11229  match params with
    113   [ nil ⇒ [λstart_lbl: label. adds_graph globals [ joint_st_goto … start_lbl ] start_lbl]
     30  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ joint_st_goto … start_lbl ] start_lbl]
    11431  | _ ⇒
    11532    let l ≝ zip_pottier ? ? params RegisterParams in
     
    12643  let 〈def, tmpr〉 ≝ fresh_reg … def in
    12744  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    128   adds_graph globals [
     45  adds_graph ertl_params1 globals [
    12946    joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl;
    13047    joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl;
     
    16077  let start_lbl ≝ joint_if_entry … (ertl_params globals) def in
    16178  let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    162   match lookup … (joint_if_code … (ertl_params globals) def) start_lbl
     79  match lookup … (joint_if_code … def) start_lbl
    16380    return λx. x ≠ None ? → ertl_internal_function globals with
    16481  [ None ⇒ λnone_absrd. ⊥
     
    16683    let def ≝
    16784      add_translates …
    168          ((adds_graph … [
    169                      joint_st_sequential … (joint_instr_extension ertl_params_ globals ertl_st_ext_new_frame) start_lbl
     85         ((adds_graph ertl_params1 … [
     86                     joint_st_sequential ertl_params_ … (joint_instr_extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl
    17087                   ]) ::
    17188         (adds_graph … [
     
    196113    let restl ≝ \snd (\fst crl) in
    197114    let restr ≝ \snd (\snd crl) in
    198     let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero ?)) start_lbl in
     115    let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero )) start_lbl in
    199116    let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in
    200     let saves ≝ map2 ? ? ? f_save commonl commonr crl_proof in
     117    let saves ≝ map2 f_save commonl commonr crl_proof in
    201118    let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in
    202     let defaults ≝ map ? ? f_default restl in
    203       adds_graph … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     119    let defaults ≝ map f_default restl in
     120      adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
    204121  ].
    205122
     
    212129    let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in
    213130    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    214       adds_graph … insts start_lbl
     131      adds_graph ertl_params1 … insts start_lbl
    215132  ].
    216133
     
    224141  let start_lbl ≝ joint_if_exit … (ertl_params globals) def in
    225142  let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    226   match lookup … (joint_if_code … (ertl_params globals) def) start_lbl
     143  match lookup … (joint_if_code … def) start_lbl
    227144    return λx. x ≠ None ? → ertl_internal_function globals with
    228145  [ None ⇒ λnone_absrd. ⊥
    229146  | Some last_stmt ⇒ λsome_prf.
    230147    let def ≝
    231       add_translates … (
     148      add_translates ertl_params1 … (
    232149        [save_return globals ret_regs] @
    233150        restore_hdws … sregs @
     
    236153          joint_st_sequential … (joint_instr_push … sral) start_lbl
    237154        ]] @
    238         [adds_graph … [
     155        [adds_graph ertl_params1 … [
    239156          joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl
    240157        ]] @
     
    261178    λdef_sregs.
    262179    let 〈def, sregs〉 ≝ def_sregs in
    263     let 〈def, r'〉 ≝ fresh_reg globals def in
     180    let 〈def, r'〉 ≝ fresh_reg ertl_params0 globals def in
    264181      〈def, 〈r', r〉 :: sregs〉
    265182   in
     
    271188  λret_regs.
    272189  λdef.
    273   match fresh_regs_strong globals def 2 with
     190  match fresh_regs_strong globals def 2 with
    274191  [ dp def_sra def_sra_proof ⇒
    275192    let def ≝ \fst def_sra in
     
    305222  let 〈def, tmpr〉 ≝ fresh_reg … def in
    306223  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    307     adds_graph ? [
     224    adds_graph ertl_params1 … [
    308225      joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl;
    309226      joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
     
    319236  λglobals,params.
    320237  match params with
    321   [ nil ⇒ [ λstart_lbl. adds_graph globals [joint_st_goto … start_lbl] start_lbl]
     238  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [joint_st_goto … start_lbl] start_lbl]
    322239  | _ ⇒
    323240    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
     
    350267      let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in
    351268      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
    352         adds_graph … (saves @ restores) start_lbl]].
     269        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
    353270[@second_crl_proof | @first_crl_proof]
    354271qed.
     
    362279  λdef.
    363280  let nb_args ≝ |args| in
    364     add_translates globals (
     281    add_translates ertl_params1 globals (
    365282      set_params … args @ [
    366       adds_graph … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];
     283      adds_graph ertl_params1 … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];
    367284      fetch_result … ret_regs
    368285      ]
     
    388305         let 〈r1,r2〉 ≝ rs in
    389306         let rs ≝ 〈pseudo r1, pseudo r2〉 in
    390           add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_move … rs) lbl') def
     307          add_graph ertl_params1 ? lbl (joint_st_sequential … (joint_instr_move … rs) lbl') def
    391308      | joint_instr_extension ext ⇒
    392309         match ext with
    393310          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
    394311          | rtlntc_st_ext_address r1 r2 ⇒
    395              adds_graph … [
     312             adds_graph ertl_params1 … [
    396313              joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
    397314              joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
     
    400317        the problem is call_id that takes different parameters, but that is pattern-matched
    401318        above. It could be made nicer at the cost of making all the rest of the code uglier *)
    402       | joint_instr_cost_label cost_lbl ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cost_label … cost_lbl) lbl') def
    403       | joint_instr_address x prf r1 r2 ⇒ add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_address … x prf r1 r2) lbl') def
    404       | joint_instr_int r i ⇒  add_graph … lbl (joint_st_sequential ertl_params_ globals (joint_instr_int … r i) lbl') def
     319      | joint_instr_cost_label cost_lbl ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cost_label … cost_lbl) lbl') def
     320      | joint_instr_address x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_address … x prf r1 r2) lbl') def
     321      | joint_instr_int r i ⇒  add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_int … r i) lbl') def
    405322      | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒
    406           add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
     323          add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
    407324      | joint_instr_op1 op1 destr srcr ⇒
    408         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op1 … op1 destr srcr) lbl') def
     325        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op1 … op1 destr srcr) lbl') def
    409326      | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
    410         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
     327        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
    411328      | joint_instr_clear_carry ⇒
    412         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_clear_carry …) lbl') def
     329        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_clear_carry …) lbl') def
    413330      | joint_instr_set_carry ⇒
    414         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_set_carry …) lbl') def
     331        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_set_carry …) lbl') def
    415332      | joint_instr_load destr addr1 addr2 ⇒
    416         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_load … destr addr1 addr2) lbl') def
     333        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_load … destr addr1 addr2) lbl') def
    417334      | joint_instr_store addr1 addr2 srcr ⇒
    418         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_store … addr1 addr2 srcr) lbl') def
     335        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) lbl') def
    419336      | joint_instr_cond srcr lbl_true ⇒
    420         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_cond … srcr lbl_true) lbl') def
     337        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cond … srcr lbl_true) lbl') def
    421338      | joint_instr_comment msg ⇒
    422         add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_comment … msg) lbl') def
     339        add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_comment … msg) lbl') def
    423340      ]].
    424   cases not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
     341  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
    425342qed.
    426343
     
    452369  λglobals.
    453370  λstmt.
    454   λdef.
     371  λdef: joint_internal_function … (ertl_params globals).
    455372  let 〈entry, nuniv〉 ≝ fresh_label … def in
    456373  let graph ≝ add ? ? (joint_if_code … def) entry stmt in
     
    476393         match inst with
    477394          [ joint_instr_cost_label cost_lbl ⇒
    478              〈Some … cost_lbl, add_graph ertl_params_ globals lbl (joint_st_goto … lbl) def〉
     395             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (joint_st_goto … lbl) def〉
    479396          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    480397      | joint_st_return ⇒ 〈None …, def〉
  • src/RTLabs/RTLAbstoRTL.ma

    r1239 r1280  
    44include "common/FrontEndOps.ma".
    55include "common/Graphs.ma".
    6 
    7 definition add_graph ≝
    8   λl: label.
    9   λstmt.
    10   λp.
    11   let rtl_if_luniverse' ≝ rtl_if_luniverse p in
    12   let rtl_if_runiverse' ≝ rtl_if_runiverse p in
    13   let rtl_if_result' ≝ rtl_if_result p in
    14   let rtl_if_params' ≝ rtl_if_params p in
    15   let rtl_if_locals' ≝ rtl_if_locals p in
    16   let rtl_if_stacksize' ≝ rtl_if_stacksize p in
    17   let rtl_if_graph' ≝ add ? ? (rtl_if_graph p) l stmt in
    18   let rtl_if_entry' ≝ rtl_if_entry p in
    19   let rtl_if_exit' ≝ rtl_if_exit p in
    20     mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse'
    21                              rtl_if_params' rtl_if_params' rtl_if_locals'
    22                              rtl_if_stacksize' rtl_if_graph' ? ?.
    23   [1: cases(rtl_if_entry')
    24       #LABEL #HYP %
    25       [1: @LABEL
    26       |2: cases(HYP)
    27           generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
    28           normalize nodelta;
    29           /2/
    30       ]
    31   |2: cases(rtl_if_exit')
    32       #LABEL #HYP %
    33       [1: @LABEL
    34       |2: cases(HYP)
    35           generalize in match (graph_add_lookup ? (rtl_if_graph p) LABEL stmt l);
    36           normalize nodelta;
    37           /2/
    38       ]
    39   ]
    40 qed.
    41      
    42 definition fresh_label: rtl_internal_function → rtl_internal_function × label ≝
    43   λdef.
    44     let 〈lbl, new_univ〉 ≝ fresh LabelTag (rtl_if_luniverse def) in
    45     let locals ≝ rtl_if_locals def in
    46     let rtl_if_luniverse' ≝ new_univ in
    47     let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    48     let rtl_if_result' ≝ rtl_if_result def in
    49     let rtl_if_params' ≝ rtl_if_params def in
    50     let rtl_if_locals' ≝ rtl_if_locals def in
    51     let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    52     let rtl_if_graph' ≝ rtl_if_graph def in
    53     let rtl_if_entry' ≝ rtl_if_entry def in
    54     let rtl_if_exit' ≝ rtl_if_exit def in
    55       〈mk_rtl_internal_function
    56         rtl_if_luniverse' rtl_if_runiverse' rtl_if_result'
    57         rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
    58         rtl_if_entry' rtl_if_exit', lbl〉.
    59 
    60 axiom register_fresh: universe RegisterTag → register.
    61 
    62 definition fresh_reg: rtl_internal_function → rtl_internal_function × register ≝
    63   λdef.
    64     let r ≝ register_fresh (rtl_if_runiverse def) in
    65     let locals ≝ r :: rtl_if_locals def in
    66     let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    67     let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    68     let rtl_if_result' ≝ rtl_if_result def in
    69     let rtl_if_params' ≝ rtl_if_params def in
    70     let rtl_if_locals' ≝ locals in
    71     let rtl_if_stacksize' ≝ rtl_if_stacksize def in
    72     let rtl_if_graph' ≝ rtl_if_graph def in
    73     let rtl_if_entry' ≝ rtl_if_entry def in
    74     let rtl_if_exit' ≝ rtl_if_exit def in
    75       〈mk_rtl_internal_function
    76         rtl_if_luniverse' rtl_if_runiverse' rtl_if_result'
    77         rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
    78         rtl_if_entry' rtl_if_exit', r〉.
    79        
    80 let rec fresh_regs (def: rtl_internal_function) (n: nat) on n ≝
    81   match n with
    82   [ O   ⇒ 〈def, [ ]〉
    83   | S n ⇒
    84     let 〈def, res〉 ≝ fresh_regs def n in
    85     let 〈def, r〉 ≝ fresh_reg def in
    86       〈def, r :: res〉
    87   ].
    88 
    89 axiom fresh_regs_length:
    90   ∀def: rtl_internal_function.
    91   ∀n: nat.
    92     |(\snd (fresh_regs def n))| = n.
    93    
    94 definition addr_regs ≝
    95   λregs.
    96   match regs with
    97   [ cons hd tl ⇒
    98     match tl with
    99     [ cons hd' tl' ⇒ Some (register × register) 〈hd, hd'〉
    100     | nil          ⇒ None (register × register)
    101     ]
    102   | nil ⇒ None (register × register) (* registers are not an address *)
    103   ].
    104 
     6include "joint/TranslateUtils.ma".
     7
     8(*
    1059let rec register_freshes (runiverse: universe RegisterTag) (n: nat) on n ≝
    10610  match n with
     
    10812  | S n' ⇒ register_fresh runiverse :: (register_freshes runiverse n')
    10913  ].
     14*)
    11015
    11116definition choose_rest ≝
     
    12934
    13035definition complete_regs ≝
     36  λglobals.
    13137  λdef.
    13238  λsrcrs1.
    13339  λsrcrs2.
    134   let nb_added ≝ abs ((length ? srcrs1) - (length ? srcrs2)) in
    135   let 〈def, added_regs〉 ≝ fresh_regs def nb_added in
    136     if gtb nb_added 0 then
    137       〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
    138     else
    139       〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
    140 
    141 (* obvious, but proof doesn't look easy! *)
    142 axiom complete_regs_length:
    143   ∀def.
    144   ∀left.
    145   ∀right.
    146     |\fst (\fst (complete_regs def left right))| = |\snd (\fst (complete_regs def left right))|.
     40  if leb (length … srcrs2) (length … srcrs1) then
     41   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs1) (length ? srcrs2)) in
     42    〈〈srcrs1, srcrs2 @ added_regs〉, added_regs〉
     43  else
     44   let 〈def, added_regs〉 ≝ fresh_regs rtl_params0 globals def (minus (length ? srcrs2) (length ? srcrs1)) in
     45    〈〈srcrs1 @ added_regs, srcrs2〉, added_regs〉.
     46
     47lemma complete_regs_length:
     48  ∀globals,def,left,right.
     49   |\fst (\fst (complete_regs globals def left right))| = |\snd (\fst (complete_regs globals def left right))|.
     50 #globals #def #left #right
     51 whd in match complete_regs normalize nodelta
     52 @leb_elim normalize nodelta #H
     53 [ generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … left) (length … right)))
     54 | generalize in match (fresh_regs_length rtl_params0 globals def (minus (length … right) (length … left)))]
     55 cases (fresh_regs ????) #def' #fresh normalize >append_length
     56 generalize in match H -H;
     57 generalize in match (length … left) generalize in match (length … right) generalize in match (length … fresh)
     58 [ /2/ | #x #y #z #H generalize in match (not_le_to_lt … H) -H #H #E >E >commutative_plus
     59         <plus_minus_m_m /2/ ]
     60qed.
    14761
    14862definition size_of_sig_type ≝
     
    16276  | register_ptr: register → register → register_type.
    16377
    164 definition local_env ≝ BitVectorTrie (list register).
    165 
    166 definition mem_local_env ≝
    167   λr: register.
    168   match r with
    169   [ an_identifier w ⇒ member (list register) 16 w
    170   ].
    171 
    172 definition add_local_env ≝
    173   λr: register.
    174   match r with
    175   [ an_identifier w ⇒ insert (list register) 16 w
    176   ].
    177 
    178 definition find_local_env ≝
    179   λr: register.
    180   λbvt.
    181   match r with
    182   [ an_identifier w ⇒ lookup (list register) 16 w bvt [ ]
    183   ].
    184 
     78definition local_env ≝ BitVectorTrie (list register) 16.
     79
     80definition mem_local_env : register → local_env → bool ≝
     81  λr. member … (word_of_identifier … r).
     82
     83definition add_local_env : register → list register → local_env → local_env ≝
     84  λr. insert … (word_of_identifier … r).
     85
     86definition find_local_env : register → local_env → list register ≝
     87  λr: register.λbvt. lookup … (word_of_identifier … r) bvt [].
     88
     89(*
    18590definition initialize_local_env_internal ≝
    18691  λruniverse.
     
    203108  in
    204109    foldl ? ? (initialize_local_env_internal runiverse) (Stub …) registers.
    205  
     110*)
     111
    206112definition map_list_local_env_internal ≝
    207   λlenv.
    208   λres.
    209   λr.
    210     res @ (find_local_env r lenv).
     113  λlenv,res,r. res @ (find_local_env r lenv).
    211114   
    212115definition map_list_local_env ≝
    213   λlenv.
    214   λregs.
    215     foldl ? ? (map_list_local_env_internal lenv) [ ] regs.
     116  λlenv,regs. foldl … (map_list_local_env_internal lenv) [ ] regs.
    216117
    217118definition make_addr ≝
     
    235136  |3: normalize in tl_nil_prf;
    236137      cases(not_le_Sn_O 0)
    237       #HYP cases(HYP tl_nil_prf)
    238   ]
     138      #HYP cases(HYP tl_nil_prf)]
    239139qed.
    240140
    241141definition find_and_addr ≝
    242   λr.
    243   λlenv.
    244     make_addr ? (find_local_env r lenv).
     142  λr,lenv. make_addr ? (find_local_env r lenv).
    245143
    246144definition rtl_args ≝
    247   λregs_list.
    248   λlenv.
    249     flatten ? (map ? ? (
    250       λr. find_local_env r lenv) regs_list).
    251 
    252 definition change_label ≝
    253   λlbl.
    254   λstmt: rtl_statement.
    255   match stmt with
    256   [ rtl_st_skip _ ⇒ rtl_st_skip lbl
    257   | rtl_st_cost cost_lbl _ ⇒ rtl_st_cost cost_lbl lbl
    258   | rtl_st_addr r1 r2 id _ ⇒ rtl_st_addr r1 r2 id lbl
    259   | rtl_st_stack_addr r1 r2 _ ⇒ rtl_st_stack_addr r1 r2 lbl
    260   | rtl_st_int r i _ ⇒ rtl_st_int r i lbl
    261   | rtl_st_move r1 r2 _ ⇒ rtl_st_move r1 r2 lbl
    262   | rtl_st_opaccs opaccs d s1 s2 s3 _ ⇒ rtl_st_opaccs opaccs d s1 s2 s3 lbl
    263   | rtl_st_op1 op1 d s _ ⇒ rtl_st_op1 op1 d s lbl
    264   | rtl_st_op2 op2 d s1 s2 _ ⇒ rtl_st_op2 op2 d s1 s2 lbl
    265   | rtl_st_load d a1 a2 _ ⇒ rtl_st_load d a1 a2 lbl
    266   | rtl_st_store a1 a2 s _ ⇒ rtl_st_store a1 a2 s lbl
    267   | rtl_st_call_id f a r _ ⇒ rtl_st_call_id f a r lbl
    268   | rtl_st_call_ptr f1 f2 a r _ ⇒ rtl_st_call_ptr f1 f2 a r lbl
    269   | rtl_st_tailcall_id f a ⇒ rtl_st_tailcall_id f a
    270   | rtl_st_tailcall_ptr f1 f2 a ⇒ rtl_st_tailcall_ptr f1 f2 a
    271   | rtl_st_cond r l1 l2 ⇒ rtl_st_cond r l1 l2
    272   | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
    273   | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
    274   | rtl_st_return ⇒ rtl_st_return
    275   ].
    276 
    277 (* Ack! Should generating a fresh label ever fail?  This seems to be a side-effect
    278    of implementing everything as a bitvector, which is bounded.  If we implemented
    279    labels as unbounded nats then this function will never fail.
    280 *)
    281 (* Fixed with changes to label generation.
    282 *)
    283 let rec adds_graph (stmt_list: ?) (start_lbl: label) (dest_lbl: label) (def: rtl_internal_function) ≝
    284   match stmt_list with
    285   [ nil ⇒ def
    286   | cons hd tl ⇒
    287     match tl with
    288     [ nil ⇒ add_graph start_lbl (change_label dest_lbl hd) def
    289     | cons hd' tl' ⇒
    290       let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
    291       let stmt ≝ change_label tmp_lbl hd in
    292       let def ≝ add_graph start_lbl stmt new_def in
    293         adds_graph tl tmp_lbl dest_lbl new_def
    294     ]
    295   ].
    296 
    297 let rec add_translates (translate_list: ?) (start_lbl: label) (dest_lbl: label)
    298                        (def: ?) on translate_list ≝
    299   match translate_list with
    300   [ nil ⇒ def
    301   | cons hd tl ⇒
    302     match tl with
    303     [ nil ⇒ hd start_lbl dest_lbl def
    304     | cons hd' tl' ⇒
    305       let 〈new_def, tmp_lbl〉 ≝ fresh_label def in
    306       let applied ≝ hd start_lbl tmp_lbl new_def in
    307         add_translates tl tmp_lbl dest_lbl applied
    308     ]
    309   ].
     145  λregs_list,lenv. flatten … (map … (λr. find_local_env r lenv) regs_list).
    310146
    311147definition translate_cst_int_internal ≝
    312   λdest_lbl.
    313   λr.
    314   λi.
    315     rtl_st_int r i dest_lbl.
    316 
     148  λglobals,dest_lbl,r,i. joint_st_sequential rtl_params_ globals (joint_instr_int … r i) dest_lbl.
     149
     150(*CSC: XXXXX *)
    317151axiom translate_cst:
     152  ∀globals.
    318153  ∀cst: constant.
    319154  ∀destrs: list register.
    320155  ∀start_lbl: label.
    321156  ∀dest_lbl: label.
    322   ∀def: rtl_internal_function.
    323     rtl_internal_function.
     157  ∀def: rtl_internal_function globals.
     158    rtl_internal_function globals.
    324159
    325160definition translate_move_internal ≝
     161  λglobals.
    326162  λstart_lbl: label.
    327163  λdestr: register.
    328164  λsrcr: register.
    329     rtl_st_move destr srcr start_lbl.
     165    joint_st_sequential rtl_params_ globals (joint_instr_move … 〈destr,srcr〉) start_lbl.
    330166
    331167definition translate_move ≝
     168  λglobals.
    332169  λdestrs: list register.
    333170  λsrcrs: list register.
     
    339176      let restl ≝ \snd (\fst crl_crr) in
    340177      let restr ≝ \snd (\snd crl_crr) in
    341       let f_common ≝ translate_move_internal start_lbl in
    342       let translate1 ≝ adds_graph (map2 … f_common commonl commonr ?) in
    343       let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
    344         add_translates [ translate1 ; translate2 ] start_lbl
     178      let f_common ≝ translate_move_internal globals start_lbl in
     179      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
     180      let translate2 ≝ translate_cst (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
     181        add_translates [ translate1 ; translate2 ] start_lbl
    345182    ].
    346183    @len_proof
     
    368205
    369206definition translate_cast_unsigned ≝
     207  λglobals.
    370208  λdestrs.
    371209  λstart_lbl.
    372210  λdest_lbl.
    373   λdef.
    374   let 〈def, tmp_zero〉 ≝ fresh_reg def in
    375   let zeros ≝ make ? tmp_zero (length ? destrs) in
    376     add_translates [
    377       adds_graph [
    378         rtl_st_int tmp_zero (bitvector_of_nat ? 0) start_lbl
     211  λdef: joint_internal_function … (rtl_params globals).
     212  let 〈def, tmp_zero〉 ≝ fresh_reg def in
     213  let zeros ≝ make … tmp_zero (length … destrs) in
     214    add_translates [
     215      adds_graph rtl_params1 … [
     216        joint_st_sequential rtl_params_ … (joint_instr_int rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
    379217        ];
    380       translate_move destrs zeros
     218      translate_move globals destrs zeros
    381219    ] start_lbl dest_lbl def.
    382220
    383221definition translate_cast_signed ≝
     222  λglobals.
    384223  λdestrs.
    385224  λsrcr.
     
    387226  λdest_lbl.
    388227  λdef.
    389   let 〈def, tmp_128〉 ≝ fresh_reg def in
    390   let 〈def, tmp_255〉 ≝ fresh_reg def in
    391   let 〈def, tmpr〉 ≝ fresh_reg def in
    392   let 〈def, dummy〉 ≝ fresh_reg def in
     228  let 〈def, tmp_128〉 ≝ fresh_reg def in
     229  let 〈def, tmp_255〉 ≝ fresh_reg def in
     230  let 〈def, tmpr〉 ≝ fresh_reg def in
     231  let 〈def, dummy〉 ≝ fresh_reg def in
    393232  let insts ≝ [
    394233    rtl_st_int tmp_128 (bitvector_of_nat ? 128) start_lbl;
     
    398237    rtl_st_opaccs Mul tmpr dummy tmpr tmp_255 start_lbl
    399238  ] in
    400   let srcrs ≝ make ? tmpr (length ? destrs) in
    401     add_translates [
    402       adds_graph insts;
     239  let srcrs ≝ make … tmpr (length … destrs) in
     240    add_translates [
     241      adds_graph insts;
    403242      translate_move destrs srcrs
    404243    ] start_lbl dest_lbl def.
  • src/joint/Joint.ma

    r1275 r1280  
    1717 
    1818 ; extend_statements: Type[0]
    19  
    20  ; resultT: Type[0]
    21  ; localsT: Type[0]
    22  ; paramsT: Type[0]
    2319 }.
    2420
     
    2723 ; succ: Type[0]
    2824 }.
     25
     26(* One common instantiation of params via Graphs of joint_statements
     27   (all languages but LIN) *)
     28definition graph_params_ : params__ → params_ ≝
     29 λpars__. mk_params_ pars__ label.
    2930
    3031inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝
     
    5253  | joint_st_return: joint_statement p globals.
    5354
     55record params0: Type[1] ≝
     56 { pars__' :> params__
     57 ; resultT: Type[0]
     58 ; paramsT: Type[0]
     59 }.
     60
     61record params1 : Type[1] ≝
     62 { pars0 :> params0
     63 ; localsT: Type[0]
     64 }.
    5465
    5566record params (globals: list ident): Type[1] ≝
    56  { pars_:> params_
     67 { succ_ : Type[0]
     68 ; pars1 :> params1
    5769 ; codeT: Type[0]
    58  ; lookup: codeT → label → option (joint_statement pars_ globals)
     70 ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals)
    5971 }.
     72 
     73definition params__of_params: ∀globals. params globals → params_ ≝
     74 λglobals,pars. mk_params_ pars (succ_ … pars).
     75coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params
     76 on _p: params ? to params_.
    6077
    6178include alias "common/Graphs.ma". (* To pick the right lookup *)
    6279
    63 (* One common instantiation of params via Graphs of joint_statements *)
    64 definition graph_params: params_ → ∀globals: list ident. params globals ≝
    65  λparams_,globals. mk_params globals params_ (graph (joint_statement params_ globals)) (lookup …).
     80(* One common instantiation of params via Graphs of joint_statements
     81   (all languages but LIN) *)
     82definition graph_params: params1 → ∀globals: list ident. params globals ≝
     83 λpars1,globals.
     84  mk_params globals label pars1
     85   (graph (joint_statement (graph_params_ pars1) globals)) (lookup …).
     86
     87
     88(* CSC: special case where localsT is a list of register (RTL and ERTL) *)
     89definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register).
     90definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0).
    6691
    6792record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝
     
    123148(* Specialized for graph_params *)
    124149definition add_graph ≝
    125   λpars_,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars_ globals).
     150  λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals).
    126151   let code ≝ add … (joint_if_code ?? p) l stmt in
    127     mk_joint_internal_function … (graph_params pars_ globals)
     152    mk_joint_internal_function … (graph_params globals)
    128153     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
    129154     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
Note: See TracChangeset for help on using the changeset viewer.