Skip to content

Commit 8ded4c5

Browse files
satiscugcatsatiscugcat
committed
Moving int_vec_interp
1 parent 34fad17 commit 8ded4c5

File tree

12 files changed

+89
-128
lines changed

12 files changed

+89
-128
lines changed

‎testable-simd-models/src/abstractions/bitvec.rs‎

Lines changed: 0 additions & 111 deletions
Original file line numberDiff line numberDiff line change
@@ -155,114 +155,3 @@ impl<const N: u64> BitVec<N> {
155155
}
156156
}
157157

158-
pub mod int_vec_interp {
159-
//! This module defines interpretation for bit vectors as vectors of machine integers of various size and signedness.
160-
use super::*;
161-
162-
/// An F* attribute that marks an item as being an interpretation lemma.
163-
#[allow(dead_code)]
164-
/// Derives interpretations functions, simplification lemmas and type
165-
/// synonyms.
166-
macro_rules! interpretations {
167-
($n:literal; $($name:ident [$ty:ty; $m:literal]),*) => {
168-
$(
169-
#[doc = concat!(stringify!($ty), " vectors of size ", stringify!($m))]
170-
#[allow(non_camel_case_types)]
171-
pub type $name = FunArray<$m, $ty>;
172-
pastey::paste! {
173-
const _: () = {
174-
impl BitVec<$n> {
175-
#[doc = concat!("Conversion from ", stringify!($ty), " vectors of size ", stringify!($m), "to bit vectors of size ", stringify!($n))]
176-
pub fn [< from_ $name >](iv: $name) -> BitVec<$n> {
177-
let vec: Vec<$ty> = iv.as_vec();
178-
Self::from_slice(&vec[..], <$ty>::bits() as u64)
179-
}
180-
#[doc = concat!("Conversion from bit vectors of size ", stringify!($n), " to ", stringify!($ty), " vectors of size ", stringify!($m))]
181-
pub fn [< to_ $name >](bv: BitVec<$n>) -> $name {
182-
let vec: Vec<$ty> = bv.to_vec();
183-
$name::from_fn(|i| vec[i as usize])
184-
}
185-
186-
187-
}
188-
189-
#[cfg(test)]
190-
impl From<BitVec<$n>> for $name {
191-
fn from(bv: BitVec<$n>) -> Self {
192-
BitVec::[< to_ $name >](bv)
193-
}
194-
}
195-
196-
impl From<$name> for BitVec<$n> {
197-
fn from(iv: $name) -> Self {
198-
BitVec::[< from_ $name >](iv)
199-
}
200-
}
201-
202-
impl $name {
203-
204-
pub fn splat(value: $ty) -> Self {
205-
FunArray::from_fn(|_| value)
206-
}
207-
}
208-
};
209-
}
210-
)*
211-
};
212-
}
213-
214-
interpretations!(256; i32x8 [i32; 8], i64x4 [i64; 4], i16x16 [i16; 16], i128x2 [i128; 2], i8x32 [i8; 32],
215-
u32x8 [u32; 8], u64x4 [u64; 4], u16x16 [u16; 16], u8x32 [u8; 32]);
216-
interpretations!(128; i32x4 [i32; 4], i64x2 [i64; 2], i16x8 [i16; 8], i128x1 [i128; 1], i8x16 [i8; 16],
217-
u32x4 [u32; 4], u64x2 [u64; 2], u16x8 [u16; 8], u8x16 [u8; 16]);
218-
219-
interpretations!(512; u32x16 [u32; 16], u16x32 [u16; 32], i32x16 [i32; 16], i16x32 [i16; 32]);
220-
interpretations!(64; i64x1 [i64; 1], i32x2 [i32; 2], i16x4 [i16; 4], i8x8 [i8; 8], u64x1 [u64; 1], u32x2 [u32; 2],u16x4 [u16; 4], u8x8 [u8; 8]);
221-
interpretations!(32; i8x4 [i8; 4], u8x4 [u8; 4]);
222-
223-
impl i64x4 {
224-
pub fn into_i32x8(self) -> i32x8 {
225-
i32x8::from_fn(|i| {
226-
let value = *self.get(i / 2);
227-
(if i % 2 == 0 { value } else { value >> 32 }) as i32
228-
})
229-
}
230-
}
231-
232-
impl i32x8 {
233-
pub fn into_i64x4(self) -> i64x4 {
234-
i64x4::from_fn(|i| {
235-
let low = *self.get(2 * i) as u32 as u64;
236-
let high = *self.get(2 * i + 1) as i32 as i64;
237-
(high << 32) | low as i64
238-
})
239-
}
240-
}
241-
242-
impl From<i64x4> for i32x8 {
243-
fn from(vec: i64x4) -> Self {
244-
vec.into_i32x8()
245-
}
246-
}
247-
248-
#[cfg(test)]
249-
mod direct_convertions_tests {
250-
use super::*;
251-
use crate::helpers::test::HasRandom;
252-
253-
#[test]
254-
fn into_i32x8() {
255-
for _ in 0..10000 {
256-
let x: i64x4 = i64x4::random();
257-
let y = x.into_i32x8();
258-
assert_eq!(BitVec::from_i64x4(x), BitVec::from_i32x8(y));
259-
}
260-
}
261-
#[test]
262-
fn into_i64x4() {
263-
let x: i32x8 = i32x8::random();
264-
let y = x.into_i64x4();
265-
assert_eq!(BitVec::from_i32x8(x), BitVec::from_i64x4(y));
266-
}
267-
}
268-
}

‎testable-simd-models/src/abstractions/simd.rs‎

Lines changed: 66 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,74 @@
1-
//! A model of SIMD compiler intrinsics.
1+
//! Models of SIMD compiler intrinsics.
22
//!
33
//! Operations are defined on FunArrs.
44
5+
6+
57
use crate::abstractions::{bit::MachineInteger, funarr::FunArray};
68

9+
pub mod int_vec_interp {
10+
use crate::abstractions::bitvec::*;
11+
12+
#[allow(dead_code)]
13+
/// Derives interpretations functions, and type synonyms.
14+
macro_rules! interpretations {
15+
($n:literal; $($name:ident [$ty:ty; $m:literal]),*) => {
16+
$(
17+
#[doc = concat!(stringify!($ty), " vectors of size ", stringify!($m))]
18+
#[allow(non_camel_case_types)]
19+
pub type $name = FunArray<$m, $ty>;
20+
pastey::paste! {
21+
const _: () = {
22+
impl BitVec<$n> {
23+
#[doc = concat!("Conversion from ", stringify!($ty), " vectors of size ", stringify!($m), "to bit vectors of size ", stringify!($n))]
24+
pub fn [< from_ $name >](iv: $name) -> BitVec<$n> {
25+
let vec: Vec<$ty> = iv.as_vec();
26+
Self::from_slice(&vec[..], <$ty>::bits() as u64)
27+
}
28+
#[doc = concat!("Conversion from bit vectors of size ", stringify!($n), " to ", stringify!($ty), " vectors of size ", stringify!($m))]
29+
pub fn [< to_ $name >](bv: BitVec<$n>) -> $name {
30+
let vec: Vec<$ty> = bv.to_vec();
31+
$name::from_fn(|i| vec[i as usize])
32+
}
33+
34+
35+
}
36+
37+
38+
impl From<BitVec<$n>> for $name {
39+
fn from(bv: BitVec<$n>) -> Self {
40+
BitVec::[< to_ $name >](bv)
41+
}
42+
}
43+
44+
impl From<$name> for BitVec<$n> {
45+
fn from(iv: $name) -> Self {
46+
BitVec::[< from_ $name >](iv)
47+
}
48+
}
49+
50+
impl $name {
51+
52+
pub fn splat(value: $ty) -> Self {
53+
FunArray::from_fn(|_| value)
54+
}
55+
}
56+
};
57+
}
58+
)*
59+
};
60+
}
61+
62+
interpretations!(256; i32x8 [i32; 8], i64x4 [i64; 4], i16x16 [i16; 16], i128x2 [i128; 2], i8x32 [i8; 32],
63+
u32x8 [u32; 8], u64x4 [u64; 4], u16x16 [u16; 16], u8x32 [u8; 32]);
64+
interpretations!(128; i32x4 [i32; 4], i64x2 [i64; 2], i16x8 [i16; 8], i128x1 [i128; 1], i8x16 [i8; 16],
65+
u32x4 [u32; 4], u64x2 [u64; 2], u16x8 [u16; 8], u8x16 [u8; 16]);
66+
67+
interpretations!(512; u32x16 [u32; 16], u16x32 [u16; 32], i32x16 [i32; 16], i16x32 [i16; 32]);
68+
interpretations!(64; i64x1 [i64; 1], i32x2 [i32; 2], i16x4 [i16; 4], i8x8 [i8; 8], u64x1 [u64; 1], u32x2 [u32; 2],u16x4 [u16; 4], u8x8 [u8; 8]);
69+
interpretations!(32; i8x4 [i8; 4], u8x4 [u8; 4]);
70+
71+
}
772
use std::convert::*;
873
use std::ops::*;
974

‎testable-simd-models/src/core_arch/arm_shared/models/mod.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@
2222
#![allow(unused)]
2323
#[allow(non_camel_case_types)]
2424
mod types {
25-
use crate::abstractions::bitvec::int_vec_interp::*;
25+
use crate::abstractions::simd::int_vec_interp::*;
2626
pub type int32x4_t = i32x4;
2727
pub type int64x1_t = i64x1;
2828
pub type int64x2_t = i64x2;

‎testable-simd-models/src/core_arch/arm_shared/specs/mod.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@
1919
#[allow(unused)]
2020
#[allow(non_camel_case_types)]
2121
mod types {
22-
use crate::abstractions::bitvec::int_vec_interp::*;
22+
use crate::abstractions::simd::int_vec_interp::*;
2323
pub type int32x4_t = i32x4;
2424
pub type int64x1_t = i64x1;
2525
pub type int64x2_t = i64x2;

‎testable-simd-models/src/core_arch/arm_shared/tests/mod.rs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ pub mod neon;
3434

3535
#[allow(non_camel_case_types)]
3636
mod types {
37-
use crate::abstractions::bitvec::int_vec_interp::*;
37+
use crate::abstractions::simd::int_vec_interp::*;
3838
pub type int32x4_t = i32x4;
3939
pub type int64x1_t = i64x1;
4040
pub type int64x2_t = i64x2;
@@ -65,7 +65,8 @@ pub mod conversions {
6565
use super::upstream::*;
6666

6767
use super::types;
68-
use crate::abstractions::bitvec::{int_vec_interp::*, BitVec};
68+
use crate::abstractions::bitvec::BitVec;
69+
use crate::simd::int_vec_interp::*;
6970
use crate::abstractions::funarr::FunArray;
7071
macro_rules! convert{
7172
($($ty1:ident [$ty2:ty ; $n:literal]),*) => {

‎testable-simd-models/src/core_arch/x86/models/avx.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,12 +16,12 @@
1616
use super::types::*;
1717
use crate::abstractions::{
1818
bit::Bit,
19-
bitvec::{int_vec_interp::*, BitVec},
19+
bitvec::BitVec,
2020
simd::*,
2121
};
2222

2323
mod c_extern {
24-
use crate::abstractions::bitvec::int_vec_interp::*;
24+
use crate::abstractions::simd::int_vec_interp::*;
2525

2626
pub fn vperm2f128si256(a: i32x8, b: i32x8, imm8: i8) -> i32x8 {
2727
let temp = i128x2::from_fn(|i| match (imm8 as u8) >> (i * 4) {

‎testable-simd-models/src/core_arch/x86/models/avx2.rs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,13 @@
2020
//! [wiki_avx]: https://en.wikipedia.org/wiki/Advanced_Vector_Extensions
2121
//! [wiki_fma]: https://en.wikipedia.org/wiki/Fused_multiply-accumulate
2222
use crate::abstractions::{
23-
bitvec::{int_vec_interp::*, BitVec},
23+
bitvec::BitVec,
24+
simd::int_vec_interp::*,
2425
funarr::FunArray,
2526
};
2627

2728
mod c_extern {
28-
use crate::abstractions::{bit::MachineInteger, bitvec::int_vec_interp::*, simd::*};
29+
use crate::abstractions::{bit::MachineInteger, simd::*, simd::int_vec_interp::*};
2930
pub fn phaddw(a: i16x16, b: i16x16) -> i16x16 {
3031
i16x16::from_fn(|i| {
3132
if i < 4 {

‎testable-simd-models/src/core_arch/x86/models/sse2.rs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,12 @@
22
use super::types::*;
33
use crate::abstractions::{
44
bit::Bit,
5-
bitvec::{int_vec_interp::*, BitVec},
5+
bitvec::BitVec,
66
simd::*,
7+
simd::int_vec_interp::*;
78
};
89
mod c_extern {
9-
use crate::abstractions::{bit::MachineInteger, bitvec::int_vec_interp::*};
10+
use crate::abstractions::{bit::MachineInteger, simd::int_vec_interp::*};
1011
pub fn packsswb(a: i16x8, b: i16x8) -> i8x16 {
1112
i8x16::from_fn(|i| {
1213
if i < 8 {

‎testable-simd-models/src/core_arch/x86/models/ssse3.rs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,14 +1,14 @@
11
//! Supplemental Streaming SIMD Extensions 3 (SSSE3)
22
33
use crate::abstractions::{
4-
bitvec::{int_vec_interp::*, BitVec},
4+
bitvec::BitVec,
55
simd::*,
66
};
77

88
use super::types::*;
99

1010
mod c_extern {
11-
use crate::abstractions::bitvec::int_vec_interp::*;
11+
use crate::abstractions::simd::int_vec_interp::*;
1212
pub fn pshufb128(a: u8x16, b: u8x16) -> u8x16 {
1313
u8x16::from_fn(|i| if b[i] > 127 { 0 } else { a[(b[i] % 16) as u64] })
1414
}

‎testable-simd-models/src/core_arch/x86/specs/avx.rs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,8 @@ use super::types::*;
22

33
use crate::abstractions::{
44
bit::Bit,
5-
bitvec::{int_vec_interp::*, BitVec},
5+
bitvec::BitVec,
6+
simd::int_vec_interp::*
67
};
78

89
pub fn _mm256_set1_epi32(x: i32) -> __m256i {

0 commit comments

Comments
 (0)