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

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

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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