From c09af32371e26168c86750cd8221fd4f6d903261 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 28 Oct 2020 10:02:14 -0700 Subject: [PATCH 1/6] JVM MethodSpec type stores a typed `MethodKey` instead of just a name. --- src/SAWScript/Crucible/JVM/MethodSpecIR.hs | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs index 35b773dbc6..79a90e39d7 100644 --- a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs @@ -73,19 +73,25 @@ type instance MS.ExtType CJ.JVM = J.Type data JVMMethodId = JVMMethodId - { _jvmMethodName :: String + { _jvmMethodKey :: J.MethodKey , _jvmClassName :: J.ClassName } deriving (Eq, Ord, Show) makeLenses ''JVMMethodId -csMethodName :: Lens' (MS.CrucibleMethodSpecIR CJ.JVM) String +jvmMethodName :: Getter JVMMethodId String +jvmMethodName = jvmMethodKey . to J.methodKeyName + +csMethodKey :: Lens' (MS.CrucibleMethodSpecIR CJ.JVM) J.MethodKey +csMethodKey = MS.csMethod . jvmMethodKey + +csMethodName :: Getter (MS.CrucibleMethodSpecIR CJ.JVM) String csMethodName = MS.csMethod . jvmMethodName instance PPL.Pretty JVMMethodId where - pretty (JVMMethodId methName className) = - PPL.text (concat [J.unClassName className ,".", methName]) + pretty (JVMMethodId methKey className) = + PPL.text (concat [J.unClassName className ,".", J.methodKeyName methKey]) type instance MS.MethodId CJ.JVM = JVMMethodId @@ -158,7 +164,7 @@ initialDefCrucibleMethodSpecIR :: ProgramLoc -> MS.CrucibleMethodSpecIR CJ.JVM initialDefCrucibleMethodSpecIR cb cname method loc = - let methId = JVMMethodId (J.methodName method) cname + let methId = JVMMethodId (J.methodKey method) cname retTy = J.methodReturnType method argTys = thisType ++ J.methodParameterTypes method in MS.makeCrucibleMethodSpecIR methId argTys retTy loc cb From c523fbb0fa23703ff57b35fde80748e9f1119b2f Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 31 Oct 2020 12:48:41 -0700 Subject: [PATCH 2/6] Avoid redundant call to `findMethod` in JVM verification code. --- src/SAWScript/Crucible/JVM/Builtins.hs | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index a16628b454..4ceeb1c3ec 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -497,6 +497,15 @@ doAlloc cc alloc = -------------------------------------------------------------------------------- +getMethodHandle :: CJ.JVMContext -> J.ClassName -> J.MethodKey -> IO CJ.JVMHandleInfo +getMethodHandle jc cname mkey = + case Map.lookup (cname, mkey) (CJ.methodHandles jc) of + Just handle -> return handle + Nothing -> + fail $ + "BUG: cannot find handle for " ++ J.unClassName cname ++ + "/" ++ J.methodKeyName mkey + registerOverride :: Options -> JVMCrucibleContext -> @@ -506,16 +515,13 @@ registerOverride :: Crucible.OverrideSim (Crucible.SAWCruciblePersonality Sym) Sym CJ.JVM rtp args ret () registerOverride opts cc _ctx top_loc cs = do let sym = cc^.jccBackend - let cb = cc^.jccCodebase let jc = cc^.jccJVMContext let c0 = head cs let cname = c0 ^. MS.csMethod . jvmClassName - let mname = c0 ^. csMethodName - let pos = SS.PosInternal "registerOverride" + let mkey = c0 ^. csMethodKey sc <- Crucible.saw_ctx <$> liftIO (readIORef (W4.sbStateManager sym)) - (mcls, meth) <- liftIO $ findMethod cb pos mname =<< lookupClass cb pos cname - mhandle <- liftIO $ CJ.findMethodHandle jc mcls meth + mhandle <- liftIO $ getMethodHandle jc cname mkey case mhandle of -- LLVMHandleInfo constructor has two existential type arguments, -- which are bound here. h :: FnHandle args' ret' @@ -545,13 +551,11 @@ verifySimulate :: IO (Maybe (J.Type, JVMVal), Crucible.SymGlobalState Sym) verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat = do let jc = cc^.jccJVMContext - let cb = cc^.jccCodebase let sym = cc^.jccBackend let cls = cc^.jccJVMClass let cname = J.className cls - let mname = mspec ^. csMethodName + let mkey = mspec ^. csMethodKey let verbosity = simVerbose opts - let pos = SS.PosInternal "verifySimulate" let halloc = cc^.jccHandleAllocator -- executeCrucibleJVM @@ -561,11 +565,10 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat = CJ.setSimulatorVerbosity verbosity sym - (mcls, meth) <- findMethod cb pos mname =<< lookupClass cb pos cname --when (not (J.methodIsStatic meth)) $ do -- fail $ unlines [ "Crucible can only extract static methods" ] - (CJ.JVMHandleInfo _ h) <- CJ.findMethodHandle jc mcls meth + (CJ.JVMHandleInfo _ h) <- getMethodHandle jc cname mkey regmap <- prepareArgs (Crucible.handleArgTypes h) (map snd args) res <- do let feats = pfs From 50e5b1664773af9e745198945ccdea1cc95c7090 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 31 Oct 2020 13:51:01 -0700 Subject: [PATCH 3/6] Allow disambiguation of JVM methods by appending type descriptors. Fixes #212. Previously `crucible_jvm_verify` and related commands would fail to verify methods whose names were not unique. However, JVM allows multiple methods to coexist in the same class as long as their types are distinct. This change now allows users to optionally add a type descriptor to a method name to specify a particular method with a given name. For example "foo(L)V" indicates method "foo" with a long argument and void result type. --- src/SAWScript/Utils.hs | 40 ++++++++++++++++++++++++++++++++++------ 1 file changed, 34 insertions(+), 6 deletions(-) diff --git a/src/SAWScript/Utils.hs b/src/SAWScript/Utils.hs index cc08e14914..aedfbd85a5 100644 --- a/src/SAWScript/Utils.hs +++ b/src/SAWScript/Utils.hs @@ -10,6 +10,7 @@ Stability : provisional {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE LambdaCase #-} module SAWScript.Utils where @@ -120,9 +121,15 @@ lookupClass cb site nm = do -- | Returns method with given name in this class or one of its subclasses. -- Throws an ExecException if method could not be found or is ambiguous. findMethod :: JSS.Codebase -> Pos -> String -> JSS.Class -> IO (JSS.Class, JSS.Method) -findMethod cb site nm initClass = impl initClass +findMethod cb site nm initClass = + do putStrLn $ "findMethod " ++ show nm + impl initClass where javaClassName = JSS.slashesToDots (JSS.unClassName (JSS.className initClass)) - methodMatches m = JSS.methodName m == nm && not (JSS.methodIsAbstract m) + methodType m = (JSS.methodParameterTypes m, JSS.methodReturnType m) + baseName m = JSS.methodName m + typedName m = JSS.methodName m ++ unparseMethodDescriptor (methodType m) + methodMatches m = + nm `elem` [baseName m, typedName m] && not (JSS.methodIsAbstract m) impl cl = case filter methodMatches (JSS.classMethods cl) of [] -> do @@ -135,10 +142,10 @@ findMethod cb site nm initClass = impl initClass Just superName -> impl =<< lookupClass cb site superName [method] -> return (cl,method) - _ -> let msg = "The method " ++ nm ++ " in class " ++ javaClassName - ++ " is ambiguous. SAWScript currently requires that " - ++ "method names are unique." - res = "Please rename the Java method so that it is unique." + l -> let msg = "The method " ++ show nm ++ " in class " ++ javaClassName ++ " is ambiguous. " ++ + "Methods can be disambiguated by appending a type descriptor: " ++ + unlines [ show (typedName m) | m <- l ] + res = "Please disambiguate method name." in throwIOExecException site (ftext msg) res throwFieldNotFound :: JSS.Type -> String -> ExceptT String IO a @@ -200,3 +207,24 @@ exitProofFalse,exitProofUnknown,exitProofSuccess :: IO a exitProofFalse = exitWith (ExitFailure 1) exitProofUnknown = exitWith (ExitFailure 2) exitProofSuccess = exitSuccess + +-------------------------------------------------------------------------------- + +unparseTypeDescriptor :: JSS.Type -> String +unparseTypeDescriptor = + \case + JSS.ArrayType ty -> "[" ++ unparseTypeDescriptor ty + JSS.BooleanType -> "Z" + JSS.ByteType -> "B" + JSS.CharType -> "C" + JSS.ClassType cn -> "L" ++ JSS.unClassName cn ++ ";" + JSS.DoubleType -> "D" + JSS.FloatType -> "F" + JSS.IntType -> "I" + JSS.LongType -> "J" + JSS.ShortType -> "S" + +unparseMethodDescriptor :: ([JSS.Type], Maybe JSS.Type) -> String +unparseMethodDescriptor (args, ret) = + "(" ++ concatMap unparseTypeDescriptor args ++ ")" ++ + maybe "V" unparseTypeDescriptor ret From e18a372ddf4865452f7b01a5dbe9558ac2d1de20 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 31 Oct 2020 14:21:27 -0700 Subject: [PATCH 4/6] Add test for #212. --- intTests/test_jvm_method_names/Makefile | 2 + intTests/test_jvm_method_names/Test.class | Bin 0 -> 884 bytes intTests/test_jvm_method_names/Test.java | 29 +++++++ intTests/test_jvm_method_names/test.saw | 94 ++++++++++++++++++++++ intTests/test_jvm_method_names/test.sh | 1 + 5 files changed, 126 insertions(+) create mode 100644 intTests/test_jvm_method_names/Makefile create mode 100644 intTests/test_jvm_method_names/Test.class create mode 100644 intTests/test_jvm_method_names/Test.java create mode 100644 intTests/test_jvm_method_names/test.saw create mode 100644 intTests/test_jvm_method_names/test.sh diff --git a/intTests/test_jvm_method_names/Makefile b/intTests/test_jvm_method_names/Makefile new file mode 100644 index 0000000000..94675b9b1f --- /dev/null +++ b/intTests/test_jvm_method_names/Makefile @@ -0,0 +1,2 @@ +%.class: %.java + javac -g $< diff --git a/intTests/test_jvm_method_names/Test.class b/intTests/test_jvm_method_names/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..dbc3738f8c1d69d0a3d6a82296821d51b2c38277 GIT binary patch literal 884 zcmZ{g&rZTX5XNVr3jIStz`u~_5iyaA7bEea!DxscG~5^5XbqI4R^kirI37$iCLVkM zAIkX6w$_@|5VkwB-~49g`}}(UAfi2LT4d0gNqJf?&_;n8g7Pyt79`FDEp|QM3lEWM zZ4U$)N7HL1sNDB_b^b6Js^Cfv$H-Ls(~%qxWZ-ceCynsdy9c9xrS8K6RJYC;A|CmA zs;{RY->6XY(a!YzQJ^NuN5*VLb*!^4rw_qM^*runGH&-y&ZI*HDmt`4iy(4VP=)iI zvGi{`7sER>3TX?Q8Q4_d4<*hb?kL1*BI@Fu->mi0zsw zrk29|Oe3hCm~{jUn-yU;voOoRto*xFKH(F%F%N*=2^rw(AHB#C$Y&%Y^u|8 gY*Q~Lx|+CyZL^pS7~f1W-Gu3aSprL73-);R8(yPTW&i*H literal 0 HcmV?d00001 diff --git a/intTests/test_jvm_method_names/Test.java b/intTests/test_jvm_method_names/Test.java new file mode 100644 index 0000000000..72555ad92d --- /dev/null +++ b/intTests/test_jvm_method_names/Test.java @@ -0,0 +1,29 @@ +class Test +{ + long val; + + public Test() { + val = 0; + } + public Test(long x) { + val = x; + } + public Test(int x) { + val = x; + } + public long get() { + return val; + } + public void increment() { + val = val + 1; + } + public void increment(long x) { + val = val + x; + } + public void increment(int x) { + val = val + (long)x; + } + public void increment(Test x) { + val = val + x.val; + } +} diff --git a/intTests/test_jvm_method_names/test.saw b/intTests/test_jvm_method_names/test.saw new file mode 100644 index 0000000000..c8d48e9638 --- /dev/null +++ b/intTests/test_jvm_method_names/test.saw @@ -0,0 +1,94 @@ +enable_experimental; +c <- java_load_class "Test"; + +crucible_jvm_verify c "get" [] false + do { + this <- jvm_alloc_object "Test"; + val <- jvm_fresh_var "val" java_long; + jvm_field_is this "Test.val" (jvm_term val); + jvm_execute_func [this]; + jvm_return (jvm_term val); + } + z3; + + +print "********************************************************************************"; +// FIXME: saw-script can't verify constructor functions +fails ( +crucible_jvm_verify c "Test(L)V" [] false + do { + x <- jvm_fresh_var "x" java_long; + jvm_execute_func [jvm_term x]; + this <- jvm_alloc_object "Test"; + jvm_field_is this "Test.val" (jvm_term x); + jvm_return this; + } + z3); + +print "********************************************************************************"; +print "increment"; +fails ( +crucible_jvm_verify c "increment" [] false + do { + this <- jvm_alloc_object "Test"; + val <- jvm_fresh_var "val" java_long; + jvm_field_is this "Test.val" (jvm_term val); + jvm_execute_func [this]; + jvm_field_is this "Test.val" (jvm_term {{ val + 1 }}); + } + z3); + +print "********************************************************************************"; +print "increment()V"; +crucible_jvm_verify c "increment()V" [] false + do { + this <- jvm_alloc_object "Test"; + val <- jvm_fresh_var "val" java_long; + jvm_field_is this "Test.val" (jvm_term val); + jvm_execute_func [this]; + jvm_field_is this "Test.val" (jvm_term {{ val + 1 }}); + } + z3; + +print "********************************************************************************"; +print "increment(J)V"; +crucible_jvm_verify c "increment(J)V" [] false + do { + this <- jvm_alloc_object "Test"; + val <- jvm_fresh_var "val" java_long; + jvm_field_is this "Test.val" (jvm_term val); + x <- jvm_fresh_var "x" java_long; + jvm_execute_func [this, jvm_term x]; + jvm_field_is this "Test.val" (jvm_term {{ val + x }}); + } + z3; + +print "********************************************************************************"; +print "increment(I)V"; +crucible_jvm_verify c "increment(I)V" [] false + do { + this <- jvm_alloc_object "Test"; + val <- jvm_fresh_var "val" java_long; + jvm_field_is this "Test.val" (jvm_term val); + x <- jvm_fresh_var "x" java_int; + jvm_execute_func [this, jvm_term x]; + jvm_field_is this "Test.val" (jvm_term {{ val + sext x }}); + } + z3; + +print "********************************************************************************"; +print "increment(LTest;)V"; +crucible_jvm_verify c "increment(LTest;)V" [] false + do { + this <- jvm_alloc_object "Test"; + val <- jvm_fresh_var "val" java_long; + jvm_field_is this "Test.val" (jvm_term val); + + x <- jvm_alloc_object "Test"; + x_val <- jvm_fresh_var "x_val" java_long; + jvm_field_is x "Test.val" (jvm_term x_val); + + jvm_execute_func [this, x]; + jvm_field_is this "Test.val" (jvm_term {{ val + x_val }}); + } + z3; diff --git a/intTests/test_jvm_method_names/test.sh b/intTests/test_jvm_method_names/test.sh new file mode 100644 index 0000000000..0b864017cd --- /dev/null +++ b/intTests/test_jvm_method_names/test.sh @@ -0,0 +1 @@ +$SAW test.saw From eff77407e0736cc52495faac0a8813ea37f2c828 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 31 Oct 2020 14:23:56 -0700 Subject: [PATCH 5/6] List known JVM method names in method-not-found error message. --- src/SAWScript/Utils.hs | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Utils.hs b/src/SAWScript/Utils.hs index aedfbd85a5..dd45a6897d 100644 --- a/src/SAWScript/Utils.hs +++ b/src/SAWScript/Utils.hs @@ -128,15 +128,17 @@ findMethod cb site nm initClass = methodType m = (JSS.methodParameterTypes m, JSS.methodReturnType m) baseName m = JSS.methodName m typedName m = JSS.methodName m ++ unparseMethodDescriptor (methodType m) - methodMatches m = - nm `elem` [baseName m, typedName m] && not (JSS.methodIsAbstract m) + methodMatches m = nm `elem` [baseName m, typedName m] impl cl = - case filter methodMatches (JSS.classMethods cl) of + let candidates = filter (not . JSS.methodIsAbstract) (JSS.classMethods cl) in + case filter methodMatches candidates of [] -> do case JSS.superClass cl of Nothing -> let msg = ftext $ "Could not find method " ++ nm - ++ " in class " ++ javaClassName ++ "." + ++ " in class " ++ javaClassName ++ ".\n" + ++ "Available methods: " + ++ unlines [ show (baseName m) | m <- candidates ] res = "Please check that the class and method are correct." in throwIOExecException site msg res Just superName -> From 02c19548ff57e5fad207864a7cae92703006e469 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Sat, 31 Oct 2020 15:05:53 -0700 Subject: [PATCH 6/6] Extend #212 test to also verify constructor methods. These are referred to by the name "", which is what they are called in the JVM class file. Like other methods, they can be used with type descriptors to disambiguate when constructors are defined at multiple types. --- intTests/test_jvm_method_names/test.saw | 43 +++++++++++++++++++++---- 1 file changed, 37 insertions(+), 6 deletions(-) diff --git a/intTests/test_jvm_method_names/test.saw b/intTests/test_jvm_method_names/test.saw index c8d48e9638..a466627e11 100644 --- a/intTests/test_jvm_method_names/test.saw +++ b/intTests/test_jvm_method_names/test.saw @@ -1,5 +1,6 @@ enable_experimental; c <- java_load_class "Test"; +print c; crucible_jvm_verify c "get" [] false do { @@ -13,18 +14,48 @@ crucible_jvm_verify c "get" [] false print "********************************************************************************"; -// FIXME: saw-script can't verify constructor functions +print ""; fails ( -crucible_jvm_verify c "Test(L)V" [] false +crucible_jvm_verify c "" [] false do { - x <- jvm_fresh_var "x" java_long; - jvm_execute_func [jvm_term x]; this <- jvm_alloc_object "Test"; - jvm_field_is this "Test.val" (jvm_term x); - jvm_return this; + jvm_execute_func [this]; + jvm_field_is this "Test.val" (jvm_term {{ 0 : [64] }}); } z3); +print "********************************************************************************"; +print "(J)V"; +crucible_jvm_verify c "(J)V" [] false + do { + this <- jvm_alloc_object "Test"; + x <- jvm_fresh_var "x" java_long; + jvm_execute_func [this, jvm_term x]; + jvm_field_is this "Test.val" (jvm_term x); + } + z3; + +print "********************************************************************************"; +print "(I)V"; +crucible_jvm_verify c "(I)V" [] false + do { + this <- jvm_alloc_object "Test"; + x <- jvm_fresh_var "x" java_int; + jvm_execute_func [this, jvm_term x]; + jvm_field_is this "Test.val" (jvm_term {{ sext x : [64] }}); + } + z3; + +print "********************************************************************************"; +print "()V"; +crucible_jvm_verify c "()V" [] false + do { + this <- jvm_alloc_object "Test"; + jvm_execute_func [this]; + jvm_field_is this "Test.val" (jvm_term {{ 0 : [64] }}); + } + z3; + print "********************************************************************************"; print "increment"; fails (