Unused fields in SAWScript.JavaMethodSpec.VerifyParams

[RyanGlScott]

The VerifyParams data types is currently defined as:

saw-script/src/SAWScript/JavaMethodSpec.hs

Lines 427 to 433 in 21565d7

	data VerifyParams = VerifyParams
	{ vpCode :: Codebase
	, vpContext :: SharedContext
	, vpOpts :: Options
	, vpSpec :: JavaMethodSpecIR
	, vpOver :: [JavaMethodSpecIR]
	}

Of these fields, only vpOpts and vpSpec are ever used anywhere (in runValidation). As a proof of concept, it's possible to remove the other fields entirely:

diff --git a/src/SAWScript/JavaBuiltins.hs b/src/SAWScript/JavaBuiltins.hs
index d763b5b2..e9884b65 100644
--- a/src/SAWScript/JavaBuiltins.hs
+++ b/src/SAWScript/JavaBuiltins.hs
@@ -219,13 +219,7 @@ verifyJava cls mname overrides setup = do
   let pos = fixPos -- TODO
   setupRes <- runJavaSetup pos cb cls mname setup
   let ms = jsSpec setupRes
-      vp = VerifyParams {
-             vpCode = cb
-           , vpContext = sc
-           , vpOpts = opts
-           , vpSpec = ms
-           , vpOver = overrides
-           }
+      vp = VerifyParams { vpOpts = opts, vpSpec = ms }
   when (jsSimulate setupRes) $ do
     let overrideText =
           case overrides of
@@ -260,10 +254,9 @@ verifyJava cls mname overrides setup = do
                 SS.Unsat _ -> liftIO $ printOutLn opts Debug "Valid."
                 SS.SatMulti _ vals ->
                        io $ showCexResults opts sc (rwPPOpts rw) ms vs exts vals
-        let ovds = vpOver vp
         initPS <- initializeVerification' sc ms bs cl
-        liftIO $ printOutLn opts Debug $ "Overriding: " ++ show (map specName ovds)
-        mapM_ (overrideFromSpec sc (specPos ms)) ovds
+        liftIO $ printOutLn opts Debug $ "Overriding: " ++ show (map specName overrides)
+        mapM_ (overrideFromSpec sc (specPos ms)) overrides
         liftIO $ printOutLn opts Debug $ "Running method: " ++ specName ms
         -- Execute code.
         run
diff --git a/src/SAWScript/JavaMethodSpec.hs b/src/SAWScript/JavaMethodSpec.hs
index 706d5e5e..0375652c 100644
--- a/src/SAWScript/JavaMethodSpec.hs
+++ b/src/SAWScript/JavaMethodSpec.hs
@@ -425,11 +425,8 @@ overrideFromSpec de pos ir
        key = methodKey method
 
 data VerifyParams = VerifyParams
-  { vpCode    :: Codebase
-  , vpContext :: SharedContext
-  , vpOpts    :: Options
-  , vpSpec    :: JavaMethodSpecIR
-  , vpOver    :: [JavaMethodSpecIR]
+  { vpOpts :: Options
+  , vpSpec :: JavaMethodSpecIR
   }
 
 type SymbolicRunHandler =

In fact, runValidation is the only function that uses VerifyParams at all (as far as I can tell), so it might even be worthwhile to just remove the data type in favor of passing the arguments directly:

-runValidation :: Prover -> VerifyParams -> SymbolicRunHandler
+runValidation :: Prover -> Options -> JavaMethodSpecIR -> SymbolicRunHandler

[RyanGlScott]

Some further digging reveals that the biJavaCodebase field of BuiltinContext also goes unused.

[brianhuffman]

You may be interested in #1005, which will make all of this code go away :)

[RyanGlScott]

Nice! I suppose that means that the only task remaining after #1005 would be to remove biJavaCodebase. Perhaps I can find a way to put that in a PR that covers similar territory.

[brianhuffman]

#1005 made this problem go away.