search

LeventErkok / sbv

SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
https://github.com/LeventErkok/sbv
Other
240 stars 33 forks source link

Set semantics with characters is unsound #601

Closed LeventErkok closed 2 years ago

LeventErkok commented 2 years ago 
satWith z3{verbose=True} $ \x -> Data.SBV.Set.complement (fromList "a" :: SSet Char) .== x

This produces unsat, but it should be sat.

The reason is how we deal with the lack of "character" type in SMTLib. We define it by putting an additional constraint on the set, saying that each element must have a size of 1. But that's not sound: Complement simply includes all the strings (except "a"), and then we choke since that is incompatible with the additional constraint.

Not sure how to deal with this; except maybe to disallow SChar completely. It's really unfortunate. I need to figure out if this unsoundness can exhibit itself outside of SSet (which I suspect it would).

LeventErkok commented 2 years ago

Resolved by detecting and rejecting calls to complement if you have a Char base type. I think this covers all the cases that we need to worry about, though I also wouldn't be surprised if there was some other gotcha lurking behind.

The code is written so if this case is detected users will be directed to this particular ticker. Please report your findings or if you spot any other issues related to this.