source: Deliverables/D3.3/id-lookup-branch/Clight/toCminor.ma @ 1097

Last change on this file since 1097 was 1097, checked in by campbell, 9 years ago

Checkpoint labels work on branch again.

File size: 48.5 KB
Line 
1
2include "Clight/Csyntax.ma".
3include "Clight/TypeComparison.ma".
4include "utilities/lists.ma".
5(*
6let rec mem_vars_expr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
7match e with
8[ Expr ed ty ⇒
9    match ed with
10    [ Ederef e1 ⇒ mem_vars_expr mem_vars e1
11    | Eaddrof e1 ⇒ mem_vars_addr mem_vars e1
12    | Eunop _ e1 ⇒ mem_vars_expr mem_vars e1
13    | Ebinop _ e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
14                       mem_vars_expr mem_vars e2
15    | Ecast _ e1 ⇒ mem_vars_expr mem_vars e1
16    | Econdition e1 e2 e3 ⇒ mem_vars_expr mem_vars e1 ∧
17                            mem_vars_expr mem_vars e2 ∧
18                            mem_vars_expr mem_vars e3
19    | Eandbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
20                       mem_vars_expr mem_vars e2
21    | Eorbool e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
22                      mem_vars_expr mem_vars e2
23    | Efield e1 _ ⇒ mem_vars_expr mem_vars e1
24    | Ecost _ e1 ⇒ mem_vars_expr mem_vars e1
25    | _ ⇒ True
26    ]
27]
28and mem_vars_addr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝
29match e with
30[ Expr ed ty ⇒
31    match ed with
32    [ Evar x ⇒ mem_set ? mem_vars x = true
33    | Ederef e1 ⇒ mem_vars_expr mem_vars e1
34    | Efield e1 _ ⇒ mem_vars_addr mem_vars e1
35    | _ ⇒ False (* not an lvalue *)
36    ]
37].
38
39let rec mem_vars_stmt (mem_vars:identifier_set SymbolTag) (s:statement) on s : Prop ≝
40match s with
41[ Sskip ⇒ True
42| Sassign e1 e2 ⇒ mem_vars_expr mem_vars e1 ∧
43                  mem_vars_expr mem_vars e2
44| Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ] ∧
45                    mem_vars_expr mem_vars e2 ∧
46                    All ? (mem_vars_expr mem_vars) es
47| Ssequence s1 s2 ⇒ mem_vars_stmt mem_vars s1 ∧
48                    mem_vars_stmt mem_vars s2
49| Sifthenelse e1 s1 s2 ⇒ mem_vars_expr mem_vars e1 ∧
50                         mem_vars_stmt mem_vars s1 ∧
51                         mem_vars_stmt mem_vars s2
52| Swhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧
53                 mem_vars_stmt mem_vars s1
54| Sdowhile e1 s1 ⇒ mem_vars_expr mem_vars e1 ∧
55                   mem_vars_stmt mem_vars s1
56| Sfor s1 e1 s2 s3 ⇒ mem_vars_stmt mem_vars s1 ∧
57                     mem_vars_expr mem_vars e1 ∧
58                     mem_vars_stmt mem_vars s2 ∧
59                     mem_vars_stmt mem_vars s3
60| Sbreak ⇒ True
61| Scontinue ⇒ True
62| Sreturn oe1 ⇒ match oe1 with [ None ⇒ True | Some e1 ⇒ mem_vars_expr mem_vars e1 ]
63| Sswitch e1 ls ⇒ mem_vars_expr mem_vars e1 ∧
64                  mem_vars_ls mem_vars ls
65| Slabel _ s1 ⇒ mem_vars_stmt mem_vars s1
66| Sgoto _ ⇒ True
67| Scost _ s1 ⇒ mem_vars_stmt mem_vars s1
68]
69and mem_vars_ls (mem_vars:identifier_set SymbolTag) (ls:labeled_statements) on ls : Prop ≝
70match ls with
71[ LSdefault s1 ⇒ mem_vars_stmt mem_vars s1
72| LScase _ s1 ls1 ⇒ mem_vars_stmt mem_vars s1 ∧
73                    mem_vars_ls mem_vars ls1
74].
75*)
76
77let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝
78match e with
79[ Expr ed ty ⇒
80    match ed with
81    [ Ederef e1 ⇒ gather_mem_vars_expr e1
82    | Eaddrof e1 ⇒ gather_mem_vars_addr e1
83    | Eunop _ e1 ⇒ gather_mem_vars_expr e1
84    | Ebinop _ e1 e2 ⇒ gather_mem_vars_expr e1 ∪
85                       gather_mem_vars_expr e2
86    | Ecast _ e1 ⇒ gather_mem_vars_expr e1
87    | Econdition e1 e2 e3 ⇒ gather_mem_vars_expr e1 ∪
88                            gather_mem_vars_expr e2 ∪
89                            gather_mem_vars_expr e3
90    | Eandbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
91                       gather_mem_vars_expr e2
92    | Eorbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪
93                      gather_mem_vars_expr e2
94    | Efield e1 _ ⇒ gather_mem_vars_expr e1
95    | Ecost _ e1 ⇒ gather_mem_vars_expr e1
96    | _ ⇒ ∅
97    ]
98]
99and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝
100match e with
101[ Expr ed ty ⇒
102    match ed with
103    [ Evar x ⇒ { (x) }
104    | Ederef e1 ⇒ gather_mem_vars_expr e1
105    | Efield e1 _ ⇒ gather_mem_vars_addr e1
106    | _ ⇒ ∅ (* not an lvalue *)
107    ]
108].
109
110let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝
111match s with
112[ Sskip ⇒ ∅
113| Sassign e1 e2 ⇒ gather_mem_vars_expr e1 ∪
114                  gather_mem_vars_expr e2
115| Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] ∪
116                    gather_mem_vars_expr e2 ∪
117                    (foldl ?? (λs,e. s ∪ gather_mem_vars_expr e) ∅ es)
118| Ssequence s1 s2 ⇒ gather_mem_vars_stmt s1 ∪
119                    gather_mem_vars_stmt s2
120| Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪
121                         gather_mem_vars_stmt s1 ∪
122                         gather_mem_vars_stmt s2
123| Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
124                 gather_mem_vars_stmt s1
125| Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪
126                   gather_mem_vars_stmt s1
127| Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪
128                     gather_mem_vars_expr e1 ∪
129                     gather_mem_vars_stmt s2 ∪
130                     gather_mem_vars_stmt s3
131| Sbreak ⇒ ∅
132| Scontinue ⇒ ∅
133| Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ]
134| Sswitch e1 ls ⇒ gather_mem_vars_expr e1 ∪
135                  gather_mem_vars_ls ls
136| Slabel _ s1 ⇒ gather_mem_vars_stmt s1
137| Sgoto _ ⇒ ∅
138| Scost _ s1 ⇒ gather_mem_vars_stmt s1
139]
140and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝
141match ls with
142[ LSdefault s1 ⇒ gather_mem_vars_stmt s1
143| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
144                      gather_mem_vars_ls ls1
145].
146
147inductive var_type : Type[0] ≝
148| Global : region → var_type
149| Stack  : nat → var_type
150| Local  : var_type
151.
152
153definition var_types ≝ identifier_map SymbolTag var_type.
154
155axiom UndeclaredIdentifier : String.
156
157definition lookup' ≝
158λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id).
159
160definition local_id : var_types → ident → Prop ≝
161λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ].
162
163(* Note that the semantics allows locals to shadow globals.
164   Parameters start out as locals, but get stack allocated if their address
165   is taken.  We will add code to store them if that's the case.
166 *)
167
168definition always_alloc : type → bool ≝
169λt. match t with
170[ Tarray _ _ _ ⇒ true
171| Tstruct _ _ ⇒ true
172| Tunion _ _ ⇒ true
173| _ ⇒ false
174].
175
176definition characterise_vars : list (ident×region) → function → var_types × nat ≝
177λglobals, f.
178  let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
179  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
180  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
181    let 〈m,stack_high〉 ≝ ms in
182    let 〈id,ty〉 ≝ v in
183    let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id
184                           then 〈Stack stack_high,stack_high + sizeof ty〉
185                           else 〈Local, stack_high〉 in
186      〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
187  〈m,stacksize〉.
188
189lemma local_id_add_global : ∀vars,id,r,id'.
190  local_id (add ?? vars id (Global r)) id' → local_id vars id'.
191#var #id #r #id'
192whd in ⊢ (% → ?) whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?)
193cases (identifier_eq ? id id')
194[ #E >E >lookup_add_hit whd in ⊢ (% → ?) *
195| #NE >lookup_add_miss // @eq_identifier_elim // #E >E in NE * /2/
196] qed.
197
198lemma local_id_add_miss : ∀vars,id,t,id'.
199  id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'.
200#vars #id #t #id' #NE
201whd in ⊢ (% → %)
202whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ])
203>lookup_add_miss
204[ #H @H | @eq_identifier_elim // #E >E in NE * /2/ ]
205qed.
206
207lemma contract_pair : ∀A,B.∀e:A×B. (let 〈a,b〉 ≝ e in 〈a,b〉) = e.
208#A #B * // qed.
209
210lemma extract_pair : ∀A,B,C,D.  ∀u:A×B. ∀Q:A → B → C×D. ∀x,y.
211((let 〈a,b〉 ≝ u in Q a b) = 〈x,y〉) →
212∃a,b. 〈a,b〉 = u ∧ Q a b = 〈x,y〉.
213#A #B #C #D * #a #b #Q #x #y normalize #E1 %{a} %{b} % try @refl @E1 qed.
214
215include "utilities/extralib.ma". (* for pair_eq1 to work around destruct's excessive normalisation *)
216
217lemma characterise_vars_all : ∀l,f,vars,n.
218  characterise_vars l f = 〈vars,n〉 →
219  ∀i. local_id vars i →
220      Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f).
221#globals #f
222whd in ⊢ (∀_.∀_.??%? → ?)
223elim (fn_params f @ fn_vars f)
224[ #vars #n whd in ⊢ (??%? → ?) #E <(pair_eq1 ?????? E) -E; #i #H @False_ind
225  elim globals in H
226  [ normalize //
227  | * #id #rg #t #IH whd in ⊢ (?%? → ?) #H @IH @(local_id_add_global ???? H)
228  ]
229| * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?) #E #i
230  cases (identifier_eq ? id i)
231  [ #E' <E' #H % @refl
232  | #NE #H whd %2 >(contract_pair var_types nat ?) in E;
233    whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
234    cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?)
235    #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2
236    @(IH m0 n0)
237    [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])) >contract_pair @EQ
238    | 2,4: <(pair_eq1 ?????? EQ2) in H #H' @(local_id_add_miss … H') @NE
239    ]
240  ]
241] qed.
242
243include "Cminor/syntax.ma".
244include "common/Errors.ma".
245
246alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)".
247
248axiom BadlyTypedAccess : String.
249axiom BadLvalue : String.
250axiom MissingField : String.
251
252alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)".
253alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)".
254
255(* XXX: For some reason matita refuses to pick the right one unless forced. *)
256alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,6,0)".
257
258definition translate_unop : type → CLunop → res CMunop ≝
259λty.λop:CLunop.
260  match op with
261  [ Onotbool ⇒ OK ? CMnotbool
262  | Onotint ⇒ OK ? Onotint
263  | Oneg ⇒
264      match ty with
265      [ Tint _ _ ⇒ OK ? Onegint
266      | Tfloat _ ⇒ OK ? Onegf
267      | _ ⇒ Error ? (msg TypeMismatch)
268      ]
269  ].
270
271definition translate_add ≝
272λty1,e1,ty2,e2,ty'.
273let ty1' ≝ typ_of_type ty1 in
274let ty2' ≝ typ_of_type ty2 in
275match classify_add ty1 ty2 with
276[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
277| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
278(* XXX using the integer size for e2 as the offset's size isn't right, because
279   if e2 produces an 8bit value then the true offset might overflow *)
280| add_case_pi ty ⇒
281    match ty2' with
282    [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty))))))
283    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
284    ]
285| add_case_ip ty ⇒
286    match ty1' with
287    [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty))))))
288    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
289    ]
290| add_default ⇒ Error ? (msg TypeMismatch)
291].
292
293definition translate_sub ≝
294λty1,e1,ty2,e2,ty'.
295let ty1' ≝ typ_of_type ty1 in
296let ty2' ≝ typ_of_type ty2 in
297match classify_sub ty1 ty2 with
298[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
299| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
300(* XXX choosing offset sizes? *)
301| sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty))))))
302| sub_case_pp ty ⇒
303    match ty' with (* XXX overflow *)
304    [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty)))))
305    | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *)
306    ]
307| sub_default ⇒ Error ? (msg TypeMismatch)
308].
309
310definition translate_mul ≝
311λty1,e1,ty2,e2,ty'.
312let ty1' ≝ typ_of_type ty1 in
313let ty2' ≝ typ_of_type ty2 in
314match classify_mul ty1 ty2 with
315[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
316| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
317| mul_default ⇒ Error ? (msg TypeMismatch)
318].
319
320definition translate_div ≝
321λty1,e1,ty2,e2,ty'.
322let ty1' ≝ typ_of_type ty1 in
323let ty2' ≝ typ_of_type ty2 in
324match classify_div ty1 ty2 with
325[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
326| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
327| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
328| div_default ⇒ Error ? (msg TypeMismatch)
329].
330
331definition translate_mod ≝
332λty1,e1,ty2,e2,ty'.
333let ty1' ≝ typ_of_type ty1 in
334let ty2' ≝ typ_of_type ty2 in
335match classify_mod ty1 ty2 with
336[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
337| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
338| mod_default ⇒ Error ? (msg TypeMismatch)
339].
340
341definition translate_shr ≝
342λty1,e1,ty2,e2,ty'.
343let ty1' ≝ typ_of_type ty1 in
344let ty2' ≝ typ_of_type ty2 in
345match classify_shr ty1 ty2 with
346[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
347| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
348| shr_default ⇒ Error ? (msg TypeMismatch)
349].
350
351definition translate_cmp ≝
352λc,ty1,e1,ty2,e2,ty'.
353let ty1' ≝ typ_of_type ty1 in
354let ty2' ≝ typ_of_type ty2 in
355match classify_cmp ty1 ty2 with
356[ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2)
357| cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2)
358| cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2)
359| cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2)
360| cmp_default ⇒ Error ? (msg TypeMismatch)
361].
362
363definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝
364λop,ty1,e1,ty2,e2,ty.
365let ty' ≝ typ_of_type ty in
366match op with
367[ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty'
368| Osub ⇒ translate_sub ty1 e1 ty2 e2 ty'
369| Omul ⇒ translate_mul ty1 e1 ty2 e2 ty'
370| Omod ⇒ translate_mod ty1 e1 ty2 e2 ty'
371| Odiv ⇒ translate_div ty1 e1 ty2 e2 ty'
372| Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2)
373| Oor  ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2)
374| Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2)
375| Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2)
376| Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty'
377| Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty'
378| One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty'
379| Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty'
380| Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty'
381| Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty'
382| Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty'
383].
384
385lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e.
386  expr_vars ? e1 P →
387  expr_vars ? e2 P →
388  translate_binop op ty1 e1 ty2 e2 ty = OK ? e →
389  expr_vars ? e P.
390#P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2
391whd in ⊢ (??%? → ?)
392[ cases (classify_add ty1 ty2)
393  [ 3,4: #z ] whd in ⊢ (??%? → ?)
394  [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
395    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
396    whd in c:(??%?); destruct % [ @H1 | % // @H2 ]
397  | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
398    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
399    whd in c:(??%?); destruct % [ @H2 | % // @H1 ]
400  | *: #E destruct (E) % try @H1 @H2
401  ]
402| cases (classify_sub ty1 ty2)
403  [ 3,4: #z] whd in ⊢ (??%? → ?)
404  [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?)
405    * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b))
406    whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I
407  | *: #E destruct (E) % try @H1 try @H2 % // @H2
408  ]
409| cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct
410    % try @H1 @H2
411| cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct
412    % try @H1 @H2
413| cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct
414    % try @H1 @H2
415| 6,7,8,9: #E destruct % try @H1 @H2
416| cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
417| 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2
418] qed.
419
420(* We'll need to implement proper translation of pointers if we really do memory
421   spaces. *)
422definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝
423λr1,r2,P.
424  match r1 return λx.P x → res (P r2) with
425  [ Any ⇒   match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
426  | Data ⇒  match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
427  | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
428  | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
429  | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
430  | Code ⇒  match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ]
431  ].
432
433definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝
434λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e.
435
436notation "hvbox(« term 19 a, break term 19 b»)"
437with precedence 90 for @{ (dp ?? $a $b) }.
438
439lemma sig_ok : ∀A:Type[0]. ∀P:A → Prop. ∀x:Σx:A.P x.
440  P x.
441#A #P * #a #p @p
442qed.
443
444definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝
445λP,ty1,ty2.
446match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with
447[ Tint sz1 sg1 ⇒ λe.
448    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
449    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e)
450    | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e)
451    | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
452    | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint r) e)
453    | _ ⇒ Error ? (msg TypeMismatch)
454    ]
455| Tfloat sz1 ⇒ λe.
456    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
457    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e, ?»
458    | Tfloat sz2 ⇒ OK ? «Op1 ?? Oid e, ?» (* FIXME *)
459    | _ ⇒ Error ? (msg TypeMismatch)
460    ]
461| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
462    match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with
463    [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2) e, ?»
464    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
465    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
466    | _ ⇒ Error ? (msg TypeMismatch)
467    ]
468| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
469    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
470    [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e, ?»
471    | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e
472    | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e
473    | _ ⇒ Error ? (msg TypeMismatch)
474    ]
475| _ ⇒ λ_. Error ? (msg TypeMismatch)
476]. whd @sig_ok qed.
477
478definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝
479λty1,ty2,P,p.
480  do E ← assert_type_eq ty1 ty2;
481  OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p).
482
483definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2).
484* * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
485qed.
486
487definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2).
488* [ #sz1 #sg1 | #r1 | #sz1 ]
489* [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ]
490[ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ]
491  *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
492| *; #P #p @(region_should_eq r1 ?? p)
493| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
494] qed.
495
496
497lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r.
498*
499[ 5: #r #ty #n #r' normalize #E destruct @refl
500| 6: #args #ret #r normalize #E destruct @refl
501| *: normalize #a #b try #c try #d destruct
502  [ cases a in d; normalize; cases b; normalize #E destruct
503  | cases a in c; normalize #E destruct
504  ]
505] qed.
506
507definition bind_eq ≝ λA,B:Type[0]. λf: res A. λg: ∀a:A. f = OK ? a → res B.
508  match f return λx. f = x → ? with
509  [ OK x ⇒ g x
510  | Error msg ⇒ λ_. Error ? msg
511  ] (refl ? f).
512
513notation > "vbox('do' ident v 'as' ident E ← e; break e')" with precedence 40 for @{ bind_eq ?? ${e} (λ${ident v}.λ${ident E}.${e'})}.
514
515let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝
516match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with
517[ Expr ed ty ⇒
518  match ed with
519  [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
520  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
521  | Evar id ⇒
522      do c as E ← lookup' vars id;
523      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
524      [ Global r ⇒ λ_.
525          match access_mode ty with
526          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?»
527          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
528          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
529          ]
530      | Stack n ⇒ λE.
531          match access_mode ty with
532          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
533          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
534          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
535          ]
536      | Local ⇒ λE. OK ? «Id ? id, ?»
537      ] E
538  | Ederef e1 ⇒
539      do e1' ← translate_expr vars e1;
540      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
541      [ ASTptr r ⇒ λe1'.
542          match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with
543          [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (eject … e1'), ?»
544          | By_reference r' ⇒ λE. do e1' ← region_should_eq r r' ? e1';
545                                  OK ? e1'⌈Σe':CMexpr ?. expr_vars ? e' (local_id vars) ↦ Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)⌉
546          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
547          ] (access_mode_typ ty)
548      | _ ⇒ λ_. Error ? (msg TypeMismatch)
549      ] e1'
550  | Eaddrof e1 ⇒
551      do e1' ← translate_addr vars e1;
552      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
553      [ ASTptr r ⇒
554          match e1' with
555          [ dp r1 e1' ⇒ region_should_eq r1 r ? e1'
556          ]
557      | _ ⇒ Error ? (msg TypeMismatch)
558      ]
559  | Eunop op e1 ⇒
560      do op' ← translate_unop ty op;
561      do e1' ← translate_expr vars e1;
562      OK ? «Op1 ?? op' e1', ?»
563  | Ebinop op e1 e2 ⇒
564      do e1' ← translate_expr vars e1;
565      do e2' ← translate_expr vars e2;
566      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
567      OK ? «e', ?»
568  | Ecast ty1 e1 ⇒
569      do e1' ← translate_expr vars e1;
570      do e' ← translate_cast ? (typeof e1) ty1 e1';
571      do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e';
572      OK ? e'
573  | Econdition e1 e2 e3 ⇒
574      do e1' ← translate_expr vars e1;
575      do e2' ← translate_expr vars e2;
576      do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
577      do e3' ← translate_expr vars e3;
578      do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3';
579      match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with
580      [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?»
581      | _ ⇒ λ_.Error ? (msg TypeMismatch)
582      ] e1'
583  | Eandbool e1 e2 ⇒
584      do e1' ← translate_expr vars e1;
585      do e2' ← translate_expr vars e2;
586      match ty with
587      [ Tint sz _ ⇒
588        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
589        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with
590        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?))), ?»
591        | _ ⇒ λ_.Error ? (msg TypeMismatch)
592        ] e1'
593      | _ ⇒ Error ? (msg TypeMismatch)
594      ]
595  | Eorbool e1 e2 ⇒
596      do e1' ← translate_expr vars e1;
597      do e2' ← translate_expr vars e2;
598      match ty with
599      [ Tint sz _ ⇒
600        do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
601        match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with
602        [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2', ?»
603        | _ ⇒ λ_.Error ? (msg TypeMismatch)
604        ] e1'
605      | _ ⇒ Error ? (msg TypeMismatch)
606      ]
607  | Esizeof ty1 ⇒
608      match ty with
609      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
610      | _ ⇒ Error ? (msg TypeMismatch)
611      ]
612  | Efield e1 id ⇒
613      match typeof e1 with
614      [ Tstruct _ fl ⇒
615          do e1' ← translate_addr vars e1;
616          match e1' with
617          [ dp r e1' ⇒
618            do off ← field_offset id fl;
619            match access_mode ty with
620            [ By_value q ⇒ OK ? «Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))),?»
621            | By_reference _ ⇒ OK ? «Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))),?»
622            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
623            ]
624          ]
625      | Tunion _ _ ⇒
626          do e1' ← translate_addr vars e1;
627          match e1' with
628          [ dp r e1' ⇒
629            match access_mode ty return λx. access_mode ty = x → res ? with
630            [ By_value q ⇒ λ_. OK ? «Mem ?? q e1', ?»
631            | By_reference r' ⇒  λE. do e1' ← region_should_eq r r' ? e1';
632                                OK ? e1'⌈Σz:CMexpr (ASTptr r').? ↦ Σz:CMexpr (typ_of_type ty).?⌉
633            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
634            ] (refl ? (access_mode ty))
635          ]
636      | _ ⇒ Error ? (msg BadlyTypedAccess)
637      ]
638  | Ecost l e1 ⇒
639      do e1' ← translate_expr vars e1;
640      do e' ← OK ? «Ecost ? l e1',?»;
641      typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e'
642  ]
643] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
644match e with
645[ Expr ed _ ⇒
646  match ed with
647  [ Evar id ⇒
648      do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
649      match c return λ_. res (Σr.Σz:CMexpr (ASTptr r).?) with
650      [ Global r ⇒ OK ? «r, «Cst ? (Oaddrsymbol id 0), ?»»
651      | Stack n ⇒ OK ? «Any, «Cst ? (Oaddrstack n), ?»»
652      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
653      ]
654  | Ederef e1 ⇒
655      do e1' ← translate_expr vars e1;
656      match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (Σr. Σz:CMexpr (ASTptr r). ?) with
657      [ ASTptr r ⇒ λe1'.OK ? «r, e1'»
658      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
659      ] e1'
660  | Efield e1 id ⇒
661      match typeof e1 with
662      [ Tstruct _ fl ⇒
663          do e1' ← translate_addr vars e1;
664          do off ← field_offset id fl;
665          match e1' with
666          [ dp r e1'' ⇒ OK (Σr:region.Σe:CMexpr (ASTptr r).?) («r, «Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1'' (Cst ? (Ointconst I32 (repr ? off))), ?» »)
667          ]
668      | Tunion _ _ ⇒ translate_addr vars e1
669      | _ ⇒ Error ? (msg BadlyTypedAccess)
670      ]
671  | _ ⇒ Error ? (msg BadLvalue)
672  ]
673].
674whd try @I
675[ >E @I
676| >(E ? (refl ??)) @refl
677| 3,4: @sig_ok
678| @(translate_binop_vars … E) @sig_ok
679| % [ % ] @sig_ok
680| % [ % @sig_ok ] whd @I
681| % [ % [ @sig_ok | @I ] | @sig_ok ]
682| % [ @sig_ok | @I ]
683| % [ @sig_ok | @I ]
684| >(access_mode_typ … E) @refl
685| @sig_ok
686| @sig_ok
687| % [ @sig_ok | @I ]
688] qed.
689
690inductive destination (vars:var_types) : Type[0] ≝
691| IdDest : ∀id:ident. local_id vars id → destination vars
692| MemDest : ∀r:region. memory_chunk → (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars.
693
694definition translate_dest ≝
695λvars,e1,ty2.
696    do q ← match access_mode ty2 with
697           [ By_value q ⇒ OK ? q
698           | By_reference r ⇒ OK ? (Mpointer r)
699           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
700           ];
701    match e1 with
702    [ Expr ed1 ty1 ⇒
703        match ed1 with
704        [ Evar id ⇒
705            do c as E ← lookup' vars id;
706            match c return λx.? → ? with
707            [ Local ⇒ λE. OK ? (IdDest vars id ?)
708            | Global r ⇒ λE. OK ? (MemDest ? r q (Cst ? (Oaddrsymbol id 0)))
709            | Stack n ⇒ λE. OK ? (MemDest ? Any q (Cst ? (Oaddrstack n)))
710            ] E
711        | _ ⇒
712            do e1' ← translate_addr vars e1;
713            match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ]
714        ]
715    ].
716whd // >E @I
717qed.
718(*
719definition translate_assign ≝
720λvars,e1,e2.
721    do e2' ← translate_expr vars e2;
722    do q ← match access_mode (typeof e2) with
723           [ By_value q ⇒ OK ? q
724           | By_reference r ⇒ OK ? (Mpointer r)
725           | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
726           ];
727    match e1 with
728    [ Expr ed1 ty1 ⇒
729        match ed1 with
730        [ Evar id ⇒
731            do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id);
732            match c with
733            [ Local ⇒ OK ? (St_assign id e2')
734            | Global ⇒ OK ? (St_store q (Cst (Oaddrsymbol id zero)) e2')
735            | Stack n ⇒ OK ? (St_store q (Cst (Oaddrstack (repr n))) e2')
736            ]
737        | _ ⇒
738            do e1' ← translate_addr vars e1;
739            OK ? (St_store q e1' e2')
740        ]
741    ].
742*)
743
744definition lenv ≝ identifier_map SymbolTag (identifier Label).
745
746definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l.
747
748let rec labels_defined (s:statement) : list ident ≝
749match s with
750[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
751| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
752| Swhile _ s ⇒ labels_defined s
753| Sdowhile _ s ⇒ labels_defined s
754| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
755| Sswitch _ ls ⇒ labels_defined_switch ls
756| Slabel l s ⇒ l::(labels_defined s)
757| Scost _ s ⇒ labels_defined s
758| _ ⇒ [ ]
759]
760and labels_defined_switch (ls:labeled_statements) : list ident ≝
761match ls with
762[ LSdefault s ⇒ labels_defined s
763| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
764].
765
766definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
767
768axiom MissingLabel : String.
769
770definition lookup_label ≝
771λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
772
773definition labels_translated : lenv → statement → stmt → Prop ≝
774λlbls,s,s'.  ∀l.
775  (Exists ? (λl'.l' = l) (labels_defined s)) →
776  ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'.
777
778definition stmt_inv ≝
779λvars. λlbls:lenv.
780  stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s).
781
782definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝
783λvars,e1,e2.
784do e2' ← translate_expr vars e2;
785do dest ← translate_dest vars e1 (typeof e2);
786match dest with
787[ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
788| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
789].
790#ls whd %
791[ % // @sig_ok
792| @I
793| % @sig_ok
794| @I
795] qed.
796
797definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
798λA,B,f,oa.
799match oa with
800[ None ⇒ OK ? (None ?)
801| Some a ⇒ do b ← f a; OK ? (Some ? b)
802].
803
804definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(Σt:typ.CMexpr t). match e with [ dp t e ⇒ expr_vars t e (local_id vars) ]) ≝
805λv,e.
806  do e' ← translate_expr v e;
807  OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?».
808whd @sig_ok
809qed.
810
811axiom FIXME : String.
812
813let rec mmap_sigma (A,B:Type[0]) (P:B → Prop) (f:A → res (Σx:B.P x)) (l:list A) on l : res (Σl':list B.All B P l') ≝
814match l with
815[ nil ⇒ OK ? «nil B, ?»
816| cons h t ⇒
817    do h' ← f h;
818    do t' ← mmap_sigma A B P f t;
819    OK ? «cons B h' t', ?»
820].
821whd // %
822[ @(sig_ok B P)
823| cases t' #l' #p @p
824] qed.
825
826lemma lookup_label_hit : ∀lbls,l,l'.
827  lookup_label lbls l = OK ? l' →
828  lpresent lbls l'.
829#lbls #l #l' whd in ⊢ (??%? → %) #E %{l} cases (lookup ??? l) in E ⊢ %
830normalize #x try #y destruct /2/
831qed.
832
833definition trans_inv : var_types → lenv → statement → stmt → Prop ≝
834λvars,lbls,s,s'. stmt_inv vars lbls s' ∧ labels_translated lbls s s'.
835
836lemma trans_inv_stmt_inv : ∀vars,lbls,s,s'.
837  trans_inv vars lbls s s' → stmt_inv vars lbls s'.
838#var #lbls #s #s' * //
839qed.
840
841lemma trans_inv_labels : ∀vars,lbls,s,s'.
842  trans_inv vars lbls s s' → labels_translated lbls s s'.
843#vars #lbls #s #s' @proj2
844qed.
845
846lemma Exists_append : ∀A,P,l1,l2.
847  Exists A P (l1@l2) →
848  Exists A P l1 ∨ Exists A P l2.
849#A #P #l1 elim l1
850[ #l2 #H %2 @H
851| #h #t #IH #l2 whd in ⊢ (% → ?) *
852  [ #H %1 %1 @H
853  | #H cases (IH l2 H) /4/
854  ]
855] qed.
856
857lemma Exists_append_l : ∀A,P,l1,l2.
858  Exists A P l1 → Exists A P (l1@l2).
859#A #P #l1 #l2 elim l1
860[ *
861| #h #t #IH *
862  [ #H %1 @H
863  | #H %2 @IH @H
864  ]
865] qed.
866
867lemma Exists_append_r : ∀A,P,l1,l2.
868  Exists A P l2 → Exists A P (l1@l2).
869#A #P #l1 #l2 elim l1
870[ #H @H
871| #h #t #IH #H %2 @IH @H
872] qed.
873
874
875let rec translate_statement (vars:var_types) (lbls:lenv) (tmp:Σi:ident.local_id vars i) (tmpp:Σi:ident.local_id vars i) (s:statement) on s : res (Σs':stmt.trans_inv vars lbls s s') ≝
876match s return λs.res (Σs':stmt.trans_inv vars lbls s s') with
877[ Sskip ⇒ OK ? «St_skip, ?»
878| Sassign e1 e2 ⇒
879    do s' ← translate_assign vars e1 e2;
880    OK ? «eject ?? s', ?»
881| Scall ret ef args ⇒
882    do ef' ← translate_expr vars ef;
883    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
884    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
885    match ret with
886    [ None ⇒ OK ? «St_call (None ?) ef' args', ?»
887    | Some e1 ⇒
888        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
889        match dest with
890        [ IdDest id p ⇒ OK ? «St_call (Some ? id) ef' args', ?»
891        | MemDest r q e1' ⇒
892            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
893            OK ? «St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), ?»
894        ]
895    ]
896| Ssequence s1 s2 ⇒
897    do s1' ← translate_statement vars lbls tmp tmpp s1;
898    do s2' ← translate_statement vars lbls tmp tmpp s2;
899    OK ? «St_seq s1' s2', ?»
900| Sifthenelse e1 s1 s2 ⇒
901    do e1' ← translate_expr vars e1;
902    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
903    [ ASTint _ _ ⇒ λe1'.
904        do s1' ← translate_statement vars lbls tmp tmpp s1;
905        do s2' ← translate_statement vars lbls tmp tmpp s2;
906        OK ? «St_ifthenelse ?? e1' s1' s2', ?»
907    | _ ⇒ λ_.Error ? (msg TypeMismatch)
908    ] e1'
909| Swhile e1 s1 ⇒
910    do e1' ← translate_expr vars e1;
911    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
912    [ ASTint _ _ ⇒ λe1'.
913        do s1' ← translate_statement vars lbls tmp tmpp s1;
914        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
915        OK ? «St_block
916               (St_loop
917                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), ?»
918    | _ ⇒ λ_.Error ? (msg TypeMismatch)
919    ] e1'
920| Sdowhile e1 s1 ⇒
921    do e1' ← translate_expr vars e1;
922    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
923    [ ASTint _ _ ⇒ λe1'.
924        do s1' ← translate_statement vars lbls tmp tmpp s1;
925        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
926        OK ? «St_block
927               (St_loop
928                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), ?»
929    | _ ⇒ λ_.Error ? (msg TypeMismatch)
930    ] e1'
931| Sfor s1 e1 s2 s3 ⇒
932    do e1' ← translate_expr vars e1;
933    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
934    [ ASTint _ _ ⇒ λe1'.
935        do s1' ← translate_statement vars lbls tmp tmpp s1;
936        do s2' ← translate_statement vars lbls tmp tmpp s2;
937        do s3' ← translate_statement vars lbls tmp tmpp s3;
938        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
939        OK ? «St_seq s1'
940             (St_block
941               (St_loop
942                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), ?»
943    | _ ⇒ λ_.Error ? (msg TypeMismatch)
944    ] e1'
945| Sbreak ⇒ OK ? «St_exit 1, ?»
946| Scontinue ⇒ OK ? «St_exit 0, ?»
947| Sreturn ret ⇒
948    match ret with
949    [ None ⇒ OK ? «St_return (None ?), ?»
950    | Some e1 ⇒
951        do e1' ← translate_expr vars e1;
952        OK ? «St_return (Some ? (dp … e1')), ?»
953    ]
954| Sswitch e1 ls ⇒ Error ? (msg FIXME)
955| Slabel l s1 ⇒
956    do l' as E ← lookup_label lbls l;
957    do s1' ← translate_statement vars lbls tmp tmpp s1;
958    OK ? «St_label l' s1', ?»
959| Sgoto l ⇒
960    do l' as E ← lookup_label lbls l;
961    OK ? «St_goto l', ?»
962| Scost l s1 ⇒
963    do s1' ← translate_statement vars lbls tmp tmpp s1;
964    OK ? «St_cost l s1', ?»
965].
966try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
967try @I
968try @(trans_inv_stmt_inv ???? (sig_ok ? (λs.trans_inv ??? s) …))
969try @(sig_ok ? (λs.stmt_inv ?? s))
970try @(sig_ok ? (λe.expr_vars ? e ?))
971try @(sig_ok ? (λs.stmt_vars ?? s))
972try @(sig_ok ? (λs.stmt_labels ?? s))
973try @(sig_ok ? (All ??))
974try @(sig_ok ? (local_id vars))
975try @(lookup_label_hit … E)
976[ 1,3,5,6,7,13,14,15,16,18: whd #l *
977| @(sig_ok ?? s')
978| @p
979| #l #H cases (Exists_append … H)
980  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
981    %{l'} % [ @E1 | @Exists_append_l @D1 ]
982  | #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
983    %{l'} % [ @E2 | @Exists_append_r @D2 ]
984  ]
985| #l #H cases (Exists_append … H)
986  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
987    %{l'} % [ @E1 | @Exists_append_l @D1 ]
988  | #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
989    %{l'} % [ @E2 | @Exists_append_r @D2 ]
990  ]
991| cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1
992  %{l'} % [ @E1 | @Exists_append_l @D1 ]
993| cases s1' #s1' * #S1 #L1 #l #H cases (L1 l H) #l' * #E1 #D1
994  %{l'} % [ @E1 | @Exists_append_l @D1 ]
995| #l #H cases (Exists_append … H)
996  [ #H1 cases s1' #s1' * #S1 #L1 cases (L1 l H1) #l' * #E1 #D1
997    %{l'} % [ @E1 | @Exists_append_l @D1 ]
998  | #H cases (Exists_append … H)
999    [ #H2 cases s2' #s2' * #S2 #L2 cases (L2 l H2) #l' * #E2 #D2
1000      %{l'} % [ @E2 | @Exists_append_r @Exists_append_l @Exists_append_r @D2 ]
1001    | #H3 cases s3' #s3' * #S3 #L3 cases (L3 l H3) #l' * #E3 #D3
1002      %{l'} % [ @E3 | @Exists_append_r @Exists_append_l @Exists_append_l @D3 ]
1003    ]
1004  ]
1005| cases s1' #s1' * #S1 #L1 #l0 *
1006  [ #El <El %{l'} >E % [ @refl | %1 @refl ]
1007  | #H cases (L1 l0 H) #l0' * #E1 #D1
1008    %{l0'} % [ @E1 | %2 @D1 ]
1009  ]
1010| cases s1' #s1' * #S1 #L1 @L1
1011] qed.
1012
1013
1014axiom ParamGlobalMixup : String.
1015
1016(* ls and s0 aren't real parameters, they're just there for giving the invariant. *)
1017definition alloc_params : ∀vars:var_types.∀ls,s0. list (ident×type) → (Σs:stmt. trans_inv vars ls s0 s) → res (Σs:stmt.trans_inv vars ls s0 s) ≝
1018λvars,ls,s0,params,s. foldl ?? (λs,it.
1019  let 〈id,ty〉 ≝ it in
1020  do s ← s;
1021  do t as E ← lookup' vars id;
1022  match t return λx.? → ? with
1023  [ Local ⇒ λE. OK (Σs:stmt.?) s
1024  | Stack n ⇒ λE.
1025      do q ← match access_mode ty with
1026      [ By_value q ⇒ OK ? q
1027      | By_reference r ⇒ OK ? (Mpointer r)
1028      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
1029      ];
1030      OK ? «St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, ?»
1031  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
1032  ] E) (OK ? s) params.
1033try @conj try @conj try @conj try @conj try @conj
1034try @I
1035[ whd >E @I
1036| @(trans_inv_stmt_inv … s0) @(sig_ok … s)
1037| cases s #s * #S #L @L
1038] qed.
1039
1040definition bigid1 ≝ an_identifier SymbolTag [[
1041false;true;false;false;
1042false;false;false;false;
1043false;false;false;false;
1044false;false;false;false]].
1045definition bigid2 ≝ an_identifier SymbolTag [[
1046false;true;false;false;
1047false;false;false;false;
1048false;false;false;false;
1049false;false;false;true]].
1050
1051lemma Exists_rm : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
1052#A #P #l1 #x #l2 elim l1
1053[ normalize #H %2 @H
1054| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
1055qed.
1056
1057lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
1058#A #P #l1 #x #l2 #H elim l1
1059[ %1 @H
1060| #h #t #IH %2 @IH
1061] qed.
1062
1063lemma Exists_map : ∀A,B,P,Q,f,l.
1064Exists A P l →
1065(∀a.P a → Q (f a)) →
1066Exists B Q (map A B f l).
1067#A #B #P #Q #f #l elim l //
1068#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
1069
1070notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
1071 with precedence 10
1072for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
1073        λ${ident E}.$s ] (refl ? $t) }.
1074
1075lemma local_id_add_local : ∀vars,id,id'.
1076  local_id vars id →
1077  local_id (add ?? vars id' Local) id.
1078#vars #id #id' #H
1079whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
1080[ #E < E >lookup_add_hit //
1081| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
1082] qed.
1083
1084definition lenv_inv : lenv → lenv → statement → Prop ≝
1085λlbls0,lbls,s. (∀l. Exists ? (λl'. l' = l) (labels_defined s) → ∃lm. lookup_label lbls l = OK ? lm) ∧
1086  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
1087
1088definition lenv_inv_switch : lenv → lenv → labeled_statements → Prop ≝
1089λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) (labels_defined_switch ls) → ∃lm. lookup_label lbls l = OK ? lm) ∧
1090  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
1091
1092axiom DuplicateLabel : String.
1093(*
1094(* We only record labels from Slabel, not Sgoto, so that we detect badly formed
1095   programs.  The gratutitous let-in expansion is so that Russell generated
1096   nice hypotheses for us. *)
1097let rec extend_label_env (s:statement) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) ≝
1098match s return λs.res (Σx:lenv × (universe ?). lenv_inv (\fst lu0) (\fst x) s) with
1099[ Ssequence s1 s2 ⇒
1100    do lu1 ← extend_label_env s1 lu0;
1101    do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»
1102| Sifthenelse _ s1 s2 ⇒
1103    do lu1 ← extend_label_env s1 lu0;
1104    do lu2 ← extend_label_env s2 lu1; OK ? «eject … lu2, ?»
1105| Swhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
1106| Sdowhile _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
1107| Sfor s1 _ s2 s3 ⇒
1108    do lu1 ← extend_label_env s1 lu0;
1109    do lu2 ← extend_label_env s2 lu1;
1110    do lu3 ← extend_label_env s3 lu2; OK ? «eject … lu3, ?»
1111| Sswitch _ ls ⇒ do lu ← extend_label_env' ls lu0; OK ? «eject … lu, ?»
1112| Slabel l s ⇒
1113    let 〈lbls, u〉 ≝ lu0 in
1114    match lookup_label lbls l with
1115    [ OK _ ⇒ Error ? (msg DuplicateLabel)
1116    | Error _ ⇒
1117        let 〈l',u〉 ≝ fresh ? u in
1118        do lu ← extend_label_env s 〈add … lbls l l', u〉; OK ? «eject … lu, ?»
1119    ]
1120| Scost _ s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
1121| _ ⇒ OK ? «lu0, ?»
1122]
1123and extend_label_env' (ls:labeled_statements) (lu0:lenv×(universe ?)) : res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) ≝
1124match ls return λls.res (Σx:lenv × (universe ?). lenv_inv_switch (\fst lu0) (\fst x) ls) with
1125[ LSdefault s ⇒ do lu ← extend_label_env s lu0; OK ? «eject … lu, ?»
1126| LScase _ _ s ls ⇒
1127    do lu1 ← extend_label_env s lu0;
1128    do lu2 ← extend_label_env' ls lu1; OK ? «eject … lu2, ?»
1129]. @conj
1130[ 1,3,5,17,19,21,27: #l *
1131| 2,4,6,18,20,22,28: #l #l' #H @H
1132| cases lu1 in lu2 ⊢ % * #lbls1 #u1 * #I1 #E1 * * #lbls2 #u2 * #I2 #E2 whd in E2:(∀_.∀_.??(?%?)? → ?) ⊢ (∀_.? → ??(λ_.??(?%?)?))
1133  #l #H cases (Exists_append … H)
1134  [ #H1 cases (I1 l H1) #l' #L1 %{l'} @E2 @L1
1135  | #H2 cases (I2 l H2) #l' #L2 %{l'} @L2
1136  ]
1137
1138definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?).
1139*)
1140
1141definition lenv_list_inv : lenv → lenv → list ident → Prop ≝
1142λlbls0,lbls,ls. (∀l. Exists ? (λl'. l' = l) ls → ∃lm. lookup_label lbls l = OK ? lm) ∧
1143  ∀l,l'. lookup_label lbls0 l = OK ? l' → lookup_label lbls l = OK ? l'.
1144
1145lemma lookup_label_add : ∀lbls,l,l'.
1146  lookup_label (add … lbls l l') l = OK ? l'.
1147#lbls #l #l' whd in ⊢ (??%?) >lookup_add_hit @refl
1148qed.
1149
1150lemma lookup_label_new : ∀lbls,l,l',msg,l0,l0'.
1151  lookup_label lbls l = Error ? msg →
1152  lookup_label lbls l0 = OK ? l0' →
1153  lookup_label (add … lbls l l') l0 = OK ? l0'.
1154#lbls #l #l' #msg #l0 #l0' #E1 #E2
1155whd in ⊢ (??%%)
1156>lookup_add_miss
1157[ @E2 | @(eq_identifier_elim ?? l0 l) // #E >E in E2 >E1 #X destruct ]
1158qed. 
1159
1160let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝
1161match ls return λls. res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) with
1162[ nil ⇒ OK ? «lbls, ?»
1163| cons l t ⇒
1164    match lookup_label lbls l return λx.lookup_label lbls l = x → ? with
1165    [ OK _ ⇒ λ_. Error ? (msg DuplicateLabel)
1166    | Error _ ⇒ λLOOK.
1167        let 〈l',u1〉 ≝ fresh … u in
1168        do lbls1 ← populate_lenv t (add … lbls l l') u1;
1169        OK ? «eject … lbls1, ?»
1170    ] (refl ? (lookup_label lbls l))
1171]. @conj
1172[  #l *
1173| #l #l' #H @H
1174| cases lbls1 #lbls' * #E1 #E2 whd in ⊢ (∀_.?→??(λ_.??(?%?)?)) #l0 *
1175  [ #E <E %{l'} @E2 @lookup_label_add
1176  | @E1
1177  ]
1178| cases lbls1 #lbls' * #E1 #E2 #l1 #l2 #L whd in ⊢ (??(?%?)?)
1179  @E2 @(lookup_label_new … LOOK L)
1180] qed.
1181
1182definition build_label_env : ∀body:statement. res (Σlbls:lenv. ∀l.Exists ? (λl'.l' = l) (labels_defined body) → ∃l'.lookup_label lbls l = OK ? l') ≝
1183λbody.
1184  do lbls ← populate_lenv (labels_defined body) (empty_map ??) (new_universe ?);
1185  OK ? «eject … lbls, ?».
1186cases lbls #lbls * #E1 #E2 @E1
1187qed.
1188
1189notation > "vbox('do' « ident v , ident p » ← e; break e')" with precedence 40
1190  for @{ bind ?? ${e} (λ${fresh x}.match ${fresh x} with [ dp ${ident v} ${ident p} ⇒ ${e'} ]) }.
1191
1192(* FIXME: the temporary handling is nonsense, I'm afraid. *)
1193definition translate_function : list (ident×region) → function → res internal_function ≝
1194λglobals, f.
1195  do «lbls, Ilbls» ← build_label_env (fn_body f);
1196  let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in
1197  let tmp ≝ bigid1 in (* FIXME *)
1198  let tmpp ≝ bigid2 in (* FIXME *)
1199  let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in
1200  do s ← translate_statement vartypes lbls tmp tmpp (fn_body f);
1201  do «s,Is» ← alloc_params vartypes lbls ? (fn_params f) s;
1202  OK ? (mk_internal_function
1203    (opttyp_of_type (fn_return f))
1204    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
1205    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
1206    stacksize
1207    s ?).
1208[ cases Is #S #L
1209  @(stmt_P_mp ???? S)
1210  #s1 * #H1 #H2 %
1211  [ @(stmt_vars_mp … H1)
1212    #i #H cases (identifier_eq ? tmp i)
1213    [ #E <E @Exists_mid @refl
1214    | #NE1 @Exists_rm cases (identifier_eq ? tmpp i)
1215      [ #E <E @Exists_mid @refl
1216      | #NE2 @Exists_rm
1217        >map_append
1218        @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
1219                         @(local_id_add_miss ?? Local ? NE1)
1220                         @(local_id_add_miss ?? Local ? NE2) @H
1221                    | skip
1222                    | * #id #ty #E1 <E1 @refl
1223                    ]
1224      ]
1225    ]
1226  | @(stmt_labels_mp … H2)
1227    #l * #l' #LOOKUP
1228   
1229     generalize in ⊢ (???(?(???(????%))))
1230    * #S #L
1231| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
1232| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
1233
1234] qed.
1235
1236definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
1237λglobals,f.
1238match f with
1239[ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
1240| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
1241].
1242
1243definition clight_to_cminor : clight_program → res Cminor_program ≝
1244λp.
1245  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
1246  let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
1247  let globals ≝ fun_globals @ var_globals in
1248  transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
Note: See TracBrowser for help on using the repository browser.