Segfault on OpenBSD - Githubissues

bentley commented 1 year ago

The following testcase from Symbiyosys (executed with z3 -smt2 -in) crashes on OpenBSD -current.

; SMT-LIBv2 description generated by Yosys 0.32 (git sha1 fbab08acf14, c++ 13.0.0 -O2 -fPIC -Os)
; yosys-smt2-stdt
; yosys-smt2-module top
(set-option :produce-models true)
(set-logic ALL)
(declare-datatype |top_s| ((|top_mk|
(|top_is| Bool)
(|top#0| (_ BitVec 8)) ; \counter
(|top#1| Bool) ; \clk
(|top#2| (_ BitVec 1)) ; \_witness_.anyinit_procdff_12
(|top#3| (_ BitVec 1)) ; $formal$autotune_div.sv:4$1_EN
)))
; yosys-smt2-witness {"offset": 0, "path": ["\\counter"], "smtname": 0, "smtoffset": 0, "type": "reg", "width": 8}
; yosys-smt2-register counter 8
; yosys-smt2-wire counter 8
(define-fun |top_n counter| ((state |top_s|)) (_ BitVec 8) (|top#0| state))
; yosys-smt2-input clk 1
; yosys-smt2-wire clk 1
; yosys-smt2-clock clk posedge
; yosys-smt2-witness {"offset": 0, "path": ["\\clk"], "smtname": "clk", "smtoffset": 0, "type": "posedge", "width": 1}
; yosys-smt2-witness {"offset": 0, "path": ["\\clk"], "smtname": "clk", "smtoffset": 0, "type": "input", "width": 1}
(define-fun |top_n clk| ((state |top_s|)) Bool (|top#1| state))
; yosys-smt2-anyinit top#2 1 autotune_div.sv:3.5-6.8
; yosys-smt2-witness {"offset": 0, "path": ["\\_witness_", "\\anyinit_procdff_12"], "smtname": 2, "smtoffset": 0, "type": "init", "width": 1}
; yosys-smt2-register _witness_.anyinit_procdff_12 1
; yosys-smt2-wire _witness_.anyinit_procdff_12 1
(define-fun |top_n _witness_.anyinit_procdff_12| ((state |top_s|)) Bool (= ((_ extract 0 0) (|top#2| state)) #b1))
; yosys-smt2-witness {"offset": 0, "path": ["$formal$autotune_div.sv:4$1_EN"], "smtname": 3, "smtoffset": 0, "type": "reg", "width": 1}
; yosys-smt2-register $formal$autotune_div.sv:4$1_EN 1
(define-fun |top_n $formal$autotune_div.sv:4$1_EN| ((state |top_s|)) Bool (= ((_ extract 0 0) (|top#3| state)) #b1))
(define-fun |top#4| ((state |top_s|)) (_ BitVec 1) (bvnot (ite (|top#1| state) #b1 #b0))) ; $auto$rtlil.cc:2400:Not$17
; yosys-smt2-assume 0 $auto$formalff.cc:758:execute$18
(define-fun |top_u 0| ((state |top_s|)) Bool (or (= ((_ extract 0 0) (|top#4| state)) #b1) (not true))) ; $auto$formalff.cc:758:execute$18
; yosys-smt2-assert 0 $assert$autotune_div.sv:4$7 autotune_div.sv:4.32-5.30
(define-fun |top_a 0| ((state |top_s|)) Bool (or (= ((_ extract 0 0) (|top#2| state)) #b1) (not (= ((_ extract 0 0) (|top#3| state)) #b1)))) ; $assert$autotune_div.sv:4$7
(define-fun |top#5| ((state |top_s|)) Bool (distinct (|top#0| state) #b00000100)) ; $0$formal$autotune_div.sv:4$1_CHECK[0:0]$3
(define-fun |top#6| ((state |top_s|)) (_ BitVec 8) (bvadd (|top#0| state) #b00000001)) ; $0\counter[7:0]
(define-fun |top_a| ((state |top_s|)) Bool
(|top_a 0| state)
)
(define-fun |top_u| ((state |top_s|)) Bool
(|top_u 0| state)
)
(define-fun |top_i| ((state |top_s|)) Bool (and
(= (|top#0| state) #b00000000) ; counter
(= (= ((_ extract 0 0) (|top#3| state)) #b1) false) ; $formal$autotune_div.sv:4$1_EN
))
(define-fun |top_h| ((state |top_s|)) Bool true)
(define-fun |top_t| ((state |top_s|) (next_state |top_s|)) Bool (and
(= #b1 (|top#3| next_state)) ; $procdff$13 $formal$autotune_div.sv:4$1_EN
(= (ite (|top#5| state) #b1 #b0) (|top#2| next_state)) ; $procdff$12 \_witness_.anyinit_procdff_12
(= (|top#6| state) (|top#0| next_state)) ; $procdff$11 \counter
)) ; end of module top
; yosys-smt2-topmod top
; end of yosys output
(declare-fun s0 () |top_s|)
(assert (|top_u| s0))
(assert (|top_h| s0))
(assert (|top_i| s0))
(assert (|top_is| s0))
(check-sat)

Backtrace:

Program terminated with signal SIGSEGV, Segmentation fault.
#0  0x0000030813fbeddd in vector<std::__1::pair<char const*, double>, false, unsigned int>::vector (this=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/util/vector.h:166
166         T * m_data = nullptr;
(gdb) bt
#0  0x0000030813fbeddd in vector<std::__1::pair<char const*, double>, false, unsigned int>::vector (this=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/util/vector.h:166
#1  svector<std::__1::pair<char const*, double>, unsigned int>::svector (
    this=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/util/vector.h:739
#2  statistics::statistics (this=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/util/statistics.h:25
#3  smt_tactic::smt_tactic (this=0x30aaa312608, m=..., p=...)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/smt/tactic/smt_tactic_core.cpp:52
#4  0x0000030813fbeb63 in mk_seq_smt_tactic (m=..., p=...)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/smt/tactic/smt_tactic_core.cpp:409
#5  mk_smt_tactic_core (m=..., p=..., logic=...)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/smt/tactic/smt_tactic_core.cpp:419
#6  0x00000308142b3da9 in mk_smt_tactic (m=..., p=...)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/tactic/smtlogics/smt_tactic.cpp:30
#7  0x00000308142ae557 in mk_qfbv_tactic (m=..., p=...)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/tactic/smtlogics/qfbv_tactic.cpp:126
#8  0x00000308142d2bf4 in mk_default_tactic (m=..., p=...)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/tactic/portfolio/default_tactic.cpp:39
#9  0x00000308142d398d in smt_strategic_solver_factory::operator() (
    this=<optimized out>, m=..., p=..., proofs_enabled=<optimized out>, 
    models_enabled=<optimized out>, unsat_core_enabled=<optimized out>, 
    logic=...)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/tactic/portfolio/smt_strategic_solver.cpp:171
#10 0x0000030813928204 in cmd_context::mk_solver (this=0x7cf7f5b81600)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/cmd_context/cmd_context.cpp:2167
#11 0x00000308139296bb in cmd_context::init_manager_core (this=0x7cf7f5b81600, 
    new_manager=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/cmd_context/cmd_context.cpp:795
#12 0x0000030813968005 in cmd_context::pm (this=0x7cf7f5b81600)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/cmd_context/cmd_context.h:413
#13 smt2::parser::pm (this=0x7cf7f5b80d78)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/parsers/smt2/smt2parser.cpp:123
#14 smt2::parser::parse_declare_datatype (this=0x7cf7f5b80d78)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/parsers/smt2/smt2parser.cpp:95--Type <RET> for more, q to quit, c to continue without paging--
2
#15 0x0000030813963014 in smt2::parser::operator() (this=0x7cf7f5b80d78)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/parsers/smt2/smt2parser.cpp:3164
#16 0x0000030813962272 in parse_smt2_commands (ctx=..., is=..., 
    interactive=<optimized out>, ps=..., filename=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/parsers/smt2/smt2parser.cpp:3215
#17 0x00000308143d140f in read_smtlib2_commands (file_name=0x0)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/shell/smtlib_frontend.cpp:185
#18 0x00000308143ceff4 in main (argc=<optimized out>, argv=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2/z3-z3-4.12.2/src/shell/main.cpp:384

This crash occurs with both the 4.12.2 release and git master (e718bb64737fac5c4b365919530fca77104560aa).

NikolajBjorner commented 1 year ago

it doesn't repro for me (but not on your arch/opsys). What is your architecture? Specifically pointer alignment may be at stake.

bentley commented 1 year ago

What is your architecture?

This is on amd64.

bentley commented 1 year ago

Here’s a minimal reproducer. This input crashes with the same backtrace:

(declare-datatype)

NikolajBjorner commented 1 year ago

The reproducer does not crash on my side. It did exhibit an issue with the parser. It should have failed earlier when reading the ")". This was fixed. I have to suspect there is an issue specific with respect to the toolchain you are using.

bentley commented 1 year ago

While that’s possible, in my experience it’s more likely to be OpenBSD’s strong malloc catching some hidden memory corruption. Of course, I can’t guarantee that’s the case (though it’s at least consistent with its failure to crash on your end).

The latest git prints out an error for (declare-datatype), as expected. Now, the simplest reproducer for the crash is (declare-datatype a).

#0  0x00000f45a1ee771e in vector<std::__1::pair<char const*, double>, false, unsigned int>::vector (this=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/util/vector.h:169
169         T * m_data = nullptr;
(gdb) bt
#0  0x00000f45a1ee771e in vector<std::__1::pair<char const*, double>, false, unsigned int>::vector (this=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/util/vector.h:169
#1  svector<std::__1::pair<char const*, double>, unsigned int>::svector (
    this=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/util/vector.h:742
#2  statistics::statistics (this=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/util/statistics.h:25
#3  smt::context::context (this=0xf489d6ff008, m=..., p=..., _p=...)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/smt/smt_context.cpp:50
#4  0x00000f45a1f21aa8 in smt::kernel::imp::imp (this=0xf489d6ff008, m=..., 
    fp=..., p=...)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/smt/smt_kernel.cpp:32
#5  smt::kernel::kernel (this=0xf4869bd7a80, m=..., fp=..., p=...)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/smt/smt_kernel.cpp:55
#6  0x00000f45a1f56d25 in (anonymous namespace)::smt_solver::smt_solver (
    this=0xf4869bd76f8, m=..., p=..., l=...)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/smt/smt_solver.cpp:75
#7  0x00000f45a1f56c85 in mk_smt_solver (m=..., p=..., logic=...)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/smt/smt_solver.cpp:511
#8  0x00000f45a258a070 in mk_smt2_solver (m=..., p=..., logic=...)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/tactic/portfolio/smt_strategic_solver.cpp:124
#9  0x00000f45a258a679 in mk_solver_for_logic (m=..., p=..., logic=...)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/tactic/portfolio/smt_strategic_solver.cpp:136
#10 smt_strategic_solver_factory::operator() (this=<optimized out>, m=..., 
    p=..., proofs_enabled=<optimized out>, models_enabled=<optimized out>, 
    unsat_core_enabled=<optimized out>, logic=...)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/tactic/portfolio/smt_strategic_solver.cpp:174
#11 0x00000f45a1bd1134 in cmd_context::mk_solver (this=0x779ab34538a0)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/cmd_context/cmd_context.cpp:2237
#12 0x00000f45a1bd25eb in cmd_context::init_manager_core (this=0x779ab34538a0, 
    new_manager=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/cmd_context/cmd_context.cpp:862
#13 0x00000f45a1c14188 in cmd_context::pm (this=0x779ab34538a0)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/cmd_context/cmd_context.h:414
#14 smt2::parser::pm (this=0x779ab3453010)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/parsers/smt2/smt2parser.cpp:124
#15 smt2::parser::parse_declare_datatype (this=0x779ab3453010)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/parsers/smt2/smt2parser.cpp:974
#16 0x00000f45a1c0ef44 in smt2::parser::operator() (this=0x779ab3453010)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/parsers/smt2/smt2parser.cpp:3191
#17 0x00000f45a1c0e182 in parse_smt2_commands (ctx=..., is=..., 
    interactive=<optimized out>, ps=..., filename=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/parsers/smt2/smt2parser.cpp:3242
#18 0x00000f45a26887af in read_smtlib2_commands (file_name=0x0)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/shell/smtlib_frontend.cpp:185
#19 0x00000f45a2686394 in main (argc=<optimized out>, argv=<optimized out>)
    at /usr/ports/pobj/z3-4.12.2pl20230927/z3-9033b826f4d55f8a4b6d6d98eab3c8dceadf07ca/src/shell/main.cpp:384

NikolajBjorner commented 12 months ago

The asan heap sanitizer does not suggest any memory corruptions. Your environment may be dealing with a pointer alignment assumption, such as 128 bit alignment?

catap commented 3 months ago

I can confirm that 4.13.0 does crashes on OpenBSD current/amd64 with similar stacktrace:

Program terminated with signal SIGSEGV, Segmentation fault.
#0  0x000008165feaa151 in vector<std::__1::pair<char const*, double>, false, unsigned int>::vector (this=<optimized out>)
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/util/vector.h:170
170         T * m_data = nullptr;
(gdb) bt
#0  0x000008165feaa151 in vector<std::__1::pair<char const*, double>, false, unsigned int>::vector (this=<optimized out>)
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/util/vector.h:170
#1  svector<std::__1::pair<char const*, double>, unsigned int>::svector (this=<optimized out>)
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/util/vector.h:757
#2  statistics::statistics (this=<optimized out>) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/util/statistics.h:25
#3  smt_tactic::smt_tactic (this=0x81889b39008, m=..., p=...) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/smt/tactic/smt_tactic_core.cpp:52
#4  0x000008165fea9ed3 in mk_seq_smt_tactic (m=..., p=...) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/smt/tactic/smt_tactic_core.cpp:409
#5  mk_smt_tactic_core (m=..., p=..., logic=...) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/smt/tactic/smt_tactic_core.cpp:419
#6  0x000008166016ee49 in mk_smt_tactic (m=..., p=...) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/tactic/smtlogics/smt_tactic.cpp:30
#7  0x0000081660169a07 in mk_qfbv_tactic (m=..., p=...) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/tactic/smtlogics/qfbv_tactic.cpp:126
#8  0x000008166018c074 in mk_default_tactic (m=..., p=...) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/tactic/portfolio/default_tactic.cpp:39
#9  0x000008166018ce29 in smt_strategic_solver_factory::operator() (this=<optimized out>, m=..., p=..., proofs_enabled=<optimized out>, 
    models_enabled=<optimized out>, unsat_core_enabled=<optimized out>, logic=...)
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/tactic/portfolio/smt_strategic_solver.cpp:171
#10 0x000008165f86dc52 in cmd_context::mk_solver (this=0x75cd37de3b08) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/cmd_context/cmd_context.cpp:2239
#11 0x000008165f86f13c in cmd_context::init_manager_core (this=0x75cd37de3b08, new_manager=<optimized out>)
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/cmd_context/cmd_context.cpp:862
#12 0x000008165f8b7c9a in cmd_context::m (this=0x75cd37de3b08) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/cmd_context/cmd_context.h:412
#13 smt2::parser::m (this=0x75cd37de3268) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/parsers/smt2/smt2parser.cpp:123
#14 smt2::parser::sort_stack (this=0x75cd37de3268) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/parsers/smt2/smt2parser.cpp:236
#15 smt2::parser::parse_sort (this=0x75cd37de3268, context=0x8165edf5a17 "Invalid constant declaration")
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/parsers/smt2/smt2parser.cpp:739
#16 0x000008165f8ac2bb in smt2::parser::parse_declare_const (this=0x75cd37de3268)
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/parsers/smt2/smt2parser.cpp:2525
#17 0x000008165f8a9c74 in smt2::parser::operator() (this=0x75cd37de3268) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/parsers/smt2/smt2parser.cpp:3191
#18 0x000008165f8a9104 in parse_smt2_commands (ctx=..., is=..., interactive=<optimized out>, ps=..., filename=<optimized out>)
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/parsers/smt2/smt2parser.cpp:3242
#19 0x0000081660288e69 in read_smtlib2_commands (file_name=0x75cd37de42fb "/tmp/test.z3")
    at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/shell/smtlib_frontend.cpp:182
#20 0x0000081660286bdb in main (argc=2, argv=0x75cd37de4198) at /usr/ports/pobj/z3-4.13.0/z3-z3-4.13.0/src/shell/main.cpp:384

with very trivial input:

(declare-const p Bool)

which I run as z3 /tmp/test.z3.

catap commented 2 months ago

@NikolajBjorner I think that this issue should be reoppened. I can easy reproduce it, and if I build z3 without optimization, it simple works.

Here a good example of an issue with similar symptopms: https://github.com/yrutschle/sslh/issues/270

intrigus-lgtm commented 2 months ago

@catap did you try building Z3 with ASAN or UBSAN?

catap commented 2 months ago

@intrigus-lgtm I had build it as simple as cmake -G Ninja ..

NikolajBjorner commented 2 months ago

These smells of an alignment bug. Either z3 or the compiler (yes it happens sometimes).

catap commented 2 months ago

@NikolajBjorner I just rebuild z3 with using clang-13 instead of clang-16 and it had crashed the same way.

catap commented 2 months ago

@NikolajBjorner meanwhile, when I build z3 without any optimization (-O0), I still can crash it on this theorem:

 (declare-const x Int)
 (declare-const y Int)
 (assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))
 (check-sat)

with stack trace:

(gdb) bt
#0  0x0000094ec7c99015 in lp::lar_solver::lar_solver() ()
#1  0x0000094ec86e74e4 in smt::theory_lra::imp::init() ()
#2  0x0000094ec86e57c7 in smt::theory_lra::init() ()
#3  0x0000094ec820f5e2 in smt::context::register_plugin(smt::theory*) ()
#4  0x0000094ec8326075 in smt::setup::setup_lra_arith() ()
#5  0x0000094ec8324668 in smt::setup::setup_QF_LIA(static_features const&) ()
#6  0x0000094ec832016b in smt::setup::setup_auto_config() ()
#7  0x0000094ec831e883 in smt::setup::operator()(smt::config_mode) ()
#8  0x0000094ec82351bf in smt::context::setup_context(bool) ()
#9  0x0000094ec8232237 in smt::context::setup_and_check(bool) ()
#10 0x0000094ec829966b in smt::kernel::setup_and_check() ()
#11 0x0000094ec89c1d0f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#12 0x0000094ec75635f2 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#13 0x0000094ec756071f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#14 0x0000094ec756071f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#15 0x0000094ec756d903 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#16 0x0000094ec7570f5d in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ()
#17 0x0000094ec75712c0 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::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >&) ()
#18 0x0000094ec7b1685f in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) ()
#19 0x0000094ec7aee5be in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
#20 0x0000094ec7ad3169 in combined_solver::check_sat_core(unsigned int, expr* const*) ()
#21 0x0000094ec7aebaf6 in solver::check_sat(unsigned int, expr* const*) ()
#22 0x0000094ec7b36e04 in cmd_context::check_sat(unsigned int, expr* const*) ()
#23 0x0000094ec7ba839c in smt2::parser::parse_check_sat() ()
#24 0x0000094ec7ba6615 in smt2::parser::parse_cmd() ()
#25 0x0000094ec7ba3775 in smt2::parser::operator()() ()
#26 0x0000094ec7ba2749 in parse_smt2_commands(cmd_context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, bool, params_ref const&, char const*) ()
#27 0x0000094ec917e157 in read_smtlib2_commands(char const*) ()
#28 0x0000094ec917a9c2 in main ()
(gdb)

catap commented 2 months ago

and that's interesting python API on the same theoreme on the same build works fine:

    ~ $ python3                                                                                                                               
    Python 3.11.9 (main, Aug 14 2024, 08:01:59) [Clang 16.0.6 ] on openbsd7
    Type "help", "copyright", "credits" or "license" for more information.
    >>> from z3 import *
    >>> x, y = Ints('x y')
    >>> s = Solver()
    >>> s.add((x % 4) + 3 * (y / 2) > x - y)
    >>> print(s.sexpr())
    (declare-fun y () Int)
    (declare-fun x () Int)
    (assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))

    >>>

NikolajBjorner commented 2 months ago

@NikolajBjorner meanwhile, when I build z3 without any optimization (-O0), I still can crash it on this theorem:

 (declare-const x Int)
 (declare-const y Int)
 (assert (> (+ (mod x 4) (* 3 (div y 2))) (- x y)))
 (check-sat)

with stack trace:

(gdb) bt
#0  0x0000094ec7c99015 in lp::lar_solver::lar_solver() ()
#1  0x0000094ec86e74e4 in smt::theory_lra::imp::init() ()
#2  0x0000094ec86e57c7 in smt::theory_lra::init() ()
#3  0x0000094ec820f5e2 in smt::context::register_plugin(smt::theory*) ()
#4  0x0000094ec8326075 in smt::setup::setup_lra_arith() ()
#5  0x0000094ec8324668 in smt::setup::setup_QF_LIA(static_features const&) ()
#6  0x0000094ec832016b in smt::setup::setup_auto_config() ()
#7  0x0000094ec831e883 in smt::setup::operator()(smt::config_mode) ()
#8  0x0000094ec82351bf in smt::context::setup_context(bool) ()
#9  0x0000094ec8232237 in smt::context::setup_and_check(bool) ()
#10 0x0000094ec829966b in smt::kernel::setup_and_check() ()
#11 0x0000094ec89c1d0f in smt_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#12 0x0000094ec75635f2 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#13 0x0000094ec756071f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#14 0x0000094ec756071f in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#15 0x0000094ec756d903 in unary_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
#16 0x0000094ec7570f5d in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ()
#17 0x0000094ec75712c0 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::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char> >&) ()
#18 0x0000094ec7b1685f in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) ()
#19 0x0000094ec7aee5be in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
#20 0x0000094ec7ad3169 in combined_solver::check_sat_core(unsigned int, expr* const*) ()
#21 0x0000094ec7aebaf6 in solver::check_sat(unsigned int, expr* const*) ()
#22 0x0000094ec7b36e04 in cmd_context::check_sat(unsigned int, expr* const*) ()
#23 0x0000094ec7ba839c in smt2::parser::parse_check_sat() ()
#24 0x0000094ec7ba6615 in smt2::parser::parse_cmd() ()
#25 0x0000094ec7ba3775 in smt2::parser::operator()() ()
#26 0x0000094ec7ba2749 in parse_smt2_commands(cmd_context&, std::__1::basic_istream<char, std::__1::char_traits<char> >&, bool, params_ref const&, char const*) ()
#27 0x0000094ec917e157 in read_smtlib2_commands(char const*) ()
#28 0x0000094ec917a9c2 in main ()
(gdb)

This would be platform specific. It doesn't reproduce on other platforms. Issues that had this flavor in the past were alignment related or in some cases compiler bugs. I don't have OpenBSD handy.

catap commented 2 months ago

@NikolajBjorner if you may give any advice how to track such issue, I willing to invest some time. I've tried static_asset with sizeof and offsetof and it holds for both optimized and non-optimized build.

As other solution you may virtual machine. I may run for you VM with OpenBSD, or you may run it inside Github CI by this method: https://github.com/catap/shell

NikolajBjorner commented 2 months ago

I checked about OpenBSD yesterday. Yes, a VM setup appears to be the way to go for local use. I use wsl2 where only ubuntu (debian/arch/alpine) appear handy and setting up these other environments tends to take quite some time on my side (mainly due to my limited skillsets when it comes to using tools effectively).

The basic culprit was in the past our custom vector class: util/vector.h It has some non-standard uses of casting, but it got cleaned up. The current static assert that is supposed to catch badness is:

https://github.com/Z3Prover/z3/blob/f6dbaee6ce32bbe83c285939731e3e36c1d6bcfc/src/util/vector.h#L183

Since unsigned is 4 bytes, a 16 byte alignment requirement could break things, but then alignof would lie or be the incorrect way to ensure validity of alignment.

Your stacks use constructors that use the vector class so there is some plausible correlation.

NikolajBjorner commented 2 months ago

Another takeaway from this may be that I create another GitHub action: https://github.com/vmactions/openbsd-vm for building z3.

catap commented 2 months ago

I checked about OpenBSD yesterday. Yes, a VM setup appears to be the way to go for local use. I use wsl2 where only ubuntu (debian/arch/alpine) appear handy and setting up these other environments tends to take quite some time on my side (mainly due to my limited skillsets when it comes to using tools effectively).

Well, I can make for you a VM with SSH access with z3, git and cmake / ninja.

catap commented 2 months ago

@NikolajBjorner I think this is different things.

It's crashed on the first call of vector, and if I remove vector from pathway by this diff:

diff --git a/src/smt/tactic/smt_tactic_core.cpp b/src/smt/tactic/smt_tactic_core.cpp
index 2be2ace58..1cfd731ef 100644
--- a/src/smt/tactic/smt_tactic_core.cpp
+++ b/src/smt/tactic/smt_tactic_core.cpp
@@ -41,7 +41,7 @@ class smt_tactic : public tactic {
     smt_params                   m_params;
     params_ref                   m_params_ref;
     expr_ref_vector              m_vars;
-    statistics                   m_stats;
+    // statistics                   m_stats;
     smt::kernel*                 m_ctx = nullptr;
     symbol                       m_logic;
     progress_callback*           m_callback = nullptr;
@@ -100,17 +100,17 @@ public:

     void collect_statistics(statistics & st) const override {
-        if (m_ctx)
-            m_ctx->collect_statistics(st); // ctx is still running...
-        else
-            st.copy(m_stats);
+        // if (m_ctx)
+        //     m_ctx->collect_statistics(st); // ctx is still running...
+        // else
+        //     st.copy(m_stats);
     }

     void cleanup() override {
     }

     void reset_statistics() override {
-        m_stats.reset();
+        // m_stats.reset();
     }

     void set_logic(symbol const & l) override {
@@ -210,11 +210,11 @@ public:
             }
             catch(...) {
                 TRACE("smt_tactic", tout << "exception\n";);
-                m_ctx->collect_statistics(m_stats);
+                // m_ctx->collect_statistics(m_stats);
                 throw;
             }
             SASSERT(m_ctx);
-            m_ctx->collect_statistics(m_stats);
+            // m_ctx->collect_statistics(m_stats);
             proof_ref pr(m_ctx->get_proof(), m);
             TRACE("smt_tactic", tout << r << " " << pr << "\n";);
             switch (r) {

it fails on almost the same time, but on different field:

Program received signal SIGSEGV, Segmentation fault.
0x00000cffe4a95441 in smt_tactic::smt_tactic (this=0xd024414f008, m=..., p=...) at /home/catap/src/z3/src/smt/tactic/smt_tactic_core.cpp:45
45          smt::kernel*                 m_ctx = nullptr;
(gdb) bt
#0  0x00000cffe4a95441 in smt_tactic::smt_tactic (this=0xd024414f008, m=..., p=...) at /home/catap/src/z3/src/smt/tactic/smt_tactic_core.cpp:45
#1  0x00000cffe4a951c3 in mk_seq_smt_tactic (m=..., p=...) at /home/catap/src/z3/src/smt/tactic/smt_tactic_core.cpp:409
#2  mk_smt_tactic_core (m=..., p=..., logic=...) at /home/catap/src/z3/src/smt/tactic/smt_tactic_core.cpp:419
#3  0x00000cffe4d64e69 in mk_smt_tactic (m=..., p=...) at /home/catap/src/z3/src/tactic/smtlogics/smt_tactic.cpp:30
#4  0x00000cffe4d5da27 in mk_qfbv_tactic (m=..., p=...) at /home/catap/src/z3/src/tactic/smtlogics/qfbv_tactic.cpp:126
#5  0x00000cffe4d823a4 in mk_default_tactic (m=..., p=...) at /home/catap/src/z3/src/tactic/portfolio/default_tactic.cpp:39
#6  0x00000cffe4d83149 in smt_strategic_solver_factory::operator() (this=<optimized out>, m=..., p=..., proofs_enabled=<optimized out>, 
    models_enabled=<optimized out>, unsat_core_enabled=<optimized out>, logic=...) at /home/catap/src/z3/src/tactic/portfolio/smt_strategic_solver.cpp:181
#7  0x00000cffe44261e2 in cmd_context::mk_solver (this=0x6ff7d72d5bb0) at /home/catap/src/z3/src/cmd_context/cmd_context.cpp:2246
#8  0x00000cffe4427655 in cmd_context::init_manager_core (this=0x6ff7d72d5bb0, new_manager=<optimized out>)
    at /home/catap/src/z3/src/cmd_context/cmd_context.cpp:862
#9  0x00000cffe447228a in cmd_context::m (this=0x6ff7d72d5bb0) at /home/catap/src/z3/src/cmd_context/cmd_context.h:412
#10 smt2::parser::m (this=0x6ff7d72d5320) at /home/catap/src/z3/src/parsers/smt2/smt2parser.cpp:123
#11 smt2::parser::sort_stack (this=0x6ff7d72d5320) at /home/catap/src/z3/src/parsers/smt2/smt2parser.cpp:236
#12 smt2::parser::parse_sort (this=0x6ff7d72d5320, context=0xcffe3938248 "Invalid constant declaration")
    at /home/catap/src/z3/src/parsers/smt2/smt2parser.cpp:739
#13 0x00000cffe44661bf in smt2::parser::parse_declare_const (this=0x6ff7d72d5320) at /home/catap/src/z3/src/parsers/smt2/smt2parser.cpp:2525
#14 0x00000cffe44638e4 in smt2::parser::operator() (this=0x6ff7d72d5320) at /home/catap/src/z3/src/parsers/smt2/smt2parser.cpp:3191
#15 0x00000cffe4462da2 in parse_smt2_commands (ctx=..., is=..., interactive=<optimized out>, ps=..., filename=<optimized out>)
    at /home/catap/src/z3/src/parsers/smt2/smt2parser.cpp:3242
#16 0x00000cffe4e840ea in read_smtlib2_commands (file_name=0x6ff7d72d63a4 "../test.z3") at /home/catap/src/z3/src/shell/smtlib_frontend.cpp:182
#17 0x00000cffe4e81f4c in main (argc=<optimized out>, argv=<optimized out>) at /home/catap/src/z3/src/shell/main.cpp:384
(gdb)

Something very odd here.

intrigus-lgtm commented 2 months ago

Can you disassemble the instructions around the crashing pc?

catap commented 2 months ago

@intrigus-lgtm thanks for suggestion. With and without diff from https://github.com/Z3Prover/z3/issues/6902#issuecomment-2316395030 it crashes on the same place / function which looks like:

   0x0000077c43c34340 <+0>:       endbr64 
   0x0000077c43c34344 <+4>:       mov    0x3f7785(%rip),%r11        # 0x77c4402bad0 <__retguard_800>
   0x0000077c43c3434b <+11>:      xor    (%rsp),%r11
   0x0000077c43c3434f <+15>:      push   %rbp
   0x0000077c43c34350 <+16>:      mov    %rsp,%rbp
   0x0000077c43c34353 <+19>:      push   %r11
   0x0000077c43c34355 <+21>:      push   %r15
   0x0000077c43c34357 <+23>:      push   %r14
   0x0000077c43c34359 <+25>:      push   %r13
   0x0000077c43c3435b <+27>:      push   %r12
   0x0000077c43c3435d <+29>:      push   %rbx
   0x0000077c43c3435e <+30>:      sub    $0x10,%rsp
   0x0000077c43c34362 <+34>:      mov    %rdx,%r13
   0x0000077c43c34365 <+37>:      mov    %rsi,%rbx
   0x0000077c43c34368 <+40>:      mov    %rdi,%r15
   0x0000077c43c3436b <+43>:      movl   $0x0,0x8(%rdi)
   0x0000077c43c34372 <+50>:      lea    0x424b17(%rip),%rax        # 0x77c44058e90 <_ZTV10smt_tactic+16>
   0x0000077c43c34379 <+57>:      mov    %rax,(%rdi)
   0x0000077c43c3437c <+60>:      mov    %rsi,0x10(%rdi)
   0x0000077c43c34380 <+64>:      lea    0x18(%rdi),%r14
   0x0000077c43c34384 <+68>:      movq   $0x0,-0x40(%rbp)
   0x0000077c43c3438c <+76>:      lea    -0x40(%rbp),%rsi
   0x0000077c43c34390 <+80>:      mov    %r14,%rdi
   0x0000077c43c34393 <+83>:      callq  0x77c435a9eb0 <smt_params::smt_params(params_ref const&)>
   0x0000077c43c34398 <+88>:      lea    -0x40(%rbp),%rdi
   0x0000077c43c3439c <+92>:      callq  0x77c42d96c20 <params_ref::~params_ref()>
   0x0000077c43c343a1 <+97>:      lea    0x330(%r15),%r12
   0x0000077c43c343a8 <+104>:     mov    %r12,%rdi
   0x0000077c43c343ab <+107>:     mov    %r13,%rsi
   0x0000077c43c343ae <+110>:     callq  0x77c42d96cc0 <params_ref::params_ref(params_ref const&)>
   0x0000077c43c343b3 <+115>:     mov    %rbx,0x338(%r15)
   0x0000077c43c343ba <+122>:     movq   $0x0,0x368(%r15)
   0x0000077c43c343c5 <+133>:     movq   $0x0,0x390(%r15)
   0x0000077c43c343d0 <+144>:     movq   $0x0,0x3c0(%r15)
   0x0000077c43c343db <+155>:     movq   $0x0,0x3f0(%r15)
   0x0000077c43c343e6 <+166>:     movq   $0x0,0x420(%r15)
   0x0000077c43c343f1 <+177>:     movq   $0x0,0x450(%r15)
   0x0000077c43c343fc <+188>:     movq   $0x0,0x480(%r15)
   0x0000077c43c34407 <+199>:     movq   $0x0,0x4b0(%r15)
   0x0000077c43c34412 <+210>:     movq   $0x0,0x4e0(%r15)
   0x0000077c43c3441d <+221>:     movq   $0x0,0x510(%r15)
   0x0000077c43c34428 <+232>:     movq   $0x0,0x520(%r15)
   0x0000077c43c34433 <+243>:     movq   $0x0,0x550(%r15)
   0x0000077c43c3443e <+254>:     xorps  %xmm0,%xmm0
=> 0x0000077c43c34441 <+257>:     movaps %xmm0,0x340(%r15)
   0x0000077c43c34449 <+265>:     movaps %xmm0,0x350(%r15)
   0x0000077c43c34451 <+273>:     movw   $0x0,0x360(%r15)
   0x0000077c43c3445b <+283>:     mov    %r13,-0x40(%rbp)
   0x0000077c43c3445f <+287>:     lea    -0x38(%rbp),%rbx
   0x0000077c43c34463 <+291>:     lea    -0x114cc88(%rip),%rsi        # 0x77c42ae77e2
   0x0000077c43c3446a <+298>:     mov    %rbx,%rdi
   0x0000077c43c3446d <+301>:     callq  0x77c42d3ee70 <gparams::get_module(char const*)>
   0x0000077c43c34472 <+306>:     mov    -0x40(%rbp),%rdi
   0x0000077c43c34476 <+310>:     lea    -0x116a447(%rip),%rsi        # 0x77c42aca036
   0x0000077c43c3447d <+317>:     mov    %rbx,%rdx
   0x0000077c43c34480 <+320>:     xor    %ecx,%ecx
   0x0000077c43c34482 <+322>:     callq  0x77c42d989e0 <params_ref::get_bool(char const*, params_ref const&, bool) const>
   0x0000077c43c34487 <+327>:     mov    %al,0x360(%r15)
   0x0000077c43c3448e <+334>:     lea    -0x116dab9(%rip),%rsi        # 0x77c42ac69dc
   0x0000077c43c34495 <+341>:     mov    %r13,%rdi
   0x0000077c43c34498 <+344>:     mov    $0x1,%edx
   0x0000077c43c3449d <+349>:     callq  0x77c42d97b10 <params_ref::get_bool(char const*, bool) const>
   0x0000077c43c344a2 <+354>:     mov    %al,0x361(%r15)
   0x0000077c43c344a9 <+361>:     mov    %rbx,%rdi

catap commented 2 months ago

BTW this is smt_tactic::smt_tactic

catap commented 2 months ago

Here a some how similar issue https://github.com/llvm/llvm-project/issues/89341

catap commented 2 months ago

Well, I just tried gcc, and it builds z3 which works.

catap commented 2 months ago

and for comparing dissasembled output for smt_tactic::smt_tactic which is produced by GCC for near the same code where crash had happened:

   0x0000038bd4f666eb <+1899>:    callq  0x38bd3f85610 <params_ref::~params_ref()>
   0x0000038bd4f666f0 <+1904>:    mov    %r12,%rsi
   0x0000038bd4f666f3 <+1907>:    mov    %r13,%rdi
   0x0000038bd4f666f6 <+1910>:    callq  0x38bd3f855e0 <params_ref::params_ref(params_ref const&)>
   0x0000038bd4f666fb <+1915>:    xor    %eax,%eax
   0x0000038bd4f666fd <+1917>:    lea    0x58(%rsp),%rdi
   0x0000038bd4f66702 <+1922>:    mov    %r15,0x348(%rbx)
   0x0000038bd4f66709 <+1929>:    lea    -0x14314c3(%rip),%rsi        # 0x38bd3b3524d
   0x0000038bd4f66710 <+1936>:    movq   $0x0,0x350(%rbx)
   0x0000038bd4f6671b <+1947>:    movq   $0x0,0x358(%rbx)
   0x0000038bd4f66726 <+1958>:    movq   $0x0,0x360(%rbx)
   0x0000038bd4f66731 <+1969>:    movq   $0x0,0x368(%rbx)
   0x0000038bd4f6673c <+1980>:    movq   $0x0,0x370(%rbx)
   0x0000038bd4f66747 <+1991>:    movq   $0x0,0x378(%rbx)
   0x0000038bd4f66752 <+2002>:    mov    %ax,0x380(%rbx)
   0x0000038bd4f66759 <+2009>:    movq   $0x0,0x388(%rbx)
   0x0000038bd4f66764 <+2020>:    movq   $0x0,0x3a0(%rbx)
   0x0000038bd4f6676f <+2031>:    movq   $0x0,0x3c0(%rbx)
   0x0000038bd4f6677a <+2042>:    movq   $0x0,0x3e0(%rbx)
   0x0000038bd4f66785 <+2053>:    movq   $0x0,0x400(%rbx)
   0x0000038bd4f66790 <+2064>:    movq   $0x0,0x420(%rbx)
   0x0000038bd4f6679b <+2075>:    movq   $0x0,0x440(%rbx)
   0x0000038bd4f667a6 <+2086>:    movq   $0x0,0x460(%rbx)
   0x0000038bd4f667b1 <+2097>:    movq   $0x0,0x480(%rbx)
   0x0000038bd4f667bc <+2108>:    movq   $0x0,0x4a0(%rbx)
   0x0000038bd4f667c7 <+2119>:    movq   $0x0,0x4b0(%rbx)
   0x0000038bd4f667d2 <+2130>:    movq   $0x0,0x4c8(%rbx)
   0x0000038bd4f667dd <+2141>:    mov    %r12,0x50(%rsp)
   0x0000038bd4f667e2 <+2146>:    callq  0x38bd3f2d1f0 <gparams::get_module(char const*)>
   0x0000038bd4f667e7 <+2151>:    mov    0x50(%rsp),%rdi
   0x0000038bd4f667ec <+2156>:    lea    0x8(%rbp),%rdx
   0x0000038bd4f667f0 <+2160>:    xor    %ecx,%ecx
   0x0000038bd4f667f2 <+2162>:    lea    -0x143c5aa(%rip),%rsi        # 0x38bd3b2a24f
   0x0000038bd4f667f9 <+2169>:    callq  0x38bd3f86ac0 <params_ref::get_bool(char const*, params_ref const&, bool) const>
   0x0000038bd4f667fe <+2174>:    mov    %al,0x380(%rbx)
   0x0000038bd4f66804 <+2180>:    mov    $0x1,%edx
   0x0000038bd4f66809 <+2185>:    lea    -0x143dc1e(%rip),%rsi        # 0x38bd3b28bf2
   0x0000038bd4f66810 <+2192>:    mov    %r12,%rdi
   0x0000038bd4f66813 <+2195>:    callq  0x38bd3f85b30 <params_ref::get_bool(char const*, bool) const>
   0x0000038bd4f66818 <+2200>:    mov    %al,0x381(%rbx)
   0x0000038bd4f6681e <+2206>:    lea    0x8(%rbp),%rdi

As you may see here no movaps.

Yes, it defently smells like padding or alignment issue.

catap commented 2 months ago

Quite probably that it is this clang issue: https://github.com/llvm/llvm-project/issues/55844

NikolajBjorner commented 2 months ago

You can try to change the #if in util/vector.h to check if removing the dirty trick with memory helps.

catap commented 2 months ago

@NikolajBjorner a3eb2ff58d9da628c98a6e06faf3e449d04b6a54 crashes the same way.

NikolajBjorner commented 2 months ago

I think you need the commit before that. But if you meant the commit before, then at least it would indicate the dirty tricks in vector are not the culprit. There are some very few other dirty tricks, pointer tagging, but I have a difficult time imagining these to be guilty for startup issues.

catap commented 2 months ago

@NikolajBjorner well, something here quite wrong.

I just tried a1bcf136a6c3a5cec5522cebd34b99ebbec90a8c and it works very long. Long mean minutes, like ten, before I interrupt it.

Inside gdb I see that it iterates inside prime_generator::process_next_k_numbers like it reached an infinity loop.

intrigus-lgtm commented 2 months ago

I checked about OpenBSD yesterday. Yes, a VM setup appears to be the way to go for local use. I use wsl2 where only ubuntu (debian/arch/alpine) appear handy and setting up these other environments tends to take quite some time on my side (mainly due to my limited skillsets when it comes to using tools effectively).

Well, I can make for you a VM with SSH access with z3, git and cmake / ninja.

I might have some time while waiting for some unrelated creduces. If you want me to have a look at it, add this key:

ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIOT9wtdlns4ifzZ3YC+hOEqCZ3Jw239Tyf96cmKHih+6 intrigus-lgtm@z3-alignment-issue-6902

catap commented 2 months ago

@intrigus-lgtm feel free to connect to island.catap.net on port 2222. It should pass you via ssh as root@ and catap@.

This is today's snapshot of OpenBSD 7.6-beta. Inside home of catap user you may z3 and inside z3/build ninja project. If you need a modern GDB it calls egdb.

intrigus-lgtm commented 2 months ago

Okay, this was a fun bug :) TLDR: clang is innocent, z3 is guilty.

Z3 does not define support for HAS_MALLOC_USABLE_SIZE for OpenBSD, only for FreeBSD: https://github.com/Z3Prover/z3/blob/ef58376c1463780af3ea1545ddb3e305f2bf2a2b/src/util/memory_manager.cpp#L23-L25
(When allocating memory for e.g. C++ classes, we end up calling memory::allocate.)
But because HAS_MALLOC_USABLE_SIZE is not defined, we end up in the else here:
https://github.com/Z3Prover/z3/blob/ef58376c1463780af3ea1545ddb3e305f2bf2a2b/src/util/memory_manager.cpp#L306-L312
Normally, malloc is apparently guaranteed to return 16 byte aligned pointers on 64 bit platforms.
But notice this line: return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field Our pointer that was once aligned to 16 bytes, is now only aligned to 8 bytes (because + 1 moved it by 8 bytes)!
When we now perform an SSE instruction on e.g. this_pointer+0x16 it will fail, because it is not 16 byte aligned.
This is exactly the bug we are seeing in this issue.

To fix:

I'm not familiar with the various BSD "flavors", but I'd suggest checking whether any others are missing.
It might be useful to add a static_assert here: https://github.com/Z3Prover/z3/blob/ef58376c1463780af3ea1545ddb3e305f2bf2a2b/src/util/memory_manager.h#L92 that ensures that the type T has an alignment <= 16 bytes.
To fix the actual issue, either get rid of the else (if possible, I did not check feasibility) or put the extra field at the end of the allocation (I guess it's somewhat unusual to put such stuff at the end) or allocate 16 additional bytes such that we can move the pointer not only by 1, but 2 thus keeping alignment intact.

NikolajBjorner commented 2 months ago

Thanks for the thorough analysis! adding size at end wouldn't work because when freeing the pointer we have the pointer offset and not the end to know how long it is. removing the else case would break assumptions that we can query the memory manager for allocation within z3. Using 2 * sizeof(size_t) is safer. or using some better facility from std to compute alignment is going to be the more feasible fix. For now I am going to hardwire the offset to 2 instead of 1 using a macro and I pray for @nunoplopes to educate me which C++ feature to use to get the alignment.

nunoplopes commented 2 months ago

@NikolajBjorner : we can't do better than your fix, I'm afraid. Because deallocate() doesn't know the type that was allocated, so it always has to lookup for a fixed offset. Anyway, all major architectures (linux, mac, windows) use the HAS_MALLOC_USABLE_SIZE path, so let's just close this.

catap commented 2 months ago

I doubt that issue is closed. I just tried 6086a30c071b7a3905c722810f3b53369edb32c0 on provided VM and it crashes as:

z3$ egdb ./z3 
GNU gdb (GDB) 9.2
Copyright (C) 2020 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-unknown-openbsd7.6".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<http://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
    <http://www.gnu.org/software/gdb/documentation/>.

For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from ./z3...
(gdb) set args ../test.z3 
(gdb) r
Starting program: /home/catap/z3/build/z3 ../test.z3 
z3(71582) in realloc(): modified chunk-pointer 0x45cd23e0f48

Program received signal SIGABRT, Aborted.
thrkill () at /tmp/-:2
2       /tmp/-: No such file or directory.
(gdb) bt
#0  thrkill () at /tmp/-:2
#1  0x8f11ff515cdf8c3c in ?? ()
#2  0x0000045cd6992b9b in _libc_abort () at /usr/src/lib/libc/stdlib/abort.c:51
#3  0x0000045cd69970d4 in wrterror (d=0x45ce0b04878, msg=0x45cd69217ed "modified chunk-pointer %p") at /usr/src/lib/libc/stdlib/malloc.c:378
#4  0x0000045cd699ceb1 in find_chunknum (d=0x0, info=<optimized out>, ptr=<optimized out>, check=-694274645) at /usr/src/lib/libc/stdlib/malloc.c:1279
#5  0x0000045cd699862e in ofree (argpool=0x7afe2e3a0ae8, p=0x45cd23e0f48, clear=<optimized out>, check=0, argsz=<optimized out>)
    at /usr/src/lib/libc/stdlib/malloc.c:1677
#6  0x0000045cd69992dd in orealloc (p=0x45cd23e0f48, newsz=88, argpool=<optimized out>) at /usr/src/lib/libc/stdlib/malloc.c:1944
#7  _libc_realloc (ptr=0x45cd23e0f48, size=88) at /usr/src/lib/libc/stdlib/malloc.c:1971
#8  0x0000045acc5a2b9f in memory::reallocate (p=<optimized out>, s=88) at /home/catap/z3/src/util/memory_manager.cpp:336
#9  0x0000045acc5f3898 in vector<unsigned long long, false, unsigned int>::expand_vector (this=0x7afe2e3a0c68) at /home/catap/z3/src/util/vector.h:642
#10 0x0000045acc5f2dcf in vector<unsigned long long, false, unsigned int>::push_back (this=<optimized out>, elem=<optimized out>)
    at /home/catap/z3/src/util/vector.h:963
#11 prime_generator::process_next_k_numbers (this=0x45acd842ea8 <g_prime_generator>, k=<optimized out>) at /home/catap/z3/src/util/prime_generator.cpp:29
#12 0x0000045acd7fb52d in mem_initialize () at src/shell/mem_initializer.cpp:11
#13 0x0000045acc5a23ac in memory::initialize (max_size=0) at /home/catap/z3/src/util/memory_manager.cpp:119
#14 0x0000045acd7fa7b0 in main (argc=2, argv=0x7afe2e3a0db8) at /home/catap/z3/src/shell/main.cpp:341
(gdb)

intrigus-lgtm commented 2 months ago

adding size at end wouldn't work because when freeing the pointer we have the pointer offset and not the end to know how long it is.

Obviously :D I guess, I was just too tired^^

My analysis regarding openbsd missing in https://github.com/Z3Prover/z3/blob/ef58376c1463780af3ea1545ddb3e305f2bf2a2b/src/util/memory_manager.cpp#L23-L25 is wrong, they actually removed support for malloc_usable_size.

intrigus-lgtm commented 2 months ago

I doubt that issue is closed. I just tried 6086a30 on provided VM and it crashes as:

@NikolajBjorner I think you missed a case here: https://github.com/Z3Prover/z3/blob/db4176adf41e7386e5b1f6f0fd3968486659f122/src/util/memory_manager.cpp#L325

the 1 should be SIZE_T_ALIGN. I fixed it on the vm and it works.

NikolajBjorner commented 2 months ago

5237e7d

NikolajBjorner commented 2 months ago

reopen until missing use of SIZE_T_ALIGN is checked.

catap commented 2 months ago

@NikolajBjorner if you have some tests which can be used to confirm that it's ok, I willing to help to run it on OpenBSD.

Anyway, a models in examples/SMT-LIB2 works well on 5237e7def20fdbdace592ea60bd68ab51f9389b5

NikolajBjorner commented 2 months ago

We have tests in several of the existing pipelines. The highlights are:

./test-z3 -a

And run the files in z3test/regressions/smt2 repository.

catap commented 2 months ago

./test-z3 -a

no crash

And run the files in z3test/regressions/smt2 repository.

run as:

find . -name '*.smt2' -exec ~/z3/build/z3 {} \;

no crash here as well.

NikolajBjorner commented 2 months ago

together with the usual BVT CI passing, I would declare this as settled. Thanks a lot for the patience and in-depth help.

catap commented 2 months ago

FYI: the next release of OpenBSD (7.6) contains patches which we had discussed on this PR make z3 quite usefull on that platfrom.

Z3Prover / z3

Segfault on OpenBSD #6902