source: src/RTLabs/RTLabs_classified_system.ma

Last change on this file was 3031, checked in by campbell, 7 years ago

Tidy up RTLabs preclassified_system definitions.

File size: 1.2 KB
Line 
1
2include "RTLabs/RTLabs_abstract.ma".
3include "RTLabs/RTLabs_semantics.ma".
4include "common/Measurable.ma".
5
6(* First, plain RTLabs.  This for for the front-end, the back-end will get a
7   prefix for its structured trace in terms of the version with the shadow
8   stack below. *)
9
10definition RTLabs_stack_ident :
11  genv →
12  ∀s:RTLabs_state.
13  match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] →
14  ident ≝
15λge,s.
16match s return λs. match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with
17[ Callstate id _ _ _ _ _ ⇒ λ_. id
18| _ ⇒ λH.⊥
19].
20try @H whd in match (RTLabs_classify …) in H; normalize nodelta in H;
21cases (next_instruction ?) in H; normalize nodelta //
22qed.
23
24definition RTLabs_pcs : preclassified_system ≝
25mk_preclassified_system
26  RTLabs_fullexec
27  (λ_.RTLabs_cost)
28  (λ_.RTLabs_classify)
29  RTLabs_stack_ident.
30
31(* Now the version extended with a shadow stack.  This is the one the back-end
32   will see, because it matches the RTLabs abstract status for the
33   structured traces. *)
34
35definition RTLabs_ext_pcs ≝ mk_preclassified_system
36  RTLabs_ext_fullexec
37  (λg,s. RTLabs_cost (Ras_state … s))
38  (λg,s. RTLabs_classify (Ras_state … s))
39  (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H).
Note: See TracBrowser for help on using the repository browser.