source: src/Cminor/syntax.ma @ 1626

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

Add extra type safety in front end. NB: critical freshness parts
axiomatised for now.

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