Changeset 2251 for src/Clight/toCminor.ma
- Timestamp:
- Jul 24, 2012, 7:40:21 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/toCminor.ma
r2250 r2251 1097 1097 stmt_P (λs1. stmt_labels (λl.ldefined s' l ∨ lpresent lbls l ∨ In ? l (labels_of_flag flag)) s1) s'. 1098 1098 1099 definition return_ok : option typ → stmt → Prop ≝ 1100 λot. 1101 stmt_P (λs. 1102 match s with [ St_return oe ⇒ 1103 match oe with [ Some e ⇒ Some ? (dpi1 … e) = ot | None ⇒ None ? = ot ] 1104 | _ ⇒ True ]). 1105 1099 1106 (* trans_inv is the invariant which is enforced during the translation from Clight to Cminor. 1100 1107 The involved arguments are the following: … … 1106 1113 . su', a couple of a Cminor statement and fresh variable generator. 1107 1114 *) 1108 definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → ((tmpgen vars) × labgen × stmt) → Prop ≝1109 λvars,lbls,s,uv,flag, su'.1115 definition trans_inv : ∀vars:var_types . ∀lbls:lenv . statement → tmpgen vars → convert_flag → option typ → ((tmpgen vars) × labgen × stmt) → Prop ≝ 1116 λvars,lbls,s,uv,flag,rettyp,su'. 1110 1117 let 〈uv', ul', s'〉 ≝ su' in 1111 1118 stmt_inv (add_tmps vars (tmp_env … uv')) s' ∧ (* remaining variables in s' are local*) 1112 1119 labels_translated lbls s s' ∧ (* all the labels in s are transformed in label of s' using [lbls] as a map *) 1113 1120 tmps_preserved vars uv uv' ∧ (* the variables generated are local and grows in a monotonic fashion *) 1121 return_ok rettyp s' ∧ (* return statements have correct typ *) 1114 1122 label_wf s s' lbls flag. (* labels are "properly" declared, as defined in [ŀabel_wf].*) 1115 1116 let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (s:statement) on s 1117 : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) ≝ 1118 match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag su) with 1123 1124 axiom ReturnMismatch : String. 1125 1126 let rec translate_statement (vars:var_types) (uv:tmpgen vars) (ul:labgen) (lbls:lenv) (flag:convert_flag) (rettyp:option typ) (s:statement) on s 1127 : res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) ≝ 1128 match s return λs.res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls s uv flag rettyp su) with 1119 1129 [ Sskip ⇒ OK ? «〈uv, ul, St_skip〉, ?» 1120 1130 | Sassign e1 e2 ⇒ … … 1144 1154 ] 1145 1155 | Ssequence s1 s2 ⇒ 1146 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;1147 do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag s2;1156 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1; 1157 do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2; 1148 1158 OK ? «〈fgens2, St_seq s1' s2'〉, ?» 1149 1159 | Sifthenelse e1 s1 s2 ⇒ … … 1151 1161 match typ_of_type (typeof e1) return λx.(Σe:CMexpr x.expr_vars ? e ?) → ? with 1152 1162 [ ASTint _ _ ⇒ λe1'. 1153 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;1154 do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag s2;1163 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1; 1164 do «fgens2, s2', H2» ← translate_statement vars (fst … fgens1) (snd … fgens1) lbls flag rettyp s2; 1155 1165 OK ? «〈fgens2, St_ifthenelse ?? e1' s1' s2'〉, ?» 1156 1166 | _ ⇒ λ_.Error ? (msg TypeMismatch) … … 1163 1173 let 〈labels, ul1〉 as E1 ≝ mklabels ul in 1164 1174 let 〈entry, exit〉 as E2 ≝ labels in 1165 do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) s1;1175 do «fgens2, s1',H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1; 1166 1176 let converted_loop ≝ 1167 1177 St_label entry … … 1179 1189 let 〈labels, ul1〉 as E1 ≝ mklabels ul in 1180 1190 let 〈entry, exit〉 as E2 ≝ labels in 1181 do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) s1;1191 do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls (ConvertTo entry exit) rettyp s1; 1182 1192 let converted_loop ≝ 1183 1193 St_label entry … … 1199 1209 let 〈labels, ul1〉 as E ≝ mklabels ul in 1200 1210 let 〈entry, exit〉 as E2 ≝ labels in 1201 do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag s1;1202 do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) s2;1203 do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) s3;1211 do «fgens2, s1', H1» ← translate_statement vars uv ul1 lbls flag rettyp s1; 1212 do «fgens3, s2', H2» ← translate_statement vars (fst … fgens2) (snd … fgens2) lbls (ConvertTo entry exit) rettyp s2; 1213 do «fgens4, s3', H3» ← translate_statement vars (fst … fgens3) (snd … fgens3) lbls (ConvertTo entry exit) rettyp s3; 1204 1214 (* TODO: this is a little different from the prototype and CompCert, is it OK? *) 1205 1215 let converted_loop ≝ … … 1231 1241 | Sreturn ret ⇒ 1232 1242 match ret with 1233 [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?» 1243 [ None ⇒ 1244 match rettyp return λx.res (Σy.trans_inv … x y) with 1245 [ None ⇒ OK ? «〈uv, ul, St_return (None ?)〉, ?» 1246 | _ ⇒ Error ? (msg ReturnMismatch) 1247 ] 1234 1248 | Some e1 ⇒ 1235 do e1' ← translate_expr vars e1; 1236 OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?» 1249 match rettyp return λx.res (Σy.trans_inv … x y) with 1250 [ Some rty ⇒ 1251 do e1' ← translate_expr vars e1; 1252 do e1' ← typ_should_eq (typ_of_type (typeof e1)) rty ? e1'; 1253 OK ? «〈uv, ul, St_return (Some ? (mk_DPair … e1'))〉, ?» 1254 | _ ⇒ Error ? (msg ReturnMismatch) 1255 ] 1237 1256 ] 1238 1257 | Sswitch e1 ls ⇒ Error ? (msg FIXME) 1239 1258 | Slabel l s1 ⇒ 1240 1259 do l' as E ← lookup_label lbls l; 1241 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;1260 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1; 1242 1261 OK ? «〈fgens1, St_label l' s1'〉, ?» 1243 1262 | Sgoto l ⇒ … … 1245 1264 OK ? «〈uv, ul, St_goto l'〉, ?» 1246 1265 | Scost l s1 ⇒ 1247 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag s1;1266 do «fgens1, s1', H1» ← translate_statement vars uv ul lbls flag rettyp s1; 1248 1267 OK ? «〈fgens1, St_cost l s1'〉, ?» 1249 1268 ]. 1250 try @conj try @conj try @conj try @conj try @conj try @conj try @conj 1269 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj 1251 1270 try (@I) 1252 1271 try (#l #H elim H) … … 1254 1273 try (#H1 try #H2 assumption) 1255 1274 [ 1,5: @(tmp_preserved … p) ] 1256 [ 1,3: elim e2' | 2,9 : elim e1' | 4,7,14: elim ef' ]1257 [ 1,2,3,4,5,6,7 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ]1275 [ 1,3: elim e2' | 2,9,24: elim e1' | 4,7,14: elim ef' ] 1276 [ 1,2,3,4,5,6,7,8 : #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) ] 1258 1277 [ 1: @All_mp [ 1: @(λe.match e with [ mk_DPair t e0 ⇒ expr_vars t e0 (local_id vars) ]) 1259 1278 | 2: * #t #e #Hev whd in Hev ⊢ %; @(expr_vars_mp … Hev) #i #t #Hp @(tmp_preserved … Hp) … … 1272 1291 [ 1: #size #sign | 2: | 3: #fsize ] 1273 1292 [ 1,2,3: #H @(alloc_tmp_preserves vars tmp uv uv1 … Etmp) @H ] 1293 try @refl (* Does (at least) the return_ok cases *) 1274 1294 try @(match fgens1 return λx.x=fgens1 → ? with 1275 1295 [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1)) … … 1281 1301 [ mk_Prod uv4 ul4 ⇒ λHfgens4.? ] (refl ? fgens4)) 1282 1302 whd in H1 H2 H3 ⊢ ?; destruct whd nodelta in H1 H2 H3; 1283 try (elim H1 -H1 * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1)1284 try (elim H2 -H2 * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2)1285 try (elim H3 -H3 * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3)1286 [ 1,2: #Hind1 #Hind2 | 3,4, 9,11: #Hind | 5: #Hind1 #Hind2 #Hind3 ]1287 try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption1303 try (elim H1 -H1 * * * #Hstmt_inv1 #Hlabels_tr1 #Htmps_pres1 #Hret1) 1304 try (elim H2 -H2 * * * #Hstmt_inv2 #Hlabels_tr2 #Htmps_pres2 #Hret2) 1305 try (elim H3 -H3 * * * #Hstmt_inv3 #Hlabels_tr3 #Htmps_pres3 #Hret3) 1306 [ 1,2: #Hind1 #Hind2 | 3,4,8,10: #Hind | 5: #Hind1 #Hind2 #Hind3 ] 1307 try @conj try @conj try @conj try @conj try @conj try @conj try (whd @I) try assumption 1288 1308 [ 1,7: @(stmt_P_mp … Hstmt_inv1) #e #Hvars @(stmt_vars_mp … Hvars) #i #t #Hlocal @(Htmps_pres2 … Hlocal) 1289 1309 | 2: #l #H cases (Exists_append ???? H) #Hcase … … 1318 1338 | 2,5: #H %1 %2 assumption 1319 1339 | 3,6: #H %2 assumption ] ] 1320 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I 1321 [ 1, 9,19,32: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal)1322 | 2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) //1323 | 3,10: whd #l #H normalize in H;1340 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I try assumption 1341 [ 1,7,17: whd elim e1' #e #Hvars @(expr_vars_mp … Hvars) #i #t #Hlocal @(tmp_preserved … Hlocal) 1342 | (*2,8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) // 1343 |*) 2,8: whd #l #H normalize in H; 1324 1344 elim (Hlabels_tr1 … H) #label #Hlabel @(ex_intro … label) 1325 1345 @conj … … 1327 1347 | 2,4: whd @or_intror normalize @Exists_append_l @Exists_append_l try @Exists_append_l 1328 1348 @(proj2 … Hlabel) ] 1329 | 30: whd %2 %2 whd /2/1330 | 31: whd %2 whd /2/1331 | 4,16: whd %1 %1 normalize /2/1332 | 5,12: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1349 | 27: whd %2 %2 whd /2/ 1350 | 28: whd %2 whd /2/ 1351 | 3,14: whd %1 %1 normalize /2/ 1352 | 4,10: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1333 1353 #l * try * [ 1,5: #H %1 %1 normalize %2 @Exists_append_l @Exists_append_l try @Exists_append_l @H 1334 1354 | 2,6: #H %1 %2 assumption … … 1338 1358 | 2,4: * ] 1339 1359 ] 1340 | 6: normalize %1 %1 %1 //1341 | 7,14: normalize %1 %1 %2 @Exists_append_r normalize /2/1342 | 11,13: whd %1 %1 normalize /2/1343 | 1 5: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ]1360 | 5: normalize %1 %1 %1 // 1361 | 6,12: normalize %1 %1 %2 @Exists_append_r normalize /2/ 1362 | 9,11: whd %1 %1 normalize /2/ 1363 | 13: whd #label * [ 1: #Eq @(ex_intro … l') @conj [ 1: destruct // | whd /2/ ] 1344 1364 | 2: #H elim (Hlabels_tr1 label H) 1345 1365 #lab * #Hlookup #Hdef @(ex_intro … lab) @conj 1346 1366 [ 1: // | 2: whd %2 assumption ] 1347 1367 ] 1348 | 1 7: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1368 | 15: @(stmt_P_mp … Hind) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1349 1369 #l * try * [ 1: #H %1 %1 normalize %2 @H 1350 1370 | 2: #H %1 %2 assumption 1351 1371 | 3: #H %2 assumption ] 1352 | 1 8: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t1372 | 16: @(stmt_P_mp … Hstmt_inv1) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1353 1373 #H @(Htmps_pres3 … (Htmps_pres2 … H)) 1354 | 20: @(stmt_P_mp … Hstmt_inv3) // 1355 | 21: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1374 | 18: @(stmt_P_mp … Hstmt_inv2) #s0 #Hstmt_vars @(stmt_vars_mp … Hstmt_vars) #i #t 1356 1375 #H @(Htmps_pres3 … H) 1357 | 22: whd #l #H normalize in H;1376 | 19: whd #l #H normalize in H; 1358 1377 cases (Exists_append … H) #Hcase 1359 1378 [ 1: elim (Hlabels_tr1 l Hcase) #label #Hlabel @(ex_intro … label) @conj … … 1376 1395 ] 1377 1396 ] 1378 | 2 3: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H)))1379 | 2 4: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1397 | 20: #id #ty #H @(Htmps_pres3 … (Htmps_pres2 … (Htmps_pres1 … H))) 1398 | 21: @(stmt_P_mp … Hind3) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1380 1399 #l * try * [ 1: #H %1 %1 normalize @Exists_append_l @H 1381 1400 | 2: #H %1 %2 assumption 1382 1401 | 3: #H %2 assumption ] 1383 | 2 5: whd %1 %1 normalize /2/1384 | 2 6: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1402 | 22: whd %1 %1 normalize /2/ 1403 | 23: @(stmt_P_mp … Hind1) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1385 1404 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1386 1405 @Exists_append_r @Exists_append_l @Exists_append_l … … 1395 1414 | 2: * ] 1396 1415 ] 1397 | 2 7: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels)1416 | 24: @(stmt_P_mp … Hind2) #s0 #Hstmt_labels @(stmt_labels_mp … Hstmt_labels) 1398 1417 #l * try * [ 1: #H %1 %1 normalize @Exists_append_r @(Exists_add ?? (nil ?)) 1399 1418 @Exists_append_r @Exists_append_l @Exists_append_l … … 1407 1426 | 2: * ] 1408 1427 ] 1409 | 2 8: whd %1 %1 normalize /2/1410 | 2 9: whd %1 %1 normalize1428 | 25: whd %1 %1 normalize /2/ 1429 | 26: whd %1 %1 normalize 1411 1430 @Exists_append_r @(Exists_add ?? (nil ?)) @Exists_append_r @Exists_append_r 1412 1431 whd %1 // 1413 | 33: whd %1 %2 whd @(ex_intro … l) @E1432 | 29: whd %1 %2 whd @(ex_intro … l) @E 1414 1433 ] qed. 1415 1434 … … 1418 1437 (* params and statement aren't real parameters, they're just there for giving the invariant. *) 1419 1438 definition alloc_params : 1420 ∀vars:var_types.∀lbls,statement,uv,flag . list (ident×type) → (Σsu:(tmpgen vars)×labgen×stmt. trans_inv vars lbls statement uv flagsu)1421 → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag su) ≝1422 λvars,lbls,statement,uv,ul, params,s. foldl ?? (λsu,it.1439 ∀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) 1440 → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv flag rettyp su) ≝ 1441 λvars,lbls,statement,uv,ul,rettyp,params,s. foldl ?? (λsu,it. 1423 1442 let 〈id,ty〉 ≝ it in 1424 1443 do «result,Is» ← su; 1425 1444 let 〈fgens1, s〉 as Eresult ≝ result in 1426 1445 do 〈t,ty'〉 as E ← lookup' vars id; 1427 match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul su) with1446 match t return λx.? → res (Σsu:(tmpgen vars)×labgen×stmt.trans_inv vars lbls statement uv ul rettyp su) with 1428 1447 [ Local ⇒ λE. OK (Σs:(tmpgen vars)×labgen×stmt.?) «result,Is» 1429 1448 | Stack n ⇒ λE. … … 1435 1454 [ mk_Prod uv1 ul1 ⇒ λHfgens1.? ] (refl ? fgens1)) 1436 1455 whd in Is ⊢ %; destruct whd in Is; 1437 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @ I1438 elim Is * * #Hincl #Hstmt_inv #Hlab_tr#Htmp_pr try assumption1456 try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @conj try @I 1457 elim Is * * * #Hincl #Hstmt_inv #Hlab_tr #Hret #Htmp_pr try assumption 1439 1458 @(expr_vars_mp … (tmp_preserved … uv1)) whd >E @refl 1440 1459 qed. … … 1551 1570 let 〈vartypes, stacksize〉 as E ≝ characterise_vars globals f in 1552 1571 let uv ≝ mk_tmpgen vartypes tmpuniverse [ ] ?? in 1553 do s0 ← translate_statement vartypes uv ul lbls DoNotConvert ( fn_body f);1554 do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert ( fn_params f) s0;1572 do s0 ← translate_statement vartypes uv ul lbls DoNotConvert (opttyp_of_type (fn_return f)) (fn_body f); 1573 do «fgens, s1, Is» ← alloc_params vartypes lbls ? uv DoNotConvert (opttyp_of_type (fn_return f)) (fn_params f) s0; 1555 1574 let params ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params f) in 1556 1575 let vars ≝ map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (tmp_env ? (fst ?? fgens) @ fn_vars f) in … … 1570 1589 [ mk_Prod uv' ul' ⇒ λHfgens.? ] (refl ? fgens)) 1571 1590 whd in Is; <Hfgens in Is; #Is whd in Is ⊢ %; 1572 elim Is * * #Hstmt_inv #Hlab_trans #Htmps_pres#Hlabel_wf1591 elim Is * * * #Hstmt_inv #Hlab_trans #Htmps_pres #Hreturn #Hlabel_wf 1573 1592 (* merge Hlabel_wf with Hstmt_inv and eliminate right away *) 1574 @(stmt_P_mp … (stmt_P_conj … Hstmt_inv Hlabel_wf))1575 #s * #Hstmt_vars #Hstmt_labels%1593 @(stmt_P_mp … (stmt_P_conj … (stmt_P_conj … Hstmt_inv Hlabel_wf) Hreturn)) 1594 #s * * #Hstmt_vars #Hstmt_labels #Hstmt_return % 1576 1595 [ 1: (* prove that variables are either parameters or locals *) 1577 1596 @(stmt_vars_mp … Hstmt_vars) #i #t #H … … 1596 1615 #H @H 1597 1616 ] 1617 | cases s in Hstmt_return; // * normalize [2: * #t #e ] 1618 cases (fn_return f) normalize #A try #B try #C try #D try #E destruct // 1598 1619 ] 1599 1620 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.