 Timestamp:
 Oct 5, 2011, 11:15:00 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1290 r1292 945 945 946 946 definition translate_load ≝ 947 λglobals: list ident. 947 948 λaddr. 948 949 λaddr_prf: 2 ≤ addr. … … 950 951 λstart_lbl: label. 951 952 λdest_lbl: label. 952 λdef: rtl_internal_function .953 match fresh_regs_strong def (addr) with953 λdef: rtl_internal_function globals. 954 match fresh_regs_strong rtl_params0 globals def (addr) with 954 955 [ dp def_save_addr save_addr_prf ⇒ 955 956 let def ≝ \fst def_save_addr in 956 957 let save_addr ≝ \snd def_save_addr in 957 match fresh_regs_strong def (addr) with958 match fresh_regs_strong rtl_params0 globals def (addr) with 958 959 [ dp def_tmp_addr tmp_addr_prf ⇒ 959 960 let def ≝ \fst def_tmp_addr in 960 961 let tmp_addr ≝ \snd def_tmp_addr in 961 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ?tmp_addr ? in962 let 〈def, tmpr〉 ≝ fresh_reg def in963 let insts_save_addr ≝ translate_move save_addr addr in962 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 964 965 let f ≝ λtranslates_off. λr. 965 966 let 〈translates, off〉 ≝ translates_off in 966 967 let translates ≝ translates @ [ 967 adds_graph [968 INT tmpr off start_lbl968 adds_graph rtl_params1 globals [ 969 sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) 969 970 ]; 970 translate_op2 Oaddp tmp_addr ? save_addr [tmpr] ? ?;971 adds_graph [972 LOAD r tmp_addr1 tmp_addr2 dest_lbl971 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) 973 974 ] 974 975 ] 975 976 in 976 let 〈carry, result〉 ≝ half_add ?off int_size in977 let 〈carry, result〉 ≝ half_add … off int_size in 977 978 〈translates, result〉 978 979 in 979 let 〈translates, ignore〉 ≝ foldl ? ?f 〈[ ], (zero ?)〉 destrs in980 add_translates (insts_save_addr :: translates) start_lbl dest_lbl def980 let 〈translates, ignore〉 ≝ foldl … f 〈[ ], (zero ?)〉 destrs in 981 add_translates rtl_params1 globals (insts_save_addr :: translates) start_lbl dest_lbl def 981 982 ] 982 983 ]. … … 991 992 992 993 definition translate_store ≝ 994 λglobals: list ident. 993 995 λaddr. 994 996 λaddr_prf: 2 ≤ addr. … … 996 998 λstart_lbl: label. 997 999 λdest_lbl: label. 998 λdef: rtl_internal_function .999 match fresh_regs_strong def (addr) with1000 λdef: rtl_internal_function globals. 1001 match fresh_regs_strong rtl_params0 globals def (addr) with 1000 1002 [ dp def_tmp_addr tmp_addr_prf ⇒ 1001 1003 let def ≝ \fst def_tmp_addr in 1002 1004 let tmp_addr ≝ \snd def_tmp_addr in 1003 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr ?tmp_addr ? in1004 let 〈def, tmpr〉 ≝ fresh_reg def in1005 let 〈tmp_addr1, tmp_addr2〉 ≝ make_addr … tmp_addr ? in 1006 let 〈def, tmpr〉 ≝ fresh_reg rtl_params0 globals def in 1005 1007 let f ≝ λtranslate_off. λsrcr. 1006 1008 let 〈translates, off〉 ≝ translate_off in 1007 1009 let translates ≝ translates @ [ 1008 adds_graph [1009 rtl_st_int tmpr off start_lbl1010 adds_graph rtl_params1 globals [ 1011 sequential rtl_params_ globals (INT rtl_params_ globals tmpr off) 1010 1012 ]; 1011 translate_op2 Oaddp tmp_addr ? addr [tmpr] ? ?;1012 adds_graph [1013 rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl1013 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) 1014 1016 ] 1015 1017 ] 1016 1018 in 1017 let 〈carry, result〉 ≝ half_add ?off int_size in1019 let 〈carry, result〉 ≝ half_add … off int_size in 1018 1020 〈translates, result〉 1019 1021 in 1020 let 〈translates, ignore〉 ≝ foldl ? ?f 〈[ ], zero ?〉 srcrs in1021 add_translates translates start_lbl dest_lbl def1022 let 〈translates, ignore〉 ≝ foldl … f 〈[ ], zero ?〉 srcrs in 1023 add_translates rtl_params1 globals translates start_lbl dest_lbl def 1022 1024 ]. 1023 1025 [1: normalize // … … 1029 1031 ] 1030 1032 qed. 1031 *)1032 1033 1033 1034 definition translate_stmt ≝ 1034 λglobals .1035 λglobals: list ident. 1035 1036 λlenv: local_env. 1036 1037 λlbl: label. 1037 1038 λstmt. 1038 λdef: joint_internal_function … (rtl_params globals).1039 λdef: rtl_internal_function globals. 1039 1040 match stmt with 1040 1041 [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def 1041  St_cost cost_lbl lbl' ⇒ add_graph lbl ( rtl_st_cost cost_lbl lbl') def1042  St_cost cost_lbl lbl' ⇒ add_graph lbl (sequential rtl_params_ globals (COST_LABEL … cost_lbl lbl')) def 1042 1043  St_const destr cst lbl' ⇒ 1043 1044 translate_cst cst (find_local_env destr lenv) lbl lbl' def 1044 1045  St_op1 op1 destr srcr lbl' ⇒ 1045 translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) ?lbl lbl' def1046 translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def 1046 1047  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' def1048 translate_op2 op2 (find_local_env destr lenv) … (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def 1048 1049  St_load ignore addr destr lbl' ⇒ 1049 translate_load (find_local_env addr lenv) ?(find_local_env destr lenv) lbl lbl' def1050 translate_load (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def 1050 1051  St_store ignore addr srcr lbl' ⇒ 1051 translate_store (find_local_env addr lenv) ?(find_local_env srcr lenv) lbl lbl' def1052 translate_store (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def 1052 1053  St_call_id f args retr lbl' ⇒ 1053 1054 match retr with 1054 1055 [ Some retr ⇒ 1055 add_graph lbl (rtl_st_call_id f (rtl_args args lenv) (find_local_env retr lenv) lbl') def1056  None ⇒ add_graph lbl (rtl_st_call_id f (rtl_args args lenv) [ ] lbl') def1056 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 1057 1058 ] 1058 1059  St_call_ptr f args retr lbl' ⇒ … … 1060 1061 [ None ⇒ 1061 1062 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1062 add_graph lbl (rtl_st_call_ptr f1 f2 (rtl_args args lenv) [ ] lbl') def1063 add_graph lbl rtl_params1 globals (sequential … (extension … (rtl_st_ext_call_ptr … f1 f2 (rtl_args args lenv) [ ] lbl'))) def 1063 1064  Some retr ⇒ 1064 1065 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') def1066 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 1066 1067 ] 1067 1068  St_tailcall_id f args ⇒ 1068 add_graph lbl (rtl_st_tailcall_id f (rtl_args args lenv)) def1069 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 1069 1070  St_tailcall_ptr f args ⇒ 1070 1071 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1071 add_graph lbl (rtl_st_tailcall_ptr f1 f2 (rtl_args args lenv)) def1072 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 1072 1073  St_cond r lbl_true lbl_false ⇒ 1073 translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def1074 translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def 1074 1075  St_jumptable r l ⇒ ? (* assert false: not implemented yet *) 1075  St_return ⇒ add_graph lbl rtl_st_returndef1076  St_return ⇒ add_graph rtl_params1 globals lbl (RETURN …) def 1076 1077 ]. 1077 1078 [10: cases not_implemented (* jtable case *) … … 1089 1090 let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse 1090 1091 (f_params def @ f_locals def) (f_result def) in 1091 let params ≝ map_list_local_env lenv (map ? ?\fst (f_params def)) in1092 let locals ≝ map_list_local_env lenv (map ? ?\fst (f_locals def)) in1092 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 1093 1094 let result ≝ 1094 1095 match (f_result def) with
Note: See TracChangeset
for help on using the changeset viewer.