Changeset 2457 for src/joint/Joint.ma


Ignore:
Timestamp:
Nov 13, 2012, 11:30:23 AM (7 years ago)
Author:
tranquil
Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2437 r2457  
    2828params : adds type of code and related properties *)
    2929
     30(*
    3031inductive possible_flows : Type[0] ≝
    3132| Labels : list label → possible_flows
    3233| Call : possible_flows.
     34*)
    3335
    3436inductive argument (T : Type[0]) : Type[0] ≝
     
    8284 (* other instructions not fitting in the general framework *)
    8385 ; ext_seq : Type[0]
    84 (* ; ext_branch : Type[0]
    85  ; ext_branch_labels : ext_branch → list label*)
    86  ; ext_call : Type[0]
    87  ; ext_tailcall : Type[0]
     86 ; has_tailcalls : bool
    8887 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
    8988 ; paramsT : Type[0]
     
    143142  step_seq on _s : joint_seq ?? to joint_step ??.
    144143
    145 definition step_flows ≝ λp,globals.λs : joint_step p globals.
    146   match s with
    147   [ step_seq s ⇒
    148     match s with
    149     [ CALL _ _ _ ⇒ Call
    150     | _ ⇒ Labels … [ ]
    151     ]
    152   | COND _ l ⇒ Labels … [l]
    153   ].
    154 
    155144definition step_labels ≝
    156145  λp, globals.λs : joint_step p globals.
    157     match step_flows … s with
    158     [ Labels lbls ⇒ lbls
    159     | Call ⇒ [ ]
    160     ].
     146  match s with
     147  [ step_seq s ⇒ [ ]
     148  | COND _ l ⇒ [l]
     149  ].
    161150
    162151definition step_forall_labels : ∀p.∀globals.
     
    173162  | GOTO: label → joint_fin_step p
    174163  | RETURN: joint_fin_step p
    175   | tailcall : ext_tailcall p → joint_fin_step p.
    176 
    177 definition fin_step_flows ≝ λp.λs : joint_fin_step p.
     164  | TAILCALL :
     165    has_tailcalls p → (ident + (dpl_arg p) × (dph_arg p)) →
     166    call_args p → joint_fin_step p.
     167
     168definition fin_step_labels ≝ λp.λs : joint_fin_step p.
    178169  match s with
    179   [ GOTO l ⇒ Labels … [l]
    180   | tailcall _ ⇒ Call (* tailcalls will need to be integrated in structured traces *)
    181   | _ ⇒ Labels … [ ]
     170  [ GOTO l ⇒ [l]
     171  | _ ⇒ [ ]
    182172  ].
    183 
    184 definition fin_step_labels ≝
    185   λp.λs : joint_fin_step p.
    186     match fin_step_flows … s with
    187     [ Labels lbls ⇒ lbls
    188     | Call ⇒ [ ]
    189     ].
    190173
    191174inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
    192175  | sequential: joint_step p globals → succ p → joint_statement p globals
    193176  | final: joint_fin_step p → joint_statement p globals.
    194 
    195 coercion extension_fin_to_fin_step : ∀p : stmt_params.
    196   ∀s : ext_tailcall p.joint_fin_step p ≝
    197   tailcall on _s : ext_tailcall ? to joint_fin_step ?.
    198177
    199178coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
Note: See TracChangeset for help on using the changeset viewer.