Skip to content

Commit 1ae4ba8

Browse files
coord-ecoord-e
committed
Add more extern specs
1 parent 600c18a commit 1ae4ba8

File tree

1 file changed

+174
-0
lines changed

1 file changed

+174
-0
lines changed

‎std.rs‎

Lines changed: 174 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,16 +14,190 @@ fn _extern_spec_std_mem_swap<T>(x: &mut T, y: &mut T) {
1414
std::mem::swap(x, y);
1515
}
1616

17+
#[thrust::extern_spec_fn]
18+
#[thrust::requires(true)]
19+
#[thrust::ensures(^dest == src && result == *dest)]
20+
fn _extern_spec_std_mem_replace<T>(dest: &mut T, src: T) -> T {
21+
std::mem::replace(dest, src)
22+
}
23+
1724
#[thrust::extern_spec_fn]
1825
#[thrust::requires(opt != std::option::Option::<T0>::None())]
1926
#[thrust::ensures(std::option::Option::<T0>::Some(result) == opt)]
2027
fn _extern_spec_option_unwrap<T>(opt: Option<T>) -> T {
2128
Option::unwrap(opt)
2229
}
2330

31+
#[thrust::extern_spec_fn]
32+
#[thrust::requires(true)]
33+
#[thrust::ensures(
34+
(*opt == std::option::Option::<T0>::None() && result == true)
35+
|| (*opt != std::option::Option::<T0>::None() && result == false)
36+
)]
37+
fn _extern_spec_option_is_none<T>(opt: &Option<T>) -> bool {
38+
Option::is_none(opt)
39+
}
40+
41+
#[thrust::extern_spec_fn]
42+
#[thrust::requires(true)]
43+
#[thrust::ensures(
44+
(*opt == std::option::Option::<T0>::None() && result == false)
45+
|| (*opt != std::option::Option::<T0>::None() && result == true)
46+
)]
47+
fn _extern_spec_option_is_some<T>(opt: &Option<T>) -> bool {
48+
Option::is_some(opt)
49+
}
50+
51+
#[thrust::extern_spec_fn]
52+
#[thrust::requires(true)]
53+
#[thrust::ensures(
54+
(opt != std::option::Option::<T0>::None() && std::option::Option::<T0>::Some(result) == opt)
55+
|| (opt == std::option::Option::<T0>::None() && result == default)
56+
)]
57+
fn _extern_spec_option_unwrap_or<T>(opt: Option<T>, default: T) -> T {
58+
Option::unwrap_or(opt, default)
59+
}
60+
61+
#[thrust::extern_spec_fn]
62+
#[thrust::requires(true)]
63+
#[thrust::ensures(
64+
(exists x:T0. opt == std::option::Option::<T0>::Some(x) && result == std::result::Result::<T0, T1>::Ok(x))
65+
|| (opt == std::option::Option::<T0>::None() && result == std::result::Result::<T0, T1>::Err(err))
66+
)]
67+
fn _extern_spec_option_ok_or<T, E>(opt: Option<T>, err: E) -> Result<T, E> {
68+
Option::ok_or(opt, err)
69+
}
70+
71+
#[thrust::extern_spec_fn]
72+
#[thrust::requires(true)]
73+
#[thrust::ensures(^opt == std::option::Option::<T0>::None() && result == *opt)]
74+
fn _extern_spec_option_take<T>(opt: &mut Option<T>) -> Option<T> {
75+
Option::take(opt)
76+
}
77+
78+
#[thrust::extern_spec_fn]
79+
#[thrust::requires(true)]
80+
#[thrust::ensures(^opt == std::option::Option::<T0>::Some(src) && result == *opt)]
81+
fn _extern_spec_option_replace<T>(opt: &mut Option<T>, src: T) -> Option<T> {
82+
Option::replace(opt, src)
83+
}
84+
85+
#[thrust::extern_spec_fn]
86+
#[thrust::requires(true)]
87+
#[thrust::ensures(
88+
(exists x:T0. opt == <std::option::Option::<T0>::Some(x)> && result == std::option::Option::<&T0>::Some(<x>))
89+
|| (opt == <std::option::Option::<T0>::None()> && result == std::option::Option::<&T0>::None())
90+
)]
91+
fn _extern_spec_option_as_ref<T>(opt: &Option<T>) -> Option<&T> {
92+
Option::as_ref(opt)
93+
}
94+
95+
#[thrust::extern_spec_fn]
96+
#[thrust::requires(true)]
97+
#[thrust::ensures(
98+
(exists x1:T0, x2:T0.
99+
*opt == std::option::Option::<T0>::Some(x1) &&
100+
^opt == std::option::Option::<T0>::Some(x2) &&
101+
result == std::option::Option::<&mut T0>::Some(<x1, x2>)
102+
)
103+
|| (
104+
*opt == std::option::Option::<T0>::None() &&
105+
^opt == std::option::Option::<T0>::None() &&
106+
result == std::option::Option::<&mut T0>::None()
107+
)
108+
)]
109+
fn _extern_spec_option_as_mut<T>(opt: &mut Option<T>) -> Option<&mut T> {
110+
Option::as_mut(opt)
111+
}
112+
24113
#[thrust::extern_spec_fn]
25114
#[thrust::requires(exists x:T0. res == std::result::Result::<T0, T1>::Ok(x))]
26115
#[thrust::ensures(std::result::Result::<T0, T1>::Ok(result) == res)]
27116
fn _extern_spec_result_unwrap<T, E: std::fmt::Debug>(res: Result<T, E>) -> T {
28117
Result::unwrap(res)
29118
}
119+
120+
#[thrust::extern_spec_fn]
121+
#[thrust::requires(exists x:T1. res == std::result::Result::<T0, T1>::Err(x))]
122+
#[thrust::ensures(std::result::Result::<T0, T1>::Err(result) == res)]
123+
fn _extern_spec_result_unwrap_err<T: std::fmt::Debug, E>(res: Result<T, E>) -> E {
124+
Result::unwrap_err(res)
125+
}
126+
127+
#[thrust::extern_spec_fn]
128+
#[thrust::requires(true)]
129+
#[thrust::ensures(
130+
(exists x:T0. res == std::option::Result::<T0, T1>::Ok(x) && result == std::option::Option::<T0>::Some(x))
131+
|| (exists x:T1. res == std::option::Result::<T0, T1>::Err(x) && result == std::option::Option::<T0>::None())
132+
)]
133+
fn _extern_spec_result_ok<T, E>(res: Result<T, E>) -> Option<T> {
134+
Result::ok(res)
135+
}
136+
137+
#[thrust::extern_spec_fn]
138+
#[thrust::requires(true)]
139+
#[thrust::ensures(
140+
(exists x:T0. res == std::option::Result::<T0, T1>::Ok(x) && result == std::option::Option::<T0>::None())
141+
|| (exists x:T1. res == std::option::Result::<T0, T1>::Err(x) && result == std::option::Option::<T0>::Some(x))
142+
)]
143+
fn _extern_spec_result_err<T, E>(res: Result<T, E>) -> Option<E> {
144+
Result::err(res)
145+
}
146+
147+
#[thrust::extern_spec_fn]
148+
#[thrust::requires(true)]
149+
#[thrust::ensures(
150+
(exists x:T0. *res == std::option::Result::<T0, T1>::Ok(x) && result == true)
151+
|| (exists x:T1. *res == std::option::Result::<T0, T1>::Err(x) && result == false)
152+
)]
153+
fn _extern_spec_option_is_ok<T, E>(res: &Result<T, E>) -> bool {
154+
Result::is_ok(res)
155+
}
156+
157+
#[thrust::extern_spec_fn]
158+
#[thrust::requires(true)]
159+
#[thrust::ensures(
160+
(exists x:T0. *res == std::option::Result::<T0, T1>::Ok(x) && result == false)
161+
|| (exists x:T1. *res == std::option::Result::<T0, T1>::Err(x) && result == true)
162+
)]
163+
fn _extern_spec_option_is_err<T, E>(res: &Result<T, E>) -> bool {
164+
Result::is_err(res)
165+
}
166+
167+
#[thrust::extern_spec_fn]
168+
#[thrust::requires(true)] // TODO: require x != i32::MIN
169+
#[thrust::ensures(result >= 0 && (result == x || result == -x))]
170+
fn _extern_spec_i32_abs(x: i32) -> i32 {
171+
i32::abs(x)
172+
}
173+
174+
#[thrust::extern_spec_fn]
175+
#[thrust::requires(true)]
176+
#[thrust::ensures(
177+
(x >= y && result == (x - y))
178+
|| (x < y && result == (y - x))
179+
)]
180+
fn _extern_spec_i32_abs_diff(x: i32, y: i32) -> u32 {
181+
i32::abs_diff(x, y)
182+
}
183+
184+
#[thrust::extern_spec_fn]
185+
#[thrust::requires(true)]
186+
#[thrust::ensures((x == 0 && result == 0) || (x > 0 && result == 1) || (x < 0 && result == -1))]
187+
fn _extern_spec_i32_signum(x: i32) -> i32 {
188+
i32::signum(x)
189+
}
190+
191+
#[thrust::extern_spec_fn]
192+
#[thrust::requires(true)]
193+
#[thrust::ensures((x < 0 && result == false) || (x >= 0 && result == true))]
194+
fn _extern_spec_i32_is_positive(x: i32) -> bool {
195+
i32::is_positive(x)
196+
}
197+
198+
#[thrust::extern_spec_fn]
199+
#[thrust::requires(true)]
200+
#[thrust::ensures((x <= 0 && result == true) || (x > 0 && result == false))]
201+
fn _extern_spec_i32_is_negative(x: i32) -> bool {
202+
i32::is_negative(x)
203+
}

0 commit comments

Comments
 (0)