search

facebookexperimental / MIRAI

Rust mid-level IR Abstract Interpreter
MIT License
1k stars 86 forks source link

Panic while compiling `libm` #1252

Closed Zeta611 closed 11 months ago

Zeta611 commented 11 months ago

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 git@github.com: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: a23ff7e4dfdf7f701a65486d61a08f124ed60026 (the most recent version)

Zeta611 commented 11 months ago

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 commented 11 months ago

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 commented 11 months ago

I have created a PR that fixes these issues.