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