content: ------------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.LLVM.Translation.Options
  -- Description      : Definition of options that can be tweaked during LLVM translation
  -- Copyright        : (c) Galois, Inc 2021
  -- License          : BSD3
  -- Maintainer       : Rob Dockins <rdockins@galois.com>
  -- Stability        : provisional
  ------------------------------------------------------------------------
  module Lang.Crucible.LLVM.Translation.Options
    ( TranslationOptions(..)
    , defaultTranslationOptions
    , debugIntrinsicsTranslationOptions
    ) where
  
  -- | This datatype encodes a variety of tweakable settings that apply during
  --   LLVM translation.
  data TranslationOptions
    = TranslationOptions
      { debugIntrinsics :: !Bool
        -- ^ Should we translate @llvm.dbg@ intrinsic statements? The upside to
        --   translating them is that they encode debugging information about a
        --   program that can be useful for external clients. The downside is
        --   that they can bloat the size of translated programs, despite being
        --   no-ops during simulation.
      , laxArith :: !Bool
        -- ^ Should we omit proof obligations related to arithmetic overflow
        --   and similar assertions?
      , optLoopMerge :: !Bool
        -- ^ Should we insert merge blocks in loops with early exits (i.e. breaks
        --   or returns)? This may improve simulation performance.
      }
  
  -- | The default translation options:
  --
  -- * Do not translate @llvm.dbg@ intrinsic statements
  --
  -- * Do not produce proof obligations for arithmetic-related assertions.
  --
  -- * Do not insert merge blocks in loops with early exits.
  defaultTranslationOptions :: TranslationOptions
  defaultTranslationOptions =
    TranslationOptions
    { debugIntrinsics = False
    , laxArith = False
    , optLoopMerge = False
    }
  
  -- | Like 'defaultTranslationOptions', but @llvm.dbg@ intrinsic statements are
  -- translated.
  debugIntrinsicsTranslationOptions :: TranslationOptions
  debugIntrinsicsTranslationOptions =
    defaultTranslationOptions
    { debugIntrinsics = True
    }
  