Changeset 2293 for src/RTLabs


Ignore:
Timestamp:
Aug 13, 2012, 12:21:28 PM (7 years ago)
Author:
campbell
Message:

Add instruction pointer for call states in RTLabs.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2288 r2293  
    132132   left.  Functions are identified by their function pointer block because
    133133   this avoids introducing functions to map back pointers to function ids using
    134    the global environment.  (See the comment at the start of this file, too.) *)
     134   the global environment.  (See the comment at the start of this file, too.)
     135   
     136   Calls also get the caller's instruction label (or None for the initial call)
     137   so that we can distinguish different calls.  This is used only for the
     138   t.*_unrepeating property, which includes the pc for call states.
     139    *)
    135140
    136141inductive RTLabs_pc : Type[0] ≝
    137142| rapc_state : block → label → RTLabs_pc
    138 | rapc_call : block → RTLabs_pc
     143| rapc_call : option label → block → RTLabs_pc
    139144| rapc_ret : option block → RTLabs_pc
    140145| rapc_fin : RTLabs_pc
    141146.
    142147
     148(* TODO: move to pointers *)
     149unification hint 0 ≔ ; D ≟ block_eq
     150(*-----------------------------------------------------*)⊢
     151block ≡ carr D.
     152
    143153definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝
    144154λx,y. match x with
    145155[ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2 | _ ⇒ false ]
    146 | rapc_call b1 ⇒ match y with [ rapc_call b2 ⇒ eq_block b1 b2 | _ ⇒ false ]
    147 | rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eq_option block_eq b1 b2 | _ ⇒ false ]
     156| rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒
     157    eqb ? o1 o2
     158    ∧ eq_block b1 b2
     159  | _ ⇒ false ]
     160| rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2 | _ ⇒ false ]
    148161| rapc_fin ⇒ match y with [ rapc_fin ⇒ true | _ ⇒ false ]
    149162].
    150163
     164(* TODO: move *)
     165lemma eqb_elim : ∀D:DeqSet. ∀P:bool → Type[0]. ∀x,y:D.
     166  (x = y → P true) →
     167  (x ≠ y → P false) →
     168  P (eqb D x y).
     169#D #P #x #y #T #F lapply (eqb_true D x y) cases (eqb D x y) *
     170[ #TT #_ @T @TT //
     171| #_ #FF @F % #E destruct lapply (FF (refl ??)) #E destruct
     172] qed.
     173
    151174definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.
    152 whd in match RTLabs_pc_eq; whd in match eq_option; whd in match block_eq;
    153 * [ #b1 #l1 | #b1 | * [2: #b1 ] | ]
    154 * [ 1,5,9,13,17: #b2 #l2 | 2,6,10,14,18: #b2 | 3,7,11,15,19: * [2,4,6,8,10: #b2] | *: ]
     175whd in match RTLabs_pc_eq;
     176* [ #b1 #l1 | #bl1 #b1 | #ob1 | ]
     177* [ 1,5,9,13: #b2 #l2 | 2,6,10,14: #bl2 #b2 | 3,7,11,15: #ob2 | *: ]
    155178normalize nodelta
    156 [ 1,7,13: @eq_block_elim [ 1,3,5: #E destruct | *: * #NE ] ]
    157 [ 1,4: @eq_identifier_elim [ 1,3: #E destruct | *: * #NE ] ]
     179[ @eq_block_elim [ #E destruct | * #NE ] ]
     180[ @eq_identifier_elim [ #E destruct | *: * #NE ] ]
     181[ 8,13: @eqb_elim [ 1,3: #E destruct | *: * #NE ] ]
     182[ @eq_block_elim [ #E destruct | * #NE ] ]
    158183normalize % #E destruct try (cases (NE (refl ??))) @refl
    159184qed.
     
    163188match s' return λs'. Ras_Fn_Match ? s' ? → ? with
    164189[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
    165 | Callstate _ _ _ _ _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call b ]
     190| Callstate _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ]
    166191| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
    167192| Finalstate _ ⇒ λmtc. rapc_fin
Note: See TracChangeset for help on using the changeset viewer.