------------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.LLVM.MemModel.Options
-- Description      : Definition of options that can be tweaked in the memory model
-- Copyright        : (c) Galois, Inc 2019
-- License          : BSD3
-- Maintainer       : Rob Dockins <rdockins@galois.com>
-- Stability        : provisional
------------------------------------------------------------------------

module Lang.Crucible.LLVM.MemModel.Options
  ( MemOptions(..)
  , IndeterminateLoadBehavior(..)
  , defaultMemOptions
  , laxPointerMemOptions
  ) where

-- | This datatype encodes a variety of tweakable settings supported
--   by the LLVM memory model.  They generally involve some weakening
--   of the strict rules of the language standard to allow common
--   idioms, at the cost that reasoning using the resulting memory model
--   is less generalizable (i.e., makes more assumptions about the
--   runtime behavior of the system).
data MemOptions
  = MemOptions
    { MemOptions -> Bool
laxPointerOrdering :: !Bool
      -- ^ Should we allow ordering comparisons on pointers that are
      --   not from the same allocation unit?  This is not allowed
      --   by the C standard, but is nonetheless commonly done.

    , MemOptions -> Bool
laxConstantEquality :: !Bool
      -- ^ Should we allow equality comparisons on pointers to constant
      --   data? Different symbols with the same data are allowed to
      --   be consolidated, so pointer apparently-distinct pointers
      --   will sometimes compare equal if the compiler decides to
      --   consolidate their storage.

    , MemOptions -> Bool
laxLoadsAndStores :: !Bool
      -- ^ Should we relax some of Crucible's validity checks for memory loads
      --   and stores? If 'True', the following checks will be relaxed:
      --
      --   * Reading from previously unwritten memory will succeed rather than
      --     throwing a 'NoSatisfyingWrite' error. The semantics of what it
      --     means to read from uninitialized memory is controlled separately
      --     by the 'indeterminateLoadBehavior' option.
      --
      --   * If reading from a region that isn't allocated or isn't large
      --     enough, Crucible will proceed rather than throw an
      --     'UnreadableRegion' error.
      --
      --   * Reading a value from a pointer with insufficent alignment is not
      --     treated as undefined behavior. That is, Crucible will not throw a
      --     'ReadBadAlignment' error.
      --
      --   * Adding an offset to a pointer that results in a pointer to an
      --     address outside of the allocation is not treated as undefined
      --     behavior. That is, Crucible will not throw a
      --     'PtrAddOffsetOutOfBounds' error.
      --
      --   This option is primarily useful for SV-COMP, which does not treat
      --   the scenarios listed above as fatal errors.

    , MemOptions -> IndeterminateLoadBehavior
indeterminateLoadBehavior :: IndeterminateLoadBehavior
      -- ^ If 'laxLoadsAndStores' is enabled, what should be the semantics of
      --   reading from uninitialized memory? See the Haddocks for
      --   'IndeterminateLoadBehavior' for an explanation of each possible
      --   semantics.
      --
      --   If 'laxLoadsAndStores' is disabled, this option has no effect.

    , MemOptions -> Bool
noSatisfyingWriteFreshConstant :: !Bool
      -- ^ If 'True', for the 'NoSatisfyingWrite' annotation, make a fresh
      --   constant as a proof obligation, which ensures it always fails. But,
      --   because it's a variable, it won't be constant-folded away and it's
      --   relatively sure the annotation will survive. If 'False', annotate
      --   'false'.
    }


-- | What should be the semantics of reading from previously uninitialized
--   memory?
data IndeterminateLoadBehavior
  = StableSymbolic
    -- ^ After allocating memory (be it through @alloca@, @malloc@, @calloc@,
    --   or a similar function), initialize it with a fresh symbolic value of
    --   the corresponding type. As a result, reading from \"uninitialized\"
    --   memory will always succeed, as uninitialized memory will contain
    --   symbolic data if it has not yet been written to. This is \"stable\"
    --   in the sense that reading from the same section of uninitialized
    --   memory multiple times will always yield the same symbolic value.
    --
    --   This is primarily useful for SV-COMP, as these semantics closely align
    --   with SV-COMP's expectations.

  | UnstableSymbolic
    -- ^ Each read from a section of uninitialized memory will return a fresh
    --   symbolic value of the corresponding type. The operative word is
    --   \"fresh\", as each of these symbolic values will be considered
    --   distinct. That is, the symbolic values are \"unstable\". Contrast this
    --   with 'StableSymbolic', in which multiple reads from the same section
    --   of uninitialized memory will all yield the same symbolic value.
    --
    --   One consequence of the 'UnstableSymbolic' approach is that any
    --   pointer can be derefenced, even if it does not actually point to
    --   anything. Dereferencing such a pointer will simply yield a fresh
    --   symbolic value. On the other hand, dereferencing such a pointer
    --   continues to be a Crucible error in 'StableSymbolic'.
  deriving (IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool
(IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool)
-> (IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool)
-> Eq IndeterminateLoadBehavior
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool
== :: IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool
$c/= :: IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool
/= :: IndeterminateLoadBehavior -> IndeterminateLoadBehavior -> Bool
Eq, Int -> IndeterminateLoadBehavior -> ShowS
[IndeterminateLoadBehavior] -> ShowS
IndeterminateLoadBehavior -> String
(Int -> IndeterminateLoadBehavior -> ShowS)
-> (IndeterminateLoadBehavior -> String)
-> ([IndeterminateLoadBehavior] -> ShowS)
-> Show IndeterminateLoadBehavior
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> IndeterminateLoadBehavior -> ShowS
showsPrec :: Int -> IndeterminateLoadBehavior -> ShowS
$cshow :: IndeterminateLoadBehavior -> String
show :: IndeterminateLoadBehavior -> String
$cshowList :: [IndeterminateLoadBehavior] -> ShowS
showList :: [IndeterminateLoadBehavior] -> ShowS
Show)

-- | The default memory model options:
--
-- * Require strict adherence to the language standard regarding pointer
--   equality and ordering.
--
-- * Perform Crucible's default validity checks for memory loads and stores.
defaultMemOptions :: MemOptions
defaultMemOptions :: MemOptions
defaultMemOptions =
  MemOptions
  { laxPointerOrdering :: Bool
laxPointerOrdering = Bool
False
  , laxConstantEquality :: Bool
laxConstantEquality = Bool
False
  , laxLoadsAndStores :: Bool
laxLoadsAndStores = Bool
False
    -- The choice of StableSymbolic here doesn't matter too much, since it
    -- won't have any effect when laxLoadsAndStores is disabled.
  , indeterminateLoadBehavior :: IndeterminateLoadBehavior
indeterminateLoadBehavior = IndeterminateLoadBehavior
StableSymbolic
  , noSatisfyingWriteFreshConstant :: Bool
noSatisfyingWriteFreshConstant = Bool
True
  }


-- | Like 'defaultMemOptions', but allow pointer ordering comparisons
--   and equality comparisons of pointers to constant data.
laxPointerMemOptions :: MemOptions
laxPointerMemOptions :: MemOptions
laxPointerMemOptions =
  MemOptions
defaultMemOptions
  { laxPointerOrdering = True
  , laxConstantEquality = True
  }