[1872] | 1 | include "Clight/ClassifyOp.ma". |
---|
[1605] | 2 | include "basics/lists/list.ma". |
---|
[1629] | 3 | include "Clight/fresh.ma". |
---|
[816] | 4 | |
---|
[1194] | 5 | (* Identify local variables that must be allocated memory. *) |
---|
[1871] | 6 | (* These are the variables whose addresses are taken. *) |
---|
[816] | 7 | let rec gather_mem_vars_expr (e:expr) : identifier_set SymbolTag ≝ |
---|
| 8 | match e with |
---|
| 9 | [ Expr ed ty ⇒ |
---|
| 10 | match ed with |
---|
| 11 | [ Ederef e1 ⇒ gather_mem_vars_expr e1 |
---|
| 12 | | Eaddrof e1 ⇒ gather_mem_vars_addr e1 |
---|
| 13 | | Eunop _ e1 ⇒ gather_mem_vars_expr e1 |
---|
| 14 | | Ebinop _ e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 15 | gather_mem_vars_expr e2 |
---|
| 16 | | Ecast _ e1 ⇒ gather_mem_vars_expr e1 |
---|
| 17 | | Econdition e1 e2 e3 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 18 | gather_mem_vars_expr e2 ∪ |
---|
| 19 | gather_mem_vars_expr e3 |
---|
| 20 | | Eandbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 21 | gather_mem_vars_expr e2 |
---|
| 22 | | Eorbool e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 23 | gather_mem_vars_expr e2 |
---|
| 24 | | Efield e1 _ ⇒ gather_mem_vars_expr e1 |
---|
| 25 | | Ecost _ e1 ⇒ gather_mem_vars_expr e1 |
---|
| 26 | | _ ⇒ ∅ |
---|
| 27 | ] |
---|
| 28 | ] |
---|
| 29 | and gather_mem_vars_addr (e:expr) : identifier_set SymbolTag ≝ |
---|
| 30 | match e with |
---|
| 31 | [ Expr ed ty ⇒ |
---|
| 32 | match ed with |
---|
| 33 | [ Evar x ⇒ { (x) } |
---|
| 34 | | Ederef e1 ⇒ gather_mem_vars_expr e1 |
---|
| 35 | | Efield e1 _ ⇒ gather_mem_vars_addr e1 |
---|
| 36 | | _ ⇒ ∅ (* not an lvalue *) |
---|
| 37 | ] |
---|
| 38 | ]. |
---|
| 39 | |
---|
| 40 | let rec gather_mem_vars_stmt (s:statement) : identifier_set SymbolTag ≝ |
---|
| 41 | match s with |
---|
| 42 | [ Sskip ⇒ ∅ |
---|
| 43 | | Sassign e1 e2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 44 | gather_mem_vars_expr e2 |
---|
| 45 | | Scall oe1 e2 es ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] ∪ |
---|
| 46 | gather_mem_vars_expr e2 ∪ |
---|
| 47 | (foldl ?? (λs,e. s ∪ gather_mem_vars_expr e) ∅ es) |
---|
| 48 | | Ssequence s1 s2 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
| 49 | gather_mem_vars_stmt s2 |
---|
| 50 | | Sifthenelse e1 s1 s2 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 51 | gather_mem_vars_stmt s1 ∪ |
---|
| 52 | gather_mem_vars_stmt s2 |
---|
| 53 | | Swhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 54 | gather_mem_vars_stmt s1 |
---|
| 55 | | Sdowhile e1 s1 ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 56 | gather_mem_vars_stmt s1 |
---|
| 57 | | Sfor s1 e1 s2 s3 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
| 58 | gather_mem_vars_expr e1 ∪ |
---|
| 59 | gather_mem_vars_stmt s2 ∪ |
---|
| 60 | gather_mem_vars_stmt s3 |
---|
| 61 | | Sbreak ⇒ ∅ |
---|
| 62 | | Scontinue ⇒ ∅ |
---|
| 63 | | Sreturn oe1 ⇒ match oe1 with [ None ⇒ ∅ | Some e1 ⇒ gather_mem_vars_expr e1 ] |
---|
| 64 | | Sswitch e1 ls ⇒ gather_mem_vars_expr e1 ∪ |
---|
| 65 | gather_mem_vars_ls ls |
---|
| 66 | | Slabel _ s1 ⇒ gather_mem_vars_stmt s1 |
---|
| 67 | | Sgoto _ ⇒ ∅ |
---|
| 68 | | Scost _ s1 ⇒ gather_mem_vars_stmt s1 |
---|
| 69 | ] |
---|
| 70 | and gather_mem_vars_ls (ls:labeled_statements) on ls : identifier_set SymbolTag ≝ |
---|
| 71 | match ls with |
---|
| 72 | [ LSdefault s1 ⇒ gather_mem_vars_stmt s1 |
---|
[961] | 73 | | LScase _ _ s1 ls1 ⇒ gather_mem_vars_stmt s1 ∪ |
---|
| 74 | gather_mem_vars_ls ls1 |
---|
[816] | 75 | ]. |
---|
| 76 | |
---|
[1871] | 77 | (* Defines where a variable should be allocated. *) |
---|
[816] | 78 | inductive var_type : Type[0] ≝ |
---|
[1871] | 79 | | Global : region → var_type (* A global, allocated statically in a given region (which one ???) *) |
---|
| 80 | | Stack : nat → var_type (* On the stack, at a given height *) |
---|
| 81 | | Local : var_type (* Locally (hopefully, in a register) *) |
---|
[816] | 82 | . |
---|
| 83 | |
---|
[1871] | 84 | (* A map associating each variable identifier to its allocation mode and its type. *) |
---|
[1626] | 85 | definition var_types ≝ identifier_map SymbolTag (var_type × type). |
---|
[816] | 86 | |
---|
[1316] | 87 | axiom UndeclaredIdentifier : String. |
---|
| 88 | |
---|
| 89 | definition lookup' ≝ |
---|
| 90 | λvars:var_types.λid. opt_to_res … [MSG UndeclaredIdentifier; CTX ? id] (lookup ?? vars id). |
---|
| 91 | |
---|
[1626] | 92 | (* Assert that an identifier is a local variable with the given typ. *) |
---|
| 93 | definition local_id : var_types → ident → typ → Prop ≝ |
---|
| 94 | λvars,id,t. match lookup' vars id with [ OK vt ⇒ match (\fst vt) with [ Global _ ⇒ False | _ ⇒ t = typ_of_type (\snd vt) ] | _ ⇒ False ]. |
---|
[1316] | 95 | |
---|
[816] | 96 | (* Note that the semantics allows locals to shadow globals. |
---|
| 97 | Parameters start out as locals, but get stack allocated if their address |
---|
| 98 | is taken. We will add code to store them if that's the case. |
---|
| 99 | *) |
---|
| 100 | |
---|
[1871] | 101 | (* Some kind of data is never allocated in registers, even if it fits, typically structured data. *) |
---|
[816] | 102 | definition always_alloc : type → bool ≝ |
---|
| 103 | λt. match t with |
---|
| 104 | [ Tarray _ _ _ ⇒ true |
---|
| 105 | | Tstruct _ _ ⇒ true |
---|
| 106 | | Tunion _ _ ⇒ true |
---|
| 107 | | _ ⇒ false |
---|
| 108 | ]. |
---|
| 109 | |
---|
[1871] | 110 | (* This builds a [var_types] map characterizing the allocation mode, of variables, |
---|
| 111 | * and it returns a stack usage for the function (in bytes, according to [sizeof]) *) |
---|
[1626] | 112 | definition characterise_vars : list (ident×region×type) → function → var_types × nat ≝ |
---|
[816] | 113 | λglobals, f. |
---|
[1871] | 114 | (* globals are added into a map, with var_type Global, region π_2(idrt) and type π_3(idrt) *) |
---|
[1626] | 115 | let m ≝ foldr ?? (λidrt,m. add ?? m (\fst (\fst idrt)) 〈Global (\snd (\fst idrt)), \snd idrt〉) (empty_map ??) globals in |
---|
[1871] | 116 | (* variables in the body of the function are gathered in [mem_vars] *) |
---|
[816] | 117 | let mem_vars ≝ gather_mem_vars_stmt (fn_body f) in |
---|
[1871] | 118 | (* iterate on the parameters and local variables of the function, with a tuple (map, stack_high) as an accumulator *) |
---|
[1316] | 119 | let 〈m,stacksize〉 ≝ foldr ?? (λv,ms. |
---|
[1871] | 120 | let 〈m,stack_high〉 ≝ ms in |
---|
| 121 | let 〈id,ty〉 ≝ v in |
---|
| 122 | let 〈c,stack_high〉 ≝ |
---|
| 123 | (* if the (local, parameter) variable is of a compound type OR if its adress is taken, we allocate it on the stack. *) |
---|
[1884] | 124 | if always_alloc ty ∨ id ∈ mem_vars then |
---|
[1871] | 125 | 〈Stack stack_high,stack_high + sizeof ty〉 |
---|
| 126 | else |
---|
| 127 | 〈Local, stack_high〉 |
---|
| 128 | in |
---|
[1626] | 129 | 〈add ?? m id 〈c, ty〉, stack_high〉) 〈m,0〉 (fn_params f @ fn_vars f) in |
---|
[816] | 130 | 〈m,stacksize〉. |
---|
| 131 | |
---|
[1871] | 132 | (* A local variable id' status is not modified by the removal of a global variable id : id' is still local *) |
---|
[1626] | 133 | lemma local_id_add_global : ∀vars,id,r,t,id',t'. |
---|
| 134 | local_id (add ?? vars id 〈Global r, t〉) id' t' → local_id vars id' t'. |
---|
| 135 | #var #id #r #t #id' #t' |
---|
[1516] | 136 | whd in ⊢ (% → ?); whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?] → ?); |
---|
[1316] | 137 | cases (identifier_eq ? id id') |
---|
[1516] | 138 | [ #E >E >lookup_add_hit whd in ⊢ (% → ?); * |
---|
[1515] | 139 | | #NE >lookup_add_miss /2/ |
---|
[1316] | 140 | ] qed. |
---|
[816] | 141 | |
---|
[1871] | 142 | (* If I add a variable id ≠ id', then id' is still local *) |
---|
[1626] | 143 | lemma local_id_add_miss : ∀vars,id,vt,id',t'. |
---|
| 144 | id ≠ id' → local_id (add ?? vars id vt) id' t' → local_id vars id' t'. |
---|
| 145 | #vars #id #vt #id' #t' #NE |
---|
[1516] | 146 | whd in ⊢ (% → %); |
---|
| 147 | whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ] → match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
[1316] | 148 | >lookup_add_miss |
---|
[1515] | 149 | [ #H @H | /2/ ] |
---|
[1316] | 150 | qed. |
---|
| 151 | |
---|
[1871] | 152 | (* After characterise_vars, a variable in the resulting map is either a global or a "local"(register or stack allocated) *) |
---|
[1629] | 153 | lemma characterise_vars_src : ∀gl,f,vars,n. |
---|
| 154 | characterise_vars gl f = 〈vars,n〉 → |
---|
[1871] | 155 | ∀id. present ?? vars id → |
---|
[1629] | 156 | (∃r,ty. lookup' vars id = OK ? 〈Global r,ty〉 ∧ Exists ? (λx.x = 〈〈id,r〉,ty〉) gl) ∨ |
---|
| 157 | ∃t.local_id vars id t. |
---|
| 158 | #globals #f |
---|
| 159 | whd in ⊢ (∀_.∀_.??%? → ?); |
---|
| 160 | elim (fn_params f @ fn_vars f) |
---|
| 161 | [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #H %1 |
---|
| 162 | elim globals in H ⊢ %; |
---|
| 163 | [ normalize * #H cases (H (refl ??)) |
---|
| 164 | | * * #id #rg #ty #tl #IH #H |
---|
| 165 | cases (identifier_eq ? i id) |
---|
| 166 | [ #E <E %{rg} %{ty} % [ whd in ⊢ (??%?); >lookup_add_hit // | %1 // ] |
---|
| 167 | | #NE cases (IH ?) |
---|
| 168 | [ #rg' * #ty' * #H1 #H2 %{rg'} %{ty'} % |
---|
| 169 | [ whd in ⊢ (??%?); >lookup_add_miss [ @H1 | @NE ] |
---|
| 170 | | %2 @H2 |
---|
| 171 | ] |
---|
| 172 | | whd in H ⊢ %; >lookup_add_miss in H; // |
---|
| 173 | ] |
---|
| 174 | ] |
---|
| 175 | ] |
---|
| 176 | | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i |
---|
| 177 | #H >(contract_pair var_types nat ?) in E; |
---|
| 178 | whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); |
---|
[1884] | 179 | cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); |
---|
[1629] | 180 | #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2 |
---|
| 181 | cases (identifier_eq ? i id) |
---|
| 182 | [ 1,3: #E' <E' in EQ2:%; #EQ2 %2 %{(typ_of_type ty)} |
---|
| 183 | destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?]); |
---|
| 184 | >lookup_add_hit @refl |
---|
| 185 | | *: #NE cases (IH m0 n0 ? i ?) |
---|
| 186 | [ 1,5: * #rg' * #ty' * #H1 #H2 %1 %{rg'} %{ty'} % // |
---|
| 187 | destruct (EQ2) whd in ⊢ (??%?); >lookup_add_miss try @NE @H1 |
---|
| 188 | | 2,6: * #t #H1 %2 %{t} destruct (EQ2) whd whd in ⊢ (match % with [_ ⇒ ?|_ ⇒ ?]); |
---|
| 189 | >lookup_add_miss // |
---|
| 190 | | 3,7: <EQ @refl |
---|
| 191 | | *: destruct (EQ2) whd in H; >lookup_add_miss in H; // |
---|
| 192 | ] |
---|
| 193 | ] |
---|
| 194 | ] qed. |
---|
| 195 | |
---|
[1871] | 196 | (* A local variable in a function is either a parameter or a "local" (:=register or stack alloc'd) |
---|
| 197 | * variable, with the right type *) |
---|
[1316] | 198 | lemma characterise_vars_all : ∀l,f,vars,n. |
---|
| 199 | characterise_vars l f = 〈vars,n〉 → |
---|
[1626] | 200 | ∀i,t. local_id vars i t → |
---|
| 201 | Exists ? (λx.\fst x = i ∧ typ_of_type (\snd x) = t) (fn_params f @ fn_vars f). |
---|
[1316] | 202 | #globals #f |
---|
[1516] | 203 | whd in ⊢ (∀_.∀_.??%? → ?); |
---|
[1316] | 204 | elim (fn_params f @ fn_vars f) |
---|
[1626] | 205 | [ #vars #n whd in ⊢ (??%? → ?); #E destruct #i #t #H @False_ind |
---|
[1516] | 206 | elim globals in H; |
---|
[1316] | 207 | [ normalize // |
---|
[1626] | 208 | | * * #id #rg #t #tl #IH whd in ⊢ (?%?? → ?); #H @IH @(local_id_add_global … H) |
---|
[1316] | 209 | ] |
---|
[1626] | 210 | | * #id #ty #tl #IH #vars #n whd in ⊢ (??(match % with [ _ ⇒ ? ])? → ?); #E #i #t |
---|
| 211 | |
---|
| 212 | #H >(contract_pair var_types nat ?) in E; |
---|
| 213 | whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); |
---|
[1884] | 214 | cases (always_alloc ty ∨ id ∈ ?) whd in ⊢ (??(match ? with [ _ ⇒ (λ_.λ_.%) ])? → ?); |
---|
[1626] | 215 | #H' lapply (extract_pair ???????? H') -H' * #m0 * #n0 * #EQ #EQ2 |
---|
| 216 | |
---|
[1316] | 217 | cases (identifier_eq ? id i) |
---|
[1626] | 218 | [ 1,3: #E' >E' in EQ2:%; #EQ2 % % |
---|
| 219 | [ 1,3: @refl |
---|
| 220 | | *: destruct (EQ2) change with (add ?????) in H:(?%??); |
---|
| 221 | whd in H; whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]); >lookup_add_hit in H; |
---|
| 222 | whd in ⊢ (% → ?); #E'' >E'' @refl |
---|
| 223 | ] |
---|
| 224 | | *: #NE %2 @(IH m0 n0) |
---|
[1516] | 225 | [ 1,3: @sym_eq whd in ⊢ (???(match ?????% with [ _ ⇒ ? ])); >contract_pair @EQ |
---|
[1351] | 226 | | 2,4: destruct (EQ2) @(local_id_add_miss … H) @NE |
---|
[1316] | 227 | ] |
---|
| 228 | ] |
---|
| 229 | ] qed. |
---|
| 230 | |
---|
[1871] | 231 | (* The map generated by characterise_vars is "correct" wrt the fresh ident generator of tag [u], |
---|
| 232 | i.e. by generating fresh idents with u, we risk no collision with the idents in the map domain. *) |
---|
[1629] | 233 | lemma characterise_vars_fresh : ∀gl,f,vars,n,u. |
---|
[1871] | 234 | characterise_vars gl f = 〈vars,n〉 → (* If we generate a map ... *) |
---|
| 235 | globals_fresh_for_univ ? gl u → (* and the globals are out of the idents generated by u *) |
---|
| 236 | fn_fresh_for_univ f u → (* and the variables of the function f are cool with u too ... *) |
---|
| 237 | fresh_map_for_univ … vars u. (* then there won't be collisions between the map and idents made from u *) |
---|
[1629] | 238 | #gl #f #vars #n #u #CH #GL #FN |
---|
| 239 | #id #H |
---|
| 240 | cases (characterise_vars_src … CH … H) |
---|
| 241 | [ * #rg * #ty * #H1 #H2 |
---|
| 242 | cases (Exists_All … H2 GL) * * #id' #rg' #ty' * #E #H destruct // |
---|
| 243 | | * #t #H lapply (characterise_vars_all … CH id t H) #EX |
---|
| 244 | cases (Exists_All … EX FN) * #id' #ty' * * #E1 #E2 #H' -H destruct // |
---|
| 245 | ] qed. |
---|
| 246 | |
---|
[816] | 247 | include "Cminor/syntax.ma". |
---|
| 248 | include "common/Errors.ma". |
---|
| 249 | |
---|
| 250 | alias id "CMexpr" = "cic:/matita/cerco/Cminor/syntax/expr.ind(1,0,0)". |
---|
| 251 | |
---|
| 252 | axiom BadlyTypedAccess : String. |
---|
| 253 | axiom BadLvalue : String. |
---|
| 254 | axiom MissingField : String. |
---|
| 255 | |
---|
[1871] | 256 | (* type_should_eq enforces that two types are equal and eliminates this equality by |
---|
| 257 | transporting P ty1 to P ty2. If ty1 != ty2, then Error *) |
---|
[1369] | 258 | definition type_should_eq : ∀ty1,ty2. ∀P:type → Type[0]. P ty1 → res (P ty2) ≝ |
---|
| 259 | λty1,ty2,P,p. |
---|
| 260 | do E ← assert_type_eq ty1 ty2; |
---|
[1871] | 261 | OK ? (match E return λx.λ_. P ty1 → P x with [ refl ⇒ λp.p ] p). |
---|
[1369] | 262 | |
---|
[1871] | 263 | (* same gig for regions *) |
---|
[1369] | 264 | definition region_should_eq : ∀r1,r2. ∀P:region → Type[0]. P r1 → res (P r2). |
---|
| 265 | * * #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
| 266 | qed. |
---|
| 267 | |
---|
[1871] | 268 | (* same gig for AST typs *) |
---|
[1369] | 269 | definition typ_should_eq : ∀ty1,ty2. ∀P:typ → Type[0]. P ty1 → res (P ty2). |
---|
| 270 | * [ #sz1 #sg1 | #r1 | #sz1 ] |
---|
| 271 | * [ 1,5,9: | *: #a #b #c try #d @(Error ? (msg TypeMismatch)) ] |
---|
| 272 | [ *; cases sz1 [ 1,5,9: | *: #a #b #c @(Error ? (msg TypeMismatch)) ] |
---|
| 273 | *; cases sg1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
| 274 | | *; #P #p @(region_should_eq r1 ?? p) |
---|
| 275 | | *; cases sz1 #P #p try @(OK ? p) @(Error ? (msg TypeMismatch)) |
---|
| 276 | ] qed. |
---|
| 277 | |
---|
[816] | 278 | alias id "CLunop" = "cic:/matita/cerco/Clight/Csyntax/unary_operation.ind(1,0,0)". |
---|
| 279 | alias id "CMunop" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.ind(1,0,0)". |
---|
| 280 | |
---|
| 281 | (* XXX: For some reason matita refuses to pick the right one unless forced. *) |
---|
[1369] | 282 | alias id "CMnotbool" = "cic:/matita/cerco/common/FrontEndOps/unary_operation.con(0,3,0)". |
---|
[816] | 283 | |
---|
[1871] | 284 | (* Translates a Clight unary operation into a Cminor one, while checking |
---|
| 285 | * that the domain and codomain types are consistent. *) |
---|
[1369] | 286 | definition translate_unop : ∀t,t':typ. CLunop → res (CMunop t t') ≝ |
---|
| 287 | λt,t'.λop:CLunop. |
---|
[816] | 288 | match op with |
---|
[1369] | 289 | [ Onotbool ⇒ |
---|
| 290 | match t return λt. res (CMunop t t') with |
---|
| 291 | [ ASTint sz sg ⇒ |
---|
| 292 | match t' return λt'. res (CMunop ? t') with |
---|
| 293 | [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????) |
---|
| 294 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 295 | ] |
---|
| 296 | | ASTptr r ⇒ |
---|
| 297 | match t' return λt'. res (CMunop ? t') with |
---|
| 298 | [ ASTint sz' sg' ⇒ OK ? (CMnotbool ????) |
---|
| 299 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 300 | ] |
---|
| 301 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 302 | ] |
---|
| 303 | | Onotint ⇒ |
---|
| 304 | match t' return λt'. res (CMunop t t') with |
---|
| 305 | [ ASTint sz sg ⇒ typ_should_eq ?? (λt. CMunop t (ASTint ??)) (Onotint sz sg) |
---|
| 306 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 307 | ] |
---|
[816] | 308 | | Oneg ⇒ |
---|
[1369] | 309 | match t' return λt'. res (CMunop t t') with |
---|
| 310 | [ ASTint sz sg ⇒ typ_should_eq ?? (λt.CMunop t (ASTint ??)) (Onegint sz sg) |
---|
| 311 | | ASTfloat sz ⇒ typ_should_eq ?? (λt.CMunop t (ASTfloat sz)) (Onegf sz) |
---|
[816] | 312 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 313 | ] |
---|
[1369] | 314 | ]. @I qed. |
---|
[816] | 315 | |
---|
[1871] | 316 | (* Translates a Clight addition into a Cminor one. Four cases to consider : |
---|
| 317 | - integer/integer add |
---|
| 318 | - fp/fp add |
---|
| 319 | - pointer/integer |
---|
| 320 | - integer/pointer. |
---|
| 321 | Consistency of the type is enforced by explicit checks. |
---|
| 322 | *) |
---|
[1872] | 323 | |
---|
| 324 | (* First, how to get rid of a abstract-away pointer or array type *) |
---|
| 325 | definition fix_ptr_type : ∀r,ty,n. expr (typ_of_type (ptr_type r ty n)) → expr (ASTptr r) ≝ |
---|
| 326 | λr,ty,n,e. e⌈expr (typ_of_type (ptr_type r ty n)) ↦ expr (ASTptr r)⌉. |
---|
| 327 | cases n // |
---|
| 328 | qed. |
---|
| 329 | |
---|
[816] | 330 | definition translate_add ≝ |
---|
[1872] | 331 | λty1,ty2,ty'. |
---|
[880] | 332 | let ty1' ≝ typ_of_type ty1 in |
---|
| 333 | let ty2' ≝ typ_of_type ty2 in |
---|
[1872] | 334 | match classify_add ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with |
---|
| 335 | [ add_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oadd ??) e1 e2) |
---|
| 336 | | add_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddf sz) e1 e2) |
---|
| 337 | (* XXX we cast up to I16 Signed to prevent overflow, but often we could use I8 *) |
---|
| 338 | | add_case_pi n r ty sz sg ⇒ |
---|
[1878] | 339 | λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty)))))) |
---|
[1872] | 340 | | add_case_ip n sz sg r ty ⇒ |
---|
[1878] | 341 | λe1,e2. typ_should_eq ??? (Op2 ??? (Oaddp I16 r) (fix_ptr_type … e2) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e1) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty)))))) |
---|
[1872] | 342 | | add_default _ _ ⇒ λe1,e2. Error ? (msg TypeMismatch) |
---|
[816] | 343 | ]. |
---|
| 344 | |
---|
[1871] | 345 | |
---|
[816] | 346 | definition translate_sub ≝ |
---|
[1872] | 347 | λty1,ty2,ty'. |
---|
[880] | 348 | let ty1' ≝ typ_of_type ty1 in |
---|
| 349 | let ty2' ≝ typ_of_type ty2 in |
---|
[1872] | 350 | match classify_sub ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with |
---|
| 351 | [ sub_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osub ??) e1 e2) |
---|
| 352 | | sub_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Osubf sz) e1 e2) |
---|
| 353 | (* XXX could optimise cast as above *) |
---|
| 354 | | sub_case_pi n r ty sz sg ⇒ |
---|
[1878] | 355 | λe1,e2. typ_should_eq ??? (Op2 ??? (Osubpi I16 r) (fix_ptr_type … e1) (Op2 ??? (Omul I16 Signed) (Op1 ?? (Ocastint sz sg I16 Signed) e2) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty)))))) |
---|
[1872] | 356 | (* XXX check in detail? *) |
---|
| 357 | | sub_case_pp n1 n2 r1 ty1 r2 ty2 ⇒ |
---|
| 358 | λe1,e2. match ty' return λty'. res (CMexpr (typ_of_type ty')) with |
---|
[1878] | 359 | [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I16 Signed sz sg) (Op2 ??? (Odiv I16) (Op2 ??? (Osubpp I16 r1 r2) (fix_ptr_type … e1) (fix_ptr_type ??? e2)) (Cst ? (Ointconst I16 Signed (repr ? (sizeof ty2)))))) |
---|
[1872] | 360 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
[961] | 361 | ] |
---|
[1872] | 362 | | sub_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) |
---|
[816] | 363 | ]. |
---|
| 364 | |
---|
| 365 | definition translate_mul ≝ |
---|
[1872] | 366 | λty1,ty2,ty'. |
---|
[880] | 367 | let ty1' ≝ typ_of_type ty1 in |
---|
| 368 | let ty2' ≝ typ_of_type ty2 in |
---|
[1872] | 369 | match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with |
---|
| 370 | [ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omul …) e1 e2) |
---|
| 371 | | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omulf …) e1 e2) |
---|
| 372 | | aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) |
---|
[816] | 373 | ]. |
---|
| 374 | |
---|
| 375 | definition translate_div ≝ |
---|
[1872] | 376 | λty1,ty2,ty'. |
---|
[880] | 377 | let ty1' ≝ typ_of_type ty1 in |
---|
| 378 | let ty2' ≝ typ_of_type ty2 in |
---|
[1872] | 379 | match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with |
---|
| 380 | [ aop_case_ii sz sg ⇒ |
---|
| 381 | match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with |
---|
| 382 | [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivu …) e1 e2) |
---|
| 383 | | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odiv …) e1 e2) |
---|
| 384 | ] |
---|
| 385 | | aop_case_ff sz ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Odivf …) e1 e2) |
---|
| 386 | | aop_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) |
---|
[816] | 387 | ]. |
---|
| 388 | |
---|
| 389 | definition translate_mod ≝ |
---|
[1872] | 390 | λty1,ty2,ty'. |
---|
[880] | 391 | let ty1' ≝ typ_of_type ty1 in |
---|
| 392 | let ty2' ≝ typ_of_type ty2 in |
---|
[1872] | 393 | match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with |
---|
| 394 | [ aop_case_ii sz sg ⇒ |
---|
| 395 | match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with |
---|
| 396 | [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2) |
---|
| 397 | | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2) |
---|
| 398 | ] |
---|
| 399 | (* no float case *) |
---|
| 400 | | _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) |
---|
[816] | 401 | ]. |
---|
| 402 | |
---|
| 403 | definition translate_shr ≝ |
---|
[1872] | 404 | λty1,ty2,ty'. |
---|
[880] | 405 | let ty1' ≝ typ_of_type ty1 in |
---|
| 406 | let ty2' ≝ typ_of_type ty2 in |
---|
[1872] | 407 | match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with |
---|
| 408 | [ aop_case_ii sz sg ⇒ |
---|
| 409 | match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with |
---|
| 410 | [ Unsigned ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omodu …) e1 e2) |
---|
| 411 | | Signed ⇒ λe1,e2. typ_should_eq ??? (Op2 ??? (Omod …) e1 e2) |
---|
| 412 | ] |
---|
| 413 | (* no float case *) |
---|
| 414 | | _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) |
---|
[816] | 415 | ]. |
---|
| 416 | |
---|
[1872] | 417 | definition complete_cmp : ∀ty'. CMexpr (ASTint I8 Unsigned) → res (CMexpr (typ_of_type ty')) ≝ |
---|
| 418 | λty',e. |
---|
| 419 | match ty' return λty'. res (CMexpr (typ_of_type ty')) with |
---|
| 420 | [ Tint sz sg ⇒ OK ? (Op1 ?? (Ocastint I8 Unsigned sz sg) e) |
---|
| 421 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 422 | ]. |
---|
| 423 | |
---|
[816] | 424 | definition translate_cmp ≝ |
---|
[1872] | 425 | λc,ty1,ty2,ty'. |
---|
[880] | 426 | let ty1' ≝ typ_of_type ty1 in |
---|
| 427 | let ty2' ≝ typ_of_type ty2 in |
---|
[1872] | 428 | match classify_cmp ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with |
---|
| 429 | [ cmp_case_ii sz sg ⇒ |
---|
| 430 | match sg return λsg. CMexpr (ASTint sz sg) → CMexpr (ASTint sz sg) → res (CMexpr (typ_of_type ty')) with |
---|
| 431 | [ Unsigned ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpu … c) e1 e2) |
---|
| 432 | | Signed ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmp … c) e1 e2) |
---|
| 433 | ] |
---|
| 434 | | cmp_case_pp n r ty ⇒ |
---|
| 435 | λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpp … c) (fix_ptr_type … e1) (fix_ptr_type … e2)) |
---|
| 436 | | cmp_case_ff sz ⇒ λe1,e2. complete_cmp ty' (Op2 ??? (Ocmpf … c) e1 e2) |
---|
| 437 | | cmp_default _ _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) |
---|
[816] | 438 | ]. |
---|
| 439 | |
---|
[1872] | 440 | definition translate_misc_aop ≝ |
---|
| 441 | λty1,ty2,ty',op. |
---|
| 442 | let ty1' ≝ typ_of_type ty1 in |
---|
| 443 | let ty2' ≝ typ_of_type ty2 in |
---|
| 444 | match classify_aop ty1 ty2 return λty1,ty2.λ_. CMexpr (typ_of_type ty1) → CMexpr (typ_of_type ty2) → res (CMexpr (typ_of_type ty')) with |
---|
| 445 | [ aop_case_ii sz sg ⇒ λe1,e2. typ_should_eq ??? (Op2 ?? (ASTint sz sg) (op sz sg) e1 e2) |
---|
| 446 | | _ ⇒ λ_.λ_. Error ? (msg TypeMismatch) |
---|
| 447 | ]. |
---|
| 448 | |
---|
[880] | 449 | definition translate_binop : binary_operation → type → CMexpr ? → type → CMexpr ? → type → res (CMexpr ?) ≝ |
---|
| 450 | λop,ty1,e1,ty2,e2,ty. |
---|
| 451 | let ty' ≝ typ_of_type ty in |
---|
[816] | 452 | match op with |
---|
[1872] | 453 | [ Oadd ⇒ translate_add ty1 ty2 ty e1 e2 |
---|
| 454 | | Osub ⇒ translate_sub ty1 ty2 ty e1 e2 |
---|
| 455 | | Omul ⇒ translate_mul ty1 ty2 ty e1 e2 |
---|
| 456 | | Omod ⇒ translate_mod ty1 ty2 ty e1 e2 |
---|
| 457 | | Odiv ⇒ translate_div ty1 ty2 ty e1 e2 |
---|
| 458 | | Oand ⇒ translate_misc_aop ty1 ty2 ty Oand e1 e2 |
---|
| 459 | | Oor ⇒ translate_misc_aop ty1 ty2 ty Oor e1 e2 |
---|
| 460 | | Oxor ⇒ translate_misc_aop ty1 ty2 ty Oxor e1 e2 |
---|
| 461 | | Oshl ⇒ translate_misc_aop ty1 ty2 ty Oshl e1 e2 |
---|
| 462 | | Oshr ⇒ translate_shr ty1 ty2 ty e1 e2 |
---|
| 463 | | Oeq ⇒ translate_cmp Ceq ty1 ty2 ty e1 e2 |
---|
| 464 | | One ⇒ translate_cmp Cne ty1 ty2 ty e1 e2 |
---|
| 465 | | Olt ⇒ translate_cmp Clt ty1 ty2 ty e1 e2 |
---|
| 466 | | Ogt ⇒ translate_cmp Cgt ty1 ty2 ty e1 e2 |
---|
| 467 | | Ole ⇒ translate_cmp Cle ty1 ty2 ty e1 e2 |
---|
| 468 | | Oge ⇒ translate_cmp Cge ty1 ty2 ty e1 e2 |
---|
[816] | 469 | ]. |
---|
| 470 | |
---|
[1872] | 471 | lemma typ_equals : ∀t1,t2. ∀P:∀t. expr t → Prop. ∀v1,v2. |
---|
| 472 | typ_should_eq t1 t2 expr v1 = OK ? v2 → |
---|
| 473 | P t1 v1 → |
---|
| 474 | P t2 v2. |
---|
| 475 | * [ * * | * | * ] |
---|
| 476 | * try * try * |
---|
| 477 | #P #v1 #v2 #E whd in E:(??%?); destruct |
---|
| 478 | #H @H |
---|
| 479 | qed. |
---|
| 480 | |
---|
| 481 | lemma unfix_ptr_type : ∀r,ty,n,e.∀P:∀t. expr t → Prop. |
---|
| 482 | P (typ_of_type (ptr_type r ty n)) e → |
---|
| 483 | P (ASTptr r) (fix_ptr_type r ty n e). |
---|
| 484 | #r #ty * [ 2: #n ] #e #P #H @H |
---|
| 485 | qed. |
---|
| 486 | |
---|
[1871] | 487 | (* Recall that [expr_vars], defined in Cminor/Syntax.ma, asserts a predicate on |
---|
| 488 | all the variables of a program. [translate_binop_vars], given |
---|
| 489 | a predicate verified for all variables of subexprs e1 and e2, produces |
---|
| 490 | a proof that all variables of [translate_binop op _ e1 _ e2 _] satisfy this |
---|
| 491 | predicate. *) |
---|
[1872] | 492 | |
---|
[1316] | 493 | lemma translate_binop_vars : ∀P,op,ty1,e1,ty2,e2,ty,e. |
---|
| 494 | expr_vars ? e1 P → |
---|
| 495 | expr_vars ? e2 P → |
---|
| 496 | translate_binop op ty1 e1 ty2 e2 ty = OK ? e → |
---|
| 497 | expr_vars ? e P. |
---|
| 498 | #P * #ty1 #e1 #ty2 #e2 #ty #e #H1 #H2 |
---|
[1516] | 499 | whd in ⊢ (??%? → ?); |
---|
[1872] | 500 | [ inversion (classify_add ty1 ty2) in ⊢ ?; |
---|
| 501 | [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 -E3 change with (typ_should_eq ???? = OK ??) in E4; |
---|
| 502 | @(typ_equals … E4) % // |
---|
| 503 | | #sz #E1 #E2 #E3 destruct >E3 #E4 |
---|
| 504 | @(typ_equals … E4) % // |
---|
| 505 | | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4 |
---|
| 506 | @(typ_equals … E4) -E4 -E3 % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ] |
---|
| 507 | | #n #sz #sg #r #ty0 #E1 #E2 #E3 destruct >E3 #E4 |
---|
| 508 | @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2)| % // ] |
---|
| 509 | | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct |
---|
[1316] | 510 | ] |
---|
[1872] | 511 | | inversion (classify_sub ty1 ty2) in ⊢ ?; |
---|
| 512 | [ #sz #sg #E1 #E2 #E3 destruct >E3 #E4 |
---|
| 513 | @(typ_equals … E4) % // |
---|
| 514 | | #sz #E1 #E2 #E3 destruct >E3 #E4 |
---|
| 515 | @(typ_equals … E4) % // |
---|
| 516 | | #n #r #ty0 #sz #sg #E1 #E2 #E3 destruct >E3 #E4 |
---|
| 517 | @(typ_equals … E4) % [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1)| % // ] |
---|
| 518 | | #n1 #n2 #r1 #ty1' #r2 #ty2' #E1 #E2 #E3 destruct >E3 |
---|
| 519 | whd in ⊢ (??%? → ?); cases ty in e ⊢ %; |
---|
| 520 | [ 2: #sz #sg #e #E4 | 4: #r #ty #e #E4 | 5: #r #ty' #n' #e #E4 |
---|
| 521 | | *: normalize #X1 #X2 try #X3 try #X4 destruct |
---|
| 522 | ] whd in E4:(??%?); destruct % // % |
---|
| 523 | [ @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) | @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) ] |
---|
| 524 | | #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct |
---|
[1316] | 525 | ] |
---|
[1872] | 526 | | 3,4,5,6,7,8,9,10: inversion (classify_aop ty1 ty2) in ⊢ ?; |
---|
| 527 | (* Note that some cases require a split on signedness of integer type. *) |
---|
| 528 | [ 1,4,7,10,13,16,19,22: #sz * #E1 #E2 #E3 destruct >E3 #E4 |
---|
| 529 | @(typ_equals … E4) % // |
---|
| 530 | | 2,5: #sz #E1 #E2 #E3 destruct >E3 #E4 |
---|
| 531 | @(typ_equals … E4) % // |
---|
| 532 | | 8,11,14,17,20,23: #sz #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct |
---|
| 533 | | 3,6,9,12,15,18,21,24: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); destruct |
---|
| 534 | ] |
---|
| 535 | | 11,12,13,14,15,16: inversion (classify_cmp ty1 ty2) in ⊢ ?; |
---|
| 536 | [ 1,5,9,13,17,21: #sz * #E1 #E2 #E3 destruct >E3 |
---|
| 537 | | 2,6,10,14,18,22: #n #r #ty' #E1 #E2 #E3 destruct >E3 |
---|
| 538 | | 3,7,11,15,19,23: #sz #E1 #E2 #E3 destruct >E3 |
---|
| 539 | | *: #ty1' #ty2' #E1 #E2 #E3 destruct >E3 #E4 whd in E4:(??%?); @⊥ destruct |
---|
| 540 | ] whd in ⊢ (??%? → ?); cases ty in e ⊢ %; |
---|
| 541 | try (normalize #X1 #X2 try #X3 try #X4 try #X5 destruct #FAIL) |
---|
| 542 | #sz #sg #e #E4 |
---|
| 543 | whd in E4:(??%?); destruct % |
---|
| 544 | [ 25,27,29,31,33,35: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H1) |
---|
| 545 | | 26,28,30,32,34,36: @(unfix_ptr_type ???? (λt,e. expr_vars t e P) H2) |
---|
| 546 | | *: // |
---|
| 547 | ] |
---|
[1316] | 548 | ] qed. |
---|
[880] | 549 | |
---|
[1872] | 550 | |
---|
[880] | 551 | (* We'll need to implement proper translation of pointers if we really do memory |
---|
| 552 | spaces. *) |
---|
[1871] | 553 | (* This function performs leibniz-style subst if r1 = r2, and fails otherwise. *) |
---|
[880] | 554 | definition check_region : ∀r1:region. ∀r2:region. ∀P:region → Type[0]. P r1 → res (P r2) ≝ |
---|
| 555 | λr1,r2,P. |
---|
| 556 | match r1 return λx.P x → res (P r2) with |
---|
| 557 | [ Any ⇒ match r2 return λx.P Any → res (P x) with [ Any ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 558 | | Data ⇒ match r2 return λx.P Data → res (P x) with [ Data ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 559 | | IData ⇒ match r2 return λx.P IData → res (P x) with [ IData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 560 | | PData ⇒ match r2 return λx.P PData → res (P x) with [ PData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 561 | | XData ⇒ match r2 return λx.P XData → res (P x) with [ XData ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 562 | | Code ⇒ match r2 return λx.P Code → res (P x) with [ Code ⇒ OK ? | _ ⇒ λ_.Error ? (msg TypeMismatch) ] |
---|
| 563 | ]. |
---|
| 564 | |
---|
[1871] | 565 | (* Simple application of [check_region] to translate between terms. *) |
---|
[1316] | 566 | definition translate_ptr : ∀P,r1,r2. (Σe:CMexpr (ASTptr r1). expr_vars ? e P) → res (Σe':CMexpr (ASTptr r2).expr_vars ? e' P) ≝ |
---|
| 567 | λP,r1,r2,e. check_region r1 r2 (λr.Σe:CMexpr (ASTptr r).expr_vars ? e P) e. |
---|
[880] | 568 | |
---|
[1369] | 569 | axiom FIXME : String. |
---|
| 570 | |
---|
[1871] | 571 | (* Given a source and target type, translate an expession of type source to type target *) |
---|
| 572 | definition translate_cast : ∀P. ∀ty1:type.∀ty2:type. (Σe:CMexpr (typ_of_type ty1). expr_vars ? e P) → res (Σe':CMexpr (typ_of_type ty2). expr_vars ? e' P) ≝ |
---|
[1316] | 573 | λP,ty1,ty2. |
---|
| 574 | match ty1 return λx.(Σe:CMexpr (typ_of_type x). expr_vars ? e P) → ? with |
---|
[880] | 575 | [ Tint sz1 sg1 ⇒ λe. |
---|
[1316] | 576 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
[1369] | 577 | [ Tint sz2 sg2 ⇒ OK ? (Op1 ?? (Ocastint ? sg1 sz2 ?) e) |
---|
| 578 | | Tfloat sz2 ⇒ OK ? (Op1 ?? (match sg1 with [ Unsigned ⇒ Ofloatofintu ?? | _ ⇒ Ofloatofint ??]) e) |
---|
| 579 | | Tpointer r _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e) |
---|
| 580 | | Tarray r _ _ ⇒ OK ? (Op1 ?? (Optrofint ?? r) e) |
---|
[816] | 581 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 582 | ] |
---|
[880] | 583 | | Tfloat sz1 ⇒ λe. |
---|
[1316] | 584 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
[1369] | 585 | [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (match sg2 with [ Unsigned ⇒ Ointuoffloat ? sz2 | _ ⇒ Ointoffloat ? sz2 ]) e, ?» |
---|
| 586 | | Tfloat sz2 ⇒ Error ? (msg FIXME) (* OK ? «Op1 ?? (Oid ?) e, ?» (* FIXME *) *) |
---|
[816] | 587 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 588 | ] |
---|
[880] | 589 | | Tpointer r1 _ ⇒ λe. (* will need changed for memory regions *) |
---|
[1316] | 590 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x). expr_vars ? e' P) with |
---|
[1369] | 591 | [ Tint sz2 sg2 ⇒ OK ? «Op1 ?? (Ointofptr sz2 ??) e, ?» |
---|
[1316] | 592 | | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e |
---|
| 593 | | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e |
---|
[816] | 594 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 595 | ] |
---|
[880] | 596 | | Tarray r1 _ _ ⇒ λe. (* will need changed for memory regions *) |
---|
[1316] | 597 | match ty2 return λx.res (Σe':CMexpr (typ_of_type x).expr_vars ? e' P) with |
---|
[1369] | 598 | [ Tint sz2 sg2 ⇒ OK ? «Op1 (ASTptr r1) (ASTint sz2 sg2) (Ointofptr sz2 ??) e, ?» |
---|
[1316] | 599 | | Tarray r2 _ _ ⇒ translate_ptr ? r1 r2 e |
---|
| 600 | | Tpointer r2 _ ⇒ translate_ptr ? r1 r2 e |
---|
[816] | 601 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 602 | ] |
---|
[880] | 603 | | _ ⇒ λ_. Error ? (msg TypeMismatch) |
---|
[1605] | 604 | ]. whd normalize nodelta @pi2 |
---|
| 605 | qed. |
---|
[816] | 606 | |
---|
[1871] | 607 | (* Translate Clight exprs into Cminor ones. |
---|
| 608 | Arguments : |
---|
| 609 | - vars:var_types, an environment mapping each variable to a couple (allocation mode, type) |
---|
| 610 | - e:expr, the expression to be converted |
---|
| 611 | Result : res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) |
---|
| 612 | that is, either |
---|
| 613 | . an error |
---|
| 614 | . an expression e', matching the type of e, such that e' respect the property that all variables |
---|
| 615 | in it are not global. In effect, [translate_expr] will replace global variables by constant symbols. |
---|
| 616 | *) |
---|
[1316] | 617 | 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)) ≝ |
---|
| 618 | match e return λe. res (Σe':CMexpr (typ_of_type (typeof e)). expr_vars ? e' (local_id vars)) with |
---|
[816] | 619 | [ Expr ed ty ⇒ |
---|
| 620 | match ed with |
---|
[1878] | 621 | [ Econst_int sz i ⇒ |
---|
| 622 | match ty return λty. res (Σe':CMexpr (typ_of_type ty). expr_vars ? e' (local_id vars)) with |
---|
| 623 | [ Tint sz' sg ⇒ intsize_eq_elim' sz sz' (λsz,sz'. res (Σe':CMexpr (typ_of_type (Tint sz' sg)). expr_vars ? e' (local_id vars))) |
---|
| 624 | (OK ? «Cst ? (Ointconst sz sg i), ?») |
---|
| 625 | (Error ? (msg TypeMismatch)) |
---|
| 626 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 627 | ] |
---|
| 628 | | Econst_float f ⇒ |
---|
| 629 | match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with |
---|
| 630 | [ Tfloat sz ⇒ OK ? «Cst ? (Ofloatconst sz f), ?» |
---|
| 631 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 632 | ] |
---|
[816] | 633 | | Evar id ⇒ |
---|
[1871] | 634 | do 〈c,t〉 as E ← lookup' vars id; (* E is an equality proof of the shape "lookup' vars id = Ok <c,t>" *) |
---|
[1316] | 635 | match c return λx.? = ? → res (Σe':CMexpr ?. ?) with |
---|
[1871] | 636 | [ Global r ⇒ λ_. |
---|
| 637 | (* We are accessing a global variable in an expression. Its Cminor counterpart also depends on |
---|
| 638 | its access mode: |
---|
| 639 | - By_value q, where q is a memory chunk specification (whitch should match the type of the global) |
---|
| 640 | - By_reference, and we only take the adress of the variable |
---|
| 641 | - By_nothing : error |
---|
| 642 | *) |
---|
[1872] | 643 | match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with |
---|
[1878] | 644 | [ By_value t ⇒ OK ? «Mem t r (Cst ? (Oaddrsymbol r id 0)), ?» (* Mem is "load" in compcert *) |
---|
| 645 | | By_reference r ⇒ OK ? «Cst ? (Oaddrsymbol r id 0), ?» |
---|
[1872] | 646 | | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
[816] | 647 | ] |
---|
[1316] | 648 | | Stack n ⇒ λE. |
---|
[1871] | 649 | (* We have decided that the variable should be allocated on the stack, |
---|
| 650 | * because its adress was taken somewhere or becauste it's a structured data. *) |
---|
[1872] | 651 | match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with |
---|
| 652 | [ By_value t ⇒ OK ? «Mem t Any (Cst ? (Oaddrstack n)), ?» |
---|
[1878] | 653 | | By_reference r ⇒ match r return λr. res (Σe':CMexpr (ASTptr r). ?) with |
---|
| 654 | [ Any ⇒ OK ? «Cst ? (Oaddrstack n), ?» |
---|
| 655 | | _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
| 656 | ] |
---|
[1872] | 657 | | By_nothing _ ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] |
---|
[816] | 658 | ] |
---|
[1871] | 659 | (* This is a local variable. Keep it as an identifier in the Cminor code, ensuring that the type of the original expr and of ty match. *) |
---|
[1626] | 660 | | Local ⇒ λE. type_should_eq t ty (λt.Σe':CMexpr (typ_of_type t).expr_vars (typ_of_type t) e' (local_id vars)) («Id (typ_of_type t) id, ?») |
---|
[1316] | 661 | ] E |
---|
[816] | 662 | | Ederef e1 ⇒ |
---|
| 663 | do e1' ← translate_expr vars e1; |
---|
[1871] | 664 | (* According to the way the data pointed to by e1 is accessed, the generated Cminor code will vary. |
---|
| 665 | - if e1 is a kind of int* ptr, then we load ("Mem") the ptr returned by e1 |
---|
| 666 | - if e1 is a struct* or a function ptr, then we acess by reference, in which case we : |
---|
| 667 | 1) check the consistency of the regions in the type of e1 and in the access mode of its type |
---|
| 668 | 2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?) |
---|
| 669 | *) |
---|
[1316] | 670 | match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with |
---|
[881] | 671 | [ ASTptr r ⇒ λe1'. |
---|
[1872] | 672 | match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with |
---|
| 673 | [ By_value t ⇒ OK ? «Mem t ? (pi1 … e1'), ?» |
---|
| 674 | | By_reference r' ⇒ region_should_eq r r' ? e1' |
---|
| 675 | | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 676 | ] |
---|
[881] | 677 | | _ ⇒ λ_. Error ? (msg TypeMismatch) |
---|
| 678 | ] e1' |
---|
[880] | 679 | | Eaddrof e1 ⇒ |
---|
| 680 | do e1' ← translate_addr vars e1; |
---|
[1316] | 681 | match typ_of_type ty return λx.res (Σz:CMexpr x.?) with |
---|
[881] | 682 | [ ASTptr r ⇒ |
---|
| 683 | match e1' with |
---|
[1605] | 684 | [ mk_DPair r1 e1' ⇒ region_should_eq r1 r ? e1' |
---|
[881] | 685 | ] |
---|
[880] | 686 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
[816] | 687 | ] |
---|
| 688 | | Eunop op e1 ⇒ |
---|
[1369] | 689 | do op' ← translate_unop (typ_of_type (typeof e1)) (typ_of_type ty) op; |
---|
[816] | 690 | do e1' ← translate_expr vars e1; |
---|
[1316] | 691 | OK ? «Op1 ?? op' e1', ?» |
---|
[816] | 692 | | Ebinop op e1 e2 ⇒ |
---|
| 693 | do e1' ← translate_expr vars e1; |
---|
| 694 | do e2' ← translate_expr vars e2; |
---|
[1316] | 695 | do e' as E ← translate_binop op (typeof e1) e1' (typeof e2) e2' ty; |
---|
| 696 | OK ? «e', ?» |
---|
[816] | 697 | | Ecast ty1 e1 ⇒ |
---|
| 698 | do e1' ← translate_expr vars e1; |
---|
[1316] | 699 | do e' ← translate_cast ? (typeof e1) ty1 e1'; |
---|
| 700 | do e' ← typ_should_eq (typ_of_type ty1) (typ_of_type ty) ? e'; |
---|
| 701 | OK ? e' |
---|
[816] | 702 | | Econdition e1 e2 e3 ⇒ |
---|
| 703 | do e1' ← translate_expr vars e1; |
---|
| 704 | do e2' ← translate_expr vars e2; |
---|
[1316] | 705 | do e2' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e2'; |
---|
[816] | 706 | do e3' ← translate_expr vars e3; |
---|
[1316] | 707 | do e3' ← type_should_eq ? ty (λx.Σe:CMexpr (typ_of_type x).?) e3'; |
---|
| 708 | match typ_of_type (typeof e1) return λx.(Σe1':CMexpr x. expr_vars ? e1' (local_id vars)) → ? with |
---|
| 709 | [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' e3', ?» |
---|
[880] | 710 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 711 | ] e1' |
---|
[816] | 712 | | Eandbool e1 e2 ⇒ |
---|
| 713 | do e1' ← translate_expr vars e1; |
---|
| 714 | do e2' ← translate_expr vars e2; |
---|
[1878] | 715 | match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with |
---|
| 716 | [ Tint sz sg ⇒ |
---|
| 717 | do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2'; |
---|
[1316] | 718 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → res ? with |
---|
[1878] | 719 | [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' e2' (Cst ? (Ointconst sz sg (zero ?))), ?» |
---|
[961] | 720 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 721 | ] e1' |
---|
| 722 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 723 | ] |
---|
[816] | 724 | | Eorbool e1 e2 ⇒ |
---|
| 725 | do e1' ← translate_expr vars e1; |
---|
| 726 | do e2' ← translate_expr vars e2; |
---|
[1878] | 727 | match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with |
---|
| 728 | [ Tint sz sg ⇒ |
---|
| 729 | do e2' ← type_should_eq ? (Tint sz sg) (λx.Σe:CMexpr (typ_of_type x).?) e2'; |
---|
[1316] | 730 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e (local_id vars)) → ? with |
---|
[1878] | 731 | [ ASTint _ _ ⇒ λe1'. OK ? «Cond ??? e1' (Cst ? (Ointconst sz sg (repr ? 1))) e2', ?» |
---|
[961] | 732 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 733 | ] e1' |
---|
| 734 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 735 | ] |
---|
| 736 | | Esizeof ty1 ⇒ |
---|
[1878] | 737 | match ty return λty. res (Σe':CMexpr (typ_of_type ty). ?) with |
---|
| 738 | [ Tint sz sg ⇒ OK ? «Cst ? (Ointconst sz sg (repr ? (sizeof ty1))), ?» |
---|
[961] | 739 | | _ ⇒ Error ? (msg TypeMismatch) |
---|
| 740 | ] |
---|
[816] | 741 | | Efield e1 id ⇒ |
---|
[1316] | 742 | match typeof e1 with |
---|
[816] | 743 | [ Tstruct _ fl ⇒ |
---|
| 744 | do e1' ← translate_addr vars e1; |
---|
[881] | 745 | match e1' with |
---|
[1605] | 746 | [ mk_DPair r e1' ⇒ |
---|
[881] | 747 | do off ← field_offset id fl; |
---|
[1872] | 748 | match access_mode ty return λt.λ_. res (Σe':CMexpr t. expr_vars ? e' (local_id vars)) with |
---|
| 749 | [ By_value t ⇒ |
---|
| 750 | OK ? «Mem t r (Op2 ? (ASTint I16 Signed (* XXX efficiency? *)) ? |
---|
[1878] | 751 | (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off)))),?» |
---|
[1872] | 752 | | By_reference r' ⇒ |
---|
| 753 | do e1' ← region_should_eq r r' ? e1'; |
---|
| 754 | OK ? «Op2 (ASTptr r') (ASTint I16 Signed (* XXX efficiency? *)) (ASTptr r') |
---|
[1878] | 755 | (Oaddp …) e1' (Cst ? (Ointconst I16 Signed (repr ? off))),?» |
---|
[1872] | 756 | | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
[881] | 757 | ] |
---|
[816] | 758 | ] |
---|
| 759 | | Tunion _ _ ⇒ |
---|
| 760 | do e1' ← translate_addr vars e1; |
---|
[881] | 761 | match e1' with |
---|
[1605] | 762 | [ mk_DPair r e1' ⇒ |
---|
[1872] | 763 | match access_mode ty return λt.λ_. res (Σz:CMexpr t.?) with |
---|
| 764 | [ By_value t ⇒ OK ? «Mem t ? e1', ?» |
---|
| 765 | | By_reference r' ⇒ region_should_eq r r' ? e1' |
---|
| 766 | | By_nothing _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 767 | ] |
---|
[816] | 768 | ] |
---|
| 769 | | _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
[1316] | 770 | ] |
---|
[816] | 771 | | Ecost l e1 ⇒ |
---|
| 772 | do e1' ← translate_expr vars e1; |
---|
[1316] | 773 | do e' ← OK ? «Ecost ? l e1',?»; |
---|
| 774 | typ_should_eq (typ_of_type (typeof e1)) (typ_of_type ty) (λx.Σe:CMexpr x.?) e' |
---|
[816] | 775 | ] |
---|
[1871] | 776 | ] |
---|
| 777 | |
---|
| 778 | (* Translate addr takes an expression e1, and returns a Cminor code computing the address of the result of [e1]. *) |
---|
| 779 | and translate_addr (vars:var_types) (e:expr) on e : res (𝚺r. Σe':CMexpr (ASTptr r). expr_vars ? e' (local_id vars)) ≝ |
---|
[816] | 780 | match e with |
---|
| 781 | [ Expr ed _ ⇒ |
---|
| 782 | match ed with |
---|
| 783 | [ Evar id ⇒ |
---|
[1626] | 784 | do 〈c,t〉 ← lookup' vars id; |
---|
[1608] | 785 | match c return λ_. res (𝚺r.Σz:CMexpr (ASTptr r).?) with |
---|
[1878] | 786 | [ Global r ⇒ OK ? ❬r, «Cst ? (Oaddrsymbol r id 0), ?»❭ |
---|
[1608] | 787 | | Stack n ⇒ OK ? ❬Any, «Cst ? (Oaddrstack n), ?»❭ |
---|
[1078] | 788 | | Local ⇒ Error ? [MSG BadlyTypedAccess; CTX ? id] (* TODO: could rule out? *) |
---|
[816] | 789 | ] |
---|
[880] | 790 | | Ederef e1 ⇒ |
---|
| 791 | do e1' ← translate_expr vars e1; |
---|
[1608] | 792 | match typ_of_type (typeof e1) return λx. (Σz:CMexpr x.expr_vars ? z (local_id vars)) → res (𝚺r. Σz:CMexpr (ASTptr r). ?) with |
---|
| 793 | [ ASTptr r ⇒ λe1'.OK ? ❬r, e1'❭ |
---|
[880] | 794 | | _ ⇒ λ_.Error ? (msg BadlyTypedAccess) |
---|
| 795 | ] e1' |
---|
[816] | 796 | | Efield e1 id ⇒ |
---|
| 797 | match typeof e1 with |
---|
| 798 | [ Tstruct _ fl ⇒ |
---|
| 799 | do e1' ← translate_addr vars e1; |
---|
| 800 | do off ← field_offset id fl; |
---|
[881] | 801 | match e1' with |
---|
[1872] | 802 | [ mk_DPair r e1'' ⇒ OK (𝚺r:region.Σe:CMexpr (ASTptr r).?) |
---|
| 803 | (❬r, «Op2 (ASTptr r) (ASTint I16 Signed (* FIXME inefficient?*)) (ASTptr r) |
---|
[1878] | 804 | (Oaddp I16 r) e1'' (Cst ? (Ointconst I16 Signed (repr ? off))), ?» ❭) |
---|
[881] | 805 | ] |
---|
[816] | 806 | | Tunion _ _ ⇒ translate_addr vars e1 |
---|
| 807 | | _ ⇒ Error ? (msg BadlyTypedAccess) |
---|
| 808 | ] |
---|
| 809 | | _ ⇒ Error ? (msg BadLvalue) |
---|
| 810 | ] |
---|
| 811 | ]. |
---|
[1316] | 812 | whd try @I |
---|
[1626] | 813 | [ >E whd @refl |
---|
[1872] | 814 | | 2,3: @pi2 |
---|
[1608] | 815 | | @(translate_binop_vars … E) @pi2 |
---|
| 816 | | % [ % ] @pi2 |
---|
| 817 | | % [ % @pi2 ] whd @I |
---|
| 818 | | % [ % [ @pi2 | @I ] | @pi2 ] |
---|
| 819 | | % [ @pi2 | @I ] |
---|
| 820 | | % [ @pi2 | @I ] |
---|
| 821 | | @pi2 |
---|
| 822 | | @pi2 |
---|
| 823 | | % [ @pi2 | @I ] |
---|
[1316] | 824 | ] qed. |
---|
[816] | 825 | |
---|
[1872] | 826 | (* We provide a function to work out how to do an assignment to an lvalue |
---|
| 827 | expression. It is used for both Clight assignments and Clight function call |
---|
| 828 | destinations, but doesn't take the value to be assigned so that we can use |
---|
| 829 | it to form a single St_store when possible (and avoid introducing an |
---|
| 830 | unnecessary temporary variable and assignment). |
---|
| 831 | *) |
---|
[1316] | 832 | inductive destination (vars:var_types) : Type[0] ≝ |
---|
[1626] | 833 | | IdDest : ∀id,ty. local_id vars id (typ_of_type ty) → destination vars |
---|
[1872] | 834 | | MemDest : ∀r:region. (Σe:CMexpr (ASTptr r).expr_vars ? e (local_id vars)) → destination vars. |
---|
[816] | 835 | |
---|
[1871] | 836 | (* Let a source Clight expression be assign(e1, e2). First of all, observe that [e1] is a |
---|
| 837 | /Clight/ expression, not converted by translate_expr. We thus have to do part of the work |
---|
| 838 | of [translate_expr] in this function. [translate_dest] will convert e1 |
---|
| 839 | into a proper destination for an assignement operation. We proceed by case analysis on e1. |
---|
| 840 | - if e1 is a variable [id], then we proceed by case analysis on its allocation mode: |
---|
| 841 | - if [id] is allocated locally (in a register), then id becomes directly |
---|
| 842 | the target for the assignement, as (IdDest vars id t H), where t is the type |
---|
| 843 | of id, and H asserts that id is indeed a local variable. |
---|
| 844 | - if [id] is a global variable stored in region [r], then we perform [translate_expr]'s |
---|
| 845 | job and return an adress, given as a constant symbol corresponding to [id], with |
---|
| 846 | region r and memory chunk specified by the access mode of the rhs type ty2 of [e2]. |
---|
| 847 | - same thing for stack-allocated variables, except that we don't specify any region. |
---|
| 848 | - if e1 is not a variable, we use [translate_addr] to generate a Cminor expression computing |
---|
| 849 | the adres of e1 |
---|
| 850 | *) |
---|
[816] | 851 | definition translate_dest ≝ |
---|
[1872] | 852 | λvars,e1. |
---|
| 853 | match e1 with |
---|
| 854 | [ Expr ed1 ty1 ⇒ |
---|
| 855 | match ed1 with |
---|
| 856 | [ Evar id ⇒ |
---|
| 857 | do 〈c,t〉 as E ← lookup' vars id; |
---|
| 858 | match c return λx.? → ? with |
---|
| 859 | [ Local ⇒ λE. OK ? (IdDest vars id t ?) |
---|
[1878] | 860 | | Global r ⇒ λE. OK ? (MemDest ? r (Cst ? (Oaddrsymbol r id 0))) |
---|
[1872] | 861 | | Stack n ⇒ λE. OK ? (MemDest ? Any (Cst ? (Oaddrstack n))) |
---|
| 862 | ] E |
---|
| 863 | | _ ⇒ |
---|
| 864 | do e1' ← translate_addr vars e1; |
---|
| 865 | match e1' with [ mk_DPair r e1' ⇒ OK ? (MemDest ? r e1') ] |
---|
| 866 | ] |
---|
| 867 | ]. |
---|
[1626] | 868 | whd // >E @refl |
---|
[1316] | 869 | qed. |
---|
[1194] | 870 | |
---|
[1871] | 871 | (* [lenv] is the type of maps from Clight labels to Cminor labels. *) |
---|
[1316] | 872 | definition lenv ≝ identifier_map SymbolTag (identifier Label). |
---|
| 873 | |
---|
| 874 | axiom MissingLabel : String. |
---|
| 875 | |
---|
[1871] | 876 | (* Find the Cminor label corresponding to [l] or fail. *) |
---|
[1316] | 877 | definition lookup_label ≝ |
---|
| 878 | λlbls:lenv.λl. opt_to_res … [MSG MissingLabel; CTX ? l] (lookup ?? lbls l). |
---|
| 879 | |
---|
[1871] | 880 | (* True iff the Cminor label [l] is in the codomain of [lbls] *) |
---|
[1316] | 881 | definition lpresent ≝ λlbls:lenv. λl. ∃l'. lookup_label lbls l' = OK ? l. |
---|
| 882 | |
---|
[1871] | 883 | (* True iff The Clight label [l] is in the domain of [lbls] *) |
---|
| 884 | definition label_in_domain ≝ λlbls:lenv. λl. present ?? lbls l. |
---|
| 885 | |
---|
| 886 | let rec fresh_list_for_univ (l:list (identifier Label)) (u:universe Label) ≝ |
---|
| 887 | match l with |
---|
| 888 | [ nil ⇒ True |
---|
| 889 | | cons elt tl ⇒ fresh_for_univ ? elt u ∧ fresh_list_for_univ tl u]. |
---|
| 890 | |
---|
| 891 | record labgen : Type[0] ≝ { |
---|
| 892 | labuniverse : universe Label; |
---|
| 893 | label_genlist : list (identifier Label); |
---|
| 894 | genlist_is_fresh : fresh_list_for_univ label_genlist labuniverse |
---|
| 895 | }. |
---|
| 896 | |
---|
| 897 | lemma fresh_list_stays_fresh : ∀l,tmp,u,u'. fresh_list_for_univ l u → 〈tmp,u'〉=fresh Label u → fresh_list_for_univ l u'. |
---|
| 898 | #l elim l |
---|
| 899 | [ 1: normalize // |
---|
| 900 | | 2: #hd #tl #Hind #tmp #u #u' #HA #HB |
---|
| 901 | whd |
---|
| 902 | @conj |
---|
| 903 | [ 1: whd in HA ⊢ ?; |
---|
| 904 | elim HA #HAleft #HAright |
---|
| 905 | @(fresh_remains_fresh ? hd tmp u u') assumption |
---|
| 906 | | 2: whd in HA ⊢ ?; |
---|
| 907 | elim HA #HAleft #HAright |
---|
| 908 | @Hind // |
---|
| 909 | ] |
---|
| 910 | ] |
---|
| 911 | qed. |
---|
| 912 | |
---|
| 913 | definition In ≝ λelttype.λelt.λl.Exists elttype (λx.x=elt) l. |
---|
| 914 | |
---|
| 915 | definition generate_fresh_label : |
---|
| 916 | ∀ul. Σlul:(identifier Label × labgen). |
---|
| 917 | (And (∀lab. In ? lab (label_genlist ul) → In ? lab (label_genlist (snd … lul))) |
---|
| 918 | (In ? (fst … lul) (label_genlist (snd … lul)))) ≝ |
---|
| 919 | λul. |
---|
| 920 | let 〈tmp,u〉 as E ≝ fresh ? (labuniverse ul) in |
---|
| 921 | «〈tmp, mk_labgen u (tmp::(label_genlist ul)) ?〉, ?». |
---|
| 922 | [ 1: normalize @conj |
---|
| 923 | [ 1: @(fresh_is_fresh ? tmp u (labuniverse ul) ?) assumption |
---|
| 924 | | 2: @fresh_list_stays_fresh // ] |
---|
| 925 | | @conj /2/ |
---|
| 926 | ] |
---|
| 927 | qed. |
---|
| 928 | |
---|
[1316] | 929 | let rec labels_defined (s:statement) : list ident ≝ |
---|
| 930 | match s with |
---|
| 931 | [ Ssequence s1 s2 ⇒ labels_defined s1 @ labels_defined s2 |
---|
| 932 | | Sifthenelse _ s1 s2 ⇒ labels_defined s1 @ labels_defined s2 |
---|
| 933 | | Swhile _ s ⇒ labels_defined s |
---|
| 934 | | Sdowhile _ s ⇒ labels_defined s |
---|
| 935 | | Sfor s1 _ s2 s3 ⇒ labels_defined s1 @ labels_defined s2 @ labels_defined s3 |
---|
| 936 | | Sswitch _ ls ⇒ labels_defined_switch ls |
---|
| 937 | | Slabel l s ⇒ l::(labels_defined s) |
---|
| 938 | | Scost _ s ⇒ labels_defined s |
---|
| 939 | | _ ⇒ [ ] |
---|
| 940 | ] |
---|
| 941 | and labels_defined_switch (ls:labeled_statements) : list ident ≝ |
---|
| 942 | match ls with |
---|
| 943 | [ LSdefault s ⇒ labels_defined s |
---|
| 944 | | LScase _ _ s ls ⇒ labels_defined s @ labels_defined_switch ls |
---|
| 945 | ]. |
---|
| 946 | |
---|
| 947 | definition ldefined ≝ λs.λl.Exists ? (λl'.l' = l) (labels_of s). |
---|
| 948 | |
---|
[1871] | 949 | (* For each label l in s, there exists a matching label l' = lenv(l) defined in s' *) |
---|
[1316] | 950 | definition labels_translated : lenv → statement → stmt → Prop ≝ |
---|
| 951 | λlbls,s,s'. ∀l. |
---|
| 952 | (Exists ? (λl'.l' = l) (labels_defined s)) → |
---|
[1871] | 953 | ∃l'. lookup_label lbls l = (OK ? l') ∧ ldefined s' l'. |
---|
[1316] | 954 | |
---|
| 955 | |
---|
[1871] | 956 | (* Invariant on statements, holds during conversion to Cminor *) |
---|
| 957 | definition stmt_inv ≝ λvars. stmt_P (stmt_vars (local_id vars)). |
---|
| 958 | |
---|
| 959 | (* I (Ilias) decided to inline the following definition, to make explicit the data constructed. |
---|
| 960 | * This was needed to prove some stuff in translate_statement at some point, but it might be |
---|
| 961 | * useless now. If needed, I can revert this change. *) |
---|
| 962 | definition translate_assign : ∀vars:var_types. expr → expr → res (Σs:stmt. stmt_inv vars s) ≝ |
---|
[816] | 963 | λvars,e1,e2. |
---|
[1872] | 964 | do e2' ← translate_expr vars e2; |
---|
| 965 | do dest ← translate_dest vars e1; |
---|
[816] | 966 | match dest with |
---|
[1626] | 967 | [ IdDest id ty p ⇒ |
---|
| 968 | do e2' ← type_should_eq (typeof e2) ty ? e2'; |
---|
| 969 | OK ? «St_assign ? id e2', ?» |
---|
[1872] | 970 | | MemDest r e1' ⇒ OK ? «St_store ? r e1' e2', ?» |
---|
[816] | 971 | ]. |
---|
[1871] | 972 | % try (//) try (elim e2' //) elim e1' // |
---|
| 973 | qed. |
---|
[816] | 974 | |
---|
| 975 | definition m_option_map : ∀A,B:Type[0]. (A → res B) → option A → res (option B) ≝ |
---|
| 976 | λA,B,f,oa. |
---|
| 977 | match oa with |
---|
| 978 | [ None ⇒ OK ? (None ?) |
---|
| 979 | | Some a ⇒ do b ← f a; OK ? (Some ? b) |
---|
| 980 | ]. |
---|
| 981 | |
---|
[1608] | 982 | definition translate_expr_sigma : ∀vars:var_types. expr → res (Σe:(𝚺t:typ.CMexpr t). match e with [ mk_DPair t e ⇒ expr_vars t e (local_id vars) ]) ≝ |
---|
[880] | 983 | λv,e. |
---|
| 984 | do e' ← translate_expr v e; |
---|
[1608] | 985 | OK (Σe:(𝚺t:typ.CMexpr t).?) «❬?, e'❭, ?». |
---|
| 986 | whd @pi2 |
---|
[1316] | 987 | qed. |
---|
[880] | 988 | |
---|
[1871] | 989 | (* Add the list of typed variables tmpenv to the environment [var_types] with |
---|
| 990 | the allocation mode Local. *) |
---|
[1627] | 991 | definition add_tmps : var_types → list (ident × type) → var_types ≝ |
---|
| 992 | λvs,tmpenv. |
---|
| 993 | foldr ?? (λidty,vs. add ?? vs (\fst idty) 〈Local, \snd idty〉) vs tmpenv. |
---|
| 994 | |
---|
| 995 | record tmpgen (vars:var_types) : Type[0] ≝ { |
---|
[1206] | 996 | tmp_universe : universe SymbolTag; |
---|
[1627] | 997 | tmp_env : list (ident × type); |
---|
| 998 | tmp_ok : fresh_map_for_univ … (add_tmps vars tmp_env) tmp_universe; |
---|
[1871] | 999 | tmp_preserved : |
---|
[1627] | 1000 | ∀id,ty. local_id vars id ty → local_id (add_tmps vars tmp_env) id ty |
---|
[1206] | 1001 | }. |
---|
| 1002 | |
---|
[1627] | 1003 | definition alloc_tmp : ∀vars. type → tmpgen vars → ident × (tmpgen vars) ≝ |
---|
| 1004 | λvars,ty,g. |
---|
| 1005 | let 〈tmp,u〉 as E ≝ fresh ? (tmp_universe ? g) in |
---|
| 1006 | 〈tmp, mk_tmpgen ? u (〈tmp, ty〉::(tmp_env ? g)) ??〉. |
---|
| 1007 | [ #id #ty' |
---|
| 1008 | whd in ⊢ (? → ?%??); |
---|
| 1009 | whd in ⊢ (% → %); |
---|
| 1010 | whd in ⊢ (? → match % with [_ ⇒ ? | _ ⇒ ?]); #H |
---|
| 1011 | >lookup_add_miss |
---|
| 1012 | [ @(tmp_preserved … g) @H |
---|
| 1013 | | @(fresh_distinct … E) @(tmp_ok … g) |
---|
| 1014 | lapply (tmp_preserved … g id ty' H) |
---|
| 1015 | whd in ⊢ (% → %); |
---|
| 1016 | whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ?] → ?); |
---|
| 1017 | cases (lookup ??? id) |
---|
| 1018 | [ * | #x #_ % #E destruct ] |
---|
| 1019 | ] |
---|
| 1020 | | @fresh_map_add |
---|
| 1021 | [ @(fresh_map_preserved … E) @(tmp_ok … g) |
---|
| 1022 | | @(fresh_is_fresh … E) |
---|
| 1023 | ] |
---|
| 1024 | ] qed. |
---|
[1206] | 1025 | |
---|
[1871] | 1026 | |
---|
[1316] | 1027 | lemma lookup_label_hit : ∀lbls,l,l'. |
---|
| 1028 | lookup_label lbls l = OK ? l' → |
---|
| 1029 | lpresent lbls l'. |
---|
| 1030 | #lbls #l #l' #E whd %{l} @E |
---|
| 1031 | qed. |
---|
| 1032 | |
---|
[1627] | 1033 | (* TODO: is this really needed now? *) |
---|
[1871] | 1034 | |
---|
[1627] | 1035 | definition tmps_preserved : ∀vars:var_types. tmpgen vars → tmpgen vars → Prop ≝ |
---|
[1316] | 1036 | λvars,u1,u2. |
---|
[1627] | 1037 | ∀id,ty. local_id (add_tmps vars (tmp_env … u1)) id ty → local_id (add_tmps vars (tmp_env … u2)) id ty. |
---|
[1316] | 1038 | |
---|
[1627] | 1039 | lemma alloc_tmp_preserves : ∀vars,tmp,u,u',q. |
---|
| 1040 | 〈tmp,u'〉 = alloc_tmp ? q u → tmps_preserved vars u u'. |
---|
| 1041 | #vars #tmp * #u1 #e1 #F1 #P1 * #u2 #e2 #F2 #P2 #q |
---|
| 1042 | whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?); |
---|
| 1043 | cases (fresh SymbolTag u1) in ⊢ (??%? → ???(match % with [ _ ⇒ ? ]?) → ?); |
---|
| 1044 | #tmp' #u' #E1 #E2 whd in E2:(???%); destruct |
---|
| 1045 | #id #ty #H whd in ⊢ (?%??); whd in H ⊢ %; |
---|
| 1046 | whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; |
---|
| 1047 | >lookup_add_miss // @(fresh_distinct … E1) @F1 |
---|
| 1048 | whd in H:(match % with [_ ⇒ ?|_ ⇒ ?]) ⊢ %; |
---|
| 1049 | cases (lookup ??? id) in H ⊢ %; |
---|
| 1050 | [ * | #x #_ % #E destruct ] |
---|
| 1051 | qed. |
---|
[1316] | 1052 | |
---|
[1871] | 1053 | lemma add_tmps_oblivious : ∀vars,s,u. |
---|
| 1054 | stmt_inv vars s → stmt_inv (add_tmps vars (tmp_env vars u)) s. |
---|
| 1055 | #vars #s #u #H |
---|
| 1056 | @(stmt_P_mp … H) |
---|
| 1057 | #s' #H1 @(stmt_vars_mp … H1) #id #t #H @(tmp_preserved ? u ?? H) |
---|
[1316] | 1058 | qed. |
---|
| 1059 | |
---|
[1627] | 1060 | lemma local_id_fresh_tmp : ∀vars,tmp,u,ty,u0. |
---|
| 1061 | 〈tmp,u〉 = alloc_tmp vars ty u0 → local_id (add_tmps vars (tmp_env … u)) tmp (typ_of_type ty). |
---|
| 1062 | #vars #tmp #u #ty #u0 |
---|
| 1063 | whd in ⊢ (???% → ?); generalize in ⊢ (???(?%) → ?); |
---|
| 1064 | cases (fresh SymbolTag (tmp_universe vars u0)) in ⊢ (??%? → ???(match % with [_⇒?]?) → ?); |
---|
| 1065 | * #tmp' #u' #e #E whd in E:(???%); |
---|
[1351] | 1066 | destruct |
---|
[1626] | 1067 | whd in ⊢ (?%??); whd whd in ⊢ match % with [ _ ⇒ ? | _ ⇒ ? ]; >lookup_add_hit |
---|
| 1068 | @refl |
---|
[1316] | 1069 | qed. |
---|
| 1070 | |
---|
[1871] | 1071 | |
---|
| 1072 | let rec mklabels (ul:labgen) : (identifier Label) × (identifier Label) × labgen ≝ |
---|
| 1073 | match generate_fresh_label ul with |
---|
| 1074 | [ mk_Sig res1 H1 ⇒ |
---|
| 1075 | let 〈entry_label, ul1〉 as E1 ≝ res1 in |
---|
| 1076 | match generate_fresh_label ul1 with |
---|
| 1077 | [ mk_Sig res2 H2 ⇒ |
---|
| 1078 | let 〈exit_label, ul2〉 as E2 ≝ res2 in |
---|
| 1079 | 〈entry_label, exit_label, ul2〉 |
---|
| 1080 | ] |
---|
| 1081 | ]. |
---|
| 1082 | |
---|
| 1083 | (* When converting loops into gotos, and in order to eliminate blocks, we have |
---|
| 1084 | * to convert continues and breaks into goto's, too. We add some "flags" in |
---|
| 1085 | * in argument to [translate_statement], meaning that the next encountered break |
---|
| 1086 | * or continue has to be converted into a goto to some contained label. |
---|
| 1087 | * ConvertTo l1 l2 means "convert continue to goto l1 and convert break to goto l2". |
---|
| 1088 | *) |
---|
| 1089 | inductive convert_flag : Type[0] ≝ |
---|
| 1090 | | DoNotConvert : convert_flag |
---|
| 1091 | | ConvertTo : identifier Label → identifier Label → convert_flag. (* continue, break *) |
---|
| 1092 | |
---|
| 1093 | let rec labels_of_flag (flag : convert_flag) : list (identifier Label) ≝ |
---|
| 1094 | match flag with |
---|
| 1095 | [ DoNotConvert ⇒ [ ] |
---|
| 1096 | | ConvertTo continue break ⇒ continue :: break :: [ ] |
---|
| 1097 | ]. |
---|
| 1098 | |
---|
| 1099 | (* For a top-level expression, [label-wf] collapses to "all labels are properly declared" *) |
---|
| 1100 | definition label_wf ≝ |
---|
| 1101 | λ (s : statement) .λ (s' : stmt) .λ (lbls : lenv). λ (flag : convert_flag). |
---|
| 1102 | stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'. |
---|
| 1103 | |
---|
| 1104 | (* trans_inv is the invariant which is enforced during the translation from Clight to Cminor. |
---|
| 1105 | The involved arguments are the following: |
---|
| 1106 | . vars:var_types, an environment mapping variables to their types and allocation modes |
---|
| 1107 | . lbls:lenv, a mapping from old (Clight) to fresh and new (Cminor) labels, |
---|
| 1108 | . s:statement, a Clight statement, |
---|
| 1109 | . uv, a fresh variable generator (containing itself some invariants) |
---|
| 1110 | . flag, wich maps "break" and "continue" to "gotos" |
---|
| 1111 | . su', a couple of a Cminor statement and fresh variable generator. |
---|
| 1112 | *) |
---|
| 1113 | definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → ((tmpgen vars) × labgen × stmt) → Prop ≝ |
---|
| 1114 | λvars,lbls,s,uv,flag,su'. |
---|
| 1115 | let 〈uv', ul', s'〉 ≝ su' in |
---|
| 1116 | stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧ (* remaining variables in s' are local*) |
---|
| 1117 | labels_translated lbls s s' ∧ (* all the labels in s are transformed in label of s' using [lbls] as a map *) |
---|
| 1118 | tmps_preserved vars uv uv' ∧ (* the variables generated are local and grows in a monotonic fashion *) |
---|
| 1119 | label_wf s s' lbls flag. (* labels are "properly" declared, as defined in [ŀabel_wf].*) |
---|
| 1120 | |
---|
| 1121 | let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (s:statement) on s |
---|
| 1122 | : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) ≝ |
---|
| 1123 | match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) with |
---|
| 1124 | [ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?» |
---|
[1316] | 1125 | | Sassign e1 e2 ⇒ |
---|
[1872] | 1126 | do e2' ← translate_expr vars e2; (* rhs *) |
---|
| 1127 | do dest ← translate_dest vars e1; (* e1 *) |
---|
[1871] | 1128 | match dest with |
---|
| 1129 | [ IdDest id ty p ⇒ |
---|
| 1130 | do e2' ← type_should_eq (typeof e2) ty ? e2'; |
---|
| 1131 | OK ? «〈uv, ul, St_assign ? id e2'〉, ?» |
---|
[1872] | 1132 | | MemDest r e1' ⇒ |
---|
| 1133 | OK ? «〈uv, ul, St_store ? r e1' e2'〉, ?» |
---|
[1871] | 1134 | ] |
---|
[816] | 1135 | | Scall ret ef args ⇒ |
---|
| 1136 | do ef' ← translate_expr vars ef; |
---|
[1316] | 1137 | do ef' ← typ_should_eq (typ_of_type (typeof ef)) (ASTptr Code) ? ef'; |
---|
[1608] | 1138 | do args' ← mmap_sigma ??? (translate_expr_sigma vars) args; |
---|
[816] | 1139 | match ret with |
---|
[1871] | 1140 | [ None ⇒ OK ? «〈uv, ul, St_call (None ?) ef' args'〉, ?» |
---|
[816] | 1141 | | Some e1 ⇒ |
---|
[1872] | 1142 | do dest ← translate_dest vars e1; |
---|
[816] | 1143 | match dest with |
---|
[1871] | 1144 | [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?» |
---|
[1872] | 1145 | | MemDest r e1' ⇒ |
---|
[1871] | 1146 | let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in |
---|
[1872] | 1147 | OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) r e1' (Id ? tmp))〉, ?» |
---|
[816] | 1148 | ] |
---|
| 1149 | ] |
---|
| 1150 | | Ssequence s1 s2 ⇒ |
---|
[1871] | 1151 | do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1; |
---|
| 1152 | do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2; |
---|
| 1153 | OK ? «〈fgens2, St_seq s1' s2'〉, ?» |
---|
[816] | 1154 | | Sifthenelse e1 s1 s2 ⇒ |
---|
| 1155 | do e1' ← translate_expr vars e1; |
---|
[1316] | 1156 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with |
---|
[880] | 1157 | [ ASTint _ _ ⇒ λe1'. |
---|
[1871] | 1158 | do «fgens1, s1', H1» ← translate_statement vars uv ul «lbls,?» flag s1; |
---|
| 1159 | do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) «lbls,?» flag s2; |
---|
| 1160 | OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?» |
---|
[880] | 1161 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 1162 | ] e1' |
---|
[816] | 1163 | | Swhile e1 s1 ⇒ |
---|
| 1164 | do e1' ← translate_expr vars e1; |
---|
[1316] | 1165 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with |
---|
[1871] | 1166 | [ ASTint _ _ ⇒ λe1'. |
---|
| 1167 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
| 1168 | match mklabels ul with |
---|
| 1169 | [ mk_Sig result Hmklabels => |
---|
| 1170 | let 〈labels, ul1〉 as E1 ≝ result in |
---|
| 1171 | let 〈entry, exit〉 as E2 ≝ labels in |
---|
| 1172 | do «fgens2, s1',H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1; |
---|
| 1173 | let converted_loop ≝ |
---|
| 1174 | St_label entry |
---|
| 1175 | (St_seq |
---|
| 1176 | (St_ifthenelse ?? e1' (St_seq s1' (St_goto entry)) St_skip) |
---|
| 1177 | (St_label exit St_skip)) |
---|
| 1178 | in |
---|
| 1179 | OK ? «〈fgens2, converted_loop〉, ?» |
---|
| 1180 | ] |
---|
[880] | 1181 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 1182 | ] e1' |
---|
[816] | 1183 | | Sdowhile e1 s1 ⇒ |
---|
| 1184 | do e1' ← translate_expr vars e1; |
---|
[1316] | 1185 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with |
---|
[880] | 1186 | [ ASTint _ _ ⇒ λe1'. |
---|
[1871] | 1187 | match mklabels ul with |
---|
| 1188 | [ mk_Sig result Hmklabels ⇒ |
---|
| 1189 | let 〈labels, ul1〉 as E1 ≝ result in |
---|
| 1190 | let 〈entry, exit〉 as E2 ≝ labels in |
---|
| 1191 | do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» (ConvertTo entry exit) s1; |
---|
| 1192 | let converted_loop ≝ |
---|
| 1193 | St_label entry |
---|
| 1194 | (St_seq |
---|
| 1195 | (St_seq |
---|
| 1196 | s1' |
---|
| 1197 | (St_ifthenelse ?? e1' (St_goto entry) St_skip) |
---|
| 1198 | ) |
---|
| 1199 | (St_label exit St_skip)) |
---|
| 1200 | in |
---|
| 1201 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
| 1202 | OK ? «〈fgens2, converted_loop〉, ?» |
---|
| 1203 | ] |
---|
[880] | 1204 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 1205 | ] e1' |
---|
[816] | 1206 | | Sfor s1 e1 s2 s3 ⇒ |
---|
| 1207 | do e1' ← translate_expr vars e1; |
---|
[1316] | 1208 | match typ_of_type (typeof e1) return λx.(Σe:CMexpr x. expr_vars ? e ?) → ? with |
---|
[880] | 1209 | [ ASTint _ _ ⇒ λe1'. |
---|
[1871] | 1210 | match mklabels ul with |
---|
| 1211 | [ mk_Sig result Hmklabels ⇒ |
---|
| 1212 | let 〈labels, ul1〉 as E ≝ result in |
---|
| 1213 | let 〈entry, exit〉 as E2 ≝ labels in |
---|
| 1214 | do «fgens2, s1', H1» ← translate_statement vars uv ul1 «lbls,?» flag s1; |
---|
| 1215 | do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) «lbls, ?» (ConvertTo entry exit) s2; |
---|
| 1216 | do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) «lbls, ?» (ConvertTo entry exit) s3; |
---|
| 1217 | (* TODO: this is a little different from the prototype and CompCert, is it OK? *) |
---|
| 1218 | let converted_loop ≝ |
---|
| 1219 | St_seq |
---|
| 1220 | s1' |
---|
| 1221 | (St_label entry |
---|
| 1222 | (St_seq |
---|
| 1223 | (St_ifthenelse ?? e1' (St_seq s3' (St_seq s2' (St_goto entry))) St_skip) |
---|
| 1224 | (St_label exit St_skip) |
---|
| 1225 | )) |
---|
| 1226 | in |
---|
| 1227 | OK ? «〈fgens4, converted_loop〉, ?» |
---|
| 1228 | ] |
---|
[880] | 1229 | | _ ⇒ λ_.Error ? (msg TypeMismatch) |
---|
| 1230 | ] e1' |
---|
[1871] | 1231 | | Sbreak ⇒ |
---|
| 1232 | match flag return λf.flag = f → ? with |
---|
| 1233 | [ DoNotConvert ⇒ λEflag. |
---|
| 1234 | Error ? (msg FIXME) |
---|
| 1235 | | ConvertTo continue_label break_label ⇒ λEflag. |
---|
| 1236 | OK ? «〈uv, ul, St_goto break_label〉, ?» |
---|
| 1237 | ] (refl ? flag) |
---|
| 1238 | | Scontinue ⇒ |
---|
| 1239 | match flag return λf.flag = f → ? with |
---|
| 1240 | [ DoNotConvert ⇒ λEflag. |
---|
| 1241 | Error ? (msg FIXME) |
---|
| 1242 | | ConvertTo continue_label break_label ⇒ λEflag. |
---|
| 1243 | OK ? «〈uv, ul, St_goto continue_label〉, ?» |
---|
| 1244 | ] (refl ? flag) |
---|
[816] | 1245 | | Sreturn ret ⇒ |
---|
[880] | 1246 | match ret with |
---|
[1871] | 1247 | [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?» |
---|
[880] | 1248 | | Some e1 ⇒ |
---|
| 1249 | do e1' ← translate_expr vars e1; |
---|
[1871] | 1250 | OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?» |
---|
[880] | 1251 | ] |
---|
[816] | 1252 | | Sswitch e1 ls ⇒ Error ? (msg FIXME) |
---|
| 1253 | | Slabel l s1 ⇒ |
---|
[1316] | 1254 | do l' as E ← lookup_label lbls l; |
---|
[1871] | 1255 | do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1; |
---|
| 1256 | OK ? «〈fgens1, St_label l' s1'〉, ?» |
---|
[1316] | 1257 | | Sgoto l ⇒ |
---|
| 1258 | do l' as E ← lookup_label lbls l; |
---|
[1871] | 1259 | OK ? «〈uv, ul, St_goto l'〉, ?» |
---|
[816] | 1260 | | Scost l s1 ⇒ |
---|
[1871] | 1261 | do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1; |
---|
| 1262 | OK ? «〈fgens1, St_cost l s1'〉, ?» |
---|
[816] | 1263 | ]. |
---|
[1871] | 1264 | try @conj try @conj try @conj try @conj try @conj try @conj try @conj |
---|
| 1265 | try (@I) |
---|
| 1266 | try (#l #H elim H) |
---|
| 1267 | try (#size #sign #H assumption) |
---|
| 1268 | try (#region #H assumption) |
---|
| 1269 | [ 1,5: @(tmp_preserved … p) ] |
---|
| 1270 | [ 1,3: elim e2' | 2,9: elim e1' | 4,7,14: elim ef' ] |
---|
| 1271 | [ 1,2,3,4,5,6,7 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] |
---|
| 1272 | [ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) |
---|
| 1273 | | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp) |
---|
| 1274 | | 3: elim args' // ] |
---|
| 1275 | | 8: (* we should be able to merge this case with the previous ... *) |
---|
| 1276 | @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) |
---|
| 1277 | | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp) |
---|
| 1278 | | 3: elim args' // ] |
---|
| 1279 | | 2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) |
---|
| 1280 | | 3: @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)])) |
---|
| 1281 | [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars)) |
---|
| 1282 | [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0) |
---|
| 1283 | | 2: assumption ] |
---|
| 1284 | | 2: elim args' // ] |
---|
| 1285 | | 4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ] |
---|
| 1286 | [ 1: #size #sign | 2: #reg | 3: #fsize ] |
---|
| 1287 | [ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ] |
---|
| 1288 | try @(match fgens1 return λx.x=fgens1 → ? with |
---|
| 1289 | [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1)) |
---|
| 1290 | try @(match fgens2 return λx.x=fgens2 → ? with |
---|
| 1291 | [ mk_Prod uv2 ul2 ⇒ λHfgens2.? ] (refl ? fgens2)) |
---|
| 1292 | try @(match fgens3 return λx.x=fgens3 → ? with |
---|
| 1293 | [ mk_Prod uv3 ul3 ⇒ λHfgens3.? ] (refl ? fgens3)) |
---|
| 1294 | try @(match fgens4 return λx.x=fgens4 → ? with |
---|
| 1295 | [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4)) |
---|
| 1296 | whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3; |
---|
| 1297 | try (elim H1 -H1 * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1) |
---|
| 1298 | try (elim H2 -H2 * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2) |
---|
| 1299 | try (elim H3 -H3 * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3) |
---|
| 1300 | [ 1,2: #Hind1 #Hind2 | 3,4,9,11: #Hind | 5: #Hind1 #Hind2 #Hind3 ] |
---|
| 1301 | try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption |
---|
| 1302 | [ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal) |
---|
| 1303 | | 2: #l #H cases (Exists_append ???? H) #Hcase |
---|
| 1304 | [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj |
---|
| 1305 | [ 1: @(proj1 ?? Hlabel) |
---|
| 1306 | | 2: normalize @Exists_append_l @(proj2 … Hlabel) ] |
---|
| 1307 | | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj |
---|
| 1308 | [ 1: @(proj1 ?? Hlabel) |
---|
| 1309 | | 2: normalize @Exists_append_r @(proj2 … Hlabel) ] |
---|
| 1310 | ] |
---|
| 1311 | | 3,9: #id #ty #H @(Htmps_pres2 … (Htmps_pres1 id ty H)) ] |
---|
| 1312 | [ 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ] |
---|
| 1313 | [ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) |
---|
| 1314 | #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H) |
---|
| 1315 | | 2,5: #H %1 %2 assumption |
---|
| 1316 | | 3,6: #H %2 assumption ] |
---|
| 1317 | (* if/then/else *) |
---|
| 1318 | | 3: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) |
---|
| 1319 | | 4: whd #l #H |
---|
| 1320 | cases (Exists_append ???? H) #Hcase |
---|
| 1321 | [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj |
---|
| 1322 | [ 1: @(proj1 ?? Hlabel) |
---|
| 1323 | | 2: normalize @Exists_append_l @(proj2 … Hlabel) ] |
---|
| 1324 | | 2: elim (Hlabels_tr2 l Hcase) #label #Hlabel @(ex_intro … label) @conj |
---|
| 1325 | [ 1: @(proj1 ?? Hlabel) |
---|
| 1326 | | 2: normalize @Exists_append_r @(proj2 … Hlabel) ] |
---|
| 1327 | ] |
---|
| 1328 | ] |
---|
| 1329 | [ 1: 1: @(stmt_P_mp … Hind2) | 2: @(stmt_P_mp … Hind1) ] |
---|
| 1330 | [ 1,2: #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) |
---|
| 1331 | #l * try * [ 1,4: #H %1 %1 normalize in H ⊢ %; try (@Exists_append_l @H); try (@Exists_append_r @H) |
---|
| 1332 | | 2,5: #H %1 %2 assumption |
---|
| 1333 | | 3,6: #H %2 assumption ] ] |
---|
| 1334 | try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I |
---|
| 1335 | [ 1,9,19,32: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) |
---|
| 1336 | | 2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) // |
---|
| 1337 | | 3,10: whd #l #H normalize in H; |
---|
| 1338 | elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label) |
---|
| 1339 | @conj |
---|
| 1340 | [ 1,3: @(proj1 … Hlabel) |
---|
| 1341 | | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l |
---|
| 1342 | @(proj2 … Hlabel) ] |
---|
| 1343 | | 30: whd %2 %2 whd /2/ |
---|
| 1344 | | 31: whd %2 whd /2/ |
---|
| 1345 | | 4,16: whd %1 %1 normalize /2/ |
---|
| 1346 | | 5,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) |
---|
| 1347 | #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H |
---|
| 1348 | | 2,6: #H %1 %2 assumption |
---|
| 1349 | | 3,7: #H <H %1 %1 normalize /2/ |
---|
| 1350 | | 4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2 |
---|
| 1351 | @Exists_append_r normalize /2/ |
---|
| 1352 | | 2,4: * ] |
---|
| 1353 | ] |
---|
| 1354 | | 6: normalize %1 %1 %1 // |
---|
| 1355 | | 7,14: normalize %1 %1 %2 @Exists_append_r normalize /2/ |
---|
| 1356 | | 11,13: whd %1 %1 normalize /2/ |
---|
| 1357 | | 15: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ] |
---|
| 1358 | | 2: #H elim (Hlabels_tr1 label H) |
---|
| 1359 | #lab * #Hlookup #Hdef @(ex_intro … lab) @conj |
---|
| 1360 | [ 1: // | 2: whd %2 assumption ] |
---|
| 1361 | ] |
---|
| 1362 | | 17: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) |
---|
| 1363 | #l * try * [ 1: #H %1 %1 normalize %2 @H |
---|
| 1364 | | 2: #H %1 %2 assumption |
---|
| 1365 | | 3: #H %2 assumption ] |
---|
| 1366 | | 18: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t |
---|
| 1367 | #H @(Htmps_pres3 … (Htmps_pres2 … H)) |
---|
| 1368 | | 20: @(stmt_P_mp … Hstmt_inv3) // |
---|
| 1369 | | 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t |
---|
| 1370 | #H @(Htmps_pres3 … H) |
---|
| 1371 | | 22: whd #l #H normalize in H; |
---|
| 1372 | cases (Exists_append … H) #Hcase |
---|
| 1373 | [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj |
---|
| 1374 | [ 1: @(proj1 … Hlabel) |
---|
| 1375 | | 2: normalize @Exists_append_l @(proj2 … Hlabel) |
---|
| 1376 | ] |
---|
| 1377 | | 2: cases (Exists_append … Hcase) #Hcase2 |
---|
| 1378 | [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj |
---|
| 1379 | [ 1: @(proj1 … Hlabel) |
---|
| 1380 | | 2: normalize >append_nil >append_nil >append_cons |
---|
| 1381 | @Exists_append_r @Exists_append_l @Exists_append_r |
---|
| 1382 | @(proj2 … Hlabel) |
---|
| 1383 | ] |
---|
| 1384 | | 2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj |
---|
| 1385 | [ 1: @(proj1 … Hlabel) |
---|
| 1386 | | 2: normalize >append_nil >append_nil >append_cons |
---|
| 1387 | @Exists_append_r @Exists_append_l @Exists_append_l |
---|
| 1388 | @(proj2 … Hlabel) |
---|
| 1389 | ] |
---|
| 1390 | ] |
---|
| 1391 | ] |
---|
| 1392 | | 23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H))) |
---|
| 1393 | | 24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) |
---|
| 1394 | #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H |
---|
| 1395 | | 2: #H %1 %2 assumption |
---|
| 1396 | | 3: #H %2 assumption ] |
---|
| 1397 | | 25: whd %1 %1 normalize /2/ |
---|
| 1398 | | 26: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) |
---|
| 1399 | #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) |
---|
| 1400 | @Exists_append_r @Exists_append_l @Exists_append_l |
---|
| 1401 | @Exists_append_l assumption |
---|
| 1402 | | 2: #H %1 %2 assumption |
---|
| 1403 | | 3: #H <H %1 %1 normalize |
---|
| 1404 | @Exists_append_r whd %1 // |
---|
| 1405 | | 4: * [ 1: #H <H %1 %1 normalize |
---|
| 1406 | @Exists_append_r @(Exists_add ?? (nil ?)) |
---|
| 1407 | @Exists_append_r @Exists_append_r |
---|
| 1408 | whd %1 // |
---|
| 1409 | | 2: * ] |
---|
| 1410 | ] |
---|
| 1411 | | 27: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) |
---|
| 1412 | #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) |
---|
| 1413 | @Exists_append_r @Exists_append_l @Exists_append_l |
---|
| 1414 | @Exists_append_r @Exists_append_l assumption |
---|
| 1415 | | 2: #H %1 %2 assumption |
---|
| 1416 | | 3: #H <H %1 %1 normalize |
---|
| 1417 | @Exists_append_r whd %1 // |
---|
| 1418 | | 4: * [ 1: #Eq <Eq %1 %1 whd normalize |
---|
| 1419 | @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r |
---|
| 1420 | @Exists_append_r whd %1 // |
---|
| 1421 | | 2: * ] |
---|
| 1422 | ] |
---|
| 1423 | | 28: whd %1 %1 normalize /2/ |
---|
| 1424 | | 29: whd %1 %1 normalize |
---|
| 1425 | @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r |
---|
| 1426 | whd %1 // |
---|
| 1427 | | 33: whd %1 %2 whd @(ex_intro … l) @E |
---|
[1316] | 1428 | ] qed. |
---|
[816] | 1429 | |
---|
[1078] | 1430 | axiom ParamGlobalMixup : String. |
---|
[816] | 1431 | |
---|
[1871] | 1432 | (* params and statement aren't real parameters, they're just there for giving the invariant. *) |
---|
| 1433 | definition alloc_params : |
---|
| 1434 | ∀vars:var_types.∀lbls,statement,uv,flag. list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flag su) |
---|
| 1435 | → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag su) ≝ |
---|
| 1436 | λvars,lbls,statement,uv,ul,params,s. foldl ?? (λsu,it. |
---|
[1078] | 1437 | let 〈id,ty〉 ≝ it in |
---|
[1871] | 1438 | do «result,Is» ← su; |
---|
| 1439 | let 〈fgens1, s〉 as Eresult ≝ result in |
---|
[1626] | 1440 | do 〈t,ty'〉 as E ← lookup' vars id; |
---|
[1871] | 1441 | match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul su) with |
---|
| 1442 | [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is» |
---|
[1316] | 1443 | | Stack n ⇒ λE. |
---|
[1872] | 1444 | OK ? «〈fgens1, St_seq (St_store ? Any (Cst ? (Oaddrstack n)) (Id (typ_of_type ty') id)) s〉, ?» |
---|
[1316] | 1445 | | Global _ ⇒ λE. Error ? [MSG ParamGlobalMixup; CTX ? id] |
---|
| 1446 | ] E) (OK ? s) params. |
---|
[1871] | 1447 | whd |
---|
| 1448 | @(match fgens1 return λx.x=fgens1 → ? with |
---|
| 1449 | [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1)) |
---|
| 1450 | whd in Is ⊢ %; destruct whd in Is; |
---|
| 1451 | try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I |
---|
| 1452 | elim Is * * #Hincl #Hstmt_inv #Hlab_tr #Htmp_pr try assumption |
---|
| 1453 | @(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl |
---|
| 1454 | qed. |
---|
[1078] | 1455 | |
---|
[1316] | 1456 | axiom DuplicateLabel : String. |
---|
| 1457 | |
---|
| 1458 | definition lenv_list_inv : lenv → lenv → list ident → Prop ≝ |
---|
| 1459 | λlbls0,lbls,ls. |
---|
| 1460 | ∀l,l'. lookup_label lbls l = OK ? l' → |
---|
| 1461 | Exists ? (λl'. l' = l) ls ∨ lookup_label lbls0 l = OK ? l'. |
---|
| 1462 | |
---|
| 1463 | lemma lookup_label_add : ∀lbls,l,l'. |
---|
| 1464 | lookup_label (add … lbls l l') l = OK ? l'. |
---|
[1516] | 1465 | #lbls #l #l' whd in ⊢ (??%?); >lookup_add_hit @refl |
---|
[1316] | 1466 | qed. |
---|
| 1467 | |
---|
| 1468 | lemma lookup_label_miss : ∀lbls,l,l',l0. |
---|
| 1469 | l0 ≠ l → |
---|
| 1470 | lookup_label (add … lbls l l') l0 = lookup_label lbls l0. |
---|
[1515] | 1471 | #lbls #l #l' #l0 #NE |
---|
[1516] | 1472 | whd in ⊢ (??%%); |
---|
[1316] | 1473 | >lookup_add_miss |
---|
[1515] | 1474 | [ @refl | @NE ] |
---|
[1871] | 1475 | qed. |
---|
[1316] | 1476 | |
---|
[1871] | 1477 | let rec populate_lenv (ls:list ident) (ul:labgen) (lbls:lenv): res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) ≝ |
---|
| 1478 | match ls return λls.res ((Σlbls':lenv. lenv_list_inv lbls lbls' ls) × labgen) with |
---|
| 1479 | [ nil ⇒ OK ? 〈«lbls, ?», ul〉 |
---|
[1316] | 1480 | | cons l t ⇒ |
---|
[1871] | 1481 | match lookup_label lbls l return λlook. lookup_label lbls l = look → ? with |
---|
| 1482 | [ OK _ ⇒ λ_.Error ? (msg DuplicateLabel) |
---|
| 1483 | | Error _ ⇒ λLOOK. |
---|
| 1484 | match generate_fresh_label … ul with |
---|
| 1485 | [ mk_Sig ret H ⇒ |
---|
| 1486 | do 〈packed_lbls, ul1〉 ← populate_lenv t (snd ?? ret) (add … lbls l (fst ?? ret)); |
---|
| 1487 | match packed_lbls with |
---|
| 1488 | [ mk_Sig lbls' Hinv ⇒ OK ? 〈«lbls', ?», ul1〉 ] |
---|
| 1489 | ] |
---|
| 1490 | ] (refl ? (lookup_label lbls l)) |
---|
[1316] | 1491 | ]. |
---|
[1871] | 1492 | [ 1: whd #l #l' #Hlookup %2 assumption |
---|
| 1493 | | 2: whd in Hinv; whd #cl_lab #cm_lab #Hlookup |
---|
| 1494 | @(eq_identifier_elim … l cl_lab) |
---|
| 1495 | [ 1: #Heq %1 >Heq whd %1 // |
---|
| 1496 | | 2: #Hneq cases (Hinv cl_lab cm_lab Hlookup) |
---|
| 1497 | [ 1: #H %1 %2 @H |
---|
| 1498 | | 2: #LOOK' %2 >lookup_label_miss in LOOK'; /2/ #H @H ] |
---|
| 1499 | ] |
---|
| 1500 | ] |
---|
| 1501 | qed. |
---|
[1316] | 1502 | |
---|
[1871] | 1503 | definition build_label_env : |
---|
| 1504 | ∀body:statement. res ((Σlbls:lenv. ∀l,l'.lookup_label lbls l = OK ? l' → Exists ? (λl'.l' = l) (labels_defined body)) × labgen) ≝ |
---|
[1316] | 1505 | λbody. |
---|
[1871] | 1506 | let initial_labgen ≝ mk_labgen (new_universe ?) (nil ?) ? in |
---|
| 1507 | do 〈label_map, u〉 ← populate_lenv (labels_defined body) initial_labgen (empty_map ??); |
---|
| 1508 | let lbls ≝ pi1 ?? label_map in |
---|
| 1509 | let H ≝ pi2 ?? label_map in |
---|
| 1510 | OK ? 〈«lbls, ?», u〉. |
---|
| 1511 | [ 1: #l #l' #E cases (H l l' E) // |
---|
| 1512 | whd in ⊢ (??%? → ?); #H destruct |
---|
| 1513 | | 2: whd @I ] |
---|
[1316] | 1514 | qed. |
---|
| 1515 | |
---|
[1626] | 1516 | lemma local_id_split : ∀vars,tmpgen,i,t. |
---|
[1627] | 1517 | local_id (add_tmps vars (tmp_env vars tmpgen)) i t → |
---|
| 1518 | local_id vars i t ∨ Exists ? (λx. \fst x = i ∧ typ_of_type (\snd x) = t) (tmp_env … tmpgen). |
---|
[1626] | 1519 | #vars #tmpgen #i #t |
---|
| 1520 | whd in ⊢ (?%?? → ?); |
---|
[1627] | 1521 | elim (tmp_env vars tmpgen) |
---|
[1316] | 1522 | [ #H %1 @H |
---|
| 1523 | | * #id #ty #tl #IH |
---|
| 1524 | cases (identifier_eq ? i id) |
---|
[1626] | 1525 | [ #E >E #H %2 whd %1 % [ @refl | whd in H; whd in H:(match % with [_⇒?|_⇒?]); >lookup_add_hit in H; #E1 >E1 @refl ] |
---|
[1515] | 1526 | | #NE #H cases (IH ?) |
---|
[1316] | 1527 | [ #H' %1 @H' |
---|
| 1528 | | #H' %2 %2 @H' |
---|
| 1529 | | whd in H; whd in H:(match % with [ _ ⇒ ? | _ ⇒ ? ]); |
---|
[1515] | 1530 | >lookup_add_miss in H; [ #H @H | @NE ] |
---|
[1316] | 1531 | ] |
---|
| 1532 | ] |
---|
| 1533 | ] qed. |
---|
| 1534 | |
---|
| 1535 | lemma Exists_squeeze : ∀A,P,l1,l2,l3. |
---|
| 1536 | Exists A P (l1@l3) → Exists A P (l1@l2@l3). |
---|
| 1537 | #A #P #l1 #l2 #l3 #EX |
---|
| 1538 | cases (Exists_append … EX) |
---|
| 1539 | [ #EX1 @Exists_append_l @EX1 |
---|
| 1540 | | #EX3 @Exists_append_r @Exists_append_r @EX3 |
---|
| 1541 | ] qed. |
---|
| 1542 | |
---|
[1871] | 1543 | (* This lemma allows to merge two stmt_P in one. Used in the following parts to merge an invariant on variables |
---|
| 1544 | and an invariant on labels. *) |
---|
| 1545 | lemma stmt_P_conj : ∀ (P1:stmt → Prop). ∀ (P2:stmt → Prop). ∀ s. stmt_P P1 s → stmt_P P2 s → stmt_P (λs.P1 s ∧ P2 s) s. |
---|
| 1546 | #P1 #P2 #s elim s |
---|
| 1547 | normalize try @conj try @conj try /3/ |
---|
| 1548 | [ #z0 #s #Hind1 #Hind2 * * #HA #HB #HC * * #HD #HE #HF try @conj try @conj try @conj try /2/ |
---|
| 1549 | | #H5 #H6 #H7 #H8 #H9 #H10 #H11 * * #H15 #H16 #H17 * * #H20 #H21 #H22 |
---|
| 1550 | try @conj try @conj try @conj try /2/ |
---|
| 1551 | | 3,4: #H24 #H25 * #H29 #H30 * #H33 #H34 try @conj try @conj try @conj try /2/ |
---|
| 1552 | | 5,6: #H36 #H37 #H38 * #H42 #H43 * #H46 #H47 try @conj try @conj try @conj try /2/ ] |
---|
| 1553 | qed. |
---|
| 1554 | |
---|
[1629] | 1555 | definition translate_function : |
---|
| 1556 | ∀tmpuniverse:universe SymbolTag. |
---|
| 1557 | ∀globals:list (ident×region×type). |
---|
| 1558 | ∀f:function. |
---|
| 1559 | globals_fresh_for_univ ? globals tmpuniverse → |
---|
| 1560 | fn_fresh_for_univ f tmpuniverse → |
---|
| 1561 | res internal_function ≝ |
---|
| 1562 | λtmpuniverse, globals, f, Fglobals, Ffn. |
---|
[1871] | 1563 | do 〈env_pack, ul〉 ← build_label_env (fn_body f); |
---|
| 1564 | match env_pack with |
---|
| 1565 | [ mk_Sig lbls Ilbls ⇒ |
---|
| 1566 | let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in |
---|
| 1567 | let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in |
---|
| 1568 | do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (fn_body f); |
---|
| 1569 | do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (fn_params f) s0; |
---|
| 1570 | let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in |
---|
| 1571 | let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in |
---|
| 1572 | do D ← check_distinct_env ?? (params @ vars); |
---|
| 1573 | OK ? (mk_internal_function |
---|
| 1574 | (opttyp_of_type (fn_return f)) |
---|
| 1575 | params |
---|
| 1576 | vars |
---|
| 1577 | D |
---|
| 1578 | stacksize |
---|
| 1579 | s1 ?) |
---|
| 1580 | ]. |
---|
| 1581 | [ 1: #i #t #Hloc whd @Hloc |
---|
| 1582 | | 2: whd #id #Hpresent normalize in Hpresent:(???%?); whd in Hpresent; |
---|
| 1583 | @(characterise_vars_fresh … (sym_eq … E)) // |
---|
| 1584 | | 3: @(match fgens return λx.x=fgens → ? with |
---|
| 1585 | [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens)) |
---|
| 1586 | whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %; |
---|
| 1587 | elim Is * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hlabel_wf |
---|
| 1588 | (* merge Hlabel_wf with Hstmt_inv and eliminate right away *) |
---|
| 1589 | @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf)) |
---|
| 1590 | #s * #Hstmt_vars #Hstmt_labels @conj |
---|
| 1591 | [ 1: (* prove that variables are either parameters or locals *) |
---|
| 1592 | @(stmt_vars_mp … Hstmt_vars) #i #t #H |
---|
| 1593 | (* Case analysis: (i, t) is either in vartypes, or in (tmp_env vartypes uv) *) |
---|
| 1594 | cases (local_id_split … H) |
---|
| 1595 | [ 1: #H' >map_append |
---|
| 1596 | @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t)) (* * #id #ty @(〈id, typ_of_type ty〉=〈i, t〉)*) |
---|
| 1597 | | 2: whd @Exists_squeeze @(characterise_vars_all globals f ?? (sym_eq ??? E) i t H') |
---|
| 1598 | | 3: * #id #ty * #E1 #E2 <E1 <E2 @refl |
---|
| 1599 | ] |
---|
| 1600 | | 2: #EX @Exists_append_r whd in ⊢ (???%); <map_append @Exists_append_l |
---|
| 1601 | @Exists_map [ 1: #x @(And (\fst x = i) (typ_of_type (\snd x) = t)) |
---|
| 1602 | | 2: <Hfgens @EX |
---|
| 1603 | | 3: * #id #ty * #E1 #E2 <E1 <E2 % @refl |
---|
| 1604 | ] |
---|
| 1605 | ] |
---|
| 1606 | | 2: (* prove that labels are properly declared. *) |
---|
| 1607 | @(stmt_labels_mp … Hstmt_labels) #l * * |
---|
| 1608 | [ 1: #H assumption |
---|
| 1609 | | 2: * #cl_label #Hlookup lapply (Ilbls cl_label l Hlookup) #Hdefined |
---|
| 1610 | cases (Hlab_trans … Hdefined) #lx * #LOOKUPx >LOOKUPx in Hlookup; #Ex destruct (Ex) |
---|
| 1611 | #H @H |
---|
| 1612 | ] |
---|
[1627] | 1613 | ] |
---|
[1871] | 1614 | ] qed. |
---|
[816] | 1615 | |
---|
[1629] | 1616 | definition translate_fundef : |
---|
| 1617 | ∀tmpuniverse:universe SymbolTag. |
---|
| 1618 | ∀globals:list (ident×region×type). |
---|
[1630] | 1619 | globals_fresh_for_univ ? globals tmpuniverse → |
---|
[1629] | 1620 | ∀f:clight_fundef. |
---|
| 1621 | fd_fresh_for_univ f tmpuniverse → |
---|
| 1622 | res (fundef internal_function) ≝ |
---|
[1630] | 1623 | λtmpuniverse,globals,Fglobals,f. |
---|
[1629] | 1624 | match f return λf. fd_fresh_for_univ f ? → ? with |
---|
| 1625 | [ CL_Internal fn ⇒ λFf. do fn' ← translate_function tmpuniverse globals fn Fglobals Ff; OK ? (Internal ? fn') |
---|
| 1626 | | CL_External fn argtys retty ⇒ λ_. OK ? (External ? (mk_external_function fn (signature_of_type argtys retty))) |
---|
[816] | 1627 | ]. |
---|
| 1628 | |
---|
[1207] | 1629 | (* TODO: move universe generation to higher level once we do runtime function |
---|
| 1630 | generation. Cheating a bit - we only need the new identifiers to be fresh |
---|
| 1631 | for individual functions. *) |
---|
| 1632 | |
---|
[1630] | 1633 | let rec map_partial_All (A,B:Type[0]) (P:A → Prop) (f:∀a:A. P a → res B) |
---|
| 1634 | (l:list A) (H:All A P l) on l : res (list B) ≝ |
---|
| 1635 | match l return λl. All A P l → ? with |
---|
| 1636 | [ nil ⇒ λ_. OK (list B) (nil B) |
---|
| 1637 | | cons hd tl ⇒ λH. |
---|
| 1638 | do b_hd ← f hd (proj1 … H); |
---|
| 1639 | do b_tl ← map_partial_All A B P f tl (proj2 … H); |
---|
| 1640 | OK (list B) (cons B b_hd b_tl) |
---|
| 1641 | ] H. |
---|
| 1642 | |
---|
[816] | 1643 | definition clight_to_cminor : clight_program → res Cminor_program ≝ |
---|
| 1644 | λp. |
---|
[1207] | 1645 | let tmpuniverse ≝ universe_for_program p in |
---|
[1626] | 1646 | let fun_globals ≝ map ?? (λidf. 〈\fst idf,Code,type_of_fundef (\snd idf)〉) (prog_funct ?? p) in |
---|
| 1647 | let var_globals ≝ map ?? (λv. 〈\fst (\fst v), \snd (\fst v), \snd (\snd v)〉) (prog_vars ?? p) in |
---|
[881] | 1648 | let globals ≝ fun_globals @ var_globals in |
---|
[1630] | 1649 | do fns ← map_partial_All ??? (λx,H. do f ← translate_fundef tmpuniverse globals ? (\snd x) H; OK ? 〈\fst x, f〉) (prog_funct ?? p) ?; |
---|
| 1650 | OK ? (mk_program ?? |
---|
| 1651 | (map ?? (λv. 〈\fst v, \fst (\snd v)〉) (prog_vars ?? p)) |
---|
| 1652 | fns |
---|
| 1653 | (prog_main ?? p)). |
---|
| 1654 | cases (prog_fresh p) * #H1 #H2 #H3 |
---|
| 1655 | [ @(All_mp … H1) #x * // |
---|
| 1656 | | @All_append |
---|
| 1657 | [ elim (prog_funct ?? p) in H1 ⊢ %; // * #id #fd #tl #IH * * #Hhd1 #Hhd2 #Htl % // @IH @Htl |
---|
| 1658 | | whd in H3; elim (prog_vars ?? p) in H3 ⊢ %; // #hd #tl #IH * #Hhd #Htl % /2/ |
---|
| 1659 | ] |
---|
| 1660 | ] qed. |
---|
| 1661 | |
---|
| 1662 | (* It'd be nice to go back to some generic thing like |
---|
| 1663 | |
---|
| 1664 | transform_partial_program2 … p (translate_fundef tmpuniverse globals) (λi. OK ? (\fst i)). |
---|
| 1665 | |
---|
| 1666 | rather than the messier definition above. |
---|
[1872] | 1667 | *) |
---|