Changeset 2822 for src/Clight/toCminor.ma
 Timestamp:
 Mar 8, 2013, 12:48:20 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r2686 r2822 701 701  if e1 is a struct* or a function ptr, then we acess by reference, in which case we : 702 702 1) check the consistency of the regions in the type of e1 and in the access mode of its type 703 2) return directly the converted CMinor expression "as is" (TODO : what is the strange notation with the ceil function and the mapsto ?)703 2) return directly the converted CMinor expression "as is" 704 704 *) 705 705 match typ_of_type (typeof e1) return λx.(Σz:CMexpr x.expr_vars ? z (local_id vars)) → ? with … … 1184 1184 do e2' ← typ_should_eq (typ_of_type (typeof e2)) (typ_of_type ty) ? e2'; 1185 1185 OK ? «〈uv, ul, St_assign ? id e2'〉, ?» 1186  MemDest e1' ⇒ 1187 OK ? «〈uv, ul, St_store ? e1' e2'〉, ?» 1186  MemDest e1' ⇒ 1187 match type_eq_dec (typeof e1) (typeof e2) with 1188 [ inl Hcl_typ_eq ⇒ 1189 OK ? «〈uv, ul, St_store ? e1' e2'〉, ?» 1190  inr Hcl_typ_neq ⇒ 1191 Error ? (msg TypeMismatch) 1192 ] 1188 1193 ] 1189 1194  Scall ret ef args ⇒ … … 1196 1201 do dest ← translate_dest vars e1; 1197 1202 match dest with 1198 [ IdDest id ty p ⇒ OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?» 1203 [ IdDest id ty p ⇒ 1204 (* No trace generated here, by inversion on translate_dest _ _ = IdDest _ _ _ *) 1205 OK ? «〈uv, ul, St_call (Some ? 〈id,typ_of_type ty〉) ef' args'〉, ?» 1199 1206  MemDest e1' ⇒ 1200 1207 let 〈tmp, uv1〉 as Etmp ≝ alloc_tmp ? (typeof e1) uv in 1201 OK ? «〈uv1, ul, St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))〉, ?» 1208 (* alloc a new variable to serve as a placeholder for the evaluation of e1', 1209 * which /must/ happen before the call. Otherwise, the cost labels are not 1210 * emitted as in Clight. *) 1211 let 〈tmp2, uv2〉 as Etmp' ≝ alloc_tmp ? (Tpointer (typeof e1)) uv1 in 1212 OK ? «〈uv2, ul, 1213 (St_seq (St_store ? (Id ? tmp2) e1') 1214 (St_seq (St_call (Some ? 〈tmp,typ_of_type (typeof e1)〉) ef' args') 1215 (St_store (typ_of_type (typeof e1)) e1' (Id ? tmp))))〉, ?» 1202 1216 ] 1203 1217 ] … … 1336 1350 try (#H1 try #H2 assumption) 1337 1351 [ 1,5: @(tmp_preserved … p) ] 1338 [ 1,3: elim e2'  2,9,23: elim e1'  4,7,13: elim ef' ] 1339 [ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] 1340 [ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) 1352 [ 6: @(local_id_fresh_tmp vars tmp2 uv2 (Tpointer (typeof e1)) uv1 Etmp') 1353  7: cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1354  8: @conj try @conj normalize nodelta 1355 [ 1: cases e1' #e #Hvars lapply (local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) 1356 @(alloc_tmp_preserves … Etmp') 1357  3: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) 1358  2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp) 1359  3: elim args' // ] 1360  2: cases ef' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] ] 1361 [ 5: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) 1341 1362  2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp) 1342  3: elim args' // ] 1343  7: (* we should be able to merge this case with the previous ... *) 1344 @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) 1363  3: elim args' // ] ] 1364 [ 5: whd @conj 1365 [ 1: cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1366  2: @(alloc_tmp_preserves … Etmp') @(local_id_fresh_tmp … Etmp) ] ] 1367 [ 1,3: elim e2' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1368  2: elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1369  4,7: elim ef' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] 1370 [ 3: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) 1345 1371  2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp) 1346 1372  3: elim args' // ] 1347  2: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) 1348  3: @(All_mp (𝚺 t:typ.expr t) (λe. match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars)])) 1349 [ 1: #a #Ha elim a in Ha ⊢ ?; #ta #a #Ha whd @(expr_vars_mp ?? (local_id vars)) 1350 [ 1: #i0 #t0 #H0 @(tmp_preserved vars uv1 i0 t0 H0) 1351  2: assumption ] 1352  2: elim args' // ] 1353  4: @(local_id_fresh_tmp vars tmp uv1 (typeof e1) uv Etmp) ] 1354 [ 1: #size #sign  2: ] 1355 [ 1,2: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ] 1373  2: #H @(alloc_tmp_preserves … Etmp' l ASTptr) @(alloc_tmp_preserves … Etmp l ASTptr) @H 1374  1: #sz #sg #H @(alloc_tmp_preserves … Etmp' l) @(alloc_tmp_preserves … Etmp l) @H ] 1356 1375 try @refl (* Does (at least) the return_ok cases *) 1357 1376 try @(match fgens1 return λx.x=fgens1 → ? with … … 1367 1386 try (elim H2 H2 * * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2 #Hret2) 1368 1387 try (elim H3 H3 * * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3 #Hret3) 1388 [ 8: whd cases e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] 1369 1389 [ 1,2: #Hind1 #Hind2  3,4,8,10: #Hind  5: #Hind1 #Hind2 #Hind3 ] 1370 1390 try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption
Note: See TracChangeset
for help on using the changeset viewer.