Grisette not normalising terms that I would expect it to

[RobinWebbers]

Hi!

So I'm using Grisette to build a symbolic evaluator plugin for GHC Core. There was something that stumped me when looking at the generated code. Specifically, Grisette is usually very good at reducing any constant expression that may exist in a term, but in this instance it appears quite a few constants weren't folded. I was curious if you (@lsrcz) have any idea as to why this happened. I did not want to make an issue for this, since I'm not sure what is happening exactly and if it is actually a bug.

Code

This is the piece of code that I symbolically interpret. It is reasonableysmall and you can assume that Signed 5 is directly interpreted as the underlying SMT solver primitive. The goal for it is to show that it is valid: the expression is always True (which holds, so no issue there!)

example :: Signed 5 -> Signed 5 -> Bool
example x y = x + y == y + x

Internal Representation

You can see what this translates to in the internal representation of my symbolic executor. A tag in Haskell can be 64 bits, hence the huge bvconcat. The remaining bit that actually determines the boolean is a bitcast of the Haskell expression you see up top. The first check is there just to ensure the tag is within bounds (otherwise, we would get Undefined Behaviour when pattern matching on this tag).

ite
  (|| (< (bvconcat 0b000000000000000000000000000000000000000000000000000000000000000 (bitcast (= (+ x y) (+ y x)))) 0x0000000000000000) (! (< (bvconcat 0b000000000000000000000000000000000000000000000000000000000000000 (bitcast (= (+ x y) (+ y x)))) 0x0000000000000002)))
  UB
  tagToEnum# @Bool (bvconcat 0b000000000000000000000000000000000000000000000000000000000000000 (bitcast (= (+ x y) (+ y x))))

Constraints

So far so good, these are pretty much what I would expect them to be. (Of course, there is room for the equivalence check to be folded, but alas). Now, if I turn this into constraints for the SMT solver, something weird happens: the constraints that are generated only contain constants but still end up in the query:

[GOOD] (declare-fun s0 () (_ BitVec 5))
[GOOD] (declare-fun s1 () (_ BitVec 5))
[GOOD] (define-fun s2 () (_ BitVec 63) #b000000000000000000000000000000000000000000000000000000000000000)
[GOOD] (define-fun s4 () (_ BitVec 1) (bvneg #b1))
[GOOD] (define-fun s8 () (_ BitVec 64) #x0000000000000000)
[GOOD] (define-fun s11 () (_ BitVec 64) #x0000000000000002)
[GOOD] (define-fun s3 () (_ BitVec 5) (bvadd s0 s1))
[GOOD] (define-fun s5 () (_ BitVec 1) s4)
[GOOD] (define-fun s6 () (_ BitVec 64) (concat s2 s5))
[GOOD] (define-fun s7 () (_ BitVec 64) s6)
[GOOD] (define-fun s9 () Bool (bvslt s7 s8))
[GOOD] (define-fun s10 () Bool (not s9))
[GOOD] (define-fun s12 () Bool (bvslt s7 s11))
[GOOD] (define-fun s13 () Bool (and s10 s12))
[GOOD] (define-fun s14 () Bool (not s13))
[GOOD] (assert s14)
[SEND] (check-sat)
[RECV] unsat

Notice s4, which is a constant but is not folded. If you follow the chain from there, you'll see that any (transitive) usage of this could have been folded. That is, the entire expression only contains constants. Another odd one here is s3, which is not even used at all (and is in fact the addition of x and y; somehow Grisette reasoned about this ahead of time?).

Minimal Example

I wasn't able to create a minimal example for the full thing. It appears the constants fold when I write them out manually. I was able to reconstruct the obsolete addition (like s3) that appears in the output with the following expression.

do
  let r0 = ("x" :: SymIntN 5) + "y" .== "y" + "x"
  let r1 = sizedBVZext @SymIntN @1 @64 Proxy $ bitCast r0
  bitCast @_ @SymBool $ sizedBVSelect @_ @64 @0 @1 Proxy Proxy r1

[GOOD] (declare-fun s0 () (_ BitVec 5))
[GOOD] (declare-fun s1 () (_ BitVec 5))
[GOOD] (define-fun s2 () (_ BitVec 5) (bvadd s0 s1))
[GOOD] (assert false)

Do you have any idea why Grisette is not folding the constants? I'm curious what you have to say on the matter!

[lsrcz]

Hi @RobinWebbers, I am traveling and am very busy this week, but I will investigate sometime. The issue sounds to be related to how we utilize sbv as our SMT backend as the internal representation looks good.

[lsrcz]

Hi @RobinWebbers , I finally got some time to look at this. It wasn't very easy to investigate the problem without a reproducer for the constant folding problem. I tried to construct something but I cannot reproduce the problem.

The obsolete definitions seem benign and would not hurt solver performance. It comes from the fact that Grisette doesn't simply such term, while the underlying sbv further simplifies it. Since sbv won't remove any value that has already been defined, it is shown in the final solver call.