Set crucible timeout in saw-remote-api.

GaloisInc · Nov 24, 2021 · d927726 · d927726
1 parent 2c05dbc
commit d927726
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 1 deletion.
diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs
@@ -47,6 +47,7 @@ import Verifier.SAW.TypedTerm (TypedTerm, CryptolModule)
 
 import SAWScript.Crucible.LLVM.Builtins (CheckPointsToType)
 import SAWScript.Crucible.LLVM.X86 (defaultStackBaseAlign)
+import qualified SAWScript.Crucible.Common as CC (defaultSAWCoreBackendTimeout)
 import qualified SAWScript.Crucible.Common.MethodSpec as CMS (ProvedSpec, GhostGlobal)
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS (SomeLLVM, LLVMModule)
 import SAWScript.Options (Options(..), processEnv, defaultOptions)
@@ -224,6 +225,7 @@ initialState readFileFn =
                 , rwStackBaseAlign = defaultStackBaseAlign
                 , rwProofs = []
                 , rwPreservedRegs = []
+                , rwCrucibleTimeout = defaultSAWCoreBackendTimeout
                 }
      return (SAWState emptyEnv bic [] ro rw M.empty)
 

diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs
@@ -15,6 +15,7 @@ module SAWScript.Crucible.Common
   , SAWCruciblePersonality(..)
   , newSAWCoreBackend
   , newSAWCoreBackendWithTimeout
+  , defaultSAWCoreBackendTimeout
   , sawCoreState
   ) where
 
@@ -50,6 +51,9 @@ data SAWCruciblePersonality sym = SAWCruciblePersonality
 newSAWCoreBackend :: SC.SharedContext -> IO Sym
 newSAWCoreBackend sc = newSAWCoreBackendWithTimeout sc 0
 
+defaultSAWCoreBackendTimeout :: Integer
+defaultSAWCoreBackendTimeout = 10000
+
 newSAWCoreBackendWithTimeout :: SC.SharedContext -> Integer -> IO Sym
 newSAWCoreBackendWithTimeout sc timeout =
   do st <- newSAWCoreState sc

diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
@@ -82,6 +82,7 @@ import qualified Verifier.SAW.Cryptol.Prelude as CryptolSAW
 
 -- Crucible
 import qualified Lang.Crucible.JVM as CJ
+import qualified SAWScript.Crucible.Common as CC
 import qualified SAWScript.Crucible.Common.MethodSpec as CMS
 import qualified SAWScript.Crucible.JVM.BuiltinsJVM as CJ
 import           SAWScript.Crucible.LLVM.Builtins
@@ -486,7 +487,7 @@ buildTopLevelEnv proxy opts =
                    , rwWhat4Eval = False
                    , rwPreservedRegs = []
                    , rwStackBaseAlign = defaultStackBaseAlign
-                   , rwCrucibleTimeout = 10000
+                   , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout
                    }
        return (bic, ro0, rw0)