hacspec / hax

A Rust verification tool
https://hacspec.org/blog
Apache License 2.0
195 stars 20 forks source link

Frontend: supposely unreachable place: `CallNotTyFnDef` #1048

Closed W95Psp closed 1 week ago

W95Psp commented 1 week ago
error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef".
              This error report happend because some assumption about the Rust AST was broken.

              Context:
               - e: Expr {
                  kind: Deref {
                      arg: e137,
                  },
                  ty: Binder { value: fn(&'^0.Named(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), "'_") str) -> std::vec::Vec<usize, std::alloc::Global>, bound_vars: [Region(BrNamed(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), '_))] },
                  temp_lifetime: Some(
                      Node(141),
                  ),
                  span: src/word_splitters.rs:165:52: 165:65 (#0),
              }
               - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), "'_") str) -> std::vec::Vec<usize, std::alloc::Global>, bound_vars: [Region(BrNamed(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), '_))] }
   --> src/word_splitters.rs:165:52
    |
165 |             WordSplitter::Custom(splitter_func) => splitter_func(word),
    |                                                    ^^^^^^^^^^^^^
    |
    = note: ⚠️ This is a bug in Hax's frontend.
            Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)!
Crate `textwrap@0.16.1` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e137, }, ty: Binder { value: fn(&'^0.Named(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), "'_") str) -> std::vec::Vec, bound_vars: [Region(BrNamed(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), '_))] }, temp_lifetime: Some( Node(141), ), span: src/word_splitters.rs:165:52: 165:65 (#0), } - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), "'_") str) -> std::vec::Vec, bound_vars: [Region(BrNamed(DefId(0:413 ~ textwrap[c191]::word_splitters::WordSplitter::'_), '_))] } --> src/word_splitters.rs:165:52 | 165 | WordSplitter::Custom(splitter_func) => splitter_func(word), | ^^^^^^^^^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `combine@4.6.7` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e0, }, ty: Binder { value: fn(&'^0.Named(DefId(0:9707 ~ combine[01d7]::parser::function::{impl#2}::'_), "'_") mut Input/#0) -> std::result::Result<(O/#1, error::Commit<()>), error::Commit>>, bound_vars: [Region(BrNamed(DefId(0:9707 ~ combine[01d7]::parser::function::{impl#2}::'_), '_))] }, temp_lifetime: Some( Node(13), ), span: src/parser/function.rs:92:9: 92:13 (#0), } - ty_kind: &'{erased} mut Binder { value: fn(&'^0.Named(DefId(0:9707 ~ combine[01d7]::parser::function::{impl#2}::'_), "'_") mut Input/#0) -> std::result::Result<(O/#1, error::Commit<()>), error::Commit>>, bound_vars: [Region(BrNamed(DefId(0:9707 ~ combine[01d7]::parser::function::{impl#2}::'_), '_))] } --> src/parser/function.rs:92:9 | 92 | self(input).into() | ^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `yansi@1.0.1` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e3, }, ty: Binder { value: fn() -> bool, bound_vars: [] }, temp_lifetime: Some( Node(12), ), span: src/style.rs:136:41: 136:42 (#0), } - ty_kind: condition::Condition --> src/style.rs:136:41 | 136 | self.condition.map_or(true, |c| c()) | ^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `pyo3@0.22.5` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e170, }, ty: Binder { value: fn() -> impl_::pymethods::PyMethodDefType, bound_vars: [] }, temp_lifetime: Some( Node(152), ), span: src/impl_/pyclass/lazy_type_object.rs:156:40: 156:47 (#0), } - ty_kind: &'{erased} Binder { value: fn() -> impl_::pymethods::PyMethodDefType, bound_vars: [] } --> src/impl_/pyclass/lazy_type_object.rs:156:40 | 156 | built_method = builder(); | ^^^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `pyo3-macros-backend@0.22.5` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e2, }, ty: Binder { value: fn(&'^0.Named(DefId(0:3898 ~ pyo3_macros_backend[4e39]::pymethod::TokenGenerator::'_), "'_") utils::Ctx) -> proc_macro2::TokenStream, bound_vars: [Region(BrNamed(DefId(0:3898 ~ pyo3_macros_backend[4e39]::pymethod::TokenGenerator::'_), '_))] }, temp_lifetime: Some( Node(25), ), span: src/pymethod.rs:1644:9: 1644:14 (#0), } - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:3898 ~ pyo3_macros_backend[4e39]::pymethod::TokenGenerator::'_), "'_") utils::Ctx) -> proc_macro2::TokenStream, bound_vars: [Region(BrNamed(DefId(0:3898 ~ pyo3_macros_backend[4e39]::pymethod::TokenGenerator::'_), '_))] } --> src/pymethod.rs:1644:9 | 1644 | (gen)(ctx).to_tokens(tokens) | ^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `proptest@1.5.0` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e0, }, ty: Binder { value: fn() -> T/#0, bound_vars: [] }, temp_lifetime: Some( Node(7), ), span: src/strategy/just.rs:143:9: 143:13 (#0), } - ty_kind: &'{erased} Binder { value: fn() -> T/#0, bound_vars: [] } --> src/strategy/just.rs:143:9 | 143 | self() | ^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `napi@2.16.13` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e399, }, ty: Binder { value: unsafe fn(*mut napi_sys::napi_env__) -> std::result::Result<*mut napi_sys::napi_value__, error::Error>, bound_vars: [] }, temp_lifetime: Some( Node(699), ), span: src/bindgen_runtime/module_register.rs:346:29: 346:37 (#0), } - ty_kind: &'{erased} Binder { value: unsafe fn(*mut napi_sys::napi_env__) -> std::result::Result<*mut napi_sys::napi_value__, error::Error>, bound_vars: [] } --> src/bindgen_runtime/module_register.rs:346:29 | 346 | if let Err(e) = callback(env).and_then(|v| { | ^^^^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `winit@0.30.5` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e59, }, ty: Binder { value: unsafe extern "C { unwind: false }" fn(*mut xkbcommon_dl::xkb_context, *const i8, xkbcommon_dl::xkb_compose_compile_flags) -> *mut xkbcommon_dl::xkb_compose_table, bound_vars: [] }, temp_lifetime: Some( Node(116), ), span: src/platform_impl/linux/common/xkb/compose.rs:33:13: 33:54 (#0), } - ty_kind: libloading::safe::Symbol<'{erased}, Binder { value: unsafe extern "C { unwind: false }" fn(*mut xkbcommon_dl::xkb_context, *const i8, xkbcommon_dl::xkb_compose_compile_flags) -> *mut xkbcommon_dl::xkb_compose_table, bound_vars: [] }> --> src/platform_impl/linux/common/xkb/compose.rs:33:13 | 33 | (XKBCH.xkb_compose_table_new_from_locale)( | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `tera@1.20.0` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e1147, }, ty: Binder { value: fn(&'^0.Named(DefId(0:3264 ~ tera[0261]::tera::EscapeFn::'_), "'_") str) -> std::string::String, bound_vars: [Region(BrNamed(DefId(0:3264 ~ tera[0261]::tera::EscapeFn::'_), '_))] }, temp_lifetime: Some( Node(1163), ), span: src/renderer/processor.rs:446:26: 446:51 (#0), } - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:3264 ~ tera[0261]::tera::EscapeFn::'_), "'_") str) -> std::string::String, bound_vars: [Region(BrNamed(DefId(0:3264 ~ tera[0261]::tera::EscapeFn::'_), '_))] } --> src/renderer/processor.rs:446:26 | 446 | to_value(self.tera.get_escape_fn()(res.as_str().unwrap())).map_err(Error::json)?, | ^^^^^^^^^^^^^^^^^^^^^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `wasmtime@26.0.0` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e158, }, ty: Binder { value: fn(&'^0.Named(DefId(0:20059 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#4), "'_") wasmtime_environ::component::InterfaceType, &'^1.Named(DefId(0:20060 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#5), "'_") runtime::component::matching::InstanceType<'^2.Named(DefId(0:20061 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#6), "'_")>) -> core::result::Result<(), anyhow::Error>, bound_vars: [Region(BrNamed(DefId(0:20059 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#4), '_)), Region(BrNamed(DefId(0:20060 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#5), '_)), Region(BrNamed(DefId(0:20061 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#6), '_))] }, temp_lifetime: Some( Node(148), ), span: src/runtime/component/func/typed.rs:1739:17: 1739:22 (#0), } - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:20059 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#4), "'_") wasmtime_environ::component::InterfaceType, &'^1.Named(DefId(0:20060 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#5), "'_") runtime::component::matching::InstanceType<'^2.Named(DefId(0:20061 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#6), "'_")>) -> core::result::Result<(), anyhow::Error>, bound_vars: [Region(BrNamed(DefId(0:20059 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#4), '_)), Region(BrNamed(DefId(0:20060 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#5), '_)), Region(BrNamed(DefId(0:20061 ~ wasmtime[4c5e]::runtime::component::func::typed::typecheck_tuple::'_#6), '_))] } --> src/runtime/component/func/typed.rs:1739:17 | 1739 | check(ty, types)?; | ^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `async-graphql@7.0.11` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e60, }, ty: Binder { value: fn(&'^0.Named(DefId(0:8648 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_), "'_") validation::visitor::VisitorContext<'^1.Named(DefId(0:8649 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#1), "'_")>, &'^2.Named(DefId(0:8650 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#2), "'_") [async_graphql_parser::Positioned], &'^3.Named(DefId(0:8651 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#3), "'_") async_graphql_parser::types::Field, usize) -> std::result::Result, bound_vars: [Region(BrNamed(DefId(0:8648 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_), '_)), Region(BrNamed(DefId(0:8649 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#1), '_)), Region(BrNamed(DefId(0:8650 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#2), '_)), Region(BrNamed(DefId(0:8651 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#3), '_))] }, temp_lifetime: Some( Node(126), ), span: src/validation/visitors/complexity.rs:61:27: 61:28 (#0), } - ty_kind: &'{erased} Binder { value: fn(&'^0.Named(DefId(0:8648 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_), "'_") validation::visitor::VisitorContext<'^1.Named(DefId(0:8649 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#1), "'_")>, &'^2.Named(DefId(0:8650 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#2), "'_") [async_graphql_parser::Positioned], &'^3.Named(DefId(0:8651 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#3), "'_") async_graphql_parser::types::Field, usize) -> std::result::Result, bound_vars: [Region(BrNamed(DefId(0:8648 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_), '_)), Region(BrNamed(DefId(0:8649 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#1), '_)), Region(BrNamed(DefId(0:8650 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#2), '_)), Region(BrNamed(DefId(0:8651 ~ async_graphql[e2d5]::registry::ComputeComplexityFn::'_#3), '_))] } --> src/validation/visitors/complexity.rs:61:27 | 61 | match f( | ^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `neon@1.0.0` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e34, }, ty: Binder { value: fn(*mut sys::bindings::types::Env__, *mut u32) -> sys::bindings::types::Status, bound_vars: [] }, temp_lifetime: Some( Node(108), ), span: src/sys/bindings/functions.rs:427:16: 427:27 (#0), } - ty_kind: libloading::Symbol<'{erased}, Binder { value: fn(*mut sys::bindings::types::Env__, *mut u32) -> sys::bindings::types::Status, bound_vars: [] }> --> src/sys/bindings/functions.rs:427:16 | 427 | assert_eq!(get_version(env, &mut version as *mut _), Status::Ok,); | ^^^^^^^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
Crate `kube-runtime@0.96.0` ``` error[E9999]: Supposely unreachable place in the Rust AST. The label is "CallNotTyFnDef". This error report happend because some assumption about the Rust AST was broken. Context: - e: Expr { kind: Deref { arg: e55, }, ty: Binder { value: fn(&'^0.Named(DefId(0:3366 ~ kube_runtime[2c1d]::utils::_::__SplitCaseProjection::'_), "'_") Alias(Projection, AliasTy { args: [S/#0], def_id: DefId(34:71 ~ futures_core[3a68]::stream::Stream::Item), .. })) -> bool, bound_vars: [Region(BrNamed(DefId(0:3366 ~ kube_runtime[2c1d]::utils::_::__SplitCaseProjection::'_), '_))] }, temp_lifetime: Some( Node(68), ), span: src/utils/mod.rs:84:20: 84:46 (#0), } - ty_kind: &'{erased} mut Binder { value: fn(&'^0.Named(DefId(0:3366 ~ kube_runtime[2c1d]::utils::_::__SplitCaseProjection::'_), "'_") Alias(Projection, AliasTy { args: [S/#0], def_id: DefId(34:71 ~ futures_core[3a68]::stream::Stream::Item), .. })) -> bool, bound_vars: [Region(BrNamed(DefId(0:3366 ~ kube_runtime[2c1d]::utils::_::__SplitCaseProjection::'_), '_))] } --> src/utils/mod.rs:84:20 | 84 | if (this.should_consume_item)(x_ref) { | ^^^^^^^^^^^^^^^^^^^^^^^^^^ | = note: ⚠️ This is a bug in Hax's frontend. Please report this error to https://github.com/hacspec/hax/issues with some context (e.g. the current crate)! ```
W95Psp commented 1 week ago

Repro:

#[derive(Clone)]
pub enum Repro {
    Custom(fn() -> ()),
}

impl Repro {
    pub fn split_points(&self) {
        match self {
            Repro::Custom(splitter_func) => splitter_func(),
        }
    }
}

Open this code snippet in the playground

W95Psp commented 1 week ago

Fixed by #1052