Changeset 1282 for src/RTL


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

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

Location:
src/RTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLTailcall.ma

    r1275 r1282  
    88  λgraph: codeT … (rtlntc_params globals).
    99  match stmt with
    10   [ joint_st_sequential seq DUMMY ⇒
     10  [ sequential seq DUMMY ⇒
    1111     match seq with
    12       [ joint_instr_extension ext ⇒
     12      [ extension ext ⇒
    1313         match ext with
    1414          [ rtl_st_ext_tailcall_id f args ⇒
    15               add ? ? graph lbl (joint_st_sequential … (joint_instr_call_id … f args [ ]) exit)
     15              add ? ? graph lbl (sequential … (CALL_ID … f args [ ]) exit)
    1616          | rtl_st_ext_tailcall_ptr f1 f2 args ⇒
    17               add ? ? graph lbl (joint_st_sequential … (joint_instr_extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
     17              add ? ? graph lbl (sequential … (extension … (rtlntc_st_ext_call_ptr f1 f2 args [ ])) exit)
    1818          | _ ⇒ graph ]
    1919      | _ ⇒ graph ]
  • src/RTL/RTLtoERTL.ma

    r1280 r1282  
    1010   λdestr_srcr.λstart_lbl.
    1111    let 〈destr, srcr〉 ≝ destr_srcr in
    12      adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
     12     adds_graph ertl_params1 globals [ sequential … (MOVE … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
    1313  in
    1414   map ? ? save_hdws_internal l.
     
    2020    λstart_lbl: label.
    2121     let 〈srcr, destr〉 ≝ srcr_destr in
    22      adds_graph ertl_params1 globals [ joint_st_sequential … (joint_instr_move … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
     22     adds_graph ertl_params1 globals [ sequential … (MOVE … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
    2323   in
    2424    map ? ? restore_hdws_internal l.
     
    2828  λparams: list register.
    2929  match params with
    30   [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ joint_st_goto … start_lbl ] start_lbl]
     30  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … start_lbl ] start_lbl]
    3131  | _ ⇒
    3232    let l ≝ zip_pottier ? ? params RegisterParams in
     
    4444  let 〈carry, int_offset〉 ≝ half_add ? (bitvector_of_nat ? off) int_size in
    4545  adds_graph ertl_params1 globals [
    46     joint_st_sequential … (joint_instr_extension … (ertl_st_ext_frame_size addr1)) start_lbl;
    47     joint_st_sequential … (joint_instr_int … tmpr int_offset) start_lbl;
    48     joint_st_sequential … (joint_instr_op2 … Sub addr1 addr1 tmpr) start_lbl;
    49     joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
    50     joint_st_sequential … (joint_instr_op2 … Add addr1 addr1 tmpr) start_lbl;
    51     joint_st_sequential … (joint_instr_int … addr2 (bitvector_of_nat 8 0)) start_lbl;
    52     joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
    53     joint_st_sequential … (joint_instr_op2 … Addc addr2 addr2 tmpr) start_lbl;
    54     joint_st_sequential … (joint_instr_load … destr addr1 addr2) start_lbl
     46    sequential … (extension … (ertl_st_ext_frame_size addr1)) start_lbl;
     47    sequential … (INT … tmpr int_offset) start_lbl;
     48    sequential … (OP2 … Sub addr1 addr1 tmpr) start_lbl;
     49    sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
     50    sequential … (OP2 … Add addr1 addr1 tmpr) start_lbl;
     51    sequential … (INT … addr2 (bitvector_of_nat 8 0)) start_lbl;
     52    sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
     53    sequential … (OP2 … Addc addr2 addr2 tmpr) start_lbl;
     54    sequential … (LOAD … destr addr1 addr2) start_lbl
    5555  ] start_lbl dest_lbl def.
    5656 
     
    5858  λglobals,params.
    5959  match params with
    60   [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl ]
     60  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl ]
    6161  | _ ⇒ mapi ? ? (get_param_stack globals) params ].
    6262
     
    8484      add_translates …
    8585         ((adds_graph ertl_params1 … [
    86                      joint_st_sequential ertl_params_ … (joint_instr_extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl
     86                     sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl
    8787                   ]) ::
    8888         (adds_graph … [
    89                       joint_st_sequential … (joint_instr_pop … sral) start_lbl;
    90                       joint_st_sequential … (joint_instr_pop … srah) start_lbl
     89                      sequential … (POP … sral) start_lbl;
     90                      sequential … (POP … srah) start_lbl
    9191                   ]) ::
    9292         (save_hdws … sregs) @
     
    113113    let restl ≝ \snd (\fst crl) in
    114114    let restr ≝ \snd (\snd crl) in
    115     let init_tmpr ≝ joint_st_sequential ertl_params_ … (joint_instr_int … tmpr (zero …)) start_lbl in
    116     let f_save ≝ λst. λr. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo r〉) start_lbl in
     115    let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) start_lbl in
     116    let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) start_lbl in
    117117    let saves ≝ map2 … f_save commonl commonr crl_proof in
    118     let f_default ≝ λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈hardware st, pseudo tmpr〉) start_lbl in
     118    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) start_lbl in
    119119    let defaults ≝ map … f_default restl in
    120120      adds_graph ertl_params1 … (init_tmpr :: saves @ defaults) start_lbl dest_lbl def
     
    127127    let commonl ≝ \fst (\fst crl) in
    128128    let commonr ≝ \fst (\snd crl) in
    129     let f ≝ λret. λst. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware ret, hardware st〉) start_lbl in
     129    let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) start_lbl in
    130130    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    131131      adds_graph ertl_params1 … insts start_lbl
     
    150150        restore_hdws … sregs @
    151151        [adds_graph … [
    152           joint_st_sequential … (joint_instr_push … srah) start_lbl;
    153           joint_st_sequential … (joint_instr_push … sral) start_lbl
     152          sequential … (PUSH … srah) start_lbl;
     153          sequential … (PUSH … sral) start_lbl
    154154        ]] @
    155155        [adds_graph ertl_params1 … [
    156           joint_st_sequential … (joint_instr_extension … ertl_st_ext_del_frame) start_lbl
     156          sequential … (extension … ertl_st_ext_del_frame) start_lbl
    157157        ]] @
    158158        [assign_result globals]
     
    205205  λglobals,params.
    206206  match params with
    207   [ nil ⇒ [ λstart_lbl. adds_graph … [joint_st_goto … start_lbl] start_lbl]
     207  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl]
    208208  | _ ⇒
    209209    let l ≝ zip_pottier ? ? params RegisterParams in
     
    223223  let 〈ignore, int_off〉 ≝ half_add ? off int_size in
    224224    adds_graph ertl_params1 … [
    225       joint_st_sequential … (joint_instr_int … addr1 int_off) start_lbl;
    226       joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
    227       joint_st_sequential … (joint_instr_clear_carry …) start_lbl;
    228       joint_st_sequential … (joint_instr_op2 … Sub addr1 tmpr addr1) start_lbl;
    229       joint_st_sequential … (joint_instr_move … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
    230       joint_st_sequential … (joint_instr_int … addr2 (zero ?)) start_lbl;
    231       joint_st_sequential … (joint_instr_op2 … Sub addr2 tmpr addr2) start_lbl;
    232       joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) start_lbl
     225      sequential … (INT … addr1 int_off) start_lbl;
     226      sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉) start_lbl;
     227      sequential … (CLEAR_CARRY …) start_lbl;
     228      sequential … (OP2 … Sub addr1 tmpr addr1) start_lbl;
     229      sequential … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉) start_lbl;
     230      sequential … (INT … addr2 (zero ?)) start_lbl;
     231      sequential … (OP2 … Sub addr2 tmpr addr2) start_lbl;
     232      sequential … (STORE … addr1 addr2 srcr) start_lbl
    233233    ] start_lbl dest_lbl def.   
    234234
     
    236236  λglobals,params.
    237237  match params with
    238   [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [joint_st_goto … start_lbl] start_lbl]
     238  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO … start_lbl] start_lbl]
    239239  | _ ⇒
    240240    let f ≝ λi. λr. set_param_stack … (bitvector_of_nat ? i) r in
     
    259259    let commonl ≝ \fst (\fst crl) in
    260260    let commonr ≝ \fst (\snd crl) in
    261     let f_save ≝ λst. λret. joint_st_sequential ertl_params_ globals (joint_instr_move … 〈hardware st, hardware ret〉) start_lbl in
     261    let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) start_lbl in
    262262    let saves ≝ map2 ? ? ? f_save commonl commonr ? in
    263263    match reduce_strong ? ? ret_regs RegisterSTS with
     
    265265      let commonl ≝ \fst (\fst crl) in
    266266      let commonr ≝ \fst (\snd crl) in
    267       let f_restore ≝ λr. λst. joint_st_sequential ertl_params_ … (joint_instr_move … 〈pseudo r, hardware st〉) start_lbl in
     267      let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) start_lbl in
    268268      let restores ≝ map2 ? ? ? f_restore commonl commonr ? in
    269269        adds_graph ertl_params1 … (saves @ restores) start_lbl]].
     
    281281    add_translates ertl_params1 globals (
    282282      set_params … args @ [
    283       adds_graph ertl_params1 … [ joint_st_sequential … (joint_instr_call_id … f nb_args it) start_lbl ];
     283      adds_graph ertl_params1 … [ sequential … (CALL_ID … f nb_args it) start_lbl ];
    284284      fetch_result … ret_regs
    285285      ]
     
    294294  λdef.
    295295  match stmt with
    296   [ joint_st_goto lbl' ⇒ add_graph … lbl (joint_st_goto … lbl') def
    297   | joint_st_return ⇒ add_graph … lbl (joint_st_return …) def
    298   | joint_st_sequential seq lbl' ⇒
     296  [ GOTO lbl' ⇒ add_graph … lbl (GOTO … lbl') def
     297  | RETURN ⇒ add_graph … lbl (RETURN …) def
     298  | sequential seq lbl' ⇒
    299299     match seq with
    300       [ joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    301       | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    302       | joint_instr_call_id f args ret_regs ⇒
     300      [ PUSH _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     301      | POP _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     302      | CALL_ID f args ret_regs ⇒
    303303         translate_call_id … f args ret_regs lbl lbl' def
    304       | joint_instr_move rs ⇒
     304      | MOVE rs ⇒
    305305         let 〈r1,r2〉 ≝ rs in
    306306         let rs ≝ 〈pseudo r1, pseudo r2〉 in
    307           add_graph ertl_params1 ? lbl (joint_st_sequential … (joint_instr_move … rs) lbl') def
    308       | joint_instr_extension ext ⇒
     307          add_graph ertl_params1 ? lbl (sequential … (MOVE … rs) lbl') def
     308      | extension ext ⇒
    309309         match ext with
    310310          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
    311311          | rtlntc_st_ext_address r1 r2 ⇒
    312312             adds_graph ertl_params1 … [
    313               joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
    314               joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
     313              sequential … (MOVE … 〈pseudo r1, hardware RegisterSPL〉) lbl;
     314              sequential … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) lbl
    315315             ] lbl lbl' def]
    316316      (*CSC: everything is just copied to re-type it from now on;
    317317        the problem is call_id that takes different parameters, but that is pattern-matched
    318318        above. It could be made nicer at the cost of making all the rest of the code uglier *)
    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
    322       | joint_instr_opaccs op destr1 destr2 srcr1 srcr2 ⇒
    323           add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_opaccs … op destr1 destr2 srcr1 srcr2) lbl') def
    324       | joint_instr_op1 op1 destr srcr ⇒
    325         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op1 … op1 destr srcr) lbl') def
    326       | joint_instr_op2 op2 destr srcr1 srcr2 ⇒
    327         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_op2 … op2 destr srcr1 srcr2) lbl') def
    328       | joint_instr_clear_carry
    329         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_clear_carry …) lbl') def
    330       | joint_instr_set_carry
    331         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_set_carry …) lbl') def
    332       | joint_instr_load destr addr1 addr2 ⇒
    333         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_load … destr addr1 addr2) lbl') def
    334       | joint_instr_store addr1 addr2 srcr ⇒
    335         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_store … addr1 addr2 srcr) lbl') def
    336       | joint_instr_cond srcr lbl_true ⇒
    337         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_cond … srcr lbl_true) lbl') def
    338       | joint_instr_comment msg ⇒
    339         add_graph ertl_params1 … lbl (joint_st_sequential … (joint_instr_comment … msg) lbl') def
     319      | COST_LABEL cost_lbl ⇒ add_graph ertl_params1 … lbl (sequential … (COST_LABEL … cost_lbl) lbl') def
     320      | ADDRESS x prf r1 r2 ⇒ add_graph ertl_params1 … lbl (sequential … (ADDRESS … x prf r1 r2) lbl') def
     321      | INT r i ⇒  add_graph ertl_params1 … lbl (sequential … (INT … r i) lbl') def
     322      | OPACCS op destr1 destr2 srcr1 srcr2 ⇒
     323          add_graph ertl_params1 … lbl (sequential … (OPACCS … op destr1 destr2 srcr1 srcr2) lbl') def
     324      | OP1 op1 destr srcr ⇒
     325        add_graph ertl_params1 … lbl (sequential … (OP1 … op1 destr srcr) lbl') def
     326      | OP2 op2 destr srcr1 srcr2 ⇒
     327        add_graph ertl_params1 … lbl (sequential … (OP2 … op2 destr srcr1 srcr2) lbl') def
     328      | CLEAR_CARRY
     329        add_graph ertl_params1 … lbl (sequential … (CLEAR_CARRY …) lbl') def
     330      | SET_CARRY
     331        add_graph ertl_params1 … lbl (sequential … (SET_CARRY …) lbl') def
     332      | LOAD destr addr1 addr2 ⇒
     333        add_graph ertl_params1 … lbl (sequential … (LOAD … destr addr1 addr2) lbl') def
     334      | STORE addr1 addr2 srcr ⇒
     335        add_graph ertl_params1 … lbl (sequential … (STORE … addr1 addr2 srcr) lbl') def
     336      | COND srcr lbl_true ⇒
     337        add_graph ertl_params1 … lbl (sequential … (COND … srcr lbl_true) lbl') def
     338      | COMMENT msg ⇒
     339        add_graph ertl_params1 … lbl (sequential … (COMMENT … msg) lbl') def
    340340      ]].
    341341  @not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
     
    350350  let entry' ≝ joint_if_entry … def in
    351351  let exit' ≝ joint_if_exit … def in
    352   let graph' ≝ add ? ? (empty_map ? ?) entry' (joint_st_goto … entry') in
    353   let graph' ≝ add ? ? graph' exit' (joint_st_goto … exit') in
     352  let graph' ≝ add ? ? (empty_map ? ?) entry' (GOTO … entry') in
     353  let graph' ≝ add ? ? graph' exit' (GOTO … exit') in
    354354  let def' ≝
    355355    mk_joint_internal_function globals (ertl_params globals)
     
    390390    | Some stmt ⇒
    391391      match stmt with
    392       [ joint_st_sequential inst lbl ⇒
     392      [ sequential inst lbl ⇒
    393393         match inst with
    394           [ joint_instr_cost_label cost_lbl ⇒
    395              〈Some … cost_lbl, add_graph ertl_params1 globals lbl (joint_st_goto … lbl) def〉
     394          [ COST_LABEL cost_lbl ⇒
     395             〈Some … cost_lbl, add_graph ertl_params1 globals lbl (GOTO … lbl) def〉
    396396          | _ ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes' ]
    397       | joint_st_return ⇒ 〈None …, def〉
    398       | joint_st_goto lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
     397      | RETURN ⇒ 〈None …, def〉
     398      | GOTO lbl ⇒ find_and_remove_first_cost_label_internal globals def lbl num_nodes'
    399399      ]]].
    400400   
     
    408408  match cost_label with
    409409  [ None ⇒ def
    410   | Some cost_label ⇒ generate … (joint_st_sequential ertl_params_ globals (joint_instr_cost_label … cost_label) (joint_if_entry … def)) def
     410  | Some cost_label ⇒ generate … (sequential ertl_params_ globals (COST_LABEL … cost_label) (joint_if_entry … def)) def
    411411  ].
    412412
Note: See TracChangeset for help on using the changeset viewer.