Changeset 2490 for src/ERTL


Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (7 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

Location:
src/ERTL
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r2286 r2490  
    3737    (* call_dest ≝ *) unit
    3838    (* ext_seq ≝ *) ertl_seq
    39     (* ext_call ≝ *) void
    40     (* ext_tailcall ≝ *) void
     39    (* has_tailcall ≝ *) false
    4140    (* paramsT ≝ *) ℕ
    4241    (* localsT ≝ *) register.
     
    8887(*---------------*) ⊢
    8988ext_seq ERTL ≡ ertl_seq.
    90 unification hint 0 ≔
    91 (*---------------*) ⊢
    92 ext_call ERTL ≡ void.
    93 unification hint 0 ≔
    94 (*---------------*) ⊢
    95 ext_tailcall ERTL ≡ void.
    9689
    9790coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝
  • src/ERTL/ERTLToLTL.ma

    r2443 r2490  
    1515  | arg_decision_colour : Register → arg_decision
    1616  | arg_decision_spill : ℕ → arg_decision
    17   | arg_decision_imm : beval → arg_decision.
     17  | arg_decision_imm : Byte → arg_decision.
    1818
    1919coercion Reg_to_arg_dec : ∀r:Register.arg_decision ≝ arg_decision_colour on _r : Register to arg_decision.
     
    7575 
    7676definition set_stack_int :
    77   ∀globals.nat → beval →  list (joint_seq LTL globals) ≝
     77  ∀globals.nat → Byte →  list (joint_seq LTL globals) ≝
    7878  λglobals,off,int.
    7979  set_dp_by_offset ? off @
     
    289289
    290290definition translate_address :
    291   ∀globals.bool → ∀i.member i (eq_identifier ?) globals → decision → decision →
     291  ∀globals.bool → ∀i.member ? (eq_identifier ?) i globals → decision → decision →
    292292  list (joint_seq LTL globals) ≝
    293293  λglobals,carry_lives_after,id,prf,addr1,addr2.
     
    367367        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    368368      ]
    369     | CALL_ID f n_args _ ⇒ CALL_ID LTL ? f n_args it
    370     | extension_call abs ⇒ match abs in void with [ ]
     369    | CALL f n_args _ ⇒
     370      match f with
     371      [ inl f ⇒ [ CALL LTL ? (inl … f) n_args it ]
     372      | inr dp ⇒
     373        let 〈dpl, dph〉 ≝ dp in
     374        move_to_dp … (lookup_arg dpl) (lookup_arg dph) @
     375        [ CALL LTL ? (inr … 〈it, it〉) n_args it ]
     376      ]
    371377    ]
    372378  | COND r ltrue ⇒
     
    380386  [ RETURN ⇒ RETURN ?
    381387  | GOTO l ⇒ GOTO ? l
    382   | tailcall abs ⇒ match abs in void with [ ]
     388  | TAILCALL abs _ _ ⇒ Ⓧabs
    383389  ].
    384390
    385391definition translate_internal: ∀globals: list ident.
    386   joint_internal_function ERTL globals →
    387   joint_internal_function LTL globals ≝
    388   λglobals: list ident.
    389   λint_fun: joint_internal_function ERTL globals.
     392  joint_closed_internal_function ERTL globals →
     393  joint_closed_internal_function LTL globals ≝
     394  λglobals,int_fun.
    390395  (* initialize graph *)
    391396  let entry ≝ pi1 … (joint_if_entry … int_fun) in
     
    406411    (translate_fin_step …)
    407412    int_fun.
     413cases daemon (* TODO *) qed.
    408414
    409415definition ertl_to_ltl: ertl_program → ltl_program ≝
  • src/ERTL/liveness.ma

    r2286 r2490  
    8383        ]
    8484      (* Potentially destroys all caller-save hardware registers. *)
    85       | CALL_ID id _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    86       | extension_call abs ⇒ match abs in void with [ ]
     85      | CALL _ _ _ ⇒ 〈set_empty …, set_from_list … RegisterCallerSaved〉
    8786      ]
    8887    | COND r lbl_true ⇒ rl_bottom
     
    139138        ]
    140139      (* Reads the hardware registers that are used to pass parameters. *)
    141       | CALL_ID _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    142       | extension_call abs ⇒ match abs in void with [ ]
     140      | CALL _ nparams _ ⇒ 〈set_empty …, set_from_list … (prefix ? nparams RegisterParams)〉
    143141      | _ ⇒ rl_bottom
    144142      ]
     
    149147    [ RETURN ⇒ 〈set_empty …, set_union … (set_from_list … RegisterCalleeSaved) ret_regs〉
    150148    | GOTO l ⇒ rl_bottom
    151     | tailcall abs ⇒ match abs in void with [ ]
     149    | TAILCALL abs _ _ ⇒ match abs in False with [ ]
    152150    ]
    153151  ].
Note: See TracChangeset for help on using the changeset viewer.