Changeset 1068


Ignore:
Timestamp:
Jul 14, 2011, 2:27:41 PM (8 years ago)
Author:
mulligan
Message:

rtlabs translation complete subject to axioms

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1066 r1068  
    2626  | rtl_st_cond: register → label → label → rtl_statement
    2727  | rtl_st_set_carry: label → rtl_statement
    28   | rtl_st_return: registers → rtl_statement.
     28  | rtl_st_return: rtl_statement. (* XXX: change from o'caml *)
    2929 
    3030definition rtl_statement_graph ≝ graph rtl_statement.
     
    3434  rtl_if_luniverse: universe LabelTag;
    3535  rtl_if_runiverse: universe RegisterTag;
    36   rtl_if_sig: signature;
     36(*  rtl_if_sig: signature;  -- dropped in front end *)
    3737  rtl_if_result: registers;
    3838  rtl_if_params: registers;
     
    4444}.
    4545
    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.
     46definition rtl_function_definition ≝ fundef rtl_internal_function.
    4947 
    5048record rtl_program: Type[0] ≝
  • src/RTLabs/RTLAbstoRTL.ma

    r1067 r1068  
    1111  let rtl_if_luniverse' ≝ rtl_if_luniverse p in
    1212  let rtl_if_runiverse' ≝ rtl_if_runiverse p in
    13   let rtl_if_sig' ≝ rtl_if_sig p in
    1413  let rtl_if_result' ≝ rtl_if_result p in
    1514  let rtl_if_params' ≝ rtl_if_params p in
     
    1918  let rtl_if_entry' ≝ rtl_if_entry p in
    2019  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'
    2221                             rtl_if_params' rtl_if_params' rtl_if_locals'
    2322                             rtl_if_stacksize' rtl_if_graph' rtl_if_entry'
     
    3029    let rtl_if_luniverse' ≝ new_univ in
    3130    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    32     let rtl_if_sig' ≝ rtl_if_sig def in
    3331    let rtl_if_result' ≝ rtl_if_result def in
    3432    let rtl_if_params' ≝ rtl_if_params def in
     
    3937    let rtl_if_exit' ≝ rtl_if_exit def in
    4038      〈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'
    4240        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
    4341        rtl_if_entry' rtl_if_exit', lbl〉.
     
    5149    let rtl_if_luniverse' ≝ rtl_if_luniverse def in
    5250    let rtl_if_runiverse' ≝ rtl_if_runiverse def in
    53     let rtl_if_sig' ≝ rtl_if_sig def in
    5451    let rtl_if_result' ≝ rtl_if_result def in
    5552    let rtl_if_params' ≝ rtl_if_params def in
     
    6057    let rtl_if_exit' ≝ rtl_if_exit def in
    6158      〈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'
    6360        rtl_if_params' rtl_if_locals' rtl_if_stacksize' rtl_if_graph'
    6461        rtl_if_entry' rtl_if_exit', r〉.
     
    258255  | rtl_st_clear_carry l ⇒ rtl_st_clear_carry lbl
    259256  | rtl_st_set_carry l ⇒ rtl_st_set_carry lbl
    260   | rtl_st_return r ⇒ rtl_st_return r
     257  | rtl_st_return ⇒ rtl_st_return
    261258  ].
    262259
     
    11571154definition translate_stmt ≝
    11581155  λlenv.
    1159   λret: register. (* change from o'caml code, this is taken from func. record *)
    11601156  λlbl: label.
    11611157  λstmt.
     
    11971193    translate_cond (find_local_env r lenv) lbl lbl_true lbl_false def
    11981194  | St_jumptable r l ⇒ ? (* assert false: not implemented yet *)
    1199   | St_return ⇒ add_graph lbl (rtl_st_return (find_local_env ret lenv)) def
     1195  | St_return ⇒ add_graph lbl rtl_st_return def
    12001196  ].
    12011197  [10: cases not_implemented (* jtable case *)
     
    12081204  let runiverse ≝ f_reggen def in
    12091205  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
     1231definition 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
     1238definition 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
     1251definition 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  
    108108  ].
    109109
     110axiom fold:
     111  ∀A, B: Type[0].
     112  ∀tag: String.
     113  (identifier tag -> A -> B -> B) -> identifier_map tag A -> B -> B.
     114
    110115(* Sets *)
    111116
Note: See TracChangeset for help on using the changeset viewer.