Merge pull request #506 from siddharthist/getglobalpair

Cleanup, enable & squash warnings

src/SAWScript/Crucible/Common/MethodSpec.hs

@@ -28,7 +28,6 @@ import           Data.List (isPrefixOf)
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Void (Void)
-import           Control.Monad.ST (RealWorld)
 import           Control.Monad.Trans.Maybe
 import           Control.Monad.Trans (lift)
 import           Control.Lens
@@ -40,9 +39,7 @@ import qualified Text.PrettyPrint.ANSI.Leijen as PP
 import           What4.ProgramLoc (ProgramLoc(plSourceLoc))
 
 import qualified Lang.Crucible.Types as Crucible
-  (IntrinsicType, EmptyCtx, SymbolRepr, knownSymbol)
-import qualified Lang.Crucible.Simulator.Intrinsics as Crucible
-  (IntrinsicClass(Intrinsic, muxIntrinsic), IntrinsicMuxFn(IntrinsicMuxFn))
+  (IntrinsicType, EmptyCtx)
 import qualified Lang.Crucible.CFG.Common as Crucible (GlobalVar)
 
 import qualified Cryptol.Utils.PP as Cryptol
@@ -54,8 +51,6 @@ import           SAWScript.Options
 import           SAWScript.Prover.SolverStats
 import           SAWScript.Utils (bullets)
 
-import           SAWScript.Crucible.Common
-
 -- | How many allocations have we made in this method spec?
 newtype AllocIndex = AllocIndex Int
   deriving (Eq, Ord, Show)

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -24,10 +24,6 @@ Stability   : provisional
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 
-{-# OPTIONS_GHC -fno-warn-unused-local-binds #-}
-{-# OPTIONS_GHC -fno-warn-unused-matches #-}
-
-
 module SAWScript.Crucible.JVM.Builtins
     ( crucible_jvm_verify
     , crucible_jvm_unsafe_assume_spec
@@ -207,7 +203,7 @@ crucible_jvm_verify bic opts cls nm lemmas checkSat setup tactic =
      pos <- getPosition
      let loc = SS.toW4Loc "_SAW_verify_prestate" pos
 
-     (cls', method) <- io $ findMethod cb pos nm cls -- TODO: switch to crucible-jvm version
+     (_cls', method) <- io $ findMethod cb pos nm cls -- TODO: switch to crucible-jvm version
      let st0 = initialCrucibleSetupState cc method loc
 
      -- execute commands of the method spec
@@ -252,7 +248,7 @@ crucible_jvm_unsafe_assume_spec bic opts cls nm setup =
      cb <- getJavaCodebase
      -- cls' is either cls or a subclass of cls
      pos <- getPosition
-     (cls', method) <- io $ findMethod cb pos nm cls -- TODO: switch to crucible-jvm version
+     (_cls', method) <- io $ findMethod cb pos nm cls -- TODO: switch to crucible-jvm version
      let loc = SS.toW4Loc "_SAW_assume_spec" pos
      let st0 = initialCrucibleSetupState cc method loc
      (view Setup.csMethodSpec) <$> execStateT (runJVMSetupM setup) st0
@@ -315,7 +311,6 @@ verifyPrestate ::
       Crucible.SymGlobalState Sym)
 verifyPrestate cc mspec globals0 =
   do let sym = cc^.jccBackend
-     let jc = cc^.jccJVMContext
      let preallocs = mspec ^. MS.csPreState . MS.csAllocs
      let tyenv = MS.csAllocations mspec
      let nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames
@@ -544,15 +539,14 @@ verifySimulate ::
   Crucible.SymGlobalState Sym   ->
   Bool {- ^ path sat checking -} ->
   IO (Maybe (J.Type, JVMVal), Crucible.SymGlobalState Sym)
-verifySimulate opts cc mspec args assumes top_loc lemmas globals checkSat =
+verifySimulate opts cc mspec args assumes top_loc lemmas globals _checkSat =
   do let jc = cc^.jccJVMContext
      let cb = cc^.jccCodebase
      let sym = cc^.jccBackend
      let cls = cc^.jccJVMClass
      let cname = J.className cls
      let mname = mspec ^. csMethodName
      let verbosity = simVerbose opts
-     let personality = Crucible.SAWCruciblePersonality
      let pos = SS.PosInternal "verifySimulate"
      let halloc = cc^.jccHandleAllocator
 
@@ -614,6 +608,8 @@ verifySimulate opts cc mspec args assumes top_loc lemmas globals checkSat =
                            , show resultDoc
                            ]
 
+       Crucible.TimeoutResult _cxt -> fail "Symbolic execution timed out."
+
   where
     prepareArg :: forall tp. Crucible.TypeRepr tp -> JVMVal -> IO (Crucible.RegValue Sym tp)
     prepareArg ty v =
@@ -774,9 +770,6 @@ setupDynamicClassTable sym jc = foldM addClass Map.empty (Map.assocs (CJ.classTa
 --------------------------------------------------------------------------------
 -- Setup builtins
 
-getCrucibleContext :: JVMSetup JVMCrucibleContext
-getCrucibleContext = view Setup.csCrucibleContext <$> get
-
 -- | Returns Cryptol type of actual type if it is an array or
 -- primitive type.
 cryptolTypeOfActual :: JavaType -> Maybe Cryptol.Type
@@ -820,8 +813,7 @@ jvm_fresh_var ::
   JVMSetupM TypedTerm {- ^ fresh typed term -}
 jvm_fresh_var bic _opts name jty =
   JVMSetupM $
-  do cctx <- getCrucibleContext
-     let sc = biSharedContext bic
+  do let sc = biSharedContext bic
      case cryptolTypeOfActual jty of
        Nothing -> fail $ "Unsupported type in jvm_fresh_var: " ++ show jty
        Just ty -> freshVariable sc name ty
@@ -876,20 +868,19 @@ jvm_field_is ::
   String     {- ^ field name -} ->
   SetupValue {- ^ field value -} ->
   JVMSetupM ()
-jvm_field_is typed _bic _opt ptr fname val =
+jvm_field_is _typed _bic _opt ptr fname val =
   JVMSetupM $
-  do cc <- getCrucibleContext
-     loc <- SS.toW4Loc "jvm_field_is" <$> lift getPosition
+  do loc <- SS.toW4Loc "jvm_field_is" <$> lift getPosition
      st <- get
      let rs = st ^. Setup.csResolvedState
      let path = Left fname
      if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [] rs
        then fail $ "Multiple points-to preconditions on same pointer (field " ++ fname ++ ")"
        else Setup.csResolvedState %= MS.markResolved ptr [path]
-     let env = MS.csAllocations (st ^. Setup.csMethodSpec)
-         nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
-     ptrTy <- typeOfSetupValue cc env nameEnv ptr
-     valTy <- typeOfSetupValue cc env nameEnv val
+     -- let env = MS.csAllocations (st ^. Setup.csMethodSpec)
+     --     nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
+     -- ptrTy <- typeOfSetupValue cc env nameEnv ptr
+     -- valTy <- typeOfSetupValue cc env nameEnv val
      --when typed (checkMemTypeCompatibility lhsTy valTy)
      Setup.addPointsTo (JVMPointsToField loc ptr fname val)
 
@@ -901,18 +892,17 @@ jvm_elem_is ::
   Int        {- ^ index -} ->
   SetupValue {- ^ element value -} ->
   JVMSetupM ()
-jvm_elem_is typed _bic _opt ptr idx val =
+jvm_elem_is _typed _bic _opt ptr idx val =
   JVMSetupM $
-  do cc <- getCrucibleContext
-     loc <- SS.toW4Loc "jvm_elem_is" <$> lift getPosition
+  do loc <- SS.toW4Loc "jvm_elem_is" <$> lift getPosition
      st <- get
      let rs = st ^. Setup.csResolvedState
      let path = Right idx
      if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [path] rs
        then fail "Multiple points-to preconditions on same pointer"
        else Setup.csResolvedState %= MS.markResolved ptr [path]
-     let env = MS.csAllocations (st ^. Setup.csMethodSpec)
-         nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
+     -- let env = MS.csAllocations (st ^. Setup.csMethodSpec)
+     --     nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
      Setup.addPointsTo (JVMPointsToElem loc ptr idx val)
 
 jvm_precond :: TypedTerm -> JVMSetupM ()

src/SAWScript/Crucible/JVM/Override.hs

@@ -24,6 +24,8 @@ Stability   : provisional
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 
+{-# OPTIONS_GHC -Wno-orphans #-} -- Pretty JVMVal
+
 module SAWScript.Crucible.JVM.Override
   ( OverrideMatcher(..)
   , runOverrideMatcher

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -23,10 +23,6 @@ Stability   : provisional
 
 {-# OPTIONS_GHC -Wno-orphans #-}
 
-{-# OPTIONS_GHC -fno-warn-unused-local-binds #-}
-{-# OPTIONS_GHC -fno-warn-unused-matches #-}
-
-
 module SAWScript.Crucible.LLVM.Builtins
     ( show_cfg
     , crucible_execute_func
@@ -282,11 +278,10 @@ createMethodSpec verificationArgs bic opts lm@(LLVMModule _ _ mtrans) nm setup =
 
   let ?lc = mtrans ^. Crucible.transContext . Crucible.llvmTypeCtx
 
-  Crucible.llvmPtrWidth (mtrans ^. Crucible.transContext) $ \ptrW ->
+  Crucible.llvmPtrWidth (mtrans ^. Crucible.transContext) $ \_ ->
     fmap NE.head $ forM defOrDecls $ \defOrDecl -> do
       setupLLVMCrucibleContext bic opts lm $ \cc -> do
         let sym = cc^.ccBackend
-        let llmod = cc^.ccLLVMModule
 
         pos <- getPosition
         let setupLoc = toW4Loc "_SAW_verify_prestate" pos
@@ -455,8 +450,6 @@ verifyPrestate ::
 verifyPrestate cc mspec globals = do
   let ?lc = cc^.ccTypeCtx
   let sym = cc^.ccBackend
-  let nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames
-
   let prestateLoc = W4.mkProgramLoc "_SAW_verify_prestate" W4.InternalPos
   liftIO $ W4.setCurrentProgramLoc sym prestateLoc
 
@@ -606,13 +599,13 @@ assertEqualVals cc v1 v2 =
 
 --------------------------------------------------------------------------------
 
--- TODO: combine with/move to executeAllocation?
+-- TODO(langston): combine with/move to executeAllocation
 doAlloc ::
   (?lc :: Crucible.TypeContext, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
   LLVMCrucibleContext arch       ->
   LLVMAllocSpec ->
   StateT MemImpl IO (LLVMPtr (Crucible.ArchWidth arch))
-doAlloc cc (LLVMAllocSpec mut memTy sz loc) = StateT $ \mem ->
+doAlloc cc (LLVMAllocSpec mut _memTy sz loc) = StateT $ \mem ->
   do let sym = cc^.ccBackend
      let dl = Crucible.llvmDataLayout ?lc
      sz' <- W4.bvLit sym Crucible.PtrWidth $ Crucible.bytesToInteger sz
@@ -804,13 +797,9 @@ verifySimulate opts cc mspec args assumes top_loc lemmas globals checkSat =
              Crucible.regValue <$> (Crucible.callBlock cfg entryId args')
     res <- Crucible.executeCrucible execFeatures initExecState
     case res of
-      Crucible.FinishedResult _ pr ->
+      Crucible.FinishedResult _ partialResult ->
         do Crucible.GlobalPair retval globals1 <-
-             case pr of
-               Crucible.TotalRes gp -> return gp
-               Crucible.PartialRes _ _ gp _ ->
-                 do printOutLn opts Info "Symbolic simulation completed with side conditions."
-                    return gp
+             getGlobalPair opts partialResult
            let ret_ty = mspec ^. MS.csRet
            retval' <- case ret_ty of
              Nothing -> return Nothing
@@ -1351,7 +1340,6 @@ crucible_alloc_internal _bic _opt lty spec = do
   cctx <- getLLVMCrucibleContext
   let ?lc = cctx ^. ccTypeCtx
   let ?dl = Crucible.llvmDataLayout ?lc
-  loc <- getW4Position "crucible_alloc_internal"
   n <- Setup.csVarCounter <<%= nextAllocIndex
   Setup.currentState . MS.csAllocs . at n ?= spec
   -- TODO: refactor

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -490,6 +490,7 @@ typeOfLLVMVal _dl val =
     Crucible.LLVMValStruct flds -> Crucible.mkStructType (fmap fieldType flds)
     Crucible.LLVMValArray tp vs -> Crucible.arrayType (fromIntegral (V.length vs)) tp
     Crucible.LLVMValZero tp     -> tp
+    Crucible.LLVMValUndef tp    -> tp
   where
     fieldType (f, _) = (f ^. Crucible.fieldVal, Crucible.fieldPad f)