Implement type checking for jvm_return.

This fixes more remaining known false positives of #938.

intTests/test_jvm_setup_errors/test.saw

@@ -429,7 +429,7 @@ check_fails test "set"
   };
 
 print "jvm_return with non-monomorphic type";
-KNOWN_FALSE_POSITIVE test "get"
+check_fails test "get"
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -439,7 +439,7 @@ KNOWN_FALSE_POSITIVE test "get"
   };
 
 print "jvm_return with non-jvm type";
-KNOWN_FALSE_POSITIVE test "get"
+check_fails test "get"
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -449,7 +449,7 @@ KNOWN_FALSE_POSITIVE test "get"
   };
 
 print "jvm_return with wrong base type";
-KNOWN_FALSE_POSITIVE test "get"
+check_fails test "get"
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -459,7 +459,7 @@ KNOWN_FALSE_POSITIVE test "get"
   };
 
 print "jvm_return with reference type when base type was expected";
-KNOWN_FALSE_POSITIVE test "get"
+check_fails test "get"
   do {
     this <- jvm_alloc_object "Test";
     val <- jvm_fresh_var "val" java_long;
@@ -478,7 +478,7 @@ KNOWN_FALSE_POSITIVE test "get"
   };
 
 print "jvm_return when none was expected";
-KNOWN_FALSE_POSITIVE test "set"
+check_fails test "set"
   do {
     this <- jvm_alloc_object "Test";
     x <- jvm_fresh_var "x" java_long;

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -811,6 +811,8 @@ data JVMSetupError
   | JVMArrayMultiple SetupValue
   | JVMArgTypeMismatch Int J.Type J.Type -- argument position, expected, found
   | JVMArgNumberWrong Int Int -- number expected, number found
+  | JVMReturnUnexpected J.Type -- found
+  | JVMReturnTypeMismatch J.Type J.Type -- expected, found
 
 instance X.Exception JVMSetupError
 
@@ -886,6 +888,17 @@ instance Show JVMSetupError where
         , "Expected: " ++ show expected
         , "Given: " ++ show found
         ]
+      JVMReturnUnexpected found ->
+        unlines
+        [ "jvm_return: Unexpected return value for void method"
+        , "Given type: " ++ show found
+        ]
+      JVMReturnTypeMismatch expected found ->
+        unlines
+        [ "jvm_return: Return type mismatch"
+        , "Expected type: " ++ show expected
+        , "Given type: " ++ show found
+        ]
 
 -- | Returns Cryptol type of actual type if it is an array or
 -- primitive type.
@@ -1102,7 +1115,21 @@ jvm_execute_func bic opts args =
      Setup.crucible_execute_func bic opts args
 
 jvm_return :: BuiltinContext -> Options -> SetupValue -> JVMSetupM ()
-jvm_return bic opts retVal = JVMSetupM $ Setup.crucible_return bic opts retVal
+jvm_return bic opts retVal =
+  JVMSetupM $
+  do st <- get
+     let cc = st ^. Setup.csCrucibleContext
+     let mspec = st ^. Setup.csMethodSpec
+     let env = MS.csAllocations mspec
+     let nameEnv = MS.csTypeNames mspec
+     valTy <- typeOfSetupValue cc env nameEnv retVal
+     case mspec ^. MS.csRet of
+       Nothing ->
+         X.throwM (JVMReturnUnexpected valTy)
+       Just retTy ->
+         unless (registerCompatible retTy valTy) $
+         X.throwM (JVMReturnTypeMismatch retTy valTy)
+     Setup.crucible_return bic opts retVal
 
 --------------------------------------------------------------------------------