source: src/Clight/abstract.ma @ 2325

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

Fill out some Clight bits and pieces in correctness.ma.

File size: 2.7 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. *)
55
56definition expr_labelled : expr → bool ≝
57any_expr (λe. match e with [ Expr e _ ⇒ match e with [ Ecost _ _ ⇒ true | _ ⇒ false ] ]).
58
59definition Clight_labelled : state → bool ≝
60λs. match s with
61[ State f s k e m ⇒
62  any_statement (λs. match s with [ Scost _ _ ⇒ true | _ ⇒ any_expr_statement expr_labelled s ]) s
63| _ ⇒ false
64].
65
66
67(* At the moment this doesn't say anything about "jumps", just calls, returns
68   and everything else. *)
69include "common/StructuredTraces.ma".
70
71definition Clight_classify : state → status_class ≝
72λs. match s with
73[ State _ _ _ _ _ ⇒ cl_other
74| Callstate _ _ _ _ ⇒ cl_call
75| Returnstate _ _ _ ⇒ cl_return
76| Finalstate _ ⇒ cl_other
77].
78
79(* Help avoid ambiguous input fun *)
80definition Clight_state ≝ state.
Note: See TracBrowser for help on using the repository browser.