projectJVMVal :: OnlineSolver solver =>
  Backend solver -> J.Type -> String -> Crucible.RegValue Sym CJ.JVMValueType -> IO JVMVal
projectJVMVal bak ty msg' v =
  case ty of
    J.BooleanType -> IVal <$> proj v CJ.tagI
    J.ByteType    -> IVal <$> proj v CJ.tagI
    J.CharType    -> IVal <$> proj v CJ.tagI
    J.ShortType   -> IVal <$> proj v CJ.tagI
    J.IntType     -> IVal <$> proj v CJ.tagI
    J.LongType    -> LVal <$> proj v CJ.tagL
    J.FloatType   -> err -- FIXME
    J.DoubleType  -> err -- FIXME
    J.ArrayType{} -> RVal <$> proj v CJ.tagR
    J.ClassType{} -> RVal <$> proj v CJ.tagR
  where
    proj ::
      forall tp.
      Crucible.RegValue Sym CJ.JVMValueType ->
      Ctx.Index CJ.JVMValueCtx tp ->
      IO (Crucible.RegValue Sym tp)
    proj val idx = Crucible.readPartExpr bak (Crucible.unVB (val Ctx.! idx)) msg

    msg = Crucible.GenericSimError $ "Ill-formed value for type " ++ show ty ++ " (" ++ msg' ++ ")"
    err = Crucible.addFailedAssertion bak msg
projectJVMVal :: OnlineSolver solver =>
  Backend solver -> J.Type -> String -> Crucible.RegValue Sym CJ.JVMValueType -> IO JVMVal
projectJVMVal bak ty msg' v =
  case ty of
    J.BooleanType -> IVal <$> proj v CJ.tagI
    J.ByteType    -> IVal <$> proj v CJ.tagI
    J.CharType    -> IVal <$> proj v CJ.tagI
    J.ShortType   -> IVal <$> proj v CJ.tagI
    J.IntType     -> IVal <$> proj v CJ.tagI
    J.LongType    -> LVal <$> proj v CJ.tagL
    J.FloatType   -> err -- FIXME
    J.DoubleType  -> err -- FIXME
    J.ArrayType{} -> RVal <$> proj v CJ.tagR
    J.ClassType{} -> RVal <$> proj v CJ.tagR
  where
    proj ::
      forall tp.
      Crucible.RegValue Sym CJ.JVMValueType ->
      Ctx.Index CJ.JVMValueCtx tp ->
      IO (Crucible.RegValue Sym tp)
    proj val idx = Crucible.readPartExpr bak (Crucible.unVB (val Ctx.! idx)) msg

    msg = Crucible.GenericSimError $ "Ill-formed value for type " ++ show ty ++ " (" ++ msg' ++ ")"
    err = Crucible.addFailedAssertion bak msg
projectJVMVal bak ty msg' v =
  case ty of
    J.BooleanType -> IVal <$> proj v CJ.tagI
    J.ByteType    -> IVal <$> proj v CJ.tagI
    J.CharType    -> IVal <$> proj v CJ.tagI
    J.ShortType   -> IVal <$> proj v CJ.tagI
    J.IntType     -> IVal <$> proj v CJ.tagI
    J.LongType    -> LVal <$> proj v CJ.tagL
    J.FloatType   -> err -- FIXME
    J.DoubleType  -> err -- FIXME
    J.ArrayType{} -> RVal <$> proj v CJ.tagR
    J.ClassType{} -> RVal <$> proj v CJ.tagR
  where
    proj ::
      forall tp.
      Crucible.RegValue Sym CJ.JVMValueType ->
      Ctx.Index CJ.JVMValueCtx tp ->
      IO (Crucible.RegValue Sym tp)
    proj val idx = Crucible.readPartExpr bak (Crucible.unVB (val Ctx.! idx)) msg

    msg = Crucible.GenericSimError $ "Ill-formed value for type " ++ show ty ++ " (" ++ msg' ++ ")"
    err = Crucible.addFailedAssertion bak msg