@@ -20,6 +20,7 @@ open Utils
20
20
open Prog
21
21
open Glob_options
22
22
open Utils
23
+ open Wsize
23
24
24
25
let unsharp = String. map (fun c -> if c = '#' then '_' else c)
25
26
@@ -849,7 +850,7 @@ module X86BaseOpU : BaseOp
849
850
let v = int_of_velem v in
850
851
let s = int_of_ws ws in
851
852
let l_tmp = I. mk_tmp_lval ~vector: (1 ,s) (CoreIdent. tu ws) in
852
- let l_tmp2 = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
853
+ let l_tmp2 = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
853
854
let l_tmp2v = I. get_lval l_tmp2 in
854
855
let ty = CL. (Vector (v, Uint (s/ v))) in
855
856
CL.Instr. Avar l_tmp2v,
@@ -1222,7 +1223,7 @@ module X86BaseOpU : BaseOp
1222
1223
let a2,i2 = cast_vector_atome ws ve (List. nth es 1 ) in
1223
1224
let v = int_of_velem ve in
1224
1225
let s = int_of_ws ws in
1225
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1226
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1226
1227
let l = I. glval_to_lval (List. nth xs 0 ) in
1227
1228
let i3 = cast_atome_vector ws v ! l_tmp l in
1228
1229
match trans with
@@ -1243,7 +1244,7 @@ module X86BaseOpU : BaseOp
1243
1244
let a2,i2 = cast_vector_atome ws VE16 (List. nth es 1 ) in
1244
1245
let s = int_of_ws ws in
1245
1246
let v = s / 16 in
1246
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1247
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1247
1248
let l = I. glval_to_lval (List. nth xs 0 ) in
1248
1249
let i3 = cast_atome_vector ws v ! l_tmp l in
1249
1250
i1 @ i2 @ [CL.Instr.Op2. and_ l_tmp a1 a2] @ i3
@@ -1256,7 +1257,7 @@ module X86BaseOpU : BaseOp
1256
1257
let a2,i2 = cast_vector_atome ws ve (List. nth es 1 ) in
1257
1258
let v = int_of_velem ve in
1258
1259
let s = int_of_ws ws in
1259
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1260
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1260
1261
let l = I. glval_to_lval (List. nth xs 0 ) in
1261
1262
let i3 = cast_atome_vector ws v ! l_tmp l in
1262
1263
match trans with
@@ -1272,8 +1273,8 @@ module X86BaseOpU : BaseOp
1272
1273
let a2,i2 = cast_vector_atome ws v (List. nth es 1 ) in
1273
1274
let v = int_of_velem v in
1274
1275
let s = int_of_ws ws in
1275
- let l0_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1276
- let l1_tmp = I. mk_tmp_lval ~sign: true ~vector: (v,s / v) (CoreIdent. tu ws) in
1276
+ let l0_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1277
+ let l1_tmp = I. mk_tmp_lval ~sign: true ~vector: (s / v, v) (CoreIdent. tu ws) in
1277
1278
let (_, l1_ty) = I. get_lval l1_tmp in
1278
1279
let l = I. glval_to_lval (List. nth xs 0 ) in
1279
1280
let i3 = cast_atome_vector ws v ! l1_tmp l in
@@ -1288,10 +1289,10 @@ module X86BaseOpU : BaseOp
1288
1289
let a2,i2 = cast_vector_atome ws VE16 (List. nth es 1 ) in
1289
1290
let s = int_of_ws ws in
1290
1291
let v = s / 16 in
1291
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1292
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1292
1293
let l = I. glval_to_lval (List. nth xs 0 ) in
1293
1294
let i3 = cast_atome_vector ws v ! l_tmp l in
1294
- let l_tmp1 = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1295
+ let l_tmp1 = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1295
1296
i1 @ i2 @ [CL.Instr.Op2_2. mull l_tmp l_tmp1 a1 a2] @ i3
1296
1297
1297
1298
| VPSRA (ve , ws ) ->
@@ -1304,34 +1305,37 @@ module X86BaseOpU : BaseOp
1304
1305
let s = int_of_ws ws in
1305
1306
match trans with
1306
1307
| `Default ->
1307
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1308
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1308
1309
let l = I. glval_to_lval (List. nth xs 0 ) in
1309
1310
let i3 = cast_atome_vector ws v ! l_tmp l in
1310
- let l_tmp1 = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1311
+ let l_tmp1 = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1311
1312
i1 @ [CL.Instr.Shifts. split l_tmp l_tmp1 a1 c] @ i3
1312
1313
| `Smt ->
1313
- let l1_tmp = I. mk_tmp_lval ~sign: true ~vector: (v,s / v) (CoreIdent. tu ws) in
1314
+ let l1_tmp = I. mk_tmp_lval ~sign: true ~vector: (s / v, v) (CoreIdent. tu ws) in
1314
1315
let (_, l1_ty) = I. get_lval l1_tmp in
1315
- let l2_tmp = I. mk_tmp_lval ~sign: true ~vector: (v,s / v) (CoreIdent. tu ws) in
1316
+ let l2_tmp = I. mk_tmp_lval ~sign: true ~vector: (s / v, v) (CoreIdent. tu ws) in
1316
1317
let (_, l2_ty) = I. get_lval l2_tmp in
1317
- let l3_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1318
- let l4_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1318
+ let l3_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1319
+ let l4_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1319
1320
let l = I. glval_to_lval (List. nth xs 0 ) in
1320
1321
let i2 = cast_atome_vector ws v ! l4_tmp l in
1321
1322
i1 @ [CL.Instr. cast l1_ty l1_tmp a1;
1322
1323
CL.Instr.Shifts. split l2_tmp l3_tmp ! l1_tmp c;
1323
1324
CL.Instr. cast l2_ty l4_tmp ! l2_tmp] @ i2
1324
1325
end
1325
1326
1326
- | VPBROADCAST (ve , ws ) -> (* FIXME *)
1327
+ | VPBROADCAST (ve , ws ) ->
1327
1328
begin
1328
- let a1,i1 = cast_vector_atome ws ve (List. nth es 0 ) in
1329
+ let a1,i1 = cast_atome (wsize_of_velem ve) (List. nth es 0 ) in
1329
1330
let v = int_of_velem ve in
1330
1331
let s = int_of_ws ws in
1331
- let l_tmp = I. mk_tmp_lval ~vector: (v,s/ v) (CoreIdent. tu ws) in
1332
+ let rec repeat acc n x =
1333
+ if n == 0 then acc else repeat (x :: acc) (n - 1 ) x in
1334
+ let ac = CL.Instr. Avatome (repeat [] (s/ v) a1) in
1335
+ let l_tmp = I. mk_tmp_lval ~vector: (s/ v,v) (CoreIdent. tu ws) in
1332
1336
let l = I. glval_to_lval (List. nth xs 0 ) in
1333
1337
let i2 = cast_atome_vector ws v ! l_tmp l in
1334
- i1 @ [CL.Instr.Op1. mov l_tmp a1 ] @ i2
1338
+ i1 @ [CL.Instr.Op1. mov l_tmp ac ] @ i2
1335
1339
end
1336
1340
1337
1341
| _ ->
@@ -1414,7 +1418,7 @@ module X86BaseOpS : BaseOp
1414
1418
let v = int_of_velem v in
1415
1419
let s = int_of_ws ws in
1416
1420
let l_tmp = I. mk_tmp_lval ~vector: (1 ,s) (CoreIdent. tu ws) in
1417
- let l_tmp2 = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1421
+ let l_tmp2 = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1418
1422
let l_tmp2v = I. get_lval l_tmp2 in
1419
1423
let ty = CL. (Vector (v, Sint (s/ v))) in
1420
1424
CL.Instr. Avar l_tmp2v,
@@ -1620,15 +1624,18 @@ module X86BaseOpS : BaseOp
1620
1624
let l = I. glval_to_lval (List. nth xs 0 ) in
1621
1625
i @ [CL.Instr.Op1. mov l a]
1622
1626
1623
- | VPBROADCAST (ve , ws ) -> (* FIXME *)
1627
+ | VPBROADCAST (ve , ws ) ->
1624
1628
begin
1625
- let a1,i1 = cast_vector_atome ws ve (List. nth es 0 ) in
1629
+ let a1,i1 = cast_atome (wsize_of_velem ve) (List. nth es 0 ) in
1626
1630
let v = int_of_velem ve in
1627
1631
let s = int_of_ws ws in
1628
- let l_tmp = I. mk_tmp_lval ~vector: (v,s/ v) (CoreIdent. tu ws) in
1632
+ let rec repeat acc n x =
1633
+ if n == 0 then acc else repeat (x :: acc) (n - 1 ) x in
1634
+ let ac = CL.Instr. Avatome (repeat [] (s/ v) a1) in
1635
+ let l_tmp = I. mk_tmp_lval ~vector: (s/ v,v) (CoreIdent. tu ws) in
1629
1636
let l = I. glval_to_lval (List. nth xs 0 ) in
1630
1637
let i2 = cast_atome_vector ws v ! l_tmp l in
1631
- i1 @ [CL.Instr.Op1. mov l_tmp a1 ] @ i2
1638
+ i1 @ [CL.Instr.Op1. mov l_tmp ac ] @ i2
1632
1639
end
1633
1640
1634
1641
| VPADD (ve ,ws ) ->
@@ -1639,7 +1646,7 @@ module X86BaseOpS : BaseOp
1639
1646
let a2,i2 = cast_vector_atome ws ve (List. nth es 1 ) in
1640
1647
let v = int_of_velem ve in
1641
1648
let s = int_of_ws ws in
1642
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1649
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1643
1650
let l = I. glval_to_lval (List. nth xs 0 ) in
1644
1651
let i3 = cast_atome_vector ws v ! l_tmp l in
1645
1652
match trans with
@@ -1658,7 +1665,7 @@ module X86BaseOpS : BaseOp
1658
1665
let a2,i2 = cast_vector_atome ws ve (List. nth es 1 ) in
1659
1666
let v = int_of_velem ve in
1660
1667
let s = int_of_ws ws in
1661
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1668
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1662
1669
let l = I. glval_to_lval (List. nth xs 0 ) in
1663
1670
let i3 = cast_atome_vector ws v ! l_tmp l in
1664
1671
match trans with
@@ -1674,7 +1681,7 @@ module X86BaseOpS : BaseOp
1674
1681
let a2,i2 = cast_vector_atome ws v (List. nth es 1 ) in
1675
1682
let v = int_of_velem v in
1676
1683
let s = int_of_ws ws in
1677
- let l0_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1684
+ let l0_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1678
1685
let l = I. glval_to_lval (List. nth xs 0 ) in
1679
1686
let i3 = cast_atome_vector ws v ! l0_tmp l in
1680
1687
i1 @ i2 @ [CL.Instr.Op2. smul l0_tmp a1 a2 ] @ i3
@@ -1684,8 +1691,8 @@ module X86BaseOpS : BaseOp
1684
1691
let a2,i2 = cast_vector_atome ws VE16 (List. nth es 1 ) in
1685
1692
let s = int_of_ws ws in
1686
1693
let v = s / 16 in
1687
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1688
- let l_tmp1 = I. mk_tmp_lval ~sign: false ~vector: (v,s / v) (CoreIdent. tu ws) in
1694
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1695
+ let l_tmp1 = I. mk_tmp_lval ~sign: false ~vector: (s / v, v) (CoreIdent. tu ws) in
1689
1696
let l = I. glval_to_lval (List. nth xs 0 ) in
1690
1697
let i3 = cast_atome_vector ws v ! l_tmp l in
1691
1698
i1 @ i2 @ [CL.Instr.Op2_2. mull l_tmp l_tmp1 a1 a2] @ i3
@@ -1701,12 +1708,12 @@ module X86BaseOpS : BaseOp
1701
1708
let ac = repeat [] 16 c in
1702
1709
let v = int_of_velem ve in
1703
1710
let s = int_of_ws ws in
1704
- let l_tmp = I. mk_tmp_lval ~vector: (v,s / v) (CoreIdent. tu ws) in
1711
+ let l_tmp = I. mk_tmp_lval ~vector: (s / v, v) (CoreIdent. tu ws) in
1705
1712
let l = I. glval_to_lval (List. nth xs 0 ) in
1706
1713
let i2 = cast_atome_vector ws v ! l_tmp l in
1707
1714
match trans with
1708
1715
| `Default ->
1709
- let l_tmp1 = I. mk_tmp_lval ~sign: false ~vector: (v,s / v) (CoreIdent. tu ws) in
1716
+ let l_tmp1 = I. mk_tmp_lval ~sign: false ~vector: (s / v, v) (CoreIdent. tu ws) in
1710
1717
i1 @ [CL.Instr.Shifts. vsars l_tmp l_tmp1 a1 ac] @ i2
1711
1718
| `Smt ->
1712
1719
i1 @ [CL.Instr.Shift. vsar l_tmp a1 ac] @ i2
0 commit comments