Merge pull request #884 from GaloisInc/issue212

Allow duplicate method names in JVM verification

intTests/test_jvm_method_names/Makefile

@@ -0,0 +1,2 @@
+%.class: %.java
+	javac -g $<

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;
+    }
+}

intTests/test_jvm_method_names/test.saw

@@ -0,0 +1,125 @@
+enable_experimental;
+c <- java_load_class "Test";
+print c;
+
+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 "********************************************************************************";
+print "<init>";
+fails (
+crucible_jvm_verify c "<init>" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    jvm_execute_func [this];
+    jvm_field_is this "Test.val" (jvm_term {{ 0 : [64] }});
+  }
+  z3);
+
+print "********************************************************************************";
+print "<init>(J)V";
+crucible_jvm_verify c "<init>(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 "<init>(I)V";
+crucible_jvm_verify c "<init>(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 "<init>()V";
+crucible_jvm_verify c "<init>()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 (
+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;

intTests/test_jvm_method_names/test.sh

@@ -0,0 +1 @@
+$SAW test.saw

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

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

src/SAWScript/Utils.hs

@@ -10,6 +10,7 @@ Stability   : provisional
 {-# LANGUAGE EmptyDataDecls #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE DeriveDataTypeable  #-}
+{-# LANGUAGE LambdaCase #-}
 
 module SAWScript.Utils where
 
@@ -120,25 +121,33 @@ 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]
         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 ->
                   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 +209,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