 Timestamp:
 Oct 5, 2012, 12:57:19 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminor.ma
r2353 r2389 1169 1169  _ ⇒ λ_.Error ? (msg TypeMismatch) 1170 1170 ] e1' 1171 (* Performing loop conversions while keeping good cost labelling properties is 1172 a little tricky. In principle we should have a cost label in each branch, 1173 but the behaviour of the next stage means that we can put in Cminor skips and 1174 goto labels before the cost label. *) 1171 1175  Swhile e1 s1 cl ⇒ 1172 1176 do e1' ← translate_expr vars e1; … … 1189 1193 [ ASTint _ _ ⇒ λe1'. 1190 1194 let 〈labels, ul1〉 as E1 ≝ mklabels ul in 1191 let 〈entry, exit〉 as E2 ≝ labels in 1192 do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1; 1195 let 〈condexpr, exit〉 as E2 ≝ labels in 1196 let 〈body, ul2〉 ≝ generate_fresh_label … ul1 in 1197 do «fgens2, s1', H1» ← translate_statement vars uv ul2 lbls (ConvertTo condexpr exit) rettyp s1; 1198 (* This is particularly carefully implemented, we need to reach the 1199 cost label in s1' or the cost label after the loop (if they are 1200 present) after the ifthenelse, and we're only allowed skips and 1201 goto labels in between. So we structure it like a while with a goto 1202 into the middle (the CFG will be essentially the same, anyway.) *) 1193 1203 let converted_loop ≝ 1194 St_label entry 1195 (St_seq 1196 (St_seq 1197 s1' 1198 (St_ifthenelse ?? e1' (St_goto entry) St_skip) 1199 ) 1200 (St_label exit St_skip)) 1204 St_seq 1205 (St_seq 1206 (St_goto body) 1207 (St_label condexpr 1208 (St_ifthenelse ?? e1' 1209 (St_label body 1210 (St_seq 1211 s1' 1212 (St_goto condexpr))) 1213 St_skip))) 1214 (St_label exit St_skip) 1201 1215 in 1202 1216 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) … … 1340 1354  3,6: #H %2 assumption ] ] 1341 1355 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption 1342 [ 1,10,2 0: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)1356 [ 1,10,22: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1343 1357  cases cl normalize /3/ 1344 1358  (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) // … … 1347 1361 @conj 1348 1362 [ 1,3: @(proj1 … Hlabel) 1349  2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l 1350 @(proj2 … Hlabel) ] 1351  30: whd %2 %2 whd /2/ 1352  31: whd %2 whd /2/ 1363  2,4: whd @or_intror normalize in ⊢ (???%); 1364 [ @Exists_append_l @Exists_append_l  %2 @Exists_append_l @Exists_append_l @Exists_append_l ] 1365 @(proj2 … Hlabel) ] 1353 1366  cases cl normalize /3/ 1354  5,1 7: whd %1 %1 normalize /2/1355  6,1 3: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1356 #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H1367  5,13,16: whd %1 %1 normalize /2/ 1368  6,15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1369 #l * try * [ 1,5: #H %1 %1 normalize %2 [ 2: %2 ] @Exists_append_l @Exists_append_l try @Exists_append_l @H 1357 1370  2,6: #H %1 %2 assumption 1358 1371  3,7: #H <H %1 %1 normalize /2/ 1359  4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2 1372  4,8: #H normalize in H; elim H [ 1,3: #E <E %1 %1 normalize %2 [2: %2] 1360 1373 @Exists_append_r normalize /2/ 1361 1374  2,4: * ] 1362 1375 ] 1363 1376  7: normalize %1 %1 %1 // 1364  8,1 5: normalize %1 %1 %2 @Exists_append_r normalize /2/1377  8,14: normalize %1 %1 %2 [ @Exists_append_r normalize /2/  %1 % ] 1365 1378  cases cl normalize /3/ 1366  12,14: whd %1 %1 normalize /2/ 1367  16: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct //  whd /2/ ] 1368  2: #H elim (Hlabels_tr1 label H) 1369 #lab * #Hlookup #Hdef @(ex_intro … lab) @conj 1370 [ 1: //  2: whd %2 assumption ] 1371 ] 1372  18: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1373 #l * try * [ 1: #H %1 %1 normalize %2 @H 1374  2: #H %1 %2 assumption 1375  3: #H %2 assumption ] 1376  19: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1377 #H @(Htmps_pres3 … (Htmps_pres2 … H)) 1378  21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1379 #H @(Htmps_pres3 … H) 1380  22: whd #l #H normalize in H; 1381 cases (Exists_append … H) #Hcase 1382 [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj 1383 [ 1: @(proj1 … Hlabel) 1384  2: normalize @Exists_append_l @(proj2 … Hlabel) 1385 ] 1386  2: cases (Exists_append … Hcase) #Hcase2 1387 [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj 1388 [ 1: @(proj1 … Hlabel) 1389  2: normalize >append_nil >append_nil >append_cons 1390 @Exists_append_r @Exists_append_l @Exists_append_r 1391 @(proj2 … Hlabel) 1392 ] 1393  2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj 1394 [ 1: @(proj1 … Hlabel) 1395  2: normalize >append_nil >append_nil >append_cons 1396 @Exists_append_r @Exists_append_l @Exists_append_l 1397 @(proj2 … Hlabel) 1398 ] 1399 ] 1379  whd %1 %1 normalize %2 %1 % 1380  normalize %1 %1 %2 %2 /2/ 1381  whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct //  whd /2/ ] 1382  2: #H elim (Hlabels_tr1 label H) 1383 #lab * #Hlookup #Hdef @(ex_intro … lab) @conj 1384 [ 1: //  2: whd %2 assumption ] 1385 ] 1386  normalize %1 %1 %1 % 1387  @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1388 #l * try * [ 1: #H %1 %1 normalize %2 @H 1389  2: #H %1 %2 assumption 1390  3: #H %2 assumption ] 1391  @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1392 #H @(Htmps_pres3 … (Htmps_pres2 … H)) 1393  @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1394 #H @(Htmps_pres3 … H) 1395  whd #l #H normalize in H; 1396 cases (Exists_append … H) #Hcase 1397 [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj 1398 [ 1: @(proj1 … Hlabel) 1399  2: normalize @Exists_append_l @(proj2 … Hlabel) 1400 ] 1401  2: cases (Exists_append … Hcase) #Hcase2 1402 [ 1: elim (Hlabels_tr2 l Hcase2) #label #Hlabel @(ex_intro … label) @conj 1403 [ 1: @(proj1 … Hlabel) 1404  2: normalize >append_nil >append_nil >append_cons 1405 @Exists_append_r @Exists_append_l @Exists_append_r 1406 @(proj2 … Hlabel) 1400 1407 ] 1401  23: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H))) 1402  24: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1408  2: elim (Hlabels_tr3 l Hcase2) #label #Hlabel @(ex_intro … label) @conj 1409 [ 1: @(proj1 … Hlabel) 1410  2: normalize >append_nil >append_nil >append_cons 1411 @Exists_append_r @Exists_append_l @Exists_append_l 1412 @(proj2 … Hlabel) 1413 ] 1414 ] 1415 ] 1416  #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H))) 1417  @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1403 1418 #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H 1404 1419  2: #H %1 %2 assumption 1405 1420  3: #H %2 assumption ] 1406  25:whd %1 %1 normalize /2/1407  26:@(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1421  whd %1 %1 normalize /2/ 1422  @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1408 1423 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1409 1424 @Exists_append_r @Exists_append_l @Exists_append_l … … 1418 1433  2: * ] 1419 1434 ] 1420  27:@(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1435  @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1421 1436 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1422 1437 @Exists_append_r @Exists_append_l @Exists_append_l … … 1430 1445  2: * ] 1431 1446 ] 1432  28: whd %1 %1 normalize /2/ 1433  29: whd %1 %1 normalize 1434 @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 1435 whd %1 // 1436  32: whd %1 %2 whd @(ex_intro … l) @E 1447  whd %1 %1 normalize /2/ 1448  whd %1 %1 normalize 1449 @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 1450 whd %1 // 1451  normalize %2 /3/ 1452  normalize /4/ 1453  whd %1 %2 whd @(ex_intro … l) @E 1437 1454 ] qed. 1438 1455
Note: See TracChangeset
for help on using the changeset viewer.