From 090b21c62e13ca3f719bb190970e313726644cd5 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Sun, 14 Feb 2021 16:40:37 -0800
Subject: [PATCH] Embed JVMSetupError inside TopLevelException datatype.

This means that JVMSetupError exceptions can now be caught by
the standard TopLevelException handlers, and get shown with
the expected stack traces in the saw-script REPL.

This is done using a new existentially-typed `SomeTopLevelException`
constructor, as recommended by the Control.Exception documentation.

Fixes #1021.
---
 src/SAWScript/Crucible/JVM/Builtins.hs |  5 ++++-
 src/SAWScript/Exceptions.hs            | 23 +++++++++++++++++++++++
 2 files changed, 27 insertions(+), 1 deletion(-)

diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
index 95f1f1cc60..6575e7129f 100644
--- a/src/SAWScript/Crucible/JVM/Builtins.hs
+++ b/src/SAWScript/Crucible/JVM/Builtins.hs
@@ -98,6 +98,7 @@ import Verifier.SAW.TypedTerm
 
 import Verifier.SAW.Simulator.What4.ReturnTrip
 
+import SAWScript.Exceptions
 import SAWScript.Proof
 import SAWScript.Prover.SolverStats
 import SAWScript.TopLevel
@@ -813,7 +814,9 @@ data JVMSetupError
   | JVMReturnUnexpected J.Type -- found
   | JVMReturnTypeMismatch J.Type J.Type -- expected, found
 
-instance X.Exception JVMSetupError
+instance X.Exception JVMSetupError where
+  toException = topLevelExceptionToException
+  fromException = topLevelExceptionFromException
 
 instance Show JVMSetupError where
   show err =
diff --git a/src/SAWScript/Exceptions.hs b/src/SAWScript/Exceptions.hs
index 017eca2f27..0d7481a5e3 100644
--- a/src/SAWScript/Exceptions.hs
+++ b/src/SAWScript/Exceptions.hs
@@ -1,11 +1,16 @@
+{-# LANGUAGE ExistentialQuantification #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+
 module SAWScript.Exceptions
   ( TypeErrors(..), failTypecheck
   , TopLevelException(..)
   , TraceException(..)
+  , topLevelExceptionToException
+  , topLevelExceptionFromException
   ) where
 
 import Control.Exception
+import Data.Typeable (cast)
 
 import What4.ProgramLoc (ProgramLoc)
 
@@ -31,6 +36,7 @@ data TopLevelException
   | CrucibleSetupException ProgramLoc String
   | OverrideMatcherException ProgramLoc String
   | LLVMMethodSpecException ProgramLoc String
+  | forall e. Exception e => SomeTopLevelException e
 
 instance Show TopLevelException where
   show (TopLevelException _ msg) = msg
@@ -38,6 +44,23 @@ instance Show TopLevelException where
   show (CrucibleSetupException _ msg) = msg
   show (OverrideMatcherException _ msg) = msg
   show (LLVMMethodSpecException _ msg) = msg
+  show (SomeTopLevelException e) = show e
+
+-- | To use a custom structured exception type that works with the
+-- saw-script REPL's exception handlers and stack tracing, define
+-- 'toException' as 'topLevelExceptionToException' in the custom
+-- exception type's 'Exception' class instance.
+topLevelExceptionToException :: Exception e => e -> SomeException
+topLevelExceptionToException = toException . SomeTopLevelException
+
+-- | To use a custom structured exception type that works with the
+-- saw-script REPL's exception handlers and stack tracing, define
+-- 'fromException' as 'topLevelExceptionFromException' in the custom
+-- exception type's 'Exception' class instance.
+topLevelExceptionFromException :: Exception e => SomeException -> Maybe e
+topLevelExceptionFromException x =
+  do SomeTopLevelException a <- fromException x
+     cast a
 
 instance Exception TopLevelException