Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Possible undefined behavior in mpz.cpp line 2252 #6085

Closed
patrick96 opened this issue Jun 6, 2022 · 1 comment
Closed

Possible undefined behavior in mpz.cpp line 2252 #6085

patrick96 opened this issue Jun 6, 2022 · 1 comment

Comments

@patrick96
Copy link

In mpz.cpp:2252, the mlog2 function executes -a.mval, if a.mval is INT_MIN, this results in undefined behavior:

z3/src/util/mpz.cpp

Lines 2248 to 2252 in dca1dcc

unsigned mpz_manager<SYNCH>::mlog2(mpz const & a) {
if (is_nonneg(a))
return 0;
if (is_small(a))
return ::log2((unsigned)-a.m_val);

The following formula triggers that case:

(declare-const a Bool)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)
(assert
    (exists ((v Int))
        (and
            (<= (mod (ite (distinct c 0) 0 b) 4294967296) (+ 4294967296 (div d b)))
            (= v 0)
            (< 0 (mod 0 0))
            (< 2147483647 (mod (ite (distinct c 0) 0 b) 4294967296))
            a
        )
    )
)
(check-sat)
$ z3-asan-8c95dff33 int_min.smt2                                                                       
/home/patrick96/Projects/github.com/z3prover/z3/src/util/mpz.cpp:2252:22: runtime error: negation of -2147483648 cannot be represented in type 'int'; cast to an unsigned type to negate this value to itself
sat

Z3 was compiled in debug mode with asan and ubsan:

cmake -DCMAKE_BUILD_TYPE=Debug -DZ3_INCLUDE_GIT_HASH=TRUE -DCMAKE_C_FLAGS="-fsanitize=address,undefined -fno-omit-frame-pointer" -DCMAKE_CXX_FLAGS="-fsanitize=address,undefined -fno-omit-frame-pointer" ..

I found this in 8c95dff and reproduced it on master (dca1dcc).
@patrick96
Copy link
Author

patrick96 commented Jun 6, 2022 •
edited
Loading

I just pulled the latest changes, the same formula now produces a segfault (null-pointer dereference):

/home/patrick96/Projects/github.com/Z3Prover/z3/src/util/mpz.cpp:2256:14: runtime error: member access within null pointer of type 'struct mpz_cell'
AddressSanitizer:DEADLYSIGNAL
=================================================================
==1844066==ERROR: AddressSanitizer: SEGV on unknown address 0x000000000000 (pc 0x558f800d6b4e bp 0x7ffd8bee3ae0 sp 0x7ffd8bee3aa0 T0)
==1844066==The signal is caused by a READ memory access.
==1844066==Hint: address points to the zero page.
    #0 0x558f800d6b4e in mpz_manager<true>::mlog2(mpz const&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/util/mpz.cpp:2256
    #1 0x558f800d6d14 in mpz_manager<true>::bitsize(mpz const&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/util/mpz.cpp:2277
    #2 0x558f80074e7a in mpq_manager<true>::bitsize(mpz const&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/util/mpq.h:798
    #3 0x558f80074f5a in mpq_manager<true>::bitsize(mpq const&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/util/mpq.h:799
    #4 0x558f83126333 in rational::bitsize() const /home/patrick96/Projects/github.com/Z3Prover/z3/src/util/rational.h:69
    #5 0x558f85d831da in smt::theory_arith<smt::i_ext>::mul_bound_of(expr*, unsigned int, old_interval&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_nl.h:279
    #6 0x558f85dd6913 in smt::theory_arith<smt::i_ext>::mk_interval_for(grobner::monomial const*) /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_nl.h:1825
    #7 0x558f85dd832f in smt::theory_arith<smt::i_ext>::is_inconsistent(old_interval const&, unsigned int, grobner::monomial* const*, dependency_manager<scoped_dependency_manager<void*>::config>::dependency*) /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_nl.h:1851
    #8 0x558f85ddad44 in smt::theory_arith<smt::i_ext>::is_inconsistent(grobner::equation const*, grobner&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_nl.h:1884
    #9 0x558f85dea36b in smt::theory_arith<smt::i_ext>::get_gb_eqs_and_look_for_conflict(ptr_vector<grobner::equation>&, grobner&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_nl.h:2155
    #10 0x558f85de6b44 in smt::theory_arith<smt::i_ext>::compute_grobner(svector<int, unsigned int> const&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_nl.h:2258
    #11 0x558f85df4ab4 in smt::theory_arith<smt::i_ext>::process_non_linear() /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_nl.h:2358
    #12 0x558f85c75131 in smt::theory_arith<smt::i_ext>::final_check_core() /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_core.h:1491
    #13 0x558f85c78cee in smt::theory_arith<smt::i_ext>::final_check_eh() /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/theory_arith_core.h:1529
    #14 0x558f8557ebed in smt::context::final_check() /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/smt_context.cpp:3974
    #15 0x558f85577be5 in smt::context::bounded_search() /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/smt_context.cpp:3889
    #16 0x558f85569cd4 in smt::context::search() /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/smt_context.cpp:3717
    #17 0x558f8555bf7e in smt::context::setup_and_check(bool) /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/smt_context.cpp:3540
    #18 0x558f8571c8e3 in smt::kernel::setup_and_check() /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/smt_kernel.cpp:124
    #19 0x558f874433b4 in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/smt/tactic/smt_tactic_core.cpp:207
    #20 0x558f81d26e3f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/tactic/tactical.cpp:121
    #21 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #22 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #23 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #24 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #25 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #26 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #27 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #28 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #29 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #30 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #31 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #32 0x558f81d433fc in cond_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x1639d3fc)
    #33 0x558f81d26e3f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/tactic/tactical.cpp:121
    #34 0x558f81d396ad in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x163936ad)
    #35 0x558f81d57b22 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/tactic/tactic.cpp:153
    #36 0x558f81d58c2a in check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >&) /home/patrick96/Projects/github.com/Z3Prover/z3/src/tactic/tactic.cpp:173
    #37 0x558f832672f1 in check_sat_core2 /home/patrick96/Projects/github.com/Z3Prover/z3/src/solver/tactic2solver.cpp:229
    #38 0x558f83236d50 in solver_na2as::check_sat_core(unsigned int, expr* const*) /home/patrick96/Projects/github.com/Z3Prover/z3/src/solver/solver_na2as.cpp:67
    #39 0x558f831eb3b2 in combined_solver::check_sat_core(unsigned int, expr* const*) /home/patrick96/Projects/github.com/Z3Prover/z3/src/solver/combined_solver.cpp:252
    #40 0x558f8322fd84 in solver::check_sat(unsigned int, expr* const*) /home/patrick96/Projects/github.com/Z3Prover/z3/src/solver/solver.cpp:318
    #41 0x558f832f68c8 in cmd_context::check_sat(unsigned int, expr* const*) /home/patrick96/Projects/github.com/Z3Prover/z3/src/cmd_context/cmd_context.cpp:1702
    #42 0x558f8349315c in smt2::parser::parse_check_sat() /home/patrick96/Projects/github.com/Z3Prover/z3/src/parsers/smt2/smt2parser.cpp:2611
    #43 0x558f834a0e5c in smt2::parser::parse_cmd() /home/patrick96/Projects/github.com/Z3Prover/z3/src/parsers/smt2/smt2parser.cpp:2953
    #44 0x558f834a8a09 in smt2::parser::operator()() /home/patrick96/Projects/github.com/Z3Prover/z3/src/parsers/smt2/smt2parser.cpp:3162
    #45 0x558f834378ce in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) /home/patrick96/Projects/github.com/Z3Prover/z3/src/parsers/smt2/smt2parser.cpp:3211
    #46 0x558f7fe6af20 in read_smtlib2_commands(char const*) /home/patrick96/Projects/github.com/Z3Prover/z3/src/shell/smtlib_frontend.cpp:142
    #47 0x558f7fe618cd in main /home/patrick96/Projects/github.com/Z3Prover/z3/src/shell/main.cpp:371
    #48 0x7f6f4ec2928f  (/usr/lib/libc.so.6+0x2928f)
    #49 0x7f6f4ec29349 in __libc_start_main (/usr/lib/libc.so.6+0x29349)
    #50 0x558f7fdbd264 in _start (/home/patrick96/Projects/github.com/Z3Prover/z3/build/z3+0x14417264)

AddressSanitizer can not provide additional info.
SUMMARY: AddressSanitizer: SEGV /home/patrick96/Projects/github.com/Z3Prover/z3/src/util/mpz.cpp:2256 in mpz_manager<true>::mlog2(mpz const&)
==1844066==ABORTING

EDIT: Seems this has been fixed in cc045de

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

No branches or pull requests
1 participant
@patrick96