Merge pull request #997 from GaloisInc/saw-what4-refactor

Refactor SAWCore<->What4 connection

saw-script.cabal

@@ -40,7 +40,6 @@ library
     , crucible >= 0.4
     , crucible-jvm
     , crucible-llvm >= 0.2
-    , crucible-saw
     , deepseq
     , either
     , exceptions

src/SAWScript/Builtins.hs

@@ -52,8 +52,6 @@ import System.Process (callCommand, readProcessWithExitCode)
 import Text.Printf (printf)
 import Text.Read (readMaybe)
 
-import What4.Expr(FloatModeRepr(..))
-
 import qualified Verifier.SAW.Cryptol as Cryptol
 import qualified Verifier.SAW.Cryptol.Simpset as Cryptol
 
@@ -90,12 +88,7 @@ import qualified Verifier.SAW.Simulator.SBV as SBVSim
 
 -- saw-core-what4
 import qualified Verifier.SAW.Simulator.What4 as W4Sim
-
--- parameterized-utils
-import Data.Parameterized.Nonce
-
--- crucible-saw
-import qualified Lang.Crucible.Backend.SAWCore as Crucible (newSAWCoreBackend, toSC)
+import qualified Verifier.SAW.Simulator.What4.ReturnTrip as W4Sim
 
 -- sbv
 import qualified Data.SBV.Dynamic as SBV
@@ -141,6 +134,7 @@ import qualified SAWScript.Prover.What4 as Prover
 import qualified SAWScript.Prover.Exporter as Prover
 import qualified SAWScript.Prover.MRSolver as Prover
 import SAWScript.VerificationSummary
+import SAWScript.Crucible.Common as Common
 
 showPrim :: SV.Value -> TopLevel String
 showPrim v = do
@@ -542,6 +536,7 @@ goal_eval unints =
   withFirstGoal $ \goal ->
   do sc <- getSharedContext
      unintSet <- resolveNames unints
+
      -- replace all pi-bound quantified variables with new free variables
      let (args, body) = asPiList (unProp (goalProp goal))
      body' <-
@@ -551,10 +546,12 @@ goal_eval unints =
      ecs <- liftIO $ traverse (\(nm, ty) -> scFreshEC sc (Text.unpack nm) ty) args
      vars <- liftIO $ traverse (scExtCns sc) ecs
      t0 <- liftIO $ instantiateVarList sc 0 (reverse vars) body'
-     let gen = globalNonceGenerator
-     sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen
-     (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym sc Map.empty unintSet t0
-     t1 <- liftIO $ Crucible.toSC sym p
+
+     sym <- liftIO $ Common.newSAWCoreBackend sc
+     st <- liftIO $ Common.sawCoreState sym
+     (_names, (_mlabels, p)) <- liftIO $ W4Sim.w4Eval sym st sc Map.empty unintSet t0
+     t1 <- liftIO $ W4Sim.toSC sym st p
+
      t2 <- liftIO $ scEqTrue sc t1
      -- turn the free variables we generated back into pi-bound variables
      t3 <- liftIO $ scGeneralizeExts sc ecs t2

src/SAWScript/Crucible/Common.hs

@@ -12,25 +12,50 @@ module SAWScript.Crucible.Common
   ( ppAbortedResult
   , Sym
   , setupProfiling
+  , SAWCruciblePersonality(..)
+  , newSAWCoreBackend
+  , sawCoreState
   ) where
 
+import           Data.IORef
+
 import           Lang.Crucible.Simulator (GenericExecutionFeature)
 import           Lang.Crucible.Simulator.ExecutionTree (AbortedResult(..), GlobalPair)
 import           Lang.Crucible.Simulator.CallFrame (SimFrame)
 import           Lang.Crucible.Simulator.Profiling
 import           Lang.Crucible.Backend (AbortExecReason(..), ppAbortExecReason, IsSymInterface)
-import           Lang.Crucible.Backend.SAWCore (SAWCoreBackend)
+import           Lang.Crucible.Backend.Online
 import qualified Data.Parameterized.Nonce as Nonce
 import qualified What4.Solver.Yices as Yices
+import qualified What4.Config as W4
 import qualified What4.Expr as W4
+import qualified What4.Interface as W4
+import qualified What4.Expr.Builder as W4
 import qualified What4.ProgramLoc as W4 (plSourceLoc)
 
 import System.Directory (createDirectoryIfMissing)
 import System.FilePath ((</>))
 import qualified Prettyprinter as PP
 
+
+import Verifier.SAW.SharedTerm as SC
+import Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState, newSAWCoreState)
+
 -- | The symbolic backend we use for SAW verification
-type Sym = SAWCoreBackend Nonce.GlobalNonceGenerator Yices.Connection (W4.Flags W4.FloatReal)
+type Sym = OnlineBackendUserSt Nonce.GlobalNonceGenerator Yices.Connection SAWCoreState (W4.Flags W4.FloatReal)
+
+data SAWCruciblePersonality sym = SAWCruciblePersonality
+
+
+newSAWCoreBackend :: SC.SharedContext -> IO Sym
+newSAWCoreBackend sc =
+  do st <- newSAWCoreState sc
+     sym <- newOnlineBackend W4.FloatRealRepr Nonce.globalNonceGenerator Yices.yicesDefaultFeatures st
+     W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym)
+     return sym
+
+sawCoreState :: Sym -> IO (SAWCoreState Nonce.GlobalNonceGenerator)
+sawCoreState sym = onlineUserState <$> readIORef (W4.sbStateManager sym)
 
 ppAbortedResult :: (forall l args. GlobalPair Sym (SimFrame Sym ext l args) -> PP.Doc ann)
                 -> AbortedResult Sym ext

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -49,7 +49,6 @@ import           Control.Monad.Trans.Except (runExceptT)
 import qualified Data.BitVector.Sized as BV
 import           Data.Foldable (for_)
 import           Data.Function
-import           Data.IORef
 import           Data.List
 import           Data.Map (Map)
 import qualified Data.Map as Map
@@ -74,7 +73,6 @@ import qualified Cryptol.Utils.PP as Cryptol (pp)
 import qualified What4.Partial as W4
 import qualified What4.ProgramLoc as W4
 import qualified What4.Interface as W4
-import qualified What4.Expr.Builder as W4
 import qualified What4.Utils.StringLiteral as W4S
 
 -- jvm-parser
@@ -83,7 +81,6 @@ import qualified Language.JVM.Common as J (dotsToSlashes)
 
 -- crucible
 import qualified Lang.Crucible.Backend as Crucible
-import qualified Lang.Crucible.Backend.SAWCore as Crucible
 import qualified Lang.Crucible.CFG.Core as Crucible (TypeRepr(..))
 import qualified Lang.Crucible.FunctionHandle as Crucible
 import qualified Lang.Crucible.Simulator as Crucible
@@ -95,14 +92,15 @@ import qualified Lang.Crucible.JVM as CJ
 
 -- parameterized-utils
 import           Data.Parameterized.Classes
-import           Data.Parameterized.Nonce
 import qualified Data.Parameterized.Context as Ctx
 
 import Verifier.SAW.FiniteValue (ppFirstOrderValue)
 import Verifier.SAW.SharedTerm
 import Verifier.SAW.Recognizer
 import Verifier.SAW.TypedTerm
 
+import Verifier.SAW.Simulator.What4.ReturnTrip
+
 import SAWScript.Proof
 import SAWScript.Prover.SolverStats
 import SAWScript.TopLevel
@@ -115,7 +113,7 @@ import SAWScript.Crucible.JVM.BuiltinsJVM (prepareClassTopLevel)
 import SAWScript.JavaExpr (JavaType(..))
 
 import qualified SAWScript.Crucible.Common as Common
-import           SAWScript.Crucible.Common (Sym)
+import           SAWScript.Crucible.Common
 import           SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), nextAllocIndex, PrePost(..))
 
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
@@ -131,10 +129,10 @@ type CrucibleMethodSpecIR = MS.CrucibleMethodSpecIR CJ.JVM
 type SetupCondition = MS.SetupCondition CJ.JVM
 
 -- TODO: something useful with the global pair?
-ppAbortedResult :: JVMCrucibleContext
+ppJVMAbortedResult :: JVMCrucibleContext
                 -> Crucible.AbortedResult Sym a
                 -> Doc ann
-ppAbortedResult _cc = Common.ppAbortedResult (\_gp -> mempty)
+ppJVMAbortedResult _cc = Common.ppAbortedResult (\_gp -> mempty)
 
 -- FIXME: We need a better way to identify a set of class names to
 -- load. This function has two problems: First, unless we put in a
@@ -205,7 +203,7 @@ jvm_verify cls nm lemmas checkSat setup tactic =
      let loc = SS.toW4Loc "_SAW_verify_prestate" pos
 
      profFile <- rwProfilingFile <$> getTopLevelRW
-     (writeFinalProfile, pfs) <- io $ Common.setupProfiling sym "jvm_verify" profFile
+     (writeFinalProfile, pfs) <- io $ setupProfiling sym "jvm_verify" profFile
 
      (cls', method) <- io $ findMethod cb pos nm cls -- TODO: switch to crucible-jvm version
      let st0 = initialCrucibleSetupState cc (cls', method) loc
@@ -266,8 +264,8 @@ verifyObligations ::
   TopLevel SolverStats
 verifyObligations cc mspec tactic assumes asserts =
   do let sym = cc^.jccBackend
-     st <- io $ readIORef $ W4.sbStateManager sym
-     let sc = Crucible.saw_ctx st
+     st <- io $ sawCoreState sym
+     let sc = saw_ctx st
      assume <- io $ scAndList sc (toListOf (folded . Crucible.labeledPred) assumes)
      let nm = mspec ^. csMethodName
      stats <- forM (zip [(0::Int)..] asserts) $ \(n, (msg, assert)) -> do
@@ -441,7 +439,7 @@ setupPrePointsTos mspec cc env pts mem0 = foldM doPointsTo mem0 pts
              rhs' <- injectSetupVal rhs
              CJ.doArrayStore sym mem lhs' idx rhs'
         JVMPointsToArray _loc lhs rhs ->
-          do sc <- Crucible.saw_ctx <$> readIORef (W4.sbStateManager sym)
+          do sc <- saw_ctx <$> sawCoreState sym
              let lhs' = lookupAllocIndex env lhs
              (_ety, tts) <-
                destVecTypedTerm sc rhs >>=
@@ -487,7 +485,9 @@ assertEqualVals ::
   JVMVal ->
   IO Term
 assertEqualVals cc v1 v2 =
-  Crucible.toSC (cc^.jccBackend) =<< equalValsPred cc v1 v2
+  do let sym = cc^.jccBackend
+     st <- sawCoreState sym
+     toSC sym st =<< equalValsPred cc v1 v2
 
 --------------------------------------------------------------------------------
 
@@ -518,16 +518,17 @@ getMethodHandle jc (JVMMethodId mkey cname) =
 registerOverride ::
   Options ->
   JVMCrucibleContext ->
-  Crucible.SimContext (Crucible.SAWCruciblePersonality Sym) Sym CJ.JVM ->
+  Crucible.SimContext (SAWCruciblePersonality Sym) Sym CJ.JVM ->
   W4.ProgramLoc ->
   [CrucibleMethodSpecIR] ->
-  Crucible.OverrideSim (Crucible.SAWCruciblePersonality Sym) Sym CJ.JVM rtp args ret ()
+  Crucible.OverrideSim (SAWCruciblePersonality Sym) Sym CJ.JVM rtp args ret ()
 registerOverride opts cc _ctx top_loc cs =
   do let sym = cc^.jccBackend
      let jc = cc^.jccJVMContext
      let c0 = head cs
      let method = c0 ^. MS.csMethod
-     sc <- Crucible.saw_ctx <$> liftIO (readIORef (W4.sbStateManager sym))
+
+     sc <- saw_ctx <$> liftIO (sawCoreState sym)
 
      mhandle <- liftIO $ getMethodHandle jc method
      case mhandle of
@@ -578,7 +579,7 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat =
      regmap <- prepareArgs (Crucible.handleArgTypes h) (map snd args)
      res <-
        do let feats = pfs
-          let simctx = CJ.jvmSimContext sym halloc stdout jc verbosity Crucible.SAWCruciblePersonality
+          let simctx = CJ.jvmSimContext sym halloc stdout jc verbosity SAWCruciblePersonality
           let simSt = Crucible.InitialState simctx globals Crucible.defaultAbortHandler (Crucible.handleReturnType h)
           let fnCall = Crucible.regValue <$> Crucible.callFnVal (Crucible.HandleFnVal h) regmap
           let overrideSim =
@@ -616,7 +617,7 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat =
             return (retval', globals1)
 
        Crucible.AbortedResult _ ar ->
-         do let resultDoc = ppAbortedResult cc ar
+         do let resultDoc = ppJVMAbortedResult cc ar
             fail $ unlines [ "Symbolic execution failed."
                            , show resultDoc
                            ]
@@ -693,11 +694,12 @@ verifyPoststate cc mspec env0 globals ret =
   where
     sym = cc^.jccBackend
 
-    verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError _loc err))) = do
-      hypTerm    <- scAndList sc =<< mapM (Crucible.toSC sym) (toListOf (folded . Crucible.labeledPred) hyps)
-      conclTerm  <- Crucible.toSC sym concl
-      obligation <- scImplies sc hypTerm conclTerm
-      return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, obligation)
+    verifyObligation sc (Crucible.ProofGoal hyps (Crucible.LabeledPred concl (Crucible.SimError _loc err))) =
+      do st         <- sawCoreState sym
+         hypTerm    <- scAndList sc =<< mapM (toSC sym st) (toListOf (folded . Crucible.labeledPred) hyps)
+         conclTerm  <- toSC sym st concl
+         obligation <- scImplies sc hypTerm conclTerm
+         return ("safety assertion: " ++ Crucible.simErrorReasonMsg err, obligation)
 
     matchResult opts sc =
       case (ret, mspec ^. MS.csRetValue) of
@@ -713,8 +715,7 @@ setupCrucibleContext jclass =
      jc <- getJVMTrans
      cb <- getJavaCodebase
      sc <- getSharedContext
-     let gen = globalNonceGenerator
-     sym <- io $ Crucible.newSAWCoreBackend W4.FloatRealRepr sc gen
+     sym <- io $ newSAWCoreBackend sc
      opts <- getOptions
      io $ CJ.setSimulatorVerbosity (simVerbose opts) sym
 

src/SAWScript/Crucible/JVM/BuiltinsJVM.hs

@@ -42,8 +42,6 @@ import           Control.Monad.State.Strict
 import qualified Data.Parameterized.Map as MapF
 import qualified Data.Parameterized.Nonce as Nonce
 
--- crucible/crucible-saw
-import qualified Lang.Crucible.Backend.SAWCore         as CrucibleSAW
 -- crucible/crucible
 import qualified Lang.Crucible.FunctionHandle          as Crucible
 import qualified Lang.Crucible.Simulator.Operations    as Crucible
@@ -71,10 +69,14 @@ import Verifier.SAW.SharedTerm(Term, SharedContext, mkSharedContext, scImplies)
 -- cryptol-saw-core
 import Verifier.SAW.TypedTerm (TypedTerm(..), abstractTypedExts)
 
+-- saw-core-what4
+import Verifier.SAW.Simulator.What4.ReturnTrip
+
 -- saw-script
 import SAWScript.Builtins(fixPos)
 import SAWScript.Value
 import SAWScript.Options(Options,simVerbose)
+import SAWScript.Crucible.Common
 import SAWScript.Crucible.LLVM.Builtins (setupArg, setupArgs, getGlobalPair, runCFG, baseCryptolType)
 
 -- jvm-verifier
@@ -162,14 +164,15 @@ jvm_extract c mname = do
   ctx <- getJVMTrans
 
   io $ do -- only the IO monad, nothing else
-          sym <- CrucibleSAW.newSAWCoreBackend W4.FloatRealRepr sc gen
+          sym <- newSAWCoreBackend sc
+          st  <- sawCoreState sym
           CJ.setSimulatorVerbosity verbosity sym
 
           (CJ.JVMHandleInfo _m2 h) <- CJ.findMethodHandle ctx mcls meth
 
           (ecs, args) <- setupArgs sc sym h
 
-          res <- CJ.runMethodHandle sym CrucibleSAW.SAWCruciblePersonality halloc
+          res <- CJ.runMethodHandle sym SAWCruciblePersonality halloc
                      ctx verbosity className h args
 
           case res of
@@ -178,7 +181,7 @@ jvm_extract c mname = do
               let regval = gp^.Crucible.gpValue
               let regty = Crucible.regType regval
               let failure = fail $ unwords ["Unexpected return type:", show regty]
-              t <- Crucible.asSymExpr regval (CrucibleSAW.toSC sym) failure
+              t <- Crucible.asSymExpr regval (toSC sym st) failure
               cty <-
                 case Crucible.asBaseType regty of
                   Crucible.NotBaseType -> failure