search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.41k stars 1.47k forks source link

Memory Leak on FP Input Involving Multiple Operators #480

Closed kyledewey closed 8 years ago

kyledewey commented 8 years ago

On the master branch at commit 40c5152075ae9a96aee4a0fdb08e65af96f25e1d, consider the following input:

(set-logic QF_FP)
(declare-fun x2 () (_ FloatingPoint 2 3))
(declare-fun x1 () (_ FloatingPoint 2 3))
(declare-fun x0 () (_ FloatingPoint 2 3))
(assert (not (fp.eq (fp.max (fp.add RTN (fp.mul RTZ x0 x1) (_ NaN 2 3)) x2) x2)))
(assert (= (_ NaN 2 3) x0))
(check-sat)
(get-model)

Placing this into a file test.smtlib2 and running with command-line z3 -smt2 test.smtlib2 yields the following output:

sat
(model 
  (define-fun x2 () (_ FloatingPoint 2 3)
    (_ NaN 2 3))
  (define-fun x1 () (_ FloatingPoint 2 3)
    (_ +zero 2 3))
  (define-fun x0 () (_ FloatingPoint 2 3)
    (_ NaN 2 3))
  (define-fun fp.max_unspecified ((x!1 (_ FloatingPoint 2 3))
   (x!2 (_ FloatingPoint 2 3))) (_ FloatingPoint 2 3)
    (_ +zero 2 3))
)
ast_manager LEAKED: 66
Leaked: bv[0:6]
Leaked: Leaked: Bool
Leaked: Leaked: (bvadd bv[1:2] bv[1:2])
Leaked: Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
(extract[0:0] #75)
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
(if #74 bv[5:4] #71)
Leaked: Leaked: bv[1:2]
Leaked: bv[5:4]
Leaked: Leaked: bv
Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
#84 := (concat bv[0:10] #85)
#73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
#82 := (concat #91 bv[0:6])
(bvlshr #82 #84)
Leaked: Leaked: Leaked: Leaked: Leaked: Leaked: bv
Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
(bvsub #79 #79)
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#76 := (extract[1:1] #75)
(bvnot #76)
Leaked: Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
(extract[1:0] #72)
Leaked: (zero_extend[1] bv[1:2])
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
(zero_extend[2] #69)
Leaked: bv
Leaked: Leaked: Leaked: #73 := (zero_extend[1] bv[1:2])
(concat #73 bv[0:3])
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
(bvule bv[5:4] #71)
Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
#84 := (concat bv[0:10] #85)
#73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
#82 := (concat #91 bv[0:6])
#86 := (bvlshr #82 #84)
(extract[5:0] #86)
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
#84 := (concat bv[0:10] #85)
#73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
#82 := (concat #91 bv[0:6])
#86 := (bvlshr #82 #84)
(extract[11:6] #86)
Leaked: bv[0:10]
Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
#84 := (concat bv[0:10] #85)
#73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
#82 := (concat #91 bv[0:6])
#86 := (bvlshr #82 #84)
#89 := (extract[5:0] #86)
(= #89 bv[0:6])
Leaked: Leaked: Leaked: #73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
(concat #91 bv[0:6])
Leaked: bv
Leaked: Leaked: bv
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
#84 := (concat bv[0:10] #85)
#73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
#82 := (concat #91 bv[0:6])
#86 := (bvlshr #82 #84)
#89 := (extract[5:0] #86)
#161 := (= #89 bv[0:6])
#101 := (if #161 bv[0:6] bv[1:6])
#88 := (extract[11:6] #86)
#102 := (bvor #88 #101)
#104 := (zero_extend[2] #102)
#103 := (zero_extend[2] #91)
(bvsub #103 #104)
Leaked: bv[0:3]
Leaked: Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
#84 := (concat bv[0:10] #85)
#73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
#82 := (concat #91 bv[0:6])
#86 := (bvlshr #82 #84)
#89 := (extract[5:0] #86)
#161 := (= #89 bv[0:6])
#101 := (if #161 bv[0:6] bv[1:6])
#88 := (extract[11:6] #86)
(bvor #88 #101)
Leaked: bv
Leaked: bv
Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
#84 := (concat bv[0:10] #85)
#73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
#82 := (concat #91 bv[0:6])
#86 := (bvlshr #82 #84)
#89 := (extract[5:0] #86)
#161 := (= #89 bv[0:6])
(if #161 bv[0:6] bv[1:6])
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
(extract[1:1] #75)
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
(concat bv[0:10] #85)
Leaked: Leaked: Leaked: #73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
(zero_extend[2] #91)
Leaked: bv
Leaked: bv[1:6]
Leaked: Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
#79 := (concat #77 #78)
#69 := (bvsub #79 #79)
#71 := (zero_extend[2] #69)
#74 := (bvule bv[5:4] #71)
#72 := (if #74 bv[5:4] #71)
#85 := (extract[1:0] #72)
#84 := (concat bv[0:10] #85)
#73 := (zero_extend[1] bv[1:2])
#91 := (concat #73 bv[0:3])
#82 := (concat #91 bv[0:6])
#86 := (bvlshr #82 #84)
#89 := (extract[5:0] #86)
#161 := (= #89 bv[0:6])
#101 := (if #161 bv[0:6] bv[1:6])
#88 := (extract[11:6] #86)
#102 := (bvor #88 #101)
(zero_extend[2] #102)
Leaked: #75 := (bvadd bv[1:2] bv[1:2])
#78 := (extract[0:0] #75)
#76 := (extract[1:1] #75)
#77 := (bvnot #76)
(concat #77 #78)

It may be possible to minimize this input further.

wintersteiger commented 8 years ago

Thanks for the report, this and a couple related ones are now fixed.