What4 eval3

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -1298,12 +1298,15 @@ setupLLVMCrucibleContext bic opts pathSat lm action =
                        return (gp^.Crucible.gpGlobals, st)
                      _ -> fail "simulator initialization failed!"
 
+               cacheRef <- newIORef mempty
+
                return
                   LLVMCrucibleContext{ _ccLLVMModule = lm
                                      , _ccBackend = sym
                                      , _ccLLVMSimContext = lsimctx
                                      , _ccLLVMGlobals = lglobals
                                      , _ccBasicSS = biBasicSS bic
+                                     , _ccUninterpCache = cacheRef
                                      }
           action cc
 

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -64,6 +64,7 @@ module SAWScript.Crucible.LLVM.MethodSpecIR
   , ccLLVMModuleTrans
   , ccLLVMContext
   , ccTypeCtx
+  , ccUninterpCache
     -- * PointsTo
   , LLVMPointsTo(..)
   , LLVMPointsToValue(..)
@@ -141,6 +142,7 @@ import           Verifier.SAW.Rewriter (Simpset)
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.TypedTerm
 
+import qualified Verifier.SAW.Simulator.What4 as W4SC
 
 --------------------------------------------------------------------------------
 -- ** Language features
@@ -321,6 +323,7 @@ data LLVMCrucibleContext arch =
   , _ccLLVMSimContext  :: Crucible.SimContext (Crucible.SAWCruciblePersonality Sym) Sym (CL.LLVM arch)
   , _ccLLVMGlobals     :: Crucible.SymGlobalState Sym
   , _ccBasicSS         :: Simpset
+  , _ccUninterpCache   :: IORef (W4SC.SymFnCache Sym)
   }
 
 makeLenses ''LLVMCrucibleContext

src/SAWScript/Crucible/LLVM/Override.hs

@@ -99,7 +99,6 @@ import qualified What4.Expr.Builder as W4
 import qualified What4.Interface as W4
 import qualified What4.LabeledPred as W4
 import qualified What4.ProgramLoc as W4
-import qualified What4.Symbol as W4
 
 import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
 import           SAWScript.Crucible.LLVM.CrucibleLLVM (LLVM)
@@ -1766,7 +1765,7 @@ executeFreshPointer ::
   AllocIndex      {- ^ SetupVar allocation ID -} ->
   IO (LLVMPtr (Crucible.ArchWidth arch)) {- ^ Symbolic pointer value -}
 executeFreshPointer cc (AllocIndex i) =
-  do let mkName base = W4.systemSymbol (base ++ show i ++ "!")
+  do let mkName base = W4.safeSymbol (base ++ show i)
          sym         = cc^.ccBackend
      blk <- W4.freshConstant sym (mkName "blk") W4.BaseNatRepr
      off <- W4.freshConstant sym (mkName "off") (W4.BaseBVRepr Crucible.PtrWidth)

src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs

@@ -31,8 +31,8 @@ import Control.Lens ((^.))
 import Control.Monad
 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 qualified Data.BitVector.Sized as BV
+import Data.Maybe (fromMaybe, listToMaybe, fromJust, isJust)
 import Data.IORef
 import           Data.Map (Map)
 import qualified Data.Map as Map
@@ -44,13 +44,17 @@ import qualified Text.LLVM.AST as L
 import qualified Cryptol.Eval.Type as Cryptol (TValue(..), tValTy, evalValType)
 import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..))
 import qualified Cryptol.Utils.PP as Cryptol (pp)
+import qualified Cryptol.Utils.Ident as Cryptol
 
 import           Data.Parameterized.Some (Some(..))
 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 What4.SWord as SW
+
+import qualified Verifier.SAW.Simulator.What4 as W4SC
 
 import qualified Lang.Crucible.LLVM.Bytes       as Crucible
 import qualified Lang.Crucible.LLVM.MemModel    as Crucible
@@ -60,13 +64,12 @@ import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as Crucible
 
 import Verifier.SAW.Rewriter
 import Verifier.SAW.SharedTerm
-import Verifier.SAW.Cryptol (importType, emptyEnv)
+import Verifier.SAW.Cryptol
+  (importType, emptyEnv, isCryptolModuleName, isCryptolInteractiveName)
 import Verifier.SAW.TypedTerm
+import qualified Verifier.SAW.Simulator.Value as Value
 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.MethodSpec (AllocIndex(..), SetupValue(..))
 
@@ -352,20 +355,25 @@ resolveSAWPred ::
   LLVMCrucibleContext arch ->
   Term ->
   IO (W4.Pred Sym)
-resolveSAWPred cc tm = do
+resolveSAWPred cc tm =
   do let sym = cc^.ccBackend
      sc <- Crucible.saw_ctx <$> readIORef (W4.sbStateManager sym)
      let ss = cc^.ccBasicSS
      tm' <- rewriteSharedTerm sc ss tm
-     mx <- case getAllExts tm' of
-             [] -> do
-               -- Evaluate in SBV to test whether 'tm' is a concrete value
-               sbv <- SBV.toBool <$> SBV.sbvSolveBasic sc Map.empty mempty tm'
-               return (SBV.svAsBool sbv)
-             _ -> return Nothing
-     case mx of
-       Just x  -> return $ W4.backendPred sym x
-       Nothing -> Crucible.bindSAWTerm sym W4.BaseBoolRepr tm'
+     modmap <- scGetModuleMap sc
+     let ref = cc^.ccUninterpCache
+
+     -- unfold names defined in the cryptol prelude, or defined locally
+     -- with let statements.
+     let ecFilter ec =
+             (isJust $ isCryptolModuleName Cryptol.preludeName $ ecName ec) ||
+             (isJust $ isCryptolInteractiveName $ ecName ec)
+
+     w4val <- W4SC.w4SimulatorEval sym sc modmap mempty ref ecFilter tm'
+     case w4val of
+       Right (Value.VBool x) -> return x
+       Left _nm -> Crucible.bindSAWTerm sym W4.BaseBoolRepr tm'
+       _ -> Crucible.bindSAWTerm sym W4.BaseBoolRepr tm'
 
 resolveSAWSymBV ::
   (1 <= w) =>
@@ -378,15 +386,20 @@ resolveSAWSymBV cc w tm =
      sc <- Crucible.saw_ctx <$> readIORef (W4.sbStateManager sym)
      let ss = cc^.ccBasicSS
      tm' <- rewriteSharedTerm sc ss tm
-     mx <- case getAllExts tm' of
-             [] -> do
-               -- Evaluate in SBV to test whether 'tm' is a concrete value
-               sbv <- SBV.toWord =<< SBV.sbvSolveBasic sc Map.empty mempty tm'
-               return (SBV.svAsInteger sbv)
-             _ -> return Nothing
-     case mx of
-       Just x  -> W4.bvLit sym w (BV.mkBV w x)
-       Nothing -> Crucible.bindSAWTerm sym (W4.BaseBVRepr w) tm'
+     modmap <- scGetModuleMap sc
+     let ref = cc^.ccUninterpCache
+
+     -- unfold names defined in the cryptol prelude, or defined locally
+     -- with let statements.
+     let ecFilter ec =
+             (isJust $ isCryptolModuleName Cryptol.preludeName $ ecName ec) ||
+             (isJust $ isCryptolInteractiveName $ ecName ec)
+
+     w4val <- W4SC.w4SimulatorEval sym sc modmap mempty ref ecFilter tm'
+     case w4val of
+       Right (Value.VWord (SW.DBV x)) | Just Refl <- testEquality w (W4.bvWidth x) -> return x
+       Left _nm -> Crucible.bindSAWTerm sym (W4.BaseBVRepr w) tm'
+       _ -> Crucible.bindSAWTerm sym (W4.BaseBVRepr w) tm'
 
 resolveSAWTerm ::
   Crucible.HasPtrWidth (Crucible.ArchWidth arch) =>

src/SAWScript/Crucible/LLVM/X86.hs

@@ -36,6 +36,7 @@ import Control.Monad.Catch (MonadThrow)
 
 import qualified Data.BitVector.Sized as BV
 import Data.Foldable (foldlM)
+import Data.IORef
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Vector as Vector
 import qualified Data.Text as Text
@@ -257,12 +258,15 @@ crucible_llvm_verify_x86 bic opts (Some (llvmModule :: LLVMModule x)) path nm gl
         else fail $ mconcat ["Address of \"", nm, "\" is not an absolute address"]
       let maxAddr = addrInt + toInteger (Macaw.segmentSize $ Macaw.segoffSegment addr)
 
+      ref <- liftIO $ newIORef mempty
+
       let
         cc :: LLVMCrucibleContext x
         cc = LLVMCrucibleContext
           { _ccLLVMModule = llvmModule
           , _ccBackend = sym
           , _ccBasicSS = biBasicSS bic
+          , _ccUninterpCache = ref
 
           -- It's unpleasant that we need to do this to use resolveSetupVal.
           , _ccLLVMSimContext = error "Attempted to access ccLLVMSimContext"