Changeset 3255 for src/ERTL/liveness.ma


Ignore:
Timestamp:
May 8, 2013, 4:53:31 PM (7 years ago)
Author:
tranquil
Message:
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/liveness.ma

    r3037 r3255  
    7474      | extension_seq ext ⇒
    7575        match ext with
    76          [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    77          | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    78          | ertl_frame_size r ⇒ rl_psingleton r
     76         [ ertl_frame_size r ⇒ rl_psingleton r
    7977         ]
    8078      (* Potentially destroys all caller-save hardware registers. *)
     
    131129      | extension_seq ext ⇒
    132130        match ext with
    133          [ ertl_new_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    134          | ertl_del_frame ⇒ rl_join (rl_hsingleton RegisterSPL) (rl_hsingleton RegisterSPH)
    135          | ertl_frame_size r ⇒ rl_bottom ]
     131         [ ertl_frame_size r ⇒ rl_bottom ]
    136132      (* Reads the hardware registers that are used to pass parameters. *)
    137133      | _ ⇒ rl_bottom
     
    190186  | extension_seq ext ⇒
    191187    match ext with
    192      [ ertl_new_frame ⇒ false
    193      | ertl_del_frame ⇒ false
    194      | ertl_frame_size r ⇒
     188     [ ertl_frame_size r ⇒
    195189       ¬set_member ? (eq_identifier RegisterTag) r pliveafter
    196190     ]
     
    253247definition vertex ≝ register + Register.
    254248
    255 definition plives : register → register_lattice → bool ≝
     249definition p_in_lattice : register → register_lattice → bool ≝
    256250  λvertex.λprop.set_member ? (eq_identifier RegisterTag) vertex (\fst prop).
    257 definition hlives : Register → register_lattice → bool ≝
     251definition h_in_lattice : Register → register_lattice → bool ≝
    258252  λvertex.λprop.set_member ? eq_Register vertex (\snd prop).
    259253
    260 definition lives : vertex → register_lattice → bool ≝
     254definition in_lattice : vertex → register_lattice → bool ≝
    261255  λvertex.
    262256  match vertex with
    263   [ inl v ⇒ plives v
    264   | inr v ⇒ hlives v
    265   ].
     257  [ inl v ⇒ p_in_lattice v
     258  | inr v ⇒ h_in_lattice v
     259  ].
Note: See TracChangeset for help on using the changeset viewer.