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

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

Checkpoint part way through adding proper C label checking to the branch.

File size: 46.6 KB
RevLine 
[816]1
2include "Clight/Csyntax.ma".
[880]3include "Clight/TypeComparison.ma".
[816]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
[961]143| LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪
144                      gather_mem_vars_ls ls1
[816]145].
146
147inductive var_type : Type[0] ≝
[881]148| Global : region → var_type
[816]149| Stack  : nat → var_type
150| Local  : var_type
151.
152
153definition var_types ≝ identifier_map SymbolTag var_type.
154
[1087]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
[816]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
[881]176definition characterise_vars : list (ident×region) → function → var_types × nat ≝
[816]177λglobals, f.
[1087]178  let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in
[816]179  let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in
[1087]180  let 〈m,stacksize〉 ≝ foldr ?? (λv,ms.
[816]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
[1078]186      〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in
[816]187  〈m,stacksize〉.
188
[1087]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.
[816]197
[1087]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
[816]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 ≝
[880]272λty1,e1,ty2,e2,ty'.
273let ty1' ≝ typ_of_type ty1 in
274let ty2' ≝ typ_of_type ty2 in
[816]275match classify_add ty1 ty2 with
[880]276[ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2)
277| add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2)
[961]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    ]
[816]290| add_default ⇒ Error ? (msg TypeMismatch)
291].
292
293definition translate_sub ≝
[880]294λty1,e1,ty2,e2,ty'.
295let ty1' ≝ typ_of_type ty1 in
296let ty2' ≝ typ_of_type ty2 in
[816]297match classify_sub ty1 ty2 with
[880]298[ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2)
299| sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2)
[961]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    ]
[816]307| sub_default ⇒ Error ? (msg TypeMismatch)
308].
309
310definition translate_mul ≝
[880]311λty1,e1,ty2,e2,ty'.
312let ty1' ≝ typ_of_type ty1 in
313let ty2' ≝ typ_of_type ty2 in
[816]314match classify_mul ty1 ty2 with
[880]315[ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2)
316| mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2)
[816]317| mul_default ⇒ Error ? (msg TypeMismatch)
318].
319
320definition translate_div ≝
[880]321λty1,e1,ty2,e2,ty'.
322let ty1' ≝ typ_of_type ty1 in
323let ty2' ≝ typ_of_type ty2 in
[816]324match classify_div ty1 ty2 with
[961]325[ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2)
[880]326| div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2)
327| div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2)
[816]328| div_default ⇒ Error ? (msg TypeMismatch)
329].
330
331definition translate_mod ≝
[880]332λty1,e1,ty2,e2,ty'.
333let ty1' ≝ typ_of_type ty1 in
334let ty2' ≝ typ_of_type ty2 in
[816]335match classify_mod ty1 ty2 with
[961]336[ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2)
[880]337| mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2)
[816]338| mod_default ⇒ Error ? (msg TypeMismatch)
339].
340
341definition translate_shr ≝
[880]342λty1,e1,ty2,e2,ty'.
343let ty1' ≝ typ_of_type ty1 in
344let ty2' ≝ typ_of_type ty2 in
[816]345match classify_shr ty1 ty2 with
[961]346[ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2)
[880]347| shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2)
[816]348| shr_default ⇒ Error ? (msg TypeMismatch)
349].
350
351definition translate_cmp ≝
[880]352λc,ty1,e1,ty2,e2,ty'.
353let ty1' ≝ typ_of_type ty1 in
354let ty2' ≝ typ_of_type ty2 in
[816]355match classify_cmp ty1 ty2 with
[880]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)
[816]360| cmp_default ⇒ Error ? (msg TypeMismatch)
361].
362
[880]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
[816]366match op with
[880]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'
[816]383].
384
[1087]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.
[880]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
[1087]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.
[880]435
[1087]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
[880]447[ Tint sz1 sg1 ⇒ λe.
[1087]448    match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with
[962]449    [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e)
[880]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)
[816]453    | _ ⇒ Error ? (msg TypeMismatch)
454    ]
[880]455| Tfloat sz1 ⇒ λe.
[1087]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 *)
[816]459    | _ ⇒ Error ? (msg TypeMismatch)
460    ]
[880]461| Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *)
[1087]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
[816]466    | _ ⇒ Error ? (msg TypeMismatch)
467    ]
[880]468| Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *)
[1087]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
[816]473    | _ ⇒ Error ? (msg TypeMismatch)
474    ]
[880]475| _ ⇒ λ_. Error ? (msg TypeMismatch)
[1087]476]. whd @sig_ok qed.
[816]477
[880]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
[881]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
[880]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))
[881]492| *; #P #p @(region_should_eq r1 ?? p)
[880]493| *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch))
494] qed.
495
[881]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
[1087]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
[816]517[ Expr ed ty ⇒
518  match ed with
[1087]519  [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?»
520  | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?»
[816]521  | Evar id ⇒
[1087]522      do c as E ← lookup' vars id;
523      match c return λx.? = ? → res (Σe':CMexpr ?. ?) with
524      [ Global r ⇒ λ_.
[816]525          match access_mode ty with
[1087]526          [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?»
527          | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?»
[816]528          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
529          ]
[1087]530      | Stack n ⇒ λE.
[816]531          match access_mode ty with
[1087]532          [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?»
533          | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?»
[816]534          | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
535          ]
[1087]536      | Local ⇒ λE. OK ? «Id ? id, ?»
537      ] E
[816]538  | Ederef e1 ⇒
539      do e1' ← translate_expr vars e1;
[1087]540      match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with
[881]541      [ ASTptr r ⇒ λe1'.
[1087]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)⌉
[881]546          | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
[1087]547          ] (access_mode_typ ty)
[881]548      | _ ⇒ λ_. Error ? (msg TypeMismatch)
549      ] e1'
[880]550  | Eaddrof e1 ⇒
551      do e1' ← translate_addr vars e1;
[1087]552      match typ_of_type ty return λx.res (Σz:CMexpr x.?) with
[881]553      [ ASTptr r ⇒
554          match e1' with
555          [ dp r1 e1' ⇒ region_should_eq r1 r ? e1'
556          ]
[880]557      | _ ⇒ Error ? (msg TypeMismatch)
[816]558      ]
559  | Eunop op e1 ⇒
560      do op' ← translate_unop ty op;
561      do e1' ← translate_expr vars e1;
[1087]562      OK ? «Op1 ?? op' e1', ?»
[816]563  | Ebinop op e1 e2 ⇒
564      do e1' ← translate_expr vars e1;
565      do e2' ← translate_expr vars e2;
[1087]566      do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty;
567      OK ? «e', ?»
[816]568  | Ecast ty1 e1 ⇒
569      do e1' ← translate_expr vars e1;
[1087]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'
[816]573  | Econdition e1 e2 e3 ⇒
574      do e1' ← translate_expr vars e1;
575      do e2' ← translate_expr vars e2;
[1087]576      do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2';
[816]577      do e3' ← translate_expr vars e3;
[1087]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', ?»
[880]581      | _ ⇒ λ_.Error ? (msg TypeMismatch)
582      ] e1'
[816]583  | Eandbool e1 e2 ⇒
584      do e1' ← translate_expr vars e1;
585      do e2' ← translate_expr vars e2;
[961]586      match ty with
587      [ Tint sz _ ⇒
[1087]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 ?))), ?»
[961]591        | _ ⇒ λ_.Error ? (msg TypeMismatch)
592        ] e1'
593      | _ ⇒ Error ? (msg TypeMismatch)
594      ]
[816]595  | Eorbool e1 e2 ⇒
596      do e1' ← translate_expr vars e1;
597      do e2' ← translate_expr vars e2;
[961]598      match ty with
599      [ Tint sz _ ⇒
[1087]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', ?»
[961]603        | _ ⇒ λ_.Error ? (msg TypeMismatch)
604        ] e1'
605      | _ ⇒ Error ? (msg TypeMismatch)
606      ]
607  | Esizeof ty1 ⇒
608      match ty with
[1087]609      [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?»
[961]610      | _ ⇒ Error ? (msg TypeMismatch)
611      ]
[816]612  | Efield e1 id ⇒
[1087]613      match typeof e1 with
[816]614      [ Tstruct _ fl ⇒
615          do e1' ← translate_addr vars e1;
[881]616          match e1' with
617          [ dp r e1' ⇒
618            do off ← field_offset id fl;
619            match access_mode ty with
[1087]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))),?»
[881]622            | By_nothing ⇒ Error ? (msg BadlyTypedAccess)
623            ]
[816]624          ]
625      | Tunion _ _ ⇒
626          do e1' ← translate_addr vars e1;
[881]627          match e1' with
628          [ dp r e1' ⇒
[1087]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).?⌉
[881]633            | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess)
634            ] (refl ? (access_mode ty))
[816]635          ]
636      | _ ⇒ Error ? (msg BadlyTypedAccess)
[1087]637      ]
[816]638  | Ecost l e1 ⇒
639      do e1' ← translate_expr vars e1;
[1087]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'
[816]642  ]
[1087]643] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝
[816]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);
[1087]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), ?»»
[1078]652      | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *)
[816]653      ]
[880]654  | Ederef e1 ⇒
655      do e1' ← translate_expr vars e1;
[1087]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'»
[880]658      | _ ⇒ λ_.Error ? (msg BadlyTypedAccess)
659      ] e1'
[816]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;
[881]665          match e1' with
[1087]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))), ?» »)
[881]667          ]
[816]668      | Tunion _ _ ⇒ translate_addr vars e1
669      | _ ⇒ Error ? (msg BadlyTypedAccess)
670      ]
671  | _ ⇒ Error ? (msg BadLvalue)
672  ]
673].
[1087]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.
[816]689
[1087]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.
[816]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 ⇒
[1087]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
[816]711        | _ ⇒
712            do e1' ← translate_addr vars e1;
[1087]713            match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ]
[816]714        ]
715    ].
[1087]716whd // >E @I
717qed.
[816]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*)
[1096]743
744definition lenv ≝ identifier_map SymbolTag (identifier Label).
745
746definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup ?? lbls l' = Some ? l.
747
748definition stmt_inv ≝
749λvars. λlbls:lenv.
750  stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s).
751
752definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝
[816]753λvars,e1,e2.
754do e2' ← translate_expr vars e2;
755do dest ← translate_dest vars e1 (typeof e2);
756match dest with
[1087]757[ IdDest id p ⇒ OK ? «St_assign ? id e2', ?»
758| MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?»
[816]759].
[1096]760#ls whd %
[1087]761[ % // @sig_ok
[1096]762| @I
[1087]763| % @sig_ok
[1096]764| @I
[1087]765] qed.
[816]766
767definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝
768λA,B,f,oa.
769match oa with
770[ None ⇒ OK ? (None ?)
771| Some a ⇒ do b ← f a; OK ? (Some ? b)
772].
773
[1087]774definition 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) ]) ≝
[880]775λv,e.
776  do e' ← translate_expr v e;
[1087]777  OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?».
778whd @sig_ok
779qed.
[880]780
[816]781axiom FIXME : String.
782
[1087]783let 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') ≝
784match l with
785[ nil ⇒ OK ? «nil B, ?»
786| cons h t ⇒
787    do h' ← f h;
788    do t' ← mmap_sigma A B P f t;
789    OK ? «cons B h' t', ?»
790].
791whd // %
792[ @(sig_ok B P)
793| cases t' #l' #p @p
794] qed.
795
[1096]796axiom MissingLabel : String.
797
798definition lookup_label ≝
799λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l).
800
801lemma lookup_label_hit : ∀lbls,l,l'.
802  lookup_label lbls l = OK ? l' →
803  lpresent lbls l'.
804#lbls #l #l' whd in ⊢ (??%? → %) #E %{l} cases (lookup ??? l) in E ⊢ %
805normalize #x try #y destruct /2/
806qed.
807
808let 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.stmt_inv vars lbls s) ≝
[816]809match s with
[1087]810[ Sskip ⇒ OK ? «St_skip, ?»
[1096]811| Sassign e1 e2 ⇒
812    do s' ← translate_assign vars e1 e2;
813    OK ? «eject ?? s', ?»
[816]814| Scall ret ef args ⇒
815    do ef' ← translate_expr vars ef;
[1087]816    do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef';
817    do args' ← mmap_sigma … (translate_expr_sigma vars) args;
[816]818    match ret with
[1087]819    [ None ⇒ OK ? «St_call (None ?) ef' args', ?»
[816]820    | Some e1 ⇒
821        do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *)
822        match dest with
[1087]823        [ IdDest id p ⇒ OK ? «St_call (Some ? id) ef' args', ?»
[881]824        | MemDest r q e1' ⇒
[816]825            let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in
[1087]826            OK ? «St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp)), ?»
[816]827        ]
828    ]
829| Ssequence s1 s2 ⇒
[1096]830    do s1' ← translate_statement vars lbls tmp tmpp s1;
831    do s2' ← translate_statement vars lbls tmp tmpp s2;
[1087]832    OK ? «St_seq s1' s2', ?»
[816]833| Sifthenelse e1 s1 s2 ⇒
834    do e1' ← translate_expr vars e1;
[1087]835    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
[880]836    [ ASTint _ _ ⇒ λe1'.
[1096]837        do s1' ← translate_statement vars lbls tmp tmpp s1;
838        do s2' ← translate_statement vars lbls tmp tmpp s2;
[1087]839        OK ? «St_ifthenelse ?? e1' s1' s2', ?»
[880]840    | _ ⇒ λ_.Error ? (msg TypeMismatch)
841    ] e1'
[816]842| Swhile e1 s1 ⇒
843    do e1' ← translate_expr vars e1;
[1087]844    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with
[880]845    [ ASTint _ _ ⇒ λe1'.
[1096]846        do s1' ← translate_statement vars lbls tmp tmpp s1;
[880]847        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
[1087]848        OK ? «St_block
[880]849               (St_loop
[1087]850                 (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), ?»
[880]851    | _ ⇒ λ_.Error ? (msg TypeMismatch)
852    ] e1'
[816]853| Sdowhile e1 s1 ⇒
854    do e1' ← translate_expr vars e1;
[1087]855    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
[880]856    [ ASTint _ _ ⇒ λe1'.
[1096]857        do s1' ← translate_statement vars lbls tmp tmpp s1;
[880]858        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
[1087]859        OK ? «St_block
[880]860               (St_loop
[1087]861                 (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), ?»
[880]862    | _ ⇒ λ_.Error ? (msg TypeMismatch)
863    ] e1'
[816]864| Sfor s1 e1 s2 s3 ⇒
865    do e1' ← translate_expr vars e1;
[1087]866    match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with
[880]867    [ ASTint _ _ ⇒ λe1'.
[1096]868        do s1' ← translate_statement vars lbls tmp tmpp s1;
869        do s2' ← translate_statement vars lbls tmp tmpp s2;
870        do s3' ← translate_statement vars lbls tmp tmpp s3;
[880]871        (* TODO: this is a little different from the prototype and CompCert, is it OK? *)
[1087]872        OK ? «St_seq s1'
[880]873             (St_block
874               (St_loop
[1087]875                 (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), ?»
[880]876    | _ ⇒ λ_.Error ? (msg TypeMismatch)
877    ] e1'
[1087]878| Sbreak ⇒ OK ? «St_exit 1, ?»
879| Scontinue ⇒ OK ? «St_exit 0, ?»
[816]880| Sreturn ret ⇒
[880]881    match ret with
[1087]882    [ None ⇒ OK ? «St_return (None ?), ?»
[880]883    | Some e1 ⇒
884        do e1' ← translate_expr vars e1;
[1087]885        OK ? «St_return (Some ? (dp … e1')), ?»
[880]886    ]
[816]887| Sswitch e1 ls ⇒ Error ? (msg FIXME)
888| Slabel l s1 ⇒
[1096]889    do l' as E ← lookup_label lbls l;
890    do s1' ← translate_statement vars lbls tmp tmpp s1;
891    OK ? «St_label l' s1', ?»
892| Sgoto l ⇒
893    do l' as E ← lookup_label lbls l;
894    OK ? «St_goto l', ?»
[816]895| Scost l s1 ⇒
[1096]896    do s1' ← translate_statement vars lbls tmp tmpp s1;
[1087]897    OK ? «St_cost l s1', ?»
[816]898].
[1096]899try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj
900try @I
901try @(sig_ok ? (λs.stmt_inv ?? s))
902try @(sig_ok ? (λe.expr_vars ? e ?))
903try @(sig_ok ? (λs.stmt_vars ?? s))
904try @(sig_ok ? (λs.stmt_labels ?? s))
905try @(sig_ok ? (All ??))
906try @(sig_ok ? (local_id vars))
907try @(lookup_label_hit … E)
908[ @(sig_ok ?? s')
909| @p
[1087]910] qed.
[816]911
[1096]912let rec labels_defined (s:statement) : list ident ≝
913match s with
914[ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2
915| Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2
916| Swhile _ s ⇒ labels_defined s
917| Sdowhile _ s ⇒ labels_defined s
918| Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3
919| Sswitch _ ls ⇒ labels_defined_switch ls
920| Slabel l s ⇒ l::(labels_defined s)
921| Scost _ s ⇒ labels_defined s
922| _ ⇒ [ ]
923]
924and labels_defined_switch (ls:labeled_statements) : list ident ≝
925match ls with
926[ LSdefault s ⇒ labels_defined s
927| LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls
928].
929
930lemma OK_sig_eq : ∀A,P,x,xp,y,yp. OK (Σx:A.P x) «x,xp» = OK (Σx:A.P x) «y,yp» → x = y.
931#A #P #x #xp #y #yp #E destruct @refl
932qed.
933
934definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s).
935
936lemma Exists_append : ∀A,P,l1,l2.
937  Exists A P (l1@l2) →
938  Exists A P l1 ∨ Exists A P l2.
939#A #P #l1 elim l1
940[ #l2 #H %2 @H
941| #h #t #IH #l2 whd in ⊢ (% → ?) *
942  [ #H %1 %1 @H
943  | #H cases (IH l2 H) /4/
944  ]
945] qed.
946
947lemma Exists_append_l : ∀A,P,l1,l2.
948  Exists A P l1 → Exists A P (l1@l2).
949#A #P #l1 #l2 elim l1
950[ *
951| #h #t #IH *
952  [ #H %1 @H
953  | #H %2 @IH @H
954  ]
955] qed.
956
957lemma Exists_append_r : ∀A,P,l1,l2.
958  Exists A P l2 → Exists A P (l1@l2).
959#A #P #l1 #l2 elim l1
960[ #H @H
961| #h #t #IH #H %2 @IH @H
962] qed.
963
964lemma reflmatch : ∀A,B,e.∀P:∀v:A. e = OK ? v → res B.∀x.
965 match e return λx.e = x → ? with [ OK v ⇒ P v | Error m ⇒ λ_.Error ? m ] (refl ? e) = OK ? x →
966 ∃v,p. P v p = OK ? x.
967#A #B *
968[ #v #P #x normalize #H %{v} % [ @refl | @H ]
969| #m #P #x normalize #H destruct
970] qed.
971
972lemma labels_translated : ∀vars,lbls,tmp,tmpp,s,l,s',p.
973  (Exists ? (λl'.l' = l) (labels_defined s)) →
974  translate_statement vars lbls tmp tmpp s = OK ? «s', p» →
975  ∃l'. lookup_label lbls l = OK ? l' ∧ ldefined s' l'.
976#vars #lbls #tmp #tmpp #s #l @(statement_ind … s) (* FIXME: once switch is done we'll need something else here *)
977[ #s' #p *
978| #e1 #e2 #s' #p *
979| #eo #e #args #s' #p *
980| #s1 #s2 #IH1 #IH2 #s' #p #H #E
981  cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
982  cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
983  <(OK_sig_eq ?????? E) -E;
984  cases (Exists_append ???? H)
985  [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
986  | #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @L2 ]
987  ]
988| #e #s1 #s2 #IH1 #IH2 #s' #p #H #E
989  (* Carefully get rid of the equality that will screw up the case analysis *)
990  cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
991  [ #sz #sg #e' #E
992    cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
993    cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
994    <(OK_sig_eq ?????? E) -E;
995    cases (Exists_append ???? H)
996    [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
997    | #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @L2 ]
998    ]
999  | *: #x #e' normalize #E destruct
1000  ]
1001| #e #s #IH #s' #p #H #E
1002  (* Carefully get rid of the equality that will screw up the case analysis *)
1003  cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
1004  [ #sz #sg #e' #E
1005    cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
1006    <(OK_sig_eq ?????? E) -E;
1007    cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La | whd; normalize in ⊢ (???%) >append_nil @Lb ]
1008  | *: #x #e' normalize #E destruct
1009  ]
1010| #e #s #IH #s' #p #H #E
1011  (* Carefully get rid of the equality that will screw up the case analysis *)
1012  cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
1013  [ #sz #sg #e' #E
1014    cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
1015    <(OK_sig_eq ?????? E) -E;
1016    cases (IH s1' I1 H E1) #l' * #La #Lb %{l'} % [ @La | whd; normalize in ⊢ (???%) >append_nil @Lb ]
1017  | *: #x #e' normalize #E destruct
1018  ]
1019| #s1 #e #s1 #s2 #IH1 #IH2 #IH3 #s' #p #H #E
1020  (* Carefully get rid of the equality that will screw up the case analysis *)
1021  cases (bind_inversion ????? E) #e' * #_ cases (typ_of_type (typeof e)) in e' ⊢ %
1022  [ #sz #sg #e' #E
1023    cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
1024    cases (bind_inversion ????? E) * #s2' #I2 * #E2 -E #E
1025    cases (bind_inversion ????? E) * #s3' #I3 * #E3 -E #E
1026    <(OK_sig_eq ?????? E) -E;
1027    cases (Exists_append ???? H)
1028    [ #H1 cases (IH1 s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_l @L2 ]
1029    | -H #H cases (Exists_append ???? H)
1030      [ #H2 cases (IH2 s2' I2 H2 E2) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @Exists_append_l @Exists_append_r @L2 ]
1031      | #H3 cases (IH3 s3' I3 H3 E3) #l' * #L1 #L2 %{l'} % [ @L1 | @Exists_append_r @Exists_append_l @Exists_append_l @L2 ]
1032      ]
1033    ]
1034  | *: #x #e' normalize #E destruct
1035  ]
1036| #s' #p *
1037| #s' #p *
1038| #eo #s' #p *
1039| #e #ls #IH #s' #p #H #E whd in E:(??%?); destruct (* FIXME once switch is implemented ... *)
1040| #l0 #s0 #IH #s' #p #H
1041  whd in ⊢ (??%? → ?) #E cases (reflmatch ????? E) -E #l1 * #El #E
1042  cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
1043  <(OK_sig_eq ?????? E) -E;
1044  cases H
1045  [ #El' %{l1} <El' % [ @El | %1 @refl ]
1046  | #H1 cases (IH s1' I1 H1 E1) #l' * #L1 #L2 %{l'} % [ @L1 | %2 @L2 ]
1047  ]
1048| #l0 #s' #p *
1049| #l0 #s0 #IH #s' #p #H #E
1050  cases (bind_inversion ????? E) * #s1' #I1 * #E1 -E #E
1051  <(OK_sig_eq ?????? E) -E;
1052  @(IH s1' I1 H E1)
1053] qed.
1054
[1078]1055axiom ParamGlobalMixup : String.
[816]1056
[1096]1057definition alloc_params : ∀vars:var_types.∀ls. list (ident×type) → (Σs:stmt. stmt_inv vars ls s) → res (Σs:stmt.stmt_inv vars ls s) ≝
1058λvars,ls,params,s. foldl ?? (λs,it.
[1078]1059  let 〈id,ty〉 ≝ it in
1060  do s ← s;
[1087]1061  do t as E ← lookup' vars id;
1062  match t return λx.? → ? with
1063  [ Local ⇒ λE. OK (Σs:stmt.?) s
1064  | Stack n ⇒ λE.
[1078]1065      do q ← match access_mode ty with
1066      [ By_value q ⇒ OK ? q
1067      | By_reference r ⇒ OK ? (Mpointer r)
1068      | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id]
1069      ];
[1087]1070      OK ? «St_seq (St_store ? Any q (Cst ? (Oaddrstack n)) (Id (typ_of_type ty) id)) s, ?»
1071  | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id]
1072  ] E) (OK ? s) params.
[1096]1073try @conj try @conj try @conj try @conj try @conj
1074try @I
1075[ whd >E @I
1076| @(sig_ok … s)
1077] qed.
[1078]1078
[816]1079definition bigid1 ≝ an_identifier SymbolTag [[
1080false;true;false;false;
1081false;false;false;false;
1082false;false;false;false;
1083false;false;false;false]].
1084definition bigid2 ≝ an_identifier SymbolTag [[
1085false;true;false;false;
1086false;false;false;false;
1087false;false;false;false;
1088false;false;false;true]].
1089
[1087]1090lemma Exists_rm : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
1091#A #P #l1 #x #l2 elim l1
1092[ normalize #H %2 @H
1093| #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
1094qed.
1095
1096lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
1097#A #P #l1 #x #l2 #H elim l1
1098[ %1 @H
1099| #h #t #IH %2 @IH
1100] qed.
1101
1102lemma Exists_map : ∀A,B,P,Q,f,l.
1103Exists A P l →
1104(∀a.P a → Q (f a)) →
1105Exists B Q (map A B f l).
1106#A #B #P #Q #f #l elim l //
1107#h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
1108
1109notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E ≝ t 'in' s)"
1110 with precedence 10
1111for @{ match $t return λx.x = $t → ? with [ pair ${ident x} ${ident y} ⇒
1112        λ${ident E}.$s ] (refl ? $t) }.
1113
1114lemma local_id_add_local : ∀vars,id,id'.
1115  local_id vars id →
1116  local_id (add ?? vars id' Local) id.
1117#vars #id #id' #H
1118whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ?] cases (identifier_eq ? id id')
1119[ #E < E >lookup_add_hit //
1120| #NE >lookup_add_miss // @eq_identifier_elim // #E cases NE >E /2/
1121] qed.
1122
[1096]1123(* We only record labels from Slabel, not Sgoto, so that we detect badly formed
1124   programs. *)
1125let rec extend_label_env (s:statement) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝
1126match s with
1127[ Ssequence s1 s2 ⇒
1128    let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
1129    extend_label_env s2 lbls u
1130| Sifthenelse _ s1 s2 ⇒
1131    let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
1132    extend_label_env s2 lbls u
1133| Swhile _ s ⇒ extend_label_env s lbls u
1134| Sdowhile _ s ⇒ extend_label_env s lbls u
1135| Sfor s1 _ s2 s3 ⇒
1136    let 〈lbls,u〉 ≝ extend_label_env s1 lbls u in
1137    let 〈lbls,u〉 ≝ extend_label_env s2 lbls u in
1138    extend_label_env s3 lbls u
1139| Sswitch _ ls ⇒ extend_label_env' ls lbls u
1140| Slabel l s ⇒
1141    let 〈l',u〉 ≝ fresh ? u in
1142    extend_label_env s (add … lbls l l') u
1143| Scost _ s ⇒ extend_label_env s lbls u
1144| _ ⇒ 〈lbls,u〉
1145]
1146and extend_label_env' (ls:labeled_statements) (lbls:lenv) (u:universe ?) : lenv × (universe ?) ≝
1147match ls with
1148[ LSdefault s ⇒ extend_label_env s lbls u
1149| LScase _ _ s ls ⇒
1150    let 〈lbls,u〉 ≝ extend_label_env s lbls u in
1151    extend_label_env' ls lbls u
1152].
1153
1154definition build_label_env ≝ λbody. extend_label_env body (empty_map ??) (new_universe ?).
1155
[886]1156(* FIXME: the temporary handling is nonsense, I'm afraid. *)
[881]1157definition translate_function : list (ident×region) → function → res internal_function ≝
[816]1158λglobals, f.
[1096]1159  let 〈lbls, label_universe〉 ≝ build_label_env (fn_body f) in
[1087]1160  let 〈vartypes0, stacksize〉 as E ≝ characterise_vars globals f in
[816]1161  let tmp ≝ bigid1 in (* FIXME *)
1162  let tmpp ≝ bigid2 in (* FIXME *)
[1087]1163  let vartypes ≝ add … (add … vartypes0 tmp Local) tmpp Local in
[1096]1164  do s as E1 ← translate_statement vartypes lbls tmp tmpp (fn_body f);
1165  do s as E2 ← alloc_params vartypes lbls (fn_params f) s;
[816]1166  OK ? (mk_internal_function
[886]1167    (opttyp_of_type (fn_return f))
1168    (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f))
1169    (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f)))
[816]1170    stacksize
[1087]1171    s ?).
1172[ whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_hit %
1173| whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) >lookup_add_miss [ >lookup_add_hit %| % ]
[1096]1174| @(stmt_P_mp ???? (sig_ok ?? s))
1175  #s1 * #H1 #H2 % [ 2: @H2 ]
1176  @stmt_vars_mp [ 3: @sig_ok | skip ]
[1087]1177  #i #H cases (identifier_eq ? tmp i)
1178  [ #E <E @Exists_mid @refl
1179  | #NE1 @Exists_rm cases (identifier_eq ? tmpp i)
1180    [ #E <E @Exists_mid @refl
1181    | #NE2 @Exists_rm
1182      >map_append
1183      @Exists_map [ 2: @(characterise_vars_all … (sym_eq ??? E) i)
1184                       @(local_id_add_miss ?? Local ? NE1)
1185                       @(local_id_add_miss ?? Local ? NE2) @H
1186                  | skip
1187                  | * #id #ty #E1 <E1 @refl
1188                  ]
1189    ]
1190  ]
1191] qed.
[816]1192
[881]1193definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝
[816]1194λglobals,f.
1195match f with
1196[ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn')
1197| CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty)))
1198].
1199
1200definition clight_to_cminor : clight_program → res Cminor_program ≝
1201λp.
[881]1202  let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in
1203  let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in
1204  let globals ≝ fun_globals @ var_globals in
[961]1205  transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p.
Note: See TracBrowser for help on using the repository browser.