Changeset 2681 for src/ERTL/ERTLToLTL.ma


Ignore:
Timestamp:
Feb 19, 2013, 6:48:32 PM (7 years ago)
Author:
tranquil
Message:
  • improvements to the graph translation function
  • fixed passes up to LTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToLTL.ma

    r2490 r2681  
    289289
    290290definition translate_address :
    291   ∀globals.bool → ∀i.member ? (eq_identifier ?) i globals → decision → decision →
     291  ∀globals.bool → ∀i.i ∈ globals → decision → decision →
    292292  list (joint_seq LTL globals) ≝
    293293  λglobals,carry_lives_after,id,prf,addr1,addr2.
     
    300300  ∀globals.∀after : valuation register_lattice.
    301301  coloured_graph after →
    302   ℕ → label → joint_step ERTL globals → seq_block LTL globals (joint_step LTL globals)
     302  ℕ → label → joint_step ERTL globals → bind_step_block LTL globals
    303303  λglobals,after,grph,stack_sz,lbl,s.
     304  bret … (
    304305  let lookup ≝ λr.colouring … grph (inl … r) in
    305306  let lookup_arg ≝ λa.match a with
     
    311312  match s with
    312313  [ step_seq s' ⇒
    313     match s' return λ_.seq_block LTL globals (joint_step LTL globals) with
    314     [ COMMENT c ⇒ COMMENT … c
    315     | COST_LABEL cost_lbl ⇒ COST_LABEL … cost_lbl
     314    match s' return λ_.step_block LTL globals with
     315    [ COMMENT c ⇒ [COMMENT … c]
     316    | COST_LABEL cost_lbl ⇒ [COST_LABEL … cost_lbl]
    316317    | POP r ⇒
    317318      POP … A ::
     
    330331        (lookup_arg addr1)
    331332        (lookup_arg addr2)
    332     | CLEAR_CARRY ⇒ CLEAR_CARRY …
    333     | SET_CARRY ⇒ CLEAR_CARRY …
     333    | CLEAR_CARRY ⇒ [CLEAR_CARRY ??]
     334    | SET_CARRY ⇒ [CLEAR_CARRY ??]
    334335    | OP2 op dst arg1 arg2 ⇒
    335336      translate_op2_smart ? carry_lives_after op
     
    367368        move (lookup r) (arg_decision_imm (byte_of_nat stack_sz))
    368369      ]
    369     | CALL f n_args _ ⇒
     370    ]
     371  | COND r ltrue ⇒
     372    〈add_dummy_variance … (move RegisterA (lookup r)),λ_.COND … it ltrue, [ ]〉
     373  | CALL f n_args _ ⇒
    370374      match f with
    371       [ inl f ⇒ [ CALL LTL ? (inl … f) n_args it ]
     375      [ inl f ⇒
     376        〈[ ],λ_.CALL LTL ? (inl … f) n_args it, [ ]〉
    372377      | inr dp ⇒
    373378        let 〈dpl, dph〉 ≝ dp in
    374         move_to_dp … (lookup_arg dpl) (lookup_arg dph) @
    375         [ CALL LTL ? (inr … 〈it, it〉) n_args it ]
     379        〈add_dummy_variance … (move_to_dp … (lookup_arg dpl) (lookup_arg dph)),
     380         λ_.CALL LTL ? (inr … 〈it, it〉) n_args it, [ ]〉
    376381      ]
    377     ]
    378   | COND r ltrue ⇒
    379     〈move RegisterA (lookup r),COND … it ltrue〉
    380   ].
     382  ]).
    381383
    382384definition translate_fin_step:
    383   ∀globals.label → joint_fin_step ERTL → seq_block LTL globals (joint_fin_step LTL)
     385  ∀globals.label → joint_fin_step ERTL → bind_fin_block LTL globals
    384386  λglobals,lbl,s.
    385   match s return λ_.seq_block LTL globals (joint_fin_step LTL) with
     387  bret … (〈[ ],
     388  match s with
    386389  [ RETURN ⇒ RETURN ?
    387390  | GOTO l ⇒ GOTO ? l
    388391  | TAILCALL abs _ _ ⇒ Ⓧabs
    389   ].
    390 
    391 definition translate_internal: ∀globals: list ident.
     392  ]〉).
     393
     394definition translate_data : ∀globals.
    392395  joint_closed_internal_function ERTL globals →
    393   joint_closed_internal_function LTL globals ≝
    394   λglobals,int_fun.
    395   (* initialize graph *)
    396   let entry ≝ pi1 … (joint_if_entry … int_fun) in
    397   let exit ≝ pi1 … (joint_if_exit … int_fun) in
    398   (* colour registers *)
    399   let after ≝ analyse_liveness globals int_fun in
    400   let coloured_graph ≝ build after in
    401   (* compute new stack size *)
    402   let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
    403   (* initialize internal function *)
    404   let init ≝ init_graph_if LTL globals
    405     (joint_if_luniverse … int_fun)
    406     (joint_if_runiverse … int_fun)
    407     it it [ ] stack_sz entry exit in
    408   graph_translate …
    409     init
    410     (translate_step … coloured_graph stack_sz)
    411     (translate_fin_step …)
    412     int_fun.
    413 cases daemon (* TODO *) qed.
     396  bind_new register (b_graph_translate_data ERTL LTL globals) ≝
     397λglobals,int_fun.
     398(* colour registers *)
     399let after ≝ analyse_liveness globals int_fun in
     400let coloured_graph ≝ build after in
     401(* compute new stack size *)
     402let stack_sz ≝ spilled_no … coloured_graph + joint_if_stacksize … int_fun in
     403bret …
     404  (mk_b_graph_translate_data ERTL LTL globals
     405    (* init_ret ≝ *) it
     406    (* init_params ≝ *) it
     407    (* init_stack_size ≝ *) stack_sz
     408    (* added_prologue ≝ *) [ ]
     409    (* f_step ≝ *) (translate_step … coloured_graph stack_sz)
     410    (* f_fin ≝ *) (translate_fin_step globals)
     411    ???).
     412@hide_prf
     413[ #l #c % ]
     414cases daemon (* TODO *)
     415qed.
    414416
    415417definition ertl_to_ltl: ertl_program → ltl_program ≝
    416   λp.transform_program … p (λvarnames. transf_fundef … (translate_internal varnames)).
     418  b_graph_transform_program … translate_data.
Note: See TracChangeset for help on using the changeset viewer.