Changeset 1293


Ignore:
Timestamp:
Oct 5, 2011, 2:47:19 PM (8 years ago)
Author:
mulligan
Message:

finished rtl abs to rtl transformation subject to closing some axioms that hopefully can be closed by establishing just what is happening in translate_op

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLAbstoRTL.ma

    r1292 r1293  
    1313     let 〈res,runiverse〉 ≝ register_freshes runiverse n' in
    1414      〈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 with
    22   [ nil ⇒ λnil_prf.
    23     match right return λx. 0 < |x| → list A with
    24     [ nil ⇒ λnil_nil_absrd. ?
    25     | _ ⇒ λnil_cons_prf. right
    26     ] prfr
    27   | _ ⇒ λcons_prf. right
    28   ] prfl.
    29   normalize in nil_prf;
    30   cases(not_le_Sn_O 0)
    31   #HYP
    32   cases(HYP nil_prf)
    33 qed.
    3415
    3516definition complete_regs ≝
     
    377358    let srcrsl_rest ≝ \snd (\fst reduced) in
    378359    let srcrsr_rest ≝ \snd (\snd reduced) in
    379     let srcrs_rest ≝ choose_rest ? srcrsl_rest srcrsr_rest ? ? in
     360    let srcrs_rest ≝ srcrsl_rest @ srcrsr_rest in
    380361    match reduce_strong register register destrs srcrsl_common with
    381362    [ dp reduced second_reduced_proof ⇒
     
    577558      let restl ≝ \snd (\snd crl) in
    578559      let restr ≝ \snd (\snd crl) in
    579       let rest ≝ choose_rest ? restl restr ? ? in
     560      let rest ≝ restl @ restr in
    580561      let inits ≝ [
    581562        sequential … (INT rtl_params_ globals destr (zero …));
     
    604585    ]
    605586  ].
    606   [1: @their_proof
    607   |*: cases not_implemented (* choose rest requires non-emptiness proofs but
    608                                these appear impossible to obtain, similar proof
    609                                to above *)
    610   ]
     587  @their_proof
    611588qed.
    612589
     
    10321009qed.
    10331010
     1011axiom fake_label: label.
     1012
     1013(* XXX: following conversation with CSC about the mix up in extension statements
     1014        and extension instructions in RTL *)
    10341015definition translate_stmt ≝
    10351016  λglobals: list ident.
     
    10401021  match stmt with
    10411022  [ 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')) def
     1023  | St_cost cost_lbl lbl' ⇒ add_graph rtl_params1 globals lbl (sequential rtl_params_ globals (COST_LABEL rtl_params_ globals cost_lbl) lbl') def
    10431024  | St_const destr cst lbl' ⇒
    1044     translate_cst cst (find_local_env destr lenv) lbl lbl' def
     1025    translate_cst globals cst (find_local_env destr lenv) lbl lbl' def
    10451026  | St_op1 op1 destr srcr lbl' ⇒
    1046     translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
     1027    translate_op1 globals op1 (find_local_env destr lenv) (find_local_env srcr lenv) … lbl lbl' def
    10471028  | 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' def
     1029    translate_op2 globals op2 (find_local_env destr lenv) … (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) ? ? lbl lbl' def
    10491030  | St_load ignore addr destr lbl' ⇒
    1050     translate_load (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def
     1031    translate_load globals (find_local_env addr lenv) … (find_local_env destr lenv) lbl lbl' def
    10511032  | St_store ignore addr srcr lbl' ⇒
    1052     translate_store (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def
     1033    translate_store globals (find_local_env addr lenv) … (find_local_env srcr lenv) lbl lbl' def
    10531034  | St_call_id f args retr lbl' ⇒
    10541035    match retr with
    10551036    [ Some retr ⇒
    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
     1037      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
    10581039    ]
    10591040  | St_call_ptr f args retr lbl' ⇒
     
    10611042    [ None ⇒
    10621043      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'))) def
     1044        add_graph rtl_params1 globals lbl (sequential … (extension … (rtl_st_ext_call_ptr f1 f2 (rtl_args args lenv) [ ])) lbl') def
    10641045    | Some retr ⇒
    10651046      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'))) def
     1047        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
    10671048    ]
    10681049  | 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) def
     1050    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
    10701051  | St_tailcall_ptr f args ⇒
    10711052    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) def
     1053      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
    10731054  | St_cond r lbl_true lbl_false ⇒
    10741055    translate_cond globals (find_local_env r lenv) lbl lbl_true lbl_false def
     
    10861067   skip instructions at these nodes. *)
    10871068definition translate_internal ≝
    1088   λglobals,def.
     1069  λglobals: list ident.
     1070  λdef.
    10891071  let runiverse ≝ f_reggen def in
    10901072  let 〈lenv,runiverse〉 ≝ initialize_local_env runiverse
     
    11081090  let entry' ≝ f_entry def in
    11091091  let exit' ≝ f_exit def in
    1110   let graph' ≝ add … (empty_map ? ?) entry' (GOTO … entry') in
    1111   let graph' ≝ add … graph' exit' (GOTO … exit') in
     1092  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
    11121094  let res ≝
    11131095    mk_joint_internal_function … (rtl_params globals) luniverse' runiverse' result' params'
    11141096     locals' stack_size' graph' ? ? in
    1115     foldi … (translate_stmt … lenv) (f_graph def) res.
     1097    foldi … (translate_stmt globals … lenv) (f_graph def) res.
    11161098[ % [@entry' | @graph_add_lookup @graph_add]
    11171099| % [@exit'  | @graph_add]]
     
    11201102(*CSC: here we are not doing any alignment on variables, like it is done in OCaml
    11211103  because of CompCert heritage *)
    1122 definition rtlabs_to_rtl : RTLabs_program → rtl_program ≝
    1123  λp. transform_program ??? p (transf_fundef … (translate_internal (prog_var_names …))).
     1104definition 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.