Changeset 1278


Ignore:
Timestamp:
Sep 27, 2011, 9:57:12 AM (8 years ago)
Author:
sacerdot
Message:

oppargs requires two more arguments. RTLtoERTL to be fixed since it was
bugged anyway

Location:
src/RTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1275 r1278  
    1414  (mk_params__ register register register register
    1515    (register × register) register (list register) (list register)
    16       rtl_statement_extension unit (list register) (list register)) label.
     16      rtl_statement_extension (list register) (list register) (list register)) label.
    1717
    1818definition rtl_statement ≝ joint_statement rtl_params_.
     
    3333inductive rtlntc_statement_extension: Type[0] ≝
    3434  | rtlntc_st_ext_address: register → register → rtlntc_statement_extension
    35   | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension
    36   | rtlntc_st_ext_tailcall_id: ident → list register → rtlntc_statement_extension
    37   | rtlntc_st_ext_tailcall_ptr: register → register → list register → rtlntc_statement_extension.
     35  | rtlntc_st_ext_call_ptr: register → register → list register → list register → rtlntc_statement_extension.
    3836
    3937definition rtlntc_params_: params_ ≝
     
    4139  (mk_params__ register register register register
    4240    (register × register) register (list register) (list register)
    43       rtlntc_statement_extension unit (list register) (list register)) label.
     41      rtlntc_statement_extension (list register) (list register) (list register)) label.
    4442
    4543definition rtlntc_statement ≝ joint_statement rtlntc_params_.
  • src/RTL/RTLtoERTL.ma

    r1275 r1278  
    370370
    371371definition translate_stmt :
    372  ∀globals: list ident. label → rtl_statement globals → ertl_internal_function globals → ertl_internal_function globals
     372 ∀globals: list ident. label → rtlntc_statement globals → ertl_internal_function globals → ertl_internal_function globals
    373373 ≝
    374374  λglobals.
     
    381381  | joint_st_sequential seq lbl' ⇒
    382382     match seq with
    383       [ joint_instr_call_id f args ret_regs ⇒
     383      [ joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     384      | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
     385      | joint_instr_call_id f args ret_regs ⇒
    384386         translate_call_id … f args ret_regs lbl lbl' def
    385387      | joint_instr_move rs ⇒
     
    389391      | joint_instr_extension ext ⇒
    390392         match ext with
    391           [ rtl_st_ext_call_ptr _ _ _ _ ⇒ ? (*CSC: XXXX not implemented in OCaml too *)
    392           | rtl_st_ext_address r1 r2 ⇒
     393          [ rtlntc_st_ext_call_ptr _ _ _ _ ⇒ ⊥ (*CSC: XXXX not implemented in OCaml too *)
     394          | rtlntc_st_ext_address r1 r2 ⇒
    393395             adds_graph … [
    394396              joint_st_sequential … (joint_instr_move … 〈pseudo r1, hardware RegisterSPL〉) lbl;
    395397              joint_st_sequential … (joint_instr_move … 〈pseudo r2, hardware RegisterSPH〉) lbl
    396              ] lbl lbl' def
    397           (*| _ ⇒ ? (* assert false: not implemented or should not happen *)*)
    398           ]
     398             ] lbl lbl' def]
    399399      (*CSC: everything is just copied to re-type it from now on;
    400400        the problem is call_id that takes different parameters, but that is pattern-matched
     
    421421      | joint_instr_comment msg ⇒
    422422        add_graph … lbl (joint_st_sequential ertl_params_ … (joint_instr_comment … msg) lbl') def
    423       | joint_instr_push _ ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    424       | joint_instr_pop _  ⇒ ⊥ (*CSC: XXXX should not be in the syntax *)
    425423      ]].
    426   cases not_implemented
     424  cases not_implemented (*CSC: XXXX spurious things in the syntax and ptr_calls *)
    427425qed.
    428426
    429427(* hack with empty graphs used here *)
    430428definition translate_funct_internal ≝
    431   λglobals.λdef:rtl_internal_function globals.
     429  λglobals.λdef:rtlntc_internal_function globals.
    432430  let nb_params ≝ |joint_if_params ?? def| in
    433431  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
Note: See TracChangeset for help on using the changeset viewer.