search

cvc5 / cvc5

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
Other
1.05k stars 234 forks source link

heap-buffer-overflow in theory::arith::nl::detect_ran_encoding #7893

Closed merlinsun closed 2 years ago

merlinsun commented 2 years ago

Hi, I feel sorry that this formula is difficult to reduce.

Commit: dfb4a4a OS: Ubuntu 20.04

$ cvc5 -q test.smt2
=================================================================
==16400==ERROR: AddressSanitizer: heap-buffer-overflow on address 0x60300014f430 at pc 0x7f470d7d7b33 bp 0x7ffe5409db90 sp 0x7ffe5409db80
READ of size 8 at 0x60300014f430 thread T0
    #0 0x7f470d7d7b32 in cvc5::theory::arith::nl::detect_ran_encoding(cvc5::NodeTemplate<true> const&) (/home/cvc5/build/src/libcvc5.so+0x1620b32)
    #1 0x7f470d7dc3e9 in cvc5::theory::arith::nl::node_to_poly_ran(cvc5::NodeTemplate<true> const&, cvc5::NodeTemplate<true> const&) (/home/cvc5/build/src/libcvc5.so+0x16253e9)
    #2 0x7f470d7dc937 in cvc5::theory::arith::nl::node_to_ran(cvc5::NodeTemplate<true> const&, cvc5::NodeTemplate<true> const&) (/home/cvc5/build/src/libcvc5.so+0x1625937)
    #3 0x7f470d385483 in cvc5::theory::arith::isExpressionZero(cvc5::Env&, cvc5::NodeTemplate<true>, std::map<cvc5::NodeTemplate<true>, cvc5::NodeTemplate<true>, std::less<cvc5::NodeTemplate<true> >, std::allocator<std::pair<cvc5::NodeTemplate<true> const, cvc5::NodeTemplate<true> > > > const&) (/home/cvc5/build/src/libcvc5.so+0x11ce483)
    #4 0x7f470d9a35c4 in cvc5::theory::arith::TheoryArith::getEqualityStatus(cvc5::NodeTemplate<false>, cvc5::NodeTemplate<false>) (/home/cvc5/build/src/libcvc5.so+0x17ec5c4)
......
$ cat test.smt2
(declare-fun real_var242 () Real)
(declare-fun real_var1068 () Real)
(declare-fun real_var723 () Real)
(declare-fun real_var542 () Real)
(declare-fun real_var1201 () Real)
(declare-fun real_var1054 () Real)
(declare-fun real_var537 () Real)
(declare-fun real_var209 () Real)
(declare-fun real_var709 () Real)
(declare-fun real_var722 () Real)
(declare-fun real_var461 () Real)
(declare-fun real_var742 () Real)
(declare-fun real_var1276 () Real)
(declare-fun real_var1202 () Real)
(declare-fun real_var652 () Real)
(declare-fun real_var207 () Real)
(declare-fun real_var204 () Real)
(declare-fun real_var1065 () Real)
(declare-fun real_var1318 () Real)
(declare-fun real_var1275 () Real)
(declare-fun real_var1319 () Real)
(declare-fun real_var945 () Real)
(declare-fun real_var538 () Real)
(declare-fun real_var6 () Real)
(declare-fun real_var45 () Real)
(declare-fun real_var462 () Real)
(declare-fun real_var748 () Real)
(declare-fun real_var1200 () Real)
(declare-fun real_var539 () Real)
(declare-fun real_var92 () Real)
(declare-fun real_var862 () Real)
(declare-fun real_var427 () Real)
(declare-fun real_var141 () Real)
(declare-fun real_var1055 () Real)
(declare-fun real_var1066 () Real)
(declare-fun real_var59 () Real)
(declare-fun real_var459 () Real)
(declare-fun real_var1279 () Real)
(declare-fun real_var655 () Real)
(declare-fun real_var641 () Real)
(declare-fun real_var142 () Real)
(declare-fun real_var84 () Real)
(declare-fun real_var654 () Real)
(declare-fun real_var642 () Real)
(declare-fun real_var1073 () Real)
(declare-fun real_var653 () Real)
(declare-fun real_var46 () Real)
(declare-fun real_var140 () Real)
(declare-fun real_var99 () Real)
(declare-fun real_var428 () Real)
(declare-fun real_var205 () Real)
(declare-fun real_var186 () Real)
(declare-fun real_var746 () Real)
(declare-fun real_var1067 () Real)
(declare-fun real_var708 () Real)
(declare-fun real_var196 () Real)
(declare-fun real_var741 () Real)
(declare-fun real_var1277 () Real)
(declare-fun real_var208 () Real)
(declare-fun real_var747 () Real)
(declare-fun real_var1278 () Real)
(declare-fun real_var187 () Real)
(declare-fun real_var707 () Real)
(declare-fun real_var206 () Real)
(declare-fun real_var749 () Real)
(assert (or (and (not (exists ((REAL_VAR427 Real)) (=> (< 0.0 real_var242) (< (* real_var427 (/ 0 (* 2.0 (+ 6 real_var428)))) 0)))) (not (exists ((REAL_VAR641 Real)) (=> (and (=> (> 0.0 (* real_var1319 real_var1318)) (and (< (* 71.0 71.0 4590495740.0 4590495740.0) 4590495740.0 0.0 71.0 71.0) (>= real_var862 0))) (= real_var140 (mod (to_int real_var141) (to_int real_var142)) (/ real_var141 real_var140)) (<= (+ (* real_var742 real_var741) (- real_var746 real_var747)) (- real_var748 real_var749)) (<= (/ (- 1) real_var538 real_var539 real_var537) real_var542) (< (/ 115 real_var206 real_var209) (/ 137 real_var207 real_var208)) (> 0.0 real_var6)) (= 0.0 (/ real_var641 (/ 423505801.1 real_var641)) 0.62829 real_var642))))) (not (exists ((REAL_VAR1065 Real)) (=> (and (=> (= real_var204 (+ real_var205 real_var196)) (= (+ (* real_var1201 real_var1200) (* (- 1) real_var1201 real_var1202) (* (- 1) real_var1200) (* (- 1) real_var1201 real_var1200 real_var1200) (* real_var1201 real_var1200 real_var1202)) (- 1))) (< 0.0 real_var1065 (/ real_var1066 (* (/ real_var1067 (/ 0.9 real_var1068)) real_var1065 7.0 real_var1065))) (< 0.0 3.0 (/ (+ 0.0 (/ 0.5277230151 0.0) (/ 325285732.0 real_var186)) real_var187) real_var186) (= real_var1073 (exp 0.4))) (< real_var459 real_var461 (/ 0.8545 real_var462)))))))
(assert (forall ((REAL_VAR1073 Real)) (or (and (= real_var1073 (exp 0.4)) (= real_var1054 0 real_var1055) (<= 0 real_var59)) (= (- real_var707 real_var708) real_var709))))
(check-sat)
merlinsun commented 2 years ago

Perhaps this case reveals a similar problem.

$ cvc5 -q case.smt2
Fatal failure within std::tuple<cvc5::NodeTemplate<true>, cvc5::Rational, cvc5::Rational> cvc5::theory::arith::nl::detect_ran_encoding(const Node&) at /cvc5/src/theory/arith/nl/poly_conversion.cpp:668
Check failure

 n.getNumChildren() == 3
Invalid node structure.
Aborted (core dumped)
$ cat case.smt2
(declare-fun r () Real)
(assert (or (forall ((R Real)) (and (< 0.0 (exp 1.0)) (= (exp 0.0) (/ r 0.0)) (= 0.0 (/ (exp 0.0) 0.0))))))
(check-sat)
aniemetz commented 2 years ago

@merlinsun did you try to reduce this with https://github.com/ddsmt/ddSMT? It subsumes pydelta (I'm assuming that's what you are using).

merlinsun commented 2 years ago

Hi, @aniemetz In fact, I could no longer reproduce heap-buffer-overflow later, and cvc5 throws fatal failure for this formula. The simplified formula using ddsmt has also been shown above. I also used cvc5 nightly build to recheck.

$ cvc5-2022-01-13-x86_64-Linux-production 7893_2.smt2 -q
cvc5 suffered a segfault.
Offending address is 0x4
Looks like a NULL pointer was dereferenced.
Segmentation fault (core dumped)
$ cat 7893_2.smt2
(declare-fun r () Real)
(assert (or (forall ((R Real)) (and (< 0.0 (exp 1.0)) (= (exp 0.0) (/ r 0.0)) (= 0.0 (/ (exp 0.0) 0.0))))))
(check-sat)
nafur commented 2 years ago

This has been fixed since #7939