Changeset 1713 for src/Cminor


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/Cminor/semantics.ma

    r1680 r1713  
    7878    ∀    m: mem.
    7979    ∀   st: stack.
    80             state.
    81 
    82 definition mem_of_state : state → mem ≝
    83 λst. match st with
    84 [ State _ _ _ _ _ m _ _ _ _ ⇒ m
    85 | Callstate _ _ m _ ⇒ m
    86 | Returnstate _ m _ ⇒ m
    87 ].
     80            state
     81| Finalstate:
     82    ∀    r: int.
     83            state
     84.
    8885
    8986axiom UnknownLocal : String.
     
    387384                   ] dstP
    388385        ]
    389     | _ ⇒ Error ? (msg BadState)
     386    | SStop ⇒
     387        match result with
     388        [ None ⇒ Error ? (msg ReturnMismatch)
     389        | Some v ⇒ match v with
     390                   [ Vint sz r ⇒ match sz return λsz. bvint sz → res ? with
     391                                 [ I32 ⇒ λr. return 〈E0, Finalstate r〉
     392                                 | _ ⇒ λ_. Error ? (msg ReturnMismatch) ] r
     393                   | _ ⇒ Error ? (msg ReturnMismatch) ]
     394        ]
    390395    ])
     396| Finalstate r ⇒ Error ? (msg BadState)
    391397].
    392398try @(π1 kInv)
     
    431437definition is_final : state → option int ≝
    432438λs. match s with
    433 [ Returnstate res m st ⇒
    434     match st with
    435     [ SStop ⇒
    436         match res with
    437         [ None ⇒ None ?
    438         | Some v ⇒
    439             match v with
    440             [ Vint sz i ⇒ intsize_eq_elim ? sz I32 ? i (λi. Some ? i) (None ?)
    441             | _ ⇒ None ?
    442             ]
    443         ]
    444     | _ ⇒ None ?
    445     ]
     439[ Finalstate r ⇒ Some ? r
    446440| _ ⇒ None ?
    447441].
Note: See TracChangeset for help on using the changeset viewer.