Merge branch 'master' into T1085

GaloisInc · Feb 23, 2021 · ec00437 · ec00437
2 parents 785db6e + 1b314f1
commit ec00437
Show file tree

Hide file tree

Showing 15 changed files with 27 additions and 44 deletions.
diff --git 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
@@ -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
@@ -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
diff --git a/deps/cryptol b/deps/cryptol
diff --git a/deps/macaw b/deps/macaw
diff --git a/deps/saw-core b/deps/saw-core
diff --git a/deps/what4 b/deps/what4
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
+1 −1		crucible-go/src/Lang/Crucible/Go/Builtin.hs
+7 −0		crucible-go/src/Lang/Crucible/Go/TransUtil.hs
+3 −3		crucible-llvm/src/Lang/Crucible/LLVM/MemModel.hs
+2 −2		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Generic.hs
+5 −3		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/MemLog.hs
+3 −3		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Partial.hs
+4 −2		crucible-llvm/src/Lang/Crucible/LLVM/MemModel/Pointer.hs
+2 −2		crucible-llvm/src/Lang/Crucible/LLVM/Translation/Instruction.hs
+13 −8		crucible-syntax/src/Lang/Crucible/Syntax/Concrete.hs
+2 −2		crucible-syntax/test-data/parser-tests/natural.out.good
+14 −14		crucible-syntax/test-data/simulator-tests/loop-err.out.good
+2 −2		crucible-syntax/test-data/simulator-tests/loop.out.good
+2 −2		crucible-wasm/src/Lang/Crucible/Wasm/Memory.hs
+1 −0		crucible/src/Lang/Crucible/Analysis/Fixpoint.hs
+1 −0		crucible/src/Lang/Crucible/Analysis/ForwardDataflow.hs
+17 −0		crucible/src/Lang/Crucible/Backend.hs
+9 −26		crucible/src/Lang/Crucible/Backend/Online.hs
+1 −2		crucible/src/Lang/Crucible/Backend/Simple.hs
+8 −0		crucible/src/Lang/Crucible/CFG/Core.hs
+15 −19		crucible/src/Lang/Crucible/CFG/Expr.hs
+7 −0		crucible/src/Lang/Crucible/CFG/Reg.hs
+8 −0		crucible/src/Lang/Crucible/CFG/SSAConversion.hs
+5 −0		crucible/src/Lang/Crucible/Simulator/EvalStmt.hs
+11 −2		crucible/src/Lang/Crucible/Simulator/Evaluation.hs
+0 −1		crucible/src/Lang/Crucible/Simulator/RegMap.hs
+1 −0		crucible/src/Lang/Crucible/Simulator/RegValue.hs
+8 −3		crucible/src/Lang/Crucible/Types.hs
+1 −0		crucible/src/Lang/Crucible/Utils/CoreRewrite.hs
+0 −2		crux-llvm/crux-llvm.cabal
+56 −25		crux-llvm/src/Crux/LLVM/Compile.hs
+10 −0		crux-llvm/src/Crux/LLVM/Config.hs
+3 −5		crux-llvm/src/Crux/LLVM/Simulate.hs
+2 −2		crux-llvm/src/CruxLLVMMain.hs
+49 −54		crux-llvm/svcomp/Main.hs
+1 −9		crux-llvm/test-data/golden/golden/vector-cmp.good
+4 −4		crux-mir/src/Mir/Intrinsics.hs
+1 −2		crux-mir/src/Mir/Overrides.hs
+0 −2		crux-mir/src/Mir/Trans.hs
+1 −1		crux/crux.cabal
+21 −2		crux/src/Crux/Config/Common.hs
+17 −27		crux/src/Crux/Model.hs
+1 −1		dependencies/what4
+27 −1		.github/workflows/nightly.yml
+3 −3		cabal.GHC-8.10.2.config
+3 −3		cabal.GHC-8.10.3.config
+4 −2		cabal.GHC-8.6.5.config
+3 −1		cabal.GHC-8.8.4.config
+28 −5		cryptol-remote-api/Dockerfile
+1 −1		cryptol-remote-api/docs/Cryptol.rst
+46 −0		cryptol-remote-api/ghc-portability.patch
+1 −2		cryptol.cabal
+6 −0		cryptol/Main.hs
+ −		docs/ProgrammingCryptol.pdf
+3 −3		docs/ProgrammingCryptol/technicalities/TechAppendix.tex
+48 −4		lib/Float.cry
+37 −7		src/Cryptol/Backend.hs
+42 −2		src/Cryptol/Backend/Concrete.hs
+3 −3		src/Cryptol/Backend/FloatHelpers.hs
+17 −0		src/Cryptol/Backend/SBV.hs
+28 −3		src/Cryptol/Backend/What4.hs
+0 −362		src/Cryptol/Backend/What4/SFloat.hs
+2 −54		src/Cryptol/Eval/Concrete.hs
+69 −1		src/Cryptol/Eval/Generic.hs
+1 −57		src/Cryptol/Eval/What4.hs
+30 −30		src/Cryptol/Parser/ParserUtils.hs
+10 −10		src/Cryptol/REPL/Command.hs
+36 −29		src/Cryptol/REPL/Monad.hs
+6 −5		src/Cryptol/REPL/Trie.hs
+1 −1		src/Cryptol/Symbolic/SBV.hs
+3 −3		src/Cryptol/Symbolic/What4.hs
+47 −22		src/Cryptol/Testing/Random.hs
+6 −10		src/Cryptol/TypeCheck/Depends.hs
+3 −1		src/Cryptol/TypeCheck/Infer.hs
+6 −0		tests/issues/issue1040.cry
+1 −0		tests/issues/issue1040.icry
+7 −0		tests/issues/issue1040.icry.stdout
+5 −0		tests/issues/issue1044.icry
+17 −0		tests/issues/issue1044.icry.stdout
+1 −0		tests/issues/issue1049.icry
+3 −0		tests/issues/issue1049.icry.stdout
+3 −0		tests/issues/issue975.icry
+13 −0		tests/issues/issue975.icry.stdout
+2 −5		tests/regression/FloatTests.cry
+2 −6		tests/regression/float.icry
+8 −2		tests/regression/float.icry.stdout
+108 −0		.github/ci.sh
+13 −0		.github/workflows/ci.yaml
+68 −61		cabal.project.dist.ghc-8.10.2.freeze
+69 −52		cabal.project.dist.ghc-8.6.5.freeze
+74 −57		cabal.project.dist.ghc-8.8.4.freeze
+1 −1		deps/asl-translator
+1 −1		deps/crucible
+1 −1		deps/llvm-pretty-bc-parser
+1 −1		deps/semmc
+1 −1		deps/what4
+1 −1		deps/what4-serialize
+6 −5		macaw-semmc/macaw-semmc.cabal
+44 −9		macaw-semmc/src/Data/Macaw/SemMC/TH.hs
+1 −4		refinement/src/Data/Macaw/Refinement/SymbolicExecution.hs
+0 −1		refinement/tests/RefinementTests.hs
+1 −1		symbolic/macaw-symbolic.cabal
+8 −1		symbolic/src/Data/Macaw/Symbolic/MemOps.hs
+0 −1		symbolic/src/Data/Macaw/Symbolic/Memory.hs
+1 −1		x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
+1 −1		rme/README.md
+1 −1		saw-core-sbv/saw-core-sbv.cabal
+0 −2		saw-core-what4/src/Verifier/SAW/Simulator/What4/FirstOrder.hs
+13 −119		saw-core-what4/src/Verifier/SAW/Simulator/What4/ReturnTrip.hs
+22 −8		.github/workflows/test.yml
+1 −34		what4-abc/src/What4/Solver/ABC.hs
+27 −0		what4/CHANGES.md
+1 −1		what4/README.md
+25 −0		what4/solverBounds.config
+0 −7		what4/src/What4/BaseTypes.hs
+0 −8		what4/src/What4/Concrete.hs
+42 −37		what4/src/What4/Config.hs
+0 −1		what4/src/What4/Expr.hs
+775 −159		what4/src/What4/Expr/App.hs
+2 −24		what4/src/What4/Expr/AppTheory.hs
+256 −919		what4/src/What4/Expr/Builder.hs
+113 −101		what4/src/What4/Expr/GroundEval.hs
+28 −54		what4/src/What4/Expr/MATLAB.hs
+1 −0		what4/src/What4/Expr/Simplify.hs
+2 −2		what4/src/What4/Expr/VarIdentification.hs
+0 −7		what4/src/What4/Expr/WeightedSum.hs
+7 −8		what4/src/What4/IndexLit.hs
+275 −137		what4/src/What4/Interface.hs
+3 −3		what4/src/What4/InterpretedFloatingPoint.hs
+6 −0		what4/src/What4/Protocol/Online.hs
+39 −62		what4/src/What4/Protocol/SMTLib2.hs
+30 −122		what4/src/What4/Protocol/SMTWriter.hs
+1 −14		what4/src/What4/Protocol/VerilogWriter/Backend.hs
+455 −0		what4/src/What4/SFloat.hs
+1 −26		what4/src/What4/SemiRing.hs
+1 −1		what4/src/What4/Solver/Adapter.hs
+1 −1		what4/src/What4/Solver/CVC4.hs
+2 −10		what4/src/What4/Solver/Yices.hs
+1 −1		what4/src/What4/Solver/Z3.hs
+41 −191		what4/src/What4/Utils/AbstractDomains.hs
+106 −0		what4/src/What4/Utils/FloatHelpers.hs
+35 −0		what4/src/What4/Utils/OnlyIntRepr.hs
+0 −35		what4/src/What4/Utils/OnlyNatRepr.hs
+15 −16		what4/src/What4/Utils/StringLiteral.hs
+85 −0		what4/src/What4/Utils/Versions.hs
+44 −49		what4/test/ExprBuilderSMTLib2.hs
+15 −20		what4/test/ExprsTest.hs
+84 −91		what4/test/GenWhat4Expr.hs
+21 −21		what4/test/IteExprs.hs
+815 −0		what4/test/TestTemplate.hs
+37 −9		what4/what4.cabal