Doc fixes

what4/src/What4/Expr/Builder.hs

@@ -4497,47 +4497,63 @@ instance IsSymExprBuilder (ExprBuilder t st fs) where
 
   freshBoundedBV sym nm w Nothing Nothing = freshConstant sym nm (BaseBVRepr w)
   freshBoundedBV sym nm w mlo mhi =
-    do v <- sbMakeBoundVar sym nm (BaseBVRepr w) UninterpVarKind (Just $! (BVD.range w lo hi))
+    do unless boundsOK (Ex.throwIO (InvalidRange (BaseBVRepr w) (fmap toInteger mlo) (fmap toInteger mhi)))
+       v <- sbMakeBoundVar sym nm (BaseBVRepr w) UninterpVarKind (Just $! (BVD.range w lo hi))
        updateVarBinding sym nm (VarSymbolBinding v)
        return $! BoundVarExpr v
    where
+   boundsOK = lo <= hi && minUnsigned w <= lo && hi <= maxUnsigned w
    lo = maybe (minUnsigned w) toInteger mlo
    hi = maybe (maxUnsigned w) toInteger mhi
 
   freshBoundedSBV sym nm w Nothing Nothing = freshConstant sym nm (BaseBVRepr w)
   freshBoundedSBV sym nm w mlo mhi =
-    do v <- sbMakeBoundVar sym nm (BaseBVRepr w) UninterpVarKind (Just $! (BVD.range w lo hi))
+    do unless boundsOK (Ex.throwIO (InvalidRange (BaseBVRepr w) mlo mhi))
+       v <- sbMakeBoundVar sym nm (BaseBVRepr w) UninterpVarKind (Just $! (BVD.range w lo hi))
        updateVarBinding sym nm (VarSymbolBinding v)
        return $! BoundVarExpr v
    where
+   boundsOK = lo <= hi && minSigned w <= lo && hi <= maxSigned w
    lo = fromMaybe (minSigned w) mlo
    hi = fromMaybe (maxSigned w) mhi
 
   freshBoundedInt sym nm mlo mhi =
-    do v <- sbMakeBoundVar sym nm BaseIntegerRepr UninterpVarKind (absVal mlo mhi)
+    do unless (boundsOK mlo mhi) (Ex.throwIO (InvalidRange BaseIntegerRepr mlo mhi))
+       v <- sbMakeBoundVar sym nm BaseIntegerRepr UninterpVarKind (absVal mlo mhi)
        updateVarBinding sym nm (VarSymbolBinding v)
        return $! BoundVarExpr v
    where
+   boundsOK (Just lo) (Just hi) = lo <= hi
+   boundsOK _ _ = True
+
    absVal Nothing Nothing = Nothing
    absVal (Just lo) Nothing = Just $! MultiRange (Inclusive lo) Unbounded
    absVal Nothing (Just hi) = Just $! MultiRange Unbounded (Inclusive hi)
    absVal (Just lo) (Just hi) = Just $! MultiRange (Inclusive lo) (Inclusive hi)
 
   freshBoundedReal sym nm mlo mhi =
-    do v <- sbMakeBoundVar sym nm BaseRealRepr UninterpVarKind (absVal mlo mhi)
+    do unless (boundsOK mlo mhi) (Ex.throwIO (InvalidRange BaseRealRepr mlo mhi))
+       v <- sbMakeBoundVar sym nm BaseRealRepr UninterpVarKind (absVal mlo mhi)
        updateVarBinding sym nm (VarSymbolBinding v)
        return $! BoundVarExpr v
    where
+   boundsOK (Just lo) (Just hi) = lo <= hi
+   boundsOK _ _ = True
+
    absVal Nothing Nothing = Nothing
    absVal (Just lo) Nothing = Just $! RAV (MultiRange (Inclusive lo) Unbounded) Nothing
    absVal Nothing (Just hi) = Just $! RAV (MultiRange Unbounded (Inclusive hi)) Nothing
    absVal (Just lo) (Just hi) = Just $! RAV (MultiRange (Inclusive lo) (Inclusive hi)) Nothing
 
   freshBoundedNat sym nm mlo mhi =
-    do v <- sbMakeBoundVar sym nm BaseNatRepr UninterpVarKind (absVal mlo mhi)
+    do unless (boundsOK mlo mhi) (Ex.throwIO (InvalidRange BaseNatRepr mlo mhi))
+       v <- sbMakeBoundVar sym nm BaseNatRepr UninterpVarKind (absVal mlo mhi)
        updateVarBinding sym nm (VarSymbolBinding v)
        return $! BoundVarExpr v
    where
+   boundsOK (Just lo) (Just hi) = lo <= hi
+   boundsOK _ _ = True
+
    absVal Nothing Nothing = Nothing
    absVal (Just lo) Nothing = Just $! natRange lo Unbounded
    absVal Nothing (Just hi) = Just $! natRange 0 (Inclusive hi)

what4/src/What4/Interface.hs

@@ -120,7 +120,7 @@ module What4.Interface
     -- * SymEncoder
   , SymEncoder(..)
 
-    -- * Utilitity combinators
+    -- * Utility combinators
     -- ** Boolean operations
   , backendPred
   , andAllOf
@@ -141,6 +141,9 @@ module What4.Interface
     -- ** Indexing
   , muxRange
 
+    -- * Exceptions
+  , InvalidRange(..)
+
     -- * Reexports
   , module Data.Parameterized.NatRepr
   , module What4.BaseTypes
@@ -159,7 +162,7 @@ module What4.Interface
 import Control.Monad.Fail( MonadFail )
 #endif
 
-import           Control.Exception (assert)
+import           Control.Exception (assert, Exception)
 import           Control.Lens
 import           Control.Monad
 import           Control.Monad.IO.Class
@@ -198,6 +201,7 @@ import           What4.Utils.StringLiteral
 ------------------------------------------------------------------------
 -- SymExpr names
 
+-- | Symbolic boolean values, AKA predicates.
 type Pred sym = SymExpr sym BaseBoolType
 
 -- | Symbolic natural numbers.
@@ -311,12 +315,15 @@ class HasAbsValue e => IsExpr e where
   -- upper and lower bounds as integers
   signedBVBounds :: (1 <= w) => e (BaseBVType w) -> Maybe (Integer, Integer)
 
+  -- | If this expression syntactically represents an "affine" form, return its components.
+  --   When @asAffineVar x = Just (c,r,o)@, then we have @x == c*r + o@.
   asAffineVar :: e tp -> Maybe (ConcreteVal tp, e tp, ConcreteVal tp)
 
   -- | Return the string value if this is a constant string
   asString :: e (BaseStringType si) -> Maybe (StringLiteral si)
   asString _ = Nothing
 
+  -- | Return the representation of the string info for a string-typed term.
   stringInfo :: e (BaseStringType si) -> StringInfoRepr si
   stringInfo e =
     case exprType e of
@@ -406,7 +413,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
   -- | Get the currently-installed solver log listener, if one has been installed.
   getSolverLogListener :: sym -> IO (Maybe (SolverEvent -> IO ()))
 
-  -- | Provide the given even to the currently installed
+  -- | Provide the given event to the currently installed
   --   solver log listener, if any.
   logSolverEvent :: sym -> SolverEvent -> IO ()
 
@@ -469,7 +476,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
   --   that can be used to maintain a connection with the given term.
   --   The 'SymAnnotation' is intended to be used as the key in a hash
   --   table or map to additional data can be maintained alongside the terms.
-  --   The returned 'SymExpr' has the same semantics as the arugmnent, but
+  --   The returned 'SymExpr' has the same semantics as the argument, but
   --   has embedded in it the 'SymAnnotation' value so that it can be used
   --   later during term traversals.
   --
@@ -598,7 +605,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
 
   -- | @intDiv x y@ computes the integer division of @x@ by @y@.  This division is
   --   interpreted the same way as the SMT-Lib integer theory, which states that
-  --   @div@ and @mod@ are the unique Eucledian division operations satisfying the
+  --   @div@ and @mod@ are the unique Euclidean division operations satisfying the
   --   following for all @y /= 0@:
   --
   --   * @x * (div x y) + (mod x y) == x@
@@ -1012,7 +1019,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
        return (ov, xy)
 
 
-  -- | Compute the carryless multiply of the two input bitvectors.
+  -- | Compute the carry-less multiply of the two input bitvectors.
   --   This operation is essentially the same as a standard multiply, except that
   --   the partial addends are simply XOR'd together instead of using a standard
   --   adder.  This operation is useful for computing on GF(2^n) polynomials.
@@ -1349,13 +1356,13 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
   -- | Round a real number to an integer.
   --
   -- Numbers are rounded to the nearest integer, with rounding away from
-  -- zero when two integers are equi-distant (e.g., 1.5 rounds to 2).
+  -- zero when two integers are equidistant (e.g., 1.5 rounds to 2).
   realRound :: sym -> SymReal sym -> IO (SymInteger sym)
 
   -- | Round a real number to an integer.
   --
-  -- Numbers are rounded to the neareset integer, with rounding toward
-  -- even values when two integers are equi-distant (e.g., 2.5 rounds to 2).
+  -- Numbers are rounded to the nearest integer, with rounding toward
+  -- even values when two integers are equidistant (e.g., 2.5 rounds to 2).
   realRoundEven :: sym -> SymReal sym -> IO (SymInteger sym)
 
   -- | Round down to the nearest integer that is at most this value.
@@ -1375,6 +1382,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
   --   whose value (signed or unsigned) is congruent to the input integer, modulo @2^w@.
   --
   --   This operation has the following properties:
+  --
   --   *  @bvToInteger (integerToBv x w) == mod x (2^w)@
   --   *  @bvToInteger (integerToBV x w) == x@     when @0 <= x < 2^w@.
   --   *  @sbvToInteger (integerToBV x w) == mod (x + 2^(w-1)) (2^w) - 2^(w-1)@
@@ -1405,7 +1413,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
   -- | Convert a real number to an unsigned bitvector.
   --
   -- Numbers are rounded to the nearest representable number, with rounding away from
-  -- zero when two integers are equi-distant (e.g., 1.5 rounds to 2).
+  -- zero when two integers are equidistant (e.g., 1.5 rounds to 2).
   -- When the real is negative the result is zero.
   realToBV :: (1 <= w) => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
   realToBV sym r w = do
@@ -1415,7 +1423,7 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
   -- | Convert a real number to a signed bitvector.
   --
   -- Numbers are rounded to the nearest representable number, with rounding away from
-  -- zero when two integers are equi-distant (e.g., 1.5 rounds to 2).
+  -- zero when two integers are equidistant (e.g., 1.5 rounds to 2).
   realToSBV  :: (1 <= w) => sym -> SymReal sym -> NatRepr w -> IO (SymBV sym w)
   realToSBV sym r w  = do
     i <- realRound sym r
@@ -1919,21 +1927,21 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
   -- | Test if a floating-point value is (positive or negative) infinity.
   floatIsInf :: sym -> SymFloat sym fpp -> IO (Pred sym)
 
-  -- | Test if a floaint-point value is (positive or negative) zero.
+  -- | Test if a floating-point value is (positive or negative) zero.
   floatIsZero :: sym -> SymFloat sym fpp -> IO (Pred sym)
 
-  -- | Test if a floaint-point value is positive.  NOTE!
+  -- | Test if a floating-point value is positive.  NOTE!
   --   NaN is considered neither positive nor negative.
   floatIsPos :: sym -> SymFloat sym fpp -> IO (Pred sym)
 
-  -- | Test if a floaint-point value is negative.  NOTE!
+  -- | Test if a floating-point value is negative.  NOTE!
   --   NaN is considered neither positive nor negative.
   floatIsNeg :: sym -> SymFloat sym fpp -> IO (Pred sym)
 
-  -- | Test if a floaint-point value is subnormal.
+  -- | Test if a floating-point value is subnormal.
   floatIsSubnorm :: sym -> SymFloat sym fpp -> IO (Pred sym)
 
-  -- | Test if a floaint-point value is normal.
+  -- | Test if a floating-point value is normal.
   floatIsNorm :: sym -> SymFloat sym fpp -> IO (Pred sym)
 
   -- | If-then-else on floating point numbers.
@@ -2271,7 +2279,9 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym)
 -- apply this newtype.
 newtype SymBV' sym w = MkSymBV' (SymBV sym w)
 
--- | Join a @Vector@ of smaller bitvectors.
+-- | Join a @Vector@ of smaller bitvectors.  The vector is
+--   interpreted in big endian order; that is, with most
+--   significant bitvector first.
 bvJoinVector :: forall sym n w. (1 <= w, IsExprBuilder sym)
              => sym
              -> NatRepr w
@@ -2287,6 +2297,8 @@ bvJoinVector sym w =
         bvConcat' _ (MkSymBV' x) (MkSymBV' y) = MkSymBV' <$> bvConcat sym x y
 
 -- | Split a bitvector to a @Vector@ of smaller bitvectors.
+--   The returned vector is in big endian order; that is, with most
+--   significant bitvector first.
 bvSplitVector :: forall sym n w. (IsExprBuilder sym, 1 <= w, 1 <= n)
               => sym
               -> NatRepr n
@@ -2349,6 +2361,12 @@ indexLit :: IsExprBuilder sym => sym -> IndexLit idx -> IO (SymExpr sym idx)
 indexLit sym (NatIndexLit i)  = natLit sym i
 indexLit sym (BVIndexLit w v) = bvLit sym w v
 
+-- | A utility combinator for combining actions
+--   that build terms with if/then/else.
+--   If the given predicate is concretely true or
+--   false only the corresponding "then" or "else"
+--   action is run; otherwise both actions are run
+--   and combined with the given "ite" action.
 iteM :: IsExprBuilder sym
         => (sym -> Pred sym -> v -> v -> IO v)
         -> sym -> Pred sym -> IO v -> IO v -> IO v
@@ -2386,11 +2404,32 @@ data UnfoldPolicy
       --   arguments are concrete.
  deriving (Eq, Ord, Show)
 
+-- | Evaluates an @UnfoldPolicy@ on a collection of arguments.
 shouldUnfold :: IsExpr e => UnfoldPolicy -> Ctx.Assignment e args -> Bool
 shouldUnfold AlwaysUnfold _ = True
 shouldUnfold NeverUnfold _ = False
 shouldUnfold UnfoldConcrete args = allFC baseIsConcrete args
 
+
+-- | This exception is thrown if the user requests to make a bounded variable,
+--   but gives incoherent or out-of-range bounds.
+data InvalidRange where
+  InvalidRange ::
+    BaseTypeRepr bt ->
+    Maybe (ConcreteValue bt) ->
+    Maybe (ConcreteValue bt) ->
+    InvalidRange
+
+instance Exception InvalidRange
+instance Show InvalidRange where
+  show (InvalidRange bt mlo mhi) =
+    case bt of
+      BaseNatRepr     -> unwords ["invalid natural range", show mlo, show mhi]
+      BaseIntegerRepr -> unwords ["invalid integer range", show mlo, show mhi]
+      BaseRealRepr    -> unwords ["invalid real range", show mlo, show mhi]
+      BaseBVRepr w    -> unwords ["invalid bitvector range", show w ++ "-bit", show mlo, show mhi]
+      _               -> unwords ["invalid range for type", show bt]
+
 -- | This extends the interface for building expressions with operations
 --   for creating new symbolic constants and functions.
 class ( IsExprBuilder sym
@@ -2407,25 +2446,57 @@ class ( IsExprBuilder sym
   -- | Create a fresh latch variable.
   freshLatch    :: sym -> SolverSymbol -> BaseTypeRepr tp -> IO (SymExpr sym tp)
 
-  -- | Create a fresh bitvector value with optional upper and lower bounds (which bound the
-  --   unsigned value of the bitvector).
-  freshBoundedBV :: (1 <= w) => sym -> SolverSymbol -> NatRepr w -> Maybe Natural -> Maybe Natural -> IO (SymBV sym w)
+  -- | Create a fresh bitvector value with optional lower and upper bounds (which bound the
+  --   unsigned value of the bitvector). If provided, the bounds are inclusive.
+  --   If inconsistent or out-of-range bounds are given, an @InvalidRange@ exception will be thrown.
+  freshBoundedBV :: (1 <= w) =>
+    sym ->
+    SolverSymbol ->
+    NatRepr w ->
+    Maybe Natural {- ^ lower bound -} ->
+    Maybe Natural {- ^ upper bound -} ->
+    IO (SymBV sym w)
 
-  -- | Create a fresh bitvector value with optional upper and lower bounds (which bound the
-  --   signed value of the bitvector)
-  freshBoundedSBV :: (1 <= w) => sym -> SolverSymbol -> NatRepr w -> Maybe Integer -> Maybe Integer -> IO (SymBV sym w)
+  -- | Create a fresh bitvector value with optional lower and upper bounds (which bound the
+  --   signed value of the bitvector).  If provided, the bounds are inclusive.
+  --   If inconsistent or out-of-range bounds are given, an InvalidRange exception will be thrown.
+  freshBoundedSBV :: (1 <= w) =>
+    sym ->
+    SolverSymbol ->
+    NatRepr w ->
+    Maybe Integer {- ^ lower bound -} ->
+    Maybe Integer {- ^ upper bound -} ->
+    IO (SymBV sym w)
 
-  -- | Create a fresh natural number constant with optional upper and lower bounds.
+  -- | Create a fresh natural number constant with optional lower and upper bounds.
   --   If provided, the bounds are inclusive.
-  freshBoundedNat :: sym -> SolverSymbol -> Maybe Natural -> Maybe Natural -> IO (SymNat sym)
+  --   If inconsistent bounds are given, an InvalidRange exception will be thrown.
+  freshBoundedNat ::
+    sym ->
+    SolverSymbol ->
+    Maybe Natural {- ^ lower bound -} ->
+    Maybe Natural {- ^ upper bound -} ->
+    IO (SymNat sym)
 
-  -- | Create a fresh integer constant with optional upper and lower bounds.
+  -- | Create a fresh integer constant with optional lower and upper bounds.
   --   If provided, the bounds are inclusive.
-  freshBoundedInt :: sym -> SolverSymbol -> Maybe Integer -> Maybe Integer -> IO (SymInteger sym)
+  --   If inconsistent bounds are given, an InvalidRange exception will be thrown.
+  freshBoundedInt ::
+    sym ->
+    SolverSymbol ->
+    Maybe Integer {- ^ lower bound -} ->
+    Maybe Integer {- ^ upper bound -} ->
+    IO (SymInteger sym)
 
-  -- | Create a fresh real constant with optional upper and lower bounds.
+  -- | Create a fresh real constant with optional lower and upper bounds.
   --   If provided, the bounds are inclusive.
-  freshBoundedReal :: sym -> SolverSymbol -> Maybe Rational -> Maybe Rational -> IO (SymReal sym)
+  --   If inconsistent bounds are given, an InvalidRange exception will be thrown.
+  freshBoundedReal ::
+    sym ->
+    SolverSymbol ->
+    Maybe Rational {- ^ lower bound -} ->
+    Maybe Rational {- ^ upper bound -} ->
+    IO (SymReal sym)
 
 
   ----------------------------------------------------------------------
@@ -2441,14 +2512,14 @@ class ( IsExprBuilder sym
   -- | Return an expression that references the bound variable.
   varExpr :: sym -> BoundVar sym tp -> SymExpr sym tp
 
-  -- | @forallPred sym v e@ returns an expression that repesents @forall v . e@.
+  -- | @forallPred sym v e@ returns an expression that represents @forall v . e@.
   -- Throws a user error if bound var has already been used in a quantifier.
   forallPred :: sym
              -> BoundVar sym tp
              -> Pred sym
              -> IO (Pred sym)
 
-  -- | @existsPred sym v e@ returns an expression that repesents @exists v . e@.
+  -- | @existsPred sym v e@ returns an expression that represents @exists v . e@.
   -- Throws a user error if bound var has already been used in a quantifier.
   existsPred :: sym
              -> BoundVar sym tp
@@ -2539,6 +2610,11 @@ baseIsConcrete x =
         Just x' -> baseIsConcrete x'
         Nothing -> False
 
+-- | Return some default value for each base type.
+--   For numeric types, this is 0; for booleans, false;
+--   for strings, the empty string.  Structs are
+--   filled with default values for every field,
+--   default arrays are constant arrays of default values.
 baseDefaultValue :: forall sym bt
                   . IsExprBuilder sym
                  => sym

what4/src/What4/Protocol/SMTWriter.hs

@@ -114,7 +114,6 @@ import qualified Data.BitVector.Sized as BV
 import           Data.ByteString (ByteString)
 import           Data.IORef
 import           Data.Kind
-import           Data.List (last)
 import           Data.List.NonEmpty (NonEmpty(..))
 import           Data.Maybe
 import           Data.Parameterized.Classes (ShowF(..))