fix assertPred and make its code more uniform

This is a fix for #424.  The primary fix consists in splitting the logic
for equality tests based on the value of `isTrue`.  I have separated it
as its own function as it's needed for two branches, and Haskell lacks
binding or-patterns.

Along the way, I have made the code for `assertPred` better documented,
and much more uniform.  This should make it easier to spot bugs and
understand the overall logic.

base/src/Data/Macaw/AbsDomain/JumpBounds.hs

@@ -661,6 +661,45 @@ addRangePred cns v p =
         _ ->
           Right $ branchAssignRangePred n p
 
+-- | @assertEqPred cns x w c isTrue@ asserts equality @x = BVValue c w@ is either true, or false,
+-- based on `isTrue`.
+assertEqPred ::
+  ( OrdF (ArchReg arch)
+  , HasRepr (ArchReg arch) TypeRepr
+  , MemWidth (ArchAddrWidth arch)
+  , ShowF (ArchReg arch)
+  ) =>
+  -- | Constraints that let us evaluate `x`
+  BlockIntraStackConstraints arch ids ->
+  -- | Value to be constrained
+  Value arch ids (BVType w) ->
+  -- | Bitsize of bitvector c
+  NatRepr w ->
+  -- | Numeric constant x should be equal/different to
+  Integer ->
+  -- | `True` if we should assert equality, `False` if we should assert non-equality
+  Bool ->
+  Either String (BranchConstraints arch ids)
+assertEqPred cns x w c isTrue
+  | isTrue =
+    addRangePred cns (intraStackValueExpr cns x)
+                     (mkRangeBound w (fromInteger c) (fromInteger c))
+  | otherwise = do
+    -- x /= c becomes:
+    --                   (x >= c + 1)   when c == 0
+    --   (x <= c - 1) \/ (x >= c + 1)   otherwise
+    -- because ranges use natural numbers and are inclusive on both ends.
+    if c == 0
+      then
+        addRangePred cns (intraStackValueExpr cns x)
+                         (mkLowerBound w (fromInteger (c + 1)))
+      else
+        disjoinBranchConstraints
+          <$> addRangePred cns (intraStackValueExpr cns x)
+                               (mkUpperBound w (fromInteger (c - 1)))
+          <*> addRangePred cns (intraStackValueExpr cns x)
+                               (mkLowerBound w (fromInteger (c + 1)))
+
 -- | Assert a predicate is true/false and update bounds.
 --
 -- If it returns a new upper bounds, then that may be used.
@@ -678,72 +717,71 @@ assertPred :: ( OrdF (ArchReg arch)
 assertPred bnds (AssignedValue a) isTrue = do
   let cns = intraStackConstraints bnds
   case assignRhs a of
-    EvalApp (Eq x (BVValue w c)) -> do
-      addRangePred cns (intraStackValueExpr cns x)
-                       (mkRangeBound w (fromInteger c) (fromInteger c))
-    EvalApp (Eq (BVValue w c) x) -> do
-      addRangePred cns (intraStackValueExpr cns x)
-                   (mkRangeBound w (fromInteger c) (fromInteger c))
-    -- Given x < c), assert x <= c-1
-    EvalApp (BVUnsignedLt x (BVValue _ c)) -> do
-      if isTrue then do
+    EvalApp (Eq x (BVValue w c)) -> assertEqPred cns x w c isTrue
+    EvalApp (Eq (BVValue w c) x) -> assertEqPred cns x w c isTrue
+    EvalApp (BVUnsignedLt x (BVValue w c))
+      | isTrue -> do
+        -- x < c becomes x <= c - 1, unless c == 0
         when (c == 0) $ Left "x < 0 must be false."
         addRangePred cns (intraStackValueExpr cns x)  $!
-          mkUpperBound (typeWidth x) (fromInteger (c-1))
-       else do
+          mkUpperBound w (fromInteger (c-1))
+      | otherwise ->
+        -- !(x < c) becomes c <= x
         addRangePred cns (intraStackValueExpr cns x)  $!
-          mkLowerBound (typeWidth x) (fromInteger c)
-    -- Given not (c < y), assert y <= c
-    EvalApp (BVUnsignedLt (BVValue w c) y) -> do
-      p <-
-        if isTrue then do
-          when (c >= maxUnsigned w) $  Left "x <= max_unsigned must be true"
-          pure $! mkLowerBound w (fromInteger (c+1))
-         else do
-          pure $! mkUpperBound w (fromInteger c)
-      addRangePred cns (intraStackValueExpr cns y) p
-    -- Given x <= c, assert x <= c
-    EvalApp (BVUnsignedLe x (BVValue w c)) -> do
-      p <-
-        if isTrue then
-          pure $! mkUpperBound w (fromInteger c)
-         else do
-          when (c >= maxUnsigned w) $  Left "x <= max_unsigned must be true"
-          pure $! mkLowerBound w (fromInteger (c+1))
-      addRangePred cns (intraStackValueExpr cns x) p
-    -- Given not (c <= y), assert y <= (c-1)
-    EvalApp (BVUnsignedLe (BVValue _ c) y)
+          mkLowerBound w (fromInteger c)
+    EvalApp (BVUnsignedLt (BVValue w c) y)
+      | isTrue -> do
+        -- c < y becomes c + 1 <= y, unless c == max
+        when (c >= maxUnsigned w) $ Left "x <= max_unsigned must be true"
+        addRangePred cns (intraStackValueExpr cns y)
+          $! mkLowerBound w (fromInteger (c+1))
+      | otherwise -> do
+        -- !(c < y) becomes y <= c
+        addRangePred cns (intraStackValueExpr cns y)
+          $! mkUpperBound w (fromInteger c)
+    EvalApp (BVUnsignedLe x (BVValue w c))
       | isTrue -> do
-          addRangePred cns (intraStackValueExpr cns y)
-                       (mkLowerBound (typeWidth y) (fromInteger c))
+        -- x <= c becomes x <= c
+        addRangePred cns (intraStackValueExpr cns x)
+          $! mkUpperBound w (fromInteger c)
       | otherwise -> do
-          when (c == 0) $ Left "0 <= x cannot be false"
-          addRangePred cns
-            (intraStackValueExpr cns y)
-            (mkUpperBound (typeWidth y) (fromInteger (c-1)))
-    EvalApp (AndApp l r) ->
-      if isTrue then
+        -- !(x <= c) becomes c + 1 <= x, unless c == max
+        when (c >= maxUnsigned w) $ Left "x <= max_unsigned must be true"
+        addRangePred cns (intraStackValueExpr cns x)
+          $! mkLowerBound w (fromInteger (c+1))
+    EvalApp (BVUnsignedLe (BVValue w c) y)
+      | isTrue -> do
+        -- c <= y becomes c <= y
+        addRangePred cns (intraStackValueExpr cns y)
+                         (mkLowerBound w (fromInteger c))
+      | otherwise -> do
+        -- !(c <= y) becomes y <= c - 1, unless c == 0
+        when (c == 0) $ Left "0 <= x cannot be false"
+        addRangePred cns (intraStackValueExpr cns y)
+                         (mkUpperBound w (fromInteger (c-1)))
+    EvalApp (AndApp l r)
+      | isTrue ->
+        -- l && r becomes l && r
         conjoinBranchConstraints
           <$> assertPred bnds l True
           <*> assertPred bnds r True
-      else
+      | otherwise ->
+        -- !(l && r) becomes !l || !r
         disjoinBranchConstraints
           <$> assertPred bnds l False
           <*> assertPred bnds r False
-    -- Given not (x || y), assert not x, then assert not y
-    EvalApp (OrApp  l r) ->
-      if isTrue then
-        -- Assert l | r
+    EvalApp (OrApp  l r)
+      | isTrue ->
+        -- l || r becomes l || r
         disjoinBranchConstraints
           <$> assertPred bnds l True
           <*> assertPred bnds r True
-      else
-        -- Assert not l && not r
+      | otherwise ->
+        -- !(l || r) becomes !l && !r
         conjoinBranchConstraints
           <$> assertPred bnds l False
           <*> assertPred bnds r False
-    EvalApp (NotApp p) ->
-      assertPred bnds p (not isTrue)
+    EvalApp (NotApp p) -> assertPred bnds p (not isTrue)
     _ -> Right emptyBranchConstraints
 assertPred _ _ _ =
   Right emptyBranchConstraints