diff --git a/cabal.GHC-8.10.3.config b/cabal.GHC-8.10.3.config index 33bbc770c6..e456e22d6c 100644 --- a/cabal.GHC-8.10.3.config +++ b/cabal.GHC-8.10.3.config @@ -185,7 +185,7 @@ constraints: any.Cabal ==3.2.1.0, language-c -allwarnings +iecfpextension +separatesyb +usebytestrings, any.lens ==4.19.2, lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.1, + any.libBF ==0.6.2, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, @@ -334,7 +334,7 @@ constraints: any.Cabal ==3.2.1.0, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-binary-instances ==0.2.5.1, any.vector-th-unbox ==0.2.1.7, - any.versions ==3.5.4, + any.versions ==4.0.2, any.void ==0.7.3, void -safe, any.wai ==3.2.3, diff --git a/cabal.GHC-8.6.5.config b/cabal.GHC-8.6.5.config index 74ad13699b..d205d9ad06 100644 --- a/cabal.GHC-8.6.5.config +++ b/cabal.GHC-8.6.5.config @@ -186,7 +186,7 @@ constraints: any.Cabal ==2.4.0.1, language-c -allwarnings +iecfpextension +separatesyb +usebytestrings, any.lens ==4.19.2, lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.1, + any.libBF ==0.6.2, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, @@ -295,9 +295,9 @@ constraints: any.Cabal ==2.4.0.1, any.temporary ==1.3, any.terminal-size ==0.3.2.1, any.terminfo ==0.4.1.2, - any.text ==1.2.3.1, any.text-short ==0.1.3, text-short -asserts, + any.text ==1.2.4.0, any.tf-random ==0.5, any.th-abstraction ==0.3.2.0, any.th-compat ==0.1.1, @@ -335,7 +335,7 @@ constraints: any.Cabal ==2.4.0.1, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-binary-instances ==0.2.5.1, any.vector-th-unbox ==0.2.1.7, - any.versions ==3.5.4, + any.versions ==4.0.2, any.void ==0.7.3, void -safe, any.wai ==3.2.3, diff --git a/cabal.GHC-8.8.4.config b/cabal.GHC-8.8.4.config index c71f0de490..5e3c16e1a6 100644 --- a/cabal.GHC-8.8.4.config +++ b/cabal.GHC-8.8.4.config @@ -186,7 +186,7 @@ constraints: any.Cabal ==3.0.1.0, language-c -allwarnings +iecfpextension +separatesyb +usebytestrings, any.lens ==4.19.2, lens -benchmark-uniplate -dump-splices +inlining -j -old-inline-pragmas -safe +test-doctests +test-hunit +test-properties +test-templates +trustworthy, - any.libBF ==0.6.1, + any.libBF ==0.6.2, libBF -system-libbf, any.libyaml ==0.1.2, libyaml -no-unicode -system-libyaml, @@ -335,7 +335,7 @@ constraints: any.Cabal ==3.0.1.0, vector-algorithms +bench +boundschecks -internalchecks -llvm +properties -unsafechecks, any.vector-binary-instances ==0.2.5.1, any.vector-th-unbox ==0.2.1.7, - any.versions ==3.5.4, + any.versions ==4.0.2, any.void ==0.7.3, void -safe, any.wai ==3.2.3, diff --git a/deps/crucible b/deps/crucible index 72c8a8d3ca..e635f160a5 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 72c8a8d3caccb47848e0d58ab458e99887c0b83d +Subproject commit e635f160a5c5ec713505e871da24cd9f39b35667 diff --git a/deps/cryptol b/deps/cryptol index 6e3c0816b7..0abde1e55e 160000 --- a/deps/cryptol +++ b/deps/cryptol @@ -1 +1 @@ -Subproject commit 6e3c0816b7b72a610ede875c5fe93f5d1eec177e +Subproject commit 0abde1e55e4db85a054e8976c61531ca7d29137a diff --git a/deps/macaw b/deps/macaw index 7b27f83640..a58f1e25dd 160000 --- a/deps/macaw +++ b/deps/macaw @@ -1 +1 @@ -Subproject commit 7b27f836403e9d032cceed40a7a03381ae60aa0f +Subproject commit a58f1e25ddd450c212a72fbdfdb0961baa62dd01 diff --git a/deps/saw-core b/deps/saw-core index 430aa313a9..b9dd3d83d9 160000 --- a/deps/saw-core +++ b/deps/saw-core @@ -1 +1 @@ -Subproject commit 430aa313a9529df3e6608591c932083cc2f3b247 +Subproject commit b9dd3d83d9cbef4ecd90344b503555d2f32a7349 diff --git a/deps/what4 b/deps/what4 index 190c3a4dc9..84685adcad 160000 --- a/deps/what4 +++ b/deps/what4 @@ -1 +1 @@ -Subproject commit 190c3a4dc93dd4dcba5fdab818b20ac591345b87 +Subproject commit 84685adcade38884139dddd96d9773e553ca2a1c diff --git a/saw-remote-api/saw-remote-api.cabal b/saw-remote-api/saw-remote-api.cabal index bfd9aabd49..41f082159d 100644 --- a/saw-remote-api/saw-remote-api.cabal +++ b/saw-remote-api/saw-remote-api.cabal @@ -26,16 +26,7 @@ flag builtin-abc common warnings ghc-options: - -Weverything - -Wno-missing-exported-signatures - -Wno-missing-import-lists - -Wno-missed-specialisations - -Wno-all-missed-specialisations - -Wno-unsafe - -Wno-safe - -Wno-missing-local-signatures - -Wno-monomorphism-restriction - -Wno-implicit-prelude + -Wall -Wno-orphans common deps diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs index 8e923585a5..e6cca931a6 100644 --- a/src/SAWScript/Crucible/Common.hs +++ b/src/SAWScript/Crucible/Common.hs @@ -17,8 +17,6 @@ module SAWScript.Crucible.Common , sawCoreState ) where -import Data.IORef - import Lang.Crucible.Simulator (GenericExecutionFeature) import Lang.Crucible.Simulator.ExecutionTree (AbortedResult(..), GlobalPair) import Lang.Crucible.Simulator.CallFrame (SimFrame) @@ -55,7 +53,7 @@ newSAWCoreBackend sc = return sym sawCoreState :: Sym -> IO (SAWCoreState Nonce.GlobalNonceGenerator) -sawCoreState sym = onlineUserState <$> readIORef (W4.sbStateManager sym) +sawCoreState sym = pure (onlineUserState (W4.sbUserState sym)) ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc ann) -> AbortedResult Sym ext diff --git a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs index 567b2b123a..e5a5b48f46 100644 --- a/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/JVM/ResolveSetupValue.hs @@ -30,7 +30,6 @@ module SAWScript.Crucible.JVM.ResolveSetupValue import Control.Lens import qualified Control.Monad.Catch as X -import Data.IORef import qualified Data.BitVector.Sized as BV import Data.Map (Map) import qualified Data.Map as Map @@ -42,7 +41,6 @@ import qualified Cryptol.Utils.PP as Cryptol (pp) import qualified What4.BaseTypes as W4 import qualified What4.Interface as W4 -import qualified What4.Expr.Builder as W4 import qualified What4.ProgramLoc as W4 import Verifier.SAW.Rewriter @@ -54,7 +52,6 @@ import Verifier.SAW.Simulator.What4.ReturnTrip -- crucible import qualified Lang.Crucible.Simulator as Crucible (RegValue) -import qualified Lang.Crucible.Backend.Online as Crucible -- what4 import qualified What4.Partial as W4 @@ -271,7 +268,7 @@ resolveBitvectorTerm sym w tm = -- TODO: Instead of evaluating in SBV backend, just evaluate in W4 backend directly. resolveBoolTerm :: Sym -> Term -> IO (W4.Pred Sym) resolveBoolTerm sym tm = - do st <- Crucible.onlineUserState <$> readIORef (W4.sbStateManager sym) + do st <- sawCoreState sym let sc = saw_ctx st ss <- basic_ss sc tm' <- rewriteSharedTerm sc ss tm diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs index 4bca3ed153..e61b6575dc 100644 --- a/src/SAWScript/Crucible/LLVM/Builtins.hs +++ b/src/SAWScript/Crucible/LLVM/Builtins.hs @@ -1377,7 +1377,6 @@ baseCryptolType bt = case bt of Crucible.BaseBoolRepr -> pure $ Cryptol.tBit Crucible.BaseBVRepr w -> pure $ Cryptol.tWord (Cryptol.tNum (natValue w)) - Crucible.BaseNatRepr -> Nothing Crucible.BaseIntegerRepr -> pure $ Cryptol.tInteger Crucible.BaseArrayRepr {} -> Nothing Crucible.BaseFloatRepr _ -> Nothing diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs index e9ed04e2cb..9ef85d24d3 100644 --- a/src/SAWScript/Crucible/LLVM/Override.hs +++ b/src/SAWScript/Crucible/LLVM/Override.hs @@ -1785,7 +1785,7 @@ executeFreshPointer :: executeFreshPointer cc (AllocIndex i) = do let mkName base = W4.systemSymbol (base ++ show i ++ "!") sym = cc^.ccBackend - blk <- W4.freshConstant sym (mkName "blk") W4.BaseNatRepr + blk <- W4.freshNat sym (mkName "blk") off <- W4.freshConstant sym (mkName "off") (W4.BaseBVRepr Crucible.PtrWidth) return (Crucible.LLVMPointer blk off) diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs index c4e712bd66..8e79d3a1a5 100644 --- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs +++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs @@ -35,7 +35,7 @@ import qualified Control.Monad.Fail as Fail import Control.Monad.State import qualified Data.BitVector.Sized as BV import Data.Maybe (fromMaybe, listToMaybe, fromJust) -import Data.IORef + import Data.Map (Map) import qualified Data.Map as Map import qualified Data.Vector as V @@ -52,12 +52,10 @@ import Data.Parameterized.NatRepr import qualified What4.BaseTypes as W4 import qualified What4.Interface as W4 -import qualified What4.Expr.Builder as W4 import qualified Lang.Crucible.LLVM.Bytes as Crucible import qualified Lang.Crucible.LLVM.MemModel as Crucible import qualified Lang.Crucible.LLVM.Translation as Crucible -import qualified Lang.Crucible.Backend.Online as Crucible import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible import Verifier.SAW.Rewriter @@ -70,7 +68,7 @@ import Text.LLVM.DebugUtils as L import qualified Verifier.SAW.Simulator.SBV as SBV import qualified Data.SBV.Dynamic as SBV -import SAWScript.Crucible.Common (Sym) +import SAWScript.Crucible.Common (Sym, sawCoreState) import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..)) import SAWScript.Crucible.LLVM.MethodSpecIR @@ -371,7 +369,7 @@ resolveSAWPred :: IO (W4.Pred Sym) resolveSAWPred cc tm = do do let sym = cc^.ccBackend - st <- Crucible.onlineUserState <$> readIORef (W4.sbStateManager sym) + st <- sawCoreState sym let sc = saw_ctx st let ss = cc^.ccBasicSS tm' <- rewriteSharedTerm sc ss tm @@ -393,7 +391,7 @@ resolveSAWSymBV :: IO (W4.SymBV Sym w) resolveSAWSymBV cc w tm = do let sym = cc^.ccBackend - st <- Crucible.onlineUserState <$> readIORef (W4.sbStateManager sym) + st <- sawCoreState sym let sc = saw_ctx st let ss = cc^.ccBasicSS tm' <- rewriteSharedTerm sc ss tm @@ -436,7 +434,7 @@ resolveSAWTerm cc tp tm = Crucible.ptrToPtrVal <$> Crucible.llvmPointer_bv sym v _ -> fail ("Invalid bitvector width: " ++ show sz) Cryptol.TVSeq sz tp' -> - do st <- Crucible.onlineUserState <$> readIORef (W4.sbStateManager sym) + do st <- sawCoreState sym let sc = saw_ctx st sz_tm <- scNat sc (fromIntegral sz) tp_tm <- importType sc emptyEnv (Cryptol.tValTy tp') @@ -451,7 +449,7 @@ resolveSAWTerm cc tp tm = Cryptol.TVStream _tp' -> fail "resolveSAWTerm: invalid infinite stream type" Cryptol.TVTuple tps -> - do st <- Crucible.onlineUserState <$> readIORef (W4.sbStateManager sym) + do st <- sawCoreState sym let sc = saw_ctx st tms <- mapM (\i -> scTupleSelector sc tm i (length tps)) [1 .. length tps] vals <- zipWithM (resolveSAWTerm cc) tps tms @@ -483,7 +481,7 @@ scPtrWidthBvNat :: IO Term scPtrWidthBvNat cc n = do let sym = cc^.ccBackend - st <- Crucible.onlineUserState <$> readIORef (W4.sbStateManager sym) + st <- sawCoreState sym let sc = saw_ctx st w <- scNat sc $ natValue Crucible.PtrWidth scBvNat sc w =<< scNat sc (fromIntegral n) @@ -600,7 +598,7 @@ memArrayToSawCoreTerm :: memArrayToSawCoreTerm crucible_context endianess typed_term = do let sym = crucible_context ^. ccBackend let data_layout = Crucible.llvmDataLayout $ ccTypeCtx crucible_context - st <- Crucible.onlineUserState <$> readIORef (W4.sbStateManager sym) + st <- sawCoreState sym let saw_context = saw_ctx st byte_type_term <- importType saw_context emptyEnv $ Cryptol.tValTy $ Cryptol.TVSeq 8 Cryptol.TVBit diff --git a/src/SAWScript/X86Spec.hs b/src/SAWScript/X86Spec.hs index 192c0edf51..33791c58d6 100644 --- a/src/SAWScript/X86Spec.hs +++ b/src/SAWScript/X86Spec.hs @@ -80,7 +80,7 @@ import Data.Parameterized.Pair import Data.Foldable(foldlM, toList) import What4.Interface - (bvLit,isEq, Pred, notPred, orPred, natEq + (bvLit,isEq, Pred, notPred, orPred, natEq, freshNat , bvUle, truePred, natLit, asNat, andPred, userSymbol, freshConstant ) import What4.ProgramLoc @@ -448,7 +448,7 @@ freshVal sym t ptrOk nm = | ptrOk, Just Refl <- testEquality w (knownNat @64) -> do sn_base <- symName (nm ++ "_base") sn_off <- symName (nm ++ "_off") - base <- freshConstant sym sn_base BaseNatRepr + base <- freshNat sym sn_base off <- freshConstant sym sn_off (BaseBVRepr w) return (LLVMPointer base off) | otherwise -> do @@ -1175,7 +1175,7 @@ checkOverlaps sym = check (_, x2) = llvmPointerView p2 (b1,y1) = llvmPointerView q1 (_,y2) = llvmPointerView q2 - opt1 <- notPred sym =<< isEq sym a1 b1 + opt1 <- notPred sym =<< natEq sym a1 b1 opt2 <- bvUle sym x2 y1 opt3 <- bvUle sym y2 x1 ok <- orPred sym opt1 =<< orPred sym opt2 opt3