Abstract values are not preserved by certain calls to bvAdd

[langston-barrett]

This test fails, when it should succeed:

-- Test unsafeSetAbstractValue on ranges
testUnsafeSetAbstractValue3 :: TestTree
testUnsafeSetAbstractValue3 = testCase "test unsafeSetAbstractValue3" $
  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
    let e2C' = unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 3)) e2C
    e2D <- bvAdd sym e2C' =<< bvLit sym w (BV.one w)
    unsignedBVBounds e2D @?= Just (3, 4)

Tests
  test unsafeSetAbstractValue3: FAIL
    test/ExprBuilderSMTLib2.hs:1172:
    expected: Just (3,4)
     but got: Just (0,255)

There's something wrong with this case in semiRingAdd:

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

Line 1401 in e46dff4

(SR_Sum xs, SR_Constant yc) ->

Note that this doesn't occur if you assign abstract values individually to x2A and x2B.

[langston-barrett]

My guess is that the problem here is that the abstract value is stored on the AppExpr holding the bvAdd (i.e., WeightedSum), rather than inside it. semiRingAdd then modifies the underlying WeightedSum (adding a constant/scalar offset) and calls sbMakeExpr, which uses abstractEval on the new WeightedSum. However, abstractEval doesn't have access to the original abstract value, which has been thrown away.

[langston-barrett]

Indeed, this diff fixes this particular test case. We should think about how to more carefully preserve abstract values for the rest of semiRingAdd, and probably for semiRingMul and many other functions. It would also be good to try and come up with some kind of testing regimen which tests for the preservation of abstract values.

diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
index 258562c9..827d7071 100644
--- a/what4/src/What4/Expr/Builder.hs
+++ b/what4/src/What4/Expr/Builder.hs
@@ -576,9 +576,17 @@ semiRingLit sb sr x = do
 
 sbMakeExpr :: ExprBuilder t st fs -> App (Expr t) tp -> IO (Expr t tp)
 sbMakeExpr sym a = do
+  let v = abstractEval exprAbsValue a
+  sbMakeExprWithAbs sym a v
+
+sbMakeExprWithAbs ::
+  ExprBuilder t st fs ->
+  App (Expr t) tp ->
+  AbstractValue tp ->
+  IO (Expr t tp)
+sbMakeExprWithAbs sym a v = do
   s <- readIORef (sbCurAllocator sym)
   pc <- curProgramLoc sym
-  let v = abstractEval exprAbsValue a
   when (isNonLinearApp a) $
     atomicModifyIORef' (sbNonLinearOps sym) (\n -> (n+1,()))
   case appType a of
@@ -1226,6 +1234,14 @@ sum' ::
 sum' sym s = sbMakeExpr sym $ SemiRingSum s
 {-# INLINE sum' #-}
 
+sumWithAbs ::
+  ExprBuilder t st fs ->
+  WeightedSum (Expr t) sr ->
+  AbstractValue (SR.SemiRingBase sr) ->
+  IO (Expr t (SR.SemiRingBase sr))
+sumWithAbs sym s = sbMakeExprWithAbs sym $ SemiRingSum s
+{-# INLINE sumWithAbs #-}
+
 scalarMul ::
    ExprBuilder t st fs ->
    SR.SemiRingRepr sr ->
@@ -1399,7 +1415,9 @@ semiRingAdd sym sr x y =
       (SR_Constant xc, SR_Sum ys) ->
         sum' sym (WSum.addConstant sr ys xc)
       (SR_Sum xs, SR_Constant yc) ->
-        sum' sym (WSum.addConstant sr xs yc)
+        case abs of
+          Just a -> sumWithAbs sym (WSum.addConstant sr xs yc) a
+          Nothing -> sum' sym (WSum.addConstant sr xs yc)
 
       (SR_Constant xc, _)
         | Just (BaseIte _ _ cond a b) <- asApp y
@@ -1427,6 +1445,15 @@ semiRingAdd sym sr x y =
         isConstantSemiRingExpr (viewSemiRing sr -> SR_Constant _) = True
         isConstantSemiRingExpr _ = False
 
+        absx = getAbsValue x
+        absy = getAbsValue y
+        abs :: Maybe (AbstractValue (SR.SemiRingBase sr))
+        abs =
+          case sr of
+            SR.SemiRingIntegerRepr -> Nothing
+            SR.SemiRingRealRepr    -> Nothing
+            SR.SemiRingBVRepr fv w -> Just $ BVD.add absx absy
+
 semiRingMul ::
   ExprBuilder t st fs ->
   SR.SemiRingRepr sr ->

[RyanGlScott]

Good catch. My experience with abstract domains is that they are somewhat fragile for reasons like this, and one usually needs to annotate an expression if you want to have any reasonable guarantees that the abstract domain will be preserved. (See also #40, which is about a proposed refactoring to make issues like this one easier to spot.) Of course, we should strive to do better, and if there are simple ways to improve things, we should do it. We have a long way to go in order to cover every what4 operation, however.