[816] | 1 | |
---|
| 2 | include "Clight/Csyntax.ma". |
---|
[880] | 3 | include "Clight/TypeComparison.ma". |
---|
[816] | 4 | include "utilities/lists.ma". |
---|
| 5 | (* |
---|
| 6 | let rec mem_vars_expr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝ |
---|
| 7 | match 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 | ] |
---|
| 28 | and mem_vars_addr (mem_vars:identifier_set SymbolTag) (e:expr) on e : Prop ≝ |
---|
| 29 | match 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 | |
---|
| 39 | let rec mem_vars_stmt (mem_vars:identifier_set SymbolTag) (s:statement) on s : Prop ≝ |
---|
| 40 | match 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 | ] |
---|
| 69 | and mem_vars_ls (mem_vars:identifier_set SymbolTag) (ls:labeled_statements) on ls : Prop ≝ |
---|
| 70 | match 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 | |
---|
| 77 | let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝ |
---|
| 78 | match 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 | ] |
---|
| 99 | and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝ |
---|
| 100 | match 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 | |
---|
| 110 | let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝ |
---|
| 111 | match 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 | ] |
---|
| 140 | and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝ |
---|
| 141 | match 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 | |
---|
| 147 | inductive var_type : Type[0] ≝ |
---|
[881] | 148 | | Global : region → var_type |
---|
[816] | 149 | | Stack : nat → var_type |
---|
| 150 | | Local : var_type |
---|
| 151 | . |
---|
| 152 | |
---|
| 153 | definition var_types ≝ identifier_map SymbolTag var_type. |
---|
| 154 | |
---|
| 155 | (* Note that the semantics allows locals to shadow globals. |
---|
| 156 | Parameters start out as locals, but get stack allocated if their address |
---|
| 157 | is taken. We will add code to store them if that's the case. |
---|
| 158 | *) |
---|
| 159 | |
---|
| 160 | definition always_alloc : type → bool ≝ |
---|
| 161 | λt. match t with |
---|
| 162 | [ Tarray _ _ _ ⇒ true |
---|
| 163 | | Tstruct _ _ ⇒ true |
---|
| 164 | | Tunion _ _ ⇒ true |
---|
| 165 | | _ ⇒ false |
---|
| 166 | ]. |
---|
| 167 | |
---|
[881] | 168 | definition characterise_vars : list (ident×region) → function → var_types × nat ≝ |
---|
[816] | 169 | λglobals, f. |
---|
[881] | 170 | let m ≝ foldl ?? (λm,idr. add ?? m (\fst idr) (Global (\snd idr))) (empty_map ??) globals in |
---|
[816] | 171 | let m ≝ foldl ?? (λm,v. add ?? m (\fst v) Local) m (fn_params f) in |
---|
| 172 | let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in |
---|
| 173 | let 〈m,stacksize〉 ≝ foldl ?? (λms,v. |
---|
| 174 | let 〈m,stack_high〉 ≝ ms in |
---|
| 175 | let 〈id,ty〉 ≝ v in |
---|
| 176 | let 〈c,stack_high〉 ≝ if always_alloc ty ∨ mem_set ? mem_vars id |
---|
| 177 | then 〈Stack stack_high,stack_high + sizeof ty〉 |
---|
| 178 | else 〈Local, stack_high〉 in |
---|
| 179 | 〈add ?? m id c, stack_high〉) 〈m,0〉 (fn_vars f) in |
---|
| 180 | 〈m,stacksize〉. |
---|
| 181 | |
---|
| 182 | |
---|
| 183 | include "Cminor/syntax.ma". |
---|
| 184 | include "common/Errors.ma". |
---|
| 185 | |
---|
| 186 | alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)". |
---|
| 187 | |
---|
| 188 | axiom UndeclaredIdentifier : String. |
---|
| 189 | axiom BadlyTypedAccess : String. |
---|
| 190 | axiom BadLvalue : String. |
---|
| 191 | axiom MissingField : String. |
---|
| 192 | |
---|
| 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. *) |
---|
| 197 | alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,6,0)". |
---|
| 198 | |
---|
| 199 | definition translate_unop : type → CLunop → res CMunop ≝ |
---|
| 200 | λty.λop:CLunop. |
---|
| 201 | match op with |
---|
| 202 | [ Onotbool ⇒ OK ? CMnotbool |
---|
| 203 | | Onotint ⇒ OK ? Onotint |
---|
| 204 | | Oneg ⇒ |
---|
| 205 | match ty with |
---|
| 206 | [ Tint _ _ ⇒ OK ? Onegint |
---|
| 207 | | Tfloat _ ⇒ OK ? Onegf |
---|
| 208 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 209 | ] |
---|
| 210 | ]. |
---|
| 211 | |
---|
| 212 | definition translate_add ≝ |
---|
[880] | 213 | λty1,e1,ty2,e2,ty'. |
---|
| 214 | let ty1' ≝ typ_of_type ty1 in |
---|
| 215 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 216 | match classify_add ty1 ty2 with |
---|
[880] | 217 | [ add_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oadd e1 e2) |
---|
| 218 | | add_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Oaddf e1 e2) |
---|
[961] | 219 | (* XXX using the integer size for e2 as the offset's size isn't right, because |
---|
| 220 | if e2 produces an 8bit value then the true offset might overflow *) |
---|
| 221 | | add_case_pi ty ⇒ |
---|
| 222 | match ty2' with |
---|
| 223 | [ ASTint sz2 _ ⇒ OK ? (Op2 ty1' ty2' ty' Oaddp e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst sz2 (repr ? (sizeof ty)))))) |
---|
| 224 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
| 225 | ] |
---|
| 226 | | add_case_ip ty ⇒ |
---|
| 227 | match ty1' with |
---|
| 228 | [ ASTint sz1 _ ⇒ OK ? (Op2 ty2' ty1' ty' Oaddp e2 (Op2 ty1' ty1' ty1' Omul e1 (Cst ? (Ointconst sz1 (repr ? (sizeof ty)))))) |
---|
| 229 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
| 230 | ] |
---|
[816] | 231 | | add_default ⇒ Error ? (msg TypeMismatch) |
---|
| 232 | ]. |
---|
| 233 | |
---|
| 234 | definition translate_sub ≝ |
---|
[880] | 235 | λty1,e1,ty2,e2,ty'. |
---|
| 236 | let ty1' ≝ typ_of_type ty1 in |
---|
| 237 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 238 | match classify_sub ty1 ty2 with |
---|
[880] | 239 | [ sub_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Osub e1 e2) |
---|
| 240 | | sub_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Osubf e1 e2) |
---|
[961] | 241 | (* XXX choosing offset sizes? *) |
---|
| 242 | | sub_case_pi ty ⇒ OK ? (Op2 ty1' ty2' ty' Osubpi e1 (Op2 ty2' ty2' ty2' Omul e2 (Cst ? (Ointconst I16 (repr ? (sizeof ty)))))) |
---|
| 243 | | sub_case_pp ty ⇒ |
---|
| 244 | match ty' with (* XXX overflow *) |
---|
| 245 | [ ASTint sz _ ⇒ OK ? (Op2 ty' ty' ty' Odivu (Op2 ty1' ty2' ty' (Osubpp sz) e1 e2) (Cst ? (Ointconst sz (repr ? (sizeof ty))))) |
---|
| 246 | | _ ⇒ Error ? (msg TypeMismatch) (* XXX impossible *) |
---|
| 247 | ] |
---|
[816] | 248 | | sub_default ⇒ Error ? (msg TypeMismatch) |
---|
| 249 | ]. |
---|
| 250 | |
---|
| 251 | definition translate_mul ≝ |
---|
[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_mul ty1 ty2 with |
---|
[880] | 256 | [ mul_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omul e1 e2) |
---|
| 257 | | mul_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Omulf e1 e2) |
---|
[816] | 258 | | mul_default ⇒ Error ? (msg TypeMismatch) |
---|
| 259 | ]. |
---|
| 260 | |
---|
| 261 | definition translate_div ≝ |
---|
[880] | 262 | λty1,e1,ty2,e2,ty'. |
---|
| 263 | let ty1' ≝ typ_of_type ty1 in |
---|
| 264 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 265 | match classify_div ty1 ty2 with |
---|
[961] | 266 | [ div_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Odivu e1 e2) |
---|
[880] | 267 | | div_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Odiv e1 e2) |
---|
| 268 | | div_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' Odivf e1 e2) |
---|
[816] | 269 | | div_default ⇒ Error ? (msg TypeMismatch) |
---|
| 270 | ]. |
---|
| 271 | |
---|
| 272 | definition translate_mod ≝ |
---|
[880] | 273 | λty1,e1,ty2,e2,ty'. |
---|
| 274 | let ty1' ≝ typ_of_type ty1 in |
---|
| 275 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 276 | match classify_mod ty1 ty2 with |
---|
[961] | 277 | [ mod_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Omodu e1 e2) |
---|
[880] | 278 | | mod_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Omod e1 e2) |
---|
[816] | 279 | | mod_default ⇒ Error ? (msg TypeMismatch) |
---|
| 280 | ]. |
---|
| 281 | |
---|
| 282 | definition translate_shr ≝ |
---|
[880] | 283 | λty1,e1,ty2,e2,ty'. |
---|
| 284 | let ty1' ≝ typ_of_type ty1 in |
---|
| 285 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 286 | match classify_shr ty1 ty2 with |
---|
[961] | 287 | [ shr_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' Oshru e1 e2) |
---|
[880] | 288 | | shr_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' Oshr e1 e2) |
---|
[816] | 289 | | shr_default ⇒ Error ? (msg TypeMismatch) |
---|
| 290 | ]. |
---|
| 291 | |
---|
| 292 | definition translate_cmp ≝ |
---|
[880] | 293 | λc,ty1,e1,ty2,e2,ty'. |
---|
| 294 | let ty1' ≝ typ_of_type ty1 in |
---|
| 295 | let ty2' ≝ typ_of_type ty2 in |
---|
[816] | 296 | match classify_cmp ty1 ty2 with |
---|
[880] | 297 | [ cmp_case_I32unsi ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpu c) e1 e2) |
---|
| 298 | | cmp_case_ii ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmp c) e1 e2) |
---|
| 299 | | cmp_case_pp ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpp c) e1 e2) |
---|
| 300 | | cmp_case_ff ⇒ OK ? (Op2 ty1' ty2' ty' (Ocmpf c) e1 e2) |
---|
[816] | 301 | | cmp_default ⇒ Error ? (msg TypeMismatch) |
---|
| 302 | ]. |
---|
| 303 | |
---|
[880] | 304 | definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝ |
---|
| 305 | λop,ty1,e1,ty2,e2,ty. |
---|
| 306 | let ty' ≝ typ_of_type ty in |
---|
[816] | 307 | match op with |
---|
[880] | 308 | [ Oadd ⇒ translate_add ty1 e1 ty2 e2 ty' |
---|
| 309 | | Osub ⇒ translate_sub ty1 e1 ty2 e2 ty' |
---|
| 310 | | Omul ⇒ translate_mul ty1 e1 ty2 e2 ty' |
---|
| 311 | | Omod ⇒ translate_mod ty1 e1 ty2 e2 ty' |
---|
| 312 | | Odiv ⇒ translate_div ty1 e1 ty2 e2 ty' |
---|
| 313 | | Oand ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oand e1 e2) |
---|
| 314 | | Oor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oor e1 e2) |
---|
| 315 | | Oxor ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oxor e1 e2) |
---|
| 316 | | Oshl ⇒ OK ? (Op2 (typ_of_type ty1) (typ_of_type ty2) ty' Oshl e1 e2) |
---|
| 317 | | Oshr ⇒ translate_shr ty1 e1 ty2 e2 ty' |
---|
| 318 | | Oeq ⇒ translate_cmp Ceq ty1 e1 ty2 e2 ty' |
---|
| 319 | | One ⇒ translate_cmp Cne ty1 e1 ty2 e2 ty' |
---|
| 320 | | Olt ⇒ translate_cmp Clt ty1 e1 ty2 e2 ty' |
---|
| 321 | | Ogt ⇒ translate_cmp Cgt ty1 e1 ty2 e2 ty' |
---|
| 322 | | Ole ⇒ translate_cmp Cle ty1 e1 ty2 e2 ty' |
---|
| 323 | | Oge ⇒ translate_cmp Cge ty1 e1 ty2 e2 ty' |
---|
[816] | 324 | ]. |
---|
| 325 | |
---|
[880] | 326 | |
---|
| 327 | (* We'll need to implement proper translation of pointers if we really do memory |
---|
| 328 | spaces. *) |
---|
| 329 | definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝ |
---|
| 330 | λr1,r2,P. |
---|
| 331 | match r1 return λx.P x → res (P r2) with |
---|
| 332 | [ Any ⇒ match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 333 | | Data ⇒ match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 334 | | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 335 | | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 336 | | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 337 | | Code ⇒ match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 338 | ]. |
---|
| 339 | |
---|
| 340 | definition translate_ptr : ∀r1,r2. CMexpr (ASTptr r1) → res (CMexpr (ASTptr r2)) ≝ |
---|
| 341 | λr1,r2,e. check_region r1 r2 ? e. |
---|
| 342 | |
---|
| 343 | definition translate_cast : type → ∀ty2:type. CMexpr ? → res (CMexpr (typ_of_type ty2)) ≝ |
---|
| 344 | λty1,ty2. |
---|
| 345 | match ty1 return λx.CMexpr (typ_of_type x) → ? with |
---|
| 346 | [ Tint sz1 sg1 ⇒ λe. |
---|
| 347 | match ty2 return λx.res (CMexpr (typ_of_type x)) with |
---|
[962] | 348 | [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint sg1 sz2) e) |
---|
[880] | 349 | | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu | _ ⇒ Ofloatofint]) e) |
---|
| 350 | | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint r) e) |
---|
| 351 | | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint r) e) |
---|
[816] | 352 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 353 | ] |
---|
[880] | 354 | | Tfloat sz1 ⇒ λe. |
---|
| 355 | match ty2 return λx.res (CMexpr (typ_of_type x)) with |
---|
[961] | 356 | [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat sz2 | _ ⇒ Ointoffloat sz2 ]) e) |
---|
[880] | 357 | | Tfloat sz2 ⇒ OK ? (Op1 ?? Oid e) (* FIXME *) |
---|
[816] | 358 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 359 | ] |
---|
[880] | 360 | | Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *) |
---|
| 361 | match ty2 return λx.res (CMexpr (typ_of_type x)) with |
---|
[961] | 362 | [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ointofptr sz2) e) |
---|
[880] | 363 | | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e |
---|
| 364 | | Tpointer r2 _ ⇒ translate_ptr r1 r2 e |
---|
[816] | 365 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 366 | ] |
---|
[880] | 367 | | Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *) |
---|
| 368 | match ty2 return λx.res (CMexpr (typ_of_type x)) with |
---|
[961] | 369 | [ Tint sz2 sg2 ⇒ OK ? (Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2) e) |
---|
[880] | 370 | | Tarray r2 _ _ ⇒ translate_ptr r1 r2 e |
---|
| 371 | | Tpointer r2 _ ⇒ translate_ptr r1 r2 e |
---|
[816] | 372 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 373 | ] |
---|
[880] | 374 | | _ ⇒ λ_. Error ? (msg TypeMismatch) |
---|
[816] | 375 | ]. |
---|
| 376 | |
---|
[880] | 377 | definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝ |
---|
| 378 | λty1,ty2,P,p. |
---|
| 379 | do E ← assert_type_eq ty1 ty2; |
---|
| 380 | OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). |
---|
| 381 | |
---|
[881] | 382 | definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2). |
---|
| 383 | * * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
| 384 | qed. |
---|
| 385 | |
---|
[880] | 386 | definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2). |
---|
| 387 | * [ #sz1 #sg1 | #r1 | #sz1 ] |
---|
| 388 | * [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ] |
---|
| 389 | [ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ] |
---|
| 390 | *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
[881] | 391 | | *; #P #p @(region_should_eq r1 ?? p) |
---|
[880] | 392 | | *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
| 393 | ] qed. |
---|
| 394 | |
---|
[881] | 395 | |
---|
| 396 | lemma access_mode_typ : ∀ty,r. access_mode ty = By_reference r → typ_of_type ty = ASTptr r. |
---|
| 397 | * |
---|
| 398 | [ 5: #r #ty #n #r' normalize #E destruct @refl |
---|
| 399 | | 6: #args #ret #r normalize #E destruct @refl |
---|
| 400 | | *: normalize #a #b try #c try #d destruct |
---|
| 401 | [ cases a in d; normalize; cases b; normalize #E destruct |
---|
| 402 | | cases a in c; normalize #E destruct |
---|
| 403 | ] |
---|
| 404 | ] qed. |
---|
| 405 | |
---|
[880] | 406 | let rec translate_expr (vars:var_types) (e:expr) on e : res (CMexpr (typ_of_type (typeof e))) ≝ |
---|
[881] | 407 | match e return λe. res (CMexpr (typ_of_type (typeof e))) with |
---|
[816] | 408 | [ Expr ed ty ⇒ |
---|
| 409 | match ed with |
---|
[961] | 410 | [ Econst_int sz i ⇒ OK ? (Cst ? (Ointconst sz i)) |
---|
[880] | 411 | | Econst_float f ⇒ OK ? (Cst ? (Ofloatconst f)) |
---|
[816] | 412 | | Evar id ⇒ |
---|
| 413 | do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); |
---|
| 414 | match c with |
---|
[881] | 415 | [ Global r ⇒ |
---|
[816] | 416 | match access_mode ty with |
---|
[961] | 417 | [ By_value q ⇒ OK ? (Mem ? r q (Cst ? (Oaddrsymbol id 0))) |
---|
| 418 | | By_reference _ ⇒ OK ? (Cst ? (Oaddrsymbol id 0)) |
---|
[816] | 419 | | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
| 420 | ] |
---|
| 421 | | Stack n ⇒ |
---|
| 422 | match access_mode ty with |
---|
[961] | 423 | [ By_value q ⇒ OK ? (Mem ? Any q (Cst ? (Oaddrstack n))) |
---|
| 424 | | By_reference _ ⇒ OK ? (Cst ? (Oaddrstack n)) |
---|
[816] | 425 | | By_nothing ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
| 426 | ] |
---|
[880] | 427 | | Local ⇒ OK ? (Id ? id) |
---|
[816] | 428 | ] |
---|
| 429 | | Ederef e1 ⇒ |
---|
| 430 | do e1' ← translate_expr vars e1; |
---|
[881] | 431 | match typ_of_type (typeof e1) return λx.CMexpr x → ? with |
---|
| 432 | [ ASTptr r ⇒ λe1'. |
---|
[882] | 433 | match access_mode ty return λx.access_mode ty = x → res (CMexpr (typ_of_type ty)) with |
---|
[881] | 434 | [ By_value q ⇒ λ_.OK ? (Mem (typ_of_type ty) ? q e1') |
---|
| 435 | | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈CMexpr (ASTptr r') ↦ CMexpr (typ_of_type ty)⌉ |
---|
| 436 | | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) |
---|
| 437 | ] (refl ? (access_mode ty)) |
---|
| 438 | | _ ⇒ λ_. Error ? (msg TypeMismatch) |
---|
| 439 | ] e1' |
---|
[880] | 440 | | Eaddrof e1 ⇒ |
---|
| 441 | do e1' ← translate_addr vars e1; |
---|
[881] | 442 | match typ_of_type ty return λx.res (CMexpr x) with |
---|
| 443 | [ ASTptr r ⇒ |
---|
| 444 | match e1' with |
---|
| 445 | [ dp r1 e1' ⇒ region_should_eq r1 r ? e1' |
---|
| 446 | ] |
---|
[880] | 447 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
[816] | 448 | ] |
---|
| 449 | | Eunop op e1 ⇒ |
---|
| 450 | do op' ← translate_unop ty op; |
---|
| 451 | do e1' ← translate_expr vars e1; |
---|
[880] | 452 | OK ? (Op1 ?? op' e1') |
---|
[816] | 453 | | Ebinop op e1 e2 ⇒ |
---|
| 454 | do e1' ← translate_expr vars e1; |
---|
| 455 | do e2' ← translate_expr vars e2; |
---|
[881] | 456 | translate_binop op (typeof e1) e1' (typeof e2) e2' ty |
---|
[816] | 457 | | Ecast ty1 e1 ⇒ |
---|
| 458 | do e1' ← translate_expr vars e1; |
---|
[880] | 459 | do e' ← translate_cast (typeof e1) ty1 e1'; |
---|
[881] | 460 | typ_should_eq ? (typ_of_type ty) ? e' |
---|
[816] | 461 | | Econdition e1 e2 e3 ⇒ |
---|
| 462 | do e1' ← translate_expr vars e1; |
---|
| 463 | do e2' ← translate_expr vars e2; |
---|
[881] | 464 | do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2'; |
---|
[816] | 465 | do e3' ← translate_expr vars e3; |
---|
[881] | 466 | do e3' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e3'; |
---|
[880] | 467 | match typ_of_type (typeof e1) return λx.CMexpr x → ? with |
---|
| 468 | [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' e3') |
---|
| 469 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 470 | ] e1' |
---|
[816] | 471 | | Eandbool e1 e2 ⇒ |
---|
| 472 | do e1' ← translate_expr vars e1; |
---|
| 473 | do e2' ← translate_expr vars e2; |
---|
[961] | 474 | match ty with |
---|
| 475 | [ Tint sz _ ⇒ |
---|
| 476 | do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2'; |
---|
| 477 | match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with |
---|
| 478 | [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' e2' (Cst ? (Ointconst sz (zero ?)))) |
---|
| 479 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 480 | ] e1' |
---|
| 481 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 482 | ] |
---|
[816] | 483 | | Eorbool e1 e2 ⇒ |
---|
| 484 | do e1' ← translate_expr vars e1; |
---|
| 485 | do e2' ← translate_expr vars e2; |
---|
[961] | 486 | match ty with |
---|
| 487 | [ Tint sz _ ⇒ |
---|
| 488 | do e2' ← type_should_eq ? ty (λx.CMexpr (typ_of_type x)) e2'; |
---|
| 489 | match typ_of_type (typeof e1) return λx.CMexpr x → res (CMexpr (typ_of_type ty)) with |
---|
| 490 | [ ASTint _ _ ⇒ λe1'. OK ? (Cond ??? e1' (Cst ? (Ointconst sz (repr ? 1))) e2') |
---|
| 491 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 492 | ] e1' |
---|
| 493 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 494 | ] |
---|
| 495 | | Esizeof ty1 ⇒ |
---|
| 496 | match ty with |
---|
| 497 | [ Tint sz _ ⇒ OK ? (Cst ? (Ointconst sz (repr ? (sizeof ty1)))) |
---|
| 498 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 499 | ] |
---|
[816] | 500 | | Efield e1 id ⇒ |
---|
[880] | 501 | do e' ← match typeof e1 with |
---|
[816] | 502 | [ Tstruct _ fl ⇒ |
---|
| 503 | do e1' ← translate_addr vars e1; |
---|
[881] | 504 | match e1' with |
---|
| 505 | [ dp r e1' ⇒ |
---|
| 506 | do off ← field_offset id fl; |
---|
| 507 | match access_mode ty with |
---|
[961] | 508 | [ By_value q ⇒ OK ? (Mem ? r q (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))) |
---|
| 509 | | By_reference _ ⇒ OK ? (Op2 ? (ASTint I32 Unsigned (* XXX efficiency? *)) ? Oaddp e1' (Cst ? (Ointconst I32 (repr ? off)))) |
---|
[881] | 510 | | By_nothing ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 511 | ] |
---|
[816] | 512 | ] |
---|
| 513 | | Tunion _ _ ⇒ |
---|
| 514 | do e1' ← translate_addr vars e1; |
---|
[881] | 515 | match e1' with |
---|
| 516 | [ dp r e1' ⇒ |
---|
| 517 | match access_mode ty return λx. access_mode ty = x → res (CMexpr (typ_of_type ty)) with |
---|
| 518 | [ By_value q ⇒ λ_. OK ? (Mem ?? q e1') |
---|
| 519 | | By_reference r' ⇒ λE. (region_should_eq r r' ? e1')⌈res (CMexpr (ASTptr r')) ↦ res (CMexpr (typ_of_type ty))⌉ |
---|
| 520 | | By_nothing ⇒ λ_. Error ? (msg BadlyTypedAccess) |
---|
| 521 | ] (refl ? (access_mode ty)) |
---|
[816] | 522 | ] |
---|
| 523 | | _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
[880] | 524 | ]; |
---|
[881] | 525 | typ_should_eq ? (typ_of_type ty) ? e' |
---|
[816] | 526 | | Ecost l e1 ⇒ |
---|
| 527 | do e1' ← translate_expr vars e1; |
---|
[880] | 528 | do e' ← OK ? (Ecost ? l e1'); |
---|
[881] | 529 | typ_should_eq ? (typ_of_type ty) ? e' |
---|
[816] | 530 | ] |
---|
[881] | 531 | ] and translate_addr (vars:var_types) (e:expr) on e : res (Σr.CMexpr (ASTptr r)) ≝ |
---|
[816] | 532 | match e with |
---|
| 533 | [ Expr ed _ ⇒ |
---|
| 534 | match ed with |
---|
| 535 | [ Evar id ⇒ |
---|
| 536 | do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); |
---|
[881] | 537 | match c return λ_. res (Σr.CMexpr (ASTptr r)) with |
---|
[961] | 538 | [ Global r ⇒ OK ? (dp ?? r (Cst ? (Oaddrsymbol id 0))) |
---|
| 539 | | Stack n ⇒ OK ? (dp ?? Any (Cst ? (Oaddrstack n))) |
---|
[816] | 540 | | Local ⇒ Error ? (msg BadlyTypedAccess) (* TODO: could rule out? *) |
---|
| 541 | ] |
---|
[880] | 542 | | Ederef e1 ⇒ |
---|
| 543 | do e1' ← translate_expr vars e1; |
---|
[881] | 544 | match typ_of_type (typeof e1) return λx. CMexpr x → res (Σr. CMexpr (ASTptr r)) with |
---|
| 545 | [ ASTptr r ⇒ λe1'.OK ? (dp ?? r e1') |
---|
[880] | 546 | | _ ⇒ λ_.Error ? (msg BadlyTypedAccess) |
---|
| 547 | ] e1' |
---|
[816] | 548 | | Efield e1 id ⇒ |
---|
| 549 | match typeof e1 with |
---|
| 550 | [ Tstruct _ fl ⇒ |
---|
| 551 | do e1' ← translate_addr vars e1; |
---|
| 552 | do off ← field_offset id fl; |
---|
[881] | 553 | match e1' with |
---|
[961] | 554 | [ dp r e1' ⇒ OK ? (dp ?? r (Op2 (ASTptr r) (ASTint I32 Unsigned (* FIXME inefficient?*)) (ASTptr r) Oaddp e1' (Cst ? (Ointconst I32 (repr ? off))))) |
---|
[881] | 555 | ] |
---|
[816] | 556 | | Tunion _ _ ⇒ translate_addr vars e1 |
---|
| 557 | | _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 558 | ] |
---|
| 559 | | _ ⇒ Error ? (msg BadLvalue) |
---|
| 560 | ] |
---|
| 561 | ]. |
---|
[881] | 562 | >(access_mode_typ … E) @refl |
---|
| 563 | qed. |
---|
[816] | 564 | |
---|
| 565 | inductive destination : Type[0] ≝ |
---|
| 566 | | IdDest : ident → destination |
---|
[881] | 567 | | MemDest : ∀r:region. memory_chunk → CMexpr (ASTptr r) → destination. |
---|
[816] | 568 | |
---|
| 569 | definition translate_dest ≝ |
---|
| 570 | λvars,e1,ty2. |
---|
| 571 | do q ← match access_mode ty2 with |
---|
| 572 | [ By_value q ⇒ OK ? q |
---|
| 573 | | By_reference r ⇒ OK ? (Mpointer r) |
---|
| 574 | | By_nothing ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 575 | ]; |
---|
| 576 | match e1 with |
---|
| 577 | [ Expr ed1 ty1 ⇒ |
---|
| 578 | match ed1 with |
---|
| 579 | [ Evar id ⇒ |
---|
| 580 | do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); |
---|
| 581 | match c with |
---|
| 582 | [ Local ⇒ OK ? (IdDest id) |
---|
[961] | 583 | | Global r ⇒ OK ? (MemDest r q (Cst ? (Oaddrsymbol id 0))) |
---|
| 584 | | Stack n ⇒ OK ? (MemDest Any q (Cst ? (Oaddrstack n))) |
---|
[816] | 585 | ] |
---|
| 586 | | _ ⇒ |
---|
| 587 | do e1' ← translate_addr vars e1; |
---|
[881] | 588 | match e1' with [ dp r e1' ⇒ OK ? (MemDest r q e1') ] |
---|
[816] | 589 | ] |
---|
| 590 | ]. |
---|
| 591 | (* |
---|
| 592 | definition translate_assign ≝ |
---|
| 593 | λvars,e1,e2. |
---|
| 594 | do e2' ← translate_expr vars e2; |
---|
| 595 | do q ← match access_mode (typeof e2) with |
---|
| 596 | [ By_value q ⇒ OK ? q |
---|
| 597 | | By_reference r ⇒ OK ? (Mpointer r) |
---|
| 598 | | By_nothing ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 599 | ]; |
---|
| 600 | match e1 with |
---|
| 601 | [ Expr ed1 ty1 ⇒ |
---|
| 602 | match ed1 with |
---|
| 603 | [ Evar id ⇒ |
---|
| 604 | do c ← opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id); |
---|
| 605 | match c with |
---|
| 606 | [ Local ⇒ OK ? (St_assign id e2') |
---|
| 607 | | Global ⇒ OK ? (St_store q (Cst (Oaddrsymbol id zero)) e2') |
---|
| 608 | | Stack n ⇒ OK ? (St_store q (Cst (Oaddrstack (repr n))) e2') |
---|
| 609 | ] |
---|
| 610 | | _ ⇒ |
---|
| 611 | do e1' ← translate_addr vars e1; |
---|
| 612 | OK ? (St_store q e1' e2') |
---|
| 613 | ] |
---|
| 614 | ]. |
---|
| 615 | *) |
---|
| 616 | definition translate_assign ≝ |
---|
| 617 | λvars,e1,e2. |
---|
| 618 | do e2' ← translate_expr vars e2; |
---|
| 619 | do dest ← translate_dest vars e1 (typeof e2); |
---|
| 620 | match dest with |
---|
[880] | 621 | [ IdDest id ⇒ OK ? (St_assign ? id e2') |
---|
[881] | 622 | | MemDest r q e1' ⇒ OK ? (St_store ? r q e1' e2') |
---|
[816] | 623 | ]. |
---|
| 624 | |
---|
| 625 | definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝ |
---|
| 626 | λA,B,f,oa. |
---|
| 627 | match oa with |
---|
| 628 | [ None ⇒ OK ? (None ?) |
---|
| 629 | | Some a ⇒ do b ← f a; OK ? (Some ? b) |
---|
| 630 | ]. |
---|
| 631 | |
---|
[880] | 632 | definition translate_expr_sigma : var_types → expr → res (Σt:typ.CMexpr t) ≝ |
---|
| 633 | λv,e. |
---|
| 634 | do e' ← translate_expr v e; |
---|
| 635 | OK ? (dp ? (λt:typ.CMexpr t) ? e'). |
---|
| 636 | |
---|
[816] | 637 | axiom FIXME : String. |
---|
| 638 | |
---|
| 639 | let rec translate_statement (vars:var_types) (tmp:ident) (tmpp:ident) (s:statement) on s : res stmt ≝ |
---|
| 640 | match s with |
---|
| 641 | [ Sskip ⇒ OK ? St_skip |
---|
| 642 | | Sassign e1 e2 ⇒ translate_assign vars e1 e2 |
---|
| 643 | | Scall ret ef args ⇒ |
---|
| 644 | do ef' ← translate_expr vars ef; |
---|
[880] | 645 | do ef' ← typ_should_eq ? (ASTptr Code) ? ef'; |
---|
| 646 | do args' ← mmap … (translate_expr_sigma vars) args; |
---|
[816] | 647 | match ret with |
---|
| 648 | [ None ⇒ OK ? (St_call (None ?) ef' args') |
---|
| 649 | | Some e1 ⇒ |
---|
| 650 | do dest ← translate_dest vars e1 (typeof e1); (* TODO: check if it's sane to use e1's type rather than the return type *) |
---|
| 651 | match dest with |
---|
| 652 | [ IdDest id ⇒ OK ? (St_call (Some ? id) ef' args') |
---|
[881] | 653 | | MemDest r q e1' ⇒ |
---|
[816] | 654 | let tmp' ≝ match q with [ Mpointer _ ⇒ tmpp | _ ⇒ tmp ] in |
---|
[881] | 655 | OK ? (St_seq (St_call (Some ? tmp) ef' args') (St_store (typ_of_memory_chunk q) r q e1' (Id ? tmp))) |
---|
[816] | 656 | ] |
---|
| 657 | ] |
---|
| 658 | | Ssequence s1 s2 ⇒ |
---|
| 659 | do s1' ← translate_statement vars tmp tmpp s1; |
---|
| 660 | do s2' ← translate_statement vars tmp tmpp s2; |
---|
| 661 | OK ? (St_seq s1' s2') |
---|
| 662 | | Sifthenelse e1 s1 s2 ⇒ |
---|
| 663 | do e1' ← translate_expr vars e1; |
---|
[880] | 664 | match typ_of_type (typeof e1) return λx.CMexpr x → ? with |
---|
| 665 | [ ASTint _ _ ⇒ λe1'. |
---|
| 666 | do s1' ← translate_statement vars tmp tmpp s1; |
---|
| 667 | do s2' ← translate_statement vars tmp tmpp s2; |
---|
| 668 | OK ? (St_ifthenelse ?? e1' s1' s2') |
---|
| 669 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 670 | ] e1' |
---|
[816] | 671 | | Swhile e1 s1 ⇒ |
---|
| 672 | do e1' ← translate_expr vars e1; |
---|
[880] | 673 | match typ_of_type (typeof e1) return λx.CMexpr x → ? with |
---|
| 674 | [ ASTint _ _ ⇒ λe1'. |
---|
| 675 | do s1' ← translate_statement vars tmp tmpp s1; |
---|
| 676 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
| 677 | OK ? (St_block |
---|
| 678 | (St_loop |
---|
| 679 | (St_ifthenelse ?? e1' (St_block s1') (St_exit 0)))) |
---|
| 680 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 681 | ] e1' |
---|
[816] | 682 | | Sdowhile e1 s1 ⇒ |
---|
| 683 | do e1' ← translate_expr vars e1; |
---|
[880] | 684 | match typ_of_type (typeof e1) return λx.CMexpr x → ? with |
---|
| 685 | [ ASTint _ _ ⇒ λe1'. |
---|
| 686 | do s1' ← translate_statement vars tmp tmpp s1; |
---|
| 687 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
| 688 | OK ? (St_block |
---|
| 689 | (St_loop |
---|
| 690 | (St_seq (St_block s1') (St_ifthenelse ?? e1' St_skip (St_exit 0))))) |
---|
| 691 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 692 | ] e1' |
---|
[816] | 693 | | Sfor s1 e1 s2 s3 ⇒ |
---|
| 694 | do e1' ← translate_expr vars e1; |
---|
[880] | 695 | match typ_of_type (typeof e1) return λx.CMexpr x → ? with |
---|
| 696 | [ ASTint _ _ ⇒ λe1'. |
---|
| 697 | do s1' ← translate_statement vars tmp tmpp s1; |
---|
| 698 | do s2' ← translate_statement vars tmp tmpp s2; |
---|
| 699 | do s3' ← translate_statement vars tmp tmpp s3; |
---|
| 700 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
| 701 | OK ? (St_seq s1' |
---|
| 702 | (St_block |
---|
| 703 | (St_loop |
---|
| 704 | (St_ifthenelse ?? e1' (St_seq (St_block s3') s2') (St_exit 0))))) |
---|
| 705 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 706 | ] e1' |
---|
[816] | 707 | | Sbreak ⇒ OK ? (St_exit 1) |
---|
| 708 | | Scontinue ⇒ OK ? (St_exit 0) |
---|
| 709 | | Sreturn ret ⇒ |
---|
[880] | 710 | match ret with |
---|
| 711 | [ None ⇒ OK ? (St_return (None ?)) |
---|
| 712 | | Some e1 ⇒ |
---|
| 713 | do e1' ← translate_expr vars e1; |
---|
| 714 | OK ? (St_return (Some ? (dp … e1'))) |
---|
| 715 | ] |
---|
[816] | 716 | | Sswitch e1 ls ⇒ Error ? (msg FIXME) |
---|
| 717 | | Slabel l s1 ⇒ |
---|
| 718 | do s1' ← translate_statement vars tmp tmpp s1; |
---|
| 719 | OK ? (St_label l s1') |
---|
| 720 | | Sgoto l ⇒ OK ? (St_goto l) |
---|
| 721 | | Scost l s1 ⇒ |
---|
| 722 | do s1' ← translate_statement vars tmp tmpp s1; |
---|
| 723 | OK ? (St_cost l s1') |
---|
| 724 | ]. |
---|
| 725 | |
---|
| 726 | |
---|
| 727 | definition bigid1 ≝ an_identifier SymbolTag [[ |
---|
| 728 | false;true;false;false; |
---|
| 729 | false;false;false;false; |
---|
| 730 | false;false;false;false; |
---|
| 731 | false;false;false;false]]. |
---|
| 732 | definition bigid2 ≝ an_identifier SymbolTag [[ |
---|
| 733 | false;true;false;false; |
---|
| 734 | false;false;false;false; |
---|
| 735 | false;false;false;false; |
---|
| 736 | false;false;false;true]]. |
---|
| 737 | |
---|
[886] | 738 | (* FIXME: the temporary handling is nonsense, I'm afraid. *) |
---|
[881] | 739 | definition translate_function : list (ident×region) → function → res internal_function ≝ |
---|
[816] | 740 | λglobals, f. |
---|
| 741 | let 〈vartypes, stacksize〉 ≝ characterise_vars globals f in |
---|
| 742 | let tmp ≝ bigid1 in (* FIXME *) |
---|
| 743 | let tmpp ≝ bigid2 in (* FIXME *) |
---|
| 744 | do s ← translate_statement vartypes tmp tmpp (fn_body f); |
---|
| 745 | OK ? (mk_internal_function |
---|
[886] | 746 | (opttyp_of_type (fn_return f)) |
---|
| 747 | (map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f)) |
---|
| 748 | (〈tmp,ASTint I32 Unsigned〉::〈tmpp,ASTptr Any〉::(map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_vars f))) |
---|
[816] | 749 | stacksize |
---|
| 750 | s). |
---|
| 751 | |
---|
[881] | 752 | definition translate_fundef : list (ident×region) → clight_fundef → res (fundef internal_function) ≝ |
---|
[816] | 753 | λglobals,f. |
---|
| 754 | match f with |
---|
| 755 | [ CL_Internal fn ⇒ do fn' ← translate_function globals fn; OK ? (Internal ? fn') |
---|
| 756 | | CL_External fn argtys retty ⇒ OK ? (External ? (mk_external_function fn (signature_of_type argtys retty))) |
---|
| 757 | ]. |
---|
| 758 | |
---|
| 759 | definition clight_to_cminor : clight_program → res Cminor_program ≝ |
---|
| 760 | λp. |
---|
[881] | 761 | let fun_globals ≝ map … (λid. 〈id,Code〉) (prog_funct_names ?? p) in |
---|
| 762 | let var_globals ≝ map … (λv. 〈\fst (\fst (\fst v)), \snd (\fst v)〉) (prog_vars ?? p) in |
---|
| 763 | let globals ≝ fun_globals @ var_globals in |
---|
[961] | 764 | transform_partial_program2 ???? (translate_fundef globals) (λ_. OK ? it) p. |
---|