what4: Don't annotate `{Nonce,}AppExpr`s

[langston-barrett]

Fixes #246. Really, Annotation shouldn't need to carry a Nonce, because the outer NonceAppExpr will already have one. However, actually removing it is challenging due to the return type of sbNonceExpr, and in turn ExprAllocator's nonceExpr, which returns an Expr. Surely in practice, this is always a NonceAppExpr, but there's no way to tell from the type. To avoid a larger refactor or introducing partiality, I'm keeping the Nonce in Annotation for now.

Fixes #246, though we may want to create a follow-up about removing the Nonce from Annotation.

[langston-barrett]

CI fails with:

test unsafeSetAbstractValue2:            FAIL
    test/ExprBuilderSMTLib2.hs:1157:
    unsafeSetAbstractValue doesn't work as expected for a
    compound symbolic expression

the test:

https://github.com/GaloisInc/what4/blob/e46dff42096550d860d210bd9cf6e435d8cd7ce5/what4/test/ExprBuilderSMTLib2.hs#L1144-L1160

I'm able to reproduce this locally with

cabal configure --enable-tests
cabal run test:expr-builder-smtlib2 -- -p 'unsafeSetAbstractValue2'

On this branch,

    print e2A
    print e2B
    print e2C
    print e2C'
    print e2D

yields

cx2A@0:bv
cx2B@1:bv
bvSum cx2B@1:bv cx2A@0:bv
bvSum cx2B@1:bv cx2A@0:bv
bvSum cx2B@1:bv cx2A@0:bv 0x1:[8]

whereas on master it yields

cx2A@0:bv
cx2B@1:bv
bvSum cx2B@1:bv cx2A@0:bv
annotation Nonce {indexValue = 3} (bvSum cx2B@1:bv cx2A@0:bv)
0x3:[8]

[langston-barrett]

Printf-debugging shows that this branch hits this case in semiRingAdd:

https://github.com/GaloisInc/what4/blob/e46dff42096550d860d210bd9cf6e435d8cd7ce5/what4/src/What4/Expr/Builder.hs#L1401

whereas master hits the base case, likely because the "annotated" expression is (incorrectly) not recognized as a semiring sum:

https://github.com/GaloisInc/what4/blob/e46dff42096550d860d210bd9cf6e435d8cd7ce5/what4/src/What4/Expr/Builder.hs#L1425

Counter-intuitively, it appears that hitting the more specialized case results in a less-specific answer. Possibly, the WSum.addConstant code doesn't take abstract domains into account as carefully as WSum.addVars?

[langston-barrett]

I think this may have to do with the fact that the catch-all case calls this function:

https://github.com/GaloisInc/what4/blob/e46dff42096550d860d210bd9cf6e435d8cd7ce5/what4/src/What4/Expr/Builder.hs#L1213-L1220

whereas the more specific case calls sum' directly, bypassing WSum.asConstant. There are two possible solutions:

1. Call semiRingSum ranther than sum' in the (SR_Sum, SR_Constant) case. This could be beneficial to performance if this case is often reducible to a constant, or detrimental if it's not. I'm not sure why sum' is called directly, perhaps it's the assumption that it's not common.
2. Call WSum.asConstant in asBV. Again, this could possibly make a lot of other code faster or slower depending on how common the case of a constant-able sum appears.

[EDIT]: This does not appear to be the problem, adding semiRingSum to the above case doesn't fix the test case.

[langston-barrett]

It appears that WSum.addVars (in master/the base case) is hitting this case of sbMakeExpr

https://github.com/GaloisInc/what4/blob/e46dff42096550d860d210bd9cf6e435d8cd7ce5/what4/src/What4/Expr/Builder.hs#L589

whereas the result of WSum.addConstant (on this branch) hits the catch-all case:

https://github.com/GaloisInc/what4/blob/e46dff42096550d860d210bd9cf6e435d8cd7ce5/what4/src/What4/Expr/Builder.hs#L590

So I need to figure out why abstractEval treats these differently.

To be more specific, the question is why BVD.asSingleton returns Nothing for bvSum cx2B@1:bv cx2A@0:bv 0x1:[8] while it returns Just for bvSum annotation Nonce {indexValue = 3} (bvSum cx2B@1:bv cx2A@0:bv) 0x1:[8].

[langston-barrett]

To be more specific, the question is why BVD.asSingleton returns Nothing for bvSum cx2B@1:bv cx2A@0:bv 0x1:[8] while it returns Just for bvSum annotation Nonce {indexValue = 3} (bvSum cx2B@1:bv cx2A@0:bv) 0x1:[8].

FWIW,

         let e2C' = O.BVDArith (A.range w 2 2)
         let e2D = O.add e2C' (O.singleton w 1)
         case O.asSingleton e2D of
           Just bv -> pure () -- bv == mkBV w 3
           Nothing -> error "sad"

works just fine. Perhaps the abstract domain is getting lost when the binary bvAdd x2B x2A gets "lifted" into the ternary sum with 0x1, which (again, probably erroneously) doesn't happen when the binary sum is "hidden" under the annotation constructor?

[langston-barrett]

Okay, I've managed to whittle down the issue to a test case, reported here (as it happens on master, not just on this branch): https://github.com/GaloisInc/what4/issues/248