-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.SimError
-- Description      : Data structure the execution state of the simulator
-- Copyright        : (c) Galois, Inc 2014
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE PatternSynonyms #-}
module Lang.Crucible.Simulator.SimError (
    SimErrorReason(..)
  , SimError(.., SimError)
  , ProgramStack(..)
  , mkSimError
  , simErrorReason
  , simErrorLoc
  , simErrorContext
  , simErrorReasonMsg
  , simErrorDetailsMsg
  , ppSimError
  , ppProgramStack
  ) where

import GHC.Stack (CallStack)

import Control.Exception
import Data.String
import Prettyprinter

import What4.ProgramLoc


------------------------------------------------------------------------
-- SimError

-- | Class for exceptions generated by simulator.
data SimErrorReason
   = GenericSimError !String
   | Unsupported !CallStack !String
      -- ^ We can't do that (yet?).  The call stack identifies where in the
      --   Haskell code the error occured.
   | ReadBeforeWriteSimError !String -- FIXME? include relevant data instead of a string?
   | AssertFailureSimError !String !String
     -- ^ An assertion failed. The first parameter is a short
     -- description. The second is a more detailed explanation.
   | ResourceExhausted String
      -- ^ A loop iteration count, or similar resource limit,
      --   was exceeded.

data SimError 
   = SimErrorWithContext !ProgramLoc !SimErrorReason !(Maybe ProgramStack)
 
-- | This pattern synonym constructs SimErrors without a program stack context when used 
-- as an expression and ignores the program stack when used as a pattern.  It exists
-- because SimError did not used to have a `ProgramStack`, and there are many usages
-- in the code of the previous constructor which is approximated by this pattern.
--
-- Using SimErrorWithContext should be preferred.
pattern SimError :: ProgramLoc -> SimErrorReason -> SimError
pattern $mSimError :: forall {r}.
SimError
-> (ProgramLoc -> SimErrorReason -> r) -> ((# #) -> r) -> r
$bSimError :: ProgramLoc -> SimErrorReason -> SimError
SimError { SimError -> ProgramLoc
simErrorLoc, SimError -> SimErrorReason
simErrorReason } <- SimErrorWithContext simErrorLoc simErrorReason _
  where SimError ProgramLoc
loc SimErrorReason
reason = ProgramLoc -> SimErrorReason -> Maybe ProgramStack -> SimError
SimErrorWithContext ProgramLoc
loc SimErrorReason
reason Maybe ProgramStack
forall a. Maybe a
Nothing

simErrorContext :: SimError -> Maybe ProgramStack
simErrorContext :: SimError -> Maybe ProgramStack
simErrorContext (SimErrorWithContext ProgramLoc
_ SimErrorReason
_ Maybe ProgramStack
c) = Maybe ProgramStack
c

simErrorReasonMsg :: SimErrorReason -> String
simErrorReasonMsg :: SimErrorReason -> String
simErrorReasonMsg (GenericSimError String
msg) = String
msg
simErrorReasonMsg (Unsupported CallStack
_ String
msg) = String
"Unsupported feature: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg
simErrorReasonMsg (ReadBeforeWriteSimError String
msg) = String
msg
simErrorReasonMsg (AssertFailureSimError String
msg String
_) = String
msg
simErrorReasonMsg (ResourceExhausted String
msg) = String
"Resource exhausted: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg

simErrorDetailsMsg :: SimErrorReason -> String
simErrorDetailsMsg :: SimErrorReason -> String
simErrorDetailsMsg (AssertFailureSimError String
_ String
msg) = String
msg
simErrorDetailsMsg (Unsupported CallStack
stk String
_) = CallStack -> String
forall a. Show a => a -> String
show CallStack
stk
simErrorDetailsMsg SimErrorReason
_ = String
""

mkSimError :: ProgramLoc -> SimErrorReason -> Maybe ProgramStack -> SimError
mkSimError :: ProgramLoc -> SimErrorReason -> Maybe ProgramStack -> SimError
mkSimError ProgramLoc
loc SimErrorReason
reason Maybe ProgramStack
mbCtx = ProgramLoc -> SimErrorReason -> Maybe ProgramStack -> SimError
SimErrorWithContext ProgramLoc
loc SimErrorReason
reason Maybe ProgramStack
mbCtx

instance IsString SimErrorReason where
  fromString :: String -> SimErrorReason
fromString = String -> SimErrorReason
GenericSimError

instance Show SimErrorReason where
  show :: SimErrorReason -> String
show = SimErrorReason -> String
simErrorReasonMsg

instance Show SimError where
  show :: SimError -> String
show = Doc Any -> String
forall a. Show a => a -> String
show (Doc Any -> String) -> (SimError -> Doc Any) -> SimError -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimError -> Doc Any
forall ann. SimError -> Doc ann
ppSimError

ppSimError :: SimError -> Doc ann
ppSimError :: forall ann. SimError -> Doc ann
ppSimError SimError
er =
  [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ [ Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Position -> Doc ann
pretty (ProgramLoc -> Position
plSourceLoc ProgramLoc
loc) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
": error: in" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FunctionName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
pretty (ProgramLoc -> FunctionName
plFunction ProgramLoc
loc)
         , String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (SimErrorReason -> String
simErrorReasonMsg SimErrorReason
rsn)
         ] [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ (if String -> Bool
forall a. [a] -> Bool
forall (t :: Type -> Type) a. Foldable t => t a -> Bool
null String
details
               then []
               else [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"Details:"
                    , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 ([Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat (String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> [String] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> [String]
lines String
details))
                    ])
          [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ (case SimError -> Maybe ProgramStack
simErrorContext SimError
er of
                Maybe ProgramStack
Nothing -> []
                Just (ProgramStack Int
_ []) -> []
                Just ProgramStack
ctx -> [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"Context:"
                            , Int -> Doc ann -> Doc ann
forall ann. Int -> Doc ann -> Doc ann
indent Int
2 (ProgramStack -> Doc ann
forall ann. ProgramStack -> Doc ann
ppProgramStack ProgramStack
ctx)
                            ])
 where loc :: ProgramLoc
loc = SimError -> ProgramLoc
simErrorLoc SimError
er
       details :: String
details = SimErrorReason -> String
simErrorDetailsMsg SimErrorReason
rsn
       rsn :: SimErrorReason
rsn = SimError -> SimErrorReason
simErrorReason SimError
er          

-- | Representation of the program stack for providing dynamic
-- context for SimErrors
data ProgramStack = ProgramStack 
  { -- | Number of calling frames omitted in the stack trace
    ProgramStack -> Int
psFrameOmitCount :: Int
    -- | The visible part of the stack strace
  , ProgramStack -> [ProgramLoc]
psFrames :: [ProgramLoc]
  }

ppProgramStack :: ProgramStack -> Doc ann
ppProgramStack :: forall ann. ProgramStack -> Doc ann
ppProgramStack (ProgramStack Int
omittedCount [ProgramLoc]
frames) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vcat ((ProgramLoc -> Doc ann
forall {ann}. ProgramLoc -> Doc ann
ppLoc (ProgramLoc -> Doc ann) -> [ProgramLoc] -> [Doc ann]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [ProgramLoc]
frames) [Doc ann] -> [Doc ann] -> [Doc ann]
forall a. [a] -> [a] -> [a]
++ [Doc ann]
omitLine)
  where
    omitLine :: [Doc ann]
omitLine =
      if Int
omittedCount Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0
        then []
        else [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"..."  Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
omittedCount Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
"calling frames omitted" ]
    ppLoc :: ProgramLoc -> Doc ann
ppLoc ProgramLoc
l = Position -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Position -> Doc ann
pretty (ProgramLoc -> Position
plSourceLoc ProgramLoc
l) Doc ann -> Doc ann -> Doc ann
forall a. Semigroup a => a -> a -> a
<> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
":" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> FunctionName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
pretty (ProgramLoc -> FunctionName
plFunction ProgramLoc
l)

instance Exception SimError