[816] | 1 | |
---|
| 2 | include "Clight/Csyntax.ma". |
---|
[880] | 3 | include "Clight/TypeComparison.ma". |
---|
[1605] | 4 | include "basics/lists/list.ma". |
---|
[816] | 5 | |
---|
[1194] | 6 | (* Identify local variables that must be allocated memory. *) |
---|
[816] | 7 | |
---|
| 8 | let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝ |
---|
| 9 | match e with |
---|
| 10 | [ Expr ed ty ⇒ |
---|
| 11 | match ed with |
---|
| 12 | [ Ederef e1 ⇒ gather_mem_vars_expr e1 |
---|
| 13 | | Eaddrof e1 ⇒ gather_mem_vars_addr e1 |
---|
| 14 | | Eunop _ e1 ⇒ gather_mem_vars_expr e1 |
---|
| 15 | | Ebinop _ e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 16 | gather_mem_vars_expr e2 |
---|
| 17 | | Ecast _ e1 ⇒ gather_mem_vars_expr e1 |
---|
| 18 | | Econdition e1 e2 e3 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 19 | gather_mem_vars_expr e2 ∪ |
---|
| 20 | gather_mem_vars_expr e3 |
---|
| 21 | | Eandbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 22 | gather_mem_vars_expr e2 |
---|
| 23 | | Eorbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 24 | gather_mem_vars_expr e2 |
---|
| 25 | | Efield e1 _ ⇒ gather_mem_vars_expr e1 |
---|
| 26 | | Ecost _ e1 ⇒ gather_mem_vars_expr e1 |
---|
| 27 | | _ ⇒ ∅ |
---|
| 28 | ] |
---|
| 29 | ] |
---|
| 30 | and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝ |
---|
| 31 | match e with |
---|
| 32 | [ Expr ed ty ⇒ |
---|
| 33 | match ed with |
---|
| 34 | [ Evar x ⇒ { (x) } |
---|
| 35 | | Ederef e1 ⇒ gather_mem_vars_expr e1 |
---|
| 36 | | Efield e1 _ ⇒ gather_mem_vars_addr e1 |
---|
| 37 | | _ ⇒ ∅ (* not an lvalue *) |
---|
| 38 | ] |
---|
| 39 | ]. |
---|
| 40 | |
---|
| 41 | let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝ |
---|
| 42 | match s with |
---|
| 43 | [ Sskip ⇒ ∅ |
---|
| 44 | | Sassign e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 45 | gather_mem_vars_expr e2 |
---|
| 46 | | Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] ∪ |
---|
| 47 | gather_mem_vars_expr e2 ∪ |
---|
| 48 | (foldl ?? (λs,e. s ∪ gather_mem_vars_expr e) ∅ es) |
---|
| 49 | | Ssequence s1 s2 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
| 50 | gather_mem_vars_stmt s2 |
---|
| 51 | | Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 52 | gather_mem_vars_stmt s1 ∪ |
---|
| 53 | gather_mem_vars_stmt s2 |
---|
| 54 | | Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 55 | gather_mem_vars_stmt s1 |
---|
| 56 | | Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 57 | gather_mem_vars_stmt s1 |
---|
| 58 | | Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
| 59 | gather_mem_vars_expr e1 ∪ |
---|
| 60 | gather_mem_vars_stmt s2 ∪ |
---|
| 61 | gather_mem_vars_stmt s3 |
---|
| 62 | | Sbreak ⇒ ∅ |
---|
| 63 | | Scontinue ⇒ ∅ |
---|
| 64 | | Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] |
---|
| 65 | | Sswitch e1 ls ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 66 | gather_mem_vars_ls ls |
---|
| 67 | | Slabel _ s1 ⇒ gather_mem_vars_stmt s1 |
---|
| 68 | | Sgoto _ ⇒ ∅ |
---|
| 69 | | Scost _ s1 ⇒ gather_mem_vars_stmt s1 |
---|
| 70 | ] |
---|
| 71 | and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝ |
---|
| 72 | match ls with |
---|
| 73 | [ LSdefault s1 ⇒ gather_mem_vars_stmt s1 |
---|
[961] | 74 | | LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
| 75 | gather_mem_vars_ls ls1 |
---|
[816] | 76 | ]. |
---|
| 77 | |
---|
| 78 | inductive var_type : Type[0] ≝ |
---|
[881] | 79 | | Global : region → var_type |
---|
[816] | 80 | | Stack : nat → var_type |
---|
| 81 | | Local : var_type |
---|
| 82 | . |
---|
| 83 | |
---|
| 84 | definition var_types ≝ identifier_map SymbolTag var_type. |
---|
| 85 | |
---|
[1316] | 86 | axiom UndeclaredIdentifier : String. |
---|
| 87 | |
---|
| 88 | definition lookup' ≝ |
---|
| 89 | λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id). |
---|
| 90 | |
---|
| 91 | definition local_id : var_types → ident → Prop ≝ |
---|
| 92 | λvars,id. match lookup' vars id with [ OK t ⇒ match t with [ Global _ ⇒ False | _ ⇒ True ] | _ ⇒ False ]. |
---|
| 93 | |
---|
[816] | 94 | (* Note that the semantics allows locals to shadow globals. |
---|
| 95 | Parameters start out as locals, but get stack allocated if their address |
---|
| 96 | is taken. We will add code to store them if that's the case. |
---|
| 97 | *) |
---|
| 98 | |
---|
| 99 | definition always_alloc : type → bool ≝ |
---|
| 100 | λt. match t with |
---|
| 101 | [ Tarray _ _ _ ⇒ true |
---|
| 102 | | Tstruct _ _ ⇒ true |
---|
| 103 | | Tunion _ _ ⇒ true |
---|
| 104 | | _ ⇒ false |
---|
| 105 | ]. |
---|
| 106 | |
---|
[881] | 107 | definition characterise_vars : list (ident×region) → function → var_types × nat ≝ |
---|
[816] | 108 | λglobals, f. |
---|
[1316] | 109 | let m ≝ foldr ?? (λidr,m. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in |
---|
[816] | 110 | let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in |
---|
[1316] | 111 | let 〈m,stacksize〉 ≝ foldr ?? (λv,ms. |
---|
[816] | 112 | let 〈m,stack_high〉 ≝ ms in |
---|
| 113 | let 〈id,ty〉 ≝ v in |
---|
| 114 | let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id |
---|
| 115 | then 〈Stack stack_high,stack_high + sizeof ty〉 |
---|
| 116 | else 〈Local, stack_high〉 in |
---|
[1078] | 117 | 〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in |
---|
[816] | 118 | 〈m,stacksize〉. |
---|
| 119 | |
---|
[1316] | 120 | lemma local_id_add_global : ∀vars,id,r,id'. |
---|
| 121 | local_id (add ?? vars id (Global r)) id' → local_id vars id'. |
---|
| 122 | #var #id #r #id' |
---|
[1516] | 123 | whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?); |
---|
[1316] | 124 | cases (identifier_eq ? id id') |
---|
[1516] | 125 | [ #E >E >lookup_add_hit whd in ⊢ (% → ?); * |
---|
[1515] | 126 | | #NE >lookup_add_miss /2/ |
---|
[1316] | 127 | ] qed. |
---|
[816] | 128 | |
---|
[1316] | 129 | lemma local_id_add_miss : ∀vars,id,t,id'. |
---|
| 130 | id ≠ id' → local_id (add ?? vars id t) id' → local_id vars id'. |
---|
| 131 | #vars #id #t #id' #NE |
---|
[1516] | 132 | whd in ⊢ (% → %); |
---|
| 133 | whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
[1316] | 134 | >lookup_add_miss |
---|
[1515] | 135 | [ #H @H | /2/ ] |
---|
[1316] | 136 | qed. |
---|
| 137 | |
---|
| 138 | lemma characterise_vars_all : ∀l,f,vars,n. |
---|
| 139 | characterise_vars l f = 〈vars,n〉 → |
---|
| 140 | ∀i. local_id vars i → |
---|
| 141 | Exists ? (λx.\fst x = i) (fn_params f @ fn_vars f). |
---|
| 142 | #globals #f |
---|
[1516] | 143 | whd in ⊢ (∀_.∀_.??%? → ?); |
---|
[1316] | 144 | elim (fn_params f @ fn_vars f) |
---|
[1516] | 145 | [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H @False_ind |
---|
| 146 | elim globals in H; |
---|
[1316] | 147 | [ normalize // |
---|
[1516] | 148 | | * #id #rg #t #IH whd in ⊢ (?%? → ?); #H @IH @(local_id_add_global ???? H) |
---|
[1316] | 149 | ] |
---|
[1516] | 150 | | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i |
---|
[1316] | 151 | cases (identifier_eq ? id i) |
---|
| 152 | [ #E' <E' #H % @refl |
---|
| 153 | | #NE #H whd %2 >(contract_pair var_types nat ?) in E; |
---|
[1516] | 154 | whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); |
---|
| 155 | cases (always_alloc ty ∨ mem_set ?? id) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); |
---|
[1316] | 156 | #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2 |
---|
| 157 | @(IH m0 n0) |
---|
[1516] | 158 | [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ |
---|
[1351] | 159 | | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE |
---|
[1316] | 160 | ] |
---|
| 161 | ] |
---|
| 162 | ] qed. |
---|
| 163 | |
---|
[816] | 164 | include "Cminor/syntax.ma". |
---|
| 165 | include "common/Errors.ma". |
---|
| 166 | |
---|
| 167 | alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)". |
---|
| 168 | |
---|
| 169 | axiom BadlyTypedAccess : String. |
---|
| 170 | axiom BadLvalue : String. |
---|
| 171 | axiom MissingField : String. |
---|
| 172 | |
---|
[1369] | 173 | |
---|
| 174 | definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝ |
---|
| 175 | λty1,ty2,P,p. |
---|
| 176 | do E ← assert_type_eq ty1 ty2; |
---|
| 177 | OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). |
---|
| 178 | |
---|
| 179 | definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2). |
---|
| 180 | * * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
| 181 | qed. |
---|
| 182 | |
---|
| 183 | definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2). |
---|
| 184 | * [ #sz1 #sg1 | #r1 | #sz1 ] |
---|
| 185 | * [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ] |
---|
| 186 | [ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ] |
---|
| 187 | *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
| 188 | | *; #P #p @(region_should_eq r1 ?? p) |
---|
| 189 | | *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
| 190 | ] qed. |
---|
| 191 | |
---|
| 192 | |
---|
[816] | 193 | alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)". |
---|
| 194 | alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)". |
---|
| 195 | |
---|
| 196 | (* XXX: For some reason matita refuses to pick the right one unless forced. *) |
---|
[1369] | 197 | alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)". |
---|
[816] | 198 | |
---|
[1369] | 199 | definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t') ≝ |
---|
| 200 | λt,t'.λop:CLunop. |
---|
[816] | 201 | match op with |
---|
[1369] | 202 | [ Onotbool ⇒ |
---|
| 203 | match t return λt. res (CMunop t t') with |
---|
| 204 | [ ASTint sz sg ⇒ |
---|
| 205 | match t' return λt'. res (CMunop ? t') with |
---|
| 206 | [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????) |
---|
| 207 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 208 | ] |
---|
| 209 | | ASTptr r ⇒ |
---|
| 210 | match t' return λt'. res (CMunop ? t') with |
---|
| 211 | [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????) |
---|
| 212 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 213 | ] |
---|
| 214 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 215 | ] |
---|
| 216 | | Onotint ⇒ |
---|
| 217 | match t' return λt'. res (CMunop t t') with |
---|
| 218 | [ ASTint sz sg ⇒ typ_should_eq ?? (λt. CMunop t (ASTint ??)) (Onotint sz sg) |
---|
| 219 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 220 | ] |
---|
[816] | 221 | | Oneg ⇒ |
---|
[1369] | 222 | match t' return λt'. res (CMunop t t') with |
---|
| 223 | [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg) |
---|
| 224 | | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz) |
---|
[816] | 225 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 226 | ] |
---|
[1369] | 227 | ]. @I qed. |
---|
[816] | 228 | |
---|
| 229 | definition translate_add ≝ |
---|
[880] | 230 | λty1,e1,ty2,e2,ty'. |
---|
| 231 | let ty1' ≝ typ_of_type ty1 in |
---|
| 232 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 233 | match classify_add ty1 ty2 with |
---|
[880] | 234 | [ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2) |
---|
| 235 | | add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2) |
---|
[961] | 236 | (* XXX using the integer size for e2 as the offset's size isn't right, because |
---|
| 237 | if e2 produces an 8bit value then the true offset might overflow *) |
---|
| 238 | | add_case_pi ty ⇒ |
---|
| 239 | match ty2' with |
---|
| 240 | [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty)))))) |
---|
| 241 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
| 242 | ] |
---|
| 243 | | add_case_ip ty ⇒ |
---|
| 244 | match ty1' with |
---|
| 245 | [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty)))))) |
---|
| 246 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
| 247 | ] |
---|
[816] | 248 | | add_default ⇒ Error ? (msg TypeMismatch) |
---|
| 249 | ]. |
---|
| 250 | |
---|
| 251 | definition translate_sub ≝ |
---|
[880] | 252 | λty1,e1,ty2,e2,ty'. |
---|
| 253 | let ty1' ≝ typ_of_type ty1 in |
---|
| 254 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 255 | match classify_sub ty1 ty2 with |
---|
[880] | 256 | [ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2) |
---|
| 257 | | sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2) |
---|
[961] | 258 | (* XXX choosing offset sizes? *) |
---|
| 259 | | sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty)))))) |
---|
| 260 | | sub_case_pp ty ⇒ |
---|
| 261 | match ty' with (* XXX overflow *) |
---|
| 262 | [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty))))) |
---|
| 263 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
| 264 | ] |
---|
[816] | 265 | | sub_default ⇒ Error ? (msg TypeMismatch) |
---|
| 266 | ]. |
---|
| 267 | |
---|
| 268 | definition translate_mul ≝ |
---|
[880] | 269 | λty1,e1,ty2,e2,ty'. |
---|
| 270 | let ty1' ≝ typ_of_type ty1 in |
---|
| 271 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 272 | match classify_mul ty1 ty2 with |
---|
[880] | 273 | [ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2) |
---|
| 274 | | mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2) |
---|
[816] | 275 | | mul_default ⇒ Error ? (msg TypeMismatch) |
---|
| 276 | ]. |
---|
| 277 | |
---|
| 278 | definition translate_div ≝ |
---|
[880] | 279 | λty1,e1,ty2,e2,ty'. |
---|
| 280 | let ty1' ≝ typ_of_type ty1 in |
---|
| 281 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 282 | match classify_div ty1 ty2 with |
---|
[961] | 283 | [ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) |
---|
[880] | 284 | | div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2) |
---|
| 285 | | div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2) |
---|
[816] | 286 | | div_default ⇒ Error ? (msg TypeMismatch) |
---|
| 287 | ]. |
---|
| 288 | |
---|
| 289 | definition translate_mod ≝ |
---|
[880] | 290 | λty1,e1,ty2,e2,ty'. |
---|
| 291 | let ty1' ≝ typ_of_type ty1 in |
---|
| 292 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 293 | match classify_mod ty1 ty2 with |
---|
[961] | 294 | [ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) |
---|
[880] | 295 | | mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2) |
---|
[816] | 296 | | mod_default ⇒ Error ? (msg TypeMismatch) |
---|
| 297 | ]. |
---|
| 298 | |
---|
| 299 | definition translate_shr ≝ |
---|
[880] | 300 | λty1,e1,ty2,e2,ty'. |
---|
| 301 | let ty1' ≝ typ_of_type ty1 in |
---|
| 302 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 303 | match classify_shr ty1 ty2 with |
---|
[961] | 304 | [ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) |
---|
[880] | 305 | | shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2) |
---|
[816] | 306 | | shr_default ⇒ Error ? (msg TypeMismatch) |
---|
| 307 | ]. |
---|
| 308 | |
---|
| 309 | definition translate_cmp ≝ |
---|
[880] | 310 | λc,ty1,e1,ty2,e2,ty'. |
---|
| 311 | let ty1' ≝ typ_of_type ty1 in |
---|
| 312 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 313 | match classify_cmp ty1 ty2 with |
---|
[880] | 314 | [ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2) |
---|
| 315 | | cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2) |
---|
| 316 | | cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2) |
---|
| 317 | | cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2) |
---|
[816] | 318 | | cmp_default ⇒ Error ? (msg TypeMismatch) |
---|
| 319 | ]. |
---|
| 320 | |
---|
[880] | 321 | definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝ |
---|
| 322 | λop,ty1,e1,ty2,e2,ty. |
---|
| 323 | let ty' ≝ typ_of_type ty in |
---|
[816] | 324 | match op with |
---|
[880] | 325 | [ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty' |
---|
| 326 | | Osub ⇒ translate_sub ty1 e1 ty2 e2 ty' |
---|
| 327 | | Omul ⇒ translate_mul ty1 e1 ty2 e2 ty' |
---|
| 328 | | Omod ⇒ translate_mod ty1 e1 ty2 e2 ty' |
---|
| 329 | | Odiv ⇒ translate_div ty1 e1 ty2 e2 ty' |
---|
| 330 | | Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2) |
---|
| 331 | | Oor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2) |
---|
| 332 | | Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2) |
---|
| 333 | | Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2) |
---|
| 334 | | Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty' |
---|
| 335 | | Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty' |
---|
| 336 | | One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty' |
---|
| 337 | | Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty' |
---|
| 338 | | Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty' |
---|
| 339 | | Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty' |
---|
| 340 | | Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty' |
---|
[816] | 341 | ]. |
---|
| 342 | |
---|
[1316] | 343 | lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e. |
---|
| 344 | expr_vars ? e1 P → |
---|
| 345 | expr_vars ? e2 P → |
---|
| 346 | translate_binop op ty1 e1 ty2 e2 ty = OK ? e → |
---|
| 347 | expr_vars ? e P. |
---|
| 348 | #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2 |
---|
[1516] | 349 | whd in ⊢ (??%? → ?); |
---|
[1316] | 350 | [ cases (classify_add ty1 ty2) |
---|
[1516] | 351 | [ 3,4: #z ] whd in ⊢ (??%? → ?); |
---|
| 352 | [ generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?); |
---|
[1316] | 353 | * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) |
---|
| 354 | whd in c:(??%?); destruct % [ @H1 | % // @H2 ] |
---|
[1516] | 355 | | generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?); |
---|
[1316] | 356 | * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) |
---|
| 357 | whd in c:(??%?); destruct % [ @H2 | % // @H1 ] |
---|
| 358 | | *: #E destruct (E) % try @H1 @H2 |
---|
| 359 | ] |
---|
| 360 | | cases (classify_sub ty1 ty2) |
---|
[1516] | 361 | [ 3,4: #z] whd in ⊢ (??%? → ?); |
---|
| 362 | [ 2: generalize in ⊢ (??(match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ])? → ?); |
---|
[1316] | 363 | * #a #b try #c try #d try whd in b:(??%?); try ( destruct (b)) |
---|
| 364 | whd in c:(??%?); destruct % [ % try @H1 @H2 ] @I |
---|
| 365 | | *: #E destruct (E) % try @H1 try @H2 % // @H2 |
---|
| 366 | ] |
---|
| 367 | | cases (classify_mul ty1 ty2) #E whd in E:(??%?); destruct |
---|
| 368 | % try @H1 @H2 |
---|
| 369 | | cases (classify_div ty1 ty2) #E whd in E:(??%?); destruct |
---|
| 370 | % try @H1 @H2 |
---|
| 371 | | cases (classify_mod ty1 ty2) #E whd in E:(??%?); destruct |
---|
| 372 | % try @H1 @H2 |
---|
| 373 | | 6,7,8,9: #E destruct % try @H1 @H2 |
---|
| 374 | | cases (classify_shr ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 |
---|
| 375 | | 11,12,13,14,15,16: cases (classify_cmp ty1 ty2) #E whd in E:(??%?); destruct % try @H1 @H2 |
---|
| 376 | ] qed. |
---|
[880] | 377 | |
---|
| 378 | (* We'll need to implement proper translation of pointers if we really do memory |
---|
| 379 | spaces. *) |
---|
| 380 | definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝ |
---|
| 381 | λr1,r2,P. |
---|
| 382 | match r1 return λx.P x → res (P r2) with |
---|
| 383 | [ Any ⇒ match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 384 | | Data ⇒ match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 385 | | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 386 | | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 387 | | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 388 | | Code ⇒ match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 389 | ]. |
---|
| 390 | |
---|
[1316] | 391 | definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝ |
---|
| 392 | λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e. |
---|
[880] | 393 | |
---|
[1369] | 394 | axiom FIXME : String. |
---|
| 395 | |
---|
[1316] | 396 | definition translate_cast : ∀P.type → ∀ty2:type. (Σe:CMexpr ?. expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝ |
---|
| 397 | λP,ty1,ty2. |
---|
| 398 | match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with |
---|
[880] | 399 | [ Tint sz1 sg1 ⇒ λe. |
---|
[1316] | 400 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
[1369] | 401 | [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e) |
---|
| 402 | | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e) |
---|
| 403 | | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e) |
---|
| 404 | | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e) |
---|
[816] | 405 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 406 | ] |
---|
[880] | 407 | | Tfloat sz1 ⇒ λe. |
---|
[1316] | 408 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
[1369] | 409 | [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?» |
---|
| 410 | | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *) |
---|
[816] | 411 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 412 | ] |
---|
[880] | 413 | | Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *) |
---|
[1316] | 414 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with |
---|
[1369] | 415 | [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ??) e, ?» |
---|
[1316] | 416 | | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e |
---|
| 417 | | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e |
---|
[816] | 418 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 419 | ] |
---|
[880] | 420 | | Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *) |
---|
[1316] | 421 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
[1369] | 422 | [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?» |
---|
[1316] | 423 | | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e |
---|
| 424 | | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e |
---|
[816] | 425 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 426 | ] |
---|
[880] | 427 | | _ ⇒ λ_. Error ? (msg TypeMismatch) |
---|
[1605] | 428 | ]. whd normalize nodelta @pi2 |
---|
| 429 | qed. |
---|
[816] | 430 | |
---|
[881] | 431 | lemma 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 | |
---|
[1316] | 441 | let rec translate_expr (vars:var_types) (e:expr) on e : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) ≝ |
---|
| 442 | match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with |
---|
[816] | 443 | [ Expr ed ty ⇒ |
---|
| 444 | match ed with |
---|
[1316] | 445 | [ Econst_int sz i ⇒ OK ? «Cst ? (Ointconst sz i), ?» |
---|
| 446 | | Econst_float f ⇒ OK ? «Cst ? (Ofloatconst f), ?» |
---|
[816] | 447 | | Evar id ⇒ |
---|
[1316] | 448 | do c as E ← lookup' vars id; |
---|
| 449 | match c return λx.? = ? → res (Σe':CMexpr ?. ?) with |
---|
| 450 | [ Global r ⇒ λ_. |
---|
[816] | 451 | match access_mode ty with |
---|
[1316] | 452 | [ By_value q ⇒ OK ? «Mem ? r q (Cst ? (Oaddrsymbol id 0)), ?» |
---|
| 453 | | By_reference _ ⇒ OK ? «Cst ? (Oaddrsymbol id 0), ?» |
---|
[816] | 454 | | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
| 455 | ] |
---|
[1316] | 456 | | Stack n ⇒ λE. |
---|
[816] | 457 | match access_mode ty with |
---|
[1316] | 458 | [ By_value q ⇒ OK ? «Mem ? Any q (Cst ? (Oaddrstack n)), ?» |
---|
| 459 | | By_reference _ ⇒ OK ? «Cst ? (Oaddrstack n), ?» |
---|
[816] | 460 | | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
| 461 | ] |
---|
[1316] | 462 | | Local ⇒ λE. OK ? «Id ? id, ?» |
---|
| 463 | ] E |
---|
[816] | 464 | | Ederef e1 ⇒ |
---|
| 465 | do e1' ← translate_expr vars e1; |
---|
[1316] | 466 | match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with |
---|
[881] | 467 | [ ASTptr r ⇒ λe1'. |
---|
[1316] | 468 | match access_mode ty return λx.? → res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with |
---|
[1605] | 469 | [ By_value q ⇒ λ_.OK ? «Mem (typ_of_type ty) ? q (pi1 … e1'), ?» |
---|
[1316] | 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)⌉ |
---|
[881] | 472 | | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) |
---|
[1316] | 473 | ] (access_mode_typ ty) |
---|
[881] | 474 | | _ ⇒ λ_. Error ? (msg TypeMismatch) |
---|
| 475 | ] e1' |
---|
[880] | 476 | | Eaddrof e1 ⇒ |
---|
| 477 | do e1' ← translate_addr vars e1; |
---|
[1316] | 478 | match typ_of_type ty return λx.res (Σz:CMexpr x.?) with |
---|
[881] | 479 | [ ASTptr r ⇒ |
---|
| 480 | match e1' with |
---|
[1605] | 481 | [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1' |
---|
[881] | 482 | ] |
---|
[880] | 483 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
[816] | 484 | ] |
---|
| 485 | | Eunop op e1 ⇒ |
---|
[1369] | 486 | do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op; |
---|
[816] | 487 | do e1' ← translate_expr vars e1; |
---|
[1316] | 488 | OK ? «Op1 ?? op' e1', ?» |
---|
[816] | 489 | | Ebinop op e1 e2 ⇒ |
---|
| 490 | do e1' ← translate_expr vars e1; |
---|
| 491 | do e2' ← translate_expr vars e2; |
---|
[1316] | 492 | do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty; |
---|
| 493 | OK ? «e', ?» |
---|
[816] | 494 | | Ecast ty1 e1 ⇒ |
---|
| 495 | do e1' ← translate_expr vars e1; |
---|
[1316] | 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' |
---|
[816] | 499 | | Econdition e1 e2 e3 ⇒ |
---|
| 500 | do e1' ← translate_expr vars e1; |
---|
| 501 | do e2' ← translate_expr vars e2; |
---|
[1316] | 502 | do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; |
---|
[816] | 503 | do e3' ← translate_expr vars e3; |
---|
[1316] | 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', ?» |
---|
[880] | 507 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 508 | ] e1' |
---|
[816] | 509 | | Eandbool e1 e2 ⇒ |
---|
| 510 | do e1' ← translate_expr vars e1; |
---|
| 511 | do e2' ← translate_expr vars e2; |
---|
[961] | 512 | match ty with |
---|
| 513 | [ Tint sz _ ⇒ |
---|
[1316] | 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 ?))), ?» |
---|
[961] | 517 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 518 | ] e1' |
---|
| 519 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 520 | ] |
---|
[816] | 521 | | Eorbool e1 e2 ⇒ |
---|
| 522 | do e1' ← translate_expr vars e1; |
---|
| 523 | do e2' ← translate_expr vars e2; |
---|
[961] | 524 | match ty with |
---|
| 525 | [ Tint sz _ ⇒ |
---|
[1316] | 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', ?» |
---|
[961] | 529 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 530 | ] e1' |
---|
| 531 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 532 | ] |
---|
| 533 | | Esizeof ty1 ⇒ |
---|
| 534 | match ty with |
---|
[1316] | 535 | [ Tint sz _ ⇒ OK ? «Cst ? (Ointconst sz (repr ? (sizeof ty1))), ?» |
---|
[961] | 536 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 537 | ] |
---|
[816] | 538 | | Efield e1 id ⇒ |
---|
[1316] | 539 | match typeof e1 with |
---|
[816] | 540 | [ Tstruct _ fl ⇒ |
---|
| 541 | do e1' ← translate_addr vars e1; |
---|
[881] | 542 | match e1' with |
---|
[1605] | 543 | [ mk_DPair r e1' ⇒ |
---|
[881] | 544 | do off ← field_offset id fl; |
---|
| 545 | match access_mode ty with |
---|
[1316] | 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))),?» |
---|
[881] | 548 | | By_nothing ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 549 | ] |
---|
[816] | 550 | ] |
---|
| 551 | | Tunion _ _ ⇒ |
---|
| 552 | do e1' ← translate_addr vars e1; |
---|
[881] | 553 | match e1' with |
---|
[1605] | 554 | [ mk_DPair r e1' ⇒ |
---|
[1316] | 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).?⌉ |
---|
[881] | 559 | | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) |
---|
| 560 | ] (refl ? (access_mode ty)) |
---|
[816] | 561 | ] |
---|
| 562 | | _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
[1316] | 563 | ] |
---|
[816] | 564 | | Ecost l e1 ⇒ |
---|
| 565 | do e1' ← translate_expr vars e1; |
---|
[1316] | 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' |
---|
[816] | 568 | ] |
---|
[1316] | 569 | ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝ |
---|
[816] | 570 | match 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); |
---|
[1316] | 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), ?»» |
---|
[1078] | 578 | | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *) |
---|
[816] | 579 | ] |
---|
[880] | 580 | | Ederef e1 ⇒ |
---|
| 581 | do e1' ← translate_expr vars e1; |
---|
[1316] | 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'» |
---|
[880] | 584 | | _ ⇒ λ_.Error ? (msg BadlyTypedAccess) |
---|
| 585 | ] e1' |
---|
[816] | 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; |
---|
[881] | 591 | match e1' with |
---|
[1605] | 592 | [ mk_DPair 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] | 593 | ] |
---|
[816] | 594 | | Tunion _ _ ⇒ translate_addr vars e1 |
---|
| 595 | | _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 596 | ] |
---|
| 597 | | _ ⇒ Error ? (msg BadLvalue) |
---|
| 598 | ] |
---|
| 599 | ]. |
---|
[1316] | 600 | whd 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. |
---|
[816] | 615 | |
---|
[1316] | 616 | inductive 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. |
---|
[816] | 619 | |
---|
| 620 | definition 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 ⇒ |
---|
[1316] | 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 |
---|
[816] | 637 | | _ ⇒ |
---|
| 638 | do e1' ← translate_addr vars e1; |
---|
[1316] | 639 | match e1' with [ dp r e1' ⇒ OK ? (MemDest ? r q e1') ] |
---|
[816] | 640 | ] |
---|
| 641 | ]. |
---|
[1316] | 642 | whd // >E @I |
---|
| 643 | qed. |
---|
[1194] | 644 | |
---|
[1316] | 645 | definition lenv ≝ identifier_map SymbolTag (identifier Label). |
---|
| 646 | |
---|
| 647 | axiom MissingLabel : String. |
---|
| 648 | |
---|
| 649 | definition lookup_label ≝ |
---|
| 650 | λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l). |
---|
| 651 | |
---|
| 652 | definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l. |
---|
| 653 | |
---|
| 654 | let rec labels_defined (s:statement) : list ident ≝ |
---|
| 655 | match 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 | ] |
---|
| 666 | and labels_defined_switch (ls:labeled_statements) : list ident ≝ |
---|
| 667 | match ls with |
---|
| 668 | [ LSdefault s ⇒ labels_defined s |
---|
| 669 | | LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls |
---|
| 670 | ]. |
---|
| 671 | |
---|
| 672 | definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). |
---|
| 673 | |
---|
| 674 | definition 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 | |
---|
| 679 | definition stmt_inv ≝ |
---|
| 680 | λvars. λlbls:lenv. |
---|
| 681 | stmt_P (λs.stmt_vars (local_id vars) s ∧ stmt_labels (lpresent lbls) s). |
---|
| 682 | |
---|
| 683 | definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt.∀ls. stmt_inv vars ls s) ≝ |
---|
[816] | 684 | λvars,e1,e2. |
---|
| 685 | do e2' ← translate_expr vars e2; |
---|
| 686 | do dest ← translate_dest vars e1 (typeof e2); |
---|
| 687 | match dest with |
---|
[1316] | 688 | [ IdDest id p ⇒ OK ? «St_assign ? id e2', ?» |
---|
| 689 | | MemDest r q e1' ⇒ OK ? «St_store ? r q e1' e2', ?» |
---|
[816] | 690 | ]. |
---|
[1316] | 691 | #ls whd % |
---|
| 692 | [ % // @use_sig |
---|
| 693 | | @I |
---|
| 694 | | % @use_sig |
---|
| 695 | | @I |
---|
| 696 | ] qed. |
---|
[816] | 697 | |
---|
| 698 | definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝ |
---|
| 699 | λA,B,f,oa. |
---|
| 700 | match oa with |
---|
| 701 | [ None ⇒ OK ? (None ?) |
---|
| 702 | | Some a ⇒ do b ← f a; OK ? (Some ? b) |
---|
| 703 | ]. |
---|
| 704 | |
---|
[1316] | 705 | definition 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] | 706 | λv,e. |
---|
| 707 | do e' ← translate_expr v e; |
---|
[1316] | 708 | OK (Σe:(Σt:typ.CMexpr t).?) ««?, e'», ?». |
---|
| 709 | whd @use_sig |
---|
| 710 | qed. |
---|
[880] | 711 | |
---|
[1206] | 712 | record tmpgen : Type[0] ≝ { |
---|
| 713 | tmp_universe : universe SymbolTag; |
---|
| 714 | tmp_env : list (ident × typ) |
---|
| 715 | }. |
---|
| 716 | |
---|
| 717 | definition 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 | |
---|
[1316] | 722 | lemma 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 |
---|
| 726 | qed. |
---|
| 727 | |
---|
| 728 | definition add_tmps : var_types → tmpgen → var_types ≝ |
---|
| 729 | λvs,g. |
---|
| 730 | foldr ?? (λidty,vs. add ?? vs (\fst idty) Local) vs (tmp_env g). |
---|
| 731 | |
---|
| 732 | definition 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 | |
---|
| 736 | lemma 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 |
---|
[1516] | 739 | whd in ⊢ (???% → ?); #E |
---|
[1316] | 740 | #id #H |
---|
[1515] | 741 | cases (identifier_eq ? id tmp) |
---|
| 742 | destruct #E |
---|
[1516] | 743 | whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; |
---|
[1515] | 744 | [ >E >lookup_add_hit @I |
---|
| 745 | | cases E #NE >lookup_add_miss [ @H | /2/ |
---|
[1316] | 746 | ] qed. |
---|
| 747 | |
---|
| 748 | definition 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 | |
---|
| 755 | lemma 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 |
---|
| 758 | qed. |
---|
| 759 | |
---|
| 760 | lemma 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 |
---|
| 763 | qed. |
---|
| 764 | |
---|
| 765 | lemma local_id_add_local_oblivious : ∀vars,id,id'. |
---|
| 766 | local_id vars id → local_id (add ?? vars id' Local) id. |
---|
[1516] | 767 | #vars #id #id' #H whd whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
[1316] | 768 | cases (identifier_eq ? id id') |
---|
| 769 | [ #E >E >lookup_add_hit @I |
---|
[1515] | 770 | | #NE >lookup_add_miss [ @H | /2/ |
---|
[1316] | 771 | ] qed. |
---|
| 772 | |
---|
| 773 | lemma 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 | |
---|
| 780 | lemma 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 | |
---|
| 790 | lemma 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 |
---|
[1516] | 793 | whd in ⊢ (???% → ?); #E |
---|
[1351] | 794 | destruct |
---|
[1516] | 795 | whd in ⊢ (?%?); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit |
---|
[1316] | 796 | @I |
---|
| 797 | qed. |
---|
| 798 | |
---|
| 799 | let 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) ≝ |
---|
| 800 | match 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〉, ?» |
---|
[816] | 805 | | Scall ret ef args ⇒ |
---|
| 806 | do ef' ← translate_expr vars ef; |
---|
[1316] | 807 | do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef'; |
---|
| 808 | do args' ← mmap_sigma … (translate_expr_sigma vars) args; |
---|
[816] | 809 | match ret with |
---|
[1316] | 810 | [ None ⇒ OK ? «〈St_call (None ?) ef' args', u〉, ?» |
---|
[816] | 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 |
---|
[1316] | 814 | [ IdDest id p ⇒ OK ? «〈St_call (Some ? id) ef' args', u〉, ?» |
---|
[881] | 815 | | MemDest r q e1' ⇒ |
---|
[1316] | 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〉, ?» |
---|
[816] | 818 | ] |
---|
| 819 | ] |
---|
| 820 | | Ssequence s1 s2 ⇒ |
---|
[1351] | 821 | do «s1', u1, H1» ← translate_statement vars lbls u s1; |
---|
| 822 | do «s2', u2, H2» ← translate_statement vars lbls u1 s2; |
---|
[1316] | 823 | OK ? «〈St_seq s1' s2', u2〉, ?» |
---|
[816] | 824 | | Sifthenelse e1 s1 s2 ⇒ |
---|
| 825 | do e1' ← translate_expr vars e1; |
---|
[1316] | 826 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with |
---|
[880] | 827 | [ ASTint _ _ ⇒ λe1'. |
---|
[1351] | 828 | do «s1', u, H1» ← translate_statement vars lbls u s1; |
---|
| 829 | do «s2', u, H2» ← translate_statement vars lbls u s2; |
---|
[1316] | 830 | OK ? «〈St_ifthenelse ?? e1' s1' s2', u〉, ?» |
---|
[880] | 831 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 832 | ] e1' |
---|
[816] | 833 | | Swhile e1 s1 ⇒ |
---|
| 834 | do e1' ← translate_expr vars e1; |
---|
[1316] | 835 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with |
---|
[880] | 836 | [ ASTint _ _ ⇒ λe1'. |
---|
[1351] | 837 | do «s1', u, H1» ← translate_statement vars lbls u s1; |
---|
[880] | 838 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
[1316] | 839 | OK ? «〈St_block |
---|
[880] | 840 | (St_loop |
---|
[1316] | 841 | (St_ifthenelse ?? e1' (St_block s1') (St_exit 0))), u〉, ?» |
---|
[880] | 842 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 843 | ] e1' |
---|
[816] | 844 | | Sdowhile e1 s1 ⇒ |
---|
| 845 | do e1' ← translate_expr vars e1; |
---|
[1316] | 846 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with |
---|
[880] | 847 | [ ASTint _ _ ⇒ λe1'. |
---|
[1351] | 848 | do «s1',u, H1» ← translate_statement vars lbls u s1; |
---|
[880] | 849 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
[1316] | 850 | OK ? «〈St_block |
---|
[880] | 851 | (St_loop |
---|
[1316] | 852 | (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0)))), u〉, ?» |
---|
[880] | 853 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 854 | ] e1' |
---|
[816] | 855 | | Sfor s1 e1 s2 s3 ⇒ |
---|
| 856 | do e1' ← translate_expr vars e1; |
---|
[1316] | 857 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with |
---|
[880] | 858 | [ ASTint _ _ ⇒ λe1'. |
---|
[1351] | 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; |
---|
[880] | 862 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
[1316] | 863 | OK ? «〈St_seq s1' |
---|
[880] | 864 | (St_block |
---|
| 865 | (St_loop |
---|
[1316] | 866 | (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0)))), u〉, ?» |
---|
[880] | 867 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 868 | ] e1' |
---|
[1316] | 869 | | Sbreak ⇒ OK ? «〈St_exit 1, u〉, ?» |
---|
| 870 | | Scontinue ⇒ OK ? «〈St_exit 0, u〉, ?» |
---|
[816] | 871 | | Sreturn ret ⇒ |
---|
[880] | 872 | match ret with |
---|
[1316] | 873 | [ None ⇒ OK ? «〈St_return (None ?), u〉, ?» |
---|
[880] | 874 | | Some e1 ⇒ |
---|
| 875 | do e1' ← translate_expr vars e1; |
---|
[1316] | 876 | OK ? «〈St_return (Some ? (dp … e1')), u〉, ?» |
---|
[880] | 877 | ] |
---|
[816] | 878 | | Sswitch e1 ls ⇒ Error ? (msg FIXME) |
---|
| 879 | | Slabel l s1 ⇒ |
---|
[1316] | 880 | do l' as E ← lookup_label lbls l; |
---|
[1351] | 881 | do «s1', u, H1» ← translate_statement vars lbls u s1; |
---|
[1316] | 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〉, ?» |
---|
[816] | 886 | | Scost l s1 ⇒ |
---|
[1351] | 887 | do «s1', u, H1» ← translate_statement vars lbls u s1; |
---|
[1316] | 888 | OK ? «〈St_cost l s1', u〉, ?» |
---|
[816] | 889 | ]. |
---|
[1316] | 890 | try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj |
---|
| 891 | try @I |
---|
| 892 | try (#l #H @(match H in False with [ ])) |
---|
| 893 | try (#id #H @H) |
---|
| 894 | [ @add_tmps_oblivious @(use_sig ?? s') |
---|
| 895 | | @local_id_add_tmps_oblivious @p |
---|
| 896 | ] |
---|
| 897 | try (@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. |
---|
[816] | 941 | |
---|
[1316] | 942 | |
---|
[1078] | 943 | axiom ParamGlobalMixup : String. |
---|
[816] | 944 | |
---|
[1316] | 945 | (* ls and s0 aren't real parameters, they're just there for giving the invariant. *) |
---|
| 946 | definition 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. |
---|
[1078] | 948 | let 〈id,ty〉 ≝ it in |
---|
[1351] | 949 | do «s,u, Is» ← su; |
---|
[1316] | 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. |
---|
[1078] | 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 | ]; |
---|
[1316] | 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. |
---|
| 962 | try @conj try @conj try @conj try @conj try @conj try @conj |
---|
| 963 | try @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. |
---|
[1078] | 969 | |
---|
[1316] | 970 | (* |
---|
| 971 | lemma 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 |
---|
| 975 | whd 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 | *) |
---|
| 980 | axiom DuplicateLabel : String. |
---|
| 981 | |
---|
| 982 | definition 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 | |
---|
| 987 | lemma lookup_label_add : ∀lbls,l,l'. |
---|
| 988 | lookup_label (add … lbls l l') l = OK ? l'. |
---|
[1516] | 989 | #lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl |
---|
[1316] | 990 | qed. |
---|
| 991 | |
---|
| 992 | lemma lookup_label_miss : ∀lbls,l,l',l0. |
---|
| 993 | l0 ≠ l → |
---|
| 994 | lookup_label (add … lbls l l') l0 = lookup_label lbls l0. |
---|
[1515] | 995 | #lbls #l #l' #l0 #NE |
---|
[1516] | 996 | whd in ⊢ (??%%); |
---|
[1316] | 997 | >lookup_add_miss |
---|
[1515] | 998 | [ @refl | @NE ] |
---|
[1316] | 999 | qed. |
---|
| 1000 | |
---|
| 1001 | let rec populate_lenv (ls:list ident) (lbls:lenv) (u:universe ?) : res (Σlbls':lenv. lenv_list_inv lbls lbls' ls) ≝ |
---|
| 1002 | match 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 |
---|
[1516] | 1014 | | cases lbls1 #lbls' #I whd in ⊢ (??%?); |
---|
[1316] | 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 |
---|
[1516] | 1019 | | #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H |
---|
[1316] | 1020 | ] |
---|
| 1021 | ] |
---|
| 1022 | ] qed. |
---|
| 1023 | |
---|
| 1024 | definition 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) // |
---|
[1516] | 1029 | whd in ⊢ (??%? → ?); #H destruct |
---|
[1316] | 1030 | qed. |
---|
| 1031 | |
---|
| 1032 | lemma 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 |
---|
[1516] | 1036 | whd in ⊢ (?%? → ?); |
---|
[1316] | 1037 | elim (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 |
---|
[1515] | 1042 | | #NE #H cases (IH ?) |
---|
[1316] | 1043 | [ #H' %1 @H' |
---|
| 1044 | | #H' %2 %2 @H' |
---|
| 1045 | | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
[1515] | 1046 | >lookup_add_miss in H; [ #H @H | @NE ] |
---|
[1316] | 1047 | ] |
---|
| 1048 | ] |
---|
| 1049 | ] qed. |
---|
| 1050 | |
---|
| 1051 | lemma 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 |
---|
| 1054 | cases (Exists_append … EX) |
---|
| 1055 | [ #EX1 @Exists_append_l @EX1 |
---|
| 1056 | | #EX3 @Exists_append_r @Exists_append_r @EX3 |
---|
| 1057 | ] qed. |
---|
| 1058 | |
---|
[1207] | 1059 | definition translate_function : universe SymbolTag → list (ident×region) → function → res internal_function ≝ |
---|
| 1060 | λtmpuniverse, globals, f. |
---|
[1316] | 1061 | do «lbls, Ilbls» ← build_label_env (fn_body f); |
---|
| 1062 | let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in |
---|
[1207] | 1063 | let tmp ≝ mk_tmpgen tmpuniverse [ ] in |
---|
[1316] | 1064 | do s ← translate_statement vartypes lbls tmp (fn_body f); |
---|
[1351] | 1065 | do «s,tmp, Is» ← alloc_params vartypes lbls ?? (fn_params f) s; |
---|
[816] | 1066 | OK ? (mk_internal_function |
---|
[886] | 1067 | (opttyp_of_type (fn_return f)) |
---|
| 1068 | (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f)) |
---|
[1206] | 1069 | ((tmp_env tmp)@(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f))) |
---|
[816] | 1070 | stacksize |
---|
[1316] | 1071 | s ?). |
---|
| 1072 | cases 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 |
---|
[1516] | 1088 | cases (L … DEFINED) #lx * #LOOKUPx >LOOKUPx in LOOKUP; #Ex destruct (Ex) |
---|
[1316] | 1089 | #H @H |
---|
| 1090 | ] qed. |
---|
[816] | 1091 | |
---|
[1207] | 1092 | definition translate_fundef : universe SymbolTag → list (ident×region) → clight_fundef → res (fundef internal_function) ≝ |
---|
| 1093 | λtmpuniverse,globals,f. |
---|
[816] | 1094 | match f with |
---|
[1207] | 1095 | [ CL_Internal fn ⇒ do fn' ← translate_function tmpuniverse globals fn; OK ? (Internal ? fn') |
---|
[816] | 1096 | | CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty))) |
---|
| 1097 | ]. |
---|
| 1098 | |
---|
[1207] | 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. *) |
---|
| 1102 | include "Clight/fresh.ma". |
---|
| 1103 | |
---|
[816] | 1104 | definition clight_to_cminor : clight_program → res Cminor_program ≝ |
---|
| 1105 | λp. |
---|
[1207] | 1106 | let tmpuniverse ≝ universe_for_program p in |
---|
[881] | 1107 | let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in |
---|
[1139] | 1108 | let var_globals ≝ map … (λv. 〈\fst (\fst v), \snd (\fst v)〉) (prog_vars ?? p) in |
---|
[881] | 1109 | let globals ≝ fun_globals @ var_globals in |
---|
[1351] | 1110 | transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)). |
---|