Changeset 1283


Ignore:
Timestamp:
Sep 30, 2011, 3:12:40 AM (8 years ago)
Author:
sacerdot
Message:

Bad programming practice removed: change_label is no longer required and
add_graph now takes function from label to statements in place of taking
statements containing a wrong label to be fixed.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTLtoERTL.ma

    r1282 r1283  
    1010   λdestr_srcr.λstart_lbl.
    1111    let 〈destr, srcr〉 ≝ destr_srcr in
    12      adds_graph ertl_params1 globals [ sequential … (MOVE … 〈pseudo destr,hardware srcr〉) start_lbl ] start_lbl
     12     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈pseudo destr,hardware srcr〉) ] 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 [ sequential … (MOVE … 〈hardware destr, pseudo srcr〉) start_lbl ] start_lbl
     22     adds_graph ertl_params1 globals [ sequential ertl_params_ … (MOVE … 〈hardware destr, pseudo srcr〉) ] 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 [ GOTO … start_lbl ] start_lbl]
     30  [ nil ⇒ [λstart_lbl: label. adds_graph ertl_params1 globals [ GOTO … ] 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     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
     46    sequential ertl_params_ … (extension … (ertl_st_ext_frame_size addr1));
     47    sequential ertl_params_ … (INT … tmpr int_offset);
     48    sequential ertl_params_ … (OP2 … Sub addr1 addr1 tmpr);
     49    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
     50    sequential ertl_params_ … (OP2 … Add addr1 addr1 tmpr);
     51    sequential ertl_params_ … (INT … addr2 (bitvector_of_nat 8 0));
     52    sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
     53    sequential ertl_params_ … (OP2 … Addc addr2 addr2 tmpr);
     54    sequential ertl_params_… (LOAD … destr addr1 addr2)
    5555  ] start_lbl dest_lbl def.
    5656 
     
    5858  λglobals,params.
    5959  match params with
    60   [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl ]
     60  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] start_lbl ]
    6161  | _ ⇒ mapi ? ? (get_param_stack globals) params ].
    6262
     
    8484      add_translates …
    8585         ((adds_graph ertl_params1 … [
    86                      sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame) start_lbl
     86                     sequential ertl_params_ … (extension ertl_params__ globals ertl_st_ext_new_frame)
    8787                   ]) ::
    88          (adds_graph … [
    89                       sequential … (POP … sral) start_lbl;
    90                       sequential … (POP … srah) start_lbl
     88         (adds_graph ertl_params1 … [
     89                      sequential ertl_params_ … (POP … sral);
     90                      sequential ertl_params_ … (POP … srah)
    9191                   ]) ::
    9292         (save_hdws … sregs) @
     
    113113    let restl ≝ \snd (\fst crl) in
    114114    let restr ≝ \snd (\snd crl) 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
     115    let init_tmpr ≝ sequential ertl_params_ … (INT … tmpr (zero …)) in
     116    let f_save ≝ λst. λr. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo r〉) in
    117117    let saves ≝ map2 … f_save commonl commonr crl_proof in
    118     let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) start_lbl in
     118    let f_default ≝ λst. sequential ertl_params_ … (MOVE … 〈hardware st, pseudo tmpr〉) 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. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) start_lbl in
     129    let f ≝ λret. λst. sequential ertl_params_ globals (MOVE … 〈hardware ret, hardware st〉) in
    130130    let insts ≝ map2 ? ? ? f commonl commonr crl_proof in
    131131      adds_graph ertl_params1 … insts start_lbl
     
    149149        [save_return globals ret_regs] @
    150150        restore_hdws … sregs @
    151         [adds_graph … [
    152           sequential … (PUSH … srah) start_lbl;
    153           sequential … (PUSH … sral) start_lbl
     151        [adds_graph ertl_params1 … [
     152          sequential ertl_params_ … (PUSH … srah);
     153          sequential ertl_params_ … (PUSH … sral)
    154154        ]] @
    155155        [adds_graph ertl_params1 … [
    156           sequential … (extension … ertl_st_ext_del_frame) start_lbl
     156          sequential ertl_params_ … (extension … ertl_st_ext_del_frame)
    157157        ]] @
    158158        [assign_result globals]
     
    205205  λglobals,params.
    206206  match params with
    207   [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO … start_lbl] start_lbl]
     207  [ nil ⇒ [ λstart_lbl. adds_graph … [GOTO …] 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       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
     225      sequential ertl_params_ … (INT … addr1 int_off);
     226      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPL〉);
     227      sequential ertl_params_ … (CLEAR_CARRY …);
     228      sequential ertl_params_ … (OP2 … Sub addr1 tmpr addr1);
     229      sequential ertl_params_ … (MOVE … 〈pseudo tmpr, hardware RegisterSPH〉);
     230      sequential ertl_params_ … (INT … addr2 (zero ?));
     231      sequential ertl_params_ … (OP2 … Sub addr2 tmpr addr2);
     232      sequential ertl_params_ … (STORE … addr1 addr2 srcr)
    233233    ] start_lbl dest_lbl def.   
    234234
     
    236236  λglobals,params.
    237237  match params with
    238   [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO … start_lbl] start_lbl]
     238  [ nil ⇒ [ λstart_lbl. adds_graph ertl_params1 globals [GOTO …] 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. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) start_lbl in
     261    let f_save ≝ λst. λret. sequential ertl_params_ globals (MOVE … 〈hardware st, hardware ret〉) 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. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) start_lbl in
     267      let f_restore ≝ λr. λst. sequential ertl_params_ … (MOVE … 〈pseudo r, hardware st〉) 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 … [ sequential … (CALL_ID … f nb_args it) start_lbl ];
     283      adds_graph ertl_params1 … [ sequential ertl_params_ … (CALL_ID … f nb_args it) ];
    284284      fetch_result … ret_regs
    285285      ]
     
    311311          | rtlntc_st_ext_address r1 r2 ⇒
    312312             adds_graph ertl_params1 … [
    313               sequential … (MOVE … 〈pseudo r1, hardware RegisterSPL〉) lbl;
    314               sequential … (MOVE … 〈pseudo r2, hardware RegisterSPH〉) lbl
     313              sequential ertl_params_ … (MOVE … 〈pseudo r1, hardware RegisterSPL〉);
     314              sequential ertl_params_ … (MOVE … 〈pseudo r2, hardware RegisterSPH〉)
    315315             ] lbl lbl' def]
    316316      (*CSC: everything is just copied to re-type it from now on;
  • src/RTLabs/RTLAbstoRTL.ma

    r1282 r1283  
    158158definition translate_move_internal ≝
    159159  λglobals.
    160   λstart_lbl: label.
    161160  λdestr: register.
    162161  λsrcr: register.
    163     sequential rtl_params_ globals (MOVE … 〈destr,srcr〉) start_lbl.
     162    sequential rtl_params_ globals (MOVE … 〈destr,srcr〉).
    164163
    165164definition translate_move ≝
     
    174173      let restl ≝ \snd (\fst crl_crr) in
    175174      let restr ≝ \snd (\snd crl_crr) in
    176       let f_common ≝ translate_move_internal globals start_lbl in
     175      let f_common ≝ translate_move_internal globals in
    177176      let translate1 ≝ adds_graph rtl_params1 … (map2 … f_common commonl commonr ?) in
    178177      let translate2 ≝ translate_cst … (Ointconst ? (repr I8 0)) restl in (* should this be 8? *)
     
    212211    add_translates … [
    213212      adds_graph rtl_params1 … [
    214         sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0)) start_lbl
     213        sequential rtl_params_ … (INT rtl_params_ ? tmp_zero (bitvector_of_nat ? 0))
    215214        ];
    216215      translate_move globals destrs zeros
  • src/joint/TranslateUtils.ma

    r1282 r1283  
    3939    fresh LabelTag (joint_if_luniverse … def).
    4040
    41 definition change_label ≝
    42   λpars1,globals.λe: joint_statement (graph_params pars1 globals) globals.λl.
    43   match e with
    44   [ GOTO _ ⇒ GOTO … l
    45   | RETURN ⇒ RETURN ??
    46   | sequential instr _ ⇒ sequential … globals instr l].
    47 
    48 (*CSC: bad programming habit: the code below puts everywhere a fake
    49   label and then adds_graph fixes them *)
    50 (*CSC: this is just an instance of add_translates below! *)
    5141let rec adds_graph
    5242  (pars1: params1) (globals: list ident)
    53   (stmt_list: list (joint_statement (graph_params_ pars1) globals))
     43  (stmt_list: list (label → joint_statement (graph_params_ pars1) globals))
    5444  (start_lbl: label) (dest_lbl: label)
    5545  (def: joint_internal_function … (graph_params pars1 globals))
     
    5949  | cons stmt stmt_list ⇒
    6050    match stmt_list with
    61     [ nil ⇒ add_graph … start_lbl (change_label … stmt dest_lbl) def
     51    [ nil ⇒ add_graph … start_lbl (stmt dest_lbl) def
    6252    | _ ⇒
    6353      let 〈tmp_lbl, nuniv〉 ≝ fresh_label … def in
    64       let stmt ≝ change_label … stmt tmp_lbl in
    65       let def ≝ add_graph … start_lbl stmt def in
     54      let def ≝ add_graph … start_lbl (stmt tmp_lbl) def in
    6655        adds_graph pars1 globals stmt_list tmp_lbl dest_lbl def]].
    6756
    68 (*CSC: bad programming habit: the code below puts everywhere a fake
    69   label and then adds_graph fixes them *)
    7057let rec add_translates
    7158  (pars1: params1) (globals: list ident)
Note: See TracChangeset for help on using the changeset viewer.