"use of impure function "std::ops::Div::div" in pure code is not allowed" and crash after setting Div for f64 as "extern_spec" #1537
Description
I am getting:
error: [Prusti: invalid specification] use of impure function "std::ops::Div::div" in pure code is not allowed
--> src/vec3.rs:43:9
|
43 | self / self.length()
| ^^^^^^^^^^^^^^^^^^^^
thread 'rustc' panicked at vir/src/../gen/polymorphic/ast/expr.rs:559:22:
internal error: entered unreachable code: f_vec3$$Vec3$$length<>(snap$<Snapshot(struct$m_vec3$$Vec3)>(_1))
stack backtrace:
0: 0x720cbc31f45c - std::backtrace_rs::backtrace::libunwind::trace::hd28b74870fb29f5e
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/../../backtrace/src/backtrace/libunwind.rs:93:5
1: 0x720cbc31f45c - std::backtrace_rs::backtrace::trace_unsynchronized::ha778ba6652f5fff7
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/../../backtrace/src/backtrace/mod.rs:66:5
2: 0x720cbc31f45c - std::sys_common::backtrace::_print_fmt::h57512da8fd27ebfe
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/sys_common/backtrace.rs:67:5
3: 0x720cbc31f45c - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h9ff91e3dfaf4de84
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/sys_common/backtrace.rs:44:22
4: 0x720cbc3855ac - core::fmt::rt::Argument::fmt::hb4c9152c9d66f707
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/core/src/fmt/rt.rs:138:9
5: 0x720cbc3855ac - core::fmt::write::hca827d819a7788c0
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/core/src/fmt/mod.rs:1094:21
6: 0x720cbc311fde - std::io::Write::write_fmt::hda6839af442363e2
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/io/mod.rs:1714:15
7: 0x720cbc31f244 - std::sys_common::backtrace::_print::h83dbca21f18ac9f0
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/sys_common/backtrace.rs:47:5
8: 0x720cbc31f244 - std::sys_common::backtrace::print::h50f6064ce0c0ed75
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/sys_common/backtrace.rs:34:9
9: 0x720cbc32233a - std::panicking::panic_hook_with_disk_dump::{{closure}}::habdb4fb696892949
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/panicking.rs:278:22
10: 0x720cbc322027 - std::panicking::panic_hook_with_disk_dump::h9e67e3f11439835d
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/panicking.rs:312:9
11: 0x720cbb149c19 - <rustc_driver_impl[2b0dd1b38bbe9303]::install_ice_hook::{closure#0} as core[b7a320a1e2fc1667]::ops::function::FnOnce<(&core[b7a320a1e2fc1667]::panic::panic_info::PanicInfo,)>>::call_once::{shim:vtable#0}
12: 0x720cbc322be0 - <alloc::boxed::Box<F,A> as core::ops::function::Fn<Args>>::call::h5d5db5c849147bae
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/alloc/src/boxed.rs:2021:9
13: 0x720cbc322be0 - std::panicking::rust_panic_with_hook::h03521a4f77cf14d2
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/panicking.rs:733:13
14: 0x720cbc322967 - std::panicking::begin_panic_handler::{{closure}}::ha8912bac885c0f14
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/panicking.rs:621:13
15: 0x720cbc31f986 - std::sys_common::backtrace::__rust_end_short_backtrace::h4ba480d82605b76d
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/sys_common/backtrace.rs:170:18
16: 0x720cbc3226b2 - rust_begin_unwind
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/panicking.rs:617:5
17: 0x720cbc3819b3 - core::panicking::panic_fmt::ha6b7709b07688c2f
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/core/src/panicking.rs:67:14
18: 0x5db0ed7503b1 - vir::gen::polymorphic::ast::expr::Expr::get_parent_ref::heb3759957e98dada
19: 0x5db0ed75043f - vir::gen::polymorphic::ast::expr::Expr::get_parent::h095738704b38ecb9
20: 0x5db0ed7512f7 - vir::gen::polymorphic::ast::expr::Expr::has_prefix::h0d7b15d0860fb3c4
21: 0x5db0ed751351 - vir::gen::polymorphic::ast::expr::Expr::has_prefix::h0d7b15d0860fb3c4
22: 0x5db0ed75122d - vir::gen::polymorphic::ast::expr::Expr::has_proper_prefix::he06a03b76b4389ff
23: 0x5db0eb9ab3c7 - prusti_viper::encoder::foldunfold::perm::Perm::has_proper_prefix::h5bc0c287b69ba5c0
24: 0x5db0eb9efb8c - prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain::{{closure}}::{{closure}}::h7025d2cb169645ee
25: 0x5db0ec18f8c2 - core::iter::traits::iterator::Iterator::find::check::{{closure}}::h6417051e45e5a62c
26: 0x5db0ebc9a5be - core::iter::traits::iterator::Iterator::try_fold::heebeaa7578f9de44
27: 0x5db0ebc96294 - core::iter::traits::iterator::Iterator::find::he5a55945ff3f9962
28: 0x5db0eb9ecad4 - prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain::{{closure}}::hbf00d58b33bfa623
29: 0x5db0eb9ead04 - prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain::hff8d81f27fe0ed96
30: 0x5db0eb9ea9e0 - prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain_all::{{closure}}::hca84f738eac5810e
31: 0x5db0ec1afd2f - core::iter::adapters::map::map_try_fold::{{closure}}::h8f93415196461138
32: 0x5db0eb717d5f - core::iter::traits::iterator::Iterator::try_fold::h2bf82a4b95d970b0
33: 0x5db0ec1724e0 - <core::iter::adapters::map::Map<I,F> as core::iter::traits::iterator::Iterator>::try_fold::he453378a1365c196
34: 0x5db0eb76eb09 - <core::iter::adapters::GenericShunt<I,R> as core::iter::traits::iterator::Iterator>::try_fold::ha2e598339941484d
35: 0x5db0eb766ad9 - <core::iter::adapters::GenericShunt<I,R> as core::iter::traits::iterator::Iterator>::next::h3b224c1da3cb3343
36: 0x5db0ec00b34c - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter_nested::SpecFromIterNested<T,I>>::from_iter::h1033ca3bca7f9055
37: 0x5db0ec0c6f8e - <alloc::vec::Vec<T> as alloc::vec::spec_from_iter::SpecFromIter<T,I>>::from_iter::hc4eda0f3b8846f7e
38: 0x5db0ec0c2bc9 - <alloc::vec::Vec<T> as core::iter::traits::collect::FromIterator<T>>::from_iter::hefa3f293ddaa2967
39: 0x5db0eb92dbd1 - <core::result::Result<V,E> as core::iter::traits::collect::FromIterator<core::result::Result<A,E>>>::from_iter::{{closure}}::h3ba757bafee407ac
40: 0x5db0eb7cfdc0 - core::iter::adapters::try_process::h8611c3a897b67c1e
41: 0x5db0eb92cce7 - <core::result::Result<V,E> as core::iter::traits::collect::FromIterator<core::result::Result<A,E>>>::from_iter::h821b368241317759
42: 0x5db0ec194cae - core::iter::traits::iterator::Iterator::collect::he8d29d6138263ba7
43: 0x5db0eb9ea868 - prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain_all::h7684b025e9a081a7
44: 0x5db0eb9f3586 - prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain_permissions::{{closure}}::h754dad7362237eb4
45: 0x5db0eb9f1a82 - prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt::obtain_permissions::h44909b19de54199d
46: 0x5db0eba2f6f3 - <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold::hda758e80d2949b6e
47: 0x5db0eb93de86 - vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_boxed::hc07d06d2bf7036fe
48: 0x5db0eb93e376 - vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_bin_op::h4082a36db0015802
49: 0x5db0ebc90fdc - vir::gen::polymorphic::ast::expr_transformers::default_fallible_fold_expr::haf6fd3f1d974e77b
50: 0x5db0eba2f9fa - <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold::hda758e80d2949b6e
51: 0x5db0eb93de86 - vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_boxed::hc07d06d2bf7036fe
52: 0x5db0eb93f56d - vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_unary_op::hb636fe3335f91991
53: 0x5db0ebc90fa9 - vir::gen::polymorphic::ast::expr_transformers::default_fallible_fold_expr::haf6fd3f1d974e77b
54: 0x5db0eba2f9fa - <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold::hda758e80d2949b6e
55: 0x5db0eb93de86 - vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_boxed::hc07d06d2bf7036fe
56: 0x5db0eb93e376 - vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder::fallible_fold_bin_op::h4082a36db0015802
57: 0x5db0ebc90fdc - vir::gen::polymorphic::ast::expr_transformers::default_fallible_fold_expr::haf6fd3f1d974e77b
58: 0x5db0eba2f9fa - <prusti_viper::encoder::foldunfold::ExprReplacer as vir::gen::polymorphic::ast::expr_transformers::FallibleExprFolder>::fallible_fold::hda758e80d2949b6e
59: 0x5db0eb9b6f45 - prusti_viper::encoder::foldunfold::FoldUnfold::replace_expr::h21734cf1f45dfbfb
60: 0x5db0eb9b73b6 - prusti_viper::encoder::foldunfold::FoldUnfold::rewrite_stmt_with_unfoldings::h3714ce041145e18d
61: 0x5db0eba24f18 - <prusti_viper::encoder::foldunfold::FoldUnfold as vir::gen::polymorphic::cfg::visitor::CfgReplacer<prusti_viper::encoder::foldunfold::path_ctxt::PathCtxt,prusti_viper::encoder::foldunfold::ActionVec>>::replace_stmt::hf8c5932bbedad00b
62: 0x5db0eb94530b - vir::gen::polymorphic::cfg::visitor::CfgReplacer::replace_cfg::hf272f26e877dccc8
63: 0x5db0eba1c283 - prusti_viper::encoder::foldunfold::add_fold_unfold::hac75a7b1cae1564d
64: 0x5db0ebabb06b - prusti_viper::encoder::procedure_encoder::ProcedureEncoder::encode::hf3a169cce1f2fd60
65: 0x5db0ebe5481c - prusti_viper::encoder::encoder::Encoder::encode_procedure::h10e5f1766b10b944
66: 0x5db0ebe5a77a - prusti_viper::encoder::encoder::Encoder::process_encoding_queue::h5828b9d33d1c8241
67: 0x5db0eb680f23 - prusti_viper::verifier::Verifier::verify::h972ce57ee15149ba
68: 0x5db0eb43c811 - prusti_driver::verifier::verify::h4d6050d6e4495106
69: 0x5db0eb45140d - <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis::{{closure}}::h529f5f5f1c24cd1a
70: 0x5db0eb460088 - rustc_middle::ty::context::GlobalCtxt::enter::{{closure}}::h3dc5573d893b3fed
71: 0x5db0eb43d83f - rustc_middle::ty::context::tls::enter_context::{{closure}}::hc073d7fb6aaa7e2a
72: 0x5db0eb45c3ee - std::thread::local::LocalKey<T>::try_with::h4391eead419db7c4
73: 0x5db0eb45ff32 - rustc_middle::ty::context::GlobalCtxt::enter::h1f86506599ff8af8
74: 0x5db0eb441422 - rustc_interface::queries::QueryResult<&rustc_middle::ty::context::GlobalCtxt>::enter::h8d03f6b053f2b45a
75: 0x5db0eb450ea0 - <prusti_driver::callbacks::PrustiCompilerCalls as rustc_driver_impl::Callbacks>::after_analysis::h38b8ac41da0735a2
76: 0x720cba44870c - <rustc_interface[34d3442556ad0076]::interface::Compiler>::enter::<rustc_driver_impl[2b0dd1b38bbe9303]::run_compiler::{closure#1}::{closure#2}, core[b7a320a1e2fc1667]::result::Result<core[b7a320a1e2fc1667]::option::Option<rustc_interface[34d3442556ad0076]::queries::Linker>, rustc_span[a2bfcccd8fd8f5bb]::ErrorGuaranteed>>
77: 0x720cba4419f8 - std[19b50d524ab2d114]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[34d3442556ad0076]::util::run_in_thread_pool_with_globals<rustc_interface[34d3442556ad0076]::interface::run_compiler<core[b7a320a1e2fc1667]::result::Result<(), rustc_span[a2bfcccd8fd8f5bb]::ErrorGuaranteed>, rustc_driver_impl[2b0dd1b38bbe9303]::run_compiler::{closure#1}>::{closure#0}, core[b7a320a1e2fc1667]::result::Result<(), rustc_span[a2bfcccd8fd8f5bb]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[b7a320a1e2fc1667]::result::Result<(), rustc_span[a2bfcccd8fd8f5bb]::ErrorGuaranteed>>
78: 0x720cba9bc9b5 - <<std[19b50d524ab2d114]::thread::Builder>::spawn_unchecked_<rustc_interface[34d3442556ad0076]::util::run_in_thread_pool_with_globals<rustc_interface[34d3442556ad0076]::interface::run_compiler<core[b7a320a1e2fc1667]::result::Result<(), rustc_span[a2bfcccd8fd8f5bb]::ErrorGuaranteed>, rustc_driver_impl[2b0dd1b38bbe9303]::run_compiler::{closure#1}>::{closure#0}, core[b7a320a1e2fc1667]::result::Result<(), rustc_span[a2bfcccd8fd8f5bb]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[b7a320a1e2fc1667]::result::Result<(), rustc_span[a2bfcccd8fd8f5bb]::ErrorGuaranteed>>::{closure#1} as core[b7a320a1e2fc1667]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
79: 0x720cbc32d3d5 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::h8108faf30968431e
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/alloc/src/boxed.rs:2007:9
80: 0x720cbc32d3d5 - <alloc::boxed::Box<F,A> as core::ops::function::FnOnce<Args>>::call_once::ha6d7c4e006483c0a
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/alloc/src/boxed.rs:2007:9
81: 0x720cbc32d3d5 - std::sys::unix::thread::Thread::new::thread_start::h06866bf1295ea7c8
at /rustc/180dffba142c47240ca0d93096ce90b9fd97c8d7/library/std/src/sys/unix/thread.rs:108:17
82: 0x720cb6694ac3 - start_thread
at ./nptl/pthread_create.c:442:8
83: 0x720cb6726850 - __GI___clone3
at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:81
84: 0x0 - <unknown>
error: the compiler unexpectedly panicked. this is a bug.
note: we would appreciate a bug report: https://github.com/viperproject/prusti-dev/issues/new
note: please attach the file at `/home/emmanuelm/Documentos/GitHub/ContractsTest/rustc-ice-2025-07-18T21:27:26.138225623Z-3409186.txt` to your bug report
note: compiler flags: --crate-type bin -C embed-bitcode=no -C debuginfo=2 -C incremental=[REDACTED]
note: some of the compiler flags provided by cargo are hidden
query stack during panic:
end of query stack
note: Prusti version: 0.2.2, commit a0681ee 2023-08-22 15:08:33 UTC, built on 2023-08-22 15:17:40 UTC
warning: `contracts_test` (bin "contracts_test") generated 7 warnings
error: could not compile `contracts_test` (bin "contracts_test") due to previous error; 7 warnings emitted
For my vec3:
use std::fmt;
use std::ops::{Add, AddAssign, Div, DivAssign, Index, IndexMut, Mul, MulAssign, Neg, Sub, SubAssign};
use crate::external_specs;
use prusti_contracts::*;
/// A 3D vector type (and also used as a point).
#[derive(Clone, Copy)]
pub struct Vec3 {
pub x: f64,
pub y: f64,
pub z: f64,
}
pub type Point3 = Vec3;
impl Vec3 {
/// Creates a new Vec3 with components (0, 0, 0).
pub fn new() -> Self {
Vec3 { x: 0.0, y: 0.0, z: 0.0 }
}
/// Creates a new Vec3 with the given components.
pub fn with(e0: f64, e1: f64, e2: f64) -> Self {
Vec3 { x: e0, y: e1, z: e2 }
}
/// Returns the squared length of the vector.
#[pure]
pub fn length_squared(self) -> f64 {
self.x * self.x + self.y * self.y + self.z * self.z
}
/// Returns the length (magnitude) of the vector.
#[pure]
pub fn length(self) -> f64 {
self.length_squared().sqrt()
}
/// Returns a unit vector in the same direction.
#[pure]
#[requires(self.length() != 0.0)]
pub fn unit(self) -> Vec3 {
self / self.length()
}
/// Dot product of two vectors.
#[pure]
pub fn dot(self, other: Vec3) -> f64 {
self.x * other.x + self.y * other.y + self.z * other.z
}
/// Cross product of two vectors.
#[pure]
pub fn cross(self, other: Vec3) -> Vec3 {
Vec3 {
x: self.y * other.z - self.z * other.y,
y: self.z * other.x - self.x * other.z,
z: self.x * other.y - self.y * other.x,
}
}
}
impl PartialEq for Vec3 {
#[pure]
fn eq(&self, other: &Self) -> bool {
self.x == other.x && self.y == other.y && self.z == other.z
}
#[pure]
fn ne(&self, other: &Self) -> bool {
self.x != other.x || self.y != other.y || self.z != other.z
}
}
// Allow Vec3[i] indexing
impl Index<usize> for Vec3 {
type Output = f64;
fn index(&self, i: usize) -> &f64 {
match i {
0 => &self.x,
1 => &self.y,
2 => &self.z,
_ => panic!("Index out of range for Vec3"),
}
}
}
impl IndexMut<usize> for Vec3 {
#[pure]
fn index_mut(&mut self, i: usize) -> &mut f64 {
match i {
0 => &mut self.x,
1 => &mut self.y,
2 => &mut self.z,
_ => panic!("Index out of range for Vec3"),
}
}
}
// Unary minus
impl Neg for Vec3 {
type Output = Vec3;
#[pure]
fn neg(self) -> Vec3 {
Vec3 { x: -self.x, y: -self.y, z: -self.z }
}
}
// Vec3 += Vec3
impl AddAssign for Vec3 {
#[pure]
fn add_assign(&mut self, other: Vec3) {
self.x += other.x;
self.y += other.y;
self.z += other.z;
}
}
// Vec3 + Vec3
impl Add for Vec3 {
type Output = Vec3;
#[pure]
fn add(self, other: Vec3) -> Vec3 {
Vec3 { x: self.x + other.x, y: self.y + other.y, z: self.z + other.z }
}
}
// Vec3 -= Vec3
impl SubAssign for Vec3 {
#[pure]
fn sub_assign(&mut self, other: Vec3) {
self.x -= other.x;
self.y -= other.y;
self.z -= other.z;
}
}
// Vec3 - Vec3
impl Sub for Vec3 {
type Output = Vec3;
#[pure]
fn sub(self, other: Vec3) -> Vec3 {
Vec3 { x: self.x - other.x, y: self.y - other.y, z: self.z - other.z }
}
}
// Vec3 *= f64
impl MulAssign<f64> for Vec3 {
#[pure]
fn mul_assign(&mut self, t: f64) {
self.x *= t;
self.y *= t;
self.z *= t;
}
}
// Vec3 * f64
impl Mul<f64> for Vec3 {
type Output = Vec3;
#[pure]
fn mul(self, t: f64) -> Vec3 {
Vec3 { x: self.x * t, y: self.y * t, z: self.z * t }
}
}
// f64 * Vec3
impl Mul<Vec3> for f64 {
type Output = Vec3;
#[pure]
fn mul(self, v: Vec3) -> Vec3 {
Vec3 { x: v.x * self, y: v.y * self, z: v.z * self }
}
}
// Vec3 /= f64
impl DivAssign<f64> for Vec3 {
#[pure]
fn div_assign(&mut self, t: f64) {
*self *= 1.0 / t;
}
}
// Vec3 / f64
impl Div<f64> for Vec3 {
type Output = Vec3;
#[pure]
fn div(self, t: f64) -> Vec3 {
self * (1.0 / t)
}
}
// Display as "x y z"
impl fmt::Display for Vec3 {
fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
write!(f, "{} {} {}", self.x, self.y, self.z)
}
}
#[test]
fn test() {
let mut v1 = Vec3::with(1.0, 2.0, 3.0);
let v2 = Vec3::with(-1.0, 0.5, 4.0);
v1 += v2;
assert_eq!(v1, Vec3::with(0.0, 2.5, 7.0));
let d = Vec3::dot(v1, v2);
assert_eq!(d, v1.x * v2.x + v1.y * v2.y + v1.z * v2.z);
}
Having some external specs defined:
use std::ops::Div;
use prusti_contracts::*;
#[extern_spec]
impl Div for f64 {
#[pure]
#[ensures(result == self / rhs)]
fn div(self, rhs: Self) -> Self::Output;
}
#[extern_spec]
impl f64 {
#[pure]
#[ensures(result * result == self)]
pub fn sqrt(self) -> f64;
}