source: src/Clight/toCminor.ma @ 1515

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

Add type of maps on positive binary numbers, and use them for identifers.

Also:

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