From 2f3637595390d0fb4b82b72d22a13ddfc237e2d2 Mon Sep 17 00:00:00 2001 From: brianhuffman Date: Tue, 28 Apr 2020 10:09:56 -0700 Subject: [PATCH 1/3] Make compile without warnings on GHC 8.4 through 8.8 (#687) Make compile without warnings on GHC 8.4, 8.6, and 8.8. Avoid "allow-newer" option in all stack.yaml files so that version constraints are not ignored. Co-authored-by: Aaron Tomb --- src/SAWScript/Builtins.hs | 1 - src/SAWScript/Crucible/Common/MethodSpec.hs | 1 - src/SAWScript/Crucible/JVM/MethodSpecIR.hs | 1 - src/SAWScript/Crucible/JVM/Override.hs | 7 ++++++- src/SAWScript/Crucible/LLVM/Builtins.hs | 2 +- src/SAWScript/Crucible/LLVM/Override.hs | 8 +++++++- src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs | 2 +- src/SAWScript/Crucible/LLVM/X86.hs | 4 +--- src/SAWScript/ImportAIG.hs | 1 - src/SAWScript/Value.hs | 1 - src/SAWScript/X86Spec.hs | 2 -- stack.ghc-8.4.yaml | 6 +++++- stack.ghc-8.6.yaml | 2 +- 13 files changed, 22 insertions(+), 16 deletions(-) diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs index 7989a57fcd..3b274d7f69 100644 --- 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 index c17bc91371..f982cf79c7 100644 --- 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 index d5a7c7a43d..35b773dbc6 100644 --- 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 index af021ef4ae..2ba7f68c29 100644 --- 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 index 4e21baa086..a1266e3c6c 100644 --- 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 index dca7d1fcb5..85e59534ba 100644 --- 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 index b4c3e01950..c394dda2a2 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -25,7 +25,7 @@ module SAWScript.Crucible.LLVM.ResolveSetupValue , memArrayToSawCoreTerm ) where -import Control.Lens +import Control.Lens ((^.)) import Control.Monad import Control.Monad.Catch (MonadThrow) import Control.Monad.State diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs index 61a9ad6234..e225de951d 100644 --- 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 index 2969c6052f..9889e9ece2 100644 --- 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 index db9a1fedbe..2155de877e 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -30,7 +30,6 @@ module SAWScript.Value where import Prelude hiding (fail) -import Data.Semigroup ((<>)) #if !MIN_VERSION_base(4,8,0) import Control.Applicative (Applicative) #endif diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index d444f897c6..eb28f60b84 100644 --- 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 index d57dcdb6f9..d53f17ac3a 100644 --- 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 index decd375983..3293a43375 100644 --- 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 From e0328e965736dc4dd60fb546df298d5bce84e6d5 Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 28 Apr 2020 10:49:57 -0700 Subject: [PATCH 2/3] Bump submodules (#692) --- deps/crucible | 2 +- deps/cryptol | 2 +- deps/macaw | 2 +- deps/what4 | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/deps/crucible b/deps/crucible index a51ac16762..2fe074cb84 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit a51ac167628804a58903bfb01f4c70cf1c503783 +Subproject commit 2fe074cb847b01d7355f993d3b2b9192fdffbd29 diff --git a/deps/cryptol b/deps/cryptol index 30b41e9c45..7e841e915f 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 30b41e9c45e5f67b5cfb352614bb23dcf4a269ab +Subproject commit 7e841e915f34a21bbfad67070c7338662ac28601 diff --git a/deps/macaw b/deps/macaw index 02c2fcd96a..3a1396b500 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 02c2fcd96ad1436360fecf41823be04749aaf910 +Subproject commit 3a1396b500e04c0e457669ff2e579d33647b41e2 diff --git a/deps/what4 b/deps/what4 index 8d6bc58c6c..e65ff5d487 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 8d6bc58c6c1d6316eb8e92e087bd9b279b565959 +Subproject commit e65ff5d48728618611e942917c00af4e84face74 From e01a1cc54bd71e49c4be3d9c30d0050d61c3379b Mon Sep 17 00:00:00 2001 From: Samuel Breese Date: Tue, 28 Apr 2020 16:25:04 -0400 Subject: [PATCH 3/3] Ensure that everything builds on GHC 8.8 --- src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs | 8 ++++---- src/SAWScript/Value.hs | 3 +++ 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index c394dda2a2..88a9803ff7 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -27,7 +27,7 @@ module SAWScript.Crucible.LLVM.ResolveSetupValue 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/Value.hs b/src/SAWScript/Value.hs index 2155de877e..b951cb2945 100644 --- a/src/SAWScript/Value.hs +++ b/src/SAWScript/Value.hs @@ -34,6 +34,7 @@ import Prelude hiding (fail) 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) @@ -399,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