what4: Don't annotate {Nonce,}AppExprs

[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:

what4/what4/test/ExprBuilderSMTLib2.hs

Lines 1144 to 1160 in e46dff4

	-- Test unsafeSetAbstractValue on a compound symbolic expression
	testUnsafeSetAbstractValue2 :: TestTree
	testUnsafeSetAbstractValue2 = testCase "test unsafeSetAbstractValue2" $
	withSym FloatIEEERepr $ \sym -> do
	let w = knownNat @8
	e2A <- freshConstant sym (userSymbol' "x2A") (BaseBVRepr w)
	e2B <- freshConstant sym (userSymbol' "x2B") (BaseBVRepr w)
	e2C <- bvAdd sym e2A e2B
	(_, e2C') <- annotateTerm sym $ unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e2C
	unsignedBVBounds e2C' @?= Just (2, 2)
	e2D <- bvAdd sym e2C' =<< bvLit sym w (BV.one w)
	case asBV e2D of
	Just bv -> bv @?= BV.mkBV w 3
	Nothing -> assertFailure $ unlines
	[ "unsafeSetAbstractValue doesn't work as expected for a"
	, "compound symbolic expression"
	]

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:

what4/what4/src/What4/Expr/Builder.hs

Line 1401 in e46dff4

(SR_Sum xs, SR_Constant yc) ->

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

what4/what4/src/What4/Expr/Builder.hs

Line 1425 in e46dff4

_ -> semiRingSum sym (WSum.addVars sr x y)

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]

EDIT: Speculation that turned out to be false

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

what4/what4/src/What4/Expr/Builder.hs

Lines 1213 to 1220 in e46dff4

	semiRingSum ::
	ExprBuilder t st fs ->
	WeightedSum (Expr t) sr ->
	IO (Expr t (SR.SemiRingBase sr))
	semiRingSum sym s
	| Just c <- WSum.asConstant s = semiRingLit sym (WSum.sumRepr s) c
	| Just r <- WSum.asVar s = return r
	| otherwise = sum' sym s

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

what4/what4/src/What4/Expr/Builder.hs

Line 589 in e46dff4

BaseBVRepr w | Just x <- BVD.asSingleton v -> bvLit sym w (BV.mkBV w x)

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

what4/what4/src/What4/Expr/Builder.hs

Line 590 in e46dff4

_ -> appExpr s pc a v

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): #248

[langston-barrett]

Alright, I've worked around the issues with the abstract domains by introducing a new type of NonceExpr, namely Opaque, which is specifically designed to preserve abstract values. See the docs and CHANGELOG.

[langston-barrett]

I'm trying this out on a codebase that makes extensive use of annotations.

[RyanGlScott]

What part of the code ignores the subterms of Opaque? (It's not obvious to me at a glance where the magic actually happens.)

[langston-barrett]

Ah, it's just that the implementation of IsExprBuilder for ExprBuilder doesn't match on it and rewrite under it! That's the second part of the Haddock here.

[RyanGlScott]

Sorry, I must be missing something—where exactly does this happen in the IsExprBuilder instance for ExprBuilder?

[langston-barrett]

Sorry, I must be missing something—where exactly does this happen in the IsExprBuilder instance for ExprBuilder?

That's the thing haha: It doesn't happen. There are no pattern matches on Opaque, which is what makes it preserve the abstract values. It works just like Annotation did for this purpose.

[langston-barrett]

To give an example of what I'm talking about: #248 happens because bvAdd calls semiRingAdd, which performs some rewrites using pattern-matching like so:

what4/what4/src/What4/Expr/Builder.hs

Line 1798 in ebf9ac0

(SR_Constant c, _) | SR.eq sr c (SR.zero sr) -> return y

Specifically, that issue calls out this case as problematic:

what4/what4/src/What4/Expr/Builder.hs

Line 1806 in ebf9ac0

(SR_Sum xs, SR_Constant yc) ->

But note that none of those patterns would match if either x or y were Opaque, so the rewrite rules wouldn't fire, so the abstract domain would be preserved. This is how it works for Annotation on master.

[RyanGlScott]

But note that none of those patterns would match if either x or y were Opaque

I'm not sure how to typecheck this sentence, since x and y are Exprs, but Opaque is a NonceApp (as is Annotation). Surely Opaque wouldn't matter here?

[langston-barrett]

I'm not sure how to typecheck this sentence, since x and y are Exprs, but Opaque is a NonceApp (as is Annotation). Surely Opaque wouldn't matter here?

To be more precise: none of those patterns would match, because viewSemiRing applied to the NonceAppExpr containing the Opaque would yield SR_General, and not any of these more particular cases.

[RyanGlScott]

Thank you! This is the part that I was missing.

[RyanGlScott]

Suggested change

	-- be careful than subsequent operations do not widen away the value. As a
	-- be careful that subsequent operations do not widen away the value. As a

[RyanGlScott]

After reading these Haddocks, I'm a bit confused about the relationship between opacify and annotateTerm. Is the idea that annotateTerm should make no guarantees about inhibiting rewrites, as that should be the role of opacify? Or is the idea that annotateTerm should guarantee that rewrites are inhibited, and that the only reason it doesn't are due to bugs (e.g., #248)? If it's the latter, is opacify meant to be a short-term workaround until bugs like #248 are fixed?

[langston-barrett]

Is the idea that annotateTerm should make no guarantees about inhibiting rewrites, as that should be the role of opacify?

Exactly! annotateTerm was previously treated as if it made this guarantee, but I think it's better to have a separate constructor (Opaque) for that (which doesn't need to attach an extra Nonce, either).

Or is the idea that annotateTerm should guarantee that rewrites are inhibited, and that the only reason it doesn't are due to bugs (e.g., #248)?

The test case in that issue doesn't use annotateTerm, which is why the abstract value is discarded. annotateTerm does happen to prevent rewrites at the moment, but for the sake of the changes in this PR, I think we should abandon that.

If it's the latter, is opacify meant to be a short-term workaround until bugs like #248 are fixed?

Yes, it is a temporary workaround for that issue.

[RyanGlScott]

Yes, it is a temporary workaround for that issue.

I am confused. If annotateTerm is no longer meant to inhibit rewrites, then isn't opacify the only part of the API that serves this role? If so, I would expect opacify to be a stable part of the API, but your wording suggests that it isn't... I must be missing something.

[langston-barrett]

If annotateTerm is no longer meant to inhibit rewrites, then isn't opacify the only part of the API that serves this role?

Yes, opacify is meant to replace the use of annotateTerm for this purpose, because the primary changes in this MR (not attaching Annotation to {Nonce,}AppExprs) make annotateTerm no longer suitable for it (as demonstrated by the weird test case failures above).

If so, I would expect opacify to be a stable part of the API, but your wording suggests that it isn't... I must be missing something.

Well, the entire use of annotateTerm to preserve abstract values was a hack to work around #248 and issues like it - If all the rewrite rules preserved abstract values, there would be no need to hide terms under Annotation/Opaque to preserve their abstract values. This behavior was not documented as part of the intent of the annotation API. So IMO, this is replacing one temporary workaround with one that is better-documented and more efficient.

[RyanGlScott]

Well, the entire use of annotateTerm to preserve abstract values was a hack to work around #248 and issues like it - If all the rewrite rules preserved abstract values, there would be no need to hide terms under Annotation/Opaque to preserve their abstract values.

Ah, you had preserving abstract values in mind when you wrote your comments—I see. I think I agree that if everything preserved abstract values, then we'd no longer need Opaque, although it's hard to say for sure that there wouldn't be other use cases for Opaque. For instance, it's conceivable that there are SAW proof goals that are easier to prove when derived from certain what4 Expr shapes than others, and Opaque could be one possible mechanism to achieve this. (I don't have a concrete example of this in mind, but it doesn't seem totally outside of the realm of possibility.)

In that case, I think if we added some additional clarification to the annotateTerm Haddocks about what it does (and does not) guarantee, then I'd be content with this.

[RyanGlScott]

It would be helpful to specify what happens if you call clarify on a SymExpr that wasn't returned by a call to opacify.

[RyanGlScott]

Do you expect that these changes to how annotations work will have effects on downstream code? If so, is it worth advertising this in the changelog?

[langston-barrett]

Do you expect that these changes to how annotations work will have effects on downstream code? If so, is it worth advertising this in the changelog?

Yes, in that using annotateTerm to preserve abstract values won't work as well and code that wants to do that should use opacify instead - which is what I put in the changelog. I'm open to suggestions on wording to make this more clear!

[RyanGlScott]

OK. I think I have large SAW proofs in mind when I wrote #247 (comment) , as I worry that this could lead to subtle changes in proof goals that are hard to track down. If all that is required is to audit uses of annotateTerm and replace them with opacify, then perhaps this isn't too bad.

[langston-barrett]

I'm not familiar with how SAW uses annotations, so not sure I can be helpful there (apologies!)