SimError.hs

-----------------------------------------------------------------------
-- |
-- 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 SimError { simErrorLoc, simErrorReason } <- SimErrorWithContext simErrorLoc simErrorReason _
  where SimError loc reason = SimErrorWithContext loc reason Nothing

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

simErrorReasonMsg :: SimErrorReason -> String
simErrorReasonMsg (GenericSimError msg) = msg
simErrorReasonMsg (Unsupported _ msg) = "Unsupported feature: " ++ msg
simErrorReasonMsg (ReadBeforeWriteSimError msg) = msg
simErrorReasonMsg (AssertFailureSimError msg _) = msg
simErrorReasonMsg (ResourceExhausted msg) = "Resource exhausted: " ++ msg

simErrorDetailsMsg :: SimErrorReason -> String
simErrorDetailsMsg (AssertFailureSimError _ msg) = msg
simErrorDetailsMsg (Unsupported stk _) = show stk
simErrorDetailsMsg _ = ""

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

instance IsString SimErrorReason where
  fromString = GenericSimError

instance Show SimErrorReason where
  show = simErrorReasonMsg

instance Show SimError where
  show = show . ppSimError

ppSimError :: SimError -> Doc ann
ppSimError er =
  vcat $ [ pretty (plSourceLoc loc) <> pretty ": error: in" <+> pretty (plFunction loc)
         , pretty (simErrorReasonMsg rsn)
         ] ++ (if null details
               then []
               else [ pretty "Details:"
                    , indent 2 (vcat (pretty <$> lines details))
                    ])
          ++ (case simErrorContext er of
                Nothing -> []
                Just (ProgramStack _ []) -> []
                Just ctx -> [ pretty "Context:"
                            , indent 2 (ppProgramStack ctx)
                            ])
 where loc = simErrorLoc er
       details = simErrorDetailsMsg rsn
       rsn = simErrorReason er          

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

ppProgramStack :: ProgramStack -> Doc ann
ppProgramStack (ProgramStack omittedCount frames) = vcat ((ppLoc <$> frames) ++ omitLine)
  where
    omitLine =
      if omittedCount <= 0
        then []
        else [ pretty "..."  <+> pretty omittedCount <+> pretty "calling frames omitted" ]
    ppLoc l = pretty (plSourceLoc l) <> pretty ":" <+> pretty (plFunction l)

instance Exception SimError