8000 Memory Leak about sat.lookahead.delta_fraction · Issue #7372 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Memory Leak about sat.lookahead.delta_fraction #7372

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
Closed
Heaven2024 opened this issue Sep 12, 2024 · 1 comment
Closed

Memory Leak about sat.lookahead.delta_fraction #7372

Heaven2024 opened this issue Sep 12, 2024 · 1 comment

Comments

@Heaven2024
Copy link

Hi
Z3 [version 4.13.1 - 64 bit].
ubuntu:22.04
for this case:

(set-logic QF_FPBV)
(declare-fun x () (_ FloatingPoint 11 53))
(declare-fun y () (_ BitVec 64))
(assert (fp.gt x ((_ to_fp 11 53) RNE 1.0)))
(assert (bvult y #x8000000000000000))
(check-sat)

z3 test.smt2 
sat

When (set-option:sat.lookahead.delta_fraction 0.3) is added, a memory leak will be triggered

(set-option :sat.lookahead.delta_fraction 0.3)
(set-logic QF_FPBV)
(declare-fun x () (_ FloatingPoint 11 53))
(declare-fun y () (_ BitVec 64))
(assert (fp.gt x ((_ to_fp 11 53) RNE 1.0)))
(assert (bvult y #x8000000000000000))
(check-sat)

z3 test.smt2 
unknown

=================================================================
==2725223==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 4408 byte(s) in 1 object(s) allocated from:
    #0 0x55d2b09eb36e in malloc (/yuhao/z3/build/z3+0x28436e) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x55d2b5f0ec95 in memory::allocate(unsigned long) /yuhao/z3/build/../src/util/memory_manager.cpp:301:16

SUMMARY: AddressSanitizer: 4408 byte(s) leaked in 1 allocation(s).

I also found that when the value of the option is set to 0.1/0.2, normal solving will not trigger the vulnerability.
@Heaven2024
Copy link
Author
Heaven2024 commented Sep 12, 2024 •
edited
Loading

Similar situation, I think it is the reason of option itself

(set-option :sat.lookahead.delta_fraction 0.4)

(set-logic QF_BV)
(check-sat)

z3 test2.smt2
(error "line 4 column 10: invalid value for delta fraction. It should be a number in the interval 0 to 1")

=================================================================
==2806344==ERROR: LeakSanitizer: detected memory leaks

Direct leak of 5256 byte(s) in 3 object(s) allocated from:
    #0 0x555d31cf036e in malloc (/yuhao/z3/build/z3+0x28436e) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x555d37213c95 in memory::allocate(unsigned long) /yuhao/z3/build/../src/util/memory_manager.cpp:301:16

Indirect leak of 146232 byte(s) in 528 object(s) allocated from:
    #0 0x555d31cf036e in malloc (/yuhao/z3/build/z3+0x28436e) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x555d37213c95 in memory::allocate(unsigned long) /yuhao/z3/build/../src/util/memory_manager.cpp:301:16

Indirect leak of 22 byte(s) in 1 object(s) allocated from:
    #0 0x555d31d2acad in operator new(unsigned long) (/yuhao/z3/build/z3+0x2becad) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x555d31d53ba6 in void std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::_M_construct<char const*>(char const*, char const*, std::forward_iterator_tag) /usr/lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/basic_string.tcc:219:14
    #2 0x555d31d53ba6 in std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::basic_string<std::allocator<char>>(char const*, std::allocator<char> const&) /usr/lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/basic_string.h:539:2
    #3 0x555d31d53ba6 in qi_params::qi_params(params_ref const&) /yuhao/z3/build/../src/smt/params/qi_params.h:81:9
    #4 0x555d31d4ff8e in smt_params::smt_params(params_ref const&) /yuhao/z3/build/../src/smt/params/smt_params.h:253:5
    #5 0x555d3325a8b3 in smt_tactic::smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:52:5
    #6 0x555d3325a126 in mk_seq_smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:409:12
    #7 0x555d3325a126 in mk_smt_tactic_core(ast_manager&, params_ref const&, symbol const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:419:78
    #8 0x555d3227dfd1 in mk_smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/tactic/smtlogics/smt_tactic.cpp:30:12
    #9 0x555d322832b6 in mk_qfbv_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/tactic/smtlogics/qfbv_tactic.cpp:128:42
    #10 0x555d3226b688 in smt_strategic_solver_factory::operator()(ast_manager&, params_ref const&, bool, bool, bool, symbol const&) /yuhao/z3/build/../src/tactic/portfolio/smt_strategic_solver.cpp:181:17
    #11 0x555d35318dee in cmd_context::mk_solver() /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:2244:16
    #12 0x555d35320039 in cmd_context::init_manager_core(bool) /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:862:9
    #13 0x555d3523e93f in cmd_context::m() const /yuhao/z3/build/../src/cmd_context/cmd_context.h:412:63
    #14 0x555d3523e93f in smt2::parser::m() const /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:123:48
    #15 0x555d3523e93f in smt2::parser::expr_stack() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:242:32
    #16 0x555d3523e93f in smt2::parser::parse_check_sat() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:2631:29

Indirect leak of 22 byte(s) in 1 object(s) allocated from:
    #0 0x555d31d2acad in operator new(unsigned long) (/yuhao/z3/build/z3+0x2becad) (BuildId: 5c00c5286df32e49d27f99f213a657243f3d2f76)
    #1 0x555d31d53ba6 in void std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::_M_construct<char const*>(char const*, char const*, std::forward_iterator_tag) /usr/lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/basic_string.tcc:219:14
    #2 0x555d31d53ba6 in std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char>>::basic_string<std::allocator<char>>(char const*, std::allocator<char> const&) /usr/lib/gcc/x86_64-linux-gnu/11/../../../../include/c++/11/bits/basic_string.h:539:2
    #3 0x555d31d53ba6 in qi_params::qi_params(params_ref const&) /yuhao/z3/build/../src/smt/params/qi_params.h:81:9
    #4 0x555d31d4ff8e in smt_params::smt_params(params_ref const&) /yuhao/z3/build/../src/smt/params/smt_params.h:253:5
    #5 0x555d3325a8b3 in smt_tactic::smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:52:5
    #6 0x555d3325a126 in mk_seq_smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:409:12
    #7 0x555d3325a126 in mk_smt_tactic_core(ast_manager&, params_ref const&, symbol const&) /yuhao/z3/build/../src/smt/tactic/smt_tactic_core.cpp:419:78
    #8 0x555d3227dfd1 in mk_smt_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/tactic/smtlogics/smt_tactic.cpp:30:12
    #9 0x555d32283229 in mk_qfbv_tactic(ast_manager&, params_ref const&) /yuhao/z3/build/../src/tactic/smtlogics/qfbv_tactic.cpp:126:61
    #10 0x555d3226b688 in smt_strategic_solver_factory::operator()(ast_manager&, params_ref const&, bool, bool, bool, symbol const&) /yuhao/z3/build/../src/tactic/portfolio/smt_strategic_solver.cpp:181:17
    #11 0x555d35318dee in cmd_context::mk_solver() /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:2244:16
    #12 0x555d35320039 in cmd_context::init_manager_core(bool) /yuhao/z3/build/../src/cmd_context/cmd_context.cpp:862:9
    #13 0x555d3523e93f in cmd_context::m() const /yuhao/z3/build/../src/cmd_context/cmd_context.h:412:63
    #14 0x555d3523e93f in smt2::parser::m() const /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:123:48
    #15 0x555d3523e93f in smt2::parser::expr_stack() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:242:32
    #16 0x555d3523e93f in smt2::parser::parse_check_sat() /yuhao/z3/build/../src/parsers/smt2/smt2parser.cpp:2631:29

SUMMARY: AddressSanitizer: 151532 byte(s) leaked in 533 allocation(s).

NikolajBjorner added a commit that referenced this issue Sep 12, 2024
@NikolajBjorner
fix #7372
99a9a4a 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix Z3Prover#7372
d150f1b 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix Z3Prover#7372
aaeed37 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
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
@Heaven2024
0