Changeset 2681 for src/joint/Traces.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/joint/Traces.ma

    r2645 r2681  
    9999
    100100definition joint_classify_step :
    101   ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝
    102   λp,st,stmt.
     101  ∀p : evaluation_params.joint_step p (globals … p) → status_class ≝
     102  λp,stmt.
    103103  match stmt with
    104104  [ step_seq _ ⇒ cl_other
    105   | CALL f args dest ⇒
    106     match (! bl ← block_of_call … (ev_genv p) f st ;
    107             fetch_function … (ev_genv p) bl) with
    108     [ OK id_fn ⇒
    109       match \snd id_fn with
    110       [ Internal _ ⇒ cl_call
    111       | External _ ⇒ cl_other
    112       ]
    113     | Error _ ⇒ cl_other
    114     ]
     105  | CALL f args dest ⇒ cl_call
    115106  | COND _ _ ⇒ cl_jump
    116107  ].
    117108
    118109definition joint_classify_final :
    119   ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝
    120   λp,st,stmt.
     110  ∀p : evaluation_params.joint_fin_step p → status_class ≝
     111  λp,stmt.
    121112  match stmt with
    122113  [ GOTO _ ⇒ cl_other
    123114  | RETURN ⇒ cl_return
    124   | TAILCALL _ f args ⇒
    125     match (! bl ← block_of_call … (ev_genv p) f st ;
    126             fetch_function … (ev_genv p) bl) with
    127     [ OK id_fn ⇒
    128       match \snd id_fn with
    129       [ Internal _ ⇒ cl_tailcall
    130       | External _ ⇒ cl_return
    131       ]
    132     | Error _ ⇒ cl_other
    133     ]
     115  | TAILCALL _ f args ⇒ cl_tailcall
    134116  ].
    135117
     
    139121  ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ;
    140122  match s with
    141   [ sequential s _ ⇒ Some ? (joint_classify_step p st s)
    142   | final s ⇒ Some ? (joint_classify_final p st s)
     123  [ sequential s _ ⇒ Some ? (joint_classify_step p s)
     124  | final s ⇒ Some ? (joint_classify_final p s)
    143125  | FCOND _ _ _ _ ⇒ Some ? cl_jump
    144126  ].
     
    152134lemma joint_classify_call : ∀p : evaluation_params.∀st.
    153135  joint_classify p st = Some ? cl_call →
    154   ∃i_f,f',args,dest,next,bl,i',fd'.
     136  ∃i_f,f',args,dest,next.
    155137  fetch_statement … (ev_genv p) (pc … st) =
    156     OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧
    157   block_of_call … (ev_genv p) f' st = OK ? bl ∧
    158   fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉.
     138    OK ? 〈i_f, sequential … (CALL … f' args dest) next〉.
    159139#p #st
    160140whd in match joint_classify; normalize nodelta
    161141inversion (fetch_statement … (ev_genv p) (pc … st))
    162142[2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ]
    163 * #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
    164 >m_return_bind normalize nodelta
    165   [3: whd in match joint_classify_final; normalize nodelta
    166     generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ]
    167     normalize nodelta ]
    168   #ABS destruct(ABS) ]
     143* #i_f *
     144[2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_
     145  >m_return_bind normalize nodelta normalize in ⊢ (%→?); #ABS destruct
     146]
    169147* [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind
    170 normalize nodelta
    171 [2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ]
    172 whd in match joint_classify_step;
    173 normalize nodelta
    174 inversion (block_of_call ?????)
    175 [ #bl #block_of_c  >m_return_bind
    176   inversion (fetch_function ???)
    177   [ * #i' *
    178     [ #fd' #fetch' #_
    179       %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'}
    180       % [ %{block_of_c} % ]
    181       whd in match fetch_internal_function; normalize nodelta
    182       >fetch' %
    183     ]
    184   ]
    185 ]
    186 #x #_ normalize in ⊢ (%→?); #ABS destruct(ABS)
     148normalize in ⊢ (%→?); #EQ destruct
     149%[|%[|%[|%[|%[| %]]]]]
    187150qed.
    188151
     
    340303   (* as_final ≝ *) (λs.is_final p  (globals ?) (ev_genv p) exit_pc s ≠ None ?)
    341304   (* as_call_ident ≝ *) (joint_call_ident p)
    342    (* as_tailcall_ident ≝ *) (joint_tailcall_ident p).
     305   (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). 
Note: See TracChangeset for help on using the changeset viewer.