 Timestamp:
 Jul 14, 2011, 2:27:41 PM (9 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/RTL/RTL.ma
r1066 r1068 26 26  rtl_st_cond: register → label → label → rtl_statement 27 27  rtl_st_set_carry: label → rtl_statement 28  rtl_st_return: r egisters → rtl_statement.28  rtl_st_return: rtl_statement. (* XXX: change from o'caml *) 29 29 30 30 definition rtl_statement_graph ≝ graph rtl_statement. … … 34 34 rtl_if_luniverse: universe LabelTag; 35 35 rtl_if_runiverse: universe RegisterTag; 36 rtl_if_sig: signature; 36 (* rtl_if_sig: signature;  dropped in front end *) 37 37 rtl_if_result: registers; 38 38 rtl_if_params: registers; … … 44 44 }. 45 45 46 inductive rtl_function_definition: Type[0] ≝ 47  rtl_f_internal: rtl_internal_function → rtl_function_definition 48  rtl_f_external: external_function → rtl_function_definition. 46 definition rtl_function_definition ≝ fundef rtl_internal_function. 49 47 50 48 record rtl_program: Type[0] ≝ 
src/RTLabs/RTLAbstoRTL.ma
r1067 r1068 11 11 let rtl_if_luniverse' ≝ rtl_if_luniverse p in 12 12 let rtl_if_runiverse' ≝ rtl_if_runiverse p in 13 let rtl_if_sig' ≝ rtl_if_sig p in14 13 let rtl_if_result' ≝ rtl_if_result p in 15 14 let rtl_if_params' ≝ rtl_if_params p in … … 19 18 let rtl_if_entry' ≝ rtl_if_entry p in 20 19 let rtl_if_exit' ≝ rtl_if_exit p in 21 mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' rtl_if_sig'20 mk_rtl_internal_function rtl_if_luniverse' rtl_if_runiverse' 22 21 rtl_if_params' rtl_if_params' rtl_if_locals' 23 22 rtl_if_stacksize' rtl_if_graph' rtl_if_entry' … … 30 29 let rtl_if_luniverse' ≝ new_univ in 31 30 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 32 let rtl_if_sig' ≝ rtl_if_sig def in33 31 let rtl_if_result' ≝ rtl_if_result def in 34 32 let rtl_if_params' ≝ rtl_if_params def in … … 39 37 let rtl_if_exit' ≝ rtl_if_exit def in 40 38 〈mk_rtl_internal_function 41 rtl_if_luniverse' rtl_if_runiverse' rtl_if_ sig' rtl_if_result'39 rtl_if_luniverse' rtl_if_runiverse' rtl_if_result' 42 40 rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph' 43 41 rtl_if_entry' rtl_if_exit', lbl〉. … … 51 49 let rtl_if_luniverse' ≝ rtl_if_luniverse def in 52 50 let rtl_if_runiverse' ≝ rtl_if_runiverse def in 53 let rtl_if_sig' ≝ rtl_if_sig def in54 51 let rtl_if_result' ≝ rtl_if_result def in 55 52 let rtl_if_params' ≝ rtl_if_params def in … … 60 57 let rtl_if_exit' ≝ rtl_if_exit def in 61 58 〈mk_rtl_internal_function 62 rtl_if_luniverse' rtl_if_runiverse' rtl_if_ sig' rtl_if_result'59 rtl_if_luniverse' rtl_if_runiverse' rtl_if_result' 63 60 rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph' 64 61 rtl_if_entry' rtl_if_exit', r〉. … … 258 255  rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl 259 256  rtl_st_set_carry l ⇒ rtl_st_set_carry lbl 260  rtl_st_return r ⇒ rtl_st_return r257  rtl_st_return ⇒ rtl_st_return 261 258 ]. 262 259 … … 1157 1154 definition translate_stmt ≝ 1158 1155 λlenv. 1159 λret: register. (* change from o'caml code, this is taken from func. record *)1160 1156 λlbl: label. 1161 1157 λstmt. … … 1197 1193 translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def 1198 1194  St_jumptable r l ⇒ ? (* assert false: not implemented yet *) 1199  St_return ⇒ add_graph lbl (rtl_st_return (find_local_env ret lenv))def1195  St_return ⇒ add_graph lbl rtl_st_return def 1200 1196 ]. 1201 1197 [10: cases not_implemented (* jtable case *) … … 1208 1204 let runiverse ≝ f_reggen def in 1209 1205 let lenv ≝ initialize_local_env runiverse 1210 (f_params def @ f_locals def) (f_result def) in ?. 1211 1212 let translate_internal def = 1213 let runiverse = def.RTLabs.f_runiverse in 1214 let lenv = 1215 initialize_local_env runiverse 1216 (def.RTLabs.f_params @ def.RTLabs.f_locals) def.RTLabs.f_result in 1217 let set_of_list l = List.fold_right Register.Set.add l Register.Set.empty in 1218 let params = map_list_local_env lenv (List.map fst def.RTLabs.f_params) in 1219 let locals = map_list_local_env lenv (List.map fst def.RTLabs.f_locals) in 1220 let locals = set_of_list locals in 1221 let result = match def.RTLabs.f_result with 1222  None > [] 1223  Some (r, _) > find_local_env r lenv in 1224 let res = 1225 { RTL.f_luniverse = def.RTLabs.f_luniverse ; 1226 RTL.f_runiverse = runiverse ; 1227 RTL.f_result = result ; 1228 RTL.f_params = params ; 1229 RTL.f_locals = locals ; 1230 RTL.f_stacksize = concrete_size def.RTLabs.f_stacksize ; 1231 RTL.f_graph = Label.Map.empty ; 1232 RTL.f_entry = def.RTLabs.f_entry ; 1233 RTL.f_exit = def.RTLabs.f_exit } in 1234 Label.Map.fold (translate_stmt lenv) def.RTLabs.f_graph res 1235 1236 definition filter_and_to_list_local_env_internal ≝ 1237 λlenv. 1238 λl. 1239 λr. 1240 match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with 1241 [ Some entry ⇒ 1242 match entry with 1243 [ register_ptr r1 r2 ⇒ (l @ [ r1; r2 ]) 1244  register_int r ⇒ (l @ [ r ]) 1245 ] 1246  None ⇒ [ ] (* dpm: should this be none? *) 1247 ]. 1248 1249 definition filter_and_to_list_local_env ≝ 1250 λlenv. 1251 λregisters. 1252 foldl ? ? (filter_and_to_list_local_env_internal lenv) [ ] registers. 1253 1254 definition list_of_register_type ≝ 1255 λrt. 1256 match rt with 1257 [ register_ptr r1 r2 ⇒ [ r1; r2 ] 1258  register_int r ⇒ [ r ] 1259 ]. 1260 1261 definition find_and_list ≝ 1262 λr. 1263 λlenv. 1264 match assoc_list_lookup ? ? r (eq_identifier RegisterTag) lenv with 1265 [ None ⇒ [ ] (* dpm: should this be none? *) 1266  Some lkup ⇒ list_of_register_type lkup 1267 ]. 1268 1269 definition find_and_list_args ≝ 1270 λargs. 1271 λlenv. 1272 map ? ? (λr. find_and_list r lenv) args. 1273 1274 (* dpm: horrendous, use dependent types. 1275 length destr = length srcrs *) 1276 let rec translate_move (destrs: ?) (srcrs: ?) (start_lbl: label) 1277 (dest_lbl: label) (def: ?) ≝ 1278 match destrs with 1279 [ nil ⇒ 1280 match srcrs with 1281 [ nil ⇒ Some ? def 1282  cons hd tl ⇒ None ? 1283 ] 1284  cons hd tl ⇒ 1285 match srcrs with 1286 [ nil ⇒ None ? 1287  cons hd' tl' ⇒ 1288 match tl with 1289 [ nil ⇒ 1290 match tl' with 1291 (* one element lists *) 1292 [ nil ⇒ Some ? (add_graph start_lbl (rtl_st_move hd hd' dest_lbl) def) 1293  cons hd'' tl'' ⇒ None ? 1294 ] 1295  cons hd'' tl'' ⇒ 1296 match tl' with 1297 [ nil ⇒ None ? 1298 (* multielement lists *) 1299  cons hd''' tl''' ⇒ 1300 let tmp_lbl ≝ fresh_label def in 1301 match tmp_lbl with 1302 [ None ⇒ None ? 1303  Some tmp_lbl ⇒ 1304 let def ≝ add_graph start_lbl (rtl_st_move hd hd' tmp_lbl) def in 1305 translate_move tl tl' tmp_lbl dest_lbl def 1306 ] 1307 ] 1308 ] 1309 ] 1310 ]. 1311 1312 definition extract_singleton ≝ 1313 λA: Type[0]. 1314 λl: list A. 1315 match l with 1316 [ nil ⇒ None ? 1317  cons hd tl ⇒ 1318 match tl with 1319 [ nil ⇒ Some ? hd 1320  cons hd tl ⇒ None ? 1321 ] 1322 ]. 1323 1324 definition extract_pair ≝ 1325 λA: Type[0]. 1326 λl: list A. 1327 match l with 1328 [ nil ⇒ None ? 1329  cons hd tl ⇒ 1330 match tl with 1331 [ nil ⇒ None ? 1332  cons hd' tl' ⇒ 1333 match tl' with 1334 [ nil ⇒ Some ? 〈hd, hd'〉 1335  cons hd'' tl'' ⇒ None ? 1336 ] 1337 ] 1338 ]. 1339 1340 definition translate_op1 ≝ 1341 λop1. 1342 λdestrs. 1343 λsrcrs. 1344 λstart_lbl. 1345 λdest_lbl. 1346 λdef. 1347 match op1 with 1348 [ op_cast8_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def 1349  op_cast8_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def 1350  op_cast16_unsigned ⇒ translate_move destrs srcrs start_lbl dest_lbl def 1351  op_cast16_signed ⇒ translate_move destrs srcrs start_lbl dest_lbl def 1352  op_neg_int ⇒ 1353 let dstr ≝ extract_singleton ? destrs in 1354 let srcr ≝ extract_singleton ? srcrs in 1355 match dstr with 1356 [ None ⇒ None ? 1357  Some dstr ⇒ 1358 match srcr with 1359 [ None ⇒ None ? 1360  Some srcr ⇒ 1361 adds_graph [ 1362 rtl_st_op1 Cmpl dstr srcr start_lbl; 1363 rtl_st_op1 Inc dstr dstr start_lbl 1364 ] start_lbl dest_lbl def 1365 ] 1366 ] 1367  op_not_int ⇒ 1368 let dstr ≝ extract_singleton ? destrs in 1369 let srcr ≝ extract_singleton ? srcrs in 1370 match dstr with 1371 [ None ⇒ None ? 1372  Some dstr ⇒ 1373 match srcr with 1374 [ None ⇒ None ? 1375  Some srcr ⇒ 1376 adds_graph [ 1377 rtl_st_op1 Cmpl dstr srcr start_lbl 1378 ] start_lbl dest_lbl def 1379 ] 1380 ] 1381  op_id ⇒ translate_move destrs srcrs start_lbl dest_lbl def 1382  op_ptr_of_int ⇒ 1383 let destr12 ≝ extract_pair ? destrs in 1384 let srcr ≝ extract_singleton ? srcrs in 1385 match destr12 with 1386 [ None ⇒ None ? 1387  Some destr12 ⇒ 1388 let 〈destr1, destr2〉 ≝ destr12 in 1389 match srcr with 1390 [ None ⇒ None ? 1391  Some srcr ⇒ 1392 adds_graph [ 1393 rtl_st_move destr1 srcr dest_lbl; 1394 rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl 1395 ] start_lbl dest_lbl def 1396 ] 1397 ] 1398  op_int_of_ptr ⇒ 1399 let destr ≝ extract_singleton ? destrs in 1400 match destr with 1401 [ None ⇒ None ? 1402  Some destr ⇒ 1403 match srcrs with 1404 [ nil ⇒ None ? 1405  cons srcr tl ⇒ 1406 Some ? (add_graph start_lbl (rtl_st_move destr srcr dest_lbl) def) 1407 ] 1408 ] 1409  op_not_bool ⇒ 1410 let destr ≝ extract_singleton ? destrs in 1411 let srcrs ≝ extract_singleton ? srcrs in 1412 match destr with 1413 [ None ⇒ None ? 1414  Some destr ⇒ 1415 match srcrs with 1416 [ None ⇒ None ? 1417  Some srcr ⇒ 1418 let 〈def, tmpr〉 ≝ fresh_reg def in 1419 adds_graph [ 1420 rtl_st_int tmpr (bitvector_of_nat ? 0) start_lbl; 1421 rtl_st_clear_carry start_lbl; 1422 rtl_st_op2 Sub destr tmpr srcr start_lbl; 1423 rtl_st_int destr (bitvector_of_nat ? 0) dest_lbl; 1424 rtl_st_op2 Addc destr destr destr start_lbl; 1425 rtl_st_int tmpr (bitvector_of_nat ? 1) dest_lbl; 1426 rtl_st_op2 Xor destr destr tmpr start_lbl 1427 ] start_lbl dest_lbl def 1428 ] 1429 ] 1430  _ ⇒ None ? (* error float *) 1431 ]. 1432 1433 definition translate_condptr ≝ 1434 λr1. 1435 λr2. 1436 λstart_lbl: label. 1437 λlbl_true: label. 1438 λlbl_false: label. 1439 λdef. 1440 let 〈def, tmpr〉 ≝ fresh_reg def in 1441 adds_graph [ 1442 rtl_st_op2 Or tmpr r1 r2 start_lbl; 1443 rtl_st_cond_acc tmpr lbl_true lbl_false 1444 ] start_lbl start_lbl def. 1445 1446 1447 1448 (* 1449 let rec translate_op2 (op2: ?) (destrs: ?) (srcrs1: ?) (srcrs2: ?) 1450 (start_lbl: label) (dest_lbl: label) (def: ?) on op2 ≝ 1451 match op2 with 1452 [ op_add ⇒ 1453 let destr ≝ extract_singleton ? destrs in 1454 let srcr1 ≝ extract_singleton ? srcrs1 in 1455 let srcr2 ≝ extract_singleton ? srcrs2 in 1456 match destr with 1457 [ None ⇒ None ? 1458  Some destr ⇒ 1459 match srcr1 with 1460 [ None ⇒ None ? 1461  Some srcr1 ⇒ 1462 match srcr2 with 1463 [ None ⇒ None ? 1464  Some srcr2 ⇒ 1465 adds_graph [ 1466 rtl_st_op2 Add destr srcr1 srcr2 start_lbl 1467 ] start_lbl dest_lbl def 1468 ] 1469 ] 1470 ] 1471  op_sub ⇒ 1472 let destr ≝ extract_singleton ? destrs in 1473 let srcr1 ≝ extract_singleton ? srcrs1 in 1474 let srcr2 ≝ extract_singleton ? srcrs2 in 1475 match destr with 1476 [ None ⇒ None ? 1477  Some destr ⇒ 1478 match srcr1 with 1479 [ None ⇒ None ? 1480  Some srcr1 ⇒ 1481 match srcr2 with 1482 [ None ⇒ None ? 1483  Some srcr2 ⇒ 1484 adds_graph [ 1485 rtl_st_clear_carry start_lbl; 1486 rtl_st_op2 Sub destr srcr1 srcr2 start_lbl 1487 ] start_lbl dest_lbl def 1488 ] 1489 ] 1490 ] 1491  op_mul ⇒ 1492 let destr ≝ extract_singleton ? destrs in 1493 let srcr1 ≝ extract_singleton ? srcrs1 in 1494 let srcr2 ≝ extract_singleton ? srcrs2 in 1495 match destr with 1496 [ None ⇒ None ? 1497  Some destr ⇒ 1498 match srcr1 with 1499 [ None ⇒ None ? 1500  Some srcr1 ⇒ 1501 match srcr2 with 1502 [ None ⇒ None ? 1503  Some srcr2 ⇒ 1504 adds_graph [ 1505 rtl_st_opaccs Mul destr srcr1 srcr2 start_lbl 1506 ] start_lbl dest_lbl def 1507 ] 1508 ] 1509 ] 1510  op_div ⇒ None ? (* signed div not supported *) 1511  op_divu ⇒ 1512 let destr ≝ extract_singleton ? destrs in 1513 let srcr1 ≝ extract_singleton ? srcrs1 in 1514 let srcr2 ≝ extract_singleton ? srcrs2 in 1515 match destr with 1516 [ None ⇒ None ? 1517  Some destr ⇒ 1518 match srcr1 with 1519 [ None ⇒ None ? 1520  Some srcr1 ⇒ 1521 match srcr2 with 1522 [ None ⇒ None ? 1523  Some srcr2 ⇒ 1524 adds_graph [ 1525 rtl_st_opaccs Divu destr srcr1 srcr2 start_lbl 1526 ] start_lbl dest_lbl def 1527 ] 1528 ] 1529 ] 1530  op_modu ⇒ 1531 let destr ≝ extract_singleton ? destrs in 1532 let srcr1 ≝ extract_singleton ? srcrs1 in 1533 let srcr2 ≝ extract_singleton ? srcrs2 in 1534 match destr with 1535 [ None ⇒ None ? 1536  Some destr ⇒ 1537 match srcr1 with 1538 [ None ⇒ None ? 1539  Some srcr1 ⇒ 1540 match srcr2 with 1541 [ None ⇒ None ? 1542  Some srcr2 ⇒ 1543 adds_graph [ 1544 rtl_st_opaccs Modu destr srcr1 srcr2 start_lbl 1545 ] start_lbl dest_lbl def 1546 ] 1547 ] 1548 ] 1549  op_mod ⇒ None ? (* signed mod not supported *) 1550  op_and ⇒ 1551 let destr ≝ extract_singleton ? destrs in 1552 let srcr1 ≝ extract_singleton ? srcrs1 in 1553 let srcr2 ≝ extract_singleton ? srcrs2 in 1554 match destr with 1555 [ None ⇒ None ? 1556  Some destr ⇒ 1557 match srcr1 with 1558 [ None ⇒ None ? 1559  Some srcr1 ⇒ 1560 match srcr2 with 1561 [ None ⇒ None ? 1562  Some srcr2 ⇒ 1563 adds_graph [ 1564 rtl_st_op2 And destr srcr1 srcr2 start_lbl 1565 ] start_lbl dest_lbl def 1566 ] 1567 ] 1568 ] 1569  op_or ⇒ 1570 let destr ≝ extract_singleton ? destrs in 1571 let srcr1 ≝ extract_singleton ? srcrs1 in 1572 let srcr2 ≝ extract_singleton ? srcrs2 in 1573 match destr with 1574 [ None ⇒ None ? 1575  Some destr ⇒ 1576 match srcr1 with 1577 [ None ⇒ None ? 1578  Some srcr1 ⇒ 1579 match srcr2 with 1580 [ None ⇒ None ? 1581  Some srcr2 ⇒ 1582 adds_graph [ 1583 rtl_st_op2 Or destr srcr1 srcr2 start_lbl 1584 ] start_lbl dest_lbl def 1585 ] 1586 ] 1587 ] 1588  op_xor ⇒ 1589 let destr ≝ extract_singleton ? destrs in 1590 let srcr1 ≝ extract_singleton ? srcrs1 in 1591 let srcr2 ≝ extract_singleton ? srcrs2 in 1592 match destr with 1593 [ None ⇒ None ? 1594  Some destr ⇒ 1595 match srcr1 with 1596 [ None ⇒ None ? 1597  Some srcr1 ⇒ 1598 match srcr2 with 1599 [ None ⇒ None ? 1600  Some srcr2 ⇒ 1601 adds_graph [ 1602 rtl_st_op2 Xor destr srcr1 srcr2 start_lbl 1603 ] start_lbl dest_lbl def 1604 ] 1605 ] 1606 ] 1607  op_shru ⇒ None ? (* shifts not supported *) 1608  op_shr ⇒ None ? 1609  op_shl ⇒ None ? 1610  op_addf ⇒ None ? (* floats not supported *) 1611  op_subf ⇒ None ? 1612  op_mulf ⇒ None ? 1613  op_divf ⇒ None ? 1614  op_cmpf _ ⇒ None ? 1615  op_addp ⇒ 1616 let destr12 ≝ extract_pair ? destrs in 1617 match destr12 with 1618 [ None ⇒ None ? 1619  Some destr12 ⇒ 1620 let 〈destr1, destr2〉 ≝ destr12 in 1621 let srcr12 ≝ extract_pair ? srcrs1 in 1622 match srcr12 with 1623 [ None ⇒ 1624 let srcr2 ≝ extract_singleton ? srcrs1 in 1625 match srcr2 with 1626 [ None ⇒ None ? 1627  Some srcr2 ⇒ 1628 let srcr12 ≝ extract_pair ? srcrs2 in 1629 match srcr12 with 1630 [ None ⇒ None ? 1631  Some srcr12 ⇒ 1632 let 〈srcr11, srcr12〉 ≝ srcr12 in 1633 let 〈def, tmpr1〉 ≝ fresh_reg def in 1634 let 〈def, tmpr2〉 ≝ fresh_reg def in 1635 adds_graph [ 1636 rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl; 1637 rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl; 1638 rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl; 1639 rtl_st_move destr1 tmpr1 start_lbl 1640 ] start_lbl dest_lbl def 1641 ] 1642 ] 1643  Some srcr12 ⇒ 1644 let 〈srcr11, srcr12〉 ≝ srcr12 in 1645 let srcr2 ≝ extract_singleton ? srcrs2 in 1646 match srcr2 with 1647 [ None ⇒ None ? 1648  Some srcr2 ⇒ 1649 let 〈def, tmpr1〉 ≝ fresh_reg def in 1650 let 〈def, tmpr2〉 ≝ fresh_reg def in 1651 adds_graph [ 1652 rtl_st_op2 Add tmpr1 srcr11 srcr2 start_lbl; 1653 rtl_st_int tmpr2 (bitvector_of_nat ? 0) start_lbl; 1654 rtl_st_op2 Addc destr2 tmpr2 srcr12 start_lbl; 1655 rtl_st_move destr1 tmpr1 start_lbl 1656 ] start_lbl dest_lbl def 1657 ] 1658 ] 1659 ] 1660  op_subp ⇒ 1661 let destr ≝ extract_singleton ? destrs in 1662 match destr with 1663 [ None ⇒ 1664 let destr12 ≝ extract_pair ? destrs in 1665 match destr12 with 1666 [ None ⇒ None ? 1667  Some destr12 ⇒ 1668 let 〈destr1, destr2〉 ≝ destr12 in 1669 let srcr12 ≝ extract_pair ? srcrs1 in 1670 match srcr12 with 1671 [ None ⇒ None ? 1672  Some srcr12 ⇒ 1673 let 〈srcr11, srcr12〉 ≝ srcr12 in 1674 let srcr2 ≝ extract_singleton ? srcrs2 in 1675 match srcr2 with 1676 [ None ⇒ None ? 1677  Some srcr2 ⇒ 1678 adds_graph [ 1679 rtl_st_clear_carry start_lbl; 1680 rtl_st_op2 Sub destr1 srcr11 srcr2 start_lbl; 1681 rtl_st_int destr2 (bitvector_of_nat ? 0) start_lbl; 1682 rtl_st_op2 Sub destr2 srcr12 destr2 start_lbl 1683 ] start_lbl dest_lbl def 1684 ] 1685 ] 1686 ] 1687  Some destr ⇒ 1688 match srcrs1 with 1689 [ nil ⇒ None ? 1690  cons srcr1 tl ⇒ 1691 match srcrs2 with 1692 [ nil ⇒ None ? 1693  cons srcr2 tl' ⇒ 1694 let 〈def, tmpr1〉 ≝ fresh_reg def in 1695 let 〈def, tmpr2〉 ≝ fresh_reg def in 1696 adds_graph [ 1697 rtl_st_op1 Cmpl tmpr1 srcr2 start_lbl; 1698 rtl_st_int tmpr2 (bitvector_of_nat ? 1) start_lbl; 1699 rtl_st_op2 Add tmpr1 tmpr1 tmpr2 start_lbl; 1700 rtl_st_op2 Add destr srcr1 tmpr1 start_lbl 1701 ] start_lbl dest_lbl def 1702 ] 1703 ] 1704 ] 1705  op_cmp cmp ⇒ 1706 match cmp with 1707 [ Compare_Equal ⇒ 1708 add_translates [ 1709 translate_op2 op_sub destrs srcrs1 srcrs2; 1710 translate_op1 op_not_bool destrs destrs 1711 ] start_lbl dest_lbl def 1712  Compare_NotEqual ⇒ 1713 translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 1714  _ ⇒ None ? 1715 ] 1716  op_cmpu cmp ⇒ 1717 match cmp with 1718 [ Compare_Equal ⇒ 1719 add_translates [ 1720 translate_op2 op_sub destrs srcrs1 srcrs2; 1721 translate_op1 op_not_bool destrs destrs 1722 ] start_lbl dest_lbl def 1723  Compare_NotEqual ⇒ 1724 translate_op2 op_sub destrs srcrs1 srcrs2 start_lbl dest_lbl def 1725  Compare 1726  _ ⇒ None ? 1727 ] 1728  _ ⇒ ? 1729 ]. 1730 1731  AST.Op_cmpu AST.Cmp_lt, [destr], [srcr1], [srcr2] > 1732 let (def, tmpr) = fresh_reg def in 1733 adds_graph 1734 [RTL.St_clear_carry start_lbl ; 1735 RTL.St_op2 (I8051.Sub, destr, srcr1, srcr2, start_lbl) ; 1736 RTL.St_int (destr, 0, start_lbl) ; 1737 RTL.St_op2 (I8051.Addc, destr, destr, destr, start_lbl)] 1738 start_lbl dest_lbl def 1739 1740  AST.Op_cmpu AST.Cmp_gt, _, _, _ > 1741 translate_op2 (AST.Op_cmpu AST.Cmp_lt) 1742 destrs srcrs2 srcrs1 start_lbl dest_lbl def 1743 1744  AST.Op_cmpu AST.Cmp_le, _, _, _ > 1745 add_translates 1746 [translate_op2 (AST.Op_cmpu AST.Cmp_gt) destrs srcrs1 srcrs2 ; 1747 translate_op1 AST.Op_notbool destrs destrs] 1748 start_lbl dest_lbl def 1749 1750  AST.Op_cmpu AST.Cmp_ge, _, _, _ > 1751 add_translates 1752 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) destrs srcrs1 srcrs2 ; 1753 translate_op1 AST.Op_notbool destrs destrs] 1754 start_lbl dest_lbl def 1755 1756  AST.Op_cmp cmp, _, _, _ > 1757 let (def, tmprs1) = fresh_regs def (List.length srcrs1) in 1758 let (def, tmprs2) = fresh_regs def (List.length srcrs2) in 1759 add_translates 1760 [translate_cst (AST.Cst_int 128) tmprs1 ; 1761 translate_cst (AST.Cst_int 128) tmprs2 ; 1762 translate_op2 AST.Op_add tmprs1 srcrs1 tmprs1 ; 1763 translate_op2 AST.Op_add tmprs2 srcrs2 tmprs2 ; 1764 translate_op2 (AST.Op_cmpu cmp) destrs tmprs1 tmprs2] 1765 start_lbl dest_lbl def 1766 1767  AST.Op_cmpp AST.Cmp_eq, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] > 1768 let (def, tmpr) = fresh_reg def in 1769 add_translates 1770 [translate_op2 (AST.Op_cmpu AST.Cmp_ne) [tmpr] [srcr11] [srcr21] ; 1771 translate_op2 (AST.Op_cmpu AST.Cmp_ne) [destr] [srcr21] [srcr22] ; 1772 translate_op2 AST.Op_or [destr] [destr] [tmpr] ; 1773 adds_graph [RTL.St_int (tmpr, 1, start_lbl)] ; 1774 translate_op2 AST.Op_xor [destr] [destr] [tmpr]] 1775 start_lbl dest_lbl def 1776 1777  AST.Op_cmpp AST.Cmp_lt, [destr], [srcr11 ; srcr12], [srcr21 ; srcr22] > 1778 let (def, tmpr1) = fresh_reg def in 1779 let (def, tmpr2) = fresh_reg def in 1780 add_translates 1781 [translate_op2 (AST.Op_cmpu AST.Cmp_lt) [tmpr1] [srcr12] [srcr22] ; 1782 translate_op2 (AST.Op_cmpu AST.Cmp_eq) [tmpr2] [srcr12] [srcr22] ; 1783 translate_op2 (AST.Op_cmpu AST.Cmp_lt) [destr] [srcr11] [srcr21] ; 1784 translate_op2 AST.Op_and [tmpr2] [tmpr2] [destr] ; 1785 translate_op2 AST.Op_or [destr] [tmpr1] [tmpr2]] 1786 start_lbl dest_lbl def 1787 1788  AST.Op_cmpp AST.Cmp_gt, _, _, _ > 1789 translate_op2 (AST.Op_cmpp AST.Cmp_lt) 1790 destrs srcrs2 srcrs1 start_lbl dest_lbl def 1791 1792  AST.Op_cmpp AST.Cmp_le, _, _, _ > 1793 add_translates 1794 [translate_op2 (AST.Op_cmpp AST.Cmp_gt) destrs srcrs1 srcrs2 ; 1795 translate_op1 AST.Op_notbool destrs destrs] 1796 start_lbl dest_lbl def 1797 1798  AST.Op_cmpp AST.Cmp_ge, _, _, _ > 1799 add_translates 1800 [translate_op2 (AST.Op_cmpp AST.Cmp_lt) destrs srcrs1 srcrs2 ; 1801 translate_op1 AST.Op_notbool destrs destrs] 1802 start_lbl dest_lbl def 1803 1804  _ > assert false (* wrong number of arguments *) 1805 *) 1806 1807 definition translate_condcst ≝ 1808 λcst. 1809 λstart_lbl: label. 1810 λlbl_true: label. 1811 λlbl_false: label. 1812 λdef. 1813 match cst with 1814 [ cast_int i ⇒ 1815 let 〈def, tmpr〉 ≝ fresh_reg def in 1816 adds_graph [ 1817 rtl_st_int tmpr i start_lbl; 1818 rtl_st_cond_acc tmpr lbl_true lbl_false 1819 ] start_lbl start_lbl def 1820  cast_addr_symbol x ⇒ 1821 let 〈def, r1〉 ≝ fresh_reg def in 1822 let 〈def, r2〉 ≝ fresh_reg def in 1823 let lbl ≝ fresh_label def in 1824 match lbl with 1825 [ None ⇒ None ? 1826  Some lbl ⇒ 1827 let def ≝ add_graph start_lbl (rtl_st_addr r1 r2 x lbl) def in 1828 translate_condptr r1 r2 lbl lbl_true lbl_false def 1829 ] 1830  cast_stack_offset off ⇒ 1831 let 〈def, r1〉 ≝ fresh_reg def in 1832 let 〈def, r2〉 ≝ fresh_reg def in 1833 let tmp_lbl ≝ fresh_label def in 1834 match tmp_lbl with 1835 [ None ⇒ None ? 1836  Some tmp_lbl ⇒ 1837 let def ≝ translate_cst (cast_stack_offset off) [r1; r2] start_lbl tmp_lbl def in 1838 match def with 1839 [ None ⇒ None ? 1840  Some def ⇒ translate_condptr r1 r2 tmp_lbl lbl_true lbl_false def 1841 ] 1842 ] 1843  cast_float f ⇒ None ? (* error_float *) 1844 ]. 1845 1846 definition size_of_op1_ret ≝ 1847 λop. 1848 match op with 1849 [ op_cast8_unsigned ⇒ Some ? 1 1850  op_cast8_signed ⇒ Some ? 1 1851  op_cast16_unsigned ⇒ Some ? 1 1852  op_cast16_signed ⇒ Some ? 1 1853  op_neg_int ⇒ Some ? 1 1854  op_not_int ⇒ Some ? 1 1855  op_int_of_ptr ⇒ Some ? 1 1856  op_ptr_of_int ⇒ Some ? 2 1857  op_id ⇒ None ? (* invalid_argument *) 1858  _ ⇒ None ? (* error_float *) 1859 ]. 1860 1861 definition translate_cond1 ≝ 1862 λop1. 1863 λsrcrs: list register. 1864 λstart_lbl: label. 1865 λlbl_true: label. 1866 λlbl_false: label. 1867 λdef. 1868 match op1 with 1869 [ op_id ⇒ 1870 let srcr ≝ extract_singleton ? srcrs in 1871 match srcr with 1872 [ None ⇒ 1873 let srcr12 ≝ extract_pair ? srcrs in 1874 match srcr12 with 1875 [ None ⇒ None ? 1876  Some srcr12 ⇒ 1877 let 〈srcr1, srcr2〉 ≝ srcr12 in 1878 translate_condptr srcr1 srcr2 start_lbl lbl_true lbl_false def 1879 ] 1880  Some srcr ⇒ 1881 adds_graph [ 1882 rtl_st_cond_acc srcr lbl_true lbl_false 1883 ] start_lbl start_lbl def 1884 ] 1885  _ ⇒ 1886 let size ≝ size_of_op1_ret op1 in 1887 match size with 1888 [ None ⇒ None ? 1889  Some size ⇒ 1890 let 〈def, destrs〉 ≝ fresh_regs def size in 1891 let lbl ≝ fresh_label def in 1892 match lbl with 1893 [ None ⇒ None ? 1894  Some lbl ⇒ 1895 let def ≝ translate_op1 op1 destrs srcrs start_lbl lbl def in 1896 match def with 1897 [ None ⇒ None ? 1898  Some def ⇒ 1899 let destr ≝ extract_singleton ? destrs in 1900 match destr with 1901 [ None ⇒ 1902 let destr12 ≝ extract_pair ? destrs in 1903 match destr12 with 1904 [ None ⇒ None ? 1905  Some destr12 ⇒ 1906 let 〈destr1, destr2〉 ≝ destr12 in 1907 translate_condptr destr1 destr2 start_lbl lbl_true lbl_false def 1908 ] 1909  Some destr ⇒ 1910 adds_graph [ 1911 rtl_st_cond_acc destr lbl_true lbl_false 1912 ] start_lbl start_lbl def 1913 ] 1914 ] 1915 ] 1916 ] 1917 ]. 1918 1919 definition size_of_op2_ret ≝ 1920 λn: nat. 1921 λop2. 1922 match op2 with 1923 [ op_add ⇒ Some ? 1 1924  op_sub ⇒ Some ? 1 1925  op_mul ⇒ Some ? 1 1926  op_div ⇒ Some ? 1 1927  op_divu ⇒ Some ? 1 1928  op_mod ⇒ Some ? 1 1929  op_modu ⇒ Some ? 1 1930  op_and ⇒ Some ? 1 1931  op_or ⇒ Some ? 1 1932  op_xor ⇒ Some ? 1 1933  op_shl ⇒ Some ? 1 1934  op_shr ⇒ Some ? 1 1935  op_shru ⇒ Some ? 1 1936  op_cmp _ ⇒ Some ? 1 1937  op_cmpu _ ⇒ Some ? 1 1938  op_cmpp _ ⇒ Some ? 1 1939  op_addp ⇒ Some ? 2 1940  op_subp ⇒ 1941 if eq_nat n 4 then 1942 Some ? 1 1943 else 1944 Some ? 2 1945  _ ⇒ None ? (* error_float *) 1946 ]. 1947 1948 axiom translate_op2: 1949 op2 → list register → list register → list register → label → label → rtl_internal_function → option rtl_internal_function. 1950 1951 definition translate_cond2 ≝ 1952 λop2. 1953 λsrcrs1: list register. 1954 λsrcrs2: list register. 1955 λstart_lbl: label. 1956 λlbl_true: label. 1957 λlbl_false: label. 1958 λdef. 1959 match op2 with 1960 [ op_cmp cmp ⇒ 1961 match cmp with 1962 [ Compare_Equal ⇒ 1963 let srcr1 ≝ extract_singleton ? srcrs1 in 1964 match srcr1 with 1965 [ None ⇒ None ? 1966  Some srcr1 ⇒ 1967 let srcr2 ≝ extract_singleton ? srcrs2 in 1968 match srcr2 with 1969 [ None ⇒ None ? 1970  Some srcr2 ⇒ 1971 let 〈def, tmpr〉 ≝ fresh_reg def in 1972 adds_graph [ 1973 rtl_st_clear_carry start_lbl; 1974 rtl_st_op2 Sub tmpr srcr1 srcr2 start_lbl; 1975 rtl_st_cond_acc tmpr lbl_false lbl_true 1976 ] start_lbl start_lbl def 1977 ] 1978 ] 1979  _ ⇒ 1980 let n ≝ length ? srcrs1 + length ? srcrs2 in 1981 match size_of_op2_ret n op2 with 1982 [ None ⇒ None ? 1983  Some size ⇒ 1984 let 〈def, destrs〉 ≝ fresh_regs def size in 1985 let lbl ≝ fresh_label def in 1986 match lbl with 1987 [ None ⇒ None ? 1988  Some lbl ⇒ 1989 match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with 1990 [ None ⇒ None ? 1991  Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def 1992 ] 1993 ] 1994 ] 1995 ] 1996  _ ⇒ 1997 let n ≝ length ? srcrs1 + length ? srcrs2 in 1998 match size_of_op2_ret n op2 with 1999 [ None ⇒ None ? 2000  Some size ⇒ 2001 let 〈def, destrs〉 ≝ fresh_regs def size in 2002 let lbl ≝ fresh_label def in 2003 match lbl with 2004 [ None ⇒ None ? 2005  Some lbl ⇒ 2006 match translate_op2 op2 destrs srcrs1 srcrs2 start_lbl lbl def with 2007 [ None ⇒ None ? 2008  Some def ⇒ translate_cond1 op_id destrs lbl lbl_true lbl_false def 2009 ] 2010 ] 2011 ] 2012 ]. 2013 2014 let rec addressing_pointer (mode: ?) (args: ?) (destr1: ?) 2015 (destr2: ?) (start_lbl: label) 2016 (dest_lbl: label) (def: rtl_internal_function) ≝ 2017 let destrs ≝ [ destr1; destr2 ] in 2018 match mode with 2019 [ Aindexed off ⇒ 2020 let srcr12 ≝ extract_singleton ? args in 2021 match srcr12 with 2022 [ None ⇒ None ? 2023  Some srcr12 ⇒ 2024 let srcr12 ≝ extract_pair ? srcr12 in 2025 match srcr12 with 2026 [ None ⇒ None ? 2027  Some srcr12 ⇒ 2028 let 〈srcr1, srcr2〉 ≝ srcr12 in 2029 let 〈def, tmpr〉 ≝ fresh_reg def in 2030 add_translates [ 2031 adds_graph [ 2032 rtl_st_int tmpr off start_lbl 2033 ]; 2034 translate_op2 op_addp destrs [ srcr1 ; srcr2 ] [tmpr] 2035 ] start_lbl dest_lbl def 2036 ] 2037 ] 2038  Aindexed2 ⇒ 2039 let args_pair ≝ extract_pair ? args in 2040 match args_pair with 2041 [ None ⇒ None ? 2042  Some args_pair ⇒ 2043 let 〈lft, rgt〉 ≝ args_pair in 2044 let srcr1112 ≝ extract_pair ? lft in 2045 let srcr2 ≝ extract_singleton ? rgt in 2046 match srcr1112 with 2047 [ None ⇒ 2048 let srcr2 ≝ extract_singleton ? rgt in 2049 let srcr1112 ≝ extract_pair ? lft in 2050 match srcr2 with 2051 [ None ⇒ None ? 2052  Some srcr2 ⇒ 2053 match srcr1112 with 2054 [ None ⇒ None ? 2055  Some srcr1112 ⇒ 2056 let 〈srcr11, srcr12〉 ≝ srcr1112 in 2057 translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def 2058 ] 2059 ] 2060  Some srcr1112 ⇒ 2061 let 〈srcr11, srcr12〉 ≝ srcr1112 in 2062 match srcr2 with 2063 [ None ⇒ None ? 2064  Some srcr2 ⇒ 2065 translate_op2 op_addp destrs [ srcr11; srcr12 ] [ srcr2 ] start_lbl dest_lbl def 2066 ] 2067 ] 2068 ] 2069  Aglobal x off ⇒ 2070 let 〈def, tmpr〉 ≝ fresh_reg def in 2071 add_translates [ 2072 adds_graph [ 2073 rtl_st_int tmpr off start_lbl; 2074 rtl_st_addr destr1 destr2 x start_lbl 2075 ]; 2076 translate_op2 op_addp destrs destrs [ tmpr ] 2077 ] start_lbl dest_lbl def 2078  Abased x off ⇒ 2079 let srcrs ≝ extract_singleton ? args in 2080 match srcrs with 2081 [ None ⇒ None ? 2082  Some srcrs ⇒ 2083 let 〈def, tmpr1〉 ≝ fresh_reg def in 2084 let 〈def, tmpr2〉 ≝ fresh_reg def in 2085 (* mode, args, destr1, destr2, start_lbl, dest_lbl, def *) 2086 (* addressing_pointer (Aglobal x off) [ ] tmpr1 tmpr2; *) 2087 let address_unfold ≝ 2088 let 〈def, tmpr〉 ≝ fresh_reg def in 2089 add_translates [ 2090 adds_graph [ 2091 rtl_st_int tmpr off start_lbl; 2092 rtl_st_addr tmpr1 tmpr2 x start_lbl 2093 ]; 2094 translate_op2 op_addp destrs destrs [ tmpr ] 2095 ] 2096 in 2097 add_translates [ 2098 address_unfold; 2099 translate_op2 op_addp destrs [ tmpr1; tmpr2 ] srcrs 2100 ] start_lbl dest_lbl def 2101 ] 2102  Ainstack off ⇒ 2103 let 〈def, tmpr〉 ≝ fresh_reg def in 2104 add_translates [ 2105 adds_graph [ 2106 rtl_st_int tmpr off start_lbl; 2107 rtl_st_stack_addr destr1 destr2 start_lbl 2108 ]; 2109 translate_op2 op_addp destrs destrs [ tmpr ] 2110 ] start_lbl dest_lbl def 2111  _ ⇒ None ? (* wrong number of arguments *) 2112 ]. 2113 2114 definition translate_load ≝ 2115 λq. 2116 λmode. 2117 λargs. 2118 λdestrs. 2119 λstart_lbl: label. 2120 λdest_lbl: label. 2121 λdef. 2122 match q with 2123 [ q_int b ⇒ 2124 if eq_bv ? b (bitvector_of_nat ? 1) then 2125 match extract_singleton ? destrs with 2126 [ None ⇒ None ? (* error: size error in load *) 2127  Some destr ⇒ 2128 let 〈def, addr1〉 ≝ fresh_reg def in 2129 let 〈def, addr2〉 ≝ fresh_reg def in 2130 Some ? (add_translates [ 2131 addressing_pointer mode args addr1 addr2; 2132 adds_graph [ 2133 rtl_st_load destr addr1 addr2 start_lbl 2134 ] 2135 ] start_lbl dest_lbl def) 2136 ] 2137 else 2138 None ? (* error: size error in load *) 2139  q_ptr ⇒ 2140 match extract_pair ? destrs with 2141 [ None ⇒ None ? (* error: size error in load *) 2142  Some destr12 ⇒ 2143 let 〈destr1, destr2〉 ≝ destr12 in 2144 let 〈def, addr1〉 ≝ fresh_reg def in 2145 let 〈def, addr2〉 ≝ fresh_reg def in 2146 let addr ≝ [ addr1; addr2 ] in 2147 let 〈def, tmpr〉 ≝ fresh_reg def in 2148 Some ? ( 2149 add_translates [ 2150 addressing_pointer mode args addr1 addr2; 2151 adds_graph [ 2152 rtl_st_load destr1 addr1 addr2 start_lbl; 2153 rtl_st_int tmpr (bitvector_of_nat ? 1) start_lbl 2154 ]; 2155 translate_op2 op_addp addr addr [ tmpr ]; 2156 adds_graph [ 2157 rtl_st_load destr2 addr1 addr2 start_lbl 2158 ] 2159 ] start_lbl dest_lbl def 2160 ) 2161 ] 2162  _ ⇒ None ? (* error: size error in load *) 2163 ]. 2164 2165 definition make_addr ≝ 2166 λA: Type[0]. 2167 λlst: list A. 2168 match lst with 2169 [ cons hd tl ⇒ 2170 match tl with 2171 [ cons hd' tl' ⇒ Some ? 〈hd, hd'〉 2172  _ ⇒ None ? (* do not use on these arguments *) 2173 ] 2174  _ ⇒ None ? (* do not use on these arguments *) 2175 ]. 2176 2177 definition translate_store_internal ≝ 2178 λaddr. 2179 λtmp_addr. 2180 λtmpr. 2181 λstart_lbl. 2182 λdest_lbl. 2183 λtmp_addr1. 2184 λtmp_addr2. 2185 λtranslates_off. 2186 λsrcr. 2187 let 〈translates, off〉 ≝ translates_off in 2188 let translates ≝ translates @ 2189 [ adds_graph [ 2190 rtl_st_int tmpr off start_lbl 2191 ]; 2192 translate_op2 op_addp tmp_addr addr [ tmpr ]; 2193 adds_graph [ 2194 rtl_st_store tmp_addr1 tmp_addr2 srcr dest_lbl 2195 ] 2196 ] 2197 in 2198 let 〈ignore, result〉 ≝ half_add ? off int_size in 2199 〈translates, result〉. 2200 2201 definition translate_store ≝ 2202 λaddr. 2203 λsrcrs. 2204 λstart_lbl. 2205 λdest_lbl. 2206 λdef. 2207 let 〈def, tmp_addr〉 ≝ fresh_regs def (length ? addr) in 2208 match make_addr ? tmp_addr with 2209 [ None ⇒ None ? 2210  Some tmp_addr12 ⇒ 2211 let 〈tmp_addr1, tmp_addr2〉 ≝ tmp_addr12 in 2212 let 〈def, tmpr〉 ≝ fresh_reg def in 2213 let f ≝ translate_store_internal addr tmp_addr tmpr start_lbl dest_lbl tmp_addr1 tmp_addr2 in 2214 let 〈translates, ignore〉 ≝ foldl ? ? f 〈[], zero ?〉 srcrs in 2215 add_translates translates start_lbl dest_lbl def 2216 ]. 2217 2218 definition translate_stmt ≝ 2219 λlenv. 2220 λlbl. 2221 λstmt. 2222 λdef. 2223 match stmt with 2224 [ St_skip lbl' ⇒ add_graph lbl (rtl_st_skip lbl') def 2225  St_cost cost_lbl lbl' ⇒ add_graph lbl (rtl_st_cost cost_lbl lbl') def 2226  St_cast destr cst lbl' ⇒ 2227 translate_cst cst (find_local_env destr lenv) lbl lbl' def 2228  _ ⇒ ? 2229 ]. 2230 2231 let translate_stmt lenv lbl stmt def = match stmt with 2232 2233  RTLabs.St_skip lbl' > 2234 add_graph lbl (RTL.St_skip lbl') def 2235 2236  RTLabs.St_cost (cost_lbl, lbl') > 2237 add_graph lbl (RTL.St_cost (cost_lbl, lbl')) def 2238 2239  RTLabs.St_cst (destr, cst, lbl') > 2240 translate_cst cst (find_local_env destr lenv) lbl lbl' def 2241 2242  RTLabs.St_op1 (op1, destr, srcr, lbl') > 2243 translate_op1 op1 (find_local_env destr lenv) (find_local_env srcr lenv) 2244 lbl lbl' def 2245 2246  RTLabs.St_op2 (op2, destr, srcr1, srcr2, lbl') > 2247 translate_op2 op2 (find_local_env destr lenv) 2248 (find_local_env srcr1 lenv) (find_local_env srcr2 lenv) lbl lbl' def 2249 2250  RTLabs.St_load (_, addr, destr, lbl') > 2251 translate_load (find_local_env addr lenv) (find_local_env destr lenv) 2252 lbl lbl' def 2253 2254  RTLabs.St_store (_, addr, srcr, lbl') > 2255 translate_store (find_local_env addr lenv) (find_local_env srcr lenv) 2256 lbl lbl' def 2257 2258  RTLabs.St_call_id (f, args, None, _, lbl') > 2259 add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, [], lbl')) def 2260 2261  RTLabs.St_call_id (f, args, Some retr, _, lbl') > 2262 add_graph lbl (RTL.St_call_id (f, rtl_args args lenv, 2263 find_local_env retr lenv, lbl')) def 2264 2265  RTLabs.St_call_ptr (f, args, None, _, lbl') > 2266 let (f1, f2) = find_and_addr f lenv in 2267 add_graph lbl (RTL.St_call_ptr (f1, f2, rtl_args args lenv, [], lbl')) def 2268 2269  RTLabs.St_call_ptr (f, args, Some retr, _, lbl') > 2270 let (f1, f2) = find_and_addr f lenv in 2271 add_graph lbl 2272 (RTL.St_call_ptr 2273 (f1, f2, rtl_args args lenv, find_local_env retr lenv, lbl')) def 2274 2275  RTLabs.St_tailcall_id (f, args, _) > 2276 add_graph lbl (RTL.St_tailcall_id (f, rtl_args args lenv)) def 2277 2278  RTLabs.St_tailcall_ptr (f, args, _) > 2279 let (f1, f2) = find_and_addr f lenv in 2280 add_graph lbl (RTL.St_tailcall_ptr (f1, f2, rtl_args args lenv)) def 2281 2282  RTLabs.St_cond (r, lbl_true, lbl_false) > 2283 translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def 2284 2285  RTLabs.St_jumptable _ > 2286 error "Jump tables not supported yet." 2287 2288  RTLabs.St_return None > 2289 add_graph lbl (RTL.St_return []) def 2290 2291  RTLabs.St_return (Some r) > 2292 add_graph lbl (RTL.St_return (find_local_env r lenv)) def 1206 (f_params def @ f_locals def) (f_result def) in 1207 let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in 1208 let locals ≝ map_list_local_env lenv (map ? ? \fst (f_locals def)) in 1209 let result ≝ 1210 match (f_result def) with 1211 [ None ⇒ [ ] 1212  Some r_typ ⇒ 1213 let 〈r, typ〉 ≝ r_typ in 1214 find_local_env r lenv 1215 ] 1216 in 1217 let luniverse' ≝ f_labgen def in 1218 let runiverse' ≝ runiverse in 1219 let result' ≝ result in 1220 let params' ≝ params in 1221 let locals' ≝ locals in 1222 let stack_size' ≝ f_stacksize def in 1223 let graph' ≝ empty_map ? ? in 1224 let entry' ≝ f_entry def in 1225 let exit' ≝ f_exit def in 1226 let res ≝ 1227 mk_rtl_internal_function luniverse' runiverse' result' params' 1228 locals' stack_size' graph' entry' exit' in 1229 fold ? ? ? (translate_stmt lenv) (f_graph def) res. 1230 1231 definition translate_fun_def ≝ 1232 λfdef: fundef internal_function. 1233 match fdef with 1234 [ Internal f ⇒ Internal ? (translate_internal f) 1235  External e ⇒ External ? e 1236 ]. 1237 1238 definition init_data_to_nat ≝ 1239 λi: init_data. 1240 match i with 1241 [ Init_int8 i8 ⇒ 8 1242  Init_int16 i16 ⇒ 16 1243  Init_int32 i32 ⇒ 32 1244  Init_float32 f32 ⇒ 32 1245  Init_float64 f64 ⇒ 64 1246  Init_space s ⇒ s 1247  Init_null r ⇒ 0 1248  Init_addrof r i o ⇒ 8 (* XXX: not at all sure about this one *) 1249 ]. 1250 1251 definition translate ≝ 1252 λp: program (fundef internal_function) unit. 1253 let f_funct ≝ λid_fun_def. 1254 let 〈id, fun_def〉 ≝ id_fun_def in 1255 〈id, translate_fun_def fun_def〉 1256 in 1257 let vars' ≝ map ? ? (λx. 1258 let 〈id_init_ignore, ignore〉 ≝ x in 1259 let 〈id_init, ignore〉 ≝ id_init_ignore in 1260 let 〈id, init〉 ≝ id_init in 1261 let init_total ≝ foldr ? ? plus 0 (map ? ? init_data_to_nat init) in 1262 〈id, init_total〉) (prog_vars ? ? p) 1263 in 1264 let functs' ≝ map ? ? f_funct (prog_funct ? ? p) in 1265 let main' ≝ prog_main ? ? p in 1266 mk_rtl_program vars' functs' (Some ? main'). 
src/common/Identifiers.ma
r1058 r1068 108 108 ]. 109 109 110 axiom fold: 111 ∀A, B: Type[0]. 112 ∀tag: String. 113 (identifier tag > A > B > B) > identifier_map tag A > B > B. 114 110 115 (* Sets *) 111 116
Note: See TracChangeset
for help on using the changeset viewer.