-----------------------------------------------------------------------
-- |
-- 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
   { simErrorLoc :: !ProgramLoc
   , simErrorReason :: !SimErrorReason
   }
 deriving (Typeable)

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

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))
                   ]
 where loc = simErrorLoc er
       details = simErrorDetailsMsg rsn
       rsn = simErrorReason er

instance Exception SimError