Changeset 1292


Ignore:
Timestamp:
Oct 5, 2011, 11:15:00 AM (8 years ago)
Author:
mulligan
Message:

more added to rtlabs translation

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1290 r1292  
    945945
    946946definition translate_load ≝
     947  λglobals: list ident.
    947948  λaddr.
    948949  λaddr_prf: 2 ≤ |addr|.
     
    950951  λstart_lbl: label.
    951952  λdest_lbl: label.
    952   λdef: rtl_internal_function.
    953   match fresh_regs_strong def (|addr|) with
     953  λdef: rtl_internal_function globals.
     954  match fresh_regs_strong rtl_params0 globals def (|addr|) with
    954955  [ dp def_save_addr save_addr_prf ⇒
    955956    let def ≝ \fst def_save_addr in
    956957    let save_addr ≝ \snd def_save_addr in
    957     match fresh_regs_strong def (|addr|) with
     958    match fresh_regs_strong rtl_params0 globals def (|addr|) with
    958959    [ dp def_tmp_addr tmp_addr_prf ⇒
    959960      let def ≝ \fst def_tmp_addr in
    960961      let tmp_addr ≝ \snd def_tmp_addr in
    961       let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
    962       let 〈def, tmpr〉 ≝ fresh_reg def in
    963       let insts_save_addr ≝ translate_move save_addr addr in
     962      let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr tmp_addr ? in
     963      let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
     964      let insts_save_addr ≝ translate_move globals save_addr addr in
    964965      let f ≝ λtranslates_off. λr.
    965966        let 〈translates, off〉 ≝ translates_off in
    966967        let translates ≝ translates @ [
    967           adds_graph [
    968             INT tmpr off start_lbl
     968          adds_graph rtl_params1 globals [
     969            sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    969970          ];
    970           translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;
    971           adds_graph [
    972             LOAD r tmp_addr1 tmp_addr2 dest_lbl
     971          translate_op2 globals Oaddp tmp_addr ? save_addr [tmpr] ? ?;
     972          adds_graph rtl_params1 globals [
     973            sequential rtl_params_ globals (LOAD rtl_params_ globals r tmp_addr1 tmp_addr2)
    973974          ]
    974975        ]
    975976        in
    976         let 〈carry, result〉 ≝ half_add ? off int_size in
     977        let 〈carry, result〉 ≝ half_add off int_size in
    977978          〈translates, result〉
    978979      in
    979       let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], (zero ?)〉 destrs in
    980         add_translates (insts_save_addr :: translates) start_lbl dest_lbl def
     980      let 〈translates, ignore〉 ≝ foldl f 〈[ ], (zero ?)〉 destrs in
     981        add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def
    981982    ]
    982983  ].
     
    991992
    992993definition translate_store ≝
     994  λglobals: list ident.
    993995  λaddr.
    994996  λaddr_prf: 2 ≤ |addr|.
     
    996998  λstart_lbl: label.
    997999  λdest_lbl: label.
    998   λdef: rtl_internal_function.
    999   match fresh_regs_strong def (|addr|) with
     1000  λdef: rtl_internal_function globals.
     1001  match fresh_regs_strong rtl_params0 globals def (|addr|) with
    10001002  [ dp def_tmp_addr tmp_addr_prf ⇒
    10011003    let def ≝ \fst def_tmp_addr in
    10021004    let tmp_addr ≝ \snd def_tmp_addr in
    1003     let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ? tmp_addr ? in
    1004     let 〈def, tmpr〉 ≝ fresh_reg def in
     1005    let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr tmp_addr ? in
     1006    let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in
    10051007    let f ≝ λtranslate_off. λsrcr.
    10061008      let 〈translates, off〉 ≝ translate_off in
    10071009      let translates ≝ translates @ [
    1008         adds_graph [
    1009           rtl_st_int tmpr off start_lbl
     1010        adds_graph rtl_params1 globals [
     1011          sequential rtl_params_ globals (INT rtl_params_ globals tmpr off)
    10101012        ];
    1011         translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?;
    1012         adds_graph [
    1013           rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl
     1013        translate_op2 globals Oaddp tmp_addr ? addr [tmpr] ? ?;
     1014        adds_graph rtl_params1 globals [
     1015          sequential rtl_params_ globals (STORE rtl_params_ globals tmp_addr1 tmp_addr2 srcr)
    10141016        ]
    10151017      ]
    10161018      in
    1017         let 〈carry, result〉 ≝ half_add ? off int_size in
     1019        let 〈carry, result〉 ≝ half_add off int_size in
    10181020          〈translates, result〉
    10191021    in
    1020     let 〈translates, ignore〉 ≝ foldl ? ? f 〈[ ], zero ?〉 srcrs in
    1021       add_translates translates start_lbl dest_lbl def
     1022    let 〈translates, ignore〉 ≝ foldl f 〈[ ], zero ?〉 srcrs in
     1023      add_translates rtl_params1 globals translates start_lbl dest_lbl def
    10221024  ].
    10231025  [1: normalize //
     
    10291031  ]
    10301032qed.
    1031 *)
    10321033
    10331034definition translate_stmt ≝
    1034   λglobals.
     1035  λglobals: list ident.
    10351036  λlenv: local_env.
    10361037  λlbl: label.
    10371038  λstmt.
    1038   λdef: joint_internal_function … (rtl_params globals).
     1039  λdef: rtl_internal_function globals.
    10391040  match stmt with
    10401041  [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def
    1041   | St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def
     1042  | St_cost cost_lbl lbl' ⇒ add_graph lbl (sequential rtl_params_ globals (COST_LABEL … cost_lbl lbl')) def
    10421043  | St_const destr cst lbl' ⇒
    10431044    translate_cst cst (find_local_env destr lenv) lbl lbl' def
    10441045  | St_op1 op1 destr srcr lbl' ⇒
    1045     translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ? lbl lbl' def
     1046    translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) lbl lbl' def
    10461047  | St_op2 op2 destr srcr1 srcr2 lbl' ⇒
    1047     translate_op2 op2 (find_local_env destr lenv) ? (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
     1048    translate_op2 op2 (find_local_env destr lenv) (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
    10481049  | St_load ignore addr destr lbl' ⇒
    1049     translate_load (find_local_env addr lenv) ? (find_local_env destr lenv) lbl lbl' def
     1050    translate_load (find_local_env addr lenv) (find_local_env destr lenv) lbl lbl' def
    10501051  | St_store ignore addr srcr lbl' ⇒
    1051     translate_store (find_local_env addr lenv) ? (find_local_env srcr lenv) lbl lbl' def
     1052    translate_store (find_local_env addr lenv) (find_local_env srcr lenv) lbl lbl' def
    10521053  | St_call_id f args retr lbl' ⇒
    10531054    match retr with
    10541055    [ Some retr ⇒
    1055       add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def
    1056     | None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def
     1056      add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) (find_local_env retr lenv) lbl')) def
     1057    | None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) [ ] lbl')) def
    10571058    ]
    10581059  | St_call_ptr f args retr lbl' ⇒
     
    10601061    [ None ⇒
    10611062      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1062         add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def
     1063        add_graph lbl rtl_params1 globals (sequential … (extension … (rtl_st_ext_call_ptr … f1 f2 (rtl_args args lenv) [ ] lbl'))) def
    10631064    | Some retr ⇒
    10641065      let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1065         add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl') def
     1066        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) (find_local_env retr lenv) lbl'))) def
    10661067    ]
    10671068  | St_tailcall_id f args ⇒
    1068     add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def
     1069    add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) lbl) def
    10691070  | St_tailcall_ptr f args ⇒
    10701071    let 〈f1, f2〉 ≝ find_and_addr f lenv ? in
    1071       add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def
     1072      add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params1 globals (rtl_st_ext_tailcall_ptr f1 f2 (rtl_args args lenv))) lbl) def
    10721073  | St_cond r lbl_true lbl_false ⇒
    1073     translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
     1074    translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
    10741075  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
    1075   | St_return ⇒ add_graph lbl rtl_st_return def
     1076  | St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def
    10761077  ].
    10771078  [10: cases not_implemented (* jtable case *)
     
    10891090  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
    10901091    (f_params def @ f_locals def) (f_result def) in
    1091   let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
    1092   let locals ≝ map_list_local_env lenv (map ? ? \fst (f_locals def)) in
     1092  let params ≝ map_list_local_env lenv (map \fst (f_params def)) in
     1093  let locals ≝ map_list_local_env lenv (map \fst (f_locals def)) in
    10931094  let result ≝
    10941095    match (f_result def) with
Note: See TracChangeset for help on using the changeset viewer.