Changeset 1293
 Timestamp:
 Oct 5, 2011, 2:47:19 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLAbstoRTL.ma
r1292 r1293 13 13 let 〈res,runiverse〉 ≝ register_freshes runiverse n' in 14 14 〈r::res,runiverse〉 ]. 15 16 definition choose_rest ≝17 λA: Type[0].18 λleft, right: list A.19 λprfl: 0 < left.20 λprfr: 0 < right.21 match left return λx. 0 < x → list A with22 [ nil ⇒ λnil_prf.23 match right return λx. 0 < x → list A with24 [ nil ⇒ λnil_nil_absrd. ?25  _ ⇒ λnil_cons_prf. right26 ] prfr27  _ ⇒ λcons_prf. right28 ] prfl.29 normalize in nil_prf;30 cases(not_le_Sn_O 0)31 #HYP32 cases(HYP nil_prf)33 qed.34 15 35 16 definition complete_regs ≝ … … 377 358 let srcrsl_rest ≝ \snd (\fst reduced) in 378 359 let srcrsr_rest ≝ \snd (\snd reduced) in 379 let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ?in360 let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in 380 361 match reduce_strong register register destrs srcrsl_common with 381 362 [ dp reduced second_reduced_proof ⇒ … … 577 558 let restl ≝ \snd (\snd crl) in 578 559 let restr ≝ \snd (\snd crl) in 579 let rest ≝ choose_rest ? restl restr ? ?in560 let rest ≝ restl @ restr in 580 561 let inits ≝ [ 581 562 sequential … (INT rtl_params_ globals destr (zero …)); … … 604 585 ] 605 586 ]. 606 [1: @their_proof 607 *: cases not_implemented (* choose rest requires nonemptiness proofs but 608 these appear impossible to obtain, similar proof 609 to above *) 610 ] 587 @their_proof 611 588 qed. 612 589 … … 1032 1009 qed. 1033 1010 1011 axiom fake_label: label. 1012 1013 (* XXX: following conversation with CSC about the mix up in extension statements 1014 and extension instructions in RTL *) 1034 1015 definition translate_stmt ≝ 1035 1016 λglobals: list ident. … … 1040 1021 match stmt with 1041 1022 [ St_skip lbl' ⇒ add_graph … lbl (GOTO … lbl') def 1042  St_cost cost_lbl lbl' ⇒ add_graph lbl (sequential rtl_params_ globals (COST_LABEL … cost_lbl lbl')) def1023  St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def 1043 1024  St_const destr cst lbl' ⇒ 1044 translate_cst cst (find_local_env destr lenv) lbl lbl' def1025 translate_cst globals cst (find_local_env destr lenv) lbl lbl' def 1045 1026  St_op1 op1 destr srcr lbl' ⇒ 1046 translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def1027 translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def 1047 1028  St_op2 op2 destr srcr1 srcr2 lbl' ⇒ 1048 translate_op2 op2 (find_local_env destr lenv) … (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def1029 translate_op2 globals op2 (find_local_env destr lenv) … (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def 1049 1030  St_load ignore addr destr lbl' ⇒ 1050 translate_load (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def1031 translate_load globals (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def 1051 1032  St_store ignore addr srcr lbl' ⇒ 1052 translate_store (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def1033 translate_store globals (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def 1053 1034  St_call_id f args retr lbl' ⇒ 1054 1035 match retr with 1055 1036 [ Some retr ⇒ 1056 add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) (find_local_env retr lenv) lbl')) def1057  None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID … f (rtl_args args lenv) [ ] lbl')) def1037 add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) (find_local_env retr lenv)) lbl') def 1038  None ⇒ add_graph rtl_params1 globals lbl (sequential … (CALL_ID rtl_params1 globals f (rtl_args args lenv) [ ]) lbl') def 1058 1039 ] 1059 1040  St_call_ptr f args retr lbl' ⇒ … … 1061 1042 [ None ⇒ 1062 1043 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 1063 add_graph lbl rtl_params1 globals (sequential … (extension … (rtl_st_ext_call_ptr … f1 f2 (rtl_args args lenv) [ ] lbl'))) def1044 add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def 1064 1045  Some retr ⇒ 1065 1046 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 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'))) def1047 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 1067 1048 ] 1068 1049  St_tailcall_id f args ⇒ 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) def1050 add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (extension rtl_params_ globals (rtl_st_ext_tailcall_id f (rtl_args args lenv))) fake_label) def 1070 1051  St_tailcall_ptr f args ⇒ 1071 1052 let 〈f1, f2〉 ≝ find_and_addr f lenv ? in 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) def1053 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))) fake_label) def 1073 1054  St_cond r lbl_true lbl_false ⇒ 1074 1055 translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def … … 1086 1067 skip instructions at these nodes. *) 1087 1068 definition translate_internal ≝ 1088 λglobals,def. 1069 λglobals: list ident. 1070 λdef. 1089 1071 let runiverse ≝ f_reggen def in 1090 1072 let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse … … 1108 1090 let entry' ≝ f_entry def in 1109 1091 let exit' ≝ f_exit def in 1110 let graph' ≝ add … (empty_map ? ?) entry' (GOTO …entry') in1111 let graph' ≝ add … graph' exit' (GOTO …exit') in1092 let graph' ≝ add LabelTag ? (empty_map LabelTag ?) entry' (GOTO rtl_params_ globals entry') in 1093 let graph' ≝ add LabelTag ? graph' exit' (GOTO rtl_params_ globals exit') in 1112 1094 let res ≝ 1113 1095 mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params' 1114 1096 locals' stack_size' graph' ? ? in 1115 foldi … (translate_stmt … lenv) (f_graph def) res.1097 foldi … (translate_stmt globals … lenv) (f_graph def) res. 1116 1098 [ % [@entry'  @graph_add_lookup @graph_add] 1117 1099  % [@exit'  @graph_add]] … … 1120 1102 (*CSC: here we are not doing any alignment on variables, like it is done in OCaml 1121 1103 because of CompCert heritage *) 1122 definition rtlabs_to_rtl 1123 λp. transform_program ???p (transf_fundef … (translate_internal (prog_var_names …))).1104 definition rtlabs_to_rtl: RTLabs_program → rtl_program ≝ 1105 λp. transform_program … p (transf_fundef … (translate_internal (prog_var_names …))).
Note: See TracChangeset
for help on using the changeset viewer.