Evaluate saw-core terms into What4 more thoughougly when setting up

the symbolic simulator.  This currently breaks some tests, as there
are some constructs that cannot be handled by this new code path.

src/SAWScript/Crucible/LLVM/Builtins.hs

@@ -1299,12 +1299,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)
@@ -1753,7 +1752,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,13 @@ 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 Verifier.SAW.TypedAST
+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 +356,29 @@ 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 ->
+         do putStrLn ("Evaluation blocked on: " ++ show (toAbsoluteName nm))
+            Crucible.bindSAWTerm sym W4.BaseBoolRepr tm'
+
+       _ -> Crucible.bindSAWTerm sym W4.BaseBoolRepr tm'
 
 resolveSAWSymBV ::
   (1 <= w) =>
@@ -378,15 +391,24 @@ 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 ->
+         do putStrLn ("Evaluation blocked on: " ++ show (toAbsoluteName 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"