source: src/Cminor/syntax.ma @ 2251

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

Add new invariant to Cminor that return typs should be respected.

File size: 5.7 KB
Line 
1
2include "common/FrontEndOps.ma".
3include "common/CostLabel.ma".
4include "basics/lists/list.ma".
5
6inductive expr : typ → Type[0] ≝
7| Id : ∀t. ident → expr t
8| Cst : ∀t. constant t → expr t
9| Op1 : ∀t,t'. unary_operation t t' → expr t → expr t'
10| Op2 : ∀t1,t2,t'. binary_operation t1 t2 t' → expr t1 → expr t2 → expr t'
11| Mem : ∀t. expr ASTptr → expr t
12| Cond : ∀sz,sg,t. expr (ASTint sz sg) → expr t → expr t → expr t
13| Ecost : ∀t. costlabel → expr t → expr t.
14
15(* Assert a predicate on every variable or parameter identifier. *)
16let rec expr_vars (t:typ) (e:expr t) (P:ident → typ → Prop) on e : Prop ≝
17match e with
18[ Id t i ⇒ P i t
19| Cst _ _ ⇒ True
20| Op1 _ _ _ e ⇒ expr_vars ? e P
21| Op2 _ _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
22| Mem _ e ⇒ expr_vars ? e P
23| Cond _ _ _ e1 e2 e3 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P ∧ expr_vars ? e3 P
24| Ecost _ _ e ⇒ expr_vars ? e P
25].
26
27lemma expr_vars_mp : ∀t,e,P,Q.
28  (∀i,t. P i t → Q i t) → expr_vars t e P → expr_vars t e Q.
29#t0 #e elim e normalize /3/
30[ #t1 #t2 #t #op #e1 #e2 #IH1 #IH2 #P #Q #H * #H1 #H2
31  % /3/
32| #sz #sg #t #e1 #e2 #e3 #IH1 #IH2 #IH3 #P #Q #H * * /5/
33] qed.
34
35axiom Label : String.
36
37inductive stmt : Type[0] ≝
38| St_skip : stmt
39| St_assign : ∀t. ident → expr t → stmt
40| St_store : ∀t. expr ASTptr → expr t → stmt
41(* ident for returned value, expression to identify fn, args. *)
42| St_call : option (ident × typ) → expr ASTptr → list (𝚺t. expr t) → stmt
43(* We don't use these at the moment, and they're getting in the way.
44| St_tailcall : expr ASTptr → list (𝚺t. expr t) → stmt
45*)
46| St_seq : stmt → stmt → stmt
47| St_ifthenelse : ∀sz,sg. expr (ASTint sz sg) → stmt → stmt → stmt
48| St_return : option (𝚺t. expr t) → stmt
49| St_label : identifier Label → stmt → stmt
50| St_goto : identifier Label → stmt
51| St_cost : costlabel → stmt → stmt.
52
53let rec stmt_P (P:stmt → Prop) (s:stmt) on s : Prop ≝
54match s with
55[ St_seq s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
56| St_ifthenelse _ _ _ s1 s2 ⇒ P s ∧ stmt_P P s1 ∧ stmt_P P s2
57| St_label _ s' ⇒ P s ∧ stmt_P P s'
58| St_cost _ s' ⇒ P s ∧ stmt_P P s'
59| _ ⇒ P s
60].
61
62lemma stmt_P_P : ∀P,s. stmt_P P s → P s.
63#P * normalize /2/
64[ #s1 #s2 * * /2/
65| #sz #sg #e #s1 #s2 * * /2/
66| *: #i #s normalize * /2/
67] qed.
68
69(* Assert a predicate on every variable or parameter identifier. *)
70definition stmt_vars : (ident → typ → Prop) → stmt → Prop ≝
71λP,s.
72match s with
73[ St_assign t i e ⇒ P i t ∧ expr_vars ? e P
74| St_store _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
75| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P (\fst i) (\snd i) ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
76(*
77| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
78*)
79| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
80| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
81| _ ⇒ True
82].
83
84definition stmt_labels : (identifier Label → Prop) → stmt → Prop ≝
85λP,s.
86match s with
87[ St_label l _ ⇒ P l
88| St_goto l ⇒ P l
89| _ ⇒ True
90].
91
92lemma stmt_P_mp : ∀P,Q. (∀s. P s → Q s) → ∀s. stmt_P P s → stmt_P Q s.
93#P #Q #H #s elim s /2/
94[ #s1 #s2 #H1 #H2 normalize * * /4/
95| #sz #sg #e #s1 #s2 #H1 #H2 * * /5/
96| #l #s #H * /5/
97| #l #s #H * /5/
98] qed.
99
100lemma stmt_vars_mp : ∀P,Q. (∀i,t. P i t → Q i t) → ∀s. stmt_vars P s → stmt_vars Q s.
101#P #Q #H #s elim s normalize
102[ //
103| #t #id #e * /4/
104| #t #e1 #e2 * /4/
105| * normalize [ 2: #id ] #e #es * * #H1 #H2 #H3 % [ 1,3: % /3/ | *: @(All_mp … H3) * #t #e normalize @expr_vars_mp @H ]
106(*
107| #e #es * #H1 #H2 % [ /3/ | @(All_mp … H2) * /3/ ]
108*)
109| #s1 #s2 #H1 #H2 * /3/
110| #sz #sg #e #s1 #s2 #H1 #H2 /5/
111| * normalize [ // | *; normalize /3/ ]
112| /2/
113| //
114| /2/
115] qed.
116
117lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
118#P #Q #H #s elim s normalize /2/ qed.
119
120(* Get labels from a Cminor statement. *)
121let rec labels_of (s:stmt) : list (identifier Label) ≝
122match s with
123[ St_seq s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
124| St_ifthenelse _ _ _ s1 s2 ⇒ (labels_of s1) @ (labels_of s2)
125| St_label l s ⇒ l::(labels_of s)
126| St_cost _ s ⇒ labels_of s
127| _ ⇒ [ ]
128].
129
130inductive rettyp_match : option typ → option (𝚺t.expr t) → Prop ≝
131| rettyp_none : rettyp_match (None ?) (None ?)
132| rettyp_some : ∀t,e. rettyp_match (Some ? t) (Some ? ❬t,e❭).
133
134record cminor_stmt_inv (env:list (ident × typ)) (labels:list (identifier Label)) (rettyp:option typ) (s:stmt) : Prop ≝ {
135  cm_inv_var : stmt_vars (λi,t.Exists ? (λx. x = 〈i,t〉) env) s;
136  cm_inv_labels : stmt_labels (λl.Exists ? (λl'.l' = l) labels) s;
137  cm_inv_return : match s with [ St_return oe ⇒ rettyp_match rettyp oe
138                               | _ ⇒ True ]
139}.
140
141record internal_function : Type[0] ≝
142{ f_return    : option typ
143; f_params    : list (ident × typ)
144; f_vars      : list (ident × typ)
145; f_distinct  : distinct_env … (f_params @ f_vars)
146; f_stacksize : nat
147; f_body      : stmt
148     (* Ensure that variables appear in the params and vars list with the
149        correct typ; and that all goto labels used are declared. *)
150; f_inv       : stmt_P (cminor_stmt_inv (f_params @ f_vars) (labels_of f_body) f_return) f_body
151}.
152
153(* We define two closely related versions of Cminor, the first with the original
154   initialisation data for global variables, and the second where the code is
155   responsible for initialisation and we only give the size of each variable. *)
156
157definition Cminor_program ≝ program (λ_.fundef internal_function) (list init_data).
158
159definition Cminor_noinit_program ≝ program (λ_.fundef internal_function) nat.
Note: See TracBrowser for help on using the repository browser.