Use throwM or panic instead of fail for error handling in JVMSetup.

This partially addresses #928. This patch only covers the uses of
`fail` that were used to implement the JVMSetup commands. There are
still a lot of uses of `fail` in other parts of the SAW/JVM code.

Author: Brian Huffman

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -41,6 +41,7 @@ module SAWScript.Crucible.JVM.Builtins
 
 import           Control.Lens
 
+import qualified Control.Monad.Catch as X
 import           Control.Monad.State
 import qualified Control.Monad.State.Strict as Strict
 import           Control.Monad.Trans.Except (runExceptT)
@@ -792,6 +793,54 @@ setupDynamicClassTable sym jc = foldM addClass Map.empty (Map.assocs (CJ.classTa
 --------------------------------------------------------------------------------
 -- Setup builtins
 
+data JVMSetupError
+  = JVMFreshVarInvalidType JavaType
+  | JVMFieldMultiple SetupValue String -- reference and field name
+  | JVMFieldFailure String -- TODO: switch to a more structured type
+  | JVMFieldTypeMismatch String J.Type J.Type -- field name, expected, found
+  | JVMElemNonArray J.Type
+  | JVMElemInvalidIndex SetupValue Int Int -- reference, length, index
+  | JVMElemTypeMismatch Int J.Type J.Type -- index, expected, found
+  | JVMElemMultiple SetupValue Int -- reference and array index
+  | JVMArrayMultiple SetupValue
+
+instance X.Exception JVMSetupError
+
+instance Show JVMSetupError where
+  show err =
+    case err of
+      JVMFreshVarInvalidType jty ->
+        "jvm_fresh_var: Invalid type: " ++ show jty
+      JVMFieldMultiple _ptr fname ->
+        "jvm_field_is: Multiple specifications for the same instance field (" ++ fname ++ ")"
+      JVMFieldFailure msg ->
+        "jvm_field_is: JVM field resolution failed:\n" ++ msg
+      JVMFieldTypeMismatch fname expected found ->
+         -- FIXME: use a pretty printing function for J.Type instead of show
+        unlines
+        [ "jvm_field_is: Incompatible types for field " ++ show fname
+        , "Expected type: " ++ show expected
+        , "Given type: " ++ show found
+        ]
+      JVMElemNonArray jty ->
+        "jvm_elem_is: Not an array type: " ++ show jty
+      JVMElemInvalidIndex _ptr len idx ->
+        unlines
+        [ "jvm_elem_is: Array index out of bounds"
+        , "Array length: " ++ show len
+        , "Given index: " ++ show idx
+        ]
+      JVMElemTypeMismatch idx expected found ->
+        unlines
+        [ "jvm_elem_is: Incompatible types for array index " ++ show idx
+        , "Expected type: " ++ show expected
+        , "Given type: " ++ show found
+        ]
+      JVMElemMultiple _ptr idx ->
+        "jvm_elem_is: Multiple specifications for the same array index (" ++ show idx ++ ")"
+      JVMArrayMultiple _ptr ->
+        "jvm_array_is: Multiple specifications for the same array reference"
+
 -- | Returns Cryptol type of actual type if it is an array or
 -- primitive type.
 cryptolTypeOfActual :: JavaType -> Maybe Cryptol.Type
@@ -837,7 +886,7 @@ jvm_fresh_var bic _opts name jty =
   JVMSetupM $
   do let sc = biSharedContext bic
      case cryptolTypeOfActual jty of
-       Nothing -> fail $ "Unsupported type in jvm_fresh_var: " ++ show jty
+       Nothing -> X.throwM $ JVMFreshVarInvalidType jty
        Just cty -> Setup.freshVariable sc name cty
 
 jvm_alloc_object ::
@@ -884,19 +933,15 @@ jvm_field_is _typed _bic _opt ptr fname val =
      let cb = cc ^. jccCodebase
      let path = Left fname
      if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [] rs
-       then fail $ "Multiple points-to preconditions on same pointer (field " ++ fname ++ ")"
+       then X.throwM $ JVMFieldMultiple ptr fname
        else Setup.csResolvedState %= MS.markResolved ptr [path]
      let env = MS.csAllocations (st ^. Setup.csMethodSpec)
      let nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
      ptrTy <- typeOfSetupValue cc env nameEnv ptr
      valTy <- typeOfSetupValue cc env nameEnv val
-     fid <- either fail pure =<< (liftIO $ runExceptT $ findField cb pos ptrTy fname)
+     fid <- either (X.throwM . JVMFieldFailure) pure =<< (liftIO $ runExceptT $ findField cb pos ptrTy fname)
      unless (registerCompatible (J.fieldIdType fid) valTy) $
-       fail $ unlines
-       [ "Incompatible types for field " ++ fname
-       , "Expected: " ++ show (J.fieldIdType fid)
-       , "but given value of type: " ++ show valTy
-       ]
+       X.throwM $ JVMFieldTypeMismatch fname (J.fieldIdType fid) valTy
      Setup.addPointsTo (JVMPointsToField loc ptr fid val)
 
 jvm_elem_is ::
@@ -915,7 +960,7 @@ jvm_elem_is _typed _bic _opt ptr idx val =
      let cc = st ^. Setup.csCrucibleContext
      let path = Right idx
      if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [path] rs
-       then fail "Multiple points-to preconditions on same pointer"
+       then X.throwM $ JVMElemMultiple ptr idx
        else Setup.csResolvedState %= MS.markResolved ptr [path]
      let env = MS.csAllocations (st ^. Setup.csMethodSpec)
      let nameEnv = MS.csTypeNames (st ^. Setup.csMethodSpec)
@@ -924,13 +969,9 @@ jvm_elem_is _typed _bic _opt ptr idx val =
      elTy <-
        case ptrTy of
          J.ArrayType elTy -> pure elTy
-         _ -> fail $ "Not an array type: " ++ show ptrTy
+         _ -> X.throwM $ JVMElemNonArray ptrTy
      unless (registerCompatible elTy valTy) $
-       fail $ unlines
-       [ "Incompatible types for array element"
-       , "Expected: " ++ show elTy
-       , "but given value of type: " ++ show valTy
-       ]
+       X.throwM $ JVMElemTypeMismatch idx elTy valTy
      Setup.addPointsTo (JVMPointsToElem loc ptr idx val)
 
 jvm_array_is ::
@@ -946,7 +987,7 @@ jvm_array_is _typed _bic _opt ptr val =
      st <- get
      let rs = st ^. Setup.csResolvedState
      if st ^. Setup.csPrePost == PreState && MS.testResolved ptr [] rs
-       then fail "Multiple points-to preconditions on same pointer"
+       then X.throwM $ JVMArrayMultiple ptr
        else Setup.csResolvedState %= MS.markResolved ptr []
      Setup.addPointsTo (JVMPointsToArray loc ptr val)
 

src/SAWScript/Crucible/JVM/ResolveSetupValue.hs

@@ -26,15 +26,15 @@ module SAWScript.Crucible.JVM.ResolveSetupValue
   ) where
 
 import           Control.Lens
-import qualified Control.Monad.Fail as Fail
+import qualified Control.Monad.Catch as X
 import           Data.IORef
 import qualified Data.BitVector.Sized as BV
 import           Data.Map (Map)
 import qualified Data.Map as Map
 import           Data.Void (absurd)
 
 import qualified Cryptol.Eval.Type as Cryptol (TValue(..), evalValType)
-import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..))
+import qualified Cryptol.TypeCheck.AST as Cryptol (Type, Schema(..))
 import qualified Cryptol.Utils.PP as Cryptol (pp)
 
 import qualified What4.BaseTypes as W4
@@ -68,6 +68,7 @@ import SAWScript.Crucible.Common (Sym)
 import SAWScript.Crucible.Common.MethodSpec (AllocIndex(..))
 
 --import SAWScript.JavaExpr (JavaType(..))
+import SAWScript.Panic
 import SAWScript.Prover.Rewrite
 import SAWScript.Crucible.JVM.MethodSpecIR
 import qualified SAWScript.Crucible.Common.MethodSpec as MS
@@ -88,8 +89,27 @@ type JVMRefVal = Crucible.RegValue Sym CJ.JVMRefType
 
 type SetupValue = MS.SetupValue CJ.JVM
 
+data JvmTypeOfError
+  = JvmPolymorphicType Cryptol.Schema
+  | JvmNonRepresentableType Cryptol.Type
+
+instance Show JvmTypeOfError where
+  show (JvmPolymorphicType s) =
+    unlines
+    [ "Expected monomorphic term"
+    , "instead got:"
+    , show (Cryptol.pp s)
+    ]
+  show (JvmNonRepresentableType ty) =
+    unlines
+    [ "Type not representable in JVM:"
+    , show (Cryptol.pp ty)
+    ]
+
+instance X.Exception JvmTypeOfError
+
 typeOfSetupValue ::
-  Fail.MonadFail m =>
+  X.MonadThrow m =>
   JVMCrucibleContext ->
   Map AllocIndex (W4.ProgramLoc, Allocation) ->
   Map AllocIndex JIdent ->
@@ -99,18 +119,16 @@ typeOfSetupValue _cc env _nameEnv val =
   case val of
     MS.SetupVar i ->
       case Map.lookup i env of
-        Nothing -> fail ("typeOfSetupValue: Unresolved prestate variable:" ++ show i)
+        Nothing -> panic "JVMSetup" ["typeOfSetupValue", "Unresolved prestate variable:" ++ show i]
         Just (_, alloc) -> return (allocationType alloc)
     MS.SetupTerm tt ->
       case ttSchema tt of
         Cryptol.Forall [] [] ty ->
           case toJVMType (Cryptol.evalValType mempty ty) of
-            Nothing -> fail "typeOfSetupValue: non-representable type"
+            Nothing -> X.throwM (JvmNonRepresentableType ty)
             Just jty -> return jty
-        s -> fail $ unlines [ "typeOfSetupValue: expected monomorphic term"
-                            , "instead got:"
-                            , show (Cryptol.pp s)
-                            ]
+        s -> X.throwM (JvmPolymorphicType s)
+
     MS.SetupNull () ->
       -- We arbitrarily set the type of NULL to java.lang.Object,
       -- because a) it is memory-compatible with any type that NULL
@@ -137,7 +155,7 @@ resolveSetupVal cc env _tyenv _nameEnv val =
   case val of
     MS.SetupVar i
       | Just v <- Map.lookup i env -> return (RVal v)
-      | otherwise -> fail ("resolveSetupVal: Unresolved prestate variable:" ++ show i)
+      | otherwise -> panic "JVMSetup" ["resolveSetupVal", "Unresolved prestate variable:" ++ show i]
     MS.SetupTerm tm -> resolveTypedTerm cc tm
     MS.SetupNull () ->
       return (RVal (W4.maybePartExpr sym Nothing))