Remove some unused BuiltinContext and Options parameters.

Removing those parameters also necessitated the addition of
a `roBasicSS` field to the `TopLevelRO` datatype.

Fixes #945.

saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs

@@ -33,7 +33,6 @@ import SAWScript.Crucible.JVM.Builtins
 import SAWScript.Crucible.JVM.BuiltinsJVM
 import qualified SAWScript.Crucible.JVM.MethodSpecIR as CMS
 import SAWScript.JavaExpr (JavaType(..))
-import SAWScript.Options (defaultOptions)
 import SAWScript.Value (BuiltinContext, JVMSetupM(..), biSharedContext)
 import qualified Verifier.SAW.CryptolEnv as CEnv
 import Verifier.SAW.CryptolEnv (CryptolEnv)
@@ -96,19 +95,19 @@ interpretJVMSetup ::
   JVMSetupM ()
 interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty, cenv0) *> pure ()
   where
-    go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return bic opts
+    go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= jvm_return
     -- TODO: do we really want two names here?
     go (SetupFresh name@(ServerName n) debugName ty) =
-      do t <- lift $ jvm_fresh_var bic opts (T.unpack debugName) ty
+      do t <- lift $ jvm_fresh_var (T.unpack debugName) ty
          (env, cenv) <- get
          put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv)
          save name (Val (MS.SetupTerm t))
     go (SetupAlloc name ty _ (Just _)) =
       error "attempted to allocate a Java object with alignment information"
     go (SetupAlloc name (JavaArray n ty) True Nothing) =
-      lift (jvm_alloc_array bic opts n ty) >>= save name . Val
+      lift (jvm_alloc_array n ty) >>= save name . Val
     go (SetupAlloc name (JavaClass c) True Nothing) =
-      lift (jvm_alloc_object bic opts c) >>= save name . Val
+      lift (jvm_alloc_object c) >>= save name . Val
     go (SetupAlloc name ty False Nothing) =
       error $ "cannot allocate type: " ++ show ty
     go (SetupPointsTo src tgt) = get >>= \env -> lift $
@@ -117,13 +116,12 @@ interpretJVMSetup fileReader bic cenv0 ss = runStateT (traverse_ go ss) (mempty,
          error "nyi: points-to"
     go (SetupExecuteFunction args) =
       get >>= \env ->
-      lift $ traverse (getSetupVal env) args >>= jvm_execute_func bic opts
+      lift $ traverse (getSetupVal env) args >>= jvm_execute_func
     go (SetupPrecond p) = get >>= \env -> lift $
       getTypedTerm env p >>= jvm_precond
     go (SetupPostcond p) = get >>= \env -> lift $
       getTypedTerm env p >>= jvm_postcond
 
-    opts = defaultOptions
     save name val = modify' (\(env, cenv) -> (Map.insert name val env, cenv))
 
     getSetupVal ::
@@ -190,7 +188,6 @@ jvmLoadClass (JVMLoadClassParams serverName cname) =
      case tasks of
        (_:_) -> raise $ notAtTopLevel $ map fst tasks
        [] ->
-         do bic <- view sawBIC <$> getState
-            c <- tl $ loadJavaClass bic cname
+         do c <- tl $ loadJavaClass cname
             setServerVal serverName c
             ok

saw-remote-api/src/SAWServer/JVMVerify.hs

@@ -12,7 +12,6 @@ import qualified Language.JVM.Common as JVM
 
 import SAWScript.Crucible.JVM.Builtins
 import SAWScript.JavaExpr (JavaType(..))
-import SAWScript.Options (defaultOptions)
 import SAWScript.Value (rwCryptol)
 
 import Argo
@@ -44,9 +43,9 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc
               VerifyContract -> do
                 lemmas <- mapM getJVMMethodSpecIR lemmaNames
                 proofScript <- interpretProofScript script
-                tl $ crucible_jvm_verify bic defaultOptions cls fun lemmas checkSat setup proofScript
+                tl $ crucible_jvm_verify cls fun lemmas checkSat setup proofScript
               AssumeContract ->
-                tl $ crucible_jvm_unsafe_assume_spec bic defaultOptions cls fun setup
+                tl $ crucible_jvm_unsafe_assume_spec cls fun setup
             dropTask
             setServerVal lemmaName res
             ok

saw-remote-api/src/SAWServer/LLVMCrucibleSetup.hs

@@ -45,7 +45,6 @@ import SAWScript.Crucible.LLVM.Builtins
     , crucible_precond
     , crucible_postcond )
 import qualified SAWScript.Crucible.LLVM.MethodSpecIR as CMS
-import SAWScript.Options (defaultOptions)
 import SAWScript.Value (BuiltinContext, LLVMCrucibleSetupM(..), biSharedContext)
 import qualified Verifier.SAW.CryptolEnv as CEnv
 import Verifier.SAW.CryptolEnv (CryptolEnv)
@@ -109,28 +108,28 @@ interpretLLVMSetup ::
 interpretLLVMSetup fileReader bic cenv0 ss =
   runStateT (traverse_ go ss) (mempty, cenv0) *> pure ()
   where
-    go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= crucible_return bic defaultOptions
+    go (SetupReturn v) = get >>= \env -> lift $ getSetupVal env v >>= crucible_return
     -- TODO: do we really want two names here?
     go (SetupFresh name@(ServerName n) debugName ty) =
-      do t <- lift $ crucible_fresh_var bic defaultOptions (T.unpack debugName) ty
+      do t <- lift $ crucible_fresh_var (T.unpack debugName) ty
          (env, cenv) <- get
          put (env, CEnv.bindTypedTerm (mkIdent n, t) cenv)
          save name (Val (CMS.anySetupTerm t))
     go (SetupAlloc name ty True Nothing) =
-      lift (crucible_alloc bic defaultOptions ty) >>= save name . Val
+      lift (crucible_alloc ty) >>= save name . Val
     go (SetupAlloc name ty False Nothing) =
-      lift (crucible_alloc_readonly bic defaultOptions ty) >>= save name . Val
+      lift (crucible_alloc_readonly ty) >>= save name . Val
     go (SetupAlloc name ty True (Just align)) =
-      lift (crucible_alloc_aligned bic defaultOptions align ty) >>= save name . Val
+      lift (crucible_alloc_aligned align ty) >>= save name . Val
     go (SetupAlloc name ty False (Just align)) =
-      lift (crucible_alloc_readonly_aligned bic defaultOptions align ty) >>= save name . Val
+      lift (crucible_alloc_readonly_aligned align ty) >>= save name . Val
     go (SetupPointsTo src tgt) = get >>= \env -> lift $
       do ptr <- getSetupVal env src
          tgt' <- getSetupVal env tgt
-         crucible_points_to True bic defaultOptions ptr tgt'
+         crucible_points_to True ptr tgt'
     go (SetupExecuteFunction args) =
       get >>= \env ->
-      lift $ traverse (getSetupVal env) args >>= crucible_execute_func bic defaultOptions
+      lift $ traverse (getSetupVal env) args >>= crucible_execute_func
     go (SetupPrecond p) = get >>= \env -> lift $
       getTypedTerm env p >>= crucible_precond
     go (SetupPostcond p) = get >>= \env -> lift $

saw-remote-api/src/SAWServer/LLVMVerify.hs

@@ -11,7 +11,6 @@ import Control.Lens
 
 import SAWScript.Crucible.LLVM.Builtins
 import SAWScript.Crucible.LLVM.X86
-import SAWScript.Options (defaultOptions)
 import SAWScript.Value (rwCryptol)
 
 import Argo
@@ -43,9 +42,9 @@ llvmVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scr
               VerifyContract -> do
                 lemmas <- mapM getLLVMMethodSpecIR lemmaNames
                 proofScript <- interpretProofScript script
-                tl $ crucible_llvm_verify bic defaultOptions mod fun lemmas checkSat setup proofScript
+                tl $ crucible_llvm_verify mod fun lemmas checkSat setup proofScript
               AssumeContract ->
-                tl $ crucible_llvm_unsafe_assume_spec bic defaultOptions mod fun setup
+                tl $ crucible_llvm_unsafe_assume_spec mod fun setup
             dropTask
             setServerVal lemmaName res
             ok
@@ -72,7 +71,7 @@ llvmVerifyX86 (X86VerifyParams modName objName fun globals _lemmaNames checkSat
             proofScript <- interpretProofScript script
             fileReader <- getFileReader
             setup <- compileLLVMContract fileReader bic cenv <$> traverse getExpr contract
-            res <- tl $ crucible_llvm_verify_x86 bic defaultOptions mod objName fun allocs checkSat setup proofScript
+            res <- tl $ crucible_llvm_verify_x86 mod objName fun allocs checkSat setup proofScript
             dropTask
             setServerVal lemmaName res
             ok

src/SAWScript/Crucible/Common/Setup/Builtins.hs

@@ -19,7 +19,6 @@ import qualified What4.ProgramLoc as W4
 
 import           Verifier.SAW.TypedTerm (TypedTerm)
 
-import           SAWScript.Options (Options)
 import           SAWScript.Value
 
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
@@ -51,22 +50,18 @@ crucible_postcond loc p = do
   addCondition (MS.SetupCond_Pred loc p)
 
 crucible_return ::
-  BuiltinContext ->
-  Options ->
   MS.SetupValue ext ->
   CrucibleSetup ext ()
-crucible_return _bic _opt retval = do
+crucible_return retval = do
   ret <- use (csMethodSpec . MS.csRetValue)
   case ret of
     Just _ -> fail "crucible_return: duplicate return value specification"
     Nothing -> csMethodSpec . MS.csRetValue .= Just retval
 
 crucible_execute_func ::
-  BuiltinContext ->
-  Options ->
   [MS.SetupValue ext] ->
   CrucibleSetup ext ()
-crucible_execute_func _bic _opt args = do
+crucible_execute_func args = do
   tps <- use (csMethodSpec . MS.csArgs)
   csPrePost .= MS.PostState
   csMethodSpec . MS.csArgBindings .= Map.fromList [ (i, (t,a))