Address code review comments, typos, improve documentation.

what4/CHANGES.md

@@ -1,9 +1,19 @@
 # next (TBA)
 
 * Add operations for increased control over the scope of
-  configuration options, both in the `What4.Confg` and
+  configuration options, both in the `What4.Config` and
   `What4.Expr.Builder` modules.
 
+* Previously, the `exprCounter`, `sbUserState`, `sbUnaryThreshold`, and
+  `sbCacheStartSize` fields of `ExprBuilder` were directly exposed; in
+  principle this allows users to modify them, which was not intended
+  in some cases.  These have been uniformly renamed to remove the `sb`
+  prefix, and exposed as `Getter` or `Lens` values instead, as
+  appropriate.
+
+* The `sbBVDomainRangeLimit` fields of `ExprBuilder` was obsolete and
+  has been removed.
+
 * Allow building with `hashable-1.4.*`:
   * Add `Eq` instances for all data types with `Hashable` instances that
     were missing corresponding `Eq` instances. This is required since

what4/src/What4/Config.hs

@@ -907,7 +907,7 @@ instance Show OptCreateFailure where
 ------------------------------------------------------------------------
 -- Config
 
--- | The main configuration datatype.  It consists of an Read/Write var
+-- | The main configuration datatype.  It consists of a Read/Write var
 --   containing the actual configuration data.
 newtype Config = Config (RWV.RWVar ConfigMap)
 
@@ -939,12 +939,12 @@ tryExtendConfig ts (Config cfg) =
 
 -- | Create a new configuration object that shares the option
 --   settings currently in the given input config. However,
---   an options added to either configuration using @extendConfig@
---   will not be propigated to the other .
+--   any options added to either configuration using @extendConfig@
+--   will not be propagated to the other.
 --
---   To restate, option settings that already exist in the
---   input configuration will be shared between both; changes
---   to those options will be visible in both configurations.
+--   Option settings that already exist in the input configuration
+--   will be shared between both; changes to those options will be
+--   visible in both configurations.
 splitConfig :: Config -> IO Config
 splitConfig (Config cfg) = Config <$> (RWV.with cfg RWV.new)
 

what4/src/What4/Expr/Allocator.hs

@@ -37,13 +37,14 @@ import           What4.Utils.AbstractDomains
 -- Cache start size
 
 -- | Starting size for element cache when caching is enabled.
+--   The default value is 100000 elements.
 --
 --   This option is named \"backend.cache_start_size\"
 cacheStartSizeOption :: ConfigOption BaseIntegerType
 cacheStartSizeOption = configOption BaseIntegerRepr "backend.cache_start_size"
 
 -- | The configuration option for setting the size of the initial hash set
--- used by simple builder
+--   used by simple builder (measured in number of elements).
 cacheStartSizeDesc :: ConfigDesc
 cacheStartSizeDesc = mkOpt cacheStartSizeOption sty help (Just (ConcreteInteger 100000))
   where sty = integerWithMinOptSty (CFG.Inclusive 0)
@@ -54,6 +55,9 @@ cacheStartSizeDesc = mkOpt cacheStartSizeOption sty help (Just (ConcreteInteger
 
 -- | Indicates if we should cache terms.  When enabled, hash-consing
 --   is used to find and deduplicate common subexpressions.
+--   Toggling this option from disabled to enabled will allocate a new
+--   hash table; toggling it from enabled to disabled will discard
+--   the current hash table.  The default value for this option is `False`.
 --
 --   This option is named \"use_cache\"
 cacheTerms :: ConfigOption BaseBoolType
@@ -163,7 +167,7 @@ cachedNonceExpr g h pc p v = do
                                             , nonceExprAbsValue = v
                                             }
       seq e $ stToIO $ PH.insert h p e
-      return $! e
+      return e
 
 
 cachedAppExpr :: forall t tp

what4/src/What4/Expr/Builder.hs

@@ -17,7 +17,8 @@ module are modified or written atomically, so modifications should
 propagate in the expected sequentially-consistent ways.  Of course,
 threads may still clobber state others have set (e.g., the current
 program location) so the potential for truly multithreaded use is
-somewhat limited.
+somewhat limited.  Consider the @exprBuilderFreshConfig@ or
+@exprBuilderSplitConfig@ operations if this is a concern.
 -}
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE BangPatterns #-}
@@ -398,7 +399,7 @@ unaryThreshold = to sbUnaryThreshold
 cacheStartSize :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseIntegerType)
 cacheStartSize = to sbCacheStartSize
 
--- | Return a new expr builder where the configuaration object has
+-- | Return a new expr builder where the configuration object has
 --   been "split" using the @splitConfig@ operation.
 --   The returned sym will share any preexisting options with the
 --   input sym, but any new options added with @extendConfig@

what4/src/What4/FloatMode.hs

@@ -1,11 +1,14 @@
 -----------------------------------------------------------------------
 -- |
 -- Module           : What4.FloatMode
--- Description      : 
+-- Description      : Mode values for controlling the "interpreted" floating point mode.
 -- Copyright        : (c) Galois, Inc 2014-2022
 -- License          : BSD3
 -- Maintainer       : [email protected]
 -- Stability        : provisional
+--
+-- Desired instances for the @IsInterpretedFloatExprBuilder@ class are selected
+-- via the different mode values from this module.
 ------------------------------------------------------------------------
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -34,8 +37,20 @@ data FloatMode where
   FloatIEEE :: FloatMode
   FloatUninterpreted :: FloatMode
   FloatReal :: FloatMode
+
+-- | In this mode "interpreted" floating-point values are treated
+--   as bit-precise IEEE-754 floats.
 type FloatIEEE = 'FloatIEEE
+
+-- | In this mode "interpreted" floating-point values are treated
+--   as bitvectors of the appropriate width, and all operations on
+--   them are translated as uninterpreted functions.
 type FloatUninterpreted = 'FloatUninterpreted
+
+-- | In this mode "interpreted" floating-point values are treated
+--   as real-number values, to the extent possible. Expressions that
+--   would result in infinities or NaN will yield unspecified values in
+--   this mode, or directly produce runtime errors.
 type FloatReal = 'FloatReal
 
 data FloatModeRepr :: FloatMode -> Type where