Changeset 1713 for src/Clight/Cexec.ma


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/Clight/Cexec.ma

    r1647 r1713  
    490490          ret ? 〈E0, (State f Sskip k' e m')〉
    491491    ]
     492  | Kstop ⇒
     493    match res with
     494    [ Vint sz r ⇒ match sz return λsz.bvint sz → ? with [ I32 ⇒ λr. ret ? 〈E0, Finalstate r〉 | _ ⇒ λ_. Wrong ??? (msg ReturnMismatch) ] r
     495    | _ ⇒ Wrong ??? (msg ReturnMismatch)
     496    ]
    492497  | _ ⇒ Wrong ??? (msg NonsenseState)
    493498  ]
     499| Finalstate r ⇒
     500    Wrong ??? (msg NonsenseState)
    494501].
    495502
     
    508515let rec is_final (s:state) : option int ≝
    509516match s with
    510 [ Returnstate res k m ⇒
    511   match k with
    512   [ Kstop ⇒
    513     match res with
    514     [ Vint sz r ⇒ intsize_eq_elim ? sz I32 ? r (λr. Some ? r) (None ?)
    515     | _ ⇒ None ?
    516     ]
    517   | _ ⇒ None ?
    518   ]
     517[ Finalstate r ⇒ Some ? r
    519518| _ ⇒ None ?
    520519].
     
    524523[ #f #s #k #e #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
    525524| #f #l #k #m %2 ; % *; #r #H inversion H; #i #m #e destruct;
    526 | #v #k #m cases k;
    527   [ cases v;
    528     [ 2: * #i [ 1,2: %2 % * #r #H inversion H #i' #m #e destruct
    529               | %1 ; %{ i} //;
    530               ]
    531     | 1: %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    532     | #f %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    533     | #r %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    534     | #ptr %2 ; % *;   #r #H inversion H; #i #m #e destruct;
    535     ]
    536   | #a #b %2 ; % *; #r #H inversion H; #i #m #e destruct;
    537   | 3,4: #a #b #c %2 ; % *; #r #H inversion H; #i #m #e destruct;
    538   | 5,6,8: #a #b #c #d %2 ; % *; #r #H inversion H; #i #m #e destruct;
    539   | #a %2 ; % *; #r #H inversion H; #i #m #e destruct;
    540   ]
     525| #v #k #m %2 % * #r #H inversion H #H1 #H2 #H3 #H4 destruct
     526| #r %1 %{r} %
    541527] qed.
    542528
     
    554540  ]
    555541].
    556 
     542(*
    557543definition mem_of_state : state → mem ≝
    558544λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ].
    559 
     545*)
    560546definition clight_exec : trans_system io_out io_in ≝
    561547  mk_trans_system ?? genv (λ_.state) (λ_.is_final) exec_step.
Note: See TracChangeset for help on using the changeset viewer.