Various metadata updates.

* Update/imporove Haddock comments and bump copyright years * Bump copyright dates in LICENSE files * Add .cabal package lower bounds. These appear to be reasonable, but I haven't exhaustively tested the various configurations. * Bump copyright dates in .cabal files * Start a basic changelog
2024-11-25 07:13:59 +03:00 · 2020-07-14 17:32:41 -07:00 · 2020-07-14 17:32:41 -07:00 · 2fe09d5fd9
commit 2fe09d5fd9
parent 96e8a439fc
66 changed files with 222 additions and 109 deletions
--- a/what4-abc/LICENSE
+++ b/what4-abc/LICENSE
@ -1,4 +1,4 @@
-Copyright (c) 2013-2018 Galois Inc.
+Copyright (c) 2013-2020 Galois Inc.
 All rights reserved.

 Redistribution and use in source and binary forms, with or without
--- a/what4-abc/what4-abc.cabal
+++ b/what4-abc/what4-abc.cabal
@ -2,7 +2,7 @@ Name:          what4-abc
 Version:       0.1
 Author:        Galois Inc.
 Maintainer:    jhendrix@galois.com
-Copyright:     (c) Galois, Inc 2014-2018
+Copyright:     (c) Galois, Inc 2014-2020
 License:       BSD3
 License-file:  LICENSE
 Build-type:    Simple
@ -41,4 +41,4 @@ library
    What4.Solver.ABC

  ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
-  ghc-prof-options: -O2 -fprof-auto-top
+  ghc-prof-options: -fprof-auto-top
--- a/what4-blt/LICENSE
+++ b/what4-blt/LICENSE
@ -1,4 +1,4 @@
-Copyright (c) 2013-2018 Galois Inc.
+Copyright (c) 2013-2020 Galois Inc.
 All rights reserved.

 Redistribution and use in source and binary forms, with or without
--- a/what4-blt/what4-blt.cabal
+++ b/what4-blt/what4-blt.cabal
@ -2,6 +2,7 @@ Name:          what4-blt
 Version:       0.2
 Author:        Galois Inc.
 Maintainer:    rdockins@galois.com
+Copyright:     (c) Galois, Inc 2014-2020
 License:       BSD3
 License-file:  LICENSE
 Build-type:    Simple
@ -32,7 +33,7 @@ library
    What4.Solver.BLT

  ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
-  ghc-prof-options: -O2 -fprof-auto-top
+  ghc-prof-options: -fprof-auto-top

  default-language: Haskell2010

@ -41,7 +42,6 @@ test-suite test
  hs-source-dirs: test

  ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
-  ghc-prof-options: -fprof-auto -O2

  main-is: Test.hs

--- a/what4/CHANGES.md
+++ b/what4/CHANGES.md
@ -0,0 +1,3 @@
+# 1.0 (July 2020)
+
+* Initial Hackage release
--- a/what4/LICENSE
+++ b/what4/LICENSE
@ -1,4 +1,4 @@
-Copyright (c) 2013-2018 Galois Inc.
+Copyright (c) 2013-2020 Galois Inc.
 All rights reserved.

 Redistribution and use in source and binary forms, with or without
--- a/what4/src/Test/Verification.hs
+++ b/what4/src/Test/Verification.hs
@ -2,8 +2,9 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE RankNTypes #-}

-{-
+{- |
 Module      : Test.Verification
+Description : Testing abstraction layer
 Copyright   : (c) Galois Inc, 2020
 License     : BSD3
 Maintainer  : kquick@galois.com
@ -23,7 +24,7 @@ extended testing.
 The actual tests should be written using only the functions exported
 in the testing exports section of this module.  Note that only the set
 of functions needed for What4 is defined by this testing abstraction;
-if additional testing functions are needed, the GenV context should be
+if additional testing functions are needed, the GenEnv context should be
 extended to add an adaptation entry and the function should be defined
 here for use by the tests.

@ -62,8 +63,8 @@ For example, to bind to QuickCheck, specify:
 module Test.Verification
  (
    -- * Testing definitions
-    --
-    -- These definitions should be used by the tests themselves.  Most
+
+    -- | These definitions should be used by the tests themselves.  Most
    -- of these parallel a corresponding function in QuickCheck or
    -- Hedgehog, so the adaptation is minimal.
    assuming
@ -74,10 +75,11 @@ module Test.Verification
  , chooseInteger
  , Gen
  , getSize
+  , Verifiable(..)

    -- * Test concretization
-    --
-    -- Used by test implementation functions to map from this
+
+    -- | Used by test implementation functions to map from this
    -- Verification abstraction to the actual test mechanism
    -- (e.g. QuickCheck, HedgeHog, etc.)
  , Property(..)
--- a/what4/src/What4/BaseTypes.hs
+++ b/what4/src/What4/BaseTypes.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.BaseTypes
 -- Description      : This module exports the types used in solver expressions.
-- Copyright        : (c) Galois, Inc 2014-2016
+-- Copyright        : (c) Galois, Inc 2014-2020
 -- License          : BSD3
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Concrete.hs
+++ b/what4/src/What4/Concrete.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Concrete
 -- Description      : Concrete values of base types
-- Copyright        : (c) Galois, Inc 2018
+-- Copyright        : (c) Galois, Inc 2018-2020
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <rdockins@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Config.hs
+++ b/what4/src/What4/Config.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.Config
 -- Description : Declares attributes for simulator configuration settings.
-- Copyright   : (c) Galois, Inc 2015-2016
+-- Copyright   : (c) Galois, Inc 2015-2020
 -- License     : BSD3
 -- Maintainer  : Rob Dockins <rdockins@galois.com>
 -- Stability   : provisional
--- a/what4/src/What4/Expr.hs
+++ b/what4/src/What4/Expr.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Expr
-Copyright   : (c) Galois, Inc 2015-2018
+Description : Commonly-used reexports from the expression representation
+Copyright   : (c) Galois, Inc 2015-2020
 License     : BSD3
 Maintainer  : Rob Dockins <rdockins@galois.com>

--- a/what4/src/What4/Expr/AppTheory.hs
+++ b/what4/src/What4/Expr/AppTheory.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.Expr.AppTheory
 -- Description : Identifying the solver theory required by a core expression
-- Copyright   : (c) Galois, Inc 2016
+-- Copyright   : (c) Galois, Inc 2016-2020
 -- License     : BSD3
 -- Maintainer  : Joe Hendrix <jhendrix@galois.com>
 -- Stability   : provisional
--- a/what4/src/What4/Expr/ArrayUpdateMap.hs
+++ b/what4/src/What4/Expr/ArrayUpdateMap.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Expr.ArrayUpdateMap
-Copyright   : (c) Galois Inc, 2019
+Description : Datastructure for representing a sequence of updates to an SMT array
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : rdockins@galois.com
 -}
--- a/what4/src/What4/Expr/BoolMap.hs
+++ b/what4/src/What4/Expr/BoolMap.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Expr.BoolMap
-Copyright   : (c) Galois Inc, 2019
+Description : Datastructure for representing a conjunction of predicates
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : rdockins@galois.com

--- a/what4/src/What4/Expr/Builder.hs
+++ b/what4/src/What4/Expr/Builder.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Expr.Builder
-Copyright   : (c) Galois Inc, 2015-2016
+Description : Main definitions of the What4 expression representation
+Copyright   : (c) Galois Inc, 2015-2020
 License     : BSD3
 Maintainer  : jhendrix@galois.com

--- a/what4/src/What4/Expr/GroundEval.hs
+++ b/what4/src/What4/Expr/GroundEval.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.Expr.GroundEval
 -- Description : Computing ground values for expressions from solver assignments
-- Copyright   : (c) Galois, Inc 2016
+-- Copyright   : (c) Galois, Inc 2016-2020
 -- License     : BSD3
 -- Maintainer  : Joe Hendrix <jhendrix@galois.com>
 -- Stability   : provisional
--- a/what4/src/What4/Expr/MATLAB.hs
+++ b/what4/src/What4/Expr/MATLAB.hs
@ -1,8 +1,9 @@
 {-|
-Module     : What4.Expr.MATLAB
-Copyright  : (c) Galois, Inc, 2016
-License    : BSD3
-Maintainer : Joe Hendrix <jhendrix@galois.com>
+Module      : What4.Expr.MATLAB
+Description : Low-level support for MATLAB-style arithmetic operations
+Copyright   : (c) Galois, Inc, 2016-2020
+License     : BSD3
+Maintainer  : Joe Hendrix <jhendrix@galois.com>

 This module provides an interface that a symbolic backend should
 implement to support MATLAB intrinsics.
--- a/what4/src/What4/Expr/Simplify.hs
+++ b/what4/src/What4/Expr/Simplify.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Solver.SimpleBackend.Simplify
-Copyright   : (c) Galois, Inc 2016
+Description : Simplification procedure for distributing operations through if/then/else
+Copyright   : (c) Galois, Inc 2016-2020
 License     : BSD3
 Maintainer  : Joe Hendrix <jhendrix@galois.com>

--- a/what4/src/What4/Expr/StringSeq.hs
+++ b/what4/src/What4/Expr/StringSeq.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Expr.StringSeq
-Copyright   : (c) Galois Inc, 2019
+Description : Datastructure for sequences of appended strings
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : rdockins@galois.com

--- a/what4/src/What4/Expr/UnaryBV.hs
+++ b/what4/src/What4/Expr/UnaryBV.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Expr.UnaryBV
-Copyright   : (c) Galois, Inc 2015-2016
+Description : A "unary" bitvector representation
+Copyright   : (c) Galois, Inc 2015-2020
 License     : BSD3
 Maintainer  : Joe Hendrix <jhendrix@galois.com>

--- a/what4/src/What4/Expr/VarIdentification.hs
+++ b/what4/src/What4/Expr/VarIdentification.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Expr.VarIdentification
 -- Description      : Compute the bound and free variables appearing in expressions
-- Copyright        : (c) Galois, Inc 2015-2016
+-- Copyright        : (c) Galois, Inc 2015-2020
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <rdockins@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Expr/WeightedSum.hs
+++ b/what4/src/What4/Expr/WeightedSum.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Expr.WeightedSum
-Copyright   : (c) Galois Inc, 2015-2016
+Description : Representations for weighted sums and products in semirings
+Copyright   : (c) Galois Inc, 2015-2020
 License     : BSD3
 Maintainer  : jhendrix@galois.com

--- a/what4/src/What4/FunctionName.hs
+++ b/what4/src/What4/FunctionName.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.FunctionName
 -- Description      : Declarations for function names.
-- Copyright        : (c) Galois, Inc 2014
+-- Copyright        : (c) Galois, Inc 2014-2020
 -- License          : BSD3
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Interface.hs
+++ b/what4/src/What4/Interface.hs
@ -1,6 +1,7 @@
 {-|
 Module           : What4.Interface
-Copyright        : (c) Galois, Inc 2014-2018
+Description      : Main interface for constructing What4 formulae
+Copyright        : (c) Galois, Inc 2014-2020
 License          : BSD3
 Maintainer       : Joe Hendrix <jhendrix@galois.com>

--- a/what4/src/What4/LabeledPred.hs
+++ b/what4/src/What4/LabeledPred.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.LabeledPred
 -- Description      : Predicates with some metadata (a tag or label).
-- Copyright        : (c) Galois, Inc 2019
+-- Copyright        : (c) Galois, Inc 2019-2020
 -- License          : BSD3
 -- Maintainer       : Langston Barrett <langston@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Panic.hs
+++ b/what4/src/What4/Panic.hs
@ -7,7 +7,13 @@ import qualified Panic

 data What4 = What4

-panic :: HasCallStack => String -> [String] -> a
+-- | `panic` represents an error condition that should only
+--   arise due to a programming error. It will exit the program
+--   and print a message asking users to open a ticket.
+panic :: HasCallStack =>
+  String {- ^ Short name of where the error occured -} ->
+  [String] {- ^ More detailed description of the error  -} ->
+  a
 panic = Panic.panic What4

 instance PanicComponent What4 where
--- a/what4/src/What4/Partial.hs
+++ b/what4/src/What4/Partial.hs
@ -1,7 +1,8 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-|
 Module           : What4.Solver.Partial
-Copyright        : (c) Galois, Inc 2014-2016
+Description      : Representation of partial values
+Copyright        : (c) Galois, Inc 2014-2020
 License          : BSD3
 Maintainer       : Langston Barrett <langston@galois.com>

--- a/what4/src/What4/ProblemFeatures.hs
+++ b/what4/src/What4/ProblemFeatures.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.ProblemFeatures
 -- Description : Descriptions of the "features" that can occur in queries
-- Copyright   : (c) Galois, Inc 2016
+-- Copyright   : (c) Galois, Inc 2016-2020
 -- License     : BSD3
 -- Maintainer  : Joe Hendrix <jhendrix@galois.com>
 -- Stability   : provisional
--- a/what4/src/What4/ProgramLoc.hs
+++ b/what4/src/What4/ProgramLoc.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.ProgramLoc
 -- Description      : Datatype for handling program locations
-- Copyright        : (c) Galois, Inc 2014
+-- Copyright        : (c) Galois, Inc 2014-2020
 -- License          : BSD3
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Protocol/Online.hs
+++ b/what4/src/What4/Protocol/Online.hs
@ -1,6 +1,7 @@
 {- |
 Module      : What4.Protocol.Online
-Copyright   : (c) Galois, Inc 2018
+Description : Online solver interactions
+Copyright   : (c) Galois, Inc 2018-2020
 License     : BSD3
 Maintainer  : Rob Dockins <rdockins@galois.com>

--- a/what4/src/What4/Protocol/PolyRoot.hs
+++ b/what4/src/What4/Protocol/PolyRoot.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Protocol.PolyRoot
-Copyright   : (c) Galois Inc, 2016
+Description : Representation for algebraic reals
+Copyright   : (c) Galois Inc, 2016-2020
 License     : BSD3
 Maintainer  : jhendrix@galois.com

--- a/what4/src/What4/Protocol/ReadDecimal.hs
+++ b/what4/src/What4/Protocol/ReadDecimal.hs
@ -1,6 +1,7 @@
 {-
 Module           : What4.Utils.ReadDecimal
-Copyright        : (c) Galois, Inc 2014
+Description      : Parsing for decimal values
+Copyright        : (c) Galois, Inc 2014-2020
 License          : BSD3
 Maintainer       : Joe Hendrix <jhendrix@galois.com>

--- a/what4/src/What4/Protocol/SExp.hs
+++ b/what4/src/What4/Protocol/SExp.hs
@ -1,6 +1,7 @@
 {-
 Module           : What4.Protocol.SExp
-Copyright        : (c) Galois, Inc 2014
+Description      : Simple datatypes for representing S-Expressions
+Copyright        : (c) Galois, Inc 2014-2020
 License          : BSD3
 Maintainer       : Joe Hendrix <jhendrix@galois.com>

--- a/what4/src/What4/Protocol/SMTLib2.hs
+++ b/what4/src/What4/Protocol/SMTLib2.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Protocol.SMTLib2
 -- Description      : Interface for solvers that consume SMTLib2
-- Copyright        : (c) Galois, Inc 2014-2016
+-- Copyright        : (c) Galois, Inc 2014-2020
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <rdockins@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Protocol/SMTWriter.hs
+++ b/what4/src/What4/Protocol/SMTWriter.hs
@ -1,6 +1,7 @@
 {- |
 Module      : What4.Protocol.SMTWriter
-Copyright   : (c) Galois, Inc 2014-16.
+Description : Infrastructure for rendering What4 expressions in the language of SMT solvers
+Copyright   : (c) Galois, Inc 2014-2020.
 License     : BSD3
 Maintainer  : Joe Hendrix <jhendrix@galois.com>

--- a/what4/src/What4/SWord.hs
+++ b/what4/src/What4/SWord.hs
@ -1,6 +1,7 @@
 ------------------------------------------------------------------------
 -- |
 -- Module      : What4.SWord
+-- Description : Dynamically-sized bitvector values
 -- Copyright   : Galois, Inc. 2018-2020
 -- License     : BSD3
 -- Maintainer  : rdockins@galois.com
--- a/what4/src/What4/SatResult.hs
+++ b/what4/src/What4/SatResult.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.SatResult
 -- Description : Simple datastructure for capturing the result of a SAT/SMT query
-- Copyright   : (c) Galois, Inc 2015
+-- Copyright   : (c) Galois, Inc 2015-2020
 -- License     : BSD3
 -- Maintainer  : Joe Hendrix <jhendrix@galois.com>
 -- Stability   : provisional
--- a/what4/src/What4/SemiRing.hs
+++ b/what4/src/What4/SemiRing.hs
@ -1,11 +1,10 @@
 {-|
 Module      : What4.SemiRing
-Copyright   : (c) Galois Inc, 2019
+Description : Definitions related to semiring structures over base types.
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : rdockins@galois.com

-Definitions related to semiring structures over base types.
-
 The algebraic assumptions we make about our semirings are that:

 * addition is commutative and associative, with a unit called zero,
--- a/what4/src/What4/Solver.hs
+++ b/what4/src/What4/Solver.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Solver
-Copyright   : (c) Galois, Inc 2015-2018
+Description : Reexports for working with solvers
+Copyright   : (c) Galois, Inc 2015-2020
 License     : BSD3
 Maintainer  : Rob Dockins <rdockins@galois.com>

--- a/what4/src/What4/Solver/Adapter.hs
+++ b/what4/src/What4/Solver/Adapter.hs
@ -3,7 +3,7 @@
 -- Module           : What4.Solver.Adapter
 -- Description      : Defines the low-level interface between a particular
 --                    solver and the SimpleBuilder family of backends.
-- Copyright        : (c) Galois, Inc 2015
+-- Copyright        : (c) Galois, Inc 2015-2020
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <rdockins@galois.com>
 -- Stability        : provisional
@ -42,6 +42,8 @@ import           What4.Expr.Builder
 import           What4.Expr.GroundEval


+-- | The main interface for interacting with a solver in an "offline" fashion,
+--   which means that a new solver process is started for each query.
 data SolverAdapter st =
  SolverAdapter
  { solver_adapter_name :: !String
@ -69,6 +71,11 @@ data SolverAdapter st =
  , solver_adapter_write_smt2 :: !(forall t fs . ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
  }

+-- | A collection of operations for producing output from solvers.
+--   Solvers can produce messages at varying verbosity levels that
+--   might be appropriate for user output by using the `logCallbackVerbose`
+--   operation.  If a `logHandle` is provided, the entire interaction
+--   sequence with the solver will be mirrored into that handle.
 data LogData = LogData { logCallbackVerbose :: Int -> String -> IO ()
                       -- ^ takes a verbosity and a message to log
                       , logVerbosity :: Int
@ -125,6 +132,8 @@ solverAdapterOptions xs@(def:_) =
                 (Just (PP.text "Indicates which solver to use for check-sat queries"))
                 (Just (ConcreteString (UnicodeLiteral (T.pack (solver_adapter_name def)))))

+-- | Test the ability to interact with a solver by peforming a check-sat query
+--   on a trivially unsatisfiable problem.
 smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe X.SomeException)
 smokeTest sym adpt = test `X.catch` (pure . Just)
  where
--- a/what4/src/What4/Solver/Boolector.hs
+++ b/what4/src/What4/Solver/Boolector.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Solver.Boolector
 -- Description      : Interface for running Boolector
-- Copyright        : (c) Galois, Inc 2014
+-- Copyright        : (c) Galois, Inc 2014-2020
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <rdockins@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Solver/CVC4.hs
+++ b/what4/src/What4/Solver/CVC4.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.Solver.CVC4
 -- Description : Solver adapter code for CVC4
-- Copyright   : (c) Galois, Inc 2015
+-- Copyright   : (c) Galois, Inc 2015-2020
 -- License     : BSD3
 -- Maintainer  : Rob Dockins <rdockins@galois.com>
 -- Stability   : provisional
--- a/what4/src/What4/Solver/DReal.hs
+++ b/what4/src/What4/Solver/DReal.hs
@ -2,7 +2,7 @@
 -- |
 -- module           : What4.Solver.DReal
 -- Description      : Interface for running dReal
-- Copyright        : (c) Galois, Inc 2014
+-- Copyright        : (c) Galois, Inc 2014-2020
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <rdockins@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Solver/STP.hs
+++ b/what4/src/What4/Solver/STP.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.Solver.STP
 -- Description : Solver adapter code for STP
-- Copyright   : (c) Galois, Inc 2015
+-- Copyright   : (c) Galois, Inc 2015-2020
 -- License     : BSD3
 -- Maintainer  : Joe Hendrix <rdockins@galois.com>
 -- Stability   : provisional
--- a/what4/src/What4/Solver/Yices.hs
+++ b/what4/src/What4/Solver/Yices.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.Solver.Yices
 -- Description : Solver adapter code for Yices
-- Copyright   : (c) Galois, Inc 2015-2016
+-- Copyright   : (c) Galois, Inc 2015-2020
 -- License     : BSD3
 -- Maintainer  : Rob Dockins <rdockins@galois.com>
 -- Stability   : provisional
--- a/what4/src/What4/Solver/Z3.hs
+++ b/what4/src/What4/Solver/Z3.hs
@ -2,7 +2,7 @@
 -- |
 -- Module      : What4.Solver.Z3
 -- Description : Solver adapter code for Z3
-- Copyright   : (c) Galois, Inc 2015
+-- Copyright   : (c) Galois, Inc 2015-2020
 -- License     : BSD3
 -- Maintainer  : Rob Dockins <rdockins@galois.com>
 -- Stability   : provisional
@ -170,7 +170,7 @@ runZ3InOverride = SMT2.runSolverInOverride Z3 nullAcknowledgementAction z3Featur
 withZ3
  :: ExprBuilder t st fs
  -> FilePath
-    -- ^ Path to CVC4 executable
+    -- ^ Path to Z3 executable
  -> LogData
  -> (SMT2.Session t Z3 -> IO a)
    -- ^ Action to run
--- a/what4/src/What4/Symbol.hs
+++ b/what4/src/What4/Symbol.hs
@ -1,5 +1,7 @@
 {-|
-Copyright   : (c) Galois Inc, 2015
+Module      : What4.Symbol
+Description : Datatype for representing names that can be communicated to solvers
+Copyright   : (c) Galois Inc, 2015-2020
 License     : BSD3
 Maintainer  : jhendrix@galois.com

--- a/what4/src/What4/Utils/AbstractDomains.hs
+++ b/what4/src/What4/Utils/AbstractDomains.hs
@ -1,9 +1,17 @@
 {-|
-Copyright   : (c) Galois Inc, 2015-2016
+Module      : What4.Utils.AbstractDomains
+Description : Abstract domains for term simplification
+Copyright   : (c) Galois Inc, 2015-2020
 License     : BSD3
 Maintainer  : jhendrix@galois.com

 This module declares a set of abstract domains used by the solver.
+These are mostly interval domains on numeric types.
+
+Since these abstract domains are baked directly into the term
+representation, we want to get as much bang-for-buck as possible.
+Thus, we prioritize compact representations and simple algorithms over
+precision.
 -}

 {-# LANGUAGE CPP #-}
--- a/what4/src/What4/Utils/AnnotatedMap.hs
+++ b/what4/src/What4/Utils/AnnotatedMap.hs
@ -1,6 +1,7 @@
 {-|
 Module      : What4.Utils.AnnotatedMap
-Copyright   : (c) Galois Inc, 2019
+Description : A finite map data structure with monoidal annotations
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : huffman@galois.com

--- a/what4/src/What4/Utils/Arithmetic.hs
+++ b/what4/src/What4/Utils/Arithmetic.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Utils.Arithmetic
 -- Description      : Utility functions for computing arithmetic
-- Copyright        : (c) Galois, Inc 2015
+-- Copyright        : (c) Galois, Inc 2015-2020
 -- License          : BSD3
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Utils/BVDomain.hs
+++ b/what4/src/What4/Utils/BVDomain.hs
@ -1,11 +1,24 @@
 {-|
 Module      : What4.Utils.BVDomain
-Copyright   : (c) Galois Inc, 2019
+Description : Abstract domains for bitvectors
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : huffman@galois.com

-Provides an interval-based implementation of bitvector abstract
-domains.
+Provides an implementation of abstract domains for bitvectors.
+This abstract domain has essentially two modes: arithmetic
+and bitvector modes. The arithmetic mode is a fairly straightforward
+interval domain, albeit one that is carefully implemented to deal
+properly with intervals that "cross zero", as is relatively common
+when using 2's complement signed representations. The bitwise
+mode tracks the values of individual bits independently in a
+3-valued logic (true, false or unknown).  The abstract domain
+transitions between the two modes when necessary, but attempts
+to retain as much precision as possible.
+
+The operations of these domains are formalized in the companion
+Cryptol files found together in this package under the \"doc\"
+directory, and their soundness properties stated and established.
 -}

 {-# LANGUAGE DataKinds #-}
@ -221,6 +234,7 @@ data BVDomain (w :: Nat)
  | BVDBitwise !(B.Domain w)
  deriving Show

+-- | Return the bitvector mask value from this domain
 bvdMask :: BVDomain w -> Integer
 bvdMask x =
  case x of
@ -232,14 +246,17 @@ proper :: NatRepr w -> BVDomain w -> Bool
 proper w (BVDArith a) = A.proper w a
 proper w (BVDBitwise b) = B.proper w b

+-- | Test if the given integer value is a member of the abstract domain
 member :: BVDomain w -> Integer -> Bool
 member (BVDArith a) x = A.member a x
 member (BVDBitwise a) x = B.member a x

+-- | Compute how many concrete elements are in the abstract domain
 size :: BVDomain w -> Integer
 size (BVDArith a)   = A.size a
 size (BVDBitwise b) = B.size b

+-- | Generate a random nonempty domain
 genDomain :: NatRepr w -> Gen (BVDomain w)
 genDomain w =
  do b <- chooseBool
@ -248,10 +265,14 @@ genDomain w =
     else
       BVDBitwise <$> B.genDomain w

+-- | Generate a random element from a domain, which
+--   is assumed to be nonempty
 genElement :: BVDomain w -> Gen Integer
 genElement (BVDArith a) = A.genElement a
 genElement (BVDBitwise b) = B.genElement b

+-- | Generate a random nonempty domain and an element
+--   contained in that domain.
 genPair :: NatRepr w -> Gen (BVDomain w, Integer)
 genPair w =
  do a <- genDomain w
@ -285,7 +306,7 @@ bitwiseRoundAbove bvmask x lomask = upperbits .|. lowerbits
 {- |
 Precondition: @lomask <= x <= himask@ and @lomask .|. himask == himask@.
 Find the (arithmetically) smallest @z@ above @x@ which is bitwise between
- @lomask@ and @himask@.  In otherwords, find the smallest @z@ such that
+ @lomask@ and @himask@.  In other words, find the smallest @z@ such that
 @x <= z@ and @lomask .|. z = z@ and @z .|. himask == himask@.
 -}
 bitwiseRoundBetween ::
@ -297,7 +318,7 @@ bitwiseRoundBetween ::
 bitwiseRoundBetween bvmask x lomask himask = final
  -- read these steps bottom up...
  where
-  -- Finally mask out the low bits and only set those requried by the lomask
+  -- Finally mask out the low bits and only set those required by the lomask
  final = (upper .&. (lobits `Bits.xor` bvmask)) .|. lomask

  -- add the correcting bit and mask out any extraneous bits set in
@ -312,7 +333,7 @@ bitwiseRoundBetween bvmask x lomask himask = final
  -- isolate just the highest incorrect bit
  highbit = rmask `Bits.xor` lobits

-  -- a mask for all the bits to the right of the higest incorrect ibt
+  -- a mask for all the bits to the right of the highest incorrect bit
  lobits = rmask `shiftR` 1

  -- set all the bits to the right of the highest incorrect bit
@ -362,7 +383,7 @@ mixedCandidates a b =
 (lomask,himask) = B.bitbounds b

 -- | Return a list of "candidate" overlap elements.  If two domains
--   overlap, then they will definintely share one of the given
+--   overlap, then they will definitely share one of the given
 --   values.
 overlapCandidates :: BVDomain w -> BVDomain w -> [Integer]
 overlapCandidates (BVDArith a)   (BVDBitwise b) = mixedCandidates a b
--- a/what4/src/What4/Utils/BVDomain/Arith.hs
+++ b/what4/src/What4/Utils/BVDomain/Arith.hs
@ -1,6 +1,6 @@
 {-|
 Module      : What4.Utils.BVDomain.Arith
-Copyright   : (c) Galois Inc, 2019
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : huffman@galois.com

@ -131,10 +131,12 @@ sameDomain (BVDAny _) (BVDAny _) = True
 sameDomain (BVDInterval _ x w) (BVDInterval _ x' w') = x == x' && w == w'
 sameDomain _ _ = False

+-- | Compute how many concrete elements are in the abstract domain
 size :: Domain w -> Integer
 size (BVDAny mask)        = mask + 1
 size (BVDInterval _ _ sz) = sz + 1

+-- | Test if the given integer value is a member of the abstract domain
 member :: Domain w -> Integer -> Bool
 member (BVDAny _) _ = True
 member (BVDInterval mask lo sz) x = ((x' - lo) .&. mask) <= sz
@ -149,6 +151,7 @@ proper w (BVDInterval mask lo sz) =
  sz .|. mask == mask &&
  sz < mask

+-- | Return the bitvector mask value from this domain
 bvdMask :: Domain w -> Integer
 bvdMask x =
  case x of
@ -163,12 +166,15 @@ genDomain w =
     sz <- chooseInteger (0, mask)
     pure $! interval mask lo sz

+-- | Generate a random element from a domain
 genElement :: Domain w -> Gen Integer
 genElement (BVDAny mask) = chooseInteger (0, mask)
 genElement (BVDInterval mask lo sz) =
   do x <- chooseInteger (0, sz)
      pure ((x+lo) .&. mask)

+-- | Generate a random domain and an element
+--   contained in that domain.
 genPair :: NatRepr w -> Gen (Domain w, Integer)
 genPair w =
  do a <- genDomain w
--- a/what4/src/What4/Utils/BVDomain/Bitwise.hs
+++ b/what4/src/What4/Utils/BVDomain/Bitwise.hs
@ -110,10 +110,12 @@ proper w (BVBitInterval mask lo hi) =
  bitle hi mask &&
  bitle lo hi

+-- | Test if the given integer value is a member of the abstract domain
 member :: Domain w -> Integer -> Bool
 member (BVBitInterval mask lo hi) x = bitle lo x' && bitle x' hi
  where x' = x .&. mask

+-- | Compute how many concrete elements are in the abstract domain
 size :: Domain w -> Integer
 size (BVBitInterval _ lo hi)
  | bitle lo hi = Bits.bit p
@ -125,6 +127,7 @@ size (BVBitInterval _ lo hi)
 bitle :: Integer -> Integer -> Bool
 bitle x y = (x .|. y) == y

+-- | Return the bitvector mask value from this domain
 bvdMask :: Domain w -> Integer
 bvdMask (BVBitInterval mask _ _) = mask

@ -168,7 +171,8 @@ genElement (BVBitInterval mask lo hi) =
     pure ((x .&. u) .|. lo)
 -}

-
+-- | Generate a random nonempty domain and an element
+--   contained in that domain.
 genPair :: NatRepr w -> Gen (Domain w, Integer)
 genPair w =
  do a <- genDomain w
@ -179,6 +183,7 @@ genPair w =
 interval :: Integer -> Integer -> Integer -> Domain w
 interval mask lo hi = BVBitInterval mask lo hi

+-- | Construct a domain from bitwise lower and upper bounds
 range :: NatRepr w -> Integer -> Integer -> Domain w
 range w lo hi = BVBitInterval (maxUnsigned w) lo' hi'
  where
@ -186,6 +191,7 @@ range w lo hi = BVBitInterval (maxUnsigned w) lo' hi'
  hi'  = hi .&. mask
  mask = maxUnsigned w

+-- | Bitwise lower and upper bounds
 bitbounds :: Domain w -> (Integer, Integer)
 bitbounds (BVBitInterval _ lo hi) = (lo, hi)

@ -205,6 +211,7 @@ singleton w x = BVBitInterval mask x' x'
  x' = x .&. mask
  mask = maxUnsigned w

+-- | Bitwise domain containing every bitvector value
 any :: NatRepr w -> Domain w
 any w = BVBitInterval mask 0 mask
  where
--- a/what4/src/What4/Utils/BVDomain/XOR.hs
+++ b/what4/src/What4/Utils/BVDomain/XOR.hs
@ -1,10 +1,10 @@
 {-|
 Module      : What4.Utils.BVDomain.XOR
-Copyright   : (c) Galois Inc, 2019
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : huffman@galois.com

-Provides an implementation of bitvecotr abstract domains
+Provides an implementation of bitvector abstract domains
 optimized for performing XOR operations.
 -}

@ -73,12 +73,15 @@ proper w (BVDXor mask val u) =
  bitle u mask &&
  bitle u val

+-- | Test if the given integer value is a member of the abstract domain
 member :: Domain w -> Integer -> Bool
 member (BVDXor mask hi unknown) x = hi == (x .&. mask) .|. unknown

+-- | Return the bitvector mask value from this domain
 bvdMask :: Domain w -> Integer
 bvdMask (BVDXor mask _ _) = mask

+-- | Construct a domain from bitwise lower and upper bounds
 range :: NatRepr w -> Integer -> Integer -> Domain w
 range w lo hi = interval mask lo' hi'
  where
@ -90,6 +93,7 @@ range w lo hi = interval mask lo' hi'
 interval :: Integer -> Integer -> Integer -> Domain w
 interval mask lo hi = BVDXor mask hi (Bits.xor lo hi)

+-- | Bitwise lower and upper bounds
 bitbounds :: Domain w -> (Integer, Integer)
 bitbounds (BVDXor _ hi u) = (Bits.xor u hi, hi)

@ -97,6 +101,8 @@ bitbounds (BVDXor _ hi u) = (Bits.xor u hi, hi)
 asSingleton :: Domain w -> Maybe Integer
 asSingleton (BVDXor _ hi u) = if u == 0 then Just hi else Nothing

+-- | Random generator for domain values.  We always generate
+--   nonempty domains values.
 genDomain :: NatRepr w -> Gen (Domain w)
 genDomain w =
  do let mask = maxUnsigned w
@ -104,6 +110,12 @@ genDomain w =
     u   <- chooseInteger (0, mask)
     pure $ BVDXor mask (val .|. u) u

+-- This generator goes to some pains to try
+-- to generate a good statistical distribution
+-- of the values in the domain.  It only choses
+-- random bits for the "unknown" values of
+-- the domain, then stripes them out among
+-- the unknown bit positions.
 genElement :: Domain w -> Gen Integer
 genElement (BVDXor _mask v u) =
   do x <- chooseInteger (0, bit bs - 1)
@ -119,13 +131,15 @@ genElement (BVDXor _mask v u) =
       stripe val' (x `shiftR` 1) (i+1)
   | otherwise = stripe val x (i+1)

+-- | Generate a random nonempty domain and an element
+--   contained in that domain.
 genPair :: NatRepr w -> Gen (Domain w, Integer)
 genPair w =
  do a <- genDomain w
     x <- genElement a
     pure (a,x)

-
+-- | Return a domain containing just the given value
 singleton :: NatRepr w -> Integer -> Domain w
 singleton w x = BVDXor mask (x .&. mask) 0
  where
--- a/what4/src/What4/Utils/Complex.hs
+++ b/what4/src/What4/Utils/Complex.hs
@ -3,7 +3,7 @@
 -- Module           : What4.Utils.Complex
 -- Description      : Provides a complex representation that is more generic
 --                    than Data.Complex.
-- Copyright        : (c) Galois, Inc 2014
+-- Copyright        : (c) Galois, Inc 2014-2020
 -- License          : BSD3
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Utils/Environment.hs
+++ b/what4/src/What4/Utils/Environment.hs
@ -4,7 +4,7 @@
 -- Description      : Provides functions for finding an executable, and
 --                    expanding a path with referenced to environment
 --                    variables.
-- Copyright        : (c) Galois, Inc 2013
+-- Copyright        : (c) Galois, Inc 2013-2020
 -- License          : BSD3
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Utils/IncrHash.hs
+++ b/what4/src/What4/Utils/IncrHash.hs
@ -1,6 +1,6 @@
 {-|
 Module      : What4.Utils.IncrHash
-Copyright   : (c) Galois Inc, 2019
+Copyright   : (c) Galois Inc, 2019-2020
 License     : BSD3
 Maintainer  : rdockins@galois.com

--- a/what4/src/What4/Utils/LeqMap.hs
+++ b/what4/src/What4/Utils/LeqMap.hs
@ -1,6 +1,6 @@
 {-|
 Module           : What4.Utils.LeqMap
-Copyright        : (c) Galois, Inc 2015-2016
+Copyright        : (c) Galois, Inc 2015-2020
 License          : BSD3
 Maintainer       : Joe Hendrix <jhendrix@galois.com>

--- a/what4/src/What4/Utils/MonadST.hs
+++ b/what4/src/What4/Utils/MonadST.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Utils.MonadST
 -- Description      : Typeclass for monads generalizing ST
-- Copyright        : (c) Galois, Inc 2014
+-- Copyright        : (c) Galois, Inc 2014-2020
 -- License          : BSD3
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Utils/OnlyNatRepr.hs
+++ b/what4/src/What4/Utils/OnlyNatRepr.hs
@ -1,6 +1,6 @@
 {-|
 Module           : What4.Utils.OnlyNatRepr
-Copyright        : (c) Galois
+Copyright        : (c) Galois, Inc. 2020
 License          : BSD3
 Maintainer       : Joe Hendrix <jhendrix@galois.com>

--- a/what4/src/What4/Utils/Process.hs
+++ b/what4/src/What4/Utils/Process.hs
@ -1,6 +1,6 @@
 {-
 Module           : What4.Utils.Process
-Copyright        : (c) Galois, Inc 2014-2016
+Copyright        : (c) Galois, Inc 2014-2020
 License          : BSD3
 Maintainer       : Rob Dockins <rdockins@galois.com>

--- a/what4/src/What4/Utils/Streams.hs
+++ b/what4/src/What4/Utils/Streams.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Utils.Streams
 -- Description      : IO stream utilities
-- Copyright        : (c) Galois, Inc 2013-2014
+-- Copyright        : (c) Galois, Inc 2013-2020
 -- License          : BSD3
 -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Utils/StringLiteral.hs
+++ b/what4/src/What4/Utils/StringLiteral.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Utils.StringLiteral
 -- Description      : Utility definitions for strings
-- Copyright        : (c) Galois, Inc 2019
+-- Copyright        : (c) Galois, Inc 2019-2020
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <rdockins@galois.com>
 -- Stability        : provisional
--- a/what4/src/What4/Utils/Word16String.hs
+++ b/what4/src/What4/Utils/Word16String.hs
@ -2,7 +2,7 @@
 -- |
 -- Module           : What4.Utils.Word16String
 -- Description      : Utility definitions for wide (2-byte) strings
-- Copyright        : (c) Galois, Inc 2019
+-- Copyright        : (c) Galois, Inc 2019-2020
 -- License          : BSD3
 -- Maintainer       : Rob Dockins <rdockins@galois.com>
 -- Stability        : provisional
@ -11,6 +11,7 @@
 module What4.Utils.Word16String
 ( Word16String
 , fromLEByteString
+, toLEByteString
 , empty
 , singleton
 , null
@ -87,14 +88,26 @@ showsWord16String (Word16String xs0) tl = '"' : go (BS.unpack xs0)
  c = toEnum (fromIntegral x)


+-- | Generate a @Word16String@ from a bytestring
+--   where the 16bit words are encoded as two bytes
+--   in little-endian order.
+--
+--   PRECONDITION: the input bytestring must 
+--   have a length which is a multiple of 2.
 fromLEByteString :: ByteString -> Word16String
 fromLEByteString xs
  | BS.length xs `mod` 2 == 0 = Word16String xs
  | otherwise = error "fromLEByteString: bytestring must have even length"

+-- | Return the underlying little endian bytestring.
+toLEByteString :: Word16String -> ByteString
+toLEByteString (Word16String xs) = xs
+
+-- | Return the empty string
 empty :: Word16String
 empty = Word16String BS.empty

+-- | Compute the string containing just the given character
 singleton :: Word16 -> Word16String
 singleton c = Word16String (BS.pack [ lo , hi ])
 where
@ -102,9 +115,12 @@ singleton c = Word16String (BS.pack [ lo , hi ])
 lo = fromIntegral (c .&. 0xFF)
 hi = fromIntegral (c `shiftR` 8)

+-- | Test if the given string is empty
 null :: Word16String -> Bool
 null (Word16String xs) = BS.null xs

+-- | Retrive the @n@th character of the string.
+--   Out of bounds accesses will cause an error.
 index :: Word16String -> Int -> Word16
 index (Word16String xs) i = (hi `shiftL` 8) .|. lo
 where
--- a/what4/src/What4/WordMap.hs
+++ b/what4/src/What4/WordMap.hs
@ -1,6 +1,7 @@
 {-|
 Module           : What4.WordMap
-Copyright        : (c) Galois, Inc 2014-2018
+Description      : Datastructure for mapping bitvectors to values
+Copyright        : (c) Galois, Inc 2014-2020
 License          : BSD3
 Maintainer       : Rob Dockins <rdockins@galois.com>
 -}
--- a/what4/what4.cabal
+++ b/what4/what4.cabal
@ -2,7 +2,7 @@ Name:          what4
 Version:       0.4.2
 Author:        Galois Inc.
 Maintainer:    jhendrix@galois.com, rdockins@galois.com
-Copyright:     (c) Galois, Inc 2014-2018
+Copyright:     (c) Galois, Inc 2014-2020
 License:       BSD3
 License-file:  LICENSE
 Build-type:    Simple
@ -33,41 +33,41 @@ flag STPTestDisable
 library
  build-depends:
    base >= 4.8 && < 5,
-    attoparsec,
-    ansi-wl-pprint,
+    attoparsec >= 0.13,
+    ansi-wl-pprint >= 0.6.8,
    bimap >= 0.2,
    bifunctors >= 5,
    bv-sized >= 1.0.0,
-    bytestring,
+    bytestring >= 0.10,
    deriving-compat >= 0.5,
    containers >= 0.5.0.0,
    data-binary-ieee754,
-    deepseq,
-    directory,
-    exceptions,
-    extra,
-    filepath,
-    fingertree,
-    hashable,
-    hashtables,
-    io-streams,
-    lens,
-    mtl,
+    deepseq >= 1.3,
+    directory >= 1.2.2,
+    exceptions >= 0.10,
+    extra >= 1.6,
+    filepath >= 1.3,
+    fingertree >= 0.1.4,
+    hashable >= 1.3,
+    hashtables >= 1.2.3,
+    io-streams >= 1.5,
+    lens >= 4.18,
+    mtl >= 2.2.1,
    panic >= 0.3,
    parameterized-utils >= 2.1 && < 2.2,
-    process,
-    scientific,
+    process >= 1.2,
+    scientific >= 0.3.6,
    temporary >= 1.2,
    template-haskell,
-    text,
+    text >= 1.1,
    th-abstraction >=0.1 && <0.4,
-    transformers,
-    unordered-containers,
-    utf8-string,
-    vector,
-    versions,
+    transformers >= 0.4,
+    unordered-containers >= 0.2.10,
+    utf8-string >= 1.0.1,
+    vector >= 0.12.1,
+    versions >= 3.5.2,
    zenc >= 0.1.0 && < 0.2.0,
-    ghc-prim
+    ghc-prim >= 0.5.3

  default-language: Haskell2010
  default-extensions:
@ -151,7 +151,7 @@ library
    What4.Expr.App

  ghc-options: -Wall -Werror=incomplete-patterns -Werror=missing-methods -Werror=overlapping-patterns
-  ghc-prof-options: -O2 -fprof-auto-top
+  ghc-prof-options: -fprof-auto-top
  if impl(ghc >= 8.6)
    default-extensions: NoStarIsType