CodePlexProject Hosting for Open Source Software

1

Closed

Version:

End of master branch built with Z3DEBUG=1 and _EXTERNAL_RELEASE=1, plus cherry-picked changes:

https://z3.codeplex.com/SourceControl/changeset/110fa0b7fb711418fe2be67f033e8ed70b354972

https://z3.codeplex.com/SourceControl/changeset/f4f1c63abb4a6fd0df908e376b0ab014bce3d9da

2c8b314a15ba

40b1137b30da

Triggered this when trying out the bvumul_noovfl construct. I don't know whether this issue will actually matter in practice, since z3 runs for so long before hitting it.

End of master branch built with Z3DEBUG=1 and _EXTERNAL_RELEASE=1, plus cherry-picked changes:

https://z3.codeplex.com/SourceControl/changeset/110fa0b7fb711418fe2be67f033e8ed70b354972

https://z3.codeplex.com/SourceControl/changeset/f4f1c63abb4a6fd0df908e376b0ab014bce3d9da

2c8b314a15ba

40b1137b30da

Triggered this when trying out the bvumul_noovfl construct. I don't know whether this issue will actually matter in practice, since z3 runs for so long before hitting it.

```
ASSERTION VIOLATION
File: third-party/z3/src/sat/sat_solver.cpp
Line: 1798
is_marked_lit(m_lemma[0])
```

Here is the input. Z3 runs for about 2 hours and 15 minutes before crashing.```
(define-sort bv32 () (_ BitVec 32))
(declare-fun _param_2_addr_26_D0!28 () bv32)
(define-fun tmp!37 () Bool (= #x00000000 _param_2_addr_26_D0!28))
(define-fun tmp!38 () Bool (not tmp!37)) ; check for division by zero
(assert tmp!38)
(define-fun tmp!36 () bv32 (bvudiv #xffffffff _param_2_addr_26_D0!28)) ; 4294967295 / j
(declare-fun _param_1_addr_13_D0!15 () bv32)
(define-fun tmp!39 () Bool (bvult tmp!36 _param_1_addr_13_D0!15))
(define-fun tmp!41 () Bool (not tmp!39)) ; [control-point] 4294967295 / j < i
(assert tmp!41)
(define-fun tmp!43 () Bool (bvumul_noovfl _param_1_addr_13_D0!15 _param_2_addr_26_D0!28))
(define-fun tmp!44 () Bool (not tmp!43))
(assert tmp!44)
(check-sat)
```

Here is a variation that only takes 15 minutes to crash:```
(define-sort bv32 () (_ BitVec 32))
(declare-fun _param_2_addr_26_D0!28 () bv32)
(define-fun tmp!40 () Bool (= #x00000000 _param_2_addr_26_D0!28))
(define-fun tmp!41 () Bool (not tmp!40)) ; check for division by zero
(assert tmp!41)
(declare-fun _param_1_addr_13_D0!15 () bv32)
(define-fun tmp!39 () bv32 (bvudiv _param_1_addr_13_D0!15 _param_2_addr_26_D0!28)) ; i / j
(define-fun tmp!49 () Bool (bvumul_noovfl tmp!39 _param_2_addr_26_D0!28))
(define-fun tmp!50 () Bool (not tmp!49))
(assert tmp!50)
(check-sat)
```

These examples correspond to checking for integer overflow in the multiplications pictured below.```
void *my_calloc(unsigned i, unsigned j)
{
if( 0xffffffffU / j < i )
return;
return malloc( i*j );
}
void *fifteen_minute_crash(unsigned i, unsigned j)
{
return malloc( (i/j)*j );
}
```

A little off topic: Any encoding suggestions to improve z3's performance here? It's OK if the answer is "no" :).No files are attached

## comments

leodemoura wrote Jun 27, 2013 at 10:49 PM

Here is the fix:

https://z3.codeplex.com/SourceControl/changeset/d26f0e1c28e9784e5c931dc326cc300089d8d03b