Segfault on OpenBSD

[bentley]

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 (e718bb6).

[NikolajBjorner]

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

[bentley]

What is your architecture?

This is on amd64.

[bentley]

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

(declare-datatype)

[NikolajBjorner]

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]

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]

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]

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]

@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: yrutschle/sslh#270

[intrigus-lgtm]

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

[catap]

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

[NikolajBjorner]

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