Skip to content
This repository has been archived by the owner on Aug 22, 2024. It is now read-only.

Panic while compiling libm #1252

Closed
Zeta611 opened this issue Nov 17, 2023 · 3 comments · Fixed by #1253
Closed

Panic while compiling libm #1252

Zeta611 opened this issue Nov 17, 2023 · 3 comments · Fixed by #1253

Comments

@Zeta611
Copy link
Contributor

Zeta611 commented Nov 17, 2023 •
edited
Loading

Issue

MIRAI panics while compiling libm.
I encountered this issue while trying to analyze multiple crates that have libm as one of their dependencies.

Steps to Reproduce

git clone [email protected]:rust-lang/libm.git
cd libm
rustup override set nightly-2023-09-10
MIRAI_LOG=info RUSTC_WRAPPER=../MIRAI/target/debug/mirai cargo build

MIRAI_LOG=debug works as well (with a much longer log), but MIRAI_LOG=trace does not reproduce this issue probably due to the timeout.

Expected Behavior

Should emit some diagnostics without panicking.

Actual Results

I get assertion failed: !(lf || rf) in checker/src/z3_solver.rs:1621:9.
The full log:

   Compiling libm v0.2.8 (/Users/jay/Developer/RustProjects/benchmark/contrib/libm)
[2023-11-17T12:17:37Z INFO  mirai] MIRAI options from environment: Options { single_func: None, test_only: false, diag_level: Default, constant_time_tag_name: None, max_analysis_time_for_body: 30, max_analysis_time_for_crate: 240, statistics: false, call_graph_config: None, print_function_names: false }
[2023-11-17T12:17:37Z INFO  mirai] MIRAI options modified by command line: Options { single_func: None, test_only: false, diag_level: Default, constant_time_tag_name: None, max_analysis_time_for_body: 30, max_analysis_time_for_crate: 240, statistics: false, call_graph_config: None, print_function_names: false }
[2023-11-17T12:17:37Z INFO  mirai::callbacks] Processing input file: build.rs
[2023-11-17T12:17:37Z INFO  mirai] MIRAI options from environment: Options { single_func: None, test_only: false, diag_level: Default, constant_time_tag_name: None, max_analysis_time_for_body: 30, max_analysis_time_for_crate: 240, statistics: false, call_graph_config: None, print_function_names: false }
[2023-11-17T12:17:37Z INFO  mirai] MIRAI options modified by command line: Options { single_func: None, test_only: false, diag_level: Default, constant_time_tag_name: None, max_analysis_time_for_body: 30, max_analysis_time_for_crate: 240, statistics: false, call_graph_config: None, print_function_names: false }
[2023-11-17T12:17:37Z INFO  mirai::callbacks] Processing input file: src/lib.rs
[2023-11-17T12:17:37Z INFO  mirai::callbacks] storing summaries for src/lib.rs at /var/folders/70/nn6j8b5x3rqcz12fq8by4hqm0000gn/T/.tmpKXf1rS/.summary_store.sled
[2023-11-17T12:17:37Z INFO  mirai::summaries] creating a new summary store from the embedded tar file
[2023-11-17T12:17:37Z INFO  mirai::crate_visitor] analyzing function libm.libm_helper.implement_libm_libm_helper_Libm_f32.acos
[2023-11-17T12:17:37Z INFO  mirai::call_visitor] function DefId(1:174 ~ core[3562]::f32::{impl#0}::from_bits::ct_u32_to_f32) has no MIR
[2023-11-17T12:17:37Z INFO  mirai::call_visitor] summary key "core.f32.implement.from_bits.ct_u32_to_f32" with signature "_"
[2023-11-17T12:17:37Z INFO  mirai::call_visitor] function DefId(1:171 ~ core[3562]::f32::{impl#0}::to_bits::ct_f32_to_u32) has no MIR
[2023-11-17T12:17:37Z INFO  mirai::call_visitor] summary key "core.f32.implement.to_bits.ct_f32_to_u32" with signature "_"
[2023-11-17T12:17:38Z INFO  mirai::crate_visitor] analyzing function libm.libm_helper.implement_libm_libm_helper_Libm_f32.acosh
[2023-11-17T12:17:38Z INFO  mirai::call_visitor] function libm.math.log1pf.log1pf can't be reliably analyzed because it calls function core.f32.implement_f32.from_bits which could not be summarized (foreign fn argument key: _).
[2023-11-17T12:17:38Z INFO  mirai::crate_visitor] analyzing function libm.libm_helper.implement_libm_libm_helper_Libm_f32.asin
[2023-11-17T12:17:38Z INFO  mirai::call_visitor] function DefId(1:288 ~ core[3562]::f64::{impl#0}::from_bits::ct_u64_to_f64) has no MIR
[2023-11-17T12:17:38Z INFO  mirai::call_visitor] summary key "core.f64.implement.from_bits.ct_u64_to_f64" with signature "_"
thread 'rustc' panicked at checker/src/z3_solver.rs:1621:9:
assertion failed: !(lf || rf)
stack backtrace:
   0:        0x10610f0c4 - <std::sys_common::backtrace::_print::DisplayBacktrace as core::fmt::Display>::fmt::h2e9954773bfb0d12
   1:        0x106162ce0 - core::fmt::write::h362ae95ace996b8b
   2:        0x106104a40 - std::io::Write::write_fmt::h5cbcacf0a52b50a3
   3:        0x10610ef04 - std::sys_common::backtrace::print::he8c5c5298b85adc1
   4:        0x106111c78 - std::panicking::panic_hook_with_disk_dump::{{closure}}::hdb4ce58c9cadc802
   5:        0x106111978 - std::panicking::panic_hook_with_disk_dump::h493c10eb8f8ae921
   6:        0x10e5e103c - rustc_driver_impl[f519250b47aaf4da]::install_ice_hook::{closure#0}
   7:        0x106112488 - std::panicking::rust_panic_with_hook::h3e3a3c0b72b094d6
   8:        0x106112210 - std::panicking::begin_panic_handler::{{closure}}::hf656d590e2bebbae
   9:        0x10610f550 - std::sys_common::backtrace::__rust_end_short_backtrace::hbff5da812bf097a7
  10:        0x106111fac - _rust_begin_unwind
  11:        0x10618de80 - core::panicking::panic_fmt::h372a6717d900bfe9
  12:        0x10618def4 - core::panicking::panic::hf6395a8b0350445c
  13:        0x1009b69b8 - mirai::z3_solver::Z3Solver::numeric_shr::h1ae88f4509c0f4db
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1621:9
  14:        0x1009b29f8 - mirai::z3_solver::Z3Solver::get_as_numeric_z3_ast::hfc74c73dddd3abad
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1128:52
  15:        0x1009b55e8 - mirai::z3_solver::Z3Solver::numeric_cast::hdc4bb967ef813dbf
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1442:52
  16:        0x1009b260c - mirai::z3_solver::Z3Solver::get_as_numeric_z3_ast::hfc74c73dddd3abad
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1073:18
  17:        0x1009aeee8 - mirai::z3_solver::Z3Solver::general_relational::haa8f3d5db2cd94a1
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:474:35
  18:        0x1009adaf4 - mirai::z3_solver::Z3Solver::get_as_z3_ast::hd241b6cc11f956d4
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:300:53
  19:        0x1009b763c - mirai::z3_solver::Z3Solver::get_as_bool_z3_ast::h08d6397792b8dce8
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1764:21
  20:        0x1009ae2b4 - mirai::z3_solver::Z3Solver::general_boolean_op::h5d2252c66e72859c
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:376:25
  21:        0x1009ad788 - mirai::z3_solver::Z3Solver::get_as_z3_ast::hd241b6cc11f956d4
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:231:17
  22:        0x1009b763c - mirai::z3_solver::Z3Solver::get_as_bool_z3_ast::h08d6397792b8dce8
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1764:21
  23:        0x1009ae288 - mirai::z3_solver::Z3Solver::general_boolean_op::h5d2252c66e72859c
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:375:24
  24:        0x1009adb9c - mirai::z3_solver::Z3Solver::get_as_z3_ast::hd241b6cc11f956d4
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:317:17
  25:        0x1009b763c - mirai::z3_solver::Z3Solver::get_as_bool_z3_ast::h08d6397792b8dce8
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1764:21
  26:        0x1009ae288 - mirai::z3_solver::Z3Solver::general_boolean_op::h5d2252c66e72859c
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:375:24
  27:        0x1009ad788 - mirai::z3_solver::Z3Solver::get_as_z3_ast::hd241b6cc11f956d4
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:231:17
  28:        0x1009b763c - mirai::z3_solver::Z3Solver::get_as_bool_z3_ast::h08d6397792b8dce8
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1764:21
  29:        0x1009ae288 - mirai::z3_solver::Z3Solver::general_boolean_op::h5d2252c66e72859c
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:375:24
  30:        0x1009ad788 - mirai::z3_solver::Z3Solver::get_as_z3_ast::hd241b6cc11f956d4
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:231:17
  31:        0x1009b763c - mirai::z3_solver::Z3Solver::get_as_bool_z3_ast::h08d6397792b8dce8
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:1764:21
  32:        0x1009ace20 - <mirai::z3_solver::Z3Solver as mirai::smt_solver::SmtSolver<*mut z3_sys::_Z3_ast>>::get_as_smt_predicate::hc5c34a9522c8a152
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/z3_solver.rs:143:9
  33:        0x1008e68b4 - mirai::body_visitor::BodyVisitor::check_condition_value_and_reachability::{{closure}}::h806bc9af983e45f4
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/body_visitor.rs:1641:17
  34:        0x100a7e418 - mirai::body_visitor::BodyVisitor::check_condition_value_and_reachability::hf5bf717c004abe5e
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/body_visitor.rs:1602:5
  35:        0x100ada988 - mirai::block_visitor::BlockVisitor::visit_assert::h91cf7b77cf5e8106
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:1522:25
  36:        0x100ad1624 - mirai::block_visitor::BlockVisitor::visit_terminator::h32eb141d992b789b
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:326:18
  37:        0x100acfa14 - mirai::block_visitor::BlockVisitor::visit_basic_block::h572cedf80e54d46e
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:105:13
  38:        0x100a7a8d4 - mirai::body_visitor::BodyVisitor::visit_basic_block::heb412465660e3ed2
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/body_visitor.rs:1101:9
  39:        0x100a78074 - mirai::body_visitor::BodyVisitor::check_for_errors::hfa77ee00b336a7fd
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/body_visitor.rs:817:13
  40:        0x100a74c70 - mirai::body_visitor::BodyVisitor::visit_body::ha1c8625aaaeeda2d
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/body_visitor.rs:236:13
  41:        0x1008f3950 - mirai::call_visitor::CallVisitor::create_and_cache_function_summary::h0eb78b1df418f415
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/call_visitor.rs:141:31
  42:        0x1008f5ab0 - mirai::call_visitor::CallVisitor::get_function_summary::h25beec6b84c3510e
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/call_visitor.rs:382:21
  43:        0x100ad4d64 - mirai::block_visitor::BlockVisitor::visit_call::h0de2be9b90c3e153
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:736:32
  44:        0x100ad1524 - mirai::block_visitor::BlockVisitor::visit_terminator::h32eb141d992b789b
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:311:18
  45:        0x100acfa14 - mirai::block_visitor::BlockVisitor::visit_basic_block::h572cedf80e54d46e
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:105:13
  46:        0x1008c1f38 - mirai::fixed_point_visitor::FixedPointVisitor::visit_basic_block::h06033db9f37b6b26
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/fixed_point_visitor.rs:130:9
  47:        0x1008c18f8 - mirai::fixed_point_visitor::FixedPointVisitor::visit_blocks::hd8355ec349109012
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/fixed_point_visitor.rs:82:21
  48:        0x100a74ae0 - mirai::body_visitor::BodyVisitor::visit_body::ha1c8625aaaeeda2d
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/body_visitor.rs:217:9
  49:        0x1008f3950 - mirai::call_visitor::CallVisitor::create_and_cache_function_summary::h0eb78b1df418f415
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/call_visitor.rs:141:31
  50:        0x1008f5ab0 - mirai::call_visitor::CallVisitor::get_function_summary::h25beec6b84c3510e
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/call_visitor.rs:382:21
  51:        0x100ad4d64 - mirai::block_visitor::BlockVisitor::visit_call::h0de2be9b90c3e153
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:736:32
  52:        0x100ad1524 - mirai::block_visitor::BlockVisitor::visit_terminator::h32eb141d992b789b
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:311:18
  53:        0x100acfa14 - mirai::block_visitor::BlockVisitor::visit_basic_block::h572cedf80e54d46e
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/block_visitor.rs:105:13
  54:        0x1008c1f38 - mirai::fixed_point_visitor::FixedPointVisitor::visit_basic_block::h06033db9f37b6b26
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/fixed_point_visitor.rs:130:9
  55:        0x1008c18f8 - mirai::fixed_point_visitor::FixedPointVisitor::visit_blocks::hd8355ec349109012
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/fixed_point_visitor.rs:82:21
  56:        0x100a74ae0 - mirai::body_visitor::BodyVisitor::visit_body::ha1c8625aaaeeda2d
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/body_visitor.rs:217:9
  57:        0x1008c5f24 - mirai::crate_visitor::CrateVisitor::analyze_body::{{closure}}::ha294e3e8adeb2738
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/crate_visitor.rs:185:23
  58:        0x1008bc24c - mirai::crate_visitor::CrateVisitor::analyze_body::hd49743381c0c135c
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/crate_visitor.rs:173:5
  59:        0x1008c566c - mirai::crate_visitor::CrateVisitor::analyze_some_bodies::{{closure}}::h1662b2539d623381
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/crate_visitor.rs:127:13
  60:        0x1008bbe4c - mirai::crate_visitor::CrateVisitor::analyze_some_bodies::h7937093482ce1f29
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/crate_visitor.rs:71:5
  61:        0x100942afc - mirai::callbacks::MiraiCallbacks::analyze_with_mirai::{{closure}}::h43f94abecba15127
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/callbacks.rs:172:9
  62:        0x100a63068 - mirai::callbacks::MiraiCallbacks::analyze_with_mirai::hacaab8748300ed7f
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/callbacks.rs:131:5
  63:        0x1009423b0 - <mirai::callbacks::MiraiCallbacks as rustc_driver_impl::Callbacks>::after_analysis::{{closure}}::{{closure}}::ha48d9fd1f75db12c
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/callbacks.rs:118:26
  64:        0x100b931c0 - rustc_middle::ty::context::GlobalCtxt::enter::{{closure}}::h27d37b6a0d4891df
                               at /rustc/8ed4537d7c238eb77509d82445cf1cb861a3b5ff/compiler/rustc_middle/src/ty/context.rs:595:37
  65:        0x100af09e0 - rustc_middle::ty::context::tls::enter_context::{{closure}}::hd38dbaa3d9a43a08
                               at /rustc/8ed4537d7c238eb77509d82445cf1cb861a3b5ff/compiler/rustc_middle/src/ty/context/tls.rs:82:9
  66:        0x100a9b1b4 - std::thread::local::LocalKey<T>::try_with::h3da8fa328efeb3e8
                               at /rustc/8ed4537d7c238eb77509d82445cf1cb861a3b5ff/library/std/src/thread/local.rs:270:16
  67:        0x100b9314c - std::thread::local::LocalKey<T>::with::h785ab93035ec42a8
                               at /rustc/8ed4537d7c238eb77509d82445cf1cb861a3b5ff/library/std/src/thread/local.rs:246:9
  68:        0x100b9314c - rustc_middle::ty::context::tls::enter_context::h6fd5ca8e1894b838
                               at /rustc/8ed4537d7c238eb77509d82445cf1cb861a3b5ff/compiler/rustc_middle/src/ty/context/tls.rs:79:9
  69:        0x100b9314c - rustc_middle::ty::context::GlobalCtxt::enter::h771528b25d90c769
                               at /rustc/8ed4537d7c238eb77509d82445cf1cb861a3b5ff/compiler/rustc_middle/src/ty/context.rs:595:9
  70:        0x1009d22a8 - rustc_interface::queries::QueryResult<&rustc_middle::ty::context::GlobalCtxt>::enter::he6b254f3b5c58e04
                               at /rustc/8ed4537d7c238eb77509d82445cf1cb861a3b5ff/compiler/rustc_interface/src/queries.rs:71:9
  71:        0x10094230c - <mirai::callbacks::MiraiCallbacks as rustc_driver_impl::Callbacks>::after_analysis::{{closure}}::hebffbd5da728d3d8
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/callbacks.rs:115:9
  72:        0x100a62f34 - <mirai::callbacks::MiraiCallbacks as rustc_driver_impl::Callbacks>::after_analysis::h55363b1d0091c115
                               at /Users/jay/Developer/RustProjects/benchmark/contrib/MIRAI/checker/src/callbacks.rs:98:5
  73:        0x10e6029d4 - <rustc_interface[3f9b0856dc8a1b35]::interface::Compiler>::enter::<rustc_driver_impl[f519250b47aaf4da]::run_compiler::{closure#1}::{closure#2}, core[35629bdc4bb5a94b]::result::Result<core[35629bdc4bb5a94b]::option::Option<rustc_interface[3f9b0856dc8a1b35]::queries::Linker>, rustc_span[b75a20f38cbca3e5]::ErrorGuaranteed>>
  74:        0x10e62385c - std[ab688d881d6d7b60]::sys_common::backtrace::__rust_begin_short_backtrace::<rustc_interface[3f9b0856dc8a1b35]::util::run_in_thread_with_globals<rustc_interface[3f9b0856dc8a1b35]::interface::run_compiler<core[35629bdc4bb5a94b]::result::Result<(), rustc_span[b75a20f38cbca3e5]::ErrorGuaranteed>, rustc_driver_impl[f519250b47aaf4da]::run_compiler::{closure#1}>::{closure#0}, core[35629bdc4bb5a94b]::result::Result<(), rustc_span[b75a20f38cbca3e5]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[35629bdc4bb5a94b]::result::Result<(), rustc_span[b75a20f38cbca3e5]::ErrorGuaranteed>>
  75:        0x10e625604 - <<std[ab688d881d6d7b60]::thread::Builder>::spawn_unchecked_<rustc_interface[3f9b0856dc8a1b35]::util::run_in_thread_with_globals<rustc_interface[3f9b0856dc8a1b35]::interface::run_compiler<core[35629bdc4bb5a94b]::result::Result<(), rustc_span[b75a20f38cbca3e5]::ErrorGuaranteed>, rustc_driver_impl[f519250b47aaf4da]::run_compiler::{closure#1}>::{closure#0}, core[35629bdc4bb5a94b]::result::Result<(), rustc_span[b75a20f38cbca3e5]::ErrorGuaranteed>>::{closure#0}::{closure#0}, core[35629bdc4bb5a94b]::result::Result<(), rustc_span[b75a20f38cbca3e5]::ErrorGuaranteed>>::{closure#1} as core[35629bdc4bb5a94b]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  76:        0x10611b204 - std::sys::unix::thread::Thread::new::thread_start::h9678d3dce1b2bcfc
  77:        0x184633034 - __pthread_joiner_wake

error: the compiler unexpectedly panicked. this is a bug.

note: we would appreciate a bug report: https://github.com/rust-lang/rust/issues/new?labels=C-bug%2C+I-ICE%2C+T-compiler&template=ice.md

note: please attach the file at `/Users/jay/Developer/RustProjects/benchmark/contrib/libm/rustc-ice-2023-11-17T12:17:37.605489Z-3166.txt` to your bug report

note: compiler flags: --crate-type lib -C embed-bitcode=no -C debuginfo=2 -C split-debuginfo=unpacked -C incremental=[REDACTED]

note: some of the compiler flags provided by cargo are hidden

query stack during panic:
end of query stack
error: could not compile `libm` (lib)

Environment

OS: macOS Sonoma 14.0
CPU: Apple M1 Pro
Rust version (rustc 1.74.0-nightly (8ed4537d7 2023-09-09))
MIRAI: a23ff7e (the most recent version)
Zeta611 added a commit to Zeta611/MIRAI that referenced this issue Nov 17, 2023
@Zeta611
Treat numeric transmute specially
51eb521 
Fixes issues with integer binary operations with floating point numbers
transmuted to integers. Fixes facebookexperimental#1252 (comment)
@Zeta611
Copy link
Contributor Author

Zeta611 commented Nov 17, 2023

I'm not really sure the above fix is the right way---at least it fixed the above issue, which happened while analyzing sqrt(https://github.com/rust-lang/libm/blob/cb2ffdf5435d3302c97a27c8ce7de48e214de037/src/math/sqrt.rs#L151).
MIRAI tried to compute transmute(old(param_1): F64, U64) / two^32 in numeric_shr, but lf was false although it was transmuted to U64.

However, MIRAI panics shortly after making more progress while analyzing the fma function(https://github.com/rust-lang/libm/blob/cb2ffdf5435d3302c97a27c8ce7de48e214de037/src/math/fma.rs#L44).

@Zeta611
Copy link
Contributor Author

Zeta611 commented Nov 18, 2023 •
edited
Loading

The issue while analyzing the fma function boils down to calling bv_cast with the result of bv_overflows.

bv_cast expects ast and mask to have same sorts, as it calls Z3_mk_bvand(_, ast, mask)(https://github.com/prove-rs/z3.rs/blob/26ddf7fb90ea62509bb235286024fc7f76319591/z3-sys/src/lib.rs#L2467).
However, if ast gets returned from bv_overflows, it has Boolean sort, due to the call to Z3_mk_not (https://github.com/prove-rs/z3.rs/blob/26ddf7fb90ea62509bb235286024fc7f76319591/z3-sys/src/lib.rs#L2285).
mask has BitVector sort.

The following is what happens:

get_as_bv_z3_ast(self: "Z3Solver",expression: (overflows((local_22(11): U64) - (local_20(11): U64))) as U64,num_bits: 64)
bv_cast(self: "Z3Solver",expression: overflows((local_22(11): U64) - (local_20(11): U64)),target_type: U64,num_bits: 64)
ast "(not (bvule |local_20(11)| |local_22(11)|))" has sort "Bool"
mask "#xffffffffffffffff" has sort "(_ BitVec 64)"
Error: operator is applied to arguments of the wrong sort

Not quite sure how to fix this though.

Zeta611 added a commit to Zeta611/MIRAI that referenced this issue Nov 18, 2023
@Zeta611
Fix the return type of bv_overflows to be of sort BitVector
e49cedd 
Resolves facebookexperimental#1252 (comment)
@Zeta611 Zeta611 mentioned this issue Nov 18, 2023
Merged
12 tasks
@Zeta611
Copy link
Contributor Author

Zeta611 commented Nov 18, 2023

I have created a PR that fixes these issues.

hermanventer pushed a commit that referenced this issue Nov 19, 2023
@Zeta611
Fix issues around Z3 sorts and floating-point flags. (#1253)
a94a8c7 
* Treat numeric transmute specially

Fixes issues with integer binary operations with floating point numbers
transmuted to integers. Fixes #1252 (comment)

* Fix the return type of `bv_overflows` to be of sort BitVector

Resolves #1252 (comment)
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Fix issues around Z3 sorts and floating-point flags. Zeta611/MIRAI
1 participant
@Zeta611