Ignore:
Timestamp:
Feb 21, 2012, 11:58:12 AM (8 years ago)
Author:
campbell
Message:

Add a distinguished final state to the front-end languages to match up
with the structured traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/semantics.ma

    r1681 r1713  
    4444   ∀ stk : list frame.
    4545   ∀   m : mem.
    46    state.
    47 
    48 definition mem_of_state : state → mem ≝
    49 λs. match s with [ State _ _ m ⇒ m | Callstate _ _ _ _ m ⇒ m | Returnstate _ _ _ m ⇒ m ].
     46   state
     47| Finalstate :
     48   ∀   r : int.
     49   state
     50.
    5051
    5152definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
     
    183184| Returnstate v dst fs m ⇒
    184185    match fs with
    185     [ nil ⇒ Error ? (msg FinalState) (* Already in final state *)
     186    [ nil ⇒
     187        match v with
     188        [ Some v' ⇒
     189          match v' with
     190          [ Vint sz r ⇒ match sz return λsz. bvint sz → monad Res ? with
     191                        [ I32 ⇒ λr. return 〈E0, Finalstate r〉
     192                        | _ ⇒ λ_. Error ? (msg ReturnMismatch)
     193                        ] r
     194          | _ ⇒ Error ? (msg ReturnMismatch)
     195          ]
     196        | _ ⇒ Error ? (msg ReturnMismatch)
     197        ]
    186198    | cons f fs' ⇒
    187199        ! locals ← match dst with
     
    192204        return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
    193205    ]
     206| Finalstate r ⇒ Error ? (msg FinalState) (* Already in final state *)
    194207]. try @(next_ok f) try @lookup_lookup_present try @H
    195208[ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ]
     
    200213definition RTLabs_is_final : state → option int ≝
    201214λs. match s with
    202 [ State _ _ _ ⇒ None ?
    203 | Callstate _ _ _ _ _ ⇒ None ?
    204 | Returnstate v _ fs _ ⇒
    205     match fs with [ nil ⇒
    206       match v with [ Some v' ⇒
    207         match v' with
    208         [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    209         | _ ⇒ None ? ]
    210       | None ⇒ None ? ]
    211     | cons _ _ ⇒ None ? ]
     215[ Finalstate r ⇒ Some ? r
     216| _ ⇒ None ?
    212217].
    213218
     
    251256| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
    252257| from_ret : ∀ge,f,fs,rtv,dst,f',m. frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m)
     258| finish : ∀ge,r,dst,m. state_rel ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) (Finalstate r)
    253259.
    254260
     
    315321  [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct
    316322    %5 cases f #func #locals #next #next_ok #sp #retdst %
    317   | #E destruct
     323  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct // | *: normalize #a try #b destruct ] ]
    318324  ]
    319 ] qed.
    320 
     325| #r #tr #s' normalize #E destruct
     326] qed.
     327
Note: See TracChangeset for help on using the changeset viewer.