Merge branch 'master' into release-0.5

GaloisInc · Apr 28, 2020 · d2d48ee · d2d48ee
2 parents 7ea13a9 + 93d8881
commit d2d48ee
Show file tree

Hide file tree

Showing 17 changed files with 33 additions and 24 deletions.
diff --git a/deps/crucible b/deps/crucible
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/macaw b/deps/macaw
diff --git a/deps/what4 b/deps/what4
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
@@ -34,7 +34,6 @@ import qualified Data.IntMap as IntMap
 import Data.List (isPrefixOf, isInfixOf)
 import qualified Data.Map as Map
 import Data.Maybe
-import Data.Monoid ((<>))
 import Data.Time.Clock
 import Data.Typeable
 import System.Directory

diff --git a/src/SAWScript/Crucible/Common/MethodSpec.hs b/src/SAWScript/Crucible/Common/MethodSpec.hs
@@ -31,7 +31,6 @@ import           Data.Void (Void)
 import           Control.Monad.Trans.Maybe
 import           Control.Monad.Trans (lift)
 import           Control.Lens
-import           Data.Monoid ((<>))
 import           Data.Kind (Type)
 import qualified Text.PrettyPrint.ANSI.Leijen as PP
 

diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs
@@ -28,7 +28,6 @@ Stability   : provisional
 module SAWScript.Crucible.JVM.MethodSpecIR where
 
 import           Control.Lens
-import           Data.Monoid ((<>))
 import qualified Text.PrettyPrint.ANSI.Leijen as PPL hiding ((<$>), (<>))
 
 -- what4

diff --git a/src/SAWScript/Crucible/JVM/Override.hs b/src/SAWScript/Crucible/JVM/Override.hs
@@ -43,7 +43,12 @@ module SAWScript.Crucible.JVM.Override
   , decodeJVMVal
   ) where
 
-import           Control.Lens
+import           Control.Lens.At
+import           Control.Lens.Each
+import           Control.Lens.Fold
+import           Control.Lens.Getter
+import           Control.Lens.Lens
+import           Control.Lens.Setter
 import           Control.Exception as X
 import           Control.Monad.IO.Class (liftIO)
 import           Control.Monad

diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -74,7 +74,7 @@ import           Control.Monad.State hiding (fail)
 import           Control.Monad.Fail (MonadFail(..))
 import qualified Data.Bimap as Bimap
 import           Data.Char (isDigit)
-import           Data.Foldable (for_, toList, find, fold)
+import           Data.Foldable (for_, toList, fold)
 import           Data.Function
 import           Data.IORef
 import           Data.List

diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -47,7 +47,13 @@ module SAWScript.Crucible.LLVM.Override
   , enableSMTArrayMemoryModel
   ) where
 
-import           Control.Lens
+import           Control.Lens.At
+import           Control.Lens.Each
+import           Control.Lens.Fold
+import           Control.Lens.Getter
+import           Control.Lens.Lens
+import           Control.Lens.Setter
+import           Control.Lens.TH
 import           Control.Exception as X
 import           Control.Monad.IO.Class (liftIO)
 import           Control.Monad

diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -25,9 +25,9 @@ module SAWScript.Crucible.LLVM.ResolveSetupValue
   , memArrayToSawCoreTerm
   ) where
 
-import Control.Lens
+import Control.Lens ((^.))
 import Control.Monad
-import Control.Monad.Catch (MonadThrow)
+import Control.Monad.Fail (MonadFail)
 import Control.Monad.State
 import Data.Foldable (toList)
 import Data.Maybe (fromMaybe, listToMaybe, fromJust)
@@ -125,7 +125,7 @@ resolveSetupFieldIndex cc env nameEnv v n =
     lc = ccTypeCtx cc
 
 resolveSetupFieldIndexOrFail ::
-  MonadThrow m =>
+  MonadFail m =>
   LLVMCrucibleContext arch {- ^ crucible context  -} ->
   Map AllocIndex LLVMAllocSpec {- ^ allocation types  -} ->
   Map AllocIndex Crucible.Ident   {- ^ allocation type names -} ->
@@ -148,7 +148,7 @@ resolveSetupFieldIndexOrFail cc env nameEnv v n =
             _ -> unlines [msg, "No field names were found for this struct"]
 
 typeOfSetupValue ::
-  MonadThrow m =>
+  MonadFail m =>
   LLVMCrucibleContext arch ->
   Map AllocIndex LLVMAllocSpec ->
   Map AllocIndex Crucible.Ident ->
@@ -159,7 +159,7 @@ typeOfSetupValue cc env nameEnv val =
      typeOfSetupValue' cc env nameEnv val
 
 typeOfSetupValue' :: forall m arch.
-  MonadThrow m =>
+  MonadFail m =>
   LLVMCrucibleContext arch ->
   Map AllocIndex LLVMAllocSpec ->
   Map AllocIndex Crucible.Ident ->

diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -29,11 +29,9 @@ import System.IO (stdout)
 import Control.Exception (catch)
 import Control.Lens (view, (^.))
 import Control.Monad.ST (stToIO)
-import Control.Monad.IO.Class (liftIO)
 import Control.Monad.State
 
-import Data.Type.Equality ((:~:)(..), testEquality)
-import Data.Foldable (foldlM, forM_)
+import Data.Foldable (foldlM)
 import Data.IORef
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Vector as Vector

diff --git a/src/SAWScript/ImportAIG.hs b/src/SAWScript/ImportAIG.hs
@@ -33,7 +33,6 @@ import qualified Data.AIG as AIG
 import Verifier.SAW.Prelude
 import Verifier.SAW.Recognizer
 import Verifier.SAW.SharedTerm hiding (scNot, scAnd, scOr)
-import Verifier.SAW.TypedAST (ppTerm, defaultPPOpts)
 import SAWScript.Options
 
 type TypeParser = StateT (V.Vector Term) (ExceptT String IO)

diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
@@ -30,11 +30,11 @@ module SAWScript.Value where
 
 import Prelude hiding (fail)
 
-import Data.Semigroup ((<>))
 #if !MIN_VERSION_base(4,8,0)
 import Control.Applicative (Applicative)
 #endif
 import Control.Lens
+import Control.Monad.Fail (MonadFail(..))
 import Control.Monad.Catch (MonadThrow(..))
 import Control.Monad.Except (ExceptT(..), runExceptT)
 import Control.Monad.Reader (MonadReader)
@@ -400,6 +400,8 @@ newtype TopLevel a =
 deriving instance MonadReader TopLevelRO TopLevel
 deriving instance MonadState TopLevelRW TopLevel
 instance Wrapped (TopLevel a) where
+instance MonadFail TopLevel where
+  fail = throwTopLevel
 
 runTopLevel :: TopLevel a -> TopLevelRO -> TopLevelRW -> IO (a, TopLevelRW)
 runTopLevel (TopLevel m) ro rw = runStateT (runReaderT m ro) rw

diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs
@@ -61,7 +61,6 @@ import GHC.Natural(Natural)
 import Data.Kind(Type)
 import Control.Applicative ( (<|>) )
 import Control.Lens (view, (^.), over)
-import Control.Monad(foldM,zipWithM,join)
 import Data.List(sortBy)
 import Data.Maybe(catMaybes)
 import Data.Map (Map)
@@ -105,7 +104,6 @@ import SAWScript.Crucible.LLVM.CrucibleLLVM
   )
 import qualified Lang.Crucible.LLVM.MemModel as Crucible
 
-import Lang.Crucible.Simulator.RegValue(RegValue'(..),RegValue)
 import Lang.Crucible.Simulator.SimError(SimErrorReason(AssertFailureSimError))
 import Lang.Crucible.Backend
           (addAssumption, getProofObligations, proofGoalsToList

diff --git a/stack.ghc-8.4.yaml b/stack.ghc-8.4.yaml
@@ -53,5 +53,9 @@ extra-deps:
   - config-value-0.6.3.1
   - simple-get-opt-0.3
   - base-orphans-0.8.2
+  - Glob-0.10.0
+  - yaml-0.11.2.0
+  - libyaml-0.1.2
+  - aeson-1.4.3.0
 resolver: lts-12.26
-allow-newer: true
+allow-newer: false
diff --git a/stack.ghc-8.6.yaml b/stack.ghc-8.6.yaml
@@ -54,4 +54,4 @@ extra-deps:
   - simple-get-opt-0.3
   - base-orphans-0.8.2
 resolver: lts-14.3
-allow-newer: true
+allow-newer: false