------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.Intrinsics.Options
-- Description      : Definition of options that affect LLVM overrides
-- Copyright        : (c) Galois, Inc 2021
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------
module Lang.Crucible.LLVM.Intrinsics.Options
  ( IntrinsicsOptions(..)
  , AbnormalExitBehavior(..)
  , defaultIntrinsicsOptions
  ) where

-- | Should Crucible fail when simulating a function which triggers an abnormal
-- exit, such as @abort()@?
data AbnormalExitBehavior
  = AlwaysFail
    -- ^ Functions which trigger an abnormal exit will always cause Crucible
    --   to fail.
  | OnlyAssertFail
    -- ^ The @__assert_fail()@ or @__assert_rtn()@ functions will cause Crucible
    --   to fail, while other functions which trigger an abnormal exit will not
    --   cause failures. This option is primarily useful for SV-COMP.
  | NeverFail
    -- ^ Functions which trigger an abnormal exit will never cause Crucible
    --   to fail. This option is primarily useful for SV-COMP.
  deriving AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
(AbnormalExitBehavior -> AbnormalExitBehavior -> Bool)
-> (AbnormalExitBehavior -> AbnormalExitBehavior -> Bool)
-> Eq AbnormalExitBehavior
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
== :: AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
$c/= :: AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
/= :: AbnormalExitBehavior -> AbnormalExitBehavior -> Bool
Eq

-- | This datatype encodes a variety of tweakable settings that to LLVM
--   overrides.
newtype IntrinsicsOptions
  = IntrinsicsOptions
    { IntrinsicsOptions -> AbnormalExitBehavior
abnormalExitBehavior :: AbnormalExitBehavior
      -- ^ Should Crucible fail when simulating a function which triggers an
      --   abnormal exit, such as @abort()@?
    }

-- | The default translation options:
--
-- * Functions which trigger an abnormal exit will always cause Crucible
--   to fail.
defaultIntrinsicsOptions :: IntrinsicsOptions
defaultIntrinsicsOptions :: IntrinsicsOptions
defaultIntrinsicsOptions =
  IntrinsicsOptions
  { abnormalExitBehavior :: AbnormalExitBehavior
abnormalExitBehavior = AbnormalExitBehavior
AlwaysFail
  }