-----------------------------------------------------------------------
-- |
-- 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 #-}
module Lang.Crucible.Simulator.SimError (
    SimErrorReason(..)
  , SimError(..)
  , simErrorReasonMsg
  , simErrorDetailsMsg
  , ppSimError
  ) where

import GHC.Stack (CallStack)

import Control.Exception
import Data.String
import Data.Typeable
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.
 deriving (Typeable)

data SimError
   = SimError
   { SimError -> ProgramLoc
simErrorLoc :: !ProgramLoc
   , SimError -> SimErrorReason
simErrorReason :: !SimErrorReason
   }
 deriving (Typeable)

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
""

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))
                   ]
 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

instance Exception SimError