source: src/Clight/abstract.ma @ 2326

Last change on this file since 2326 was 2326, checked in by campbell, 8 years ago

More accurate notion of labelled states in Clight.

File size: 3.8 KB
Line 
1include "Clight/Csem.ma".
2
3(* Definitions about Clight syntax and semantics for use in overall results. *)
4
5let rec any_expr (P:expr → bool) (e:expr) on e : bool ≝
6P e ∨
7match e with [ Expr e _ ⇒
8match e with
9[ Ederef e' ⇒ any_expr P e'
10| Eunop _ e' ⇒ any_expr P e'
11| Ebinop _ e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
12| Ecast _ e' ⇒ any_expr P e'
13| Econdition e1 e2 e3 ⇒ any_expr P e1 ∨ any_expr P e2 ∨ any_expr P e3
14| Eandbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
15| Eorbool e1 e2 ⇒ any_expr P e1 ∨ any_expr P e2
16| Efield e' _ ⇒ any_expr P e'
17| Ecost _ e' ⇒ any_expr P e'
18| _ ⇒ false
19] ].
20
21definition any_expr_statement : (expr → bool) → statement → bool ≝
22λP,s.
23match s with
24[ Sassign e1 e2 ⇒ P e1 ∨ P e2
25| Scall oe e es ⇒ (option_map_def … P false oe) ∨ P e ∨ all ? P es
26| Sifthenelse e _ _ ⇒ P e
27| Swhile e _ ⇒ P e
28| Sdowhile e _ ⇒ P e
29| Sfor _ e _ _ ⇒ P e
30| Sreturn oe ⇒ option_map_def … P false oe
31| _ ⇒ false
32].
33
34let rec any_statement (P:statement → bool) (s:statement) on s : bool ≝
35P s ∨
36match s with
37[ Ssequence s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2
38| Sifthenelse _ s1 s2 ⇒ any_statement P s1 ∨ any_statement P s2
39| Swhile _ s1 ⇒ any_statement P s1
40| Sdowhile _ s1 ⇒ any_statement P s1
41| Sfor s1 _ s2 s3 ⇒ any_statement P s1 ∨ any_statement P s2 ∨ any_statement P s3
42| Sswitch _ ls ⇒ any_labeled_statement P ls
43| Slabel _ s1 ⇒ any_statement P s1
44| Scost _ s1 ⇒ any_statement P s1
45| _ ⇒ false
46] and any_labeled_statement (P:statement → bool) (ls:labeled_statements) on ls : bool ≝
47match ls with
48[ LSdefault s ⇒ any_statement P s
49| LScase _ _ s ls' ⇒ any_statement P s ∨ any_labeled_statement P ls'
50].
51
52(* Labelled states in Clight are a little tricky because there are cost labels
53   in the expressions in addition to the cost statement.  Note that a labelled
54   state may produce several cost labels due to expressions, and that we should
55   only check the root of the statement because sub-statements will not be
56   executed until later.
57   
58   Also, a labelled state will only be guaranteed to generate a cost label in
59   the trace if the program is properly cost labelled - if it isn't then an
60   Econd might be used to with a cost label in only one branch.
61    *)
62
63definition expr_labelled : expr → bool ≝
64any_expr (λe. match e with [ Expr e _ ⇒ match e with [ Ecost _ _ ⇒ true | _ ⇒ false ] ]).
65
66definition statement_cont_labelled : statement → cont → bool ≝
67λs,k.
68match s with
69[ Sskip ⇒
70  match k with
71  [ Kdowhile e _ _ ⇒ expr_labelled e
72  | _ ⇒ false
73  ]
74| Sassign e1 e2 ⇒ expr_labelled e1 ∨ expr_labelled e2
75| Scall oe e es ⇒ (option_map_def … expr_labelled false oe) ∨ expr_labelled e ∨ all ? expr_labelled es
76| Ssequence _ _ ⇒ false
77| Sifthenelse e _ _ ⇒ expr_labelled e
78| Swhile e _ ⇒ expr_labelled e
79| Sdowhile e _ ⇒ false
80| Sfor s e _ _ ⇒ match s with [ Sskip ⇒ expr_labelled e | _ ⇒ false ]
81| Sbreak ⇒ false
82| Scontinue ⇒
83  match k with
84  [ Kdowhile e _ _ ⇒ expr_labelled e
85  | _ ⇒ false
86  ]
87| Sreturn oe ⇒ option_map_def … expr_labelled false oe
88| Sswitch e _ ⇒ expr_labelled e (* should not occur due to early switch removal *)
89| Slabel _ _ ⇒ false
90| Sgoto _ ⇒ false
91| Scost _ _ ⇒ true
92].
93
94definition Clight_labelled : state → bool ≝
95λs. match s with
96[ State f s k e m ⇒ statement_cont_labelled s k
97| _ ⇒ false
98].
99
100
101(* At the moment this doesn't say anything about "jumps", just calls, returns
102   and everything else. *)
103include "common/StructuredTraces.ma".
104
105definition Clight_classify : state → status_class ≝
106λs. match s with
107[ State _ _ _ _ _ ⇒ cl_other
108| Callstate _ _ _ _ ⇒ cl_call
109| Returnstate _ _ _ ⇒ cl_return
110| Finalstate _ ⇒ cl_other
111].
112
113(* Help avoid ambiguous input fun *)
114definition Clight_state ≝ state.
Note: See TracBrowser for help on using the repository browser.